    {-# LANGUAGE CPP, DeriveDataTypeable #-}

    {-| The concrete syntax is a raw representation of the program text
        without any desugaring at all.  This is what the parser produces.
        The idea is that if we figure out how to keep the concrete syntax
        around, it can be printed exactly as the user wrote it.
    -}
    module Agda.Syntax.Concrete
        ( -- * Expressions
          Expr(..)
        , module Agda.Syntax.Concrete.Name
        , appView, AppView(..)
          -- * Bindings
        , LamBinding(..)
        , TypedBindings(..)
        , TypedBinding(..)
        , BoundName(..), mkBoundName_
        , Telescope -- (..)
          -- * Declarations
        , Declaration(..)
        , TypeSignature
        , Constructor
        , Field
        , ImportDirective(..), UsingOrHiding(..), ImportedName(..)
        , Renaming(..), AsName(..)
        , defaultImportDir
        , OpenShortHand(..)
        , LHS(..), Pattern(..)
        , RHS(..), WhereClause(..)
        , Pragma(..)
        , Module
        , topLevelModuleName
        )
        where

    import Data.Generics hiding (Fixity, Infix)

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Fixity
    import Agda.Syntax.Literal

    import Agda.Syntax.Concrete.Name

    import Agda.Utils.Impossible
    #include "../undefined.h"

    -- | Concrete expressions. Should represent exactly what the user wrote.
    data Expr
    	= Ident QName			       -- ^ ex: @x@
    	| Lit Literal			       -- ^ ex: @1@ or @\"foo\"@
    	| QuestionMark !Range (Maybe Nat)      -- ^ ex: @?@ or @{! ... !}@
    	| Underscore !Range (Maybe Nat)	       -- ^ ex: @_@
    	| RawApp !Range [Expr]		       -- ^ before parsing operators
    	| App !Range Expr (NamedArg Expr)      -- ^ ex: @e e@, @e {e}@, or @e {x = e}@
    	| OpApp !Range Name [Expr]	       -- ^ ex: @e + e@
            | WithApp !Range Expr [Expr]           -- ^ ex: @e | e1 | .. | en@
    	| HiddenArg !Range (Named String Expr) -- ^ ex: @{e}@ or @{x=e}@
    	| Lam !Range [LamBinding] Expr	       -- ^ ex: @\\x {y} -> e@ or @\\(x:A){y:B} -> e@
            | AbsurdLam !Range Hiding              -- ^ ex: @\\ ()@
    	| Fun !Range Expr Expr		       -- ^ ex: @e -> e@ or @{e} -> e@
    	| Pi Telescope Expr		       -- ^ ex: @(xs:e) -> e@ or @{xs:e} -> e@
    	| Set !Range			       -- ^ ex: @Set@
    	| Prop !Range			       -- ^ ex: @Prop@
    	| SetN !Range Nat		       -- ^ ex: @Set0, Set1, ..@
    	| Rec !Range [(Name, Expr)]	       -- ^ ex: @record {x = a; y = b}@
    	| Let !Range [Declaration] Expr	       -- ^ ex: @let Ds in e@
    	| Paren !Range Expr		       -- ^ ex: @(e)@
    	| Absurd !Range			       -- ^ ex: @()@ or @{}@, only in patterns
    	| As !Range Name Expr		       -- ^ ex: @x\@p@, only in patterns
    	| Dot !Range Expr		       -- ^ ex: @.p@, only in patterns
            | ETel Telescope                       -- ^ only used for printing telescopes
        deriving (Typeable, Data, Eq)

    -- | Concrete patterns. No literals in patterns at the moment.
    data Pattern
    	= IdentP QName
    	| AppP Pattern (NamedArg Pattern)
    	| RawAppP !Range [Pattern]
    	| OpAppP !Range Name [Pattern]
    	| HiddenP !Range (Named String Pattern)
    	| ParenP !Range Pattern
    	| WildP !Range
    	| AbsurdP !Range
    	| AsP !Range Name Pattern
    	| DotP !Range Expr
    	| LitP Literal
        deriving (Typeable, Data, Eq)

    -- | A lambda binding is either domain free or typed.
    data LamBinding
    	= DomainFree Hiding BoundName -- ^ . @x@ or @{x}@
    	| DomainFull TypedBindings    -- ^ . @(xs:e,..,ys:e')@ or @{xs:e,..,ys:e'}@
        deriving (Typeable, Data, Eq)

    -- | A sequence of typed bindings with hiding information. Appears in dependent
    --   function spaces, typed lambdas, and telescopes.
    data TypedBindings = TypedBindings !Range Hiding [TypedBinding]
    	-- ^ . @(xs:e;..;ys:e')@ or @{xs:e;..;ys:e'}@
        deriving (Typeable, Data, Eq)

    data BoundName = BName { boundName   :: Name
                           , bnameFixity :: Fixity
                           }
        deriving (Typeable, Data, Eq)

    mkBoundName_ :: Name -> BoundName
    mkBoundName_ x = BName x defaultFixity

    -- | A typed binding.
    data TypedBinding
    	= TBind !Range [BoundName] Expr   -- Binding @x1,..,xn:A@
    	| TNoBind Expr		    -- No binding @A@, equivalent to @_ : A@.
        deriving (Typeable, Data, Eq)

    -- | A telescope is a sequence of typed bindings. Bound variables are in scope
    --   in later types. Or it's the mysterious Thierry-function-telescope. Only it's not.
    type Telescope = [TypedBindings]
    -- data Telescope = TeleBind [TypedBindings]
    -- 	       | TeleFun Telescope Telescope
    --     deriving (Typeable, Data, Eq)

    {-| Left hand sides can be written in infix style. For example:

        > n + suc m = suc (n + m)
        > (f ∘ g) x = f (g x)

       We use fixity information to see which name is actually defined.
    -}
    data LHS = LHS Pattern [Pattern] [RewriteEqn] [WithExpr]
             -- ^ original pattern, with-patterns, rewrite equations and with-expressions
             | Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
             -- ^ new with-patterns, rewrite equations and with-expressions
      deriving (Typeable, Data, Eq)

    type RewriteEqn = Expr
    type WithExpr   = Expr

    data RHS = AbsurdRHS
    	 | RHS Expr
        deriving (Typeable, Data, Eq)

    data WhereClause = NoWhere | AnyWhere [Declaration] | SomeWhere Name [Declaration]
      deriving (Typeable, Data, Eq)

    -- | The things you are allowed to say when you shuffle names between name
    --   spaces (i.e. in @import@, @namespace@, or @open@ declarations).
    data ImportDirective
    	= ImportDirective
    	    { importDirRange	:: !Range
    	    , usingOrHiding	:: UsingOrHiding
    	    , renaming		:: [Renaming]
    	    , publicOpen	:: Bool	-- ^ Only for @open@. Exports the opened names from the current module.
    	    }
        deriving (Typeable, Data, Eq)

    defaultImportDir :: ImportDirective
    defaultImportDir = ImportDirective noRange (Hiding []) [] False

    data UsingOrHiding
    	= Hiding [ImportedName]
    	| Using  [ImportedName]
        deriving (Typeable, Data, Eq)

    -- | An imported name can be a module or a defined name
    data ImportedName = ImportedModule  { importedName :: Name }
    		  | ImportedName    { importedName :: Name }
        deriving (Typeable, Data, Eq, Ord)

    instance Show ImportedName where
        show (ImportedModule x) = "module " ++ show x
        show (ImportedName   x) = show x

    data Renaming = Renaming { renFrom    :: ImportedName
                               -- ^ Rename from this name.
                             , renTo      :: Name
                               -- ^ To this one.
                             , renToRange :: Range
                               -- ^ The range of the \"to\" keyword. Retained
                               --   for highlighting purposes.
                             }
        deriving (Eq, Typeable, Data)

    data AsName = AsName { asName  :: Name
                           -- ^ The \"as\" name.
                         , asRange :: Range
                           -- ^ The range of the \"as\" keyword. Retained
                           --   for highlighting purposes.
                         }
        deriving (Eq, Typeable, Data)

    {--------------------------------------------------------------------------
        Declarations
     --------------------------------------------------------------------------}

    -- | Just type signatures.
    type TypeSignature   = Declaration

    -- | A constructor or field declaration is just a type signature.
    type Constructor = TypeSignature
    type Field	 = TypeSignature

    {-| The representation type of a declaration. The comments indicate
        which type in the intended family the constructor targets.
    -}
    data Declaration
    	= TypeSig Name Expr
            | Field Hiding Name Expr
    	| FunClause LHS RHS WhereClause
    	| Data        !Range Induction Name [TypedBindings] Expr [Constructor]
    	| Record      !Range Name (Maybe Name) [TypedBindings] Expr [Declaration]
              -- ^ The optional name is a name for the record constructor.
    	| Infix Fixity [Name]
    	| Mutual      !Range [Declaration]
    	| Abstract    !Range [Declaration]
    	| Private     !Range [Declaration]
    	| Postulate   !Range [TypeSignature]
    	| Primitive   !Range [TypeSignature]
    	| Open        !Range QName ImportDirective
    	| Import      !Range QName (Maybe AsName) OpenShortHand ImportDirective
    	| ModuleMacro !Range  Name [TypedBindings] Expr OpenShortHand ImportDirective
    	| Module      !Range QName [TypedBindings] [Declaration]
    	| Pragma      Pragma
        deriving (Eq, Typeable, Data)

    data OpenShortHand = DoOpen | DontOpen
        deriving (Eq, Typeable, Data, Show)

    -- Pragmas ----------------------------------------------------------------

    data Pragma = OptionsPragma     !Range [String]
    	    | BuiltinPragma     !Range String Expr
                | CompiledDataPragma !Range QName String [String]
                | CompiledTypePragma !Range QName String
                | CompiledPragma    !Range QName String
                | ImportPragma      !Range String
                  -- ^ Invariant: The string must be a valid Haskell
                  -- module name.
                | ImpossiblePragma !Range
        deriving (Eq, Typeable, Data)

    ---------------------------------------------------------------------------

    -- | Modules: Top-level pragmas plus other top-level declarations.

    type Module = ([Pragma], [Declaration])

    -- | Computes the top-level module name.
    --
    -- Precondition: The 'Module' has to be well-formed.

    topLevelModuleName :: Module -> TopLevelModuleName
    topLevelModuleName (_, []) = __IMPOSSIBLE__
    topLevelModuleName (_, ds) = case last ds of
      Module _ n _ _ -> toTopLevelModuleName n
      _              -> __IMPOSSIBLE__

    {--------------------------------------------------------------------------
        Views
     --------------------------------------------------------------------------}

    -- | The 'Expr' is not an application.
    data AppView = AppView Expr [NamedArg Expr]

    appView :: Expr -> AppView
    appView (App r e1 e2) = vApp (appView e1) e2
        where
    	vApp (AppView e es) arg = AppView e (es ++ [arg])
    appView (RawApp _ (e:es)) = AppView e $ map arg es
        where
    	arg (HiddenArg _ e) = Arg Hidden e
    	arg e		    = Arg NotHidden (unnamed e)
    appView e = AppView e []

    {--------------------------------------------------------------------------
        Instances
     --------------------------------------------------------------------------}

    instance HasRange Expr where
        getRange e =
    	case e of
    	    Ident x		-> getRange x
    	    Lit x		-> getRange x
    	    QuestionMark r _	-> r
    	    Underscore r _	-> r
    	    App r _ _		-> r
    	    RawApp r _		-> r
    	    OpApp r _ _		-> r
                WithApp r _ _       -> r
    	    Lam r _ _		-> r
                AbsurdLam r _       -> r
    	    Fun r _ _		-> r
    	    Pi b e		-> fuseRange b e
    	    Set r		-> r
    	    Prop r		-> r
    	    SetN r _		-> r
    	    Let r _ _		-> r
    	    Paren r _		-> r
    	    As r _ _		-> r
    	    Dot r _		-> r
    	    Absurd r		-> r
    	    HiddenArg r _	-> r
    	    Rec r _		-> r
                ETel tel            -> getRange tel

    -- instance HasRange Telescope where
    --     getRange (TeleBind bs) = getRange bs
    --     getRange (TeleFun x y) = fuseRange x y

    instance HasRange TypedBindings where
        getRange (TypedBindings r _ _) = r

    instance HasRange TypedBinding where
        getRange (TBind r _ _) = r
        getRange (TNoBind e)   = getRange e

    instance HasRange LamBinding where
        getRange (DomainFree _ x)	= getRange x
        getRange (DomainFull b)	= getRange b

    instance HasRange BoundName where
      getRange = getRange . boundName

    instance HasRange WhereClause where
      getRange  NoWhere	    = noRange
      getRange (AnyWhere ds)    = getRange ds
      getRange (SomeWhere _ ds) = getRange ds

    instance HasRange Declaration where
        getRange (TypeSig x t)		= fuseRange x t
        getRange (Field _ x t)              = fuseRange x t
        getRange (FunClause lhs rhs wh)	= fuseRange lhs rhs `fuseRange` wh
        getRange (Data r _ _ _ _ _)		= r
        getRange (Record r _ _ _ _ _)	= r
        getRange (Mutual r _)		= r
        getRange (Abstract r _)		= r
        getRange (Open r _ _)		= r
        getRange (ModuleMacro r _ _ _ _ _)	= r
        getRange (Import r _ _ _ _)		= r
        getRange (Private r _)		= r
        getRange (Postulate r _)		= r
        getRange (Primitive r _)		= r
        getRange (Module r _ _ _)		= r
        getRange (Infix f _)		= getRange f
        getRange (Pragma p)			= getRange p

    instance HasRange LHS where
      getRange (LHS p ps eqns ws) = fuseRange p (fuseRange ps (eqns ++ ws))
      getRange (Ellipsis r _ _ _) = r

    instance HasRange RHS where
        getRange AbsurdRHS = noRange
        getRange (RHS e)   = getRange e

    instance HasRange Pragma where
        getRange (OptionsPragma r _)          = r
        getRange (BuiltinPragma r _ _)        = r
        getRange (CompiledDataPragma r _ _ _) = r
        getRange (CompiledTypePragma r _ _)   = r
        getRange (CompiledPragma r _ _)       = r
        getRange (ImportPragma r _)           = r
        getRange (ImpossiblePragma r)         = r

    instance HasRange UsingOrHiding where
        getRange (Using xs)	    = getRange xs
        getRange (Hiding xs)    = getRange xs

    instance HasRange ImportDirective where
        getRange = importDirRange

    instance HasRange ImportedName where
        getRange (ImportedName x)	= getRange x
        getRange (ImportedModule x)	= getRange x

    instance HasRange Renaming where
      getRange r = getRange (renFrom r, renTo r)

    instance HasRange AsName where
      getRange a = getRange (asRange a, asName a)

    instance HasRange Pattern where
        getRange (IdentP x)		= getRange x
        getRange (AppP p q)		= fuseRange p q
        getRange (OpAppP r _ _)	= r
        getRange (RawAppP r _)	= r
        getRange (ParenP r _)	= r
        getRange (WildP r)		= r
        getRange (AsP r _ _)	= r
        getRange (AbsurdP r)	= r
        getRange (LitP l)		= getRange l
        getRange (HiddenP r _)	= r
        getRange (DotP r _)		= r