Commit 75f433ad authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Mlw: handle "old" and "at" in specifications

parent e1cb6b38
...@@ -307,7 +307,9 @@ type ghost = bool ...@@ -307,7 +307,9 @@ type ghost = bool
type dbinder = preid option * ghost * dity type dbinder = preid option * ghost * dity
type 'a later = vsymbol Mstr.t -> 'a type register_old = pvsymbol -> string -> pvsymbol
type 'a later = pvsymbol Mstr.t -> register_old -> 'a
(* specification terms are parsed and typechecked after the program (* specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are expressions, when the types of locally bound program variables are
already established. *) already established. *)
...@@ -712,10 +714,8 @@ let create_assert = to_fmla ...@@ -712,10 +714,8 @@ let create_assert = to_fmla
let create_invariant pl = List.map to_fmla pl let create_invariant pl = List.map to_fmla pl
let create_pre = create_invariant
let create_post ty ql = List.map (fun (v,f) -> let create_post ty ql = List.map (fun (v,f) ->
let f = (*Mlw_wp.remove_old*) (to_fmla f) in match v with let f = to_fmla f in match v with
| None -> Ity.create_post (create_vsymbol (id_fresh "result") ty) f | None -> Ity.create_post (create_vsymbol (id_fresh "result") ty) f
| Some v -> Ty.ty_equal_check ty v.vs_ty; Ity.create_post v f) ql | Some v -> Ty.ty_equal_check ty v.vs_ty; Ity.create_post v f) ql
...@@ -771,8 +771,8 @@ let check_spec dsp ecty e = ...@@ -771,8 +771,8 @@ let check_spec dsp ecty e =
(* computed effect vs user effect *) (* computed effect vs user effect *)
let check_rwd = dsp.ds_checkrw in let check_rwd = dsp.ds_checkrw in
let uwrl, ue = effect_of_dspec dsp in let uwrl, ue = effect_of_dspec dsp in
let ucty = create_cty ecty.cty_args ecty.cty_pre let ucty = create_cty ecty.cty_args ecty.cty_pre ecty.cty_post
ecty.cty_post ecty.cty_xpost ue ecty.cty_result in ecty.cty_xpost ecty.cty_oldies ue ecty.cty_result in
let ueff = ucty.cty_effect and eeff = ecty.cty_effect in let ueff = ucty.cty_effect and eeff = ecty.cty_effect in
let urds = ueff.eff_reads and erds = eeff.eff_reads in let urds = ueff.eff_reads and erds = eeff.eff_reads in
(* check that every user effect actually happens *) (* check that every user effect actually happens *)
...@@ -843,29 +843,70 @@ let check_fun rsym dsp e = ...@@ -843,29 +843,70 @@ let check_fun rsym dsp e =
type env = { type env = {
rsm : rsymbol Mstr.t; rsm : rsymbol Mstr.t;
pvm : pvsymbol Mstr.t; pvm : pvsymbol Mstr.t;
vsm : vsymbol Mstr.t; old : (pvsymbol Mstr.t * (let_defn * pvsymbol) Hpv.t) Mstr.t;
} }
let env_empty = { let env_empty = {
rsm = Mstr.empty; rsm = Mstr.empty;
pvm = Mstr.empty; pvm = Mstr.empty;
vsm = Mstr.empty; old = Mstr.empty;
} }
let add_rsymbol ({rsm = rsm; vsm = vsm} as env) rs = exception UnboundLabel of string
let find_old pvm (ovm,old) v =
let n = v.pv_vs.vs_name.id_string in
(* if v is top-level, both ov and pv are None.
If v is local, ov and pv must be equal to v.
If they are not equal, then v is defined under the label,
so we return v and do not register an "oldie" for it. *)
let ov = Mstr.find_opt n ovm in
let pv = Mstr.find_opt n pvm in
if not (Opt.equal pv_equal ov pv) then v
else match Hpv.find_opt old v with
| Some (_,o) -> o
| None ->
let e = e_pure (t_var v.pv_vs) in
let id = id_clone v.pv_vs.vs_name in
let ld = let_var id ~ghost:true e in
Hpv.add old v ld; snd ld
let register_old env v l =
find_old env.pvm (Mstr.find_exn (UnboundLabel l) l env.old) v
let get_later env later = later env.pvm (register_old env)
let add_label ({pvm = pvm; old = old} as env) l =
let ht = Hpv.create 3 in
{ env with old = Mstr.add l (pvm, ht) old }, ht
let create_pre pvm preold old pl =
let pl = List.map to_fmla pl in
let fvs = List.fold_left t_freevars Mvs.empty pl in
let rebase v (_,{pv_vs = o}) sbs =
if not (Mvs.mem o fvs) then sbs else match preold with
| Some preold ->
Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs
| None -> raise (UnboundLabel "'0") in
let sbs = Hpv.fold rebase old Mvs.empty in
List.map (t_subst sbs) pl
let get_oldies old =
Hpv.fold (fun v (_,o) sbs -> Mpv.add o v sbs) old Mpv.empty
let add_rsymbol ({rsm = rsm; pvm = pvm} as env) rs =
let n = rs.rs_name.id_string in let n = rs.rs_name.id_string in
let vsm = match rs.rs_logic with let pvm = match rs.rs_logic with
| RLpv pv -> Mstr.add n pv.pv_vs vsm | RLpv pv -> Mstr.add n pv pvm
| _ -> vsm in | _ -> pvm in
{ env with rsm = Mstr.add n rs rsm; vsm = vsm } { env with rsm = Mstr.add n rs rsm; pvm = pvm }
let add_pvsymbol ({pvm = pvm; vsm = vsm} as env) pv = let add_pvsymbol ({pvm = pvm} as env) pv =
let n = pv.pv_vs.vs_name.id_string in let n = pv.pv_vs.vs_name.id_string in
{ env with pvm = Mstr.add n pv pvm; vsm = Mstr.add n pv.pv_vs vsm } { env with pvm = Mstr.add n pv pvm }
let add_pv_map ({pvm = pvm; vsm = vsm} as env) vm = let add_pv_map ({pvm = pvm} as env) vm =
let um = Mstr.map (fun pv -> pv.pv_vs) vm in { env with pvm = Mstr.set_union vm pvm }
{ env with pvm = Mstr.set_union vm pvm; vsm = Mstr.set_union um vsm }
let add_binders env pvl = List.fold_left add_pvsymbol env pvl let add_binders env pvl = List.fold_left add_pvsymbol env pvl
...@@ -876,13 +917,15 @@ let cty_of_spec env bl dsp dity = ...@@ -876,13 +917,15 @@ let cty_of_spec env bl dsp dity =
let ty = ty_of_ity ity in let ty = ty_of_ity ity in
let bl = binders bl in let bl = binders bl in
let env = add_binders env bl in let env = add_binders env bl in
let dsp = dsp env.vsm ty in let preold = Mstr.find_opt "'0" env.old in
let _,eff = effect_of_dspec dsp in let env, old = add_label env "'0" in
let dsp = get_later env dsp ty in
let _, eff = effect_of_dspec dsp in
let eff = eff_strong eff in let eff = eff_strong eff in
let p = create_pre dsp.ds_pre in let p = create_pre env.pvm preold old dsp.ds_pre in
let q = create_post ty dsp.ds_post in let q = create_post ty dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in let xq = create_xpost dsp.ds_xpost in
create_cty bl p q xq eff ity create_cty bl p q xq (get_oldies old) eff ity
(** Expressions *) (** Expressions *)
...@@ -937,7 +980,8 @@ and try_cexp uloc env ghost de0 = match de0.de_node with ...@@ -937,7 +980,8 @@ and try_cexp uloc env ghost de0 = match de0.de_node with
| _ -> app (cexp uloc env ghost de) el in | _ -> app (cexp uloc env ghost de) el in
down de0 [] down de0 []
| DEfun (bl,dsp,de) -> | DEfun (bl,dsp,de) ->
let c, dsp, _ = lambda uloc env (binders bl) dsp de in let dvl _ _ = [] in
let c, dsp, _ = lambda uloc env (binders bl) dsp dvl de in
check_fun None dsp c; check_fun None dsp c;
[], c_ghostify ghost c [], c_ghostify ghost c
| DEany (bl,dsp,dity) -> | DEany (bl,dsp,dity) ->
...@@ -1038,8 +1082,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = ...@@ -1038,8 +1082,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DEwhile (de1,dinv,dvarl,de2) -> | DEwhile (de1,dinv,dvarl,de2) ->
let e1 = expr uloc env de1 in let e1 = expr uloc env de1 in
let e2 = expr uloc env de2 in let e2 = expr uloc env de2 in
let inv = dinv env.vsm in let inv = get_later env dinv in
let varl = dvarl env.vsm in let varl = get_later env dvarl in
e_while e1 (create_invariant inv) varl e2 e_while e1 (create_invariant inv) varl e2
| DEfor (id,de_from,dir,de_to,dinv,de) -> | DEfor (id,de_from,dir,de_to,dinv,de) ->
let e_from = expr uloc env de_from in let e_from = expr uloc env de_from in
...@@ -1047,7 +1091,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = ...@@ -1047,7 +1091,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let v = create_pvsymbol id ity_int in let v = create_pvsymbol id ity_int in
let env = add_pvsymbol env v in let env = add_pvsymbol env v in
let e = expr uloc env de in let e = expr uloc env de in
let inv = dinv env.vsm in let inv = get_later env dinv in
e_for v e_from dir e_to (create_invariant inv) e e_for v e_from dir e_to (create_invariant inv) e
| DEtry (de1,bl) -> | DEtry (de1,bl) ->
let e1 = expr uloc env de1 in let e1 = expr uloc env de1 in
...@@ -1080,21 +1124,19 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = ...@@ -1080,21 +1124,19 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DEghost de -> | DEghost de ->
e_ghostify true (expr uloc env de) e_ghostify true (expr uloc env de)
| DEassert (ak,f) -> | DEassert (ak,f) ->
e_assert ak (create_assert (f env.vsm)) e_assert ak (create_assert (get_later env f))
| DEpure t -> | DEpure t ->
e_pure (t env.vsm) e_pure (get_later env t)
| DEabsurd -> | DEabsurd ->
e_absurd (ity_of_dity res) e_absurd (ity_of_dity res)
| DEtrue -> | DEtrue ->
e_true e_true
| DEfalse -> | DEfalse ->
e_false e_false
| DEmark _ -> assert false (* TODO *) | DEmark ({pre_name = l},de) ->
(* let env, old = add_label env l in
let ld,v = create_let_defn_pv id Mlw_wp.e_now in let put _ (ld,_) e = e_let ld e in
let env = add_pvsymbol env v in Hpv.fold put old (expr uloc env de)
e_let ld (expr uloc env de)
*)
| DEcast _ | DEuloc _ | DElabel _ -> | DEcast _ | DEuloc _ | DElabel _ ->
assert false (* already stripped *) assert false (* already stripped *)
...@@ -1118,15 +1160,15 @@ and rec_defn uloc env ghost {fds = dfdl} = ...@@ -1118,15 +1160,15 @@ and rec_defn uloc env ghost {fds = dfdl} =
let step1 env (id, gh, kind, bl, dsp, dvl, ({de_dvty = dvty} as de)) = let step1 env (id, gh, kind, bl, dsp, dvl, ({de_dvty = dvty} as de)) =
let pvl = binders bl in let pvl = binders bl in
let ity = Loc.try1 ?loc:de.de_loc ity_of_dity (dity_of_dvty dvty) in let ity = Loc.try1 ?loc:de.de_loc ity_of_dity (dity_of_dvty dvty) in
let cty = create_cty pvl [] [] Mexn.empty eff_empty ity in let cty = create_cty pvl [] [] Mexn.empty Mpv.empty eff_empty ity in
let rs = create_rsymbol id ~ghost:(gh || ghost) ~kind:RKnone cty in let rs = create_rsymbol id ~ghost:(gh || ghost) ~kind:RKnone cty in
add_rsymbol env rs, (rs, kind, dsp, dvl, de) in add_rsymbol env rs, (rs, kind, dsp, dvl, de) in
let env, fdl = Lists.map_fold_left step1 env dfdl in let env, fdl = Lists.map_fold_left step1 env dfdl in
let step2 ({rs_cty = c} as rs, kind, dsp, dvl, de) (fdl, dspl) = let step2 ({rs_cty = c} as rs, kind, dsp, dvl, de) (fdl, dspl) =
let lam, dsp, env = lambda uloc env c.cty_args dsp de in let lam, dsp, dvl = lambda uloc env c.cty_args dsp dvl de in
if c_ghost lam && not (rs_ghost rs) then Loc.errorm ?loc:rs.rs_name.id_loc if c_ghost lam && not (rs_ghost rs) then Loc.errorm ?loc:rs.rs_name.id_loc
"Function %s must be explicitly marked ghost" rs.rs_name.id_string; "Function %s must be explicitly marked ghost" rs.rs_name.id_string;
(rs, lam, dvl env.vsm, kind)::fdl, dsp::dspl in (rs, lam, dvl, kind)::fdl, dsp::dspl in
(* check for unexpected aliases in case of trouble *) (* check for unexpected aliases in case of trouble *)
let fdl, dspl = try List.fold_right step2 fdl ([],[]) with let fdl, dspl = try List.fold_right step2 fdl ([],[]) with
| Loc.Located (_, Ity.TypeMismatch _) | Ity.TypeMismatch _ as exn -> | Loc.Located (_, Ity.TypeMismatch _) | Ity.TypeMismatch _ as exn ->
...@@ -1143,15 +1185,18 @@ and rec_defn uloc env ghost {fds = dfdl} = ...@@ -1143,15 +1185,18 @@ and rec_defn uloc env ghost {fds = dfdl} =
add_rsymbol env s in add_rsymbol env s in
ld, List.fold_left2 add_fd env rdl dspl ld, List.fold_left2 add_fd env rdl dspl
and lambda uloc env pvl dsp de = and lambda uloc env pvl dsp dvl de =
let env = add_binders env pvl in let env = add_binders env pvl in
let e = expr uloc env de in let e = expr uloc env de in
let ty = ty_of_ity e.e_ity in let ty = ty_of_ity e.e_ity in
let dsp = dsp env.vsm ty in let preold = Mstr.find_opt "'0" env.old in
let p = create_pre dsp.ds_pre in let env, old = add_label env "'0" in
let dsp = get_later env dsp ty in
let dvl = get_later env dvl in
let p = create_pre env.pvm preold old dsp.ds_pre in
let q = create_post ty dsp.ds_post in let q = create_post ty dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in let xq = create_xpost dsp.ds_xpost in
c_fun pvl p q xq e, dsp, env c_fun pvl p q xq (get_oldies old) e, dsp, dvl
let rec_defn ?(keep_loc=true) drdf = let rec_defn ?(keep_loc=true) drdf =
reunify_regions (); reunify_regions ();
...@@ -1173,7 +1218,7 @@ let let_defn ?(keep_loc=true) (id,ghost,kind,de) = ...@@ -1173,7 +1218,7 @@ let let_defn ?(keep_loc=true) (id,ghost,kind,de) =
let e = expr uloc env_empty de in let e = expr uloc env_empty de in
if e_ghost e && not ghost then Loc.errorm ?loc:id.pre_loc if e_ghost e && not ghost then Loc.errorm ?loc:id.pre_loc
"Function %s must be explicitly marked ghost" id.pre_name; "Function %s must be explicitly marked ghost" id.pre_name;
let c = c_fun [] [] [] Mexn.empty e in let c = c_fun [] [] [] Mexn.empty Mpv.empty e in
(* the rsymbol will carry a single postcondition "the result (* the rsymbol will carry a single postcondition "the result
is equal to the logical constant". Any user-written spec is equal to the logical constant". Any user-written spec
will be checked once, in-place, under Eexec. Since kind will be checked once, in-place, under Eexec. Since kind
...@@ -1202,3 +1247,8 @@ let expr ?(keep_loc=true) de = ...@@ -1202,3 +1247,8 @@ let expr ?(keep_loc=true) de =
reunify_regions (); reunify_regions ();
let uloc = if keep_loc then None else Some None in let uloc = if keep_loc then None else Some None in
expr uloc env_empty de expr uloc env_empty de
let () = Exn_printer.register (fun fmt e -> match e with
| UnboundLabel s ->
Format.fprintf fmt "unbound label %s" s
| _ -> raise e)
...@@ -55,10 +55,16 @@ type dbinder = preid option * ghost * dity ...@@ -55,10 +55,16 @@ type dbinder = preid option * ghost * dity
(** Specifications *) (** Specifications *)
type 'a later = vsymbol Mstr.t -> 'a exception UnboundLabel of string
(* Specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are type register_old = pvsymbol -> string -> pvsymbol
already established. *) (** Program variables occurring under [old] or [at] are passed to
a registrar function. The label string must be ['0] for [old]. *)
type 'a later = pvsymbol Mstr.t -> register_old -> 'a
(** Specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are
already established. *)
type dspec_final = { type dspec_final = {
ds_pre : term list; ds_pre : term list;
......
...@@ -170,7 +170,7 @@ let create_projection s v = ...@@ -170,7 +170,7 @@ let create_projection s v =
let arg = create_pvsymbol (id_fresh "arg") ity in let arg = create_pvsymbol (id_fresh "arg") ity in
let ls = create_fsymbol id [arg.pv_vs.vs_ty] v.pv_vs.vs_ty in let ls = create_fsymbol id [arg.pv_vs.vs_ty] v.pv_vs.vs_ty in
let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in
let c = create_cty [arg] [] [q] Mexn.empty eff v.pv_ity in let c = create_cty [arg] [] [q] Mexn.empty Mpv.empty eff v.pv_ity in
mk_rs ls.ls_name c (RLls ls) (Some v) mk_rs ls.ls_name c (RLls ls) (Some v)
exception FieldExpected of rsymbol exception FieldExpected of rsymbol
...@@ -196,7 +196,7 @@ let create_constructor ~constr id s fl = ...@@ -196,7 +196,7 @@ let create_constructor ~constr id s fl =
let ls = create_fsymbol ~constr id argl ty in let ls = create_fsymbol ~constr id argl ty in
let argl = List.map (fun a -> t_var a.pv_vs) fl in let argl = List.map (fun a -> t_var a.pv_vs) fl in
let q = make_post (fs_app ls argl ty) in let q = make_post (fs_app ls argl ty) in
let c = create_cty fl [] [q] Mexn.empty eff_empty ity in let c = create_cty fl [] [q] Mexn.empty Mpv.empty eff_empty ity in
mk_rs ls.ls_name c (RLls ls) None mk_rs ls.ls_name c (RLls ls) None
let rs_of_ls ls = let rs_of_ls ls =
...@@ -205,7 +205,7 @@ let rs_of_ls ls = ...@@ -205,7 +205,7 @@ let rs_of_ls ls =
let t_args = List.map (fun v -> t_var v.pv_vs) v_args in let t_args = List.map (fun v -> t_var v.pv_vs) v_args in
let q = make_post (t_app ls t_args ls.ls_value) in let q = make_post (t_app ls t_args ls.ls_value) in
let ity = ity_of_ty (t_type q) in let ity = ity_of_ty (t_type q) in
let c = create_cty v_args [] [q] Mexn.empty eff_empty ity in let c = create_cty v_args [] [q] Mexn.empty Mpv.empty eff_empty ity in
mk_rs ls.ls_name c (RLls ls) None mk_rs ls.ls_name c (RLls ls) None
let rs_ghost s = s.rs_cty.cty_effect.eff_ghost let rs_ghost s = s.rs_cty.cty_effect.eff_ghost
...@@ -492,8 +492,11 @@ let e_exec ({c_cty = cty} as c) = match cty.cty_args with ...@@ -492,8 +492,11 @@ let e_exec ({c_cty = cty} as c) = match cty.cty_args with
let c_any c = mk_cexp Cany c let c_any c = mk_cexp Cany c
let c_fun args p q xq ({e_effect = eff} as e) = let c_fun args p q xq old ({e_effect = eff} as e) =
mk_cexp (Cfun e) (create_cty args p q xq eff e.e_ity) (* reset variables are forbidden in post-conditions *)
let c = try create_cty args p q xq old eff e.e_ity with
| StaleVariable (v,r) -> localize_cover_stale v r [e] in
mk_cexp (Cfun e) c
let c_app s vl ityl ity = let c_app s vl ityl ity =
mk_cexp (Capp (s,vl)) (cty_apply s.rs_cty vl ityl ity) mk_cexp (Capp (s,vl)) (cty_apply s.rs_cty vl ityl ity)
...@@ -741,7 +744,8 @@ and c_rs_subst sm ({c_node = n; c_cty = c} as d) = ...@@ -741,7 +744,8 @@ and c_rs_subst sm ({c_node = n; c_cty = c} as d) =
let al = List.map (fun v -> v.pv_ity) c.cty_args in let al = List.map (fun v -> v.pv_ity) c.cty_args in
c_app (Mrs.find_def s s sm) vl al c.cty_result c_app (Mrs.find_def s s sm) vl al c.cty_result
| Cfun e -> | Cfun e ->
c_fun c.cty_args c.cty_pre c.cty_post c.cty_xpost (e_rs_subst sm e)) c_fun c.cty_args c.cty_pre c.cty_post
c.cty_xpost c.cty_oldies (e_rs_subst sm e))
and rec_fixp dl = and rec_fixp dl =
let update sm (s,({c_cty = c} as d)) = let update sm (s,({c_cty = c} as d)) =
...@@ -809,7 +813,7 @@ let let_rec fdl = ...@@ -809,7 +813,7 @@ let let_rec fdl =
(* create the clean rsymbol *) (* create the clean rsymbol *)
let id = id_clone s.rs_name in let id = id_clone s.rs_name in
let c = create_cty c.cty_args pre let c = create_cty c.cty_args pre
c.cty_post c.cty_xpost start_eff c.cty_result in c.cty_post c.cty_xpost c.cty_oldies start_eff c.cty_result in
let ns = create_rsymbol id ~ghost:(rs_ghost s) ~kind:RKnone c in let ns = create_rsymbol id ~ghost:(rs_ghost s) ~kind:RKnone c in
let sm = Mrs.add_new (Invalid_argument "Expr.let_rec") s ns sm in let sm = Mrs.add_new (Invalid_argument "Expr.let_rec") s ns sm in
sm, (ns, c_ghostify (rs_ghost s) d) in sm, (ns, c_ghostify (rs_ghost s) d) in
......
...@@ -176,8 +176,8 @@ val ls_decr_of_let_defn : let_defn -> lsymbol option ...@@ -176,8 +176,8 @@ val ls_decr_of_let_defn : let_defn -> lsymbol option
val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
val c_fun : val c_fun : pvsymbol list ->
pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> cexp pre list -> post list -> post list Mexn.t -> pvsymbol Mpv.t -> expr -> cexp
val c_any : cty -> cexp val c_any : cty -> cexp
......
...@@ -712,7 +712,7 @@ let eff_read_post e rd = ...@@ -712,7 +712,7 @@ let eff_read_post e rd =
let _ = check_covers e.eff_covers rd in let _ = check_covers e.eff_covers rd in
{ e with eff_reads = Spv.union e.eff_reads rd } { e with eff_reads = Spv.union e.eff_reads rd }
let eff_bind rd e = if Spv.is_empty rd then e else let eff_bind rd e = if Mpv.is_empty rd then e else
{ e with eff_reads = Mpv.set_diff e.eff_reads rd } { e with eff_reads = Mpv.set_diff e.eff_reads rd }
let eff_read rd = let eff_read rd =
...@@ -888,16 +888,18 @@ type cty = { ...@@ -888,16 +888,18 @@ type cty = {
cty_pre : pre list; cty_pre : pre list;
cty_post : post list; cty_post : post list;
cty_xpost : post list Mexn.t; cty_xpost : post list Mexn.t;
cty_oldies : pvsymbol Mpv.t;
cty_effect : effect; cty_effect : effect;
cty_result : ity; cty_result : ity;
cty_freeze : ity_subst; cty_freeze : ity_subst;
} }
let cty_unsafe args pre post xpost effect result freeze = { let cty_unsafe args pre post xpost oldies effect result freeze = {
cty_args = args; cty_args = args;
cty_pre = pre; cty_pre = pre;
cty_post = post; cty_post = post;
cty_xpost = xpost; cty_xpost = xpost;
cty_oldies = oldies;
cty_effect = effect; cty_effect = effect;
cty_result = result; cty_result = result;
cty_freeze = freeze; cty_freeze = freeze;
...@@ -939,17 +941,26 @@ let check_post exn ity post = ...@@ -939,17 +941,26 @@ let check_post exn ity post =
| Teps _ -> Ty.ty_equal_check ty (t_type q) | Teps _ -> Ty.ty_equal_check ty (t_type q)
| _ -> raise exn) post | _ -> raise exn) post
let create_cty args pre post xpost effect result = let create_cty args pre post xpost oldies effect result =
let exn = Invalid_argument "Ity.create_cty" in let exn = Invalid_argument "Ity.create_cty" in
(* pre, post, and xpost are well-typed *) (* pre, post, and xpost are well-typed *)
check_pre pre; check_post exn result post; check_pre pre; check_post exn result post;
Mexn.iter (fun xs xq -> check_post exn xs.xs_ity xq) xpost; Mexn.iter (fun xs xq -> check_post exn xs.xs_ity xq) xpost;
(* the arguments must be pairwise distinct *) (* the arguments must be pairwise distinct *)
let sarg = List.fold_right (Spv.add_new exn) args Spv.empty in let sarg = List.fold_right (Spv.add_new exn) args Spv.empty in
(* complete the reads and freeze the external context (* complete the reads and freeze the external context.
FIXME/TODO: detect stale variables in post and xpost *) oldies must be fresh: collisions with args and external
let reads = spec_t_fold t_freepvs sarg pre post xpost in reads are forbidden, to simplify instantiation later. *)
let effect = eff_read_pre reads effect in let preads = spec_t_fold t_freepvs sarg pre [] Mexn.empty in
let qreads = spec_t_fold t_freepvs Spv.empty [] post xpost in
let effect = eff_read_post effect qreads in
Mpv.iter (fun {pv_ghost = gh; pv_ity = o} {pv_ity = t} ->
if not (gh && o == ity_purify t) then raise exn) oldies;
let oldies = Mpv.set_inter oldies effect.eff_reads in
let effect = eff_bind oldies effect in
let preads = Mpv.fold (Util.const Spv.add) oldies preads in
if not (Mpv.set_disjoint preads oldies) then raise exn;
let effect = eff_read_pre preads effect in
let freeze = Spv.diff effect.eff_reads sarg in let freeze = Spv.diff effect.eff_reads sarg in
let freeze = Spv.fold freeze_pv freeze isb_empty in let freeze = Spv.fold freeze_pv freeze isb_empty in
check_tvs effect.eff_reads result pre post xpost; check_tvs effect.eff_reads result pre post xpost;
...@@ -984,11 +995,11 @@ let create_cty args pre post xpost effect result = ...@@ -984,11 +995,11 @@ let create_cty args pre post xpost effect result =
let resets = Mreg.map (fun _ -> Sreg.empty) unknwn in let resets = Mreg.map (fun _ -> Sreg.empty) unknwn in
let covers = Mreg.set_union resets effect.eff_covers in let covers = Mreg.set_union resets effect.eff_covers in
let effect = { effect with eff_covers = covers } in let effect = { effect with eff_covers = covers } in
cty_unsafe args pre post xpost effect result freeze cty_unsafe args pre post xpost oldies effect result freeze
let cty_apply c vl args res = let cty_apply c vl args res =
let vsb_add vsb {pv_vs = u} {pv_vs = v} = let vsb_add vsb {pv_vs = u} v =
if vs_equal u v then vsb else Mvs.add u (t_var v) vsb in if vs_equal u v.pv_vs then vsb else Mvs.add u v vsb in
let match_v isb u v = ity_match isb u.pv_ity v.pv_ity in let match_v isb u v = ity_match isb u.pv_ity v.pv_ity in
(* stage 1: apply c to vl *) (* stage 1: apply c to vl *)
let rec apply gh same isb vsb ul vl = match ul, vl with let rec apply gh same isb vsb ul vl = match ul, vl with
...@@ -1015,6 +1026,13 @@ let cty_apply c vl args res = ...@@ -1015,6 +1026,13 @@ let cty_apply c vl args res =
| [], [] -> same, rul, rvl, vsb | [], [] -> same, rul, rvl, vsb
| _ -> invalid_arg "Ity.cty_apply" in | _ -> invalid_arg "Ity.cty_apply" in
let same, rcargs, rargs, vsb = cut same [] [] vsb cargs args in let same, rcargs, rargs, vsb = cut same [] [] vsb cargs args in
let vsb, oldies = if Mvs.is_empty vsb then vsb, c.cty_oldies else
Mpv.fold (fun {pv_vs = o} v (s,m) ->
let id = id_clone o.vs_name in
let v = Mvs.find_def v v.pv_vs vsb in
let n = create_pvsymbol id ~ghost:true (ity_purify v.pv_ity) in
Mvs.add o n s, Mpv.add n v m) c.cty_oldies (vsb, Mpv.empty) in
let vsb = Mvs.map (fun v -> t_var v.pv_vs) vsb in
let same = same && ity_equal c.cty_result res in let same = same && ity_equal c.cty_result res in
if same && vl = [] then (* trivial *) c else if same && vl = [] then (* trivial *) c else
let isb = if same then isb_empty else let isb = if same then isb_empty else
...@@ -1045,7 +1063,7 @@ let cty_apply c vl args res = ...@@ -1045,7 +1063,7 @@ let cty_apply c vl args res =
let subst_l l = List.map subst_t l in let subst_l l = List.map subst_t l in
cty_unsafe (List.rev rargs) (subst_l c.cty_pre)