diff options
Diffstat (limited to 'lib/Ast.ml')
| -rw-r--r-- | lib/Ast.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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" |