Initial

1 files changed, 34 insertions, 0 deletions

diff --git a/src/AST.hs b/src/AST.hs
new file mode 100644
index 0000000..42967bc
--- /dev/null
+++ b/src/AST.hs
@@ -0,0 +1,34 @@
+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
+
+  -- 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)
+
+type Env = Map Name Term