Commit 509cc380 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Give proper semantics to nested marks in programs.

Suppose that marks appear in order L1, L2, L3 in a program.
Previously, x@L2@L1@L3 would end up with the value of x at mark L1 (the latest mark encountered by WP, that is, the earliest mark in the program).
Now, x@L2@L1@L3 will end up with the value of x at mark L2 (the innermost mark in the expression).

From a WP point of view, the sequence was
x@L2@L1@L3 -> x@L2@L1@now (L3) -> x@L2@L1 (unref) -> x@now@L1 (L2) -> x@now@L1 (unref) -> x@now@now (L1) -> x_L1 (unref).
Now the sequence of substitution is
x@L2@L1@L3 -> x@L2@L1@now (L3) -> x@L2@L1 (unref) -> x@now@L1 (L2) -> x_L2 (unref).
parent 3d12b47d
......@@ -123,23 +123,23 @@ let old_mark lab t = t_subst_single vs_old (t_var lab) t
(* replace [at(t,lab)] with [at(t,'now)] everywhere in formula [f] *)
let erase_mark lab t = t_subst_single lab (t_var vs_now) t
let rec unref s t = match t.t_node with
| Tvar vs ->
let rec unref ~now s t = match t.t_node with
| Tvar vs when now ->
begin try t_var (Mvs.find vs s) with Not_found -> t end
| Tapp (ls, _) when ls_equal ls fs_old ->
assert false
| Tapp (ls, [e;{t_node = Tvar lab}]) when ls_equal ls fs_at ->
if vs_equal lab vs_old then assert false else
if vs_equal lab vs_now then unref s e else
(* do not recurse in at(...) *)
t
if vs_equal lab vs_now then unref ~now:true s e else
(* no longer assume that unmarked variables are at mark 'now *)
t_map (unref ~now:false s) t
| Tlet _ | Tcase _ | Teps _ | Tquant _ ->
(* do not open unless necessary *)
let s = Mvs.set_inter s t.t_vars in
if Mvs.is_empty s then t else
t_map (unref s) t
t_map (unref ~now s) t
| _ ->
t_map (unref s) t
t_map (unref ~now s) t
let find_constructor env ts =
let km = get_known (pure_uc env) in
......@@ -247,7 +247,7 @@ let quantify env rm sreg f =
in
Spv.fold add vars Mvs.empty
in
let f = unref vv' f in
let f = unref ~now:true vv' f in
let f =
let add_update x f =
let v' = Mvs.find x.pv_pure vv' in
......
Markdown is supported
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