diff options
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index c500beb1..b0fdb2dc 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -383,7 +383,14 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e)) | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) - | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector")) + | Tapp("implicit",[TA_nexp r]) -> + (match r.nexp with + | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" + kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e)) + | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id %a) %a)) (%a,%a))@]" + kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e)) + | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const")) + | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit")) | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload") in print_e ppf e @@ -906,7 +913,12 @@ let doc_exp, doc_let = (match r.nexp with | Nconst bi -> utf8string (Big_int.string_of_big_int bi) | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) - | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector")) + | Tapp("implicit",[TA_nexp r]) -> + (match r.nexp with + | Nconst bi -> utf8string (Big_int.string_of_big_int bi) + | Nvar v -> utf8string v + | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const")) + | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector, non-implicit")) (* XXX missing case AAA internal_cast should never have an overload, if it's been seen it's a bug *) |