diff options
| -rw-r--r-- | lib/Ast.ml | 40 |
1 files changed, 20 insertions, 20 deletions
@@ -27,41 +27,41 @@ and raw_expr = and expr = raw_expr Asai.Range.located -let pp_raw_ident fmt (id : raw_ident) = Format.pp_print_list +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 pp_ident fmt ({ value; _ } : ident) = pp_raw_ident fmt value +let dump_ident fmt ({ value; _ } : ident) = dump_raw_ident fmt value -let rec pp_raw_arg fmt ({ name; ty } : raw_arg) = - Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" pp_ident name pp_expr ty +let rec dump_raw_arg fmt ({ name; ty } : raw_arg) = + Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr ty -and pp_arg fmt ({ value; _ } : arg) = pp_raw_arg fmt value +and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value -and pp_raw_expr fmt = function - | Var id -> Format.fprintf fmt "Var @[%a@]" pp_raw_ident id +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@])@]" - pp_ident motive_var - pp_expr motive_body - pp_expr true_case - pp_expr false_case - pp_expr scrut + 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@])@]" pp_arg dom pp_expr cod + Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod | Lam (var, body) -> - Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" pp_ident var pp_expr body + Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr body | App (fn, arg) -> - Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" pp_expr fn pp_expr arg + Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg | Sg (fst, snd) -> - Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" pp_arg fst pp_expr snd + Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd | Pair (fst, snd) -> - Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" pp_expr fst pp_expr snd - | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" pp_expr p - | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" pp_expr p + 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 pp_expr fmt ({ value; _ } : expr) = pp_raw_expr fmt value +and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value |