Skip to content

why3
why3
Commit 903df0ef authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

remove duplicate functions from Term (f_map => t_map, etc)

parent 8a0f0ab5
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 303 additions and 541 deletions
src/coq-plugin/whytac.ml
View file @ 903df0ef
......@@ -821,9 +821,9 @@ and tr_formula dep tvm bv env f =
let ls = tr_global_ls dep env (ConstructRef cj) in
if List.length vars <> List.length ls.ls_args then raise NotFO;
let pat = pat_app ls (List.map pat_var vars) ty in
f_close_branch pat (tr_formula dep tvm bv env bj)
t_close_branch pat (tr_formula dep tvm bv env bj)
in
f_case t (Array.to_list (Array.mapi branch br))
t_case t (Array.to_list (Array.mapi branch br))
| Case _, _ :: _ ->
raise NotFO (* TODO: we could possibly swap case and application *)
| _ ->
......@@ -874,7 +874,7 @@ let tr_goal gl =
let ty = tr_type dep tvm env ty in
let vs = Term.create_vsymbol (preid_of_id id) ty in
let bv = Idmap.add id vs bv in
Term.f_let_close vs d (tr_ctxt tvm bv ctxt)
Term.t_let_close vs d (tr_ctxt tvm bv ctxt)
with NotFO ->
tr_ctxt tvm bv ctxt
end
......
src/core/decl.ml
View file @ 903df0ef
......@@ -40,7 +40,7 @@ type logic_decl = lsymbol * ls_defn option
exception UnboundVar of vsymbol
let check_fvs f =
let fvs = f_freevars Svs.empty (t_prop f) in
let fvs = t_freevars Svs.empty (t_prop f) in
Svs.iter (fun vs -> raise (UnboundVar vs)) fvs;
f
......@@ -62,7 +62,7 @@ let make_ps_defn ps vl f =
List.iter2 check_vl ps.ls_args vl;
ps, Some (ps, check_fvs pd)
let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
let make_ls_defn ls vl = e_map (make_fs_defn ls vl) (make_ps_defn ls vl)
let open_ls_defn (_,f) =
let vl, ef = f_open_forall f in
......@@ -140,24 +140,24 @@ let build_call_graph cgr syms ls =
| _ -> t_fold (term vm) (fmla vm) () t
and fmla vm () f = match f.t_node with
| Tapp (s,tl) when Mls.mem s syms ->
f_fold (term vm) (fmla vm) () f; call vm s tl
t_fold (term vm) (fmla vm) () f; call vm s tl
| Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
let u,e = f_open_bound b in
let u,e = t_open_bound b in
fmla (Mvs.add u (Mvs.find v vm) vm) () e
| Tcase (e,bl) ->
term vm () e; List.iter (fun b ->
let p,f = f_open_branch b in
let p,f = t_open_branch b in
let vml = match_term vm e [vm] p in
List.iter (fun vm -> fmla vm () f) vml) bl
| Fquant (_,b) ->
let _,_,f = f_open_quant b in fmla vm () f
| _ -> f_fold (term vm) (fmla vm) () f
| _ -> t_fold (term vm) (fmla vm) () f
in
fun (vl,e) ->
let i = ref (-1) in
let add vm v = incr i; Mvs.add v (Equal !i) vm in
let vm = List.fold_left add Mvs.empty vl in
e_apply (term vm ()) (fmla vm ()) e
e_map (term vm ()) (fmla vm ()) e
let build_call_list cgr ls =
let htb = Hls.create 5 in
......@@ -309,12 +309,12 @@ module Hsdecl = Hashcons.Make (struct
| _ -> false
let eq_ld (ls1,ld1) (ls2,ld2) = ls_equal ls1 ls2 && match ld1,ld2 with
| Some (_,f1), Some (_,f2) -> f_equal f1 f2
| Some (_,f1), Some (_,f2) -> t_equal f1 f2
| None, None -> true
| _ -> false
let eq_iax (pr1,fr1) (pr2,fr2) =
pr_equal pr1 pr2 && f_equal fr1 fr2
pr_equal pr1 pr2 && t_equal fr1 fr2
let eq_ind (ps1,al1) (ps2,al2) =
ls_equal ps1 ps2 && list_all2 eq_iax al1 al2
......@@ -324,7 +324,7 @@ module Hsdecl = Hashcons.Make (struct
| Dlogic l1, Dlogic l2 -> list_all2 eq_ld l1 l2
| Dind l1, Dind l2 -> list_all2 eq_ind l1 l2
| Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
k1 = k2 && pr_equal pr1 pr2 && f_equal f1 f2
k1 = k2 && pr_equal pr1 pr2 && t_equal f1 f2
| _,_ -> false
let hs_td (ts,td) = match td with
......@@ -332,9 +332,9 @@ module Hsdecl = Hashcons.Make (struct
| Talgebraic l -> 1 + Hashcons.combine_list ls_hash (ts_hash ts) l
let hs_ld (ls,ld) = Hashcons.combine (ls_hash ls)
(Hashcons.combine_option (fun (_,f) -> f_hash f) ld)
(Hashcons.combine_option (fun (_,f) -> t_hash f) ld)
let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (f_hash f)
let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (t_hash f)
let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
......@@ -390,7 +390,7 @@ let syms_ls s ls = Sid.add ls.ls_name s
let syms_ty s ty = ty_s_fold syms_ts s ty
let syms_term s t = t_s_fold syms_ts syms_ls s t
let syms_fmla s f = f_s_fold syms_ts syms_ls s f
let syms_fmla s f = t_s_fold syms_ts syms_ls s f
let create_ty_decl tdl =
if tdl = [] then raise EmptyDecl;
......@@ -465,7 +465,7 @@ let rec f_pos_ps sps pol f = match f.t_node, pol with
f_pos_ps sps (option_map not pol) f
| Tif (f,g,h), _ ->
f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
| _ -> f_all (t_pos_ps sps) (f_pos_ps sps pol) f
| _ -> t_all (t_pos_ps sps) (f_pos_ps sps pol) f
let create_ind_decl idl =
if idl = [] then raise EmptyDecl;
......@@ -548,16 +548,16 @@ let decl_map_fold fnT fnF acc d =
match d.d_node with
| Dtype _ -> acc, d
| Dprop (k,pr,f) ->
let acc, f = f_map_fold fnT fnF acc f in
let acc, f = t_map_fold fnT fnF acc f in
acc, create_prop_decl k pr f
| Dind l ->
let acc, l =
list_rpair_map_fold (list_rpair_map_fold (f_map_fold fnT fnF)) acc l in
list_rpair_map_fold (list_rpair_map_fold (t_map_fold fnT fnF)) acc l in
acc, create_ind_decl l
| Dlogic l ->
let acc, l =
list_rpair_map_fold (option_map_fold
(rpair_map_fold (f_map_fold fnT fnF))) acc l in
(rpair_map_fold (t_map_fold fnT fnF))) acc l in
acc, create_logic_decl l
......@@ -642,11 +642,11 @@ let rec check_matchT kn () t = match t.t_node with
and check_matchF kn () f = match f.t_node with
| Tcase (t1,bl) ->
let bl = List.map (fun b -> let p,f = f_open_branch b in [p],f) bl in
ignore (try Pattern.CompileFmla.compile (find_constructors kn) [t1] bl
let bl = List.map (fun b -> let p,f = t_open_branch b in [p],f) bl in
ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,f)));
f_fold (check_matchT kn) (check_matchF kn) () f
| _ -> f_fold (check_matchT kn) (check_matchF kn) () f
t_fold (check_matchT kn) (check_matchF kn) () f
| _ -> t_fold (check_matchT kn) (check_matchF kn) () f
let check_match kn d = decl_fold (check_matchT kn) (check_matchF kn) () d
......
src/core/pattern.ml
View file @ 903df0ef
......@@ -150,11 +150,3 @@ module CompileTerm = Compile (struct
let mk_case t bl = t_case t bl
end)
module CompileFmla = Compile (struct
type action = fmla
type branch = fmla_branch
let mk_let v t f = f_let_close_simp v t f
let mk_branch p f = f_close_branch p f
let mk_case t bl = f_case t bl
end)
src/core/pattern.mli
View file @ 903df0ef
......@@ -42,9 +42,3 @@ module CompileTerm : sig
val compile : (tysymbol -> lsymbol list) ->
term list -> (pattern list * term) list -> term
end
module CompileFmla : sig
val compile : (tysymbol -> lsymbol list) ->
term list -> (pattern list * fmla) list -> fmla
end
src/core/pretty.ml
View file @ 903df0ef
......@@ -246,7 +246,7 @@ and print_tnode pri fmt t = match t.t_node with
fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
print_term t1 (print_list newline print_tbranch) bl
| Teps fb ->
let v,f = f_open_bound fb in
let v,f = t_open_bound fb in
fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
print_vsty v print_fmla f;
forget_var v
......@@ -274,7 +274,7 @@ and print_fnode pri fmt f = match f.t_node with
fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
print_fmla f1 print_fmla f2 print_fmla f3
| Tlet (t,f) ->
let v,f = f_open_bound f in
let v,f = t_open_bound f in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
print_vs v (print_lterm 4) t print_fmla f;
forget_var v
......@@ -289,7 +289,7 @@ and print_tbranch fmt br =
Svs.iter forget_var p.pat_vars
and print_fbranch fmt br =
let p,f = f_open_branch br in
let p,f = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
Svs.iter forget_var p.pat_vars
......@@ -297,7 +297,7 @@ and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma print_expr)) tl
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
and print_expr fmt = e_map (print_term fmt) (print_fmla fmt)
(** Declarations *)
......
src/core/term.ml
View file @ 903df0ef
This diff is collapsed.
src/core/term.mli
View file @ 903df0ef
This diff is collapsed.
src/core/theory.ml
View file @ 903df0ef
......@@ -459,7 +459,7 @@ let cl_find_ls cl ls =
cl.ls_table <- Mls.add ls ls' cl.ls_table;
ls'
let cl_trans_fmla cl f = f_s_map (cl_find_ts cl) (cl_find_ls cl) f
let cl_trans_fmla cl f = t_s_map (cl_find_ts cl) (cl_find_ls cl) f
let cl_find_pr cl pr =
if not (Sid.mem pr.pr_name cl.cl_local) then pr
......
src/parser/denv.ml
View file @ 903df0ef
......@@ -236,7 +236,7 @@ and fmla env = function
| Fbinop (op, f1, f2) ->
f_binary op (fmla env f1) (fmla env f2)
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
t_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, uqu, trl, f1) ->
let uquant env (id,ty) =
let v = create_user_vs id (ty_of_dty ty) in
......@@ -256,17 +256,17 @@ and fmla env = function
let v = create_user_vs id (t_type e1) in
let env = Mstr.add id.id v env in
let f2 = fmla env f2 in
f_let_close v e1 f2
t_let_close v e1 f2
| Fmatch (t, bl) ->
let branch (p,e) =
let env, p = pattern env p in f_close_branch p (fmla env e)
let env, p = pattern env p in t_close_branch p (fmla env e)
in
f_case (term env t) (List.map branch bl)
t_case (term env t) (List.map branch bl)
| (Fnamed _) as f ->
let rec collect p ll = function
| Fnamed (Lstr l, e) -> collect p (l::ll) e
| Fnamed (Lpos p, e) -> collect (Some p) ll e
| e -> f_label ?loc:p ll (fmla env e)
| e -> t_label ?loc:p ll (fmla env e)
in
collect None [] f
| Fvar f ->
......@@ -345,7 +345,7 @@ and specialize_term_node ~loc htv = function
in
Tmatch (specialize_term ~loc htv t1, List.map branch bl)
| Term.Teps fb ->
let v, f = f_open_bound fb in
let v, f = t_open_bound fb in
Teps (ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty,
specialize_fmla ~loc htv f)
| Term.Fquant _ | Term.Fbinop _ | Term.Fnot _
......@@ -376,11 +376,11 @@ and specialize_fmla_node ~loc htv = function
Fif (specialize_fmla ~loc htv f1,
specialize_fmla ~loc htv f2, specialize_fmla ~loc htv f3)
| Term.Tlet (t1, f2b) ->
let v, f2 = f_open_bound f2b in
let v, f2 = t_open_bound f2b in
Flet (specialize_term ~loc htv t1,
ident_of_vs ~loc v, specialize_fmla ~loc htv f2)
| Term.Tcase (t, fbl) ->
let branch b = let p, f = f_open_branch b in
let branch b = let p, f = t_open_branch b in
specialize_pattern ~loc htv p, specialize_fmla ~loc htv f
in
Fmatch (specialize_term ~loc htv t, List.map branch fbl)
......
src/printer/alt_ergo.ml
View file @ 903df0ef
......@@ -139,7 +139,7 @@ let rec print_fmla info fmt f = match f.t_node with
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_expr info fmt = e_map (print_term info fmt) (print_fmla info fmt)
and print_triggers info fmt tl =
let filter = function
......
src/printer/coq.ml
View file @ 903df0ef
......@@ -227,7 +227,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
(print_term info) t
(print_list newline (print_tbranch info)) bl
| Teps fb ->
let v,f = f_open_bound fb in
let v,f = t_open_bound fb in
fprintf fmt (protect_on opr "epsilon %a.@ %a")
(print_vsty info) v (print_opl_fmla info) f;
forget_var v
......@@ -274,7 +274,7 @@ and print_fnode opl opr info fmt f = match f.t_node with
| Fnot f ->
fprintf fmt (protect_on opr "~ %a") (print_opl_fmla info) f
| Tlet (t,f) ->
let v,f = f_open_bound f in
let v,f = t_open_bound f in
fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
print_vs v (print_opl_term info) t (print_opl_fmla info) f;
forget_var v
......@@ -300,7 +300,7 @@ and print_tbranch info fmt br =
Svs.iter forget_var p.pat_vars
and print_fbranch info fmt br =
let p,f = f_open_branch br in
let p,f = t_open_branch br in
fprintf fmt "@[<hov 4>| %a =>@ %a@]"
(print_pat info) p (print_fmla info) f;
Svs.iter forget_var p.pat_vars
......@@ -309,7 +309,7 @@ and print_tl info fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma (print_expr info))) tl
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_expr info fmt = e_map (print_term info fmt) (print_fmla info fmt)
(** Declarations *)
......@@ -507,7 +507,7 @@ let print_decl ~old info fmt d = match d.d_node with
| Dind il -> print_list nothing (print_ind_decl info) fmt il
| Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem -> ()
| Dprop (k,pr,f) ->
let params = f_ty_freevars Stv.empty f in
let params = t_ty_freevars Stv.empty f in
fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a"
(print_pkind info) k
print_pr pr
......
src/printer/cvc3.ml
View file @ 903df0ef
......@@ -102,12 +102,12 @@ let rec iter_complex_type info fmt () ty = match ty.ty_node with
end
let find_complex_type info fmt f =
f_ty_fold (iter_complex_type info fmt) () f
t_ty_fold (iter_complex_type info fmt) () f
let find_complex_type_expr info fmt f =
e_fold
(t_ty_fold (iter_complex_type info fmt))
(f_ty_fold (iter_complex_type info fmt))
(t_ty_fold (iter_complex_type info fmt))
() f
let print_type info fmt =
......@@ -207,7 +207,7 @@ and print_fmla info fmt f = match f.t_node with
fprintf fmt "@[(IF %a@ THEN %a@ ELSE %a ENDIF)@]"
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
| Tlet (t1, tb) ->
let v, f2 = f_open_bound tb in
let v, f2 = t_open_bound tb in
fprintf fmt "@[(LET %a =@ %a IN@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v
......@@ -215,7 +215,7 @@ and print_fmla info fmt f = match f.t_node with
"cvc3 : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_expr info fmt = e_map (print_term info fmt) (print_fmla info fmt)
and print_triggers info fmt = function
| [] -> ()
......
src/printer/simplify.ml
View file @ 903df0ef
......@@ -130,7 +130,7 @@ and print_fmla info fmt f = match f.t_node with
unsupportedFmla f "simplify : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_expr info fmt = e_map (print_term info fmt) (print_fmla info fmt)
and print_trigger info fmt = function
| [] -> ()
......
src/printer/smt.ml
View file @ 903df0ef
......@@ -146,7 +146,7 @@ and print_fmla info fmt f = match f.t_node with
fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
| Tlet (t1, tb) ->
let v, f2 = f_open_bound tb in
let v, f2 = t_open_bound tb in
fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v
......@@ -154,7 +154,7 @@ and print_fmla info fmt f = match f.t_node with
"smtv1 : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_expr info fmt = e_map (print_term info fmt) (print_fmla info fmt)
and print_triggers info fmt tl = print_list comma (print_expr info) fmt tl
......
src/printer/smt2.ml
View file @ 903df0ef
......@@ -96,12 +96,12 @@ let iter_complex_type info fmt () ty =
let find_complex_type info fmt f =
f_ty_fold (iter_complex_type info fmt) () f
t_ty_fold (iter_complex_type info fmt) () f
let find_complex_type_expr info fmt f =
e_fold
(t_ty_fold (iter_complex_type info fmt))
(f_ty_fold (iter_complex_type info fmt))
(t_ty_fold (iter_complex_type info fmt))
() f
let print_type info fmt ty =
......@@ -212,7 +212,7 @@ and print_fmla info fmt f = match f.t_node with
fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
| Tlet (t1, tb) ->
let v, f2 = f_open_bound tb in
let v, f2 = t_open_bound tb in
fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v
......@@ -220,7 +220,7 @@ and print_fmla info fmt f = match f.t_node with
"smtv2 : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_expr info fmt = e_map (print_term info fmt) (print_fmla info fmt)
and print_trigger info fmt e = fprintf fmt "(%a)" (print_expr info) e
......
src/printer/tptp.ml
View file @ 903df0ef
......@@ -101,7 +101,7 @@ and print_fmla info fmt f = match f.t_node with
(* fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3 *)
| Tlet (_, _) -> unsupportedFmla f "Tlet not supported"
(* let v, f2 = f_open_bound tb in
(* let v, f2 = t_open_bound tb in
fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v *)
......
src/printer/why3.ml
View file @ 903df0ef
......@@ -213,7 +213,7 @@ and print_tnode pri fmt t = match t.t_node with
fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
print_term t1 (print_list newline print_tbranch) bl
| Teps fb ->
let v,f = f_open_bound fb in
let v,f = t_open_bound fb in
fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
print_vsty v print_fmla f;
forget_var v
......@@ -247,7 +247,7 @@ and print_fnode pri fmt f = match f.t_node with
fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
print_fmla f1 print_fmla f2 print_fmla f3
| Tlet (t,f) ->
let v,f = f_open_bound f in
let v,f = t_open_bound f in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
print_vs v (print_lterm 4) t print_fmla f;
forget_var v
......@@ -262,7 +262,7 @@ and print_tbranch fmt br =
Svs.iter forget_var p.pat_vars
and print_fbranch fmt br =
let p,f = f_open_branch br in
let p,f = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
Svs.iter forget_var p.pat_vars
......@@ -270,7 +270,7 @@ and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma print_expr)) tl
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
and print_expr fmt = e_map (print_term fmt) (print_fmla fmt)
(** Declarations *)
......
src/programs/pgm_fastwp.ml
View file @ 903df0ef
......@@ -97,7 +97,7 @@ end = struct
t_map (term_at env old cur s) (fmla_at env old cur s) t
and fmla_at env old cur s f =
f_map (term_at env old cur s) (fmla_at env old cur s) f
t_map (term_at env old cur s) (fmla_at env old cur s) f
let term env s t = term_at env None None s t
let fmla env ?old s f = fmla_at env old None s f
......
src/programs/pgm_types.ml
View file @ 903df0ef
......@@ -362,20 +362,20 @@ end = struct
let subst_post ts s ((v, q), ql) =
let ts = Mtv.map purify ts in
let vq = let s, v = subst_var ts s v in v, f_ty_subst ts s q in
let vq = let s, v = subst_var ts s v in v, t_ty_subst ts s q in
let handler (e, (v, q)) = match v with
| None ->
e, (v, f_ty_subst ts s q)
e, (v, t_ty_subst ts s q)
| Some v ->
let s, v = subst_var ts s v in
e, (Some v, f_ty_subst ts s q)
e, (Some v, t_ty_subst ts s q)
in
vq, List.map handler ql
let rec subst_type_c ts s c =
{ c_result_type = subst_type_v ts s c.c_result_type;
c_effect = E.subst ts c.c_effect;
c_pre = (let ts = Mtv.map purify ts in f_ty_subst ts s c.c_pre);
c_pre = (let ts = Mtv.map purify ts in t_ty_subst ts s c.c_pre);
c_post = subst_post ts s c.c_post; }
and subst_type_v ts s = function
......
src/programs/pgm_typing.ml
View file @ 903df0ef
......@@ -1278,7 +1278,7 @@ let declare_global ls pv =
Hls.add globals ls pv
let rec fmla_effect ef f =
f_map_fold term_effect fmla_effect ef f
t_map_fold term_effect fmla_effect ef f
and term_effect ef t = match t.t_node with
| Term.Tapp (ls, []) when Hls.mem globals ls ->
......
src/programs/pgm_wp.ml
View file @ 903df0ef
......@@ -42,10 +42,10 @@ let wp_and ?(sym=false) f1 f2 =
(* if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2) *)
let f = f_and_simp f1 f2 in
(* experiment, but does not work
let f = f_label_add Split_goal.stop_split f in
let f = t_label_add Split_goal.stop_split f in
*)
match f.t_node with
| Fbinop (Fand, _, _) when not sym -> f_label_add Split_goal.asym_split f
| Fbinop (Fand, _, _) when not sym -> t_label_add Split_goal.asym_split f
| _ -> f
let wp_ands ?(sym=false) fl =
......@@ -66,16 +66,16 @@ let is_arrow_ty ty = match ty.ty_node with
let wp_forall v f =
if is_arrow_ty v.vs_ty then f else
if f_occurs_single v f then f_forall_close_simp [v] [] f else f
if t_occurs_single v f then f_forall_close_simp [v] [] f else f
(*
match f.t_node with
| Fbinop (Fimplies, {f_node = Fapp (s,[{t_node = Tvar u};r])},h)
when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
f_subst_single v r h
t_subst_single v r h
| Fbinop (Fimplies, {f_node = Fbinop (Fand, g,
{f_node = Fapp (s,[{t_node = Tvar u};r])})},h)
when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
f_subst_single v r (f_implies_simp g h)
t_subst_single v r (f_implies_simp g h)
| _ when f_occurs_single v f ->
f_forall_close_simp [v] [] f
| _ ->
......@@ -107,7 +107,7 @@ let add_binders = List.fold_right add_binder
(* replace old(t) with at(t,lab) everywhere in formula f *)
let rec old_label env lab f =
f_map (old_label_term env lab) (old_label env lab) f
t_map (old_label_term env lab) (old_label env lab) f
and old_label_term env lab t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (find_ls ~pure:true env "old") ->
......@@ -118,7 +118,7 @@ and old_label_term env lab t = match t.t_node with
(* replace at(t,lab) with t everywhere in formula f *)
let rec erase_label env lab f =
f_map (erase_label_term env lab) (erase_label env lab) f
t_map (erase_label_term env lab) (erase_label env lab) f
and erase_label_term env lab t = match t.t_node with
| Tapp (ls, [t; {t_node = Tvar l}])
......@@ -128,7 +128,7 @@ and erase_label_term env lab t = match t.t_node with
t_map (erase_label_term env lab) (erase_label env lab) t
let rec unref env s f =
f_map (unref_term env s) (unref env s) f
t_map (unref_term env s) (unref env s) f
and unref_term env s t = match t.t_node with
(***
......@@ -237,7 +237,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, f_subst (subst1 v' (t_var v)) f'
| Some v', Some v -> Some v, t_subst (subst1 v' (t_var v)) f'
| None, None -> None, f'
| _ -> assert false
in
......@@ -247,7 +247,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 f_subst (subst1 res' (t_var res)) f'
else t_subst (subst1 res' (t_var res)) f'
in
quantify_res f' f (Some res)
in
......@@ -292,7 +292,7 @@ let saturate_post ef q (_, ql) =
(* maximum *)
let is_default_post = f_equal f_true
let is_default_post = t_equal f_true
let sup ((q, ql) : post) (_, ql') =
assert (List.length ql = List.length ql');
......@@ -312,7 +312,7 @@ let term_at env lab t =
e_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
let wp_expl l f =
f_label ?loc:f.t_loc (("expl:"^l)::Split_goal.stop_split::f.t_label) f
t_label ?loc:f.t_loc (("expl:"^l)::Split_goal.stop_split::f.t_label) f
let while_post_block env inv var lab e =
let decphi = match var with
......@@ -344,7 +344,7 @@ let well_founded_rel = function
let wp_label ?loc f =
if List.mem "WP" f.t_label then f
else f_label ?loc ("WP"::f.t_label) f
else t_label ?loc ("WP"::f.t_label) f
let t_True env =
t_app (find_ls ~pure:true env "True") []
......@@ -352,7 +352,7 @@ let t_True env =
(*
let add_expl msg f =
f_label_add Split_goal.stop_split (f_label_add ("expl:"^msg) f)
t_label_add Split_goal.stop_split (t_label_add ("expl:"^msg) f)
*)
(*
......@@ -376,15 +376,15 @@ let rec wp_expr env rm e q =
and wp_desc env rm e q = match e.expr_desc with
| Elogic t ->
let (v, q), _ = q in
f_subst_single v t q
t_subst_single v t q
| Elocal v ->
let (res, q), _ = q in
f_subst (subst1 res (t_var v.pv_pure)) q
t_subst (subst1 res (t_var v.pv_pure)) q
| Eglobal { ps_kind = PSfun _ } ->
let (_, q), _ = q in q
| Eglobal { ps_kind = PSvar pv } ->
let (v, q), _ = q in
f_subst_single v (t_var pv.pv_pure) q
t_subst_single v (t_var pv.pv_pure) q
| Eglobal { ps_kind = PSlogic } ->
assert false
| Efun (bl, t) ->
......@@ -395,7 +395,7 @@ and wp_desc env rm e q = match e.expr_desc with
let w2 = wp_expr env rm e2 (filter_post e2.expr_effect q) 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, f_subst (subst1 x.pv_pure t1) w2 in
let q1 = v1, t_subst (subst1 x.pv_pure t1) w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_expr env rm e1 q1
| Eletrec (dl, e1) ->
......@@ -409,7 +409,7 @@ and wp_desc env rm e q = match e.expr_desc with
let res = v_result e1.expr_type in
let test = f_equ (t_var res) (t_True env) in
let test = wp_label ~loc:e1.expr_loc test in
let q1 = f_if test w2 w3 in
let q1 = t_if test w2 w3 in
saturate_post e1.expr_effect (res, q1) q
in
wp_expr env rm e1 q1
......@@ -435,11 +435,11 @@ and wp_desc env rm e q = match e.expr_desc with
wp_expr env rm e (filter_post e.expr_effect q)
| Ematch (x, bl) ->
let branch (p, e) =
f_close_branch p.ppat_pat
t_close_branch p.ppat_pat
(wp_expr env rm e (filter_post e.expr_effect q))
in
let t = t_var x.pv_pure in
f_case t (List.map branch bl)
t_case t (List.map branch bl)
| Eabsurd ->
f_false
| Eraise (x, None) ->
......@@ -496,13 +496,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 = t_app add [t_var x.pv_pure; incr] ty_int in
let post = f_subst (subst1 x.pv_pure xp1) inv in
let post = t_subst (subst1 x.pv_pure xp1) inv in