Commit 76cd6017 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: assignment

parent e48e8ed3
......@@ -110,7 +110,7 @@ and expr_node =
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Eif of pvsymbol * expr * expr
| Eassign of pvsymbol * pvsymbol (* mutable pv <- expr *)
| Eassign of pvsymbol * region * pvsymbol (* mutable pv <- expr *)
| Eany
and let_defn = {
......@@ -210,6 +210,9 @@ let e_inst ps sbs =
else ps.ps_vta
in
mk_expr (Einst (ps,sbs)) (VTarrow vta) eff_empty tvs regs
(* FIXME? We store the substitution in the expr as given, though it could
be restricted to type variables and regions (both top and subordinate)
of ps_vta.vta_tvs/regs. *)
let e_app_real pa pv =
let tvs = add_pv_tvs (add_pa_tvs Mid.empty pa) pv in
......@@ -383,15 +386,34 @@ let e_if_real pv e1 e2 =
let vtv2 = vtv_of_expr e2 in
ity_equal_check vtv1.vtv_ity vtv2.vtv_ity;
ity_equal_check pv.pv_vtv.vtv_ity ity_bool;
let ghost = pv.pv_vtv.vtv_ghost || vtv1.vtv_ghost || vtv2.vtv_ghost in
let vtv = vty_value ~ghost vtv1.vtv_ity in
let eff = eff_union e1.e_effect e2.e_effect in
let tvs = add_expr_tvs (add_expr_tvs (add_pv_tvs Mid.empty pv) e1) e2 in
let regs = add_expr_regs (add_expr_regs (add_pv_regs Mid.empty pv) e1) e2 in
mk_expr (Eif (pv,e1,e2)) (VTvalue vtv) eff tvs regs
let ghost = pv.pv_vtv.vtv_ghost || vtv1.vtv_ghost || vtv2.vtv_ghost in
let vty = VTvalue (vty_value ~ghost vtv1.vtv_ity) in
mk_expr (Eif (pv,e1,e2)) vty eff tvs regs
let e_if e e1 e2 = on_value (fun pv -> e_if_real pv e1 e2) e
exception Immutable of pvsymbol
let e_assign_real mpv pv =
let r = match mpv.pv_vtv.vtv_mut with
| Some r -> r
| None -> raise (Immutable mpv)
in
let eff = eff_assign eff_empty r pv.pv_vtv.vtv_ity in
let tvs = add_pv_tvs (add_pv_tvs Mid.empty mpv) pv in
let regs = add_pv_regs (add_pv_regs Mid.empty mpv) pv in
let ghost = mpv.pv_vtv.vtv_ghost || pv.pv_vtv.vtv_ghost in
let vty = VTvalue (vty_value ~ghost ity_unit) in
mk_expr (Eassign (mpv,r,pv)) vty eff tvs regs
let e_assign me e =
let assign pv mpv = e_assign_real mpv pv in
let assign pv = on_value (assign pv) me in
on_value assign e
(*
- A "proper type" of a vty [v] is [v] with empty specification
(effect/pre/post/xpost). Basically, it is formed from pv_ity's
......
......@@ -122,7 +122,7 @@ and expr_node = private
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Eif of pvsymbol * expr * expr
| Eassign of pvsymbol * pvsymbol (* mutable pv <- expr *)
| Eassign of pvsymbol * region * pvsymbol (* mutable pv <- expr *)
| Eany
and let_defn = private {
......@@ -161,9 +161,6 @@ val e_value : pvsymbol -> expr
val e_arrow : pasymbol -> expr
val e_inst : psymbol -> ity_subst -> expr
(* FIXME? We store the substitution in the expr as given, though it could
be restricted to type variables and regions (both top and subordinate)
of ps_vta.vta_tvs/regs. *)
exception ValueExpected of expr
exception ArrowExpected of expr
......@@ -186,6 +183,10 @@ val e_let : let_defn -> expr -> expr
val e_if : expr -> expr -> expr -> expr
exception Immutable of pvsymbol
val e_assign : expr -> expr -> expr
(* TODO: when should we check for escaping identifiers (regions?)
in pre/post/xpost/effects? Here or in WP? *)
......@@ -383,6 +383,7 @@ let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
let ity_int = ity_of_ty Ty.ty_int
let ity_bool = ity_of_ty Ty.ty_bool
let ity_unit = ity_of_ty (Ty.ty_tuple [])
(** computation types (with effects) *)
......@@ -446,7 +447,10 @@ let eff_assign e r ty =
let e = eff_write e r in
let sub = ity_match ity_subst_empty r.reg_ity ty in
(* assignment cannot instantiate type variables *)
if not (Mtv.is_empty sub.ity_subst_tv) then
let check tv ity = match ity.ity_node with
| Ityvar tv' -> tv_equal tv tv'
| _ -> false in
if not (Mtv.for_all check sub.ity_subst_tv) then
raise (TypeMismatch (r.reg_ity,ty));
(* r:t[r1,r2] <- t[r1,r1] introduces an alias *)
let add_right _ v s = Sreg.add_new (IllegalAlias v) v s in
......@@ -455,7 +459,7 @@ let eff_assign e r ty =
let add_right k v m = if reg_equal k v then m else Mreg.add v None m in
let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
(* ...except those which occur on the lhs : they are preserved under r *)
let add_left k v m = if reg_equal k v then m else Mreg.add v (Some r) m in
let add_left k v m = if reg_equal k v then m else Mreg.add k (Some r) m in
let reset = Mreg.fold add_left sub.ity_subst_reg reset in
{ e with eff_resets = Mreg.union join_reset e.eff_resets reset }
......
......@@ -129,6 +129,7 @@ val ity_pure : ity -> bool
val ity_int : ity
val ity_bool : ity
val ity_unit : ity
exception RegionMismatch of region * region
exception TypeMismatch of ity * ity
......
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