Commit 1a970541 authored by Andrei Paskevich's avatar Andrei Paskevich

replace t_subst . subst1 with t_subst_single

parent f14be792
......@@ -264,8 +264,6 @@ module rec T : sig
val post_map : (term -> term) -> post -> post
val subst1 : vsymbol -> term -> term Mvs.t
val eq_type_v : type_v -> type_v -> bool
(* pretty-printers *)
......@@ -492,13 +490,11 @@ end = struct
c_pre = t_true;
c_post = (v_result ty, t_true), []; }
let subst1 vs1 t2 = Mvs.add vs1 t2 Mvs.empty
let apply_type_v_var v pv = match v with
| Tarrow (x :: bl, c) ->
let ts = ty_match Mtv.empty x.pv_effect.vs_ty pv.pv_effect.vs_ty in
let c = type_c_of_type_v (Tarrow (bl, c)) in
subst_type_c ts (subst1 x.pv_pure (t_var pv.pv_pure)) c
subst_type_c ts (Mvs.singleton x.pv_pure (t_var pv.pv_pure)) c
| Tarrow ([], _) | Tpure _ ->
assert false
......@@ -507,7 +503,7 @@ end = struct
(* let ts = ty_match Mtv.empty x.pv_effect.vs_ty s.p_ty in *)
(* let c = type_c_of_type_v (Tarrow (bl, c)) in *)
(* let t = t_app s.p_ls [] (ty_inst ts x.pv_effect.vs_ty) in *)
(* subst_type_c ts (subst1 x.pv_pure t) c *)
(* subst_type_c ts (Mvs.singleton x.pv_pure t) c *)
(* | _ -> *)
(* assert false *)
......
......@@ -165,8 +165,6 @@ module rec T : sig
val post_map : (term -> term) -> post -> post
val subst1 : vsymbol -> term -> term Mvs.t
val eq_type_v : type_v -> type_v -> bool
(* pretty-printers *)
......
......@@ -303,7 +303,7 @@ let abstract_wp env rm ef (q',ql') (q,ql) =
let quantify_h (e',(x',f')) (e,(x,f)) =
assert (ls_equal e' e);
let res, f' = match x', x with
| Some v', Some v -> Some v, t_subst (subst1 v' (t_var v)) f'
| Some v', Some v -> Some v, t_subst_single v' (t_var v) f'
| None, None -> None, f'
| _ -> assert false
in
......@@ -313,7 +313,7 @@ let abstract_wp env rm ef (q',ql') (q,ql) =
let res, f = q and res', f' = q' in
let f' =
if is_arrow_ty res'.vs_ty then f'
else t_subst (subst1 res' (t_var res)) f'
else t_subst_single res' (t_var res) f'
in
quantify_res f' f (Some res)
in
......@@ -463,7 +463,7 @@ and wp_desc env rm e q = match e.expr_desc with
in
let v1 = v_result x.pv_pure.vs_ty in
let t1 = t_label ~loc:e1.expr_loc ["let"] (t_var v1) in
let q1 = v1, t_subst (subst1 x.pv_pure t1) w2 in
let q1 = v1, t_subst_single x.pv_pure t1 w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_label e (wp_expr env rm e1 q1)
| Eletrec (dl, e1) ->
......@@ -580,13 +580,13 @@ and wp_desc env rm e q = match e.expr_desc with
let add = find_ls~pure:true env "infix +" in
let wp1 =
let xp1 = fs_app add [t_var x.pv_pure; incr] ty_int in
let post = t_subst (subst1 x.pv_pure xp1) inv in
let post = t_subst_single x.pv_pure xp1 inv in
let q1 = saturate_post e1.expr_effect (res, post) q in
wp_expr env rm e1 q1
in
let f = wp_and ~sym:true
(wp_expl "for loop initialization"
(t_subst (subst1 x.pv_pure (t_var v1.pv_pure)) inv))
(t_subst_single x.pv_pure (t_var v1.pv_pure) inv))
(quantify env rm e.expr_effect.E.writes
(wp_and ~sym:true
(wp_expl "for loop preservation"
......@@ -596,7 +596,7 @@ and wp_desc env rm e q = match e.expr_desc with
(ps_app le [t_var x.pv_pure; t_var v2.pv_pure]))
(wp_implies inv wp1))))
(let sv2 = fs_app add [t_var v2.pv_pure; incr] ty_int in
wp_implies (t_subst (subst1 x.pv_pure sv2) inv) q1)))
wp_implies (t_subst_single x.pv_pure sv2 inv) q1)))
in
let f =
wp_and ~sym:true (wp_implies v1_gt_v2 q1) (wp_implies v1_le_v2 f) 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