aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/Setoid.tex177
-rw-r--r--doc/refman/biblio.bib7
-rw-r--r--proofs/clenv.ml10
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--tactics/autorewrite.ml20
-rw-r--r--tactics/autorewrite.mli4
-rw-r--r--tactics/extratactics.ml48
-rw-r--r--tactics/rewrite.ml451
9 files changed, 217 insertions, 64 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index c0913135c..8a293ea2b 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -1,15 +1,16 @@
\newtheorem{cscexample}{Example}
-\achapter{\protect{User defined equalities and relations}}
+\achapter{\protect{Generalized rewriting}}
\aauthor{Matthieu Sozeau}
-\tacindex{setoid\_replace}
\label{setoid_replace}
-This chapter presents the extension of several equality related tactics to
-work over user-defined structures (called setoids) that are equipped with
-ad-hoc equivalence relations meant to behave as equalities.
-Actually, the tactics have also been generalized to relations weaker then
-equivalences (e.g. rewriting systems).
+This chapter presents the extension of several equality related tactics
+to work over user-defined structures (called setoids) that are equipped
+with ad-hoc equivalence relations meant to behave as equalities.
+Actually, the tactics have also been generalized to relations weaker
+then equivalences (e.g. rewriting systems). The toolbox also extends the
+automatic rewriting capabilities of the system, allowing to specify
+custom strategies for rewriting.
This documentation is adapted from the previous setoid documentation by
Claudio Sacerdoti Coen (based on previous work by Cl\'ement Renard).
@@ -43,7 +44,9 @@ the previous implementation in several ways:
user to customize the proof-search if necessary.
\end{itemize}
-\asection{Relations and morphisms}
+\asection{Introduction to generalized rewriting}
+
+\subsection{Relations and morphisms}
A parametric \emph{relation} \texttt{R} is any term of type
\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), relation $A$}. The
@@ -162,7 +165,7 @@ will fail replacing the third occurrence of \texttt{S2} unless \texttt{f}
has also been declared as a morphism.
\end{cscexample}
-\asection{Adding new relations and morphisms}
+\subsection{Adding new relations and morphisms}
A parametric relation
\textit{Aeq}\texttt{: forall ($y_1 : \beta_!$ \ldots $y_m : \beta_m$), relation (A $t_1$ \ldots $t_n$)} over
\textit{(A : $\alpha_i$ -> \ldots $\alpha_n$ -> }\texttt{Type})
@@ -329,7 +332,7 @@ declaration (see \S\ref{setoid:first-class}) at definition time.
When loading a compiled file or importing a module,
all the declarations of this module will be loaded.
-\asection{Rewriting and non reflexive relations}
+\subsection{Rewriting and non reflexive relations}
To replace only one argument of an n-ary morphism it is necessary to prove
that all the other arguments are related to themselves by the respective
relation instances.
@@ -360,7 +363,7 @@ non zero elements). Division can be declared as a morphism of signature
is equivalent to \texttt{n=n $\land$ n$\neq$0}.
\end{cscexample}
-\asection{Rewriting and non symmetric relations}
+\subsection{Rewriting and non symmetric relations}
When the user works up to relations that are not symmetric, it is no longer
the case that any covariant morphism argument is also contravariant. As a
result it is no longer possible to replace a term with a related one in
@@ -408,7 +411,7 @@ is contravariant in its second argument), and finally covariantly in
is contravariant in its first argument with respect to the relation itself).
\end{cscexample}
-\asection{Rewriting in ambiguous setoid contexts}
+\subsection{Rewriting in ambiguous setoid contexts}
One function can respect several different relations and thus it can be
declared as a morphism having multiple signatures.
@@ -431,7 +434,8 @@ tactic will always choose the first possible solution to the set of
constraints generated by a rewrite and will not try to find \emph{all}
possible solutions to warn the user about.
-\asection{First class setoids and morphisms}
+\asection{Commands and tactics}
+\subsection{First class setoids and morphisms}
\label{setoid:first-class}
The implementation is based on a first-class representation of
@@ -507,7 +511,7 @@ Proof. intros. rewrite H. reflexivity. Qed.
\end{coq_example*}
\end{cscexample}
-\asection{Tactics enabled on user provided relations}
+\subsection{Tactics enabled on user provided relations}
\label{setoidtactics}
The following tactics, all prefixed by \texttt{setoid\_},
deal with arbitrary
@@ -519,20 +523,20 @@ the prefixed tactics it is possible to pass additional arguments such as
\texttt{using relation}.
\medskip
-\comindex{setoid\_reflexivity}
+\tacindex{setoid\_reflexivity}
\texttt{setoid\_reflexivity}
-\comindex{setoid\_symmetry}
+\tacindex{setoid\_symmetry}
\texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}}
-\comindex{setoid\_transitivity}
+\tacindex{setoid\_transitivity}
\texttt{setoid\_transitivity}
-\comindex{setoid\_rewrite}
+\tacindex{setoid\_rewrite}
\texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}}
-\comindex{setoid\_replace}
+\tacindex{setoid\_replace}
\texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
~\zeroone{\texttt{in} \textit{ident}}
~\zeroone{\texttt{using relation} \textit{term}}
@@ -557,7 +561,7 @@ not proof of Leibniz equalities. In particular it is possible to exploit
\texttt{autorewrite} to simulate normalization in a term rewriting system
up to user defined equalities.
-\asection{Printing relations and morphisms}
+\subsection{Printing relations and morphisms}
The \texttt{Print Instances} command can be used to show the list of
currently registered \texttt{Reflexive} (using \texttt{Print Instances Reflexive}),
\texttt{Symmetric} or \texttt{Transitive} relations,
@@ -568,7 +572,7 @@ because the latter is not a composition of morphisms, the \texttt{Print Instance
commands can be useful to understand what additional morphisms should be
registered.
-\asection{Deprecated syntax and backward incompatibilities}
+\subsection{Deprecated syntax and backward incompatibilities}
Due to backward compatibility reasons, the following syntax for the
declaration of setoids and morphisms is also accepted.
@@ -607,7 +611,8 @@ contexts that were refused by the old implementation. As discussed in
the next section, the semantics of the new \texttt{setoid\_rewrite}
command differs slightly from the old one and \texttt{rewrite}.
-\asection{Rewriting under binders}
+\asection{Extensions}
+\subsection{Rewriting under binders}
\textbf{Warning}: Due to compatibility issues, this feature is enabled only when calling
the \texttt{setoid\_rewrite} tactics directly and not \texttt{rewrite}.
@@ -678,7 +683,7 @@ and in its local environment, and all matches are rewritten
\texttt{setoid\_rewrite} implementation can almost be recovered using
the \texttt{at 1} modifier.
-\asection{Sub-relations}
+\subsection{Sub-relations}
Sub-relations can be used to specify that one relation is included in
another, so that morphisms signatures for one can be used for the other.
@@ -698,14 +703,136 @@ any rewriting constraints arising from a rewrite using \texttt{iff},
Sub-relations are implemented in \texttt{Classes.Morphisms} and are a
prime example of a mostly user-space extension of the algorithm.
-\asection{Constant unfolding}
+\subsection{Constant unfolding}
The resolution tactic is based on type classes and hence regards user-defined
constants as transparent by default. This may slow down the resolution
due to a lot of unifications (all the declared \texttt{Proper}
instances are tried at each node of the search tree).
To speed it up, declare your constant as rigid for proof search
-using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparency}).
+using the command \texttt{Typeclasses Opaque} (see \S
+\ref{TypeclassesTransparency}).
+
+\asection{Strategies for rewriting}
+
+\subsection{Definitions}
+The generalized rewriting tactic is based on a set of strategies that
+can be combined to obtain custom rewriting procedures. Its set of
+strategies is based on Elan's rewriting strategies
+\cite{Luttik97specificationof}. Rewriting strategies are applied using
+the tactic $\texttt{rewrite\_strat}~s$ where $s$ is a strategy
+expression. Strategies are defined inductively as described by the
+following grammar:
+
+\def\str#1{\texttt{#1}}
+
+\def\strline#1#2{& \vert & #1 & \text{#2}}
+\def\strlinea#1#2#3{& \vert & \str{#1}~#2 & \text{#3}}
+
+\[\begin{array}{lcll}
+ s, t, u & ::= & ( s ) & \text{strategy} \\
+ \strline{c}{lemma} \\
+ \strline{\str{<-}~c}{lemma, right-to-left} \\
+
+ \strline{\str{fail}}{failure} \\
+ \strline{\str{id}}{identity} \\
+ \strline{\str{refl}}{reflexivity} \\
+ \strlinea{progress}{s}{progress} \\
+ \strlinea{try}{s}{failure catch} \\
+
+ \strline{s~\str{;}~u}{composition} \\
+ \strline{\str{choice}~s~t}{left-biased choice} \\
+
+ \strlinea{repeat}{s}{iteration (+)} \\
+ \strlinea{any}{s}{iteration (*)} \\
+
+ \strlinea{subterm}{s}{one subterm} \\
+ \strlinea{subterms}{s}{all subterms} \\
+ \strlinea{innermost}{s}{innermost first} \\
+ \strlinea{outermost}{s}{outermost first}\\
+ \strlinea{bottomup}{s}{bottom-up} \\
+ \strlinea{topdown}{s}{top-down} \\
+
+ \strlinea{hints}{hintdb}{apply hint} \\
+ \strlinea{terms}{c \ldots c}{any of the terms}\\
+ \strlinea{eval}{redexpr}{apply reduction}\\
+ \strlinea{fold}{c}{fold expression}
+\end{array}\]
+
+Actually a few of these are defined in term of the others using
+a primitive fixpoint operator:
+
+\[\begin{array}{lcl}
+ \str{try}~s & = & \str{choice}~s~\str{id} \\
+ \str{any}~s & = & \str{fix}~u. \str{try}~(s~\str{;}~u) \\
+ \str{repeat}~s & = & s~\str{;}~\str{any}~s \\
+ \str{bottomup}~s & = &
+ \str{fix}~bu. (\str{choice}~(\str{progress}~(\str{subterms}~bu))~s)~\str{;}~\str{try}~bu \\
+ \str{topdown}~s & = &
+ \str{fix}~td. (\str{choice}~s~(\str{progress}~(\str{subterms}~td)))~\str{;}~\str{try}~td \\
+ \str{innermost}~s & = & \str{fix}~i. (\str{choice}~(\str{subterm}~i)~s) \\
+ \str{outermost}~s & = &
+ \str{fix}~o. (\str{choice}~s~(\str{subterm}~o))
+\end{array}\]
+
+The basic control strategy semantics are straightforward: strategies are
+applied to subterms of the term to rewrite, starting from the root of
+the term. The lemma strategies unify the left-hand-side of the
+lemma with the current subterm and on success rewrite it to the
+right-hand-side. Composition can be used to continue rewriting on the
+current subterm. The fail strategy always fails while the identity
+strategy succeeds without making progress. The reflexivity strategy
+succeeds, making progress using a reflexivity proof of
+rewriting. Progress tests progress of the argument strategy and fails if
+no progress was made, while \str{try} always succeeds, catching
+failures. Choice is left-biased: it will launch the first strategy and
+fall back on the second one in case of failure. One can iterate a
+strategy at least 1 time using \str{repeat} and at least 0 times using
+\str{any}.
+
+The \str{subterm} and \str{subterms} strategies apply their argument
+strategy $s$ to respectively one or all subterms of the current term
+under consideration, left-to-right. \str{subterm} stops at the first
+subterm for which $s$ made progress. The composite strategies
+\str{innermost} and \str{outermost} perform a single innermost our outermost
+rewrite using their argument strategy. Their counterparts
+\str{bottomup} and \str{topdown} perform as many rewritings as possible,
+starting from the bottom or the top of the term.
+
+Hint databases created for \texttt{autorewrite} can also be used by
+\texttt{rewrite\_strat} using the \str{hints} strategy that applies any
+of the lemmas at the current subterm. The \str{terms} strategy takes the
+lemma names directly as arguments. The \str{eval} strategy expects a
+reduction expression (see \S\ref{Conversion-tactics}) and succeeds if it
+reduces the subterm under consideration. The \str{fold} strategy takes a
+term $c$ and tries to \emph{unify} it to the current subterm, converting
+it to $c$ on success, it is stronger than the tactic \texttt{fold}.
+
+
+\subsection{Usage}
+\tacindex{rewrite\_strat}
+
+\texttt{rewrite\_strat}~\textit{s}~\zeroone{\texttt{in} \textit{ident}}:
+
+ Rewrite using the strategy \textit{s} in hypothesis \textit{ident}
+ or the conclusion.
+
+ \begin{ErrMsgs}
+ \item \errindex{Nothing to rewrite}. If the strategy failed.
+ \item \errindex{No progress made}. If the strategy succeeded but
+ made no progress.
+ \item \errindex{Unable to satisfy the rewriting constraints}.
+ If the strategy succeeded and made progress but the corresponding
+ rewriting constraints are not satisfied.
+ \end{ErrMsgs}
+
+
+The \texttt{setoid\_rewrite}~c tactic is basically equivalent to
+\texttt{rewrite\_strat}~(\str{outermost}~c).
+
+
+
+
%%% Local Variables:
%%% mode: latex
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 192a96998..3715c4c79 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -786,6 +786,13 @@ of the {ML} language},
year = {1990}
}
+@inproceedings{Luttik97specificationof,
+ Author = {Sebastiaan P. Luttik and Eelco Visser},
+ Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
+ Publisher = {Springer-Verlag},
+ Title = {Specification of Rewriting Strategies},
+ Year = {1997}}
+
@Book{MaL84,
author = {{P. Martin-L\"of}},
publisher = {Bibliopolis},
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index bc6da8c34..3f3b40bed 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -308,19 +308,19 @@ let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
*)
let clenv_pose_metas_as_evars clenv dep_mvs =
- let rec fold clenv = function
- | [] -> clenv
+ let rec fold clenv l = function
+ | [] -> clenv, l
| mv::mvs ->
let ty = clenv_meta_type clenv mv in
(* Postpone the evar-ization if dependent on another meta *)
(* This assumes no cycle in the dependencies - is it correct ? *)
- if occur_meta ty then fold clenv (mvs@[mv])
+ if occur_meta ty then fold clenv l (mvs@[mv])
else
let (evd,evar) =
new_evar clenv.evd (cl_env clenv) ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in
let clenv = clenv_assign mv evar {clenv with evd=evd} in
- fold clenv mvs in
- fold clenv dep_mvs
+ fold clenv (destEvar evar::l) mvs in
+ fold clenv [] dep_mvs
let evar_clenv_unique_resolver = clenv_unique_resolver
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index bfb5ee27c..f80bff396 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -73,7 +73,7 @@ val evar_clenv_unique_resolver :
val clenv_dependent : clausenv -> metavariable list
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * existential list
(** {6 Bindings } *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 389075c9a..23a835ede 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -55,7 +55,7 @@ let clenv_pose_dependent_evars with_evars clenv =
if not (List.is_empty dep_mvs) && not with_evars then
raise
(RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
- clenv_pose_metas_as_evars clenv dep_mvs
+ fst (clenv_pose_metas_as_evars clenv dep_mvs)
let clenv_refine with_evars ?(with_classes=true) clenv gls =
let clenv = clenv_pose_dependent_evars with_evars clenv in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 39e0c653c..4ebe089e9 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -25,13 +25,13 @@ type rew_rule = { rew_lemma: constr;
rew_type: types;
rew_pat: constr;
rew_l2r: bool;
- rew_tac: glob_tactic_expr }
+ rew_tac: glob_tactic_expr option }
let subst_hint subst hint =
let cst' = subst_mps subst hint.rew_lemma in
let typ' = subst_mps subst hint.rew_type in
let pat' = subst_mps subst hint.rew_pat in
- let t' = Tacsubst.subst_tactic subst hint.rew_tac in
+ let t' = Option.smartmap (Tacsubst.subst_tactic subst) hint.rew_tac in
if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
{ hint with
rew_lemma = cst'; rew_type = typ';
@@ -82,16 +82,18 @@ let print_rewrite_hintdb bas =
(fun h ->
str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
- str " then use tactic " ++
- Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
+ Option.cata (fun tac -> str " then use tactic " ++
+ Pptactic.pr_glob_tactic (Global.env()) tac) (mt ()) h.rew_tac)
(find_rewrites bas))
-type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr
+type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr option
(* Applies all the rules of one base *)
let one_base general_rewrite_maybe_in tac_main bas =
let lrul = find_rewrites bas in
- let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in
+ let lrul = List.map (fun h ->
+ let tac = match h.rew_tac with None -> tclIDTAC | Some t -> Tacinterp.eval_tactic t in
+ (h.rew_lemma,h.rew_l2r,tac)) lrul in
tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
tclTHEN tac
(tclREPEAT_MAIN
@@ -104,7 +106,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
(List.fold_left (fun tac bas ->
tclTHEN tac
(one_base (fun dir c tac ->
- let tac = tac, conds in
+ let tac = (tac, conds) in
general_rewrite dir AllOccurrences true false ~tac c)
tac_main bas))
tclIDTAC lbas))
@@ -238,7 +240,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
let eqclause =
if metas then eqclause
- else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+ else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
in
let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
@@ -286,7 +288,7 @@ let add_rew_rules base lrul =
let pat = if b then info.hyp_left else info.hyp_right in
let rul = { rew_lemma = c; rew_type = info.hyp_ty;
rew_pat = pat; rew_l2r = b;
- rew_tac = Tacintern.glob_tactic t}
+ rew_tac = Option.map Tacintern.glob_tactic t}
in incr counter;
HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 773e3694e..9ddabc584 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Tacmach
open Equality
(** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr
+type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr option
(** To add rewriting rules to a base *)
val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -29,7 +29,7 @@ type rew_rule = { rew_lemma: constr;
rew_type: types;
rew_pat: constr;
rew_l2r: bool;
- rew_tac: glob_tactic_expr }
+ rew_tac: glob_tactic_expr option }
val find_rewrites : string -> rew_rule list
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 75fedc598..e14c23421 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -259,14 +259,14 @@ let add_rewrite_hint bases ort t lcsr =
VERNAC COMMAND EXTEND HintRewrite
[ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
- [ add_rewrite_hint bl o (Tacexpr.TacId []) l ]
+ [ add_rewrite_hint bl o None l ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- [ add_rewrite_hint bl o t l ]
+ [ add_rewrite_hint bl o (Some t) l ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- [ add_rewrite_hint ["core"] o (Tacexpr.TacId []) l ]
+ [ add_rewrite_hint ["core"] o None l ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
- [ add_rewrite_hint ["core"] o t l ]
+ [ add_rewrite_hint ["core"] o (Some t) l ]
END
(**********************************************************************)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 0e6654545..f7c13d01a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -348,7 +348,22 @@ let refresh_hypinfo env sigma hypinfo =
| _ -> hypinfo
else hypinfo
-let unify_eqn env sigma hypinfo t =
+
+let solve_remaining_by by env prf =
+ match by with
+ | None -> env, prf
+ | Some tac ->
+ let indep = clenv_independent env in
+ let tac = eval_tactic tac in
+ let evd' =
+ List.fold_right (fun mv evd ->
+ let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
+ let c = Pfedit.build_by_tactic env.env ty (tclCOMPLETE tac) in
+ meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
+ indep env.evd
+ in { env with evd = evd' }, prf
+
+let unify_eqn env sigma hypinfo by t =
if isEvar t then None
else try
let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
@@ -365,10 +380,11 @@ let unify_eqn env sigma hypinfo t =
(* let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
let env' = { env' with evd = evd' } in
- let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in
+ let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in
+ let nf c = Evarutil.nf_evar env'.evd (Clenv.clenv_nf_meta env' c) in
let c1 = nf c1 and c2 = nf c2
and car = nf car and rel = nf rel
- and prf = nf (Clenv.clenv_value env') in
+ and prf = nf prf in
let ty1 = Typing.type_of env'.env env'.evd c1
and ty2 = Typing.type_of env'.env env'.evd c2
in
@@ -633,7 +649,7 @@ let apply_constraint env avoid car rel prf cstr res =
let eq_env x y = x == y
-let apply_rule hypinfo loccs : strategy =
+let apply_rule hypinfo by loccs : strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
let is_occ occ =
if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
@@ -641,7 +657,7 @@ let apply_rule hypinfo loccs : strategy =
fun env avoid t ty cstr evars ->
if not (eq_env !hypinfo.cl.env env) then
hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
- let unif = unify_eqn env (goalevars evars) hypinfo t in
+ let unif = unify_eqn env (goalevars evars) hypinfo by t in
if not (Option.is_empty unif) then incr occ;
match unif with
| Some (evd', (prf, (car, rel, c1, c2))) when is_occ !occ ->
@@ -655,10 +671,10 @@ let apply_rule hypinfo loccs : strategy =
end
| _ -> None
-let apply_lemma flags (evm,c) left2right loccs : strategy =
+let apply_lemma flags (evm,c) left2right by loccs : strategy =
fun env avoid t ty cstr evars ->
let hypinfo = ref (decompose_applied_relation env (goalevars evars) flags None c left2right) in
- apply_rule hypinfo loccs env avoid t ty cstr evars
+ apply_rule hypinfo by loccs env avoid t ty cstr evars
let make_leibniz_proof c ty r =
let prf =
@@ -1010,8 +1026,8 @@ module Strategies =
fix (fun out -> choice s (one_subterm out))
let lemmas flags cs : strategy =
- List.fold_left (fun tac (l,l2r) ->
- choice tac (apply_lemma flags l l2r AllOccurrences))
+ List.fold_left (fun tac (l,l2r,by) ->
+ choice tac (apply_lemma flags l l2r by AllOccurrences))
fail cs
let inj_open c = (Evd.empty,c)
@@ -1019,12 +1035,13 @@ module Strategies =
let old_hints (db : string) : strategy =
let rules = Autorewrite.find_rewrites db in
lemmas rewrite_unif_flags
- (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules)
+ (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac)) rules)
let hints (db : string) : strategy =
fun env avoid t ty cstr evars ->
let rules = Autorewrite.find_matches db t in
- let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r) in
+ let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r,
+ hint.Autorewrite.rew_tac) in
let lems = List.map lemma rules in
lemmas rewrite_unif_flags lems env avoid t ty cstr evars
@@ -1078,7 +1095,7 @@ end
(** The strategy for a single rewrite, dealing with occurences. *)
let rewrite_strat flags occs hyp =
- let app = apply_rule hyp occs in
+ let app = apply_rule hyp None occs in
let rec aux () =
Strategies.choice app (subterm true flags (fun env -> aux () env))
in aux ()
@@ -1359,22 +1376,22 @@ let occurrences_of = function
let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings))
- l2r occs env avoid t ty cstr (evd, cstrevars evars)
+ l2r None occs env avoid t ty cstr (evd, cstrevars evars)
let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings))
- l2r occs env avoid t ty cstr (evd, cstrevars evars)
+ l2r None occs env avoid t ty cstr (evd, cstrevars evars)
let interp_constr_list env sigma =
List.map (fun c ->
let evd, c = Constrintern.interp_open_constr sigma env c in
- (evd, (c, NoBindings)), true)
+ (evd, (c, NoBindings)), true, None)
let interp_glob_constr_list env sigma =
List.map (fun c ->
let evd, c = Pretyping.understand_tcc sigma env c in
- (evd, (c, NoBindings)), true)
+ (evd, (c, NoBindings)), true, None)
(* Syntax for rewriting with strategies *)
@@ -1945,7 +1962,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
let apply_lemma gl (c,l) cl l2r occs =
let sigma = project gl in
let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in
- let app = apply_rule hypinfo occs in
+ let app = apply_rule hypinfo None occs in
let rec aux () =
Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
in !hypinfo, aux ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 01:08:33 +0000