Commit f542a3e4 authored by Andrei Paskevich's avatar Andrei Paskevich

Subst: avoid selecting polymorphic symbols and constructors

Also, add an .mli file and export the relevant functions.

Also, provide a variant of "split_vc" in introduction.ml
which uses subst over introduced non-model constants instead
of "simplify_trivial_quantification". This is more efficient
and produces better results. Commented at the moment because
of session breakage.
parent 6ea5648e
......@@ -213,20 +213,19 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
args_wrapper detect_polymorphism reduction_engine compute \
eliminate_definition eliminate_algebraic \
abstract_quantifiers eliminate_unknown_types \
eliminate_unknown_lsymbols \
eliminate_symbol \
eliminate_unknown_lsymbols eliminate_symbol \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate encoding encoding_select \
encoding_guards_full encoding_tags_full \
encoding_guards encoding_tags encoding_twin \
encoding_sort simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
abstraction close_epsilon lift_epsilon \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \
prop_curry eliminate_literal \
generic_arg_trans_utils case apply subst \
ind_itp destruct cut \
introduction ind_itp destruct cut \
induction induction_pr matching reflection
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
......
......@@ -282,6 +282,16 @@ let simplify_intros =
Trans.compose Simplify_formula.simplify_trivial_wp_quantification
introduce_premises
(*
let subst_filter ls =
Sattr.mem intro_attr ls.ls_name.id_attrs &&
not (Ident.has_a_model_attr ls.ls_name)
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered subst_filter)
*)
let split_vc =
Trans.compose_l
(Trans.compose generalize_intro Split_goal.split_goal_right)
......
......@@ -162,7 +162,6 @@ let rec occurs_in_term ls t =
| Tapp(ls',[]) when ls_equal ls' ls -> true
| _ -> t_any (occurs_in_term ls) t
(* [find_equalities filter t] searches in task [t] for equalities of
the form constant = term or term = constant, where constant does
not occur in the term. That function returns first the set of
......@@ -176,6 +175,18 @@ let rec occurs_in_term ls t =
constant, the first one is considered.
*)
let find_equalities filter =
let valid ls =
ls.ls_args = [] && ls.ls_constr = 0 && ls.ls_value <> None &&
List.for_all Ty.ty_closed (Ty.oty_cons ls.ls_args ls.ls_value) &&
filter ls
in
let select ls t sigma =
let () = Debug.dprintf debug_subst "selected: %a -> %a@."
Pretty.print_ls ls Pretty.print_term t in
let sigma' = Mls.add ls t Mls.empty in
let sigma = Mls.map (subst_in_term sigma') sigma in
Mls.add ls t sigma
in
Trans.fold_decl
(fun d ((prs,sigma) as acc) ->
match d.d_node with
......@@ -187,30 +198,20 @@ let find_equalities filter =
begin
try match t1.t_node with
| Tapp (ls, []) when
filter ls &&
valid ls &&
not (Mls.mem ls sigma) ->
let t2' = subst_in_term sigma t2 in
if occurs_in_term ls t2' then raise Exit
else
let () = Debug.dprintf debug_subst "selected: %a -> %a@."
Pretty.print_ls ls Pretty.print_term t2' in
let sigma' = Mls.add ls t2' Mls.empty in
let sigma = Mls.map (subst_in_term sigma') sigma in
(Spr.add pr prs, Mls.add ls t2' sigma)
else (Spr.add pr prs, select ls t2' sigma)
| _ -> raise Exit
with Exit ->
match t2.t_node with
| Tapp (ls, []) when
filter ls &&
valid ls &&
not (Mls.mem ls sigma) ->
let t1' = subst_in_term sigma t1 in
if occurs_in_term ls t1' then acc
else
let () = Debug.dprintf debug_subst "selected: %a -> %a@."
Pretty.print_ls ls Pretty.print_term t1' in
let sigma' = Mls.add ls t1' Mls.empty in
let sigma = Mls.map (subst_in_term sigma') sigma in
(Spr.add pr prs, Mls.add ls t1' sigma)
else (Spr.add pr prs, select ls t1' sigma)
| _ -> acc
end
| _ -> acc
......@@ -218,12 +219,11 @@ let find_equalities filter =
| Dlogic ld ->
List.fold_left
(fun ((prs,sigma) as acc) (ls,ld) ->
if filter ls then
let vl, t = open_ls_defn ld in
if vl = [] && not (occurs_in_term ls t) then
let t = subst_in_term sigma t in
(prs, Mls.add ls t sigma)
else acc
if valid ls && not (Mls.mem ls sigma) then
let _, t = open_ls_defn ld in
let t' = subst_in_term sigma t in
if occurs_in_term ls t' then acc
else (prs, select ls t' sigma)
else acc)
acc
ld
......@@ -236,10 +236,12 @@ let get_decls =
let apply_subst x t =
apply_subst x (List.rev (Trans.apply get_decls t))
let subst_all =
Trans.bind (find_equalities (fun _ -> true))
let subst_filtered filter =
Trans.bind (find_equalities filter)
(fun x -> Trans.store (apply_subst x))
let subst_all = subst_filtered (fun _ -> true)
let () =
wrap_and_register ~desc:"substitutes with all equalities between a constant and a term"
"subst_all"
......@@ -253,8 +255,7 @@ let subst tl =
| Tapp (ls, []) -> Sls.add ls acc
| _ -> raise (Arg_trans "subst: %a is not a constant")) Sls.empty tl
in
Trans.bind (find_equalities (fun ls -> Sls.mem ls to_subst))
(fun x -> Trans.store (apply_subst x))
subst_filtered (fun ls -> Sls.mem ls to_subst)
let () =
wrap_and_register ~desc:"substitutes with all equalities involving one of the given constants"
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val subst_filtered : (Term.lsymbol -> bool) -> Task.task Trans.trans
val subst : Term.term list -> Task.task Trans.trans
val subst_all : Task.task Trans.trans
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