split code into smaller libraries and make a better repl

1 files changed, 67 insertions, 0 deletions

diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml
new file mode 100644
index 0000000..1a1d4c5
--- /dev/null
+++ b/src/ast/Ast.ml
@@ -0,0 +1,67 @@
+type ident = Ident.t Asai.Range.located
+type local_name = Ident.local Asai.Range.located
+
+type arg = local_name * expr
+
+and raw_expr =
+  | Var of Ident.t
+  | Check of expr * expr
+  | Pi of arg * expr
+  | Lam of local_name * expr
+  | App of expr * expr
+  | Sg of arg * expr
+  | Pair of expr * expr
+  | Fst of expr
+  | Snd of expr
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive_var : local_name;
+      motive_body : expr;
+      true_case : expr;
+      false_case : expr;
+      scrut : expr;
+    }
+
+and expr = raw_expr Asai.Range.located
+
+let dump_ident fmt ({ value; _ } : ident) = Ident.pp fmt value
+
+let dump_local_name fmt ({ value; _ } : local_name) = match value with
+  | Some name -> Format.pp_print_string fmt name
+  | None -> Format.pp_print_char fmt '_'
+
+let rec dump_arg fmt ((name, tp) : arg) =
+  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_local_name name dump_expr tp
+
+and dump_raw_expr fmt = function
+  | Var id -> Format.fprintf fmt "Var @[%a@]" Ident.pp id
+  | Check (tm, tp) -> Format.fprintf fmt "@[%a@] : @[%a@]" dump_expr tm dump_expr tp
+  | 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_local_name 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_local_name 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
+  | Type -> Format.pp_print_string fmt "Type"
+
+and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value