Commit aee6644c authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: add e_any

parent aa063026
......@@ -159,8 +159,14 @@ let rec unify d1 d2 =
and unify_reg r1 r2 =
if !r1.rid <> !r2.rid then
if not !r1.ruser then r1 := !r2
else if not !r2.ruser then r2 := !r1
if not !r1.ruser then begin
unify !r1.rity !r2.rity;
r1 := !r2
end
else if not !r2.ruser then begin
unify !r1.rity !r2.rity;
r2 := !r1
end
else begin (* two user regions *)
if not (Lazy.lazy_is_val !r1.reg) then raise Exit;
if not (Lazy.lazy_is_val !r2.reg) then raise Exit;
......
......@@ -284,6 +284,7 @@ and expr_node =
| Ecase of pvsymbol * (ppattern * expr) list
| Eassign of pvsymbol * region * pvsymbol (* mutable pv <- expr *)
| Eghost of expr
| Eany of any_effect
and let_defn = {
let_var : let_var;
......@@ -314,6 +315,12 @@ and variant = {
v_rel : lsymbol option; (* tau tau : prop *)
}
and any_effect = {
aeff_reads : expr list;
aeff_writes : expr list;
aeff_raises : (bool * xsymbol) list;
}
(* smart constructors *)
let e_label ?loc l e = { e with e_label = l; e_loc = loc }
......@@ -611,12 +618,12 @@ let e_case_real pv bl =
let e_case e bl = on_value (fun pv -> e_case_real pv bl) e
exception Immutable of pvsymbol
exception Immutable of expr
let e_assign_real mpv pv =
let e_assign_real me mpv pv =
let r = match mpv.pv_vtv.vtv_mut with
| Some r -> r
| None -> raise (Immutable mpv)
| None -> raise (Immutable me)
in
let ghost = mpv.pv_vtv.vtv_ghost || pv.pv_vtv.vtv_ghost in
let eff = eff_assign eff_empty ~ghost r pv.pv_vtv.vtv_ity in
......@@ -640,14 +647,35 @@ let e_assign_real mpv pv =
e
let e_assign me e =
let assign pv mpv = e_assign_real mpv pv in
let assign pv mpv = e_assign_real me mpv pv in
let assign pv = on_value (assign pv) me in
on_value assign e
let e_ghost e =
mk_expr (Eghost e) (vty_ghostify e.e_vty) e.e_effect e.e_vars
(* Computing the fixpoint on recursive definitions *)
let e_any ee ity =
let add_effect fn eff e =
let vtv = vtv_of_expr e in
let r = match vtv.vtv_mut with
| Some r -> r
| None -> raise (Immutable e) in
fn eff ?ghost:(Some vtv.vtv_ghost) r
in
let add_raise eff (ghost,xs) =
eff_raise eff ~ghost xs
in
let eff = eff_empty in
let eff = List.fold_left (add_effect eff_read) eff ee.aeff_reads in
let eff = List.fold_left (add_effect eff_read) eff ee.aeff_writes in
let eff = List.fold_left add_raise eff ee.aeff_raises in
let eff = Sreg.fold (fun r e -> eff_reset e r) ity.ity_vars.vars_reg eff in
let vars = Mid.empty in
let vars = List.fold_right add_e_vars ee.aeff_reads vars in
let vars = List.fold_right add_e_vars ee.aeff_writes vars in
mk_expr (Eany ee) (VTvalue (vty_value ity)) eff vars
(* Compute the fixpoint on recursive definitions *)
let vars_equal vs1 vs2 =
Stv.equal vs1.vars_tv vs2.vars_tv &&
......@@ -706,6 +734,12 @@ let rec expr_subst psm e = match e.e_node with
e_case_real pv (List.map (fun (pp,e) -> pp, expr_subst psm e) bl)
| Eghost e ->
e_ghost (expr_subst psm e)
| Eany ee ->
e_any {
aeff_reads = List.map (expr_subst psm) ee.aeff_reads;
aeff_writes = List.map (expr_subst psm) ee.aeff_writes;
aeff_raises = ee.aeff_raises;
} (vtv_of_expr e).vtv_ity
| Elogic _ | Evalue _ | Earrow _ | Eassign _ -> e
and create_rec_defn defl =
......
......@@ -137,6 +137,7 @@ and expr_node = private
| Ecase of pvsymbol * (ppattern * expr) list
| Eassign of pvsymbol * region * pvsymbol (* mutable pv <- expr *)
| Eghost of expr
| Eany of any_effect
and let_defn = private {
let_var : let_var;
......@@ -167,6 +168,15 @@ and variant = {
v_rel : lsymbol option; (* tau tau : prop *)
}
(* TODO? Every top region in the type of Eany is reset.
This is enough for our current purposes, but we might
need to be more flexible later. *)
and any_effect = {
aeff_reads : expr list; (* for a ghost read, use a ghost expression *)
aeff_writes : expr list; (* for a ghost write, use a ghost expression *)
aeff_raises : (bool * xsymbol) list; (* ghost raise * exception symbol *)
}
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
......@@ -200,12 +210,14 @@ val e_rec : rec_defn list -> expr -> expr
val e_if : expr -> expr -> expr -> expr
val e_case : expr -> (ppattern * expr) list -> expr
exception Immutable of pvsymbol
exception Immutable of expr
val e_assign : expr -> expr -> expr
val e_ghost : expr -> expr
val e_any : any_effect -> ity -> expr
(* TODO: when should we check for escaping identifiers (regions?)
in pre/post/xpost/effects? Here or in WP? *)
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