Commit bcbf9ac4 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: cosmetic

parent f924e69e
......@@ -362,7 +362,7 @@ type expr = {
e_node : expr_node;
e_vty : vty;
e_effect : effect;
e_vars : varmap;
e_varm : varmap;
e_label : Slab.t;
e_loc : Loc.position option;
}
......@@ -420,11 +420,11 @@ let e_label_copy { e_label = lab; e_loc = loc } e =
exception GhostWrite of expr * region
exception GhostRaise of expr * xsymbol
let mk_expr node vty eff vars = {
let mk_expr node vty eff varm = {
e_node = node;
e_vty = vty;
e_effect = if vty_ghost vty then eff_ghostify eff else eff;
e_vars = vars;
e_varm = varm;
e_label = Slab.empty;
e_loc = None;
}
......@@ -432,7 +432,7 @@ let mk_expr node vty eff vars = {
let varmap_union = Mid.set_union
let add_t_vars t m = Mvs.fold (fun vs _ m -> add_vs_vars vs m) t.t_vars m
let add_e_vars e m = varmap_union e.e_vars m
let add_e_vars e m = varmap_union e.e_varm m
let e_value pv =
mk_expr (Evalue pv) (VTvalue pv.pv_vtv) eff_empty (add_pv_vars pv Mid.empty)
......@@ -450,27 +450,27 @@ let vta_of_expr e = match e.e_vty with
let e_arrow ps vta =
let sbs = vta_vars_match ps.ps_subst ps.ps_vta vta in
let vars = Mid.add ps.ps_name ps.ps_vars ps.ps_varm in
let varm = Mid.add ps.ps_name ps.ps_vars ps.ps_varm in
let vta = vta_full_inst sbs ps.ps_vta in
mk_expr (Earrow ps) (VTarrow vta) eff_empty vars
mk_expr (Earrow ps) (VTarrow vta) eff_empty varm
let create_let_defn id e =
let lv = match e.e_vty with
| VTvalue vtv ->
LetV (create_pvsymbol id (vtv_unmut vtv))
| VTarrow vta ->
LetA (create_psymbol_mono id vta e.e_vars)
LetA (create_psymbol_mono id vta e.e_varm)
in
{ let_sym = lv ; let_expr = e }
exception StaleRegion of expr * region * ident
let check_reset e vars =
let check_reset e varm =
(* If we reset a region, then it may only occur in the later code
as the result of the resetting expression. Otherwise, this is
a freshness violation: some symbol defined earlier carries that
region into the later code. *)
let check_reset r u = (* does r occur in vars? *)
let check_reset r u = (* does r occur in varm? *)
let check_id id s = (* does r occur among the regions of id? *)
let rec check_reg reg =
reg_equal r reg || match u with
......@@ -480,7 +480,7 @@ let check_reset e vars =
if Sreg.exists check_reg s.vars_reg then
Loc.error ?loc:e.e_loc (StaleRegion (e,r,id))
in
Mid.iter check_id vars
Mid.iter check_id varm
in
Mreg.iter check_reset e.e_effect.eff_resets
......@@ -492,24 +492,24 @@ let check_ghost_write e eff =
if not (Sreg.is_empty badwr) then
Loc.error ?loc:e.e_loc (GhostWrite (e, Sreg.choose badwr))
let check_postexpr e eff vars =
let check_postexpr e eff varm =
check_ghost_write e eff;
check_reset e vars
check_reset e varm
let e_let ({ let_sym = lv ; let_expr = d } as ld) e =
let id = match lv with
| LetV pv -> pv.pv_vs.vs_name
| LetA ps -> ps.ps_name in
let vars = Mid.remove id e.e_vars in
check_postexpr d e.e_effect vars;
let varm = Mid.remove id e.e_varm in
check_postexpr d e.e_effect varm;
let eff = eff_union d.e_effect e.e_effect in
mk_expr (Elet (ld,e)) e.e_vty eff (add_e_vars d vars)
mk_expr (Elet (ld,e)) e.e_vty eff (add_e_vars d varm)
let e_app_real e pv =
let spec,vty = vta_app (vta_of_expr e) pv in
check_postexpr e spec.c_effect (add_pv_vars pv Mid.empty);
let eff = eff_union e.e_effect spec.c_effect in
mk_expr (Eapp (e,pv,spec)) vty eff (add_pv_vars pv e.e_vars)
mk_expr (Eapp (e,pv,spec)) vty eff (add_pv_vars pv e.e_varm)
let create_fun_defn id lam recsyms =
let e = lam.l_expr in
......@@ -530,9 +530,9 @@ let create_fun_defn id lam recsyms =
the varmap calculation below might be off. We should probably
make [rec_defn list] a private type. *)
let e_rec rdl e =
let add_vars m rd = varmap_union m rd.rec_ps.ps_varm in
let vars = List.fold_left add_vars e.e_vars rdl in
mk_expr (Erec (rdl,e)) e.e_vty e.e_effect vars
let add_varm m rd = varmap_union m rd.rec_ps.ps_varm in
let varm = List.fold_left add_varm e.e_varm rdl in
mk_expr (Erec (rdl,e)) e.e_vty e.e_effect varm
let on_value fn e = match e.e_node with
| Evalue pv -> fn pv
......@@ -565,7 +565,7 @@ let e_app = List.fold_left (fun e -> on_value (e_app_real e))
let e_plapp pls el ity =
if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
let rec app tl vars ghost eff sbs vtvl argl =
let rec app tl varm ghost eff sbs vtvl argl =
match vtvl, argl with
| [],[] ->
let vtv = pls.pl_value in
......@@ -577,7 +577,7 @@ let e_plapp pls el ity =
let t = match pls.pl_ls.ls_value with
| Some _ -> fs_app pls.pl_ls tl (ty_of_ity ity)
| None -> ps_app pls.pl_ls tl in
mk_expr (Elogic t) vty eff vars
mk_expr (Elogic t) vty eff varm
| [],_ | _,[] ->
raise (Term.BadArity
(pls.pl_ls, List.length pls.pl_args, List.length el))
......@@ -589,13 +589,13 @@ let e_plapp pls el ity =
let ghost = ghost || (evtv.vtv_ghost && not vtv.vtv_ghost) in
let eff = eff_union eff e.e_effect in
let sbs = ity_match sbs vtv.vtv_ity evtv.vtv_ity in
app (t::tl) (add_e_vars e vars) ghost eff sbs vtvl argl
app (t::tl) (add_e_vars e varm) ghost eff sbs vtvl argl
| vtv::vtvl, e::argl ->
let apply_to_pv pv =
let t = t_var pv.pv_vs in
let ghost = ghost || (pv.pv_vtv.vtv_ghost && not vtv.vtv_ghost) in
let sbs = ity_match sbs vtv.vtv_ity pv.pv_vtv.vtv_ity in
app (t::tl) (add_pv_vars pv vars) ghost eff sbs vtvl argl
app (t::tl) (add_pv_vars pv varm) ghost eff sbs vtvl argl
in
on_value apply_to_pv e
in
......@@ -614,21 +614,21 @@ let e_if e0 e1 e2 =
ity_equal_check vtv0.vtv_ity ity_bool;
ity_equal_check vtv1.vtv_ity vtv2.vtv_ity;
let eff = eff_union e1.e_effect e2.e_effect in
let vars = add_e_vars e2 (add_e_vars e1 Mid.empty) in
let varm = add_e_vars e2 (add_e_vars e1 Mid.empty) in
let ghost = vtv0.vtv_ghost || vtv1.vtv_ghost || vtv2.vtv_ghost in
let vty = VTvalue (vty_value ~ghost vtv1.vtv_ity) in
let eff = if ghost then eff_ghostify eff else eff in
check_postexpr e0 eff vars;
let vars = add_e_vars e0 vars in
check_postexpr e0 eff varm;
let varm = add_e_vars e0 varm in
let eff = eff_union e0.e_effect eff in
mk_expr (Eif (e0,e1,e2)) vty eff vars
mk_expr (Eif (e0,e1,e2)) vty eff varm
let e_case e0 bl =
let vtv0 = vtv_of_expr e0 in
let bity = match bl with
| (_,e)::_ -> (vtv_of_expr e).vtv_ity
| [] -> raise Term.EmptyCase in
let rec branch ghost eff vars = function
let rec branch ghost eff varm = function
| (pp,e)::bl ->
let vtv = vtv_of_expr e in
if pp.ppat_vtv.vtv_mut <> None then
......@@ -639,16 +639,16 @@ let e_case e0 bl =
ity_equal_check bity vtv.vtv_ity;
let ghost = ghost || vtv.vtv_ghost in
let del_vs vs _ m = Mid.remove vs.vs_name m in
let bvars = Mvs.fold del_vs pp.ppat_pattern.pat_vars e.e_vars in
let bvarm = Mvs.fold del_vs pp.ppat_pattern.pat_vars e.e_varm in
let eff = eff_union (eff_union eff pp.ppat_effect) e.e_effect in
branch ghost eff (varmap_union vars bvars) bl
branch ghost eff (varmap_union varm bvarm) bl
| [] ->
(* the cumulated effect of all branches, w/out e0 *)
let eff = if ghost then eff_ghostify eff else eff in
check_postexpr e0 eff vars; (* cumulated vars *)
check_postexpr e0 eff varm; (* cumulated varmap *)
let eff = eff_union e0.e_effect eff in
let vty = VTvalue (vty_value ~ghost bity) in
mk_expr (Ecase (e0,bl)) vty eff (add_e_vars e0 vars)
mk_expr (Ecase (e0,bl)) vty eff (add_e_vars e0 varm)
in
branch vtv0.vtv_ghost eff_empty Mid.empty bl
......@@ -661,12 +661,12 @@ let e_assign_real e0 pv =
| None -> Loc.error ?loc:e0.e_loc (Immutable e0) in
let ghost = vtv0.vtv_ghost || pv.pv_vtv.vtv_ghost in
let eff = eff_assign eff_empty ~ghost r pv.pv_vtv.vtv_ity in
let vars = add_pv_vars pv Mid.empty in
check_postexpr e0 eff vars;
let vars = add_e_vars e0 vars in
let varm = add_pv_vars pv Mid.empty in
check_postexpr e0 eff varm;
let varm = add_e_vars e0 varm in
let eff = eff_union e0.e_effect eff in
let vty = VTvalue (vty_value ~ghost ity_unit) in
let e = mk_expr (Eassign (e0,r,pv)) vty eff vars in
let e = mk_expr (Eassign (e0,r,pv)) vty eff varm in
(* FIXME? Ok, this is awkward. We prohibit assignments
where a ghost value is being written in a non-ghost
mutable lvalue (which is reasonable), but we build the
......@@ -686,7 +686,7 @@ let e_assign_real e0 pv =
let e_assign me e = on_value (e_assign_real me) e
let e_ghost e =
mk_expr (Eghost e) (vty_ghostify e.e_vty) e.e_effect e.e_vars
mk_expr (Eghost e) (vty_ghostify e.e_vty) e.e_effect e.e_varm
let e_any spec vty =
let varm = spec_varmap (vty_varmap vty) [] spec in
......@@ -727,7 +727,7 @@ let e_not e =
let vtv = vtv_of_expr e in
ity_equal_check vtv.vtv_ity ity_bool;
let vty = VTvalue (vty_value ~ghost:vtv.vtv_ghost ity_bool) in
mk_expr (Elogic (t_not f)) vty e.e_effect e.e_vars) e
mk_expr (Elogic (t_not f)) vty e.e_effect e.e_varm) e
let e_binop op e1 e2 =
on_fmla (fun e2 f2 -> on_fmla (fun e1 f1 ->
......@@ -735,11 +735,11 @@ let e_binop op e1 e2 =
let vtv2 = vtv_of_expr e2 in
ity_equal_check vtv1.vtv_ity ity_bool;
ity_equal_check vtv2.vtv_ity ity_bool;
let vars = add_e_vars e1 e2.e_vars in
let varm = add_e_vars e1 e2.e_varm in
let eff = eff_union e1.e_effect e2.e_effect in
let ghost = vtv1.vtv_ghost || vtv2.vtv_ghost in
let vty = VTvalue (vty_value ~ghost ity_bool) in
mk_expr (Elogic (t_binary op f1 f2)) vty eff vars) e1) e2
mk_expr (Elogic (t_binary op f1 f2)) vty eff varm) e1) e2
let e_lazy_and e1 e2 =
if eff_is_empty e2.e_effect then e_binop Tand e1 e2 else e_if e1 e2 e_false
......@@ -752,10 +752,10 @@ let e_loop inv variant e =
ity_equal_check vtv.vtv_ity ity_unit;
let vsset = pre_vars inv Mvs.empty in
let vsset = variant_vars variant vsset in
let vars = Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset e.e_vars in
check_postexpr e e.e_effect vars;
let varm = Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset e.e_varm in
check_postexpr e e.e_effect varm;
let vty = VTvalue (vtv_unmut vtv) in
mk_expr (Eloop (inv,variant,e)) vty e.e_effect vars
mk_expr (Eloop (inv,variant,e)) vty e.e_effect varm
let e_for_real pv bounds inv e =
let vtv = vtv_of_expr e in
......@@ -769,15 +769,15 @@ let e_for_real pv bounds inv e =
let ghost = pv.pv_vtv.vtv_ghost || pvfrom.pv_vtv.vtv_ghost ||
pvto.pv_vtv.vtv_ghost || vtv.vtv_ghost in
let eff = if ghost then eff_ghostify e.e_effect else e.e_effect in
let vars = add_t_vars inv e.e_vars in
let varm = add_t_vars inv e.e_varm in
(* FIXME? We check that no variable in the loop body, _including_
the index variable, is not invalidated because of a region reset.
We ignore the loop bounds, since they are computed just once. *)
check_postexpr e eff vars;
let vars = Mid.remove pv.pv_vs.vs_name vars in
let vars = add_pv_vars pvfrom (add_pv_vars pvto vars) in
check_postexpr e eff varm;
let varm = Mid.remove pv.pv_vs.vs_name varm in
let varm = add_pv_vars pvfrom (add_pv_vars pvto varm) in
let vty = VTvalue (vty_value ~ghost ity_unit) in
mk_expr (Efor (pv,bounds,inv,e)) vty eff vars
mk_expr (Efor (pv,bounds,inv,e)) vty eff varm
let e_for pv efrom dir eto inv e =
let apply pvto pvfrom = e_for_real pv (pvfrom,dir,pvto) inv e in
......@@ -792,11 +792,11 @@ let e_raise xs e ity =
let vty = VTvalue (vty_value ~ghost ity) in
check_postexpr e eff Mid.empty;
let eff = eff_union eff e.e_effect in
mk_expr (Eraise (xs,e)) vty eff e.e_vars
mk_expr (Eraise (xs,e)) vty eff e.e_varm
let e_try e0 bl =
let vtv0 = vtv_of_expr e0 in
let rec branch ghost eff vars = function
let rec branch ghost eff varm = function
| (xs,pv,e)::bl ->
let vtv = vtv_of_expr e in
ity_equal_check vtv0.vtv_ity vtv.vtv_ity;
......@@ -806,13 +806,13 @@ let e_try e0 bl =
(* we don't care about pv being ghost *)
let ghost = ghost || vtv.vtv_ghost in
let eff = eff_union eff e.e_effect in
let bvars = Mid.remove pv.pv_vs.vs_name e.e_vars in
branch ghost eff (varmap_union vars bvars) bl
let bvarm = Mid.remove pv.pv_vs.vs_name e.e_varm in
branch ghost eff (varmap_union varm bvarm) bl
| [] ->
let vty = VTvalue (vty_value ~ghost vtv0.vtv_ity) in
(* the cumulated effect of all branches, w/out e0 *)
let eff = if ghost then eff_ghostify eff else eff in
check_postexpr e0 eff vars; (* cumulated vars *)
check_postexpr e0 eff varm; (* cumulated varmap *)
(* remove from e0.e_effect the catched exceptions *)
let remove eff0 (xs,_,_) =
(* we catch in a ghost exception in a non-ghost code *)
......@@ -820,10 +820,10 @@ let e_try e0 bl =
Loc.error ?loc:e0.e_loc (GhostRaise (e0,xs));
eff_remove_raise eff0 xs in
let eff0 = List.fold_left remove e0.e_effect bl in
(* total effect and vars *)
(* total effect and varmap *)
let eff = eff_union eff0 eff in
let vars = add_e_vars e0 vars in
mk_expr (Etry (e0,bl)) vty eff vars
let varm = add_e_vars e0 varm in
mk_expr (Etry (e0,bl)) vty eff varm
in
branch vtv0.vtv_ghost eff_empty Mid.empty bl
......@@ -834,13 +834,13 @@ let e_abstract e q xq =
c_xpost = xq;
c_effect = e.e_effect; } in
spec_check spec e.e_vty;
let varm = spec_varmap e.e_vars [] spec in
let varm = spec_varmap e.e_varm [] spec in
mk_expr (Eabstr (e,q,xq)) e.e_vty e.e_effect varm
let e_assert ak f =
let vars = add_t_vars f Mid.empty in
let varm = add_t_vars f Mid.empty in
let vty = VTvalue (vty_value ity_unit) in
mk_expr (Eassert (ak, f)) vty eff_empty vars
mk_expr (Eassert (ak, f)) vty eff_empty varm
let e_absurd ity =
let vty = VTvalue (vty_value ity) in
......
......@@ -128,7 +128,7 @@ type expr = private {
e_node : expr_node;
e_vty : vty;
e_effect : effect;
e_vars : varmap;
e_varm : varmap;
e_label : Slab.t;
e_loc : Loc.position option;
}
......
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