    {-# OPTIONS_GHC -fwarn-missing-signatures #-}

    module Agda.Syntax.Reflected where

    import Agda.Syntax.Common
    import Agda.Syntax.Literal
    import Agda.Syntax.Abstract.Name

    type Args       = [Arg Term]

    data Elim' a = Apply (Arg a) -- no record projections for now
      deriving (Show)
    type Elim = Elim' Term
    type Elims = [Elim]

    argsToElims :: Args -> Elims
    argsToElims = map Apply

    data Abs a = Abs String a
      deriving (Show)

    data Term = Var Int Elims
              | Con QName Elims
              | Def QName Elims
              | Meta MetaId Elims
              | Lam Hiding (Abs Term)
              | ExtLam [Clause] Elims
              | Pi (Dom Type) (Abs Type)
              | Sort Sort
              | Lit Literal
              | Unknown
      deriving (Show)

    type Type = Term

    data Sort = SetS Term
              | LitS Integer
              | UnknownS
      deriving (Show)

    data Pattern = ConP QName [Arg Pattern]
                 | DotP
                 | VarP String
                 | LitP Literal
                 | AbsurdP
                 | ProjP QName
      deriving (Show)

    data Clause = Clause [Arg Pattern] Term | AbsurdClause [Arg Pattern]
      deriving (Show)

    data Definition = FunDef Type [Clause]
                    | DataDef   -- nothing for now
                    | RecordDef -- nothing for now
                    | DataConstructor
                    | Axiom
                    | Primitive
      deriving (Show)