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