From 04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 17 Jun 2024 17:41:38 +0200 Subject: implement typechecking --- lib/Ast.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'lib/Ast.ml') diff --git a/lib/Ast.ml b/lib/Ast.ml index 70e03dd..35611ac 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -1,11 +1,11 @@ type raw_ident = Yuujinchou.Trie.path type ident = raw_ident Asai.Range.located -type raw_arg = { name : ident; ty : expr } -and arg = raw_arg Asai.Range.located +type arg = ident * expr and raw_expr = | Var of raw_ident + | Check of expr * expr | Pi of arg * expr | Lam of ident * expr | App of expr * expr @@ -27,18 +27,18 @@ and raw_expr = and expr = raw_expr Asai.Range.located +(* TODO this is the same as Syntax.pretty.pp_name *) let dump_raw_ident fmt (id : raw_ident) = Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.') Format.pp_print_string fmt 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 +let rec dump_arg fmt ((name, tp) : arg) = + Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr tp and dump_raw_expr fmt = function | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident 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" -- cgit 1.4.1