Commit 9cd6b3d0 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Mlw: type inference with snapshots

parent ec1896ac
This diff is collapsed.
......@@ -653,9 +653,11 @@ let e_exec ({c_cty = cty} as c) = match cty.cty_args with
if List.exists (fun a -> not a.pv_ity.ity_imm) al ||
not cty.cty_result.ity_imm then Loc.errorm "This function \
has mutable type signature, it cannot be used as pure";
let func a ity = ity_func a.pv_ity ity in
let ity = List.fold_right func al cty.cty_result in
let ghost = List.exists (fun a -> a.pv_ghost) al in
let effect = eff_bind (Spv.of_list al) cty.cty_effect in
mk_expr (Eexec c) (cty_purify cty) (eff_ghostify ghost effect)
mk_expr (Eexec c) ity (eff_ghostify ghost effect)
| [] ->
mk_expr (Eexec c) cty.cty_result cty.cty_effect
......@@ -483,7 +483,6 @@ let its_inst_regs fresh_reg s tl =
| Ityvar (v, false) ->
sbs, Mtv.find v sbs.isb_var
| Ityvar (v,true) ->
try sbs, Mtv.find v sbs.isb_pur with Not_found ->
sbs, ity_purify (Mtv.find v sbs.isb_var)
and reg_inst sbs r =
try sbs, Mreg.find r sbs.isb_reg with Not_found ->
......@@ -1338,8 +1337,9 @@ let print_spec args pre post xpost oldies eff fmt ity =
forget_var v in
let print_xpost fmt (xs,ql) =
Pp.print_list Pp.nothing (print_xpost xs) fmt ql in
Pp.print_list_pre print_pvty fmt args;
Pp.print_option print_result fmt ity;
fprintf fmt "@[<hov 4>%a%a@]"
(Pp.print_list_pre print_pvty) args
(Pp.print_option print_result) ity;
if eff.eff_oneway then pp_print_string fmt " diverges";
let reads = List.fold_right Spv.remove args eff.eff_reads in
if not (Spv.is_empty reads) then fprintf fmt "@\nreads { %a }"
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment