Commit 134580a4 authored by Andrei Paskevich's avatar Andrei Paskevich

revise Term: provide close_bound, close_branch, and close_quant

parent 6b615e1f
......@@ -46,12 +46,12 @@ let check_fvs f =
let make_fs_defn fs vl t =
let hd = t_app fs (List.map t_var vl) t.t_ty in
let fd = f_forall vl [] (f_equ hd t) in
let fd = f_forall_close vl [] (f_equ hd t) in
fs, Some (fs, check_fvs fd)
let make_ps_defn ps vl f =
let hd = f_app ps (List.map t_var vl) in
let pd = f_forall vl [] (f_iff hd f) in
let pd = f_forall_close vl [] (f_iff hd f) in
ps, Some (ps, check_fvs pd)
let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
......
......@@ -24,8 +24,10 @@ open Term
module type Action = sig
type action
type branch
val mk_let : vsymbol -> term -> action -> action
val mk_case : term -> (pattern * action) list -> action
val mk_branch : pattern -> action -> branch
val mk_case : term -> branch list -> action
end
exception ConstructorExpected of lsymbol
......@@ -124,28 +126,32 @@ module Compile (X : Action) = struct
| _ ->
let base =
if Sls.for_all (fun cs -> Mls.mem cs types) css
then [] else [pat_wild ty, comp_wilds ()]
then [] else [mk_branch (pat_wild ty) (comp_wilds ())]
in
let add cs ql acc =
let get_vs q = create_vsymbol (id_fresh "x") q.pat_ty in
let vl = List.rev_map get_vs ql in
let pl = List.rev_map pat_var vl in
let al = List.rev_map t_var vl in
(pat_app cs pl ty, comp_cases cs al) :: acc
mk_branch (pat_app cs pl ty) (comp_cases cs al) :: acc
in
mk_case t (Mls.fold add types base)
end
module CompileTerm = Compile (struct
module CompileTerm = Compile (struct
type action = term
let mk_let v s t = t_let v s t
let mk_case t bl = t_case t bl (snd (List.hd bl)).t_ty
type branch = term_branch
let mk_let v s t = t_let_close v s t
let mk_branch p t = t_close_branch p t
let mk_case t bl = t_case t bl
end)
module CompileFmla = Compile (struct
module CompileFmla = Compile (struct
type action = fmla
let mk_let v t f = f_let v t f
let mk_case t bl = f_case t bl
type branch = fmla_branch
let mk_let v t f = f_let_close v t f
let mk_branch p f = f_close_branch p f
let mk_case t bl = f_case t bl
end)
......@@ -24,8 +24,10 @@ open Term
module type Action = sig
type action
type branch
val mk_let : vsymbol -> term -> action -> action
val mk_case : term -> (pattern * action) list -> action
val mk_branch : pattern -> action -> branch
val mk_case : term -> branch list -> action
end
exception ConstructorExpected of lsymbol
......
This diff is collapsed.
......@@ -179,17 +179,61 @@ val e_equal : expr -> expr -> bool
val tr_equal : trigger list -> trigger list -> bool
(** close bindings *)
val t_close_bound : vsymbol -> term -> term_bound
val f_close_bound : vsymbol -> fmla -> fmla_bound
val t_close_branch : pattern -> term -> term_branch
val f_close_branch : pattern -> fmla -> fmla_branch
val f_close_quant : vsymbol list -> trigger list -> fmla -> fmla_quant
(** open bindings *)
val t_open_bound : term_bound -> vsymbol * term
val f_open_bound : fmla_bound -> vsymbol * fmla
val t_open_branch : term_branch -> pattern * term
val f_open_branch : fmla_branch -> pattern * fmla
val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
val f_open_forall : fmla -> vsymbol list * fmla
val f_open_exists : fmla -> vsymbol list * fmla
(** open bindings with optimized closing callbacks *)
val t_open_bound_cb :
term_bound -> vsymbol * term * (vsymbol -> term -> term_bound)
val f_open_bound_cb :
fmla_bound -> vsymbol * fmla * (vsymbol -> fmla -> fmla_bound)
val t_open_branch_cb :
term_branch -> pattern * term * (pattern -> term -> term_branch)
val f_open_branch_cb :
fmla_branch -> pattern * fmla * (pattern -> fmla -> fmla_branch)
val f_open_quant_cb :
fmla_quant -> vsymbol list * trigger list * fmla *
(vsymbol list -> trigger list -> fmla -> fmla_quant)
(** smart constructors for term *)
val t_var : vsymbol -> term
val t_const : constant -> ty -> term
val t_const : constant -> term
val t_int_const : string -> term
val t_real_const : real_constant -> term
val t_app : lsymbol -> term list -> ty -> term
val t_if : fmla -> term -> term -> term
val t_let : vsymbol -> term -> term -> term
val t_case : term -> (pattern * term) list -> ty -> term
val t_eps : vsymbol -> fmla -> term
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
val t_eps : fmla_bound -> term
val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> fmla -> term
val t_app_infer : lsymbol -> term list -> term
val t_app_inst : lsymbol -> term list -> ty -> ty Mtv.t
......@@ -201,20 +245,25 @@ val t_label_copy : term -> term -> term
(** smart constructors for fmla *)
val f_app : lsymbol -> term list -> fmla
val f_forall : vsymbol list -> trigger list -> fmla -> fmla
val f_exists : vsymbol list -> trigger list -> fmla -> fmla
val f_quant : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_quant : quant -> fmla_quant -> fmla
val f_forall : fmla_quant -> fmla
val f_exists : fmla_quant -> fmla
val f_binary : binop -> fmla -> fmla -> fmla
val f_and : fmla -> fmla -> fmla
val f_or : fmla -> fmla -> fmla
val f_implies : fmla -> fmla -> fmla
val f_iff : fmla -> fmla -> fmla
val f_binary : binop -> fmla -> fmla -> fmla
val f_not : fmla -> fmla
val f_true : fmla
val f_false : fmla
val f_if : fmla -> fmla -> fmla -> fmla
val f_let : vsymbol -> term -> fmla -> fmla
val f_case : term -> (pattern * fmla) list -> fmla
val f_let : term -> fmla_bound -> fmla
val f_case : term -> fmla_branch list -> fmla
val f_let_close : vsymbol -> term -> fmla -> fmla
val f_quant_close : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_close : vsymbol list -> trigger list -> fmla -> fmla
val f_app_inst : lsymbol -> term list -> ty Mtv.t
......@@ -224,33 +273,25 @@ val f_label_copy : fmla -> fmla -> fmla
(** constructors with propositional simplification *)
val f_forall_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_quant_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_quant_simp : quant -> fmla_quant -> fmla
val f_forall_simp : fmla_quant -> fmla
val f_exists_simp : fmla_quant -> fmla
val f_binary_simp : binop -> fmla -> fmla -> fmla
val f_and_simp : fmla -> fmla -> fmla
val f_and_simp_l : fmla list -> fmla
val f_or_simp : fmla -> fmla -> fmla
val f_or_simp_l : fmla list -> fmla
val f_implies_simp : fmla -> fmla -> fmla
val f_iff_simp : fmla -> fmla -> fmla
val f_binary_simp : binop -> fmla -> fmla -> fmla
val f_not_simp : fmla -> fmla
val t_if_simp : fmla -> term -> term -> term
val f_if_simp : fmla -> fmla -> fmla -> fmla
val f_let_simp : vsymbol -> term -> fmla -> fmla
(** open bindings *)
val f_let_simp : term -> fmla_bound -> fmla
val t_open_bound : term_bound -> vsymbol * term
val f_open_bound : fmla_bound -> vsymbol * fmla
val t_open_branch : term_branch -> pattern * term
val f_open_branch : fmla_branch -> pattern * fmla
val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
val f_open_forall : fmla -> vsymbol list * fmla
val f_open_exists : fmla -> vsymbol list * fmla
val f_let_close_simp : vsymbol -> term -> fmla -> fmla
val f_quant_close_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_close_simp : vsymbol list -> trigger list -> fmla -> fmla
(** expr and trigger traversal *)
......
......@@ -187,7 +187,7 @@ let rec term env t = match t.dt_node with
assert (Mstr.mem x env);
t_var (Mstr.find x env)
| Tconst c ->
t_const c (ty_of_dty t.dt_ty)
t_const c
| Tapp (s, tl) ->
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| Tif (f, t1, t2) ->
......@@ -198,14 +198,12 @@ let rec term env t = match t.dt_node with
let v = create_vsymbol (id_user x loc) ty in
let env = Mstr.add x v env in
let e2 = term env e2 in
t_let v e1 e2
t_let_close v e1 e2
| Tmatch (t1, bl) ->
let branch (p,e) =
let env, p = pattern env p in (p, term env e)
let env, p = pattern env p in t_close_branch p (term env e)
in
let bl = List.map branch bl in
let ty = (snd (List.hd bl)).t_ty in
t_case (term env t1) bl ty
t_case (term env t1) (List.map branch bl)
| Tnamed (x, e1) ->
let e1 = term env e1 in
t_label_add x e1
......@@ -214,7 +212,7 @@ let rec term env t = match t.dt_node with
let v = create_vsymbol (id_user x loc) ty in
let env = Mstr.add x v env in
let e1 = fmla env e1 in
t_eps v e1
t_eps_close v e1
and fmla env = function
| Ftrue ->
......@@ -239,7 +237,7 @@ and fmla env = function
| TRfmla f -> Fmla (fmla env f)
in
let trl = List.map (List.map trigger) trl in
f_quant q vl trl (fmla env f1)
f_quant_close q vl trl (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, { id = x ; id_loc = loc }, f2) ->
......@@ -248,10 +246,10 @@ and fmla env = function
let v = create_vsymbol (id_user x loc) ty in
let env = Mstr.add x v env in
let f2 = fmla env f2 in
f_let v e1 f2
f_let_close v e1 f2
| Fmatch (t, bl) ->
let branch (p,e) =
let env, p = pattern env p in (p, fmla env e)
let env, p = pattern env p in f_close_branch p (fmla env e)
in
f_case (term env t) (List.map branch bl)
| Fnamed (x, f1) ->
......
......@@ -560,10 +560,10 @@ let add_projection cl p (fs,tyarg,tyval) th =
| _ -> pat_wild (ty_inst m ty)
in
let al = List.map2 per_param cs.ls_args pl in
pat_app cs al tyarg, t_var vs
t_close_branch (pat_app cs al tyarg) (t_var vs)
in
let vs = create_vsymbol (id_fresh "u") tyarg in
let t = t_case (t_var vs) (List.map per_cs cl) tyval in
let t = t_case (t_var vs) (List.map per_cs cl) in
let d = make_fs_defn fs [vs] t in
add_logic_decl th [d]
......
......@@ -620,7 +620,7 @@ let rec iexpr gl env e =
and iexpr_desc gl env loc ty = function
| DEconstant c ->
IElogic (t_const c ty)
IElogic (t_const c)
| DElocal (x, tyv) ->
IElocal (Mstr.find x env, type_v gl env tyv)
| DEglobal (ls, tyv) ->
......
......@@ -57,7 +57,7 @@ let is_arrow_ty env ty = match ty.ty_node with
| _ -> false
let wp_forall env v f =
if is_arrow_ty env v.vs_ty then f else f_forall_simp [v] [] f
if is_arrow_ty env v.vs_ty then f else f_forall_close_simp [v] [] f
(* utility functions for building WPs *)
......@@ -252,7 +252,7 @@ let rec wp_expr env e q =
and wp_desc env e q = match e.expr_desc with
| Elogic t ->
let (v, q), _ = q in
f_let v t q
f_let_close v t q
| Elocal v ->
let (res, q), _ = q in
f_subst (subst1 res (t_var v)) q
......@@ -305,7 +305,9 @@ and wp_desc env e q = match e.expr_desc with
in
w
| Ematch (x, bl) ->
let branch (p, e) = p, wp_expr env e (filter_post e.expr_effect q) in
let branch (p, e) =
f_close_branch p (wp_expr env e (filter_post e.expr_effect q))
in
let t = t_var x in
f_case t (List.map branch bl)
| Eskip ->
......
......@@ -77,7 +77,7 @@ let rec rewriteT kn state t = match t.t_node with
match p with
| { pat_node = Papp (cs,pl) } ->
let add_var e p pj = match p.pat_node with
| Pvar v -> t_let v (t_app pj [t1] v.vs_ty) e
| Pvar v -> t_let_close v (t_app pj [t1] v.vs_ty) e
| _ -> Printer.unsupportedTerm t uncompiled
in
let pjl = Mls.find cs state.pj_map in
......@@ -125,13 +125,13 @@ and rewriteF kn state av sign f = match f.f_node with
let hd = t_app cs (List.map t_var vl) t1.t_ty in
match t1.t_node with
| Tvar v when Svs.mem v av ->
let hd = f_let v hd e in if sign
then f_forall_simp vl [] hd
else f_exists_simp vl [] hd
let hd = f_let_close v hd e in if sign
then f_forall_close_simp vl [] hd
else f_exists_close_simp vl [] hd
| _ ->
let hd = f_equ t1 hd in if sign
then f_forall_simp vl [] (f_implies_simp hd e)
else f_exists_simp vl [] (f_and_simp hd e)
then f_forall_close_simp vl [] (f_implies_simp hd e)
else f_exists_close_simp vl [] (f_and_simp hd e)
in
let ts = match t1.t_ty.ty_node with
| Tyapp (ts,_) -> ts
......@@ -140,12 +140,12 @@ and rewriteF kn state av sign f = match f.f_node with
let op = if sign then f_and_simp else f_or_simp in
map_join_left find op (find_constructors kn ts)
| Fquant (q, bf) when (q = Fforall && sign) || (q = Fexists && not sign) ->
let vl, tr, f1 = f_open_quant bf in
let tr' = tr_map (rewriteT kn state)
(rewriteF kn state Svs.empty sign) tr in
let vl, tr, f1, close = f_open_quant_cb bf in
let tr = tr_map (rewriteT kn state)
(rewriteF kn state Svs.empty sign) tr in
let av = List.fold_left (fun s v -> Svs.add v s) av vl in
let f1' = rewriteF kn state av sign f1 in
if f_equal f1' f1 && tr_equal tr' tr then f else f_quant q vl tr' f1'
let f1 = rewriteF kn state av sign f1 in
f_quant q (close vl tr f1)
| Fbinop (o, _, _) when (o = Fand && sign) || (o = For && not sign) ->
f_map_sign (rewriteT kn state) (rewriteF kn state av) sign f
| Flet (t1, _) ->
......@@ -177,7 +177,7 @@ let add_type (state, task) ts csl =
let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in
let hd = t_app mt_ls (hd::mt_tl) mt_ty in
let vl = List.rev_append mt_vl (List.rev vl) in
let ax = f_forall vl [[Term hd]] (f_equ hd t) in
let ax = f_forall_close vl [[Term hd]] (f_equ hd t) in
add_decl tsk (create_prop_decl Paxiom pr ax)
in
let task = List.fold_left2 mt_add task csl mt_tl in
......@@ -195,7 +195,7 @@ let add_type (state, task) ts csl =
let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
let pr = create_prsymbol id in
let hh = t_app ls [hd] t.t_ty in
let ax = f_forall (List.rev vl) [[Term hd]] (f_equ hh t) in
let ax = f_forall_close (List.rev vl) [[Term hd]] (f_equ hh t) in
ls::pjl, add_decl tsk (create_prop_decl Paxiom pr ax)
in
let pjl,tsk = List.fold_left add ([],tsk) tl in
......@@ -214,7 +214,7 @@ let add_type (state, task) ts csl =
in
let ax_f = map_join_left mk_cs f_or csl in
let trgl = t_app mt_ls (ax_hd :: mt_tl) mt_ty in
let ax_f = f_forall (ax_vs :: mt_vl) [[Term trgl]] ax_f in
let ax_f = f_forall_close (ax_vs :: mt_vl) [[Term trgl]] ax_f in
let task = add_decl task (create_prop_decl Paxiom ax_pr ax_f) in
(* add the tag for enumeration if the type is one *)
let enum = List.for_all (fun ls -> ls.ls_args = []) csl in
......
......@@ -53,9 +53,12 @@ let rec t_insert hd t = match t.t_node with
f_if f1 (t_insert hd t2) (t_insert hd t3)
| Tlet (t1,bt) ->
let v,t2 = t_open_bound bt in
f_let v t1 (t_insert hd t2)
f_let_close v t1 (t_insert hd t2)
| Tcase (tl,bl) ->
let br b = let pl,t1 = t_open_branch b in pl, t_insert hd t1 in
let br b =
let pl,t1 = t_open_branch b in
f_close_branch pl (t_insert hd t1)
in
f_case tl (List.map br bl)
| _ -> f_equ_simp hd t
......@@ -64,9 +67,12 @@ let rec f_insert hd f = match f.f_node with
f_if f1 (f_insert hd f2) (f_insert hd f3)
| Flet (t1,bf) ->
let v,f2 = f_open_bound bf in
f_let v t1 (f_insert hd f2)
f_let_close v t1 (f_insert hd f2)
| Fcase (tl,bl) ->
let br b = let pl,f1 = f_open_branch b in pl, f_insert hd f1 in
let br b =
let pl,f1 = f_open_branch b in
f_close_branch pl (f_insert hd f1)
in
f_case tl (List.map br bl)
| _ -> f_iff_simp hd f
......@@ -78,13 +84,13 @@ let add_ld func pred axl d = match d with
| Term t when func ->
let nm = ls.ls_name.id_string ^ "_def" in
let hd = t_app ls (List.map t_var vl) t.t_ty in
let ax = f_forall vl [[Term hd]] (t_insert hd t) in
let ax = f_forall_close vl [[Term hd]] (t_insert hd t) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None)
| Fmla f when pred ->
let nm = ls.ls_name.id_string ^ "_def" in
let hd = f_app ls (List.map t_var vl) in
let ax = f_forall vl [[Fmla hd]] (f_insert hd f) in
let ax = f_forall_close vl [[Fmla hd]] (f_insert hd f) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None)
| _ -> axl, d
......
......@@ -26,16 +26,13 @@ open Decl
let rec elim_t letl contT t = match t.t_node with
| Tlet (t1,tb) ->
let u,t2 = t_open_bound tb in
let t_let e1 e2 =
if t_equal e1 t1 && t_equal e2 t2 then t else t_let u e1 e2
in
let cont_in t1 t2 = contT (t_let t1 t2) in
let u,t2,close = t_open_bound_cb tb in
let cont_in t1 t2 = contT (t_let t1 (close u t2)) in
let cont_let t1 = elim_t ((u,t1)::letl) (cont_in t1) t2 in
elim_t letl cont_let t1
| Tif (f,t1,t2) ->
let f = elim_f (fun f -> f) f in
let f = List.fold_left (fun f (v,t) -> f_let v t f) f letl in
let f = List.fold_left (fun f (v,t) -> f_let_close v t f) f letl in
f_if f (elim_t letl contT t1) (elim_t letl contT t2)
| Tcase _ ->
Printer.unsupportedTerm t
......@@ -72,7 +69,7 @@ let add_ld axl d = match d with
let nm = ls.ls_name.id_string ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
let hd = t_app ls (List.map t_var vl) t.t_ty in
let f = f_forall vl [[Term hd]] (elim_f (f_equ hd t)) in
let f = f_forall_close vl [[Term hd]] (elim_f (f_equ hd t)) in
create_prop_decl Paxiom pr f :: axl, (ls, None)
| _ ->
axl, make_ls_defn ls vl (e_map elim_t elim_f e)
......
......@@ -30,7 +30,7 @@ let exi vl (_,f) =
let rec descend f = match f.f_node with
| Fquant (Fforall,f) ->
let vl,tl,f = f_open_quant f in
f_exists vl tl (descend f)
f_exists_close vl tl (descend f)
| Fbinop (Fimplies,g,f) ->
f_and g (descend f)
| Fapp (_,tl) ->
......@@ -46,7 +46,7 @@ let inv acc (ps,al) =
let hd = f_app ps tl in
let dj = Util.map_join_left (exi tl) f_or al in
let hsdj = Simplify_formula.fmla_remove_quant (f_implies hd dj) in
let ax = f_forall vl [[Fmla hd]] hsdj in
let ax = f_forall_close vl [[Fmla hd]] hsdj in
let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
......
......@@ -227,12 +227,12 @@ let rec rewrite_term tenv tvar vsvar t =
conv_res_app tenv tvar p tl t.t_ty
| Tif (f, t1, t2) ->
t_if (fnF f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) -> let u,t2 = t_open_bound b in
let t1' = fnT vsvar t1 in
let (vsvar',u) = conv_vs_let vsvar u t1'.t_ty in
let t2' = fnT vsvar' t2 in
if t_equal t1' t1 && t_equal t2' t2 then t else
t_let u t1' t2'
| Tlet (t1, b) ->
let u,t2,close = t_open_bound_cb b in
let t1 = fnT vsvar t1 in
let (vsvar,u) = conv_vs_let vsvar u t1.t_ty in
let t2 = fnT vsvar t2 in
t_let t1 (close u t2)
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t
"Encoding decorate : I can't encode this term"
......@@ -260,22 +260,21 @@ and rewrite_fmla tenv tvar vsvar f =
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
f_app p tl
| Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
let (vsvar',vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1' = fnF vsvar' f1 in
(* Ici un trigger qui ne match pas assez de variables
peut tre gnr *)
let tl = tr_map (rewrite_term tenv tvar vsvar') (fnF vsvar') tl in
(*if f_equal f1' f1 && vsvar' == vsvar (*&& tr_equal tl' tl*) then f
else *)
let vl = List.rev vl in
f_quant q vl tl f1'
| Flet (t1, b) -> let u,f2 = f_open_bound b in
let t1' = fnT t1 in
let (vsvar,u) = conv_vs_let vsvar u t1'.t_ty in
let f2' = fnF vsvar f2 in
if t_equal t1' t1 && f_equal f2' f2 then f else
f_let u t1' f2'
| Fquant (q, b) ->
let vl, tl, f1, close = f_open_quant_cb b in
let (vsvar,vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut tre gnr *)
let tl = tr_map (rewrite_term tenv tvar vsvar) (fnF vsvar) tl in
let vl = List.rev vl in
f_quant q (close vl tl f1)
| Flet (t1, b) ->
let u,f2,close = f_open_bound_cb b in
let t1 = fnT t1 in
let (vsvar,u) = conv_vs_let vsvar u t1.t_ty in
let f2 = fnF vsvar f2 in
f_let t1 (close u f2)
| _ -> f_map fnT (fnF vsvar) f
let decl (tenv:tenv) d =
......@@ -320,7 +319,7 @@ let decl (tenv:tenv) d =
let tvar = Htv.create 17 in
let f = fnF tvar Mvs.empty f in
let tvl = Htv.fold (fun _ tv acc -> tv::acc) tvar [] in
let f = f_forall tvl [] f in
let f = f_forall_close tvl [] f in
[create_decl (create_prop_decl k pr f)]
(*
......
......@@ -148,10 +148,11 @@ let rec rewrite_term tenv tvar vsvar t =
conv_res_app tenv tvar p tl t.t_ty
| Tif (f, t1, t2) ->
t_if (fnF f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) -> let u,t2 = t_open_bound b in
let (vsvar',u) = conv_vs_let tenv vsvar u in
let t1' = fnT vsvar t1 in let t2' = fnT vsvar' t2 in
if t_equal t1' t1 && t_equal t2' t2 then t else t_let u t1' t2'
| Tlet (t1, b) ->
let u,t2,close = t_open_bound_cb b in
let (vsvar',u) = conv_vs_let tenv vsvar u in
let t1 = fnT vsvar t1 in let t2 = fnT vsvar' t2 in
t_let t1 (close u t2)
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t
"Encoding decorate : I can't encode this term"
......@@ -171,22 +172,21 @@ and rewrite_fmla tenv tvar vsvar f =
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
f_app p tl
| Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
let (vsvar',vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1' = fnF vsvar' f1 in
| Fquant (q, b) ->
let vl, tl, f1, close = f_open_quant_cb b in
let (vsvar,vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut tre gnr *)
let tl = tr_map (rewrite_term tenv tvar vsvar') (fnF vsvar') tl in
(*if f_equal f1' f1 && vsvar' == vsvar (*&& tr_equal tl' tl*) then f
else *)
let vl = List.rev vl in
f_quant q vl tl f1'
| Flet (t1, b) -> let u,f2 = f_open_bound b in
let tl = tr_map (rewrite_term tenv tvar vsvar) (fnF vsvar) tl in
let vl = List.rev vl in
f_quant q (close vl tl f1)
| Flet (t1, b) ->
let u, f2, close = f_open_bound_cb b in
let (vsvar,u) = conv_vs_let tenv vsvar u in
let t1' = fnT t1 in let f2' = fnF vsvar f2 in
assert (u.vs_ty == t1'.t_ty);
(*if t_equal t1' t1 && f_equal f2' f2 then f else *)
f_let u t1' f2'
let t1 = fnT t1 in let f2 = fnF vsvar f2 in
assert (u.vs_ty == t1.t_ty);
f_let t1 (close u f2)
| _ -> f_map fnT (fnF vsvar) f
let is_kept ls = List.for_all (fun ty -> ty_equal ty_int ty) ls.ls_args
......@@ -239,7 +239,7 @@ Perhaps you could use eliminate_definition"
let t1 = t_app ls1 terms1 ty_int in
let t2 = t_app ls2 terms2 ty_int in
f_equ t1 t2 in
let fmla = f_forall vars [] fmla in
let fmla = f_forall_close vars [] fmla in
let name = create_prsymbol (id_clone ls1.ls_name) in
(create_prop_decl Paxiom name fmla)::d::acc
end else acc in
......@@ -255,7 +255,7 @@ Perhaps you could use eliminate_definition"
let tvar = Htv.create 17 in
let f = fnF tvar Mvs.empty f in
let tvl = Htv.fold (fun _ tv acc -> tv::acc) tvar [] in
let f = f_forall tvl [] f in
let f = f_forall_close tvl [] f in
[create_decl (create_prop_decl k pr f)]
(*
......
......@@ -58,8 +58,8 @@ let init_tenv kept =
let tt = t_var vt in
let u2t2u = t_app t2u [t_app u2t [tu] ty] ty_uni in
let t2u2t = t_app u2t [t_app t2u [tt] ty_uni] ty in
let u2t2u = f_forall [vu] [] (f_equ u2t2u tu) in
let t2u2t = f_forall [vt] [] (f_equ t2u2t tt) in
let u2t2u = f_forall_close [vu] [] (f_equ u2t2u tu) in
let t2u2t = f_forall_close [vt] [] (f_equ t2u2t tt) in
Hty.add specials ty { u2t = u2t ; t2u = t2u };
[ create_ty_decl [ts, Tabstract];
create_logic_decl [u2t, None];
......@@ -132,12 +132,11 @@ let rec rewrite_term tenv vm t =
| Tif (f, t1, t2) ->
t_if (fnF vm f) (fnT vm t1) (fnT vm t2)
| Tlet (t1, b) ->
let u,t2 = t_open_bound b in
let u,t2,close = t_open_bound_cb b in
let u' = conv_vs tenv u in
let t1' = fnT vm t1 in
let t2' = fnT (Mvs.add u (t_var u') vm) t2 in
if vs_equal u u' && t_equal t1 t1' && t_equal t2 t2'
then t else t_let u' t1' t2'
t_let t1' (close u' t2')
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t "unsupported term"
......@@ -153,20 +152,18 @@ and rewrite_fmla tenv vm f =
let tl = List.map2 fn ps.ls_args tl in
f_app ps tl
| Fquant (q,b) ->
let vl, tl, f1 = f_open_quant b in
let vl, tl, f1, close = f_open_quant_cb b in
let add m v = let v' = conv_vs tenv v in Mvs.add v (t_var v') m, v' in
let vm', vl' = Util.map_fold_left add vm vl in
let tl' = tr_map (fnT vm') (fnF vm') tl in
let f1' = fnF vm' f1 in
if List.for_all2 vs_equal vl vl' && tr_equal tl tl' && f_equal f1 f1'
then f else f_quant q vl' tl' f1'
f_quant q (close vl' tl' f1')
| Flet (t1, b) ->
let u,f1 = f_open_bound b in
let u,f1,close = f_open_bound_cb b in
let u' = conv_vs tenv u in
let t1' = fnT vm t1 in
let f1' = fnF (Mvs.add u (t_var u') vm) f1 in
if vs_equal u u' && t_equal t1 t1' && f_equal f1 f1'
then f else f_let u' t1' f1'
f_let t1' (close u' f1')