Commit 5a245c24 authored by MARCHE Claude's avatar MARCHE Claude

Put transformations "subst" and "subst_all" in a separate file

Incidentally, move the local "fold" function of apply.ml into the general
module Trans
parent 3a3014de
......@@ -199,7 +199,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
intro_vc_vars_counterexmp prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
prop_curry \
generic_arg_trans_utils case apply \
generic_arg_trans_utils case apply subst \
ind_itp destruct cut \
eliminate_literal induction induction_pr
......
......@@ -101,6 +101,13 @@ let fold fn v =
let fold_l fn v = fold (fun task -> Lists.apply (fn task)) [v]
let fold_decl fn v =
fold (fun task v ->
match task.task_decl.td_node with
| Decl d -> fn d v
| _ -> v)
v
let fold_map fn v t = conv_res snd (fold fn (v, t))
let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t))
(* we use List.map instead of List.map_rev to preserve the order *)
......
......@@ -52,6 +52,7 @@ val par : task trans list -> task tlist
(** {2 Iterating transformations} *)
val fold : (task_hd -> 'a -> 'a ) -> 'a -> 'a trans
val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
val fold_decl : (decl -> 'a -> 'a ) -> 'a -> 'a trans
val fold_map : (task_hd -> 'a * 'b -> ('a * 'b) ) -> 'a -> 'b -> 'b trans
val fold_map_l : (task_hd -> 'a * 'b -> ('a * 'b) list) -> 'a -> 'b -> 'b tlist
......
......@@ -19,7 +19,7 @@ open Reduction_engine
open Generic_arg_trans_utils
(** This file contains transformations with arguments that acts on specific
declarations to refine them (rewrite, replace, apply, unfold, subst...) *)
declarations to refine them (rewrite, replace, apply, unfold...) *)
let debug_matching = Debug.register_info_flag "print_match"
......@@ -181,12 +181,6 @@ let replace rev f1 f2 t =
| true -> replace_in_term f1 f2 t
| false -> replace_in_term f2 f1 t
(* Generic fold to be put in Trans ? TODO *)
let fold (f: decl -> 'a -> 'a) (acc: 'a): 'a Trans.trans =
Trans.fold (fun t acc -> match t.task_decl.td_node with
| Decl d -> f d acc
| _ -> acc) acc
(* - If f1 unifiable to t with substitution s then return s.f2 and replace every
occurences of s.f1 with s.f2 in the rest of the term
- Else call recursively on subterms of t *)
......@@ -234,7 +228,7 @@ let rewrite_in rev with_terms h h1 =
(* Used to find the equality we are rewriting on *)
(* TODO here should fold with a boolean stating if we found equality yet to
not go through all possible hypotheses *)
fold (fun d acc ->
Trans.fold_decl (fun d acc ->
match d.d_node with
| Dprop (Paxiom, pr, t) when Ident.id_equal pr.pr_name h.pr_name ->
let lp, lv, f = intros t in
......@@ -253,7 +247,7 @@ let rewrite_in rev with_terms h h1 =
match found_eq with
| None -> raise (Arg_error "rewrite")
| Some (lp, lv, t1, t2) ->
fold (fun d acc ->
Trans.fold_decl (fun d acc ->
match d.d_node with
| Dprop (p, pr, t)
when (Ident.id_equal pr.pr_name h1.pr_name &&
......@@ -376,312 +370,26 @@ let unfold unf hl =
end
| _ -> [d]) None
(* This found any equality which at one side contains a single lsymbol and is
local. It gives same output as found_eq. *)
let find_eq2 is_local_decl =
fold (fun d acc ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal && is_local_decl d ->
begin
let acc = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(match t1.t_node, t2.t_node with
| Tapp (_, []), _ ->
Some (Some pr, t1, t2)
| _, Tapp (_, []) ->
Some (Some pr, t2, t1)
| _ -> acc)
| _ -> acc) in
acc
end
| Dlogic [(ls, ld)] when is_local_decl d ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Some (None, t_app_infer ls [], e)
else
acc
| _ -> acc) None
let subst_eq found_eq =
match found_eq with
| None -> raise (Arg_trans "subst_eq")
| Some (Some pr_eq, t1, t2) ->
begin
Trans.decl (fun d ->
match d.d_node with
(* Remove equality over which we subst *)
| Dprop (_k, pr, _t) when pr_equal pr pr_eq ->
[]
(* Replace in all hypothesis *)
| Dprop (kind, pr, t) ->
[create_prop_decl kind pr (t_replace t1 t2 t)]
| Dlogic ldecl_list ->
let ldecl_list =
List.map (fun (ls, ls_def) ->
let (vl, t) = open_ls_defn ls_def in
make_ls_defn ls vl (t_replace t1 t2 t)) ldecl_list
in
[create_logic_decl ldecl_list]
(* TODO unbelievably complex for something that simple... *)
| Dind ((is: ind_sign), (ind_list: ind_decl list)) ->
let ind_list: ind_decl list =
List.map (fun ((ls: lsymbol), (idl: (prsymbol * term) list)) ->
let idl = List.map (fun (pr, t) -> (pr, t_replace t1 t2 t)) idl in
(ls, idl)) ind_list
in
[create_ind_decl is ind_list]
| Dtype _ | Ddata _ | Dparam _ -> [d]) None
end
| Some (None, t1, t2) ->
begin
Trans.decl (fun d ->
match d.d_node with
| Dlogic [(ls, _ld)] when try (t1 = Term.t_app_infer ls []) with _ -> false ->
[]
(* Replace in all hypothesis *)
| Dprop (kind, pr, t) ->
[create_prop_decl kind pr (t_replace t1 t2 t)]
| Dlogic ldecl_list ->
let ldecl_list =
List.map (fun (ls, ls_def) ->
let (vl, t) = open_ls_defn ls_def in
make_ls_defn ls vl (t_replace t1 t2 t)) ldecl_list
in
[create_logic_decl ldecl_list]
(* TODO unbelievably complex for something that simple... *)
| Dind ((is: ind_sign), (ind_list: ind_decl list)) ->
let ind_list: ind_decl list =
List.map (fun ((ls: lsymbol), (idl: (prsymbol * term) list)) ->
let idl = List.map (fun (pr, t) -> (pr, t_replace t1 t2 t)) idl in
(ls, idl)) ind_list
in
[create_ind_decl is ind_list]
| Dtype _ | Ddata _ | Dparam _ -> [d]) None
end
let subst_eq_list (found_eq_list, _) =
List.fold_left (fun acc_tr found_eq ->
Trans.compose (subst_eq found_eq) acc_tr) Trans.identity found_eq_list
let subst_all (is_local_decl: Decl.decl -> bool) =
Trans.bind (find_eq2 is_local_decl) subst_eq
let return_local_decl task =
let decl_list = get_local_task task in
let is_local_decl d = List.exists (fun x -> Decl.d_equal d x) decl_list in
is_local_decl
let return_local_decl = Trans.store return_local_decl
let subst_all = Trans.bind return_local_decl subst_all
let rec repeat f task =
try
let new_task = Trans.apply f task in
(* TODO this is probably expansive. Use a checksum or an integer ? *)
if Task.task_equal new_task task then
raise Exit
else
repeat f new_task
with
| _ -> task
let repeat f = Trans.store (repeat f)
let subst_all = repeat subst_all
(* TODO implement subst_all as repeat subst ??? *)
let () =
wrap_and_register ~desc:"substitute all ident equalities and remove them"
"subst_all"
(Ttrans) subst_all
let () = wrap_and_register ~desc:"sort declarations"
"sort"
(Ttrans) sort
"sort"
(Ttrans) sort
let () = wrap_and_register ~desc:"unfold ls [in] pr: unfold logic symbol ls in list of hypothesis pr. The argument in is optional: by default unfold in the goal." (* TODO *)
"unfold"
(Tlsymbol (Topt ("in", Tprlist Ttrans))) unfold
"unfold"
(Tlsymbol (Topt ("in", Tprlist Ttrans))) unfold
let () = wrap_and_register
~desc:"replace <term1> <term2> [in] <name list> replaces occcurences of term1 by term2 in prop name. If no list is given, replace in the goal."
"replace"
(Tterm (Tterm (Topt ("in", Tprlist Ttrans_l)))) replace
~desc:"replace <term1> <term2> [in] <name list> replaces occcurences of term1 by term2 in prop name. If no list is given, replace in the goal."
"replace"
(Tterm (Tterm (Topt ("in", Tprlist Ttrans_l)))) replace
let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> [with] <list term> rewrites equality defined in name into name2 using exactly all terms of the list as instance for what cannot be deduced directly" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol (Topt ("with", Ttermlist Ttrans_l))))))) (fun rev h h1opt term_list -> rewrite term_list rev h h1opt)
~desc:"rewrite [<-] <name> [in] <name2> [with] <list term> rewrites equality defined in name into name2 using exactly all terms of the list as instance for what cannot be deduced directly" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol (Topt ("with", Ttermlist Ttrans_l))))))) (fun rev h h1opt term_list -> rewrite term_list rev h h1opt)
let () = wrap_and_register
~desc:"apply <prop> [with] <list term> applies prop to the goal and \
uses the list of terms to instantiate the variables that are not found." "apply"
(Tprsymbol (Topt ("with", Ttermlist Ttrans_l))) (fun x y -> apply x y)
(*********)
(* Subst *)
(*********)
(* Creation of as structure that associates the replacement of terms as a
function of the
*)
type constant_subst_defining =
| Cls of lsymbol
| Cpr of prsymbol
module Csd = Stdlib.MakeMSHW (struct
type t = constant_subst_defining
let tag (c: t) = match c with
| Cls ls -> ls.ls_name.Ident.id_tag
| Cpr pr -> pr.pr_name.Ident.id_tag
end)
module Mcsd = Csd.M
(* We find the hypotheses that have a substitution equality for elements of the
to_subst list. We check that we never take more than one equality per
lsymbol to substitute.
*)
let find_eq_aux (to_subst: Term.lsymbol list) =
fold (fun d (acc, used) ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal ->
let acc, used = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Allow to rewrite from the right *)
begin
match t1.t_node, t2.t_node with
| Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
Mcsd.add (Cpr pr) (t1, t2) acc, ls :: used
| _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
Mcsd.add (Cpr pr) (t2, t1) acc, ls :: used
| _ -> acc, used
end
| _ -> acc, used) in
acc, used
| Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Mcsd.add (Cls ls) (t_app_infer ls [], e) acc, ls :: used
else
acc, used
| _ -> acc, used) (Mcsd.empty,[])
(* Wrap-around function to parse lsymbol instead of terms *)
let find_eq to_subst =
let to_subst = (List.map
(fun t -> match t.t_node with
| Tapp (ls, []) -> ls
| _ -> raise (Arg_trans "subst_eq")) to_subst)
in
find_eq_aux to_subst
(* This produce an ordered list of tdecl which is the original task minus the
hypotheses/constants that were identified for substitution.
This shall be done on tdecl.
*)
let remove_hyp_and_constants (replacing_hyps, used_ls) =
(* The task_fold on tdecl is necessary as we *need* all the tdecl (in
particular to identify local decls).
*)
Task.task_fold (fun (subst, list_tdecl) td ->
match td.td_node with
| Decl d ->
begin
match d.d_node with
| Dprop (kind, pr, _t) when kind != Pgoal &&
Mcsd.mem (Cpr pr) replacing_hyps ->
let from_t, to_t = Mcsd.find (Cpr pr) replacing_hyps in
(* TODO find a way to be more efficient than this *)
let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
Mterm.add from_t to_t subst, list_tdecl
| Dlogic [ls, _] when Mcsd.mem (Cls ls) replacing_hyps ->
let from_t, to_t = Mcsd.find (Cls ls) replacing_hyps in
(* TODO find a way to be more efficient than this *)
let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
Mterm.add from_t to_t subst, list_tdecl
| Dparam ls when List.exists (ls_equal ls) used_ls ->
subst, list_tdecl
| _ ->
subst, (replace_tdecl subst td :: list_tdecl)
end
| _ -> (subst, td :: list_tdecl)
) (Mterm.empty, [])
let remove_hyp_and_constants (replacing_hyps, used_ls) =
Trans.store (remove_hyp_and_constants (replacing_hyps, used_ls))
let is_goal td =
match td.td_node with
| Decl d ->
begin
match d.d_node with
| Dprop (Pgoal, _, _) -> true
| _ -> false
end
| _ -> false
(* Use the list of tdecl that should be able to be readded into a task if there
was sufficiently few things that were removed to the task.
To do this, we use Task.add_tdecl (because we think its the safest).
Note that we also try to keep the order of the declarations (because
usability). So, each time we add a new declaration, we try to add all the
transformations that failed (supposedly because they use a variable declared
after it).
*)
let readd_decls (list_decls, subst: tdecl list * _) =
List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
let d = replace_tdecl subst d in
let task_uc, list_to_add =
List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
try
let new_task_uc = Task.add_tdecl task_uc d in
new_task_uc, list_to_add
with
(* TODO find all possible exceptions here *)
_ -> task_uc, d :: list_to_add)
(task_uc, []) list_to_add
in
(* We always need to add the goal last *)
if is_goal d then
if list_to_add != [] then
raise (Arg_trans_decl ("subst_eq", list_to_add))
else
try
(Task.add_tdecl task_uc d, [])
with
(* TODO find all possible exceptions here *)
_ -> raise (Arg_trans_decl ("subst_eq", [d]))
else
try
(Task.add_tdecl task_uc d, List.rev list_to_add)
with
_ -> (task_uc, List.rev (d :: list_to_add)))
(None, []) list_decls
let readd_decls (subst, list_decls) =
let (task, _l) = readd_decls (list_decls, subst) in
Trans.return task
let find args = Trans.bind (find_eq args) remove_hyp_and_constants
let subst args = Trans.bind (find args) readd_decls
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Ttermlist Ttrans) subst
~desc:"apply <prop> [with] <list term> applies prop to the goal and \
uses the list of terms to instantiate the variables that are not found." "apply"
(Tprsymbol (Topt ("with", Ttermlist Ttrans_l))) (fun x y -> apply x y)
......@@ -117,7 +117,7 @@ let destruct_alg replace (x: term) : Task.task Trans.tlist =
| _ -> [[d]]) None
in
if replace && is_lsymbol x then
Trans.compose_l trans (Trans.singleton (Apply.subst [x]))
Trans.compose_l trans (Trans.singleton (Subst.subst [x]))
else
trans
end
......
(********************************************************************)
(* *)
(* 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. *)
(* *)
(********************************************************************)
open Term
open Decl
open Theory
open Generic_arg_trans_utils
open Args_wrapper
(* transformations "subst" and "subst_all" *)
(* This found any equality which at one side contains a single lsymbol and is
local. It gives same output as found_eq. *)
let find_eq2 is_local_decl =
Trans.fold_decl (fun d acc ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal && is_local_decl d ->
begin
let acc = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(match t1.t_node, t2.t_node with
| Tapp (_, []), _ ->
Some (Some pr, t1, t2)
| _, Tapp (_, []) ->
Some (Some pr, t2, t1)
| _ -> acc)
| _ -> acc) in
acc
end
| Dlogic [(ls, ld)] when is_local_decl d ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Some (None, t_app_infer ls [], e)
else
acc
| _ -> acc) None
let subst_eq found_eq =
match found_eq with
| None -> raise (Arg_trans "subst_eq")
| Some (Some pr_eq, t1, t2) ->
begin
Trans.decl (fun d ->
match d.d_node with
(* Remove equality over which we subst *)
| Dprop (_k, pr, _t) when pr_equal pr pr_eq ->
[]
(* Replace in all hypothesis *)
| Dprop (kind, pr, t) ->
[create_prop_decl kind pr (t_replace t1 t2 t)]
| Dlogic ldecl_list ->
let ldecl_list =
List.map (fun (ls, ls_def) ->
let (vl, t) = open_ls_defn ls_def in
make_ls_defn ls vl (t_replace t1 t2 t)) ldecl_list
in
[create_logic_decl ldecl_list]
(* TODO unbelievably complex for something that simple... *)
| Dind ((is: ind_sign), (ind_list: ind_decl list)) ->
let ind_list: ind_decl list =
List.map (fun ((ls: lsymbol), (idl: (prsymbol * term) list)) ->
let idl = List.map (fun (pr, t) -> (pr, t_replace t1 t2 t)) idl in
(ls, idl)) ind_list
in
[create_ind_decl is ind_list]
| Dtype _ | Ddata _ | Dparam _ -> [d]) None
end
| Some (None, t1, t2) ->
begin
Trans.decl (fun d ->
match d.d_node with
| Dlogic [(ls, _ld)] when try (t1 = Term.t_app_infer ls []) with _ -> false ->
[]
(* Replace in all hypothesis *)
| Dprop (kind, pr, t) ->
[create_prop_decl kind pr (t_replace t1 t2 t)]
| Dlogic ldecl_list ->
let ldecl_list =
List.map (fun (ls, ls_def) ->
let (vl, t) = open_ls_defn ls_def in
make_ls_defn ls vl (t_replace t1 t2 t)) ldecl_list
in
[create_logic_decl ldecl_list]
(* TODO unbelievably complex for something that simple... *)
| Dind ((is: ind_sign), (ind_list: ind_decl list)) ->
let ind_list: ind_decl list =
List.map (fun ((ls: lsymbol), (idl: (prsymbol * term) list)) ->
let idl = List.map (fun (pr, t) -> (pr, t_replace t1 t2 t)) idl in
(ls, idl)) ind_list
in
[create_ind_decl is ind_list]
| Dtype _ | Ddata _ | Dparam _ -> [d]) None
end
let subst_eq_list (found_eq_list, _) =
List.fold_left (fun acc_tr found_eq ->
Trans.compose (subst_eq found_eq) acc_tr) Trans.identity found_eq_list
let subst_all (is_local_decl: Decl.decl -> bool) =
Trans.bind (find_eq2 is_local_decl) subst_eq
let return_local_decl task =
let decl_list = get_local_task task in
let is_local_decl d = List.exists (fun x -> Decl.d_equal d x) decl_list in
is_local_decl
let return_local_decl = Trans.store return_local_decl
let subst_all = Trans.bind return_local_decl subst_all
let rec repeat f task =
try
let new_task = Trans.apply f task in
(* TODO this is probably expansive. Use a checksum or an integer ? *)
if Task.task_equal new_task task then
raise Exit
else
repeat f new_task
with
| _ -> task
let repeat f = Trans.store (repeat f)
let subst_all = repeat subst_all
(* TODO implement subst_all as repeat subst ??? *)
let () =
wrap_and_register ~desc:"substitute all ident equalities and remove them"
"subst_all"
(Ttrans) subst_all
(*********)
(* Subst *)
(*********)
(* Creation of as structure that associates the replacement of terms as a
function of the
*)
type constant_subst_defining =
| Cls of lsymbol
| Cpr of prsymbol
module Csd = Stdlib.MakeMSHW (struct
type t = constant_subst_defining
let tag (c: t) = match c with
| Cls ls -> ls.ls_name.Ident.id_tag
| Cpr pr -> pr.pr_name.Ident.id_tag
end)
module Mcsd = Csd.M
(* We find the hypotheses that have a substitution equality for elements of the
to_subst list. We check that we never take more than one equality per
lsymbol to substitute.
*)
let find_eq_aux (to_subst: Term.lsymbol list) =
Trans.fold_decl (fun d (acc, used) ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal ->
let acc, used = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Allow to rewrite from the right *)
begin
match t1.t_node, t2.t_node with
| Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
Mcsd.add (Cpr pr) (t1, t2) acc, ls :: used
| _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
Mcsd.add (Cpr pr) (t2, t1) acc, ls :: used
| _ -> acc, used
end
| _ -> acc, used) in
acc, used
| Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Mcsd.add (Cls ls) (t_app_infer ls [], e) acc, ls :: used
else
acc, used
| _ -> acc, used) (Mcsd.empty,[])
(* Wrap-around function to parse lsymbol instead of terms *)
let find_eq to_subst =
let to_subst = (List.map
(fun t -> match t.t_node with
| Tapp (ls, []) -> ls
| _ -> raise (Arg_trans "subst_eq")) to_subst)
in
find_eq_aux to_subst
(* This produce an ordered list of tdecl which is the original task minus the
hypotheses/constants that were identified for substitution.
This shall be done on tdecl.
*)
let remove_hyp_and_constants (replacing_hyps, used_ls) =
(* The task_fold on tdecl is necessary as we *need* all the tdecl (in
particular to identify local decls).
*)
Task.task_fold (fun (subst, list_tdecl) td ->
match td.td_node with
| Decl d ->
begin
match d.d_node with
| Dprop (kind, pr, _t) when kind != Pgoal &&
Mcsd.mem (Cpr pr) replacing_hyps ->
let from_t, to_t = Mcsd.find (Cpr pr) replacing_hyps in
(* TODO find a way to be more efficient than this *)
let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
Mterm.add from_t to_t subst, list_tdecl
| Dlogic [ls, _] when Mcsd.mem (Cls ls) replacing_hyps ->
let from_t, to_t = Mcsd.find (Cls ls) replacing_hyps in
(* TODO find a way to be more efficient than this *)
let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
Mterm.add from_t to_t subst, list_tdecl
| Dparam ls when List.exists (ls_equal ls) used_ls ->
subst, list_tdecl
| _ ->
subst, (replace_tdecl subst td :: list_tdecl)
end
| _ -> (subst, td :: list_tdecl)
) (Mterm.empty, [])
let remove_hyp_and_constants (replacing_hyps, used_ls) =
Trans.store (remove_hyp_and_constants (replacing_hyps, used_ls))
let is_goal td =
match td.td_node with
| Decl d ->
begin
match d.d_node with
| Dprop (Pgoal, _, _) -> true
| _ -> false
end
| _ -> false
(* Use the list of tdecl that should be able to be readded into a task if there
was sufficiently few things that were removed to the task.
To do this, we use Task.add_tdecl (because we think its the safest).
Note that we also try to keep the order of the declarations (because
usability). So, each time we add a new declaration, we try to add all the
transformations that failed (supposedly because they use a variable declared
after it).
*)
let readd_decls (list_decls, subst: tdecl list * _) =
List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
let d = replace_tdecl subst d in
let task_uc, list_to_add =
List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
try
let new_task_uc = Task.add_tdecl task_uc d in
new_task_uc, list_to_add
with
(* TODO find all possible exceptions here *)
_ -> task_uc, d :: list_to_add)
(task_uc, []) list_to_add
in
(* We always need to add the goal last *)
if is_goal d then
if list_to_add != [] then
raise (Arg_trans_decl ("subst_eq", list_to_add))
else
try
(Task.add_tdecl task_uc d, [])
with
(* TODO find all possible exceptions here *)
_ -> raise (Arg_trans_decl ("subst_eq", [d]))
else
try
(Task.add_tdecl task_uc d, List.rev list_to_add)
with
_ -> (task_uc, List.rev (d :: list_to_add)))
(None, []) list_decls
let readd_decls (subst, list_decls) =
let (task, _l) = readd_decls (list_decls, subst) in
Trans.return task
let find args = Trans.bind (find_eq args) remove_hyp_and_constants
let subst args = Trans.bind (find args) readd_decls
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Ttermlist Ttrans) subst