1{-# OPTIONS_GHC -fwarn-missing-signatures #-} 2 3module Agda.Syntax.Reflected where 4 5import Data.Text (Text) 6 7import Agda.Syntax.Common 8import Agda.Syntax.Literal 9import Agda.Syntax.Abstract.Name 10import Agda.Syntax.Internal (Dom) 11 12import Agda.Utils.List1 (List1, pattern (:|)) 13import qualified Agda.Utils.List1 as List1 14 15type Args = [Arg Term] 16 17data Elim' a = Apply (Arg a) -- no record projections for now 18 deriving (Show) 19type Elim = Elim' Term 20type Elims = [Elim] 21 22argsToElims :: Args -> Elims 23argsToElims = map Apply 24 25data Abs a = Abs String a 26 deriving (Show) 27 28data Term = Var Int Elims 29 | Con QName Elims 30 | Def QName Elims 31 | Meta MetaId Elims 32 | Lam Hiding (Abs Term) 33 | ExtLam (List1 Clause) Elims 34 | Pi (Dom Type) (Abs Type) 35 | Sort Sort 36 | Lit Literal 37 | Unknown 38 deriving (Show) 39 40type Type = Term 41 42data Sort = SetS Term 43 | LitS Integer 44 | PropS Term 45 | PropLitS Integer 46 | InfS Integer 47 | UnknownS 48 deriving (Show) 49 50data Pattern = ConP QName [Arg Pattern] 51 | DotP Term 52 | VarP Int 53 | LitP Literal 54 | AbsurdP Int 55 | ProjP QName 56 deriving (Show) 57 58data Clause 59 = Clause 60 { clauseTel :: [(Text, Arg Type)] 61 , clausePats :: [Arg Pattern] 62 , clauseRHS :: Term 63 } 64 | AbsurdClause 65 { clauseTel :: [(Text, Arg Type)] 66 , clausePats :: [Arg Pattern] 67 } 68 deriving (Show) 69 70data Definition = FunDef Type [Clause] 71 | DataDef -- nothing for now 72 | RecordDef -- nothing for now 73 | DataConstructor 74 | Axiom 75 | Primitive 76 deriving (Show) 77