blob: ba018f51f21b50aa6817c2075b64fd405449e1cc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
module AST where
import Data.Map.Strict (Map)
data Nat = Z | S Nat
deriving (Show)
type Name = String
data Term
= TSet Term -- ^ The n-th universe (n : Level)
| TVar Name -- ^ variable
| TPi Name Term Term -- ^ Pi: (x : A) -> B
| TLam Name Term Term -- ^ λ(x : A). B
| TApp Term Term -- ^ application
| TLift Term -- ^ Γ |- t : Set i ~> Γ |- lift t : Set (Succ i)
| TLevel -- ^ The Level type
| TLevelUniv -- ^ The LevelUniv type: the type of Level
| TIZero -- ^ Level zero
| TIMax Term Term -- ^ Maximum of two levels
| TISucc Term -- ^ Level + 1
| TAnnot (OfType Term Term) -- ^ term : type
-- Temporary stuff until we have proper inductive types:
| TOne -- ^ The unit type
| TUnit -- ^ The element of the unit type
| TSigma Name Term Term -- ^ Sigma: (x : A) × B
| TPair Term Term -- ^ Dependent pair
| TProj1 Term -- ^ First projection of a dependent pair
| TProj2 Term -- ^ Second projection of a dependent pair
deriving (Show)
data Definition = Definition Name (OfType Term Term)
deriving (Show)
type Env = Map Name Term
data OfType a b = a :| b
deriving (Show)
infix 1 :|
|
