1 files changed, 0 insertions, 67 deletions
diff --git a/lib/Ast.ml b/lib/Ast.ml
deleted file mode 100644
index 1a1d4c5..0000000
--- a/lib/Ast.ml
+++ /dev/null
@@ -1,67 +0,0 @@
-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