diff options
| author | Kathy Gray | 2014-06-04 18:17:32 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-06-04 18:17:32 +0100 |
| commit | 68ea054c0a26fd8da8198a449fc248ed621311c5 (patch) | |
| tree | 2d404f4a8f5a13ea06d7f04b3a873a170b3d5ec9 /src/pretty_print.ml | |
| parent | 978f5bc208248afe284bb9488c4e892e9315c8a2 (diff) | |
Fixup type coercions and overloading
Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions.
Warning: test_power does not run as not all overloaded funcitons are implemented
Warning: vector concatenation does not pretty print to sail source yet
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 3d8b0e91..7ade113c 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -348,6 +348,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot | E_vector_update_subrange(v,e1,e2,e3) -> fprintf ppf "@[<0>(E_aux (%a %a %a %a %a) (%a, %a))@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 pp_lem_l l pp_annot annot + | E_vector_append(v1,v2) -> + fprintf ppf "@[<0>(E_aux (E_vector_append %a %a) (%a, %a))@]" pp_lem_exp v1 pp_lem_exp v2 pp_lem_l l pp_annot annot | E_list(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot | E_cons(e1,e2) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> |