diff options
| author | Thomas Bauereiss | 2017-12-05 17:05:22 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-12-06 14:54:28 +0000 |
| commit | c3c3c40a1d4f81448d8356317e88be2b04363df7 (patch) | |
| tree | 4caeea3f28af968a59241df7a7ebd1828fd61086 /src/pretty_print_lem_ast.ml | |
| parent | 4a7d6e6d7e9221a19bc50c627b5714e45b1748bc (diff) | |
Make AST after rewriting for Lem backend type-checkable
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
Diffstat (limited to 'src/pretty_print_lem_ast.ml')
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index a91a6f08..4cb7bef2 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -616,7 +616,7 @@ let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) = fprintf ppf "@[<0>(DEC_aux (DEC_typ_alias %a %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot -let pp_lem_def ppf d = +let rec pp_lem_def ppf d = match d with | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec @@ -628,6 +628,7 @@ let pp_lem_def ppf d = | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec | DEF_comm d -> fprintf ppf "" | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_big_int n) pp_lem_id id + | DEF_internal_mutrec f_defs -> List.iter (fun f_def -> pp_lem_def ppf (DEF_fundef f_def)) f_defs | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = |