basic lexer and parser

1 files changed, 62 insertions, 8 deletions

diff --git a/lib/Ast.ml b/lib/Ast.ml
index 4ca7899..002dfff 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -1,8 +1,62 @@
-type expr' =
-  | Var of string
-| Bool
-| True
-| False
-| BoolElim of string
-
-type expr = expr' Asai.Range.located
\ No newline at end of file
+type raw_ident = string
+type ident = raw_ident Asai.Range.located
+
+type raw_arg = { name : ident; ty : expr }
+and arg = raw_arg Asai.Range.located
+
+and raw_expr =
+  | Var of raw_ident
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive_var : ident;
+      motive_body : expr;
+      true_case : expr;
+      false_case : expr;
+      scrut : expr;
+    }
+  | Pi of arg * expr
+  | Lam of ident * expr
+  | App of expr * expr
+  | Sg of arg * expr
+  | Pair of expr * expr
+  | Fst of expr
+  | Snd of expr
+
+and expr = raw_expr Asai.Range.located
+
+let dump_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id
+let dump_ident fmt ({ value; _ } : ident) = dump_raw_ident fmt value
+
+let rec dump_raw_arg fmt ({ name; ty } : raw_arg) =
+  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr ty
+
+and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value
+
+and dump_raw_expr fmt = function
+  | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id
+  | Bool -> Format.pp_print_string fmt "Bool"
+  | True -> Format.pp_print_string fmt "True"
+  | False -> Format.pp_print_string fmt "False"
+  | BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
+      Format.fprintf fmt
+        "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]" dump_ident
+        motive_var dump_expr motive_body dump_expr true_case dump_expr
+        false_case dump_expr scrut
+  | Pi (dom, cod) ->
+      Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
+  | Lam (var, body) ->
+      Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr
+        body
+  | App (fn, arg) ->
+      Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
+  | Sg (fst, snd) ->
+      Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd
+  | Pair (fst, snd) ->
+      Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr
+        snd
+  | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p
+  | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p
+
+and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value