aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.travis.yml9
-rw-r--r--CHANGES4
-rw-r--r--Makefile.common5
-rw-r--r--Makefile.doc2
-rw-r--r--dev/doc/proof-engine.md134
-rw-r--r--doc/refman/RefMan-decl.tex823
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/evd.mli4
-rw-r--r--kernel/cClosure.ml11
-rw-r--r--kernel/cooking.ml8
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/opaqueproof.ml51
-rw-r--r--kernel/opaqueproof.mli5
-rw-r--r--kernel/reduction.ml13
-rw-r--r--kernel/term_typing.ml21
-rw-r--r--lib/cErrors.ml5
-rw-r--r--lib/pp.ml19
-rw-r--r--lib/pp.mli1
-rw-r--r--plugins/decl_mode/decl_expr.mli102
-rw-r--r--plugins/decl_mode/decl_interp.ml471
-rw-r--r--plugins/decl_mode/decl_interp.mli15
-rw-r--r--plugins/decl_mode/decl_mode.ml136
-rw-r--r--plugins/decl_mode/decl_mode.mli79
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mlpack5
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml1575
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli108
-rw-r--r--plugins/decl_mode/g_decl_mode.ml4387
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml218
-rw-r--r--plugins/decl_mode/ppdecl_proof.mli14
-rw-r--r--plugins/firstorder/g_ground.ml418
-rw-r--r--plugins/ltac/extratactics.ml48
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/tacinterp.ml24
-rw-r--r--pretyping/evarconv.ml28
-rw-r--r--pretyping/pretyping.ml62
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/unification.ml6
-rw-r--r--pretyping/unification.mli6
-rw-r--r--proofs/pfedit.ml12
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--tactics/tactics.ml18
-rw-r--r--tactics/tactics.mli2
-rw-r--r--test-suite/bugs/closed/2640.v17
-rw-r--r--test-suite/ide/undo.v103
-rw-r--r--test-suite/ide/undo011.fake34
-rw-r--r--test-suite/output/ErrorInModule.out1
-rw-r--r--test-suite/output/ErrorInSection.out1
-rw-r--r--test-suite/output/qualification.out1
-rw-r--r--test-suite/success/decl_mode.v182
-rw-r--r--test-suite/success/decl_mode2.v249
-rw-r--r--theories/Init/Prelude.v1
-rw-r--r--toplevel/coqloop.ml132
-rw-r--r--toplevel/coqloop.mli7
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--vernac/command.ml8
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/topfmt.ml25
-rw-r--r--vernac/topfmt.mli8
60 files changed, 418 insertions, 4783 deletions
diff --git a/.travis.yml b/.travis.yml
index 81f50af0a..d35b7a842 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -123,3 +123,12 @@ script:
- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
- ${TW} make -j ${NJOBS} ${TEST_TARGET}
- echo -en 'travis_fold:end:coq.test\\r'
+
+# Testing Gitter webhook
+notifications:
+ webhooks:
+ urls:
+ - https://webhooks.gitter.im/e/3cdabdec318214c7cd63
+ on_success: change # options: [always|never|change] default: always
+ on_failure: always # options: [always|never|change] default: always
+ on_start: never # options: [always|never|change] default: always
diff --git a/CHANGES b/CHANGES
index 0acc2bb95..240d71ec0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,6 +22,10 @@ Standard Library
- Real constants are now represented using IZR rather than R0 and R1;
this might cause rewriting rules to fail to apply to constants.
+Plugins
+
+- The mathematical proof language (also known as declarative mode) was removed.
+
Changes from V8.6beta1 to V8.6
==============================
diff --git a/Makefile.common b/Makefile.common
index 1e71bcf7d..d5f79d76b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -61,7 +61,7 @@ PLUGINDIRS:=\
omega romega micromega quote \
setoid_ring extraction fourier \
cc funind firstorder derive \
- rtauto nsatz syntax decl_mode btauto \
+ rtauto nsatz syntax btauto \
ssrmatching ltac
SRCDIRS:=\
@@ -117,12 +117,11 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
r_syntax_plugin.cmo \
ascii_syntax_plugin.cmo \
string_syntax_plugin.cmo )
-DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
DERIVECMO:=plugins/derive/derive_plugin.cmo
LTACCMO:=plugins/ltac/ltac_plugin.cmo
SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
-PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
+PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
$(QUOTECMO) $(RINGCMO) \
$(FOURIERCMO) $(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
diff --git a/Makefile.doc b/Makefile.doc
index 9ae20ba76..39c3255f5 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -48,7 +48,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
RefMan-cic.v.tex RefMan-lib.v.tex \
RefMan-tacex.v.tex RefMan-syn.v.tex \
RefMan-oth.v.tex RefMan-ltac.v.tex \
- RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
+ RefMan-pro.v.tex RefMan-sch.v.tex \
Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
Setoid.v.tex Classes.v.tex Universes.v.tex \
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
new file mode 100644
index 000000000..db69b08a2
--- /dev/null
+++ b/dev/doc/proof-engine.md
@@ -0,0 +1,134 @@
+Tutorial on the new proof engine for ML tactic writers
+======================================================
+
+Starting from Coq 8.5, a new proof engine has been introduced, replacing the old
+meta-based engine which had a lot of drawbacks, ranging from expressivity to
+soundness, the major one being that the type of tactics was transparent. This
+was pervasively abused and made virtually impossible to tweak the implementation
+of the engine.
+
+The old engine is deprecated and is slowly getting removed from the source code.
+
+The new engine relies on a monadic API defined in the `Proofview` module. Helper
+functions and higher-level operations are defined in the `Tacmach` and
+`Tacticals` modules, and end-user tactics are defined amongst other in the
+`Tactics` module.
+
+At the root of the engine is a representation of proofs as partial terms that
+can contain typed holes, called evars, short for *existential variable*. An evar
+is essentially defined by its context and return type, that we will write
+`?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type
+`Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by
+applying `EConstr.mkEvar`, and which we will write `?e{σ}`.
+
+The engine monad features a notion of global state called `evar_map`, defined in
+the `Evd` module, which is the structure containing the incremental refinement
+of evars. `Evd` is a low-level API and its use is discouraged in favour of the
+`Evarutil` module which provides more abstract primitives.
+
+In addition to this state, the monad also features a goal state, that is
+an ordered list of current holes to be filled. While these holes are referred
+to as goals at a high-enough level, they are actually no more than evars. The
+API provided to deal with these holes can be found in the `Proofview.Goal`
+module. Tactics are naturally operating on several goals at once, so that it is
+usual to use the `Proofview.Goal.enter` function and its variants to dispatch a
+tactic to each of the goals under focus.
+
+Primitive tactics by term refining
+-------------------------------------
+
+A typical low-level tactic will be defined by plugging partial terms in the
+goal holes thanks to the `Refine` module, and in particular to the
+`Refine.refine` primitive.
+
+```ocaml
+val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+(** In [refine ?unsafe t], [t] is a term with holes under some
+ [evar_map] context. The term [t] is used as a partial solution
+ for the current goal (refine is a goal-dependent tactic), the
+ new holes created by [t] become the new subgoals. Exceptions
+ raised during the interpretation of [t] are caught and result in
+ tactic failures. If [unsafe] is [false] (default is [true]) [t] is
+ type-checked beforehand. *)
+```
+
+In a first approximation, we can think of `'a Sigma.run` as
+`evar_map -> 'a * evar_map`. What the function does is first evaluate the
+`Constr.t Sigma.run` argument in the current proof state, and then use the
+resulting term as a filler for the proof under focus. All evars that have been
+created by the invocation of this thunk are then turned into new goals added in
+the order of their creation.
+
+To see how we can use it, let us have a look at an idealized example, the `cut`
+tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
+with a term `let x : X := ?e2{Γ} in ?e1{Γ} x` where `x` is a fresh variable and
+`?e1 : [Γ ⊢ _ : X -> A]` and `?e2 : [Γ ⊢ _ : X]`. The current goal is solved and
+two new holes `[e1, e2]` are added to the goal state in this order.
+
+```ocaml
+let cut c =
+ let open Sigma in
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ (** In this block, we focus on one goal at a time indicated by gl *)
+ let env = Proofview.Goal.env gl in
+ (** Get the context of the goal, essentially [Γ] *)
+ let concl = Proofview.Goal.concl gl in
+ (** Get the conclusion [A] of the goal *)
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
+ (** List of hypotheses from the context of the goal *)
+ let id = Namegen.next_name_away Anonymous hyps in
+ (** Generate a fresh identifier *)
+ let t = mkArrow c (Vars.lift 1 concl) in
+ (** Build [X -> A]. Note the lifting of [A] due to being on the right hand
+ side of the arrow. *)
+ Refine.refine { run = begin fun sigma ->
+ (** All evars generated by this block will be added as goals *)
+ let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
+ (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
+ term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
+ substitution for [Γ] is extracted from the [env] argument, so that
+ one must be careful to pass the correct context here in order for the
+ resulting term to be well-typed. The [p] return value is a proof term
+ used to enforce sigma monotonicity. *)
+ let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
+ (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
+ [x := Γ ⊢ ?e2{Γ} : X]. *)
+ let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
+ (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
+ Sigma (r, sigma, p +> q)
+ (** Fills the current hole with [r]. The [p +> q] thingy ensures
+ monotonicity of sigma. *)
+ end }
+ end }
+```
+
+The `Evarutil.new_evar` function is the preferred way to generate evars in
+tactics. It returns a ready-to-use term, so that one does not have to call
+the `mkEvar` primitive. There are lower-level variants whose use is dedicated to
+special use cases, *e.g.* whenever one wants a non-identity substitution. One
+should take care to call it with the proper `env` argument so that the evar
+and term it generates make sense in the context they will be plugged in.
+
+For the sake of completeness, the old engine was relying on the `Tacmach.refine`
+function to provide a similar feature. Nonetheless, it was using untyped metas
+instead of evars, so that it had to mangle the argument term to actually produce
+the term that would be put into the hole. For instance, to work around the
+untypedness, some metas had to be coerced with a cast to enforce their type,
+otherwise leading to runtime errors. This was working for very simple
+instances, but was unreliable for everything else.
+
+High-level composition of tactics
+------------------------------------
+
+It is possible to combine low-level refinement tactics to create more powerful
+abstractions. While it was the standard way of doing things in the old engine
+to overcome its technical limitations (namely that one was forced to go through
+a limited set of derivation rules), it is recommended to generate proofs as
+much as possible by refining in ML tactics when it is possible and easy enough.
+Indeed, this prevents dependence on fragile constructions such as unification.
+
+Obviously, it does not forbid the use of tacticals to mimick what one would do
+in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple
+semantics. A list of such tacticals can be found in the `Tacticals` module. Most
+of them are a porting of the tacticals from the old engine to the new one, so
+that if they share the same name they are expected to have the same semantics.
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
deleted file mode 100644
index aae10e323..000000000
--- a/doc/refman/RefMan-decl.tex
+++ /dev/null
@@ -1,823 +0,0 @@
-\newcommand{\DPL}{Mathematical Proof Language}
-
-\chapter{The \DPL\label{DPL}\index{DPL}}
-
-\section{Introduction}
-
-\subsection{Foreword}
-
-In this chapter, we describe an alternative language that may be used
-to do proofs using the Coq proof assistant. The language described
-here uses the same objects (proof-terms) as Coq, but it differs in the
-way proofs are described. This language was created by Pierre
-Corbineau at the Radboud University of Nijmegen, The Netherlands.
-
-The intent is to provide language where proofs are less formalism-{}
-and implementation-{}sensitive, and in the process to ease a bit the
-learning of computer-{}aided proof verification.
-
-\subsection{What is a declarative proof?}
-In vanilla Coq, proofs are written in the imperative style: the user
-issues commands that transform a so called proof state until it
-reaches a state where the proof is completed. In the process, the user
-mostly described the transitions of this system rather than the
-intermediate states it goes through.
-
-The purpose of a declarative proof language is to take the opposite
-approach where intermediate states are always given by the user, but
-the transitions of the system are automated as much as possible.
-
-\subsection{Well-formedness and Completeness}
-
-The \DPL{} introduces a notion of well-formed
-proofs which are weaker than correct (and complete)
-proofs. Well-formed proofs are actually proof script where only the
-reasoning is incomplete. All the other aspects of the proof are
-correct:
-\begin{itemize}
-\item All objects referred to exist where they are used
-\item Conclusion steps actually prove something related to the
- conclusion of the theorem (the {\tt thesis}.
-\item Hypothesis introduction steps are done when the goal is an
- implication with a corresponding assumption.
-\item Sub-objects in the elimination steps for tuples are correct
- sub-objects of the tuple being decomposed.
-\item Patterns in case analysis are type-correct, and induction is well guarded.
-\end{itemize}
-
-\subsection{Note for tactics users}
-
-This section explain what differences the casual Coq user will
-experience using the \DPL.
-\begin{enumerate}
-\item The focusing mechanism is constrained so that only one goal at
- a time is visible.
-\item Giving a statement that Coq cannot prove does not produce an
- error, only a warning: this allows going on with the proof and fill
- the gap later.
-\item Tactics can still be used for justifications and after
-{\texttt{escape}}.
-\end{enumerate}
-
-\subsection{Compatibility}
-
-The \DPL{} is available for all Coq interfaces that use
-text-based interaction, including:
-\begin{itemize}
-\item the command-{}line toplevel {\texttt{coqtop}}
-\item the native GUI {\CoqIDE}
-\item the {\ProofGeneral} Emacs mode
-\item Cezary Kaliszyk'{}s Web interface
-\item L.E. Mamane'{}s tmEgg TeXmacs plugin
-\end{itemize}
-
-However it is not supported by structured editors such as PCoq.
-
-
-
-\section{Syntax}
-
-Here is a complete formal description of the syntax for \DPL{} commands.
-
-\begin{figure}[htbp]
-\begin{centerframe}
-\begin{tabular}{lcl@{\qquad}r}
- instruction & ::= & {\tt proof} \\
- & $|$ & {\tt assume } \nelist{statement}{\tt and}
- \zeroone{[{\tt and } \{{\tt we have}\}-clause]} \\
- & $|$ & \{{\tt let},{\tt be}\}-clause \\
- & $|$ & \{{\tt given}\}-clause \\
- & $|$ & \{{\tt consider}\}-clause {\tt from} term \\
- & $|$ & ({\tt have} $|$ {\tt then} $|$ {\tt thus} $|$ {\tt hence}]) statement
- justification \\
- & $|$ & \zeroone{\tt thus} ($\sim${\tt =}|{\tt =}$\sim$) \zeroone{\ident{\tt :}}\term\relax justification \\ & $|$ & {\tt suffices} (\{{\tt to have}\}-clause $|$
- \nelist{statement}{\tt and } \zeroone{{\tt and} \{{\tt to have}\}-clause})\\
- & & {\tt to show} statement justification \\
- & $|$ & ({\tt claim} $|$ {\tt focus on}) statement \\
- & $|$ & {\tt take} \term \\
- & $|$ & {\tt define} \ident \sequence{var}{,} {\tt as} \term\\
- & $|$ & {\tt reconsider} (\ident $|$ {\tt thesis}) {\tt as} type\\
- & $|$ &
- {\tt per} ({\tt cases}$|${\tt induction}) {\tt on} \term \\
- & $|$ & {\tt per cases of} type justification \\
- & $|$ & {\tt suppose} \zeroone{\nelist{ident}{,} {\tt and}}~
- {\tt it is }pattern\\
- & & \zeroone{{\tt such that} \nelist{statement} {\tt and} \zeroone{{\tt and} \{{\tt we have}\}-clause}} \\
- & $|$ & {\tt end}
- ({\tt proof} $|$ {\tt claim} $|$ {\tt focus} $|$ {\tt cases} $|$ {\tt induction}) \\
- & $|$ & {\tt escape} \\
- & $|$ & {\tt return} \medskip \\
- \{$\alpha,\beta$\}-clause & ::=& $\alpha$ \nelist{var}{,}~
- $\beta$ {\tt such that} \nelist{statement}{\tt and } \\
- & & \zeroone{{\tt and } \{$\alpha,\beta$\}-clause} \medskip\\
- statement & ::= & \zeroone{\ident {\tt :}} type \\
- & $|$ & {\tt thesis} \\
- & $|$ & {\tt thesis for} \ident \medskip \\
- var & ::= & \ident \zeroone{{\tt :} type} \medskip \\
- justification & ::= &
- \zeroone{{\tt by} ({\tt *} | \nelist{\term}{,})}
- ~\zeroone{{\tt using} tactic} \\
-\end{tabular}
-\end{centerframe}
-\caption{Syntax of mathematical proof commands}
-\end{figure}
-
-The lexical conventions used here follows those of section \ref{lexical}.
-
-
-Conventions:\begin{itemize}
-
- \item {\texttt{<{}tactic>{}}} stands for a Coq tactic.
-
- \end{itemize}
-
-\subsection{Temporary names}
-
-In proof commands where an optional name is asked for, omitting the
-name will trigger the creation of a fresh temporary name (e.g. for a
-hypothesis). Temporary names always start with an underscore `\_'
-character (e.g. {\tt \_hyp0}). Temporary names have a lifespan of one
-command: they get erased after the next command. They can however be safely in the step after their creation.
-
-\section{Language description}
-
-\subsection{Starting and Ending a mathematical proof}
-
-The standard way to use the \DPL{} is to first state a \texttt{Lemma} /
-\texttt{Theorem} / \texttt{Definition} and then use the \texttt{proof}
-command to switch the current subgoal to mathematical mode. After the
-proof is completed, the \texttt{end proof} command will close the
-mathematical proof. If any subgoal remains to be proved, they will be
-displayed using the usual Coq display.
-
-\begin{coq_example}
-Theorem this_is_trivial: True.
-proof.
- thus thesis.
-end proof.
-Qed.
-\end{coq_example}
-
-The {\texttt{proof}} command only applies to \emph{one subgoal}, thus
-if several sub-goals are already present, the {\texttt{proof ... end
- proof}} sequence has to be used several times.
-
-\begin{coq_example*}
-Theorem T: (True /\ True) /\ True.
- split. split.
-\end{coq_example*}
-\begin{coq_example}
- Show.
- proof. (* first subgoal *)
- thus thesis.
- end proof.
- trivial. (* second subgoal *)
- proof. (* third subgoal *)
- thus thesis.
- end proof.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-As with all other block structures, the {\texttt{end proof}} command
-assumes that your proof is complete. If not, executing it will be
-equivalent to admitting that the statement is proved: A warning will
-be issued and you will not be able to run the {\texttt{Qed}}
-command. Instead, you can run {\texttt{Admitted}} if you wish to start
-another theorem and come back
-later.
-
-\begin{coq_example}
-Theorem this_is_not_so_trivial: False.
-proof.
-end proof. (* here a warning is issued *)
-Fail Qed. (* fails: the proof in incomplete *)
-Admitted. (* Oops! *)
-\end{coq_example}
-\begin{coq_eval}
-Reset this_is_not_so_trivial.
-\end{coq_eval}
-
-\subsection{Switching modes}
-
-When writing a mathematical proof, you may wish to use procedural
-tactics at some point. One way to do so is to write a using-{}phrase
-in a deduction step (see section~\ref{justifications}). The other way
-is to use an {\texttt{escape...return}} block.
-
-\begin{coq_eval}
-Theorem T: True.
-proof.
-\end{coq_eval}
-\begin{coq_example}
- Show.
- escape.
- auto.
- return.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-The return statement expects all subgoals to be closed, otherwise a
-warning is issued and the proof cannot be saved anymore.
-
-It is possible to use the {\texttt{proof}} command inside an
-{\texttt{escape...return}} block, thus nesting a mathematical proof
-inside a procedural proof inside a mathematical proof...
-
-\subsection{Computation steps}
-
-The {\tt reconsider ... as} command allows changing the type of a hypothesis or of {\tt thesis} to a convertible one.
-
-\begin{coq_eval}
-Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False).
-intros a b.
-proof.
-assume H:(if a then True else False).
-\end{coq_eval}
-\begin{coq_example}
- Show.
- reconsider H as False.
- reconsider thesis as True.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-
-\subsection{Deduction steps}
-
-The most common instruction in a mathematical proof is the deduction
-step: it asserts a new statement (a formula/type of the \CIC) and tries
-to prove it using a user-provided indication: the justification. The
-asserted statement is then added as a hypothesis to the proof context.
-
-\begin{coq_eval}
-Theorem T: forall x, x=2 -> 2+x=4.
-proof.
-let x be such that H:(x=2).
-\end{coq_eval}
-\begin{coq_example}
- Show.
- have H':(2+x=2+2) by H.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-It is often the case that the justifications uses the last hypothesis
-introduced in the context, so the {\tt then} keyword can be used as a
-shortcut, e.g. if we want to do the same as the last example:
-
-\begin{coq_eval}
-Theorem T: forall x, x=2 -> 2+x=4.
-proof.
-let x be such that H:(x=2).
-\end{coq_eval}
-\begin{coq_example}
- Show.
- then (2+x=2+2).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-In this example, you can also see the creation of a temporary name {\tt \_fact}.
-
-\subsection{Iterated equalities}
-
-A common proof pattern when doing a chain of deductions is to do
-multiple rewriting steps over the same term, thus proving the
-corresponding equalities. The iterated equalities are a syntactic
-support for this kind of reasoning:
-
-\begin{coq_eval}
-Theorem T: forall x, x=2 -> x + x = x * x.
-proof.
-let x be such that H:(x=2).
-\end{coq_eval}
-\begin{coq_example}
- Show.
- have (4 = 4).
- ~= (2 * 2).
- ~= (x * x) by H.
- =~ (2 + 2).
- =~ H':(x + x) by H.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Notice that here we use temporary names heavily.
-
-\subsection{Subproofs}
-
-When an intermediate step in a proof gets too complicated or involves a
-well contained set of intermediate deductions, it can be useful to insert
-its proof as a subproof of the current proof. This is done by using the
-{\tt claim ... end claim} pair of commands.
-
-\begin{coq_eval}
-Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2.
-proof.
-let x be such that H:(x + x = x * x).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-claim H':((x - 2) * x = 0).
-\end{coq_example}
-
-A few steps later...
-
-\begin{coq_example}
-thus thesis.
-end claim.
-\end{coq_example}
-
-Now the rest of the proof can happen.
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Conclusion steps}
-
-The commands described above have a conclusion counterpart, where the
-new hypothesis is used to refine the conclusion.
-
-\begin{figure}[b]
- \centering
-\begin{tabular}{c|c|c|c|c|}
- X & \,simple\, & \,with previous step\, &
- \,opens sub-proof\, & \,iterated equality\, \\
-\hline
-intermediate step & {\tt have} & {\tt then} &
- {\tt claim} & {\tt $\sim$=/=$\sim$}\\
-conclusion step & {\tt thus} & {\tt hence} &
- {\tt focus on} & {\tt thus $\sim$=/=$\sim$}\\
-\hline
-\end{tabular}
-\caption{Correspondence between basic forward steps and conclusion steps}
-\end{figure}
-
-Let us begin with simple examples:
-
-\begin{coq_eval}
-Theorem T: forall (A B:Prop), A -> B -> A /\ B.
-intros A B HA HB.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-hence B.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-In the next example, we have to use {\tt thus} because {\tt HB} is no longer
-the last hypothesis.
-
-\begin{coq_eval}
-Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C.
-intros A B C HA HB HC.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-thus B by HB.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-The command fails if the refinement process cannot find a place to fit
-the object in a proof of the conclusion.
-
-
-\begin{coq_eval}
-Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B.
-intros A B C HA HB HC.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-Fail hence C. (* fails *)
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-The refinement process may induce non
-reversible choices, e.g. when proving a disjunction it may {\it
- choose} one side of the disjunction.
-
-\begin{coq_eval}
-Theorem T: forall (A B:Prop), B -> A \/ B.
-intros A B HB.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-hence B.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-In this example you can see that the right branch was chosen since {\tt D} remains to be proved.
-
-\begin{coq_eval}
-Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D).
-intros A B C D HC HD.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-thus C by HC.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Now for existential statements, we can use the {\tt take} command to
-choose {\tt 2} as an explicit witness of existence.
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
-intros P HP.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-take 2.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-It is also possible to prove the existence directly.
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
-intros P HP.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-hence (P 2).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Here a more involved example where the choice of {\tt P 2} propagates
-the choice of {\tt 2} to another part of the formula.
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y.
-intros P R HP HR.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-thus (P 2) by HP.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Now, an example with the {\tt suffices} command. {\tt suffices}
-is a sort of dual for {\tt have}: it allows replacing the conclusion
-(or part of it) by a sufficient condition.
-
-\begin{coq_eval}
-Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B.
-intros A B P HP HA.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-suffices to have x such that HP':(P x) to show B by HP,HP'.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Finally, an example where {\tt focus} is handy: local assumptions.
-
-\begin{coq_eval}
-Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x).
-intros A P HP HA.
-proof.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-focus on (forall x, x = 2 -> P x).
-let x be such that (x = 2).
-hence thesis by HP.
-end focus.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Declaring an Abbreviation}
-
-In order to shorten long expressions, it is possible to use the {\tt
- define ... as ...} command to give a name to recurring expressions.
-
-\begin{coq_eval}
-Theorem T: forall x, x = 0 -> x + x = x * x.
-proof.
-let x be such that H:(x = 0).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-define sqr x as (x * x).
-reconsider thesis as (x + x = sqr x).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Introduction steps}
-
-When the {\tt thesis} consists of a hypothetical formula (implication
-or universal quantification (e.g. \verb+A -> B+), it is possible to
-assume the hypothetical part {\tt A} and then prove {\tt B}. In the
-\DPL{}, this comes in two syntactic flavors that are semantically
-equivalent: {\tt let} and {\tt assume}. Their syntax is designed so that
-{\tt let} works better for universal quantifiers and {\tt assume} for
-implications.
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-let x:nat.
-assume HP:(P x).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-In the {\tt let} variant, the type of the assumed object is optional
-provided it can be deduced from the command. The objects introduced by
-let can be followed by assumptions using {\tt such that}.
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-Fail let x. (* fails because x's type is not clear *)
-let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-In the {\tt assume } variant, the type of the assumed object is mandatory
-but the name is optional:
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x:nat.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-assume (P x). (* temporary name created *)
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-After {\tt such that}, it is also the case:
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-let x be such that (P x). (* temporary name created *)
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Tuple elimination steps}
-
-In the \CIC, many objects dealt with in simple proofs are tuples:
-pairs, records, existentially quantified formulas. These are so
-common that the \DPL{} provides a mechanism to extract members of
-those tuples, and also objects in tuples within tuples within
-tuples...
-
-\begin{coq_eval}
-Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A.
-proof.
-let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-consider x such that HP:(P x) and HA:A from H.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Here is an example with pairs:
-
-\begin{coq_eval}
-Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p).
-proof.
-let p:(nat * nat)%type.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-consider x:nat,y:nat from p.
-reconsider thesis as (x >= y \/ x < y).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-It is sometimes desirable to combine assumption and tuple
-decomposition. This can be done using the {\tt given} command.
-
-\begin{coq_eval}
-Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) ->
-(exists m, P m) -> P 0.
-proof.
-let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)).
-\end{coq_eval}
-\begin{coq_example}
-Show.
-given m such that Hm:(P m).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Disjunctive reasoning}
-
-In some proofs (most of them usually) one has to consider several
-cases and prove that the {\tt thesis} holds in all the cases. This is
-done by first specifying which object will be subject to case
-distinction (usually a disjunction) using {\tt per cases}, and then specifying which case is being proved by using {\tt suppose}.
-
-
-\begin{coq_eval}
-Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C.
-proof.
-let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C).
-assume HAB:(A \/ B).
-\end{coq_eval}
-\begin{coq_example}
-per cases on HAB.
-suppose A.
- hence thesis by HAC.
-suppose HB:B.
- thus thesis by HB,HBC.
-end cases.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-The proof is well formed (but incomplete) even if you type {\tt end
- cases} or the next {\tt suppose} before the previous case is proved.
-
-If the disjunction is derived from a more general principle, e.g. the
-excluded middle axiom), it is desirable to just specify which instance
-of it is being used:
-
-\begin{coq_eval}
-Section Coq.
-\end{coq_eval}
-\begin{coq_example}
-Hypothesis EM : forall P:Prop, P \/ ~ P.
-\end{coq_example}
-\begin{coq_eval}
-Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
-proof.
-let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
-\end{coq_eval}
-\begin{coq_example}
-per cases of (A \/ ~A) by EM.
-suppose (~A).
- hence thesis by HNAC.
-suppose A.
- hence thesis by HAC.
-end cases.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Proofs per cases}
-
-If the case analysis is to be made on a particular object, the script
-is very similar: it starts with {\tt per cases on }\emph{object} instead.
-
-\begin{coq_eval}
-Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
-proof.
-let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
-\end{coq_eval}
-\begin{coq_example}
-per cases on (EM A).
-suppose (~A).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-End Coq.
-\end{coq_eval}
-
-If the object on which a case analysis occurs in the statement to be
-proved, the command {\tt suppose it is }\emph{pattern} is better
-suited than {\tt suppose}. \emph{pattern} may contain nested patterns
-with {\tt as} clauses. A detailed description of patterns is to be
-found in figure \ref{term-syntax-aux}. here is an example.
-
-\begin{coq_eval}
-Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B.
-proof.
-let A:Prop,B:Prop,x:bool.
-\end{coq_eval}
-\begin{coq_example}
-per cases on x.
-suppose it is true.
- assume A.
- hence A.
-suppose it is false.
- assume B.
- hence B.
-end cases.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Proofs by induction}
-
-Proofs by induction are very similar to proofs per cases: they start
-with {\tt per induction on }{\tt object} and proceed with {\tt suppose
- it is }\emph{pattern}{\tt and }\emph{induction hypothesis}. The
-induction hypothesis can be given explicitly or identified by the
-sub-object $m$ it refers to using {\tt thesis for }\emph{m}.
-
-\begin{coq_eval}
-Theorem T: forall (n:nat), n + 0 = n.
-proof.
-let n:nat.
-\end{coq_eval}
-\begin{coq_example}
-per induction on n.
-suppose it is 0.
- thus (0 + 0 = 0).
-suppose it is (S m) and H:thesis for m.
- then (S (m + 0) = S m).
- thus =~ (S m + 0).
-end induction.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\subsection{Justifications}\label{justifications}
-
-
-Intuitively, justifications are hints for the system to understand how
-to prove the statements the user types in. In the case of this
-language justifications are made of two components:
-
-Justification objects: {\texttt{by}} followed by a comma-{}separated
-list of objects that will be used by a selected tactic to prove the
-statement. This defaults to the empty list (the statement should then
-be tautological). The * wildcard provides the usual tactics behavior:
-use all statements in local context. However, this wildcard should be
-avoided since it reduces the robustness of the script.
-
-Justification tactic: {\texttt{using}} followed by a Coq tactic that
-is executed to prove the statement. The default is a solver for
-(intuitionistic) first-{}order with equality.
-
-\section{More details and Formal Semantics}
-
-I suggest the users looking for more information have a look at the
-paper \cite{corbineau08types}. They will find in that paper a formal
-semantics of the proof state transition induces by mathematical
-commands.
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index dcb98d96b..291c07de4 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -98,7 +98,6 @@ Options A and B of the licence are {\em not} elected.}
\include{RefMan-tac.v}% Tactics and tacticals
\include{RefMan-ltac.v}% Writing tactics
\include{RefMan-tacex.v}% Detailed Examples of tactics
-\include{RefMan-decl.v}% The mathematical proof language
\part{User extensions}
\include{RefMan-syn.v}% The Syntax and the Grammar commands
diff --git a/engine/evd.ml b/engine/evd.ml
index 0ea15dd21..5419a10a8 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1103,10 +1103,6 @@ let set_extra_data extras evd = { evd with extras }
(*******************************************************************)
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
type open_constr = evar_map * constr
(*******************************************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index 9c6cd60bc..9c40c8b71 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -584,10 +584,6 @@ val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -
(* constr with holes and pending resolution of classes, conversion *)
(* problems, candidates, etc. *)
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
type open_constr = evar_map * constr (* Special case when before is empty *)
(** Partially constructed constrs. *)
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index fe9ec5794..b1dd26119 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -540,7 +540,16 @@ let mk_clos e t =
| (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
{norm = Red; term = FCLOS(t,e)}
-let mk_clos_vect env v = CArray.Fun1.map mk_clos env v
+(** Hand-unrolling of the map function to bypass the call to the generic array
+ allocation *)
+let mk_clos_vect env v = match v with
+| [||] -> [||]
+| [|v0|] -> [|mk_clos env v0|]
+| [|v0; v1|] -> [|mk_clos env v0; mk_clos env v1|]
+| [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|]
+| [|v0; v1; v2; v3|] ->
+ [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
+| v -> CArray.Fun1.map mk_clos env v
(* Translate the head constructor of t from constr to fconstr. This
function is parameterized by the function to apply on the direct
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f5059cd75..a9f212393 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -191,15 +191,19 @@ let lift_univs cb subst =
subst, Univ.UContext.make (inst,cstrs')
else subst, cb.const_universes
-let cook_constant env { from = cb; info } =
+let cook_constant ~hcons env { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
let usubst, univs = lift_univs cb usubst in
let expmod = expmod_constr_subst cache modlist usubst in
let hyps = Context.Named.map expmod abstract in
+ let map c =
+ let c = abstract_constant_body (expmod c) hyps in
+ if hcons then hcons_constr c else c
+ in
let body = on_body modlist (hyps, usubst, abs_ctx)
- (fun c -> abstract_constant_body (expmod c) hyps)
+ map
cb.const_body
in
let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index eb4073096..7d47eba23 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,7 @@ type result =
bool * constant_universes * inline
* Context.Named.t option
-val cook_constant : env -> recipe -> result
+val cook_constant : hcons:bool -> env -> recipe -> result
val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
(** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f147ea343..d0593c0e0 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -21,8 +21,18 @@ type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
| Direct of cooking_info list * proofterm
-type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t
-let empty_opaquetab = Int.Map.empty, DirPath.initial
+type opaquetab = {
+ opaque_val : (cooking_info list * proofterm) Int.Map.t;
+ (** Actual proof terms *)
+ opaque_len : int;
+ (** Size of the above map *)
+ opaque_dir : DirPath.t;
+}
+let empty_opaquetab = {
+ opaque_val = Int.Map.empty;
+ opaque_len = 0;
+ opaque_dir = DirPath.initial;
+}
(* hooks *)
let default_get_opaque dp _ =
@@ -42,21 +52,25 @@ let set_indirect_univ_accessor f = (get_univ := f)
let create cu = Direct ([],cu)
-let turn_indirect dp o (prfs,odp) = match o with
+let turn_indirect dp o tab = match o with
| Indirect (_,_,i) ->
- if not (Int.Map.mem i prfs)
+ if not (Int.Map.mem i tab.opaque_val)
then CErrors.anomaly (Pp.str "Indirect in a different table")
else CErrors.anomaly (Pp.str "Already an indirect opaque")
| Direct (d,cu) ->
- let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
- let id = Int.Map.cardinal prfs in
- let prfs = Int.Map.add id (d,cu) prfs in
- let ndp =
- if DirPath.equal dp odp then odp
- else if DirPath.equal odp DirPath.initial then dp
+ (** Uncomment to check dynamically that all terms turned into
+ indirections are hashconsed. *)
+(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
+(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
+ let id = tab.opaque_len in
+ let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+ let opaque_dir =
+ if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
+ else if DirPath.equal tab.opaque_dir DirPath.initial then dp
else CErrors.anomaly
(Pp.str "Using the same opaque table for multiple dirpaths") in
- Indirect ([],dp,id), (prfs, ndp)
+ let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
+ Indirect ([],dp,id), ntab
let subst_opaque sub = function
| Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
@@ -72,21 +86,21 @@ let discharge_direct_opaque ~cook_constr ci = function
| Direct (d,cu) ->
Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
-let join_opaque (prfs,odp) = function
+let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) -> ignore(Future.join cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp then
let fp = snd (Int.Map.find i prfs) in
ignore(Future.join fp)
-let uuid_opaque (prfs,odp) = function
+let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) -> Some (Future.uuid cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
then Some (Future.uuid (snd (Int.Map.find i prfs)))
else None
-let force_proof (prfs,odp) = function
+let force_proof { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) ->
fst(Future.force cu)
| Indirect (l,dp,i) ->
@@ -97,7 +111,7 @@ let force_proof (prfs,odp) = function
let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
-let force_constraints (prfs,odp) = function
+let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
@@ -106,14 +120,14 @@ let force_constraints (prfs,odp) = function
| None -> Univ.ContextSet.empty
| Some u -> Future.force u
-let get_constraints (prfs,odp) = function
+let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
else !get_univ dp i
-let get_proof (prfs,odp) = function
+let get_proof { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) -> Future.chain ~pure:true cu fst
| Indirect (l,dp,i) ->
let pt =
@@ -129,8 +143,7 @@ let a_constr = Future.from_val (Term.mkRel 1)
let a_univ = Future.from_val Univ.ContextSet.empty
let a_discharge : cooking_info list = []
-let dump (otab,_) =
- let n = Int.Map.cardinal otab in
+let dump { opaque_val = otab; opaque_len = n } =
let opaque_table = Array.make n a_constr in
let univ_table = Array.make n a_univ in
let disch_table = Array.make n a_discharge in
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5139cf051..3897d5e51 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,8 +28,9 @@ val empty_opaquetab : opaquetab
(** From a [proofterm] to some [opaque]. *)
val create : proofterm -> opaque
-(** Turn a direct [opaque] into an indirect one, also hashconses constr.
- * The integer is an hint of the maximum id used so far *)
+(** Turn a direct [opaque] into an indirect one. It is your responsibility to
+ hashcons the inner term beforehand. The integer is an hint of the maximum id
+ used so far *)
val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
(** From a [opaque] back to a [constr]. This might use the
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1ae89347a..0d7f77eda 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -71,6 +71,17 @@ let rec zlapp v = function
Zlapp v2 :: s -> zlapp (Array.append v v2) s
| s -> Zlapp v :: s
+(** Hand-unrolling of the map function to bypass the call to the generic array
+ allocation. Type annotation is required to tell OCaml that the array does
+ not contain floats. *)
+let map_lift (l : lift) (v : fconstr array) = match v with
+| [||] -> assert false
+| [|c0|] -> [|(l, c0)|]
+| [|c0; c1|] -> [|(l, c0); (l, c1)|]
+| [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
+| [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
+| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+
let pure_stack lfts stk =
let rec pure_rec lfts stk =
match stk with
@@ -80,7 +91,7 @@ let pure_stack lfts stk =
(Zupdate _,lpstk) -> lpstk
| (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
| (Zapp a, (l,pstk)) ->
- (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
+ (l,zlapp (map_lift l a) pstk)
| (Zproj (n,m,c), (l,pstk)) ->
(l, Zlproj (c,l)::pstk)
| (Zfix(fx,a),(l,pstk)) ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2eb2c040e..6dfa64357 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -139,6 +139,12 @@ let inline_side_effects env body ctx side_eff =
(* CAVEAT: we assure a proper order *)
List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
+let rec is_nth_suffix n l suf =
+ if Int.equal n 0 then l == suf
+ else match l with
+ | [] -> false
+ | _ :: l -> is_nth_suffix (pred n) l suf
+
(* Given the list of signatures of side effects, checks if they match.
* I.e. if they are ordered descendants of the current revstruct *)
let check_signatures curmb sl =
@@ -151,7 +157,7 @@ let check_signatures curmb sl =
match sl with
| None -> sl, None
| Some n ->
- if List.length mb >= how_many && CList.skipn how_many mb == curmb
+ if is_nth_suffix how_many mb curmb
then Some (n + how_many), Some mb
else None, None
with CEphemeron.InvalidKey -> None, None in
@@ -185,9 +191,6 @@ let rec unzip ctx j =
| `Cut (n,ty,arg) :: ctx ->
unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
-let hcons_j j =
- { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type}
-
let feedback_completion_typecheck =
let open Feedback in
Option.iter (fun state_id ->
@@ -224,13 +227,13 @@ let infer_declaration ~trust env kn dcl =
let body,env,ectx = skip_trusted_seff valid_signatures body env in
let j = infer env body in
unzip ectx j in
- let j = hcons_j j in
let subst = Univ.LMap.empty in
let _ = judge_of_cast env j DEFAULTcast tyj in
assert (eq_constr typ tyj.utj_val);
+ let c = hcons_constr j.uj_val in
let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in
feedback_completion_typecheck feedback_id;
- j.uj_val, uctx) in
+ c, uctx) in
let def = OpaqueDef (Opaqueproof.create proofterm) in
def, RegularArity typ, None, c.const_entry_polymorphic,
c.const_entry_universes,
@@ -507,7 +510,11 @@ let translate_local_assum env t =
t
let translate_recipe env kn r =
- build_constant_declaration kn env (Cooking.cook_constant env r)
+ (** We only hashcons the term when outside of a section, otherwise this would
+ be useless. It is detected by the dirpath of the constant being empty. *)
+ let (_, dir, _) = Constant.repr3 kn in
+ let hcons = DirPath.is_empty dir in
+ build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
let translate_local_def mb env id centry =
let def,typ,proj,poly,univs,inline_code,ctx =
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 99b763602..1c1ff7e2f 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -92,9 +92,8 @@ let print_backtrace e = match Backtrace.get_backtrace e with
let print_anomaly askreport e =
if askreport then
- hov 0 (raw_anomaly e ++ spc () ++
- strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
- str ".")
+ hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++
+ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
else
hov 0 (raw_anomaly e)
diff --git a/lib/pp.ml b/lib/pp.ml
index 9f33756df..66feae761 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -116,25 +116,6 @@ let strbrk s =
else if p = n then [] else [str (String.sub s p (n-p))]
in Ppcmd_glue (aux 0 0)
-let pr_loc_pos loc =
- if Loc.is_ghost loc then (str"<unknown>")
- else
- let loc = Loc.unloc loc in
- int (fst loc) ++ str"-" ++ int (snd loc)
-
-let pr_loc loc =
- if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
- else
- let fname = loc.Loc.fname in
- if CString.equal fname "" then
- Loc.(str"Toplevel input, characters " ++ int loc.bp ++
- str"-" ++ int loc.ep ++ str":" ++ fnl ())
- else
- Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
- str", line " ++ int loc.line_nb ++ str", characters " ++
- int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
- str":" ++ fnl())
-
let ismt = function | Ppcmd_empty -> true | _ -> false
(* boxing commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 802ffe8e7..7a191b01a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -171,7 +171,6 @@ val surround : std_ppcmds -> std_ppcmds
(** Surround with parenthesis. *)
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-val pr_loc : Loc.t -> std_ppcmds
(** {6 Main renderers, to formatter and to string } *)
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
deleted file mode 100644
index 29ecb94ca..000000000
--- a/plugins/decl_mode/decl_expr.mli
+++ /dev/null
@@ -1,102 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Tacexpr
-
-type 'it statement =
- {st_label:Name.t;
- st_it:'it}
-
-type thesis_kind =
- Plain
- | For of Id.t
-
-type 'this or_thesis =
- This of 'this
- | Thesis of thesis_kind
-
-type side = Lhs | Rhs
-
-type elim_type =
- ET_Case_analysis
- | ET_Induction
-
-type block_type =
- B_proof
- | B_claim
- | B_focus
- | B_elim of elim_type
-
-type ('it,'constr,'tac) cut =
- {cut_stat: 'it;
- cut_by: 'constr list option;
- cut_using: 'tac option}
-
-type ('var,'constr) hyp =
- Hvar of 'var
- | Hprop of 'constr statement
-
-type ('constr,'tac) casee =
- Real of 'constr
- | Virtual of ('constr statement,'constr,'tac) cut
-
-type ('var,'constr,'pat,'tac) bare_proof_instr =
- | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr
- | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr
- | Phence of ('var,'constr,'pat,'tac) bare_proof_instr
- | Pcut of ('constr or_thesis statement,'constr,'tac) cut
- | Prew of side * ('constr statement,'constr,'tac) cut
- | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
- | Passume of ('var,'constr) hyp list
- | Plet of ('var,'constr) hyp list
- | Pgiven of ('var,'constr) hyp list
- | Pconsider of 'constr*('var,'constr) hyp list
- | Pclaim of 'constr statement
- | Pfocus of 'constr statement
- | Pdefine of Id.t * 'var list * 'constr
- | Pcast of Id.t or_thesis * 'constr
- | Psuppose of ('var,'constr) hyp list
- | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list)
- | Ptake of 'constr list
- | Pper of elim_type * ('constr,'tac) casee
- | Pend of block_type
- | Pescape
-
-type emphasis = int
-
-type ('var,'constr,'pat,'tac) gen_proof_instr=
- {emph: emphasis;
- instr: ('var,'constr,'pat,'tac) bare_proof_instr }
-
-
-type raw_proof_instr =
- ((Id.t * (Constrexpr.constr_expr option)) Loc.located,
- Constrexpr.constr_expr,
- Constrexpr.cases_pattern_expr,
- raw_tactic_expr) gen_proof_instr
-
-type glob_proof_instr =
- ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located,
- Tacexpr.glob_constr_and_expr,
- Constrexpr.cases_pattern_expr,
- Tacexpr.glob_tactic_expr) gen_proof_instr
-
-type proof_pattern =
- {pat_vars: Term.types statement list;
- pat_aliases: (Term.constr*Term.types) statement list;
- pat_constr: Term.constr;
- pat_typ: Term.types;
- pat_pat: Glob_term.cases_pattern;
- pat_expr: Constrexpr.cases_pattern_expr}
-
-type proof_instr =
- (Term.constr statement,
- Term.constr,
- proof_pattern,
- Geninterp.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
deleted file mode 100644
index a29480a55..000000000
--- a/plugins/decl_mode/decl_interp.ml
+++ /dev/null
@@ -1,471 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Util
-open Names
-open Constrexpr
-open Tacintern
-open Decl_expr
-open Decl_mode
-open Pretyping
-open Glob_term
-open Term
-open Vars
-open Pp
-open Decl_kinds
-open Misctypes
-
-(* INTERN *)
-
-let glob_app (loc,hd,args) = if List.is_empty args then hd else GApp(loc,hd,args)
-
-let intern_justification_items globs =
- Option.map (List.map (intern_constr globs))
-
-let intern_justification_method globs =
- Option.map (intern_pure_tactic globs)
-
-let intern_statement intern_it globs st =
- {st_label=st.st_label;
- st_it=intern_it globs st.st_it}
-
-let intern_no_bind intern_it globs x =
- globs,intern_it globs x
-
-let intern_constr_or_thesis globs = function
- Thesis n -> Thesis n
- | This c -> This (intern_constr globs c)
-
-let add_var id globs=
- {globs with ltacvars = Id.Set.add id globs.ltacvars}
-
-let add_name nam globs=
- match nam with
- Anonymous -> globs
- | Name id -> add_var id globs
-
-let intern_hyp iconstr globs = function
- Hvar (loc,(id,topt)) -> add_var id globs,
- Hvar (loc,(id,Option.map (intern_constr globs) topt))
- | Hprop st -> add_name st.st_label globs,
- Hprop (intern_statement iconstr globs st)
-
-let intern_hyps iconstr globs hyps =
- snd (List.fold_map (intern_hyp iconstr) globs hyps)
-
-let intern_cut intern_it globs cut=
- let nglobs,nstat=intern_it globs cut.cut_stat in
- {cut_stat=nstat;
- cut_by=intern_justification_items nglobs cut.cut_by;
- cut_using=intern_justification_method nglobs cut.cut_using}
-
-let intern_casee globs = function
- Real c -> Real (intern_constr globs c)
- | Virtual cut -> Virtual
- (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut)
-
-let intern_hyp_list args globs =
- let intern_one globs (loc,(id,opttyp)) =
- (add_var id globs),
- (loc,(id,Option.map (intern_constr globs) opttyp)) in
- List.fold_map intern_one globs args
-
-let intern_suffices_clause globs (hyps,c) =
- let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in
- nglobs,(nhyps,intern_constr_or_thesis nglobs c)
-
-let intern_fundecl args body globs=
- let nglobs,nargs = intern_hyp_list args globs in
- nargs,intern_constr nglobs body
-
-let rec add_vars_of_simple_pattern globs = function
- CPatAlias (loc,p,id) ->
- add_vars_of_simple_pattern (add_var id globs) p
-(* Loc.raise loc
- (UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
- | CPatOr (loc, _)->
- Loc.raise ~loc
- (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
- | CPatDelimiters (_,_,p) ->
- add_vars_of_simple_pattern globs p
- | CPatCstr (_,_,pl1,pl2) ->
- List.fold_left add_vars_of_simple_pattern
- (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2
- | CPatNotation(_,_,(pl,pll),pl') ->
- List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll))
- | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
- | _ -> globs
-
-let rec intern_bare_proof_instr globs = function
- Pthus i -> Pthus (intern_bare_proof_instr globs i)
- | Pthen i -> Pthen (intern_bare_proof_instr globs i)
- | Phence i -> Phence (intern_bare_proof_instr globs i)
- | Pcut c -> Pcut
- (intern_cut
- (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c)
- | Psuffices c ->
- Psuffices (intern_cut intern_suffices_clause globs c)
- | Prew (s,c) -> Prew
- (s,intern_cut
- (intern_no_bind (intern_statement intern_constr)) globs c)
- | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
- | Pcase (params,pat,hyps) ->
- let nglobs,nparams = intern_hyp_list params globs in
- let nnglobs= add_vars_of_simple_pattern nglobs pat in
- let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in
- Pcase (nparams,pat,nhyps)
- | Ptake witl -> Ptake (List.map (intern_constr globs) witl)
- | Pconsider (c,hyps) -> Pconsider (intern_constr globs c,
- intern_hyps intern_constr globs hyps)
- | Pper (et,c) -> Pper (et,intern_casee globs c)
- | Pend bt -> Pend bt
- | Pescape -> Pescape
- | Passume hyps -> Passume (intern_hyps intern_constr globs hyps)
- | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps)
- | Plet hyps -> Plet (intern_hyps intern_constr globs hyps)
- | Pclaim st -> Pclaim (intern_statement intern_constr globs st)
- | Pfocus st -> Pfocus (intern_statement intern_constr globs st)
- | Pdefine (id,args,body) ->
- let nargs,nbody = intern_fundecl args body globs in
- Pdefine (id,nargs,nbody)
- | Pcast (id,typ) ->
- Pcast (id,intern_constr globs typ)
-
-let intern_proof_instr globs instr=
- {emph = instr.emph;
- instr = intern_bare_proof_instr globs instr.instr}
-
-(* INTERP *)
-
-let interp_justification_items env sigma =
- Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c))))
-
-let interp_constr check_sort env sigma c =
- if check_sort then
- fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *))
- else
- fst (understand env sigma (fst c))
-
-let special_whd env =
- let infos=CClosure.create_clos_infos CClosure.all env in
- (fun t -> CClosure.whd_val infos (CClosure.inject t))
-
-let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
-
-let decompose_eq env id =
- let typ = Environ.named_type id env in
- let whd = special_whd env typ in
- match kind_of_term whd with
- App (f,args)->
- if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
- then args.(0)
- else error "Previous step is not an equality."
- | _ -> error "Previous step is not an equality."
-
-let get_eq_typ info env =
- let typ = decompose_eq env (get_last env) in
- typ
-
-let interp_constr_in_type typ env sigma c =
- fst (understand env sigma (fst c) ~expected_type:(OfType (EConstr.of_constr typ)))(*FIXME*)
-
-let interp_statement interp_it env sigma st =
- {st_label=st.st_label;
- st_it=interp_it env sigma st.st_it}
-
-let interp_constr_or_thesis check_sort env sigma = function
- Thesis n -> Thesis n
- | This c -> This (interp_constr check_sort env sigma c)
-
-let abstract_one_hyp inject h glob =
- match h with
- Hvar (loc,(id,None)) ->
- GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
- | Hvar (loc,(id,Some typ)) ->
- GProd (Loc.ghost,Name id, Explicit, fst typ, glob)
- | Hprop st ->
- GProd (Loc.ghost,st.st_label, Explicit, inject st.st_it, glob)
-
-let glob_constr_of_hyps inject hyps head =
- List.fold_right (abstract_one_hyp inject) hyps head
-
-let glob_prop = GSort (Loc.ghost,GProp)
-
-let rec match_hyps blend names constr = function
- [] -> [],substl names constr
- | hyp::q ->
- let (name,typ,body)=destProd constr in
- let st= {st_label=name;st_it=substl names typ} in
- let qnames=
- match name with
- Anonymous -> mkMeta 0 :: names
- | Name id -> mkVar id :: names in
- let qhyp = match hyp with
- Hprop st' -> Hprop (blend st st')
- | Hvar _ -> Hvar st in
- let rhyps,head = match_hyps blend qnames body q in
- qhyp::rhyps,head
-
-let interp_hyps_gen inject blend env sigma hyps head =
- let constr= fst(*FIXME*) (understand env sigma (glob_constr_of_hyps inject hyps head)) in
- match_hyps blend [] constr hyps
-
-let interp_hyps env sigma hyps = fst (interp_hyps_gen fst (fun x _ -> x) env sigma hyps glob_prop)
-
-let dummy_prefix= Id.of_string "__"
-
-let rec deanonymize ids =
- function
- PatVar (loc,Anonymous) ->
- let (found,known) = !ids in
- let new_id=Namegen.next_ident_away dummy_prefix known in
- let _= ids:= (loc,new_id) :: found , new_id :: known in
- PatVar (loc,Name new_id)
- | PatVar (loc,Name id) as pat ->
- let (found,known) = !ids in
- let _= ids:= (loc,id) :: found , known in
- pat
- | PatCstr(loc,cstr,lpat,nam) ->
- PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
-
-let rec glob_of_pat =
- function
- PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable")
- | PatVar (loc,Name id) ->
- GVar (loc,id)
- | PatCstr(loc,((ind,_) as cstr),lpat,_) ->
- let mind= fst (Global.lookup_inductive ind) in
- let rec add_params n q =
- if n<=0 then q else
- add_params (pred n) (GHole(Loc.ghost,
- Evar_kinds.TomatchTypeParameter(ind,n), Misctypes.IntroAnonymous, None)::q) in
- let args = List.map glob_of_pat lpat in
- glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None),
- add_params mind.Declarations.mind_nparams args)
-
-let prod_one_hyp = function
- (loc,(id,None)) ->
- (fun glob ->
- GProd (Loc.ghost,Name id, Explicit,
- GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob))
- | (loc,(id,Some typ)) ->
- (fun glob ->
- GProd (Loc.ghost,Name id, Explicit, fst typ, glob))
-
-let prod_one_id (loc,id) glob =
- GProd (Loc.ghost,Name id, Explicit,
- GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
-
-let let_in_one_alias (id,pat) glob =
- GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob)
-
-let rec bind_primary_aliases map pat =
- match pat with
- PatVar (_,_) -> map
- | PatCstr(loc,_,lpat,nam) ->
- let map1 =
- match nam with
- Anonymous -> map
- | Name id -> (id,pat)::map
- in
- List.fold_left bind_primary_aliases map1 lpat
-
-let bind_secondary_aliases map subst =
- Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map
-
-let bind_aliases patvars subst patt =
- let map = bind_primary_aliases [] patt in
- let map1 = bind_secondary_aliases map subst in
- List.rev map1
-
-let interp_pattern env pat_expr =
- let patvars,pats = Constrintern.intern_pattern env pat_expr in
- match pats with
- [] -> anomaly (Pp.str "empty pattern list")
- | [subst,patt] ->
- (patvars,bind_aliases patvars subst patt,patt)
- | _ -> anomaly (Pp.str "undetected disjunctive pattern")
-
-let rec match_args dest names constr = function
- [] -> [],names,substl names constr
- | _::q ->
- let (name,typ,body)=dest constr in
- let st={st_label=name;st_it=substl names typ} in
- let qnames=
- match name with
- Anonymous -> assert false
- | Name id -> mkVar id :: names in
- let args,bnames,body = match_args dest qnames body q in
- st::args,bnames,body
-
-let rec match_aliases names constr = function
- [] -> [],names,substl names constr
- | _::q ->
- let (name,c,typ,body)=destLetIn constr in
- let st={st_label=name;st_it=(substl names c,substl names typ)} in
- let qnames=
- match name with
- Anonymous -> assert false
- | Name id -> mkVar id :: names in
- let args,bnames,body = match_aliases qnames body q in
- st::args,bnames,body
-
-let detype_ground env c = Detyping.detype false [] env Evd.empty (EConstr.of_constr c)
-
-let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
- let et,pinfo =
- match info.pm_stack with
- Per(et,pi,_,_)::_ -> et,pi
- | _ -> error "No proof per cases/induction/inversion in progress." in
- let mib,oib=Global.lookup_inductive pinfo.per_ind in
- let num_params = pinfo.per_nparams in
- let _ =
- let expected = mib.Declarations.mind_nparams - num_params in
- if not (Int.equal (List.length params) expected) then
- user_err ~hdr:"suppose it is"
- (str "Wrong number of extra arguments: " ++
- (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
- str "expected.") in
- let app_ind =
- let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
- let rparams = List.map (detype_ground env) pinfo.per_params in
- let rparams_rec =
- List.map
- (fun (loc,(id,_)) ->
- GVar (loc,id)) params in
- let dum_args=
- List.init oib.Declarations.mind_nrealargs
- (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),Misctypes.IntroAnonymous, None)) in
- glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
- let pat_vars,aliases,patt = interp_pattern env pat in
- let inject = function
- Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
- | Thesis (For rec_occ) ->
- if not (Id.List.mem rec_occ pat_vars) then
- user_err ~hdr:"suppose it is"
- (str "Variable " ++ Nameops.pr_id rec_occ ++
- str " does not occur in pattern.");
- Glob_term.GSort(Loc.ghost,GProp)
- | This (c,_) -> c in
- let term1 = glob_constr_of_hyps inject hyps glob_prop in
- let loc_ids,npatt =
- let rids=ref ([],pat_vars) in
- let npatt= deanonymize rids patt in
- List.rev (fst !rids),npatt in
- let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in
- let term3=List.fold_right let_in_one_alias aliases term2 in
- let term4=List.fold_right prod_one_id loc_ids term3 in
- let term5=List.fold_right prod_one_hyp params term4 in
- let constr = fst (understand env sigma term5)(*FIXME*) in
- let tparams,nam4,rest4 = match_args destProd [] constr params in
- let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
- let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
- let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
- let blend st st' =
- match st'.st_it with
- Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
- | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
- let thyps = fst (match_hyps blend nam2 (Vars.lift (-1) rest1) hyps) in
- tparams,{pat_vars=tpatvars;
- pat_aliases=taliases;
- pat_constr=pat_pat;
- pat_typ=pat_typ;
- pat_pat=patt;
- pat_expr=pat},thyps
-
-let interp_cut interp_it env sigma cut=
- let nenv,nstat = interp_it env sigma cut.cut_stat in
- { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
- cut_stat=nstat;
- cut_by=interp_justification_items nenv sigma cut.cut_by}
-
-let interp_no_bind interp_it env sigma x =
- env,interp_it env sigma x
-
-let interp_suffices_clause env sigma (hyps,cot)=
- let (locvars,_) as res =
- match cot with
- This (c,_) ->
- let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in
- nhyps,This nc
- | Thesis Plain as th -> interp_hyps env sigma hyps,th
- | Thesis (For n) -> error "\"thesis for\" is not applicable here." in
- let push_one hyp env0 =
- match hyp with
- (Hprop st | Hvar st) ->
- match st.st_label with
- Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0
- | _ -> env in
- let nenv = List.fold_right push_one locvars env in
- nenv,res
-
-let interp_casee env sigma = function
- Real c -> Real (fst (understand env sigma (fst c)))(*FIXME*)
- | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) env sigma cut)
-
-let abstract_one_arg = function
- (loc,(id,None)) ->
- (fun glob ->
- GLambda (Loc.ghost,Name id, Explicit,
- GHole (loc,Evar_kinds.BinderType (Name id),Misctypes.IntroAnonymous,None), glob))
- | (loc,(id,Some typ)) ->
- (fun glob ->
- GLambda (Loc.ghost,Name id, Explicit, fst typ, glob))
-
-let glob_constr_of_fun args body =
- List.fold_right abstract_one_arg args (fst body)
-
-let interp_fun env sigma args body =
- let constr=fst (*FIXME*) (understand env sigma (glob_constr_of_fun args body)) in
- match_args destLambda [] constr args
-
-let rec interp_bare_proof_instr info env sigma = function
- Pthus i -> Pthus (interp_bare_proof_instr info env sigma i)
- | Pthen i -> Pthen (interp_bare_proof_instr info env sigma i)
- | Phence i -> Phence (interp_bare_proof_instr info env sigma i)
- | Pcut c -> Pcut (interp_cut
- (interp_no_bind (interp_statement
- (interp_constr_or_thesis true)))
- env sigma c)
- | Psuffices c ->
- Psuffices (interp_cut interp_suffices_clause env sigma c)
- | Prew (s,c) -> Prew (s,interp_cut
- (interp_no_bind (interp_statement
- (interp_constr_in_type (get_eq_typ info env))))
- env sigma c)
-
- | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps)
- | Pcase (params,pat,hyps) ->
- let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in
- Pcase (tparams,tpat,thyps)
- | Ptake witl ->
- Ptake (List.map (fun c -> fst (*FIXME*) (understand env sigma (fst c))) witl)
- | Pconsider (c,hyps) -> Pconsider (interp_constr false env sigma c,
- interp_hyps env sigma hyps)
- | Pper (et,c) -> Pper (et,interp_casee env sigma c)
- | Pend bt -> Pend bt
- | Pescape -> Pescape
- | Passume hyps -> Passume (interp_hyps env sigma hyps)
- | Pgiven hyps -> Pgiven (interp_hyps env sigma hyps)
- | Plet hyps -> Plet (interp_hyps env sigma hyps)
- | Pclaim st -> Pclaim (interp_statement (interp_constr true) env sigma st)
- | Pfocus st -> Pfocus (interp_statement (interp_constr true) env sigma st)
- | Pdefine (id,args,body) ->
- let nargs,_,nbody = interp_fun env sigma args body in
- Pdefine (id,nargs,nbody)
- | Pcast (id,typ) ->
- Pcast(id,interp_constr true env sigma typ)
-
-let interp_proof_instr info env sigma instr=
- {emph = instr.emph;
- instr = interp_bare_proof_instr info env sigma instr.instr}
-
-
-
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
deleted file mode 100644
index 4303ecdb4..000000000
--- a/plugins/decl_mode/decl_interp.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Tacintern
-open Decl_expr
-
-
-val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
-val interp_proof_instr : Decl_mode.pm_info ->
- Environ.env -> Evd.evar_map -> glob_proof_instr -> proof_instr
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
deleted file mode 100644
index 92d408901..000000000
--- a/plugins/decl_mode/decl_mode.ml
+++ /dev/null
@@ -1,136 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-open CErrors
-open Util
-
-let daimon_flag = ref false
-
-let set_daimon_flag () = daimon_flag:=true
-let clear_daimon_flag () = daimon_flag:=false
-let get_daimon_flag () = !daimon_flag
-
-
-
-
-type split_tree=
- Skip_patt of Id.Set.t * split_tree
- | Split_patt of Id.Set.t * inductive *
- (bool array * (Id.Set.t * split_tree) option) array
- | Close_patt of split_tree
- | End_patt of (Id.t * (int * int))
-
-type elim_kind =
- EK_dep of split_tree
- | EK_nodep
- | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
- {per_casee:constr;
- per_ctype:types;
- per_ind:inductive;
- per_pred:constr;
- per_args:constr list;
- per_params:constr list;
- per_nparams:int;
- per_wf:recpath}
-
-type stack_info =
- Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list
- | Suppose_case
- | Claim
- | Focus_claim
-
-type pm_info =
- { pm_stack : stack_info list}
-let info = Store.field ()
-
-
-(* Current proof mode *)
-
-type command_mode =
- Mode_tactic
- | Mode_proof
- | Mode_none
-
-let mode_of_pftreestate pts =
- (* spiwack: it used to be "top_goal_..." but this should be fine *)
- let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
- let goal = List.hd goals in
- match Store.get (Goal.V82.extra sigma goal) info with
- | None -> Mode_tactic
- | Some _ -> Mode_proof
-
-let get_current_mode () =
- try
- mode_of_pftreestate (Pfedit.get_pftreestate ())
- with Proof_global.NoCurrentProof -> Mode_none
-
-let check_not_proof_mode str =
- match get_current_mode () with
- | Mode_proof -> error str
- | _ -> ()
-
-let get_info sigma gl=
- match Store.get (Goal.V82.extra sigma gl) info with
- | None -> invalid_arg "get_info"
- | Some pm -> pm
-
-let try_get_info sigma gl =
- Store.get (Goal.V82.extra sigma gl) info
-
-let get_goal_stack pts =
- let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
- let info = get_info sigma (List.hd goals) in
- info.pm_stack
-
-
-let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.done_cond proof_focus
-
-let focus p =
- let inf = get_goal_stack p in
- Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
-
-let unfocus () =
- Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
-
-let get_top_stack pts =
- try
- Proof.get_at_focus proof_focus pts
- with Proof.NoSuchFocus ->
- let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
- let info = get_info sigma gl in
- info.pm_stack
-
-let get_stack pts = Proof.get_at_focus proof_focus pts
-
-let get_last env = match Environ.named_context env with
- | decl :: _ -> Context.Named.Declaration.get_id decl
- | [] -> error "no previous statement to use"
-
-
-let get_end_command pts =
- match get_top_stack pts with
- | [] -> "\"end proof\""
- | Claim::_ -> "\"end claim\""
- | Focus_claim::_-> "\"end focus\""
- | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ ->
- begin
- match et with
- Decl_expr.ET_Case_analysis ->
- "\"end cases\" or start a new case"
- | Decl_expr.ET_Induction ->
- "\"end induction\" or start a new case"
- end
- | _ -> anomaly (Pp.str"lonely suppose")
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
deleted file mode 100644
index dfeee833c..000000000
--- a/plugins/decl_mode/decl_mode.mli
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-
-val set_daimon_flag : unit -> unit
-val clear_daimon_flag : unit -> unit
-val get_daimon_flag : unit -> bool
-
-type command_mode =
- Mode_tactic
- | Mode_proof
- | Mode_none
-
-val mode_of_pftreestate : Proof.proof -> command_mode
-
-val get_current_mode : unit -> command_mode
-
-val check_not_proof_mode : string -> unit
-
-type split_tree=
- Skip_patt of Id.Set.t * split_tree
- | Split_patt of Id.Set.t * inductive *
- (bool array * (Id.Set.t * split_tree) option) array
- | Close_patt of split_tree
- | End_patt of (Id.t * (int * int))
-
-type elim_kind =
- EK_dep of split_tree
- | EK_nodep
- | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
- {per_casee:constr;
- per_ctype:types;
- per_ind:inductive;
- per_pred:constr;
- per_args:constr list;
- per_params:constr list;
- per_nparams:int;
- per_wf:recpath}
-
-type stack_info =
- Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list
- | Suppose_case
- | Claim
- | Focus_claim
-
-type pm_info =
- {pm_stack : stack_info list }
-
-val info : pm_info Store.field
-
-val get_info : Evd.evar_map -> Proof_type.goal -> pm_info
-
-val try_get_info : Evd.evar_map -> Proof_type.goal -> pm_info option
-
-val get_stack : Proof.proof -> stack_info list
-
-val get_top_stack : Proof.proof -> stack_info list
-
-val get_last: Environ.env -> Id.t
-(** [get_last] raises a [UserError] when it cannot find a previous
- statement in the environment. *)
-
-val get_end_command : Proof.proof -> string
-
-val focus : Proof.proof -> unit
-
-val unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack
deleted file mode 100644
index 1b84a0790..000000000
--- a/plugins/decl_mode/decl_mode_plugin.mlpack
+++ /dev/null
@@ -1,5 +0,0 @@
-Decl_mode
-Decl_interp
-Decl_proof_instr
-Ppdecl_proof
-G_decl_mode
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
deleted file mode 100644
index 2ea4538c3..000000000
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ /dev/null
@@ -1,1575 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Util
-open Pp
-open Evd
-
-open Tacmach
-open Tacintern
-open Decl_expr
-open Decl_mode
-open Decl_interp
-open Glob_term
-open Glob_ops
-open Names
-open Nameops
-open Declarations
-open Tactics
-open Tacticals
-open Term
-open Vars
-open Termops
-open Namegen
-open Goptions
-open Misctypes
-open Sigma.Notations
-open Context.Named.Declaration
-
-module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
-
-(* Strictness option *)
-
-let clear ids { it = goal; sigma } =
- let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
- let env = Goal.V82.env sigma goal in
- let sign = Goal.V82.hyps sigma goal in
- let cl = Goal.V82.concl sigma goal in
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps, concl) =
- try Evarutil.clear_hyps_in_evi env evdref sign cl ids
- with Evarutil.ClearDependencyError (id, _) ->
- user_err (str "Cannot clear " ++ pr_id id)
- in
- let sigma = !evdref in
- let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
- let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
- { it = [gl]; sigma }
-
-let get_its_info gls = get_info gls.sigma gls.it
-
-let get_strictness,set_strictness =
- let strictness = ref false in
- (fun () -> (!strictness)),(fun b -> strictness:=b)
-
-let _ =
- declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "strict proofs";
- optkey = ["Strict";"Proofs"];
- optread = get_strictness;
- optwrite = set_strictness }
-
-let tcl_change_info_gen info_gen =
- (fun gls ->
- let it = sig_it gls in
- let concl = pf_concl gls in
- let hyps = Goal.V82.hyps (project gls) it in
- let extra = Goal.V82.extra (project gls) it in
- let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
- let sigma = Goal.V82.partial_solution sigma it ev in
- { it = [gl] ; sigma= sigma; } )
-
-let tcl_change_info info gls =
- let info_gen s = Store.set s Decl_mode.info info in
- tcl_change_info_gen info_gen gls
-
-let tcl_erase_info gls =
- let info_gen s = Store.remove s Decl_mode.info in
- tcl_change_info_gen info_gen gls
-
-let special_whd gl=
- let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
- (fun t -> CClosure.whd_val infos (CClosure.inject (EConstr.Unsafe.to_constr t)))
-
-let special_nf gl=
- let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
- (fun t -> CClosure.norm_val infos (CClosure.inject t))
-
-let is_good_inductive env ind =
- let mib,oib = Inductive.lookup_mind_specif env ind in
- Int.equal oib.mind_nrealargs 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
-
-let check_not_per pts =
- if not (Proof.is_done pts) then
- match get_stack pts with
- Per (_,_,_,_)::_ ->
- error "You are inside a proof per cases/induction.\n\
-Please \"suppose\" something or \"end\" it now."
- | _ -> ()
-
-let mk_evd metalist gls =
- let evd0= clear_metas (sig_sig gls) in
- let add_one (meta,typ) evd =
- meta_declare meta typ evd in
- List.fold_right add_one metalist evd0
-
-let is_tmp id = (Id.to_string id).[0] == '_'
-
-let tmp_ids gls =
- let ctx = pf_hyps gls in
- match ctx with
- [] -> []
- | _::q -> List.filter is_tmp (ids_of_named_context q)
-
-let clean_tmp gls =
- let clean_id id0 gls0 =
- tclTRY (clear [id0]) gls0 in
- let rec clean_all = function
- [] -> tclIDTAC
- | id :: rest -> tclTHEN (clean_id id) (clean_all rest)
- in
- clean_all (tmp_ids gls) gls
-
-let assert_postpone id t =
- assert_before (Name id) (EConstr.of_constr t)
-
-(* start a proof *)
-
-
-let start_proof_tac gls=
- let info={pm_stack=[]} in
- tcl_change_info info gls
-
-let go_to_proof_mode () =
- ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac));
- let p = Proof_global.give_me_the_proof () in
- Decl_mode.focus p
-
-(* closing gaps *)
-
-(* spiwack: should use [Proofview.give_up] but that would require
- moving the whole declarative mode into the new proof engine. It
- will eventually have to be done.
-
- As far as I can tell, [daimon_tac] is used after a [thus thesis],
- it will leave uninstantiated variables instead of giving a relevant
- message at [Qed]. *)
-let daimon_tac gls =
- set_daimon_flag ();
- {it=[];sigma=sig_sig gls;}
-
-let daimon_instr env p =
- let (p,(status,_)) =
- Proof.run_tactic env begin
- Proofview.tclINDEPENDENT Proofview.give_up
- end p
- in
- p,status
-
-let do_daimon () =
- let env = Global.env () in
- let status =
- Proof_global.with_current_proof begin fun _ p ->
- daimon_instr env p
- end
- in
- if not status then Feedback.feedback Feedback.AddedAxiom else ()
-
-(* post-instruction focus management *)
-
-let goto_current_focus () =
- Decl_mode.unfocus ()
-
-(* spiwack: used to catch errors indicating lack of "focusing command"
- in the proof tree. In the current implementation, however, entering
- the declarative mode puts a focus first, there should, therefore,
- never be exception raised here. *)
-let goto_current_focus_or_top () =
- goto_current_focus ()
-
-(* return *)
-
-let close_tactic_mode () =
- try do_daimon ();goto_current_focus ()
- with Not_found ->
- error "\"return\" cannot be used outside of Declarative Proof Mode."
-
-let return_from_tactic_mode () =
- close_tactic_mode ()
-
-(* end proof/claim *)
-
-let close_block bt pts =
- if Proof.no_focused_goal pts then
- goto_current_focus ()
- else
- let stack =
- if Proof.is_done pts then
- get_top_stack pts
- else
- get_stack pts
- in
- match bt,stack with
- B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
- do_daimon ();goto_current_focus ()
- | _, Claim::_ ->
- error "\"end claim\" expected."
- | _, Focus_claim::_ ->
- error "\"end focus\" expected."
- | _, [] ->
- error "\"end proof\" expected."
- | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
- begin
- match et with
- ET_Case_analysis -> error "\"end cases\" expected."
- | ET_Induction -> error "\"end induction\" expected."
- end
- | _,_ -> anomaly (Pp.str "Lonely suppose on stack.")
-
-
-(* utility for suppose / suppose it is *)
-
-let close_previous_case pts =
- if
- Proof.is_done pts
- then
- match get_top_stack pts with
- Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
- | Suppose_case :: Per (et,_,_,_) :: _ ->
- goto_current_focus ()
- | _ -> error "Not inside a proof per cases or induction."
- else
- match get_stack pts with
- Per (et,_,_,_) :: _ -> ()
- | Suppose_case :: Per (et,_,_,_) :: _ ->
- do_daimon ();goto_current_focus ()
- | _ -> error "Not inside a proof per cases or induction."
-
-(* Proof instructions *)
-
-(* automation *)
-
-let filter_hyps f gls =
- let filter_aux id =
- let id = NamedDecl.get_id id in
- if f id then
- tclIDTAC
- else
- tclTRY (clear [id]) in
- tclMAP filter_aux (pf_hyps gls) gls
-
-let local_hyp_prefix = Id.of_string "___"
-
-let add_justification_hyps keep items gls =
- let add_aux c gls=
- match kind_of_term c with
- Var id ->
- keep:=Id.Set.add id !keep;
- tclIDTAC gls
- | _ ->
- let id=pf_get_new_id local_hyp_prefix gls in
- keep:=Id.Set.add id !keep;
- let c = EConstr.of_constr c in
- tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
- (Proofview.V82.of_tactic (clear_body [id])) gls in
- tclMAP add_aux items gls
-
-let prepare_goal items gls =
- let tokeep = ref Id.Set.empty in
- let auxres = add_justification_hyps tokeep items gls in
- tclTHENLIST
- [ (fun _ -> auxres);
- filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
-
-let my_automation_tac = ref
- (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
-
-let register_automation_tac tac = my_automation_tac:= tac
-
-let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
-
-let warn_insufficient_justification =
- CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
- (fun () -> strbrk "Insufficient justification.")
-
-let justification tac gls=
- tclORELSE
- (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
- (fun gls ->
- if get_strictness () then
- error "Insufficient justification."
- else
- begin
- warn_insufficient_justification ();
- daimon_tac gls
- end) gls
-
-let default_justification elems gls=
- justification (tclTHEN (prepare_goal elems) (Proofview.V82.of_tactic automation_tac)) gls
-
-(* code for conclusion refining *)
-
-let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s)
-
-let _and = constant ["Init";"Logic"] "and"
-
-let _and_rect = constant ["Init";"Logic"] "and_rect"
-
-let _prod = constant ["Init";"Datatypes"] "prod"
-
-let _prod_rect = constant ["Init";"Datatypes"] "prod_rect"
-
-let _ex = constant ["Init";"Logic"] "ex"
-
-let _ex_ind = constant ["Init";"Logic"] "ex_ind"
-
-let _sig = constant ["Init";"Specif"] "sig"
-
-let _sig_rect = constant ["Init";"Specif"] "sig_rect"
-
-let _sigT = constant ["Init";"Specif"] "sigT"
-
-let _sigT_rect = constant ["Init";"Specif"] "sigT_rect"
-
-type stackd_elt =
-{se_meta:metavariable;
- se_type:types;
- se_last_meta:metavariable;
- se_meta_list:(metavariable*types) list;
- se_evd: evar_map}
-
-let rec replace_in_list m l = function
- [] -> raise Not_found
- | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q
-
-let enstack_subsubgoals env se stack gls=
- let hd,params = decompose_app (special_whd gls (EConstr.of_constr se.se_type)) in
- match kind_of_term hd with
- Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *)
- let mib,oib=
- Inductive.lookup_mind_specif env ind in
- let gentypes=
- Inductive.arities_of_constructors indu (mib,oib) in
- let process i gentyp =
- let constructor = mkConstructU ((ind,succ i),u)
- (* constructors numbering*) in
- let appterm = applist (constructor,params) in
- let apptype = Term.prod_applist gentyp params in
- let rc,_ = Reduction.dest_prod env apptype in
- let rec meta_aux last lenv = function
- [] -> (last,lenv,[])
- | decl::q ->
- let nlast=succ last in
- let (llast,holes,metas) =
- meta_aux nlast (mkMeta nlast :: lenv) q in
- (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in
- let (nlast,holes,nmetas) =
- meta_aux se.se_last_meta [] (List.rev rc) in
- let refiner = applist (appterm,List.rev holes) in
- let evd = meta_assign se.se_meta
- (refiner,(Conv,TypeProcessed (* ? *))) se.se_evd in
- let ncreated = replace_in_list
- se.se_meta nmetas se.se_meta_list in
- let evd0 = List.fold_left
- (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in
- List.iter (fun (m,typ) ->
- Stack.push
- {se_meta=m;
- se_type=typ;
- se_evd=evd0;
- se_meta_list=ncreated;
- se_last_meta=nlast} stack) (List.rev nmetas)
- in
- Array.iteri process gentypes
- | _ -> ()
-
-let nf_meta sigma c =
- EConstr.Unsafe.to_constr (Reductionops.nf_meta sigma (EConstr.of_constr c))
-
-let rec nf_list evd =
- function
- [] -> []
- | (m,typ)::others ->
- if meta_defined evd m then
- nf_list evd others
- else
- (m,nf_meta evd typ)::nf_list evd others
-
-let find_subsubgoal c ctyp skip submetas gls =
- let env= pf_env gls in
- let concl = pf_concl gls in
- let concl = EConstr.Unsafe.to_constr concl in
- let evd = mk_evd ((0,concl)::submetas) gls in
- let stack = Stack.create () in
- let max_meta =
- List.fold_left (fun a (m,_) -> max a m) 0 submetas in
- let _ = Stack.push
- {se_meta=0;
- se_type=concl;
- se_last_meta=max_meta;
- se_meta_list=[0,concl];
- se_evd=evd} stack in
- let rec dfs n =
- let se = Stack.pop stack in
- try
- let unifier =
- Unification.w_unify env se.se_evd Reduction.CUMUL
- ~flags:(Unification.elim_flags ()) ctyp (EConstr.of_constr se.se_type) in
- if n <= 0 then
- {se with
- se_evd=meta_assign se.se_meta
- (c,(Conv,TypeNotProcessed (* ?? *))) unifier;
- se_meta_list=replace_in_list
- se.se_meta submetas se.se_meta_list}
- else
- dfs (pred n)
- with e when CErrors.noncritical e ->
- begin
- enstack_subsubgoals env se stack gls;
- dfs n
- end in
- let nse= try dfs skip with Stack.Empty -> raise Not_found in
- nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0)
-
-let concl_refiner metas body gls =
- let concl = pf_concl gls in
- let evd = sig_sig gls in
- let env = pf_env gls in
- let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
- let concl = EConstr.Unsafe.to_constr concl in
- let rec aux env avoid subst = function
- [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
- | (n,typ)::rest ->
- let _A = subst_meta subst typ in
- let x = id_of_name_using_hdchar env evd (EConstr.of_constr _A) Anonymous in
- let _x = fresh_id avoid x gls in
- let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
- let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
- let nsubst = (n,mkVar _x)::subst in
- if List.is_empty rest then
- asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
- else
- let bsort,_B,nbody =
- aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in
- let body = mkNamedLambda _x _A nbody in
- if local_occur_var evd _x (EConstr.of_constr _B) then
- begin
- let _P = mkNamedLambda _x _A _B in
- match bsort,sort with
- InProp,InProp ->
- let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in
- InProp,_AxB,
- mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|])
- | InProp,_ ->
- let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in
- let _P0 = mkLambda(Anonymous,_AxB,concl) in
- InType,_AxB,
- mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|])
- | _,_ ->
- let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in
- let _P0 = mkLambda(Anonymous,_AxB,concl) in
- InType,_AxB,
- mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|])
- end
- else
- begin
- match asort,bsort with
- InProp,InProp ->
- let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in
- InProp,_AxB,
- mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|])
- |_,_ ->
- let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in
- let _P0 = mkLambda(Anonymous,_AxB,concl) in
- InType,_AxB,
- mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|])
- end
- in
- let (_,_,prf) = aux env [] [] metas in
- mkApp(prf,[|mkMeta 1|])
-
-let thus_tac c ctyp submetas gls =
- let list,proof =
- try
- find_subsubgoal c ctyp 0 submetas gls
- with Not_found ->
- error "I could not relate this statement to the thesis." in
- if List.is_empty list then
- let proof = EConstr.of_constr proof in
- Proofview.V82.of_tactic (exact_check proof) gls
- else
- let refiner = concl_refiner list proof gls in
- Tacmach.refine (EConstr.of_constr refiner) gls
-
-(* general forward step *)
-
-let mk_stat_or_thesis info gls = function
- This c -> c
- | Thesis (For _ ) ->
- error "\"thesis for ...\" is not applicable here."
- | Thesis Plain -> EConstr.Unsafe.to_constr (pf_concl gls)
-
-let just_tac _then cut info gls0 =
- let last_item =
- if _then then
- try [mkVar (get_last (pf_env gls0))]
- with UserError _ ->
- error "\"then\" and \"hence\" require at least one previous fact"
- else []
- in
- let items_tac gls =
- match cut.cut_by with
- None -> tclIDTAC gls
- | Some items -> prepare_goal (last_item@items) gls in
- let method_tac gls =
- match cut.cut_using with
- None ->
- Proofview.V82.of_tactic automation_tac gls
- | Some tac ->
- Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
- justification (tclTHEN items_tac method_tac) gls0
-
-let instr_cut mkstat _thus _then cut gls0 =
- let info = get_its_info gls0 in
- let stat = cut.cut_stat in
- let (c_id,_) = match stat.st_label with
- Anonymous ->
- pf_get_new_id (Id.of_string "_fact") gls0,false
- | Name id -> id,true in
- let c_stat = mkstat info gls0 stat.st_it in
- let thus_tac gls=
- if _thus then
- thus_tac (mkVar c_id) (EConstr.of_constr c_stat) [] gls
- else tclIDTAC gls in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
- [tclTHEN tcl_erase_info (just_tac _then cut info);
- thus_tac] gls0
-
-
-(* iterated equality *)
-let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
-
-let decompose_eq id gls =
- let typ = pf_get_hyp_typ gls id in
- let whd = (special_whd gls typ) in
- match kind_of_term whd with
- App (f,args)->
- if Term.eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
- then (args.(0),
- args.(1),
- args.(2))
- else error "Previous step is not an equality."
- | _ -> error "Previous step is not an equality."
-
-let instr_rew _thus rew_side cut gls0 =
- let last_id =
- try get_last (pf_env gls0)
- with UserError _ -> error "No previous equality."
- in
- let typ,lhs,rhs = decompose_eq last_id gls0 in
- let items_tac gls =
- match cut.cut_by with
- None -> tclIDTAC gls
- | Some items -> prepare_goal items gls in
- let method_tac gls =
- match cut.cut_using with
- None ->
- Proofview.V82.of_tactic automation_tac gls
- | Some tac ->
- Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
- let just_tac gls =
- justification (tclTHEN items_tac method_tac) gls in
- let (c_id,_) = match cut.cut_stat.st_label with
- Anonymous ->
- pf_get_new_id (Id.of_string "_eq") gls0,false
- | Name id -> id,true in
- let thus_tac new_eq gls=
- if _thus then
- thus_tac (mkVar c_id) (EConstr.of_constr new_eq) [] gls
- else tclIDTAC gls in
- match rew_side with
- Lhs ->
- let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
- [tclTHEN tcl_erase_info
- (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr lhs)))
- [just_tac;Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id))]);
- thus_tac new_eq] gls0
- | Rhs ->
- let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
- [tclTHEN tcl_erase_info
- (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr rhs)))
- [Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id));just_tac]);
- thus_tac new_eq] gls0
-
-
-(* tactics for claim/focus *)
-
-let instr_claim _thus st gls0 =
- let info = get_its_info gls0 in
- let (id,_) = match st.st_label with
- Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false
- | Name id -> id,true in
- let thus_tac gls=
- if _thus then
- thus_tac (mkVar id) (EConstr.of_constr st.st_it) [] gls
- else tclIDTAC gls in
- let ninfo1 = {pm_stack=
- (if _thus then Focus_claim else Claim)::info.pm_stack} in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone id st.st_it))
- [thus_tac;
- tcl_change_info ninfo1] gls0
-
-(* tactics for assume *)
-
-let push_intro_tac coerce nam gls =
- let (hid,_) =
- match nam with
- Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false
- | Name id -> id,true in
- tclTHENLIST
- [Proofview.V82.of_tactic (intro_mustbe_force hid);
- coerce hid]
- gls
-
-let assume_tac hyps gls =
- List.fold_right
- (fun (Hvar st | Hprop st) ->
- tclTHEN
- (push_intro_tac
- (fun id ->
- Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) st.st_label))
- hyps tclIDTAC gls
-
-let assume_hyps_or_theses hyps gls =
- List.fold_right
- (function
- (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) ->
- tclTHEN
- (push_intro_tac
- (fun id ->
- Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr c)))) nam)
- | Hprop {st_label=nam;st_it=Thesis (tk)} ->
- tclTHEN
- (push_intro_tac
- (fun id -> tclIDTAC) nam))
- hyps tclIDTAC gls
-
-let assume_st hyps gls =
- List.fold_right
- (fun st ->
- tclTHEN
- (push_intro_tac
- (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it)))) st.st_label))
- hyps tclIDTAC gls
-
-let assume_st_letin hyps gls =
- List.fold_right
- (fun st ->
- tclTHEN
- (push_intro_tac
- (fun id ->
- Proofview.V82.of_tactic (convert_hyp (LocalDef (id, EConstr.of_constr (fst st.st_it), EConstr.of_constr (snd st.st_it))))) st.st_label))
- hyps tclIDTAC gls
-
-(* suffices *)
-
-let rec metas_from n hyps =
- match hyps with
- _ :: q -> n :: metas_from (succ n) q
- | [] -> []
-
-let rec build_product sigma args body =
- match args with
- (Hprop st| Hvar st )::rest ->
- let pprod= lift 1 (build_product sigma rest body) in
- let lbody =
- match st.st_label with
- Anonymous -> pprod
- | Name id -> subst_var id pprod in
- mkProd (st.st_label, st.st_it, lbody)
- | [] -> body
-
-let rec build_applist prod = function
- [] -> [],prod
- | n::q ->
- let (_,typ,_) = destProd prod in
- let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
- (n,typ)::ctx,head
-
-let instr_suffices _then cut gls0 =
- let info = get_its_info gls0 in
- let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
- let ctx,hd = cut.cut_stat in
- let c_stat = build_product (project gls0) ctx (mk_stat_or_thesis info gls0 hd) in
- let metas = metas_from 1 ctx in
- let c_ctx,c_head = build_applist c_stat metas in
- let c_term = applist (mkVar c_id,List.map mkMeta metas) in
- let thus_tac gls=
- thus_tac c_term (EConstr.of_constr c_head) c_ctx gls in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
- [tclTHENLIST
- [ assume_tac ctx;
- tcl_erase_info;
- just_tac _then cut info];
- thus_tac] gls0
-
-(* tactics for consider/given *)
-
-let conjunction_arity id gls =
- let typ = pf_get_hyp_typ gls id in
- let hd,params = decompose_app (special_whd gls typ) in
- let env =pf_env gls in
- match kind_of_term hd with
- Ind (ind,u as indu) when is_good_inductive env ind ->
- let mib,oib=
- Inductive.lookup_mind_specif env ind in
- let gentypes=
- Inductive.arities_of_constructors indu (mib,oib) in
- let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in
- let apptype = Term.prod_applist gentypes.(0) params in
- let rc,_ = Reduction.dest_prod env apptype in
- List.length rc
- | _ -> raise Not_found
-
-let rec intron_then n ids ltac gls =
- if n<=0 then
- ltac ids gls
- else
- let id = pf_get_new_id (Id.of_string "_tmp") gls in
- tclTHEN
- (Proofview.V82.of_tactic (intro_mustbe_force id))
- (intron_then (pred n) (id::ids) ltac) gls
-
-
-let rec consider_match may_intro introduced available expected gls =
- match available,expected with
- [],[] ->
- tclIDTAC gls
- | _,[] -> error "Last statements do not match a complete hypothesis."
- (* should tell which ones *)
- | [],hyps ->
- if may_intro then
- begin
- let id = pf_get_new_id (Id.of_string "_tmp") gls in
- tclIFTHENELSE
- (Proofview.V82.of_tactic (intro_mustbe_force id))
- (consider_match true [] [id] hyps)
- (fun _ ->
- error "Not enough sub-hypotheses to match statements.")
- gls
- end
- else
- error "Not enough sub-hypotheses to match statements."
- (* should tell which ones *)
- | id::rest_ids,(Hvar st | Hprop st)::rest ->
- tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it))))
- begin
- match st.st_label with
- Anonymous ->
- consider_match may_intro ((id,false)::introduced) rest_ids rest
- | Name hid ->
- tclTHENLIST
- [Proofview.V82.of_tactic (rename_hyp [id,hid]);
- consider_match may_intro ((hid,true)::introduced) rest_ids rest]
- end
- begin
- (fun gls ->
- let nhyps =
- try conjunction_arity id gls with
- Not_found -> error "Matching hypothesis not found." in
- tclTHENLIST
- [Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id));
- intron_then nhyps []
- (fun l -> consider_match may_intro introduced
- (List.rev_append l rest_ids) expected)] gls)
- end
- gls
-
-let consider_tac c hyps gls =
- let c = EConstr.of_constr c in
- match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with
- Var id ->
- consider_match false [] [id] hyps gls
- | _ ->
- let id = pf_get_new_id (Id.of_string "_tmp") gls in
- tclTHEN
- (Proofview.V82.of_tactic (pose_proof (Name id) c))
- (consider_match false [] [id] hyps) gls
-
-
-let given_tac hyps gls =
- consider_match true [] [] hyps gls
-
-(* tactics for take *)
-
-let rec take_tac wits gls =
- match wits with
- [] -> tclIDTAC gls
- | wit::rest ->
- let typ = pf_unsafe_type_of gls (EConstr.of_constr wit) in
- tclTHEN (thus_tac wit typ []) (take_tac rest) gls
-
-
-(* tactics for define *)
-
-let subst_term sigma c t =
- EConstr.Unsafe.to_constr (subst_term sigma c t)
-
-let rec build_function sigma args body =
- match args with
- st::rest ->
- let pfun= lift 1 (build_function sigma rest body) in
- let id = match st.st_label with
- Anonymous -> assert false
- | Name id -> id in
- mkLambda (Name id, st.st_it, subst_term sigma (EConstr.mkVar id) (EConstr.of_constr pfun))
- | [] -> body
-
-let define_tac id args body gls =
- let t = build_function (project gls) args body in
- let t = EConstr.of_constr t in
- Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls
-
-(* tactics for reconsider *)
-
-let cast_tac id_or_thesis typ gls =
- let typ = EConstr.of_constr typ in
- match id_or_thesis with
- | This id ->
- Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
- | Thesis (For _ ) ->
- error "\"thesis for ...\" is not applicable here."
- | Thesis Plain ->
- Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls
-
-(* per cases *)
-
-let is_rec_pos (main_ind,wft) =
- match main_ind with
- None -> false
- | Some index ->
- match fst (Rtree.dest_node wft) with
- Mrec (_,i) when Int.equal i index -> true
- | _ -> false
-
-let rec constr_trees (main_ind,wft) ind =
- match Rtree.dest_node wft with
- Norec,_ ->
- let itree =
- (snd (Global.lookup_inductive ind)).mind_recargs in
- constr_trees (None,itree) ind
- | _,constrs -> main_ind,constrs
-
-let ind_args rp ind =
- let main_ind,constrs = constr_trees rp ind in
- let args ctree =
- Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in
- Array.map args constrs
-
-let init_tree ids ind rp nexti =
- let indargs = ind_args rp ind in
- let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in
- Split_patt (ids,ind,Array.mapi do_i indargs)
-
-let map_tree_rp rp id_fun mapi = function
- Split_patt (ids,ind,branches) ->
- let indargs = ind_args rp ind in
- let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in
- Split_patt (id_fun ids,ind,Array.mapi do_i branches)
- | _ -> failwith "map_tree_rp: not a splitting node"
-
-let map_tree id_fun mapi = function
- Split_patt (ids,ind,branches) ->
- let do_i i (recargs,bri) = recargs,mapi i bri in
- Split_patt (id_fun ids,ind,Array.mapi do_i branches)
- | _ -> failwith "map_tree: not a splitting node"
-
-
-let start_tree env ind rp =
- init_tree Id.Set.empty ind rp (fun _ _ -> None)
-
-let build_per_info etype casee gls =
- let concl=pf_concl gls in
- let env=pf_env gls in
- let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
- let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in
- let hd,args = decompose_app (special_whd gls ctyp) in
- let (ind,u) =
- try
- destInd hd
- with DestKO ->
- error "Case analysis must be done on an inductive object." in
- let mind,oind = Global.lookup_inductive ind in
- let nparams,index =
- match etype with
- ET_Induction -> mind.mind_nparams_rec,Some (snd ind)
- | _ -> mind.mind_nparams,None in
- let params,real_args = List.chop nparams args in
- let abstract_obj c body =
- let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
- lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
- let pred= List.fold_right abstract_obj
- real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
- let ctyp = EConstr.Unsafe.to_constr ctyp in
- let pred = EConstr.Unsafe.to_constr pred in
- is_dep,
- {per_casee=casee;
- per_ctype=ctyp;
- per_ind=ind;
- per_pred=pred;
- per_args=real_args;
- per_params=params;
- per_nparams=nparams;
- per_wf=index,oind.mind_recargs}
-
-let per_tac etype casee gls=
- let env=pf_env gls in
- let info = get_its_info gls in
- match casee with
- Real c ->
- let is_dep,per_info = build_per_info etype c gls in
- let ek =
- if is_dep then
- EK_dep (start_tree env per_info.per_ind per_info.per_wf)
- else EK_unknown in
- tcl_change_info
- {pm_stack=
- Per(etype,per_info,ek,[])::info.pm_stack} gls
- | Virtual cut ->
- assert (cut.cut_stat.st_label == Anonymous);
- let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in
- let c = mkVar id in
- let modified_cut =
- {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
- tclTHEN
- (instr_cut (fun _ _ c -> c) false false modified_cut)
- (fun gls0 ->
- let is_dep,per_info = build_per_info etype c gls0 in
- assert (not is_dep);
- tcl_change_info
- {pm_stack=
- Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
- gls
-
-(* suppose *)
-
-let register_nodep_subcase id= function
- Per(et,pi,ek,clauses)::s ->
- begin
- match ek with
- EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
- | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
- | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"."
- end
- | _ -> anomaly (Pp.str "wrong stack state")
-
-let suppose_tac hyps gls0 =
- let info = get_its_info gls0 in
- let thesis = pf_concl gls0 in
- let thesis = EConstr.Unsafe.to_constr thesis in
- let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
- let clause = build_product (project gls0) hyps thesis in
- let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
- let old_clauses,stack = register_nodep_subcase id info.pm_stack in
- let ninfo2 = {pm_stack=stack} in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause))
- [tclTHENLIST [tcl_change_info ninfo1;
- assume_tac hyps;
- clear old_clauses];
- tcl_change_info ninfo2] gls0
-
-(* suppose it is ... *)
-
-(* pattern matching compiling *)
-
-let rec skip_args rest ids n =
- if n <= 0 then
- Close_patt rest
- else
- Skip_patt (ids,skip_args rest ids (pred n))
-
-let rec tree_of_pats ((id,_) as cpl) pats =
- match pats with
- [] -> End_patt cpl
- | args::stack ->
- match args with
- [] -> Close_patt (tree_of_pats cpl stack)
- | (patt,rp) :: rest_args ->
- match patt with
- PatVar (_,v) ->
- Skip_patt (Id.Set.singleton id,
- tree_of_pats cpl (rest_args::stack))
- | PatCstr (_,(ind,cnum),args,nam) ->
- let nexti i ati =
- if Int.equal i (pred cnum) then
- let nargs =
- List.map_i (fun j a -> (a,ati.(j))) 0 args in
- Some (Id.Set.singleton id,
- tree_of_pats cpl (nargs::rest_args::stack))
- else None
- in init_tree Id.Set.empty ind rp nexti
-
-let rec add_branch ((id,_) as cpl) pats tree=
- match pats with
- [] ->
- begin
- match tree with
- End_patt cpl0 -> End_patt cpl0
- (* this ensures precedence for overlapping patterns *)
- | _ -> anomaly (Pp.str "tree is expected to end here")
- end
- | args::stack ->
- match args with
- [] ->
- begin
- match tree with
- Close_patt t ->
- Close_patt (add_branch cpl stack t)
- | _ -> anomaly (Pp.str "we should pop here")
- end
- | (patt,rp) :: rest_args ->
- match patt with
- PatVar (_,v) ->
- begin
- match tree with
- Skip_patt (ids,t) ->
- Skip_patt (Id.Set.add id ids,
- add_branch cpl (rest_args::stack) t)
- | Split_patt (_,_,_) ->
- map_tree (Id.Set.add id)
- (fun i bri ->
- append_branch cpl 1 (rest_args::stack) bri)
- tree
- | _ -> anomaly (Pp.str "No pop/stop expected here")
- end
- | PatCstr (_,(ind,cnum),args,nam) ->
- match tree with
- Skip_patt (ids,t) ->
- let nexti i ati =
- if Int.equal i (pred cnum) then
- let nargs =
- List.map_i (fun j a -> (a,ati.(j))) 0 args in
- Some (Id.Set.add id ids,
- add_branch cpl (nargs::rest_args::stack)
- (skip_args t ids (Array.length ati)))
- else
- Some (ids,
- skip_args t ids (Array.length ati))
- in init_tree ids ind rp nexti
- | Split_patt (_,ind0,_) ->
- if (not (eq_ind ind ind0)) then error
- (* this can happen with coercions *)
- "Case pattern belongs to wrong inductive type.";
- let mapi i ati bri =
- if Int.equal i (pred cnum) then
- let nargs =
- List.map_i (fun j a -> (a,ati.(j))) 0 args in
- append_branch cpl 0
- (nargs::rest_args::stack) bri
- else bri in
- map_tree_rp rp (fun ids -> ids) mapi tree
- | _ -> anomaly (Pp.str "No pop/stop expected here")
-and append_branch ((id,_) as cpl) depth pats = function
- Some (ids,tree) ->
- Some (Id.Set.add id ids,append_tree cpl depth pats tree)
- | None ->
- Some (Id.Set.singleton id,tree_of_pats cpl pats)
-and append_tree ((id,_) as cpl) depth pats tree =
- if depth<=0 then add_branch cpl pats tree
- else match tree with
- Close_patt t ->
- Close_patt (append_tree cpl (pred depth) pats t)
- | Skip_patt (ids,t) ->
- Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t)
- | End_patt _ -> anomaly (Pp.str "Premature end of branch")
- | Split_patt (_,_,_) ->
- map_tree (Id.Set.add id)
- (fun i bri -> append_branch cpl (succ depth) pats bri) tree
-
-(* suppose it is *)
-
-let rec st_assoc id = function
- [] -> raise Not_found
- | st::_ when Name.equal st.st_label id -> st.st_it
- | _ :: rest -> st_assoc id rest
-
-let thesis_for obj typ per_info env=
- let rc,hd1=decompose_prod typ in
- let cind,all_args=decompose_app typ in
- let ind,u = destInd cind in
- let _ = if not (eq_ind ind per_info.per_ind) then
- user_err ~hdr:"thesis_for"
- ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
- str"cannot give an induction hypothesis (wrong inductive type).") in
- let params,args = List.chop per_info.per_nparams all_args in
- let _ = if not (List.for_all2 Term.eq_constr params per_info.per_params) then
- user_err ~hdr:"thesis_for"
- ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
- str "cannot give an induction hypothesis (wrong parameters).") in
- let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
- compose_prod rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2)))
-
-let rec build_product_dep pat_info per_info args body gls =
- match args with
- (Hprop {st_label=nam;st_it=This c}
- | Hvar {st_label=nam;st_it=c})::rest ->
- let pprod=
- lift 1 (build_product_dep pat_info per_info rest body gls) in
- let lbody =
- match nam with
- Anonymous -> body
- | Name id -> subst_var id pprod in
- mkProd (nam,c,lbody)
- | Hprop ({st_it=Thesis tk} as st)::rest ->
- let pprod=
- lift 1 (build_product_dep pat_info per_info rest body gls) in
- let lbody =
- match st.st_label with
- Anonymous -> body
- | Name id -> subst_var id pprod in
- let ptyp =
- match tk with
- For id ->
- let obj = mkVar id in
- let typ =
- try st_assoc (Name id) pat_info.pat_vars
- with Not_found ->
- snd (st_assoc (Name id) pat_info.pat_aliases) in
- thesis_for obj typ per_info (pf_env gls)
- | Plain -> EConstr.Unsafe.to_constr (pf_concl gls) in
- mkProd (st.st_label,ptyp,lbody)
- | [] -> body
-
-let build_dep_clause params pat_info per_info hyps gls =
- let concl=
- thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in
- let open_clause =
- build_product_dep pat_info per_info hyps concl gls in
- let prod_one st body =
- match st.st_label with
- Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body)
- | Name id -> mkNamedProd id st.st_it (lift 1 body) in
- let let_one_in st body =
- match st.st_label with
- Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body)
- | Name id ->
- mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in
- let aliased_clause =
- List.fold_right let_one_in pat_info.pat_aliases open_clause in
- List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause
-
-let rec register_dep_subcase id env per_info pat = function
- EK_nodep -> error "Only \"suppose it is\" can be used here."
- | EK_unknown ->
- register_dep_subcase id env per_info pat
- (EK_dep (start_tree env per_info.per_ind per_info.per_wf))
- | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
-
-let case_tac params pat_info hyps gls0 =
- let info = get_its_info gls0 in
- let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
- let et,per_info,ek,old_clauses,rest =
- match info.pm_stack with
- Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest)
- | _ -> anomaly (Pp.str "wrong place for cases") in
- let clause = build_dep_clause params pat_info per_info hyps gls0 in
- let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
- let nek =
- register_dep_subcase (id,(List.length params,List.length hyps))
- (pf_env gls0) per_info pat_info.pat_pat ek in
- let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause))
- [tclTHENLIST
- [tcl_change_info ninfo1;
- assume_st (params@pat_info.pat_vars);
- assume_st_letin pat_info.pat_aliases;
- assume_hyps_or_theses hyps;
- clear old_clauses];
- tcl_change_info ninfo2] gls0
-
-(* end cases *)
-
-type ('a, 'b) instance_stack =
- ('b * (('a option * constr list) list)) list
-
-let initial_instance_stack ids : (_, _) instance_stack =
- List.map (fun id -> id,[None,[]]) ids
-
-let push_one_arg arg = function
- [] -> anomaly (Pp.str "impossible")
- | (head,args) :: ctx ->
- ((head,(arg::args)) :: ctx)
-
-let push_arg arg stacks =
- List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks
-
-
-let push_one_head c ids (id,stack) =
- let head = if Id.Set.mem id ids then Some c else None in
- id,(head,[]) :: stack
-
-let push_head c ids stacks =
- List.map (push_one_head c ids) stacks
-
-let pop_one (id,stack) =
- let nstack=
- match stack with
- [] -> anomaly (Pp.str "impossible")
- | [c] as l -> l
- | (Some head,args)::(head0,args0)::ctx ->
- let arg = applist (head,(List.rev args)) in
- (head0,(arg::args0))::ctx
- | (None,args)::(head0,args0)::ctx ->
- (head0,(args@args0))::ctx
- in id,nstack
-
-let pop_stacks stacks =
- List.map pop_one stacks
-
-let hrec_for fix_id per_info gls obj_id =
- let obj=mkVar obj_id in
- let typ=pf_get_hyp_typ gls obj_id in
- let typ = EConstr.Unsafe.to_constr typ in
- let rc,hd1=decompose_prod typ in
- let cind,all_args=decompose_app typ in
- let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
- let params,args= List.chop per_info.per_nparams all_args in
- assert begin
- try List.for_all2 Term.eq_constr params per_info.per_params with
- Invalid_argument _ -> false end;
- let hd2 = applist (mkVar fix_id,args@[obj]) in
- EConstr.of_constr (compose_lam rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2))))
-
-let warn_missing_case =
- CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
- (fun () -> strbrk "missing case")
-
-let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
- match tree, objs with
- Close_patt t,_ ->
- let args0 = pop_stacks args in
- execute_cases fix_name per_info tacnext args0 objs nhrec t gls
- | Skip_patt (_,t),skipped::next_objs ->
- let args0 = push_arg skipped args in
- execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
- | End_patt (id,(nparams,nhyps)),[] ->
- begin
- match Id.List.assoc id args with
- [None,br_args] ->
- let all_metas =
- List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in
- let param_metas,hyp_metas = List.chop nparams all_metas in
- tclTHEN
- (tclDO nhrec (Proofview.V82.of_tactic introf))
- (tacnext
- (applist (mkVar id,
- List.append param_metas
- (List.rev_append br_args hyp_metas)))) gls
- | _ -> anomaly (Pp.str "wrong stack size")
- end
- | Split_patt (ids,ind,br), casee::next_objs ->
- let (mind,oind) as spec = Global.lookup_inductive ind in
- let nparams = mind.mind_nparams in
- let concl=pf_concl gls in
- let env=pf_env gls in
- let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
- let hd,all_args = decompose_app (special_whd gls ctyp) in
- let ind', u = destInd hd in
- let _ = assert (eq_ind ind' ind) in (* just in case *)
- let params,real_args = List.chop nparams all_args in
- let abstract_obj c body =
- let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
- lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
- let elim_pred = List.fold_right abstract_obj
- real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
- let elim_pred = EConstr.Unsafe.to_constr elim_pred in
- let case_info = Inductiveops.make_case_info env ind RegularStyle in
- let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
- let f_ids typ =
- let sign =
- (prod_assum (Term.prod_applist typ params)) in
- let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
- find_intro_names sign gls in
- let constr_args_ids = Array.map f_ids gen_arities in
- let case_term =
- mkCase(case_info,elim_pred,casee,
- Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in
- let branch_tac i (recargs,bro) gls0 =
- let args_ids = constr_args_ids.(i) in
- let rec aux n = function
- [] ->
- assert (Int.equal n (Array.length recargs));
- next_objs,[],nhrec
- | id :: q ->
- let objs,recs,nrec = aux (succ n) q in
- if recargs.(n)
- then (mkVar id::objs),(id::recs),succ nrec
- else (mkVar id::objs),recs,nrec in
- let objs,recs,nhrec = aux 0 args_ids in
- tclTHENLIST
- [tclMAP (fun id -> Proofview.V82.of_tactic (intro_mustbe_force id)) args_ids;
- begin
- fun gls1 ->
- let hrecs =
- List.map
- (fun id ->
- hrec_for (out_name fix_name) per_info gls1 id)
- recs in
- Proofview.V82.of_tactic (generalize hrecs) gls1
- end;
- match bro with
- None ->
- warn_missing_case ();
- tacnext (mkMeta 1)
- | Some (sub_ids,tree) ->
- let br_args =
- List.filter
- (fun (id,_) -> Id.Set.mem id sub_ids) args in
- let construct =
- applist (mkConstruct(ind,succ i),params) in
- let p_args =
- push_head construct ids br_args in
- execute_cases fix_name per_info tacnext
- p_args objs nhrec tree] gls0 in
- tclTHENSV
- (refine (EConstr.of_constr case_term))
- (Array.mapi branch_tac br) gls
- | Split_patt (_, _, _) , [] ->
- anomaly ~label:"execute_cases " (Pp.str "Nothing to split")
- | Skip_patt _ , [] ->
- anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
- | End_patt (_,_) , _ :: _ ->
- anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
-
-let understand_my_constr env sigma c concl =
- let env = env in
- let c = EConstr.of_constr c in
- let rawc = Detyping.detype false [] env Evd.empty c in
- let rec frob = function
- | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
- | rc -> map_glob_constr frob rc
- in
- Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
-
-let my_refine c gls =
- let oc = { run = begin fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
- Sigma.Unsafe.of_pair (c, sigma)
- end } in
- Proofview.V82.of_tactic (Tactics.New.refine oc) gls
-
-(* end focus/claim *)
-
-let end_tac et2 gls =
- let info = get_its_info gls in
- let et1,pi,ek,clauses =
- match info.pm_stack with
- Suppose_case::_ ->
- anomaly (Pp.str "This case should already be trapped")
- | Claim::_ ->
- error "\"end claim\" expected."
- | Focus_claim::_ ->
- error "\"end focus\" expected."
- | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses)
- | [] ->
- anomaly (Pp.str "This case should already be trapped") in
- let et = match et1, et2 with
- | ET_Case_analysis, ET_Case_analysis -> et1
- | ET_Induction, ET_Induction -> et1
- | ET_Case_analysis, _ -> error "\"end cases\" expected."
- | ET_Induction, _ -> error "\"end induction\" expected."
- in
- tclTHEN
- tcl_erase_info
- begin
- match et,ek with
- _,EK_unknown ->
- tclSOLVE [Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr pi.per_casee))]
- | ET_Case_analysis,EK_nodep ->
- tclTHEN
- (Proofview.V82.of_tactic (simplest_case (EConstr.of_constr pi.per_casee)))
- (default_justification (List.map mkVar clauses))
- | ET_Induction,EK_nodep ->
- tclTHENLIST
- [Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee])));
- Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
- default_justification (List.map mkVar clauses)]
- | ET_Case_analysis,EK_dep tree ->
- execute_cases Anonymous pi
- (fun c -> tclTHENLIST
- [my_refine c;
- clear clauses;
- justification (Proofview.V82.of_tactic assumption)])
- (initial_instance_stack clauses) [pi.per_casee] 0 tree
- | ET_Induction,EK_dep tree ->
- let nargs = (List.length pi.per_args) in
- tclTHEN (Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee]))))
- begin
- fun gls0 ->
- let fix_id =
- pf_get_new_id (Id.of_string "_fix") gls0 in
- let c_id =
- pf_get_new_id (Id.of_string "_main_arg") gls0 in
- tclTHENLIST
- [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
- tclDO nargs (Proofview.V82.of_tactic introf);
- Proofview.V82.of_tactic (intro_mustbe_force c_id);
- execute_cases (Name fix_id) pi
- (fun c ->
- tclTHENLIST
- [clear [fix_id];
- my_refine c;
- clear clauses;
- justification (Proofview.V82.of_tactic assumption)])
- (initial_instance_stack clauses)
- [mkVar c_id] 0 tree] gls0
- end
- end gls
-
-(* escape *)
-
-let escape_tac gls =
- (* spiwack: sets an empty info stack to avoid interferences.
- We could erase the info altogether, but that doesn't play
- well with the Decl_mode.focus (used in post_processing). *)
- let info={pm_stack=[]} in
- tcl_change_info info gls
-
-(* General instruction engine *)
-
-let rec do_proof_instr_gen _thus _then instr =
- match instr with
- Pthus i ->
- assert (not _thus);
- do_proof_instr_gen true _then i
- | Pthen i ->
- assert (not _then);
- do_proof_instr_gen _thus true i
- | Phence i ->
- assert (not (_then || _thus));
- do_proof_instr_gen true true i
- | Pcut c ->
- instr_cut mk_stat_or_thesis _thus _then c
- | Psuffices c ->
- instr_suffices _then c
- | Prew (s,c) ->
- assert (not _then);
- instr_rew _thus s c
- | Pconsider (c,hyps) -> consider_tac c hyps
- | Pgiven hyps -> given_tac hyps
- | Passume hyps -> assume_tac hyps
- | Plet hyps -> assume_tac hyps
- | Pclaim st -> instr_claim false st
- | Pfocus st -> instr_claim true st
- | Ptake witl -> take_tac witl
- | Pdefine (id,args,body) -> define_tac id args body
- | Pcast (id,typ) -> cast_tac id typ
- | Pper (et,cs) -> per_tac et cs
- | Psuppose hyps -> suppose_tac hyps
- | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
- | Pend (B_elim et) -> end_tac et
- | Pend _ -> anomaly (Pp.str "Not applicable")
- | Pescape -> escape_tac
-
-let eval_instr {instr=instr} =
- do_proof_instr_gen false false instr
-
-let rec preprocess pts instr =
- match instr with
- Phence i |Pthus i | Pthen i -> preprocess pts i
- | Psuffices _ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _
- | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _
- | Pdefine (_,_,_) | Pper _ | Prew _ ->
- check_not_per pts;
- true
- | Pescape ->
- check_not_per pts;
- true
- | Pcase _ | Psuppose _ | Pend (B_elim _) ->
- close_previous_case pts ;
- true
- | Pend bt ->
- close_block bt pts ;
- false
-
-let rec postprocess pts instr =
- match instr with
- Phence i | Pthus i | Pthen i -> postprocess pts i
- | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
- | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> ()
- | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ ->
- Decl_mode.focus pts
- | Pescape ->
- Decl_mode.focus pts;
- Proof_global.set_proof_mode "Classic"
- | Pend (B_elim ET_Induction) ->
- begin
- let pfterm = List.hd (Proof.partial_proof pts) in
- let pfterm = EConstr.Unsafe.to_constr pfterm in
- let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in
- let env = try
- Goal.V82.env sigma (List.hd gls)
- with Failure "hd" ->
- Global.env ()
- in
- try
- Inductiveops.control_only_guard env pfterm;
- goto_current_focus_or_top ()
- with
- Type_errors.TypeError(env,
- Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
- anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
- end
- | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
- | Pend B_proof -> Proof_global.set_proof_mode "Classic"
- | Pend _ -> ()
-
-let do_instr raw_instr pts =
- let has_tactic = preprocess pts raw_instr.instr in
- (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
- current proof (and, actually so does [do_instr] later one, so
- it's ok to do the same here. Ideally the proof should be properly
- threaded through the commands here, but since the are interleaved
- with actions on the proof mode, which is attached to the global
- proof environment, it is not possible without heavy lifting. *)
- let pts = Proof_global.give_me_the_proof () in
- let pts =
- if has_tactic then
- let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
- let gl = { it=List.hd gls ; sigma=sigma; } in
- let env= pf_env gl in
- let ist = {ltacvars = Id.Set.empty; genv = env} in
- let glob_instr = intern_proof_instr ist raw_instr in
- let instr =
- interp_proof_instr (get_its_info gl) env sigma glob_instr in
- let (pts',_) = Proof.run_tactic (Global.env())
- (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
- pts'
- else pts
- in
- Proof_global.simple_with_current_proof (fun _ _ -> pts);
- postprocess pts raw_instr.instr
-
-let proof_instr raw_instr =
- let p = Proof_global.give_me_the_proof () in
- do_instr raw_instr p
-
-(*
-
-(* STUFF FOR ITERATED RELATIONS *)
-let decompose_bin_app t=
- let hd,args = destApp
-
-let identify_transitivity_lemma c =
- let varx,tx,c1 = destProd c in
- let vary,ty,c2 = destProd (pop c1) in
- let varz,tz,c3 = destProd (pop c2) in
- let _,p1,c4 = destProd (pop c3) in
- let _,lp2,lp3 = destProd (pop c4) in
- let p2=pop lp2 in
- let p3=pop lp3 in
-*)
-
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
deleted file mode 100644
index ba196ff01..000000000
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ /dev/null
@@ -1,108 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Tacmach
-open Decl_mode
-
-val go_to_proof_mode: unit -> unit
-val return_from_tactic_mode: unit -> unit
-
-val register_automation_tac: unit Proofview.tactic -> unit
-
-val automation_tac : unit Proofview.tactic
-
-val concl_refiner:
- Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
-
-val do_instr: Decl_expr.raw_proof_instr -> Proof.proof -> unit
-val proof_instr: Decl_expr.raw_proof_instr -> unit
-
-val tcl_change_info : Decl_mode.pm_info -> tactic
-
-val execute_cases :
- Name.t ->
- Decl_mode.per_info ->
- (Term.constr -> Proof_type.tactic) ->
- (Id.Set.elt * (Term.constr option * Term.constr list) list) list ->
- Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
-
-val tree_of_pats :
- Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
- split_tree
-
-val add_branch :
- Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
- split_tree -> split_tree
-
-val append_branch :
- Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
- (Id.Set.t * Decl_mode.split_tree) option ->
- (Id.Set.t * Decl_mode.split_tree) option
-
-val append_tree :
- Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
- split_tree -> split_tree
-
-val build_dep_clause : Term.types Decl_expr.statement list ->
- Decl_expr.proof_pattern ->
- Decl_mode.per_info ->
- (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis)
- Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
-
-val register_dep_subcase :
- Id.t * (int * int) ->
- Environ.env ->
- Decl_mode.per_info ->
- Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
-
-val thesis_for : Term.constr ->
- Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr
-
-val close_previous_case : Proof.proof -> unit
-
-val pop_stacks :
- (Id.t *
- (Term.constr option * Term.constr list) list) list ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list
-
-val push_head : Term.constr ->
- Id.Set.t ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list
-
-val push_arg : Term.constr ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list
-
-val hrec_for:
- Id.t ->
- Decl_mode.per_info -> Proof_type.goal Tacmach.sigma ->
- Id.t -> EConstr.constr
-
-val consider_match :
- bool ->
- (Id.Set.elt*bool) list ->
- Id.Set.elt list ->
- (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
- Proof_type.tactic
-
-val init_tree:
- Id.Set.t ->
- inductive ->
- int option * Declarations.wf_paths ->
- (int ->
- (int option * Declarations.recarg Rtree.t) array ->
- (Id.Set.t * Decl_mode.split_tree) option) ->
- Decl_mode.split_tree
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
deleted file mode 100644
index a71d20f0d..000000000
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ /dev/null
@@ -1,387 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-DECLARE PLUGIN "decl_mode_plugin"
-
-open Ltac_plugin
-open Compat
-open Pp
-open Decl_expr
-open Names
-open Pcoq
-open Vernacexpr
-open Tok (* necessary for camlp4 *)
-
-open Pcoq.Constr
-open Pltac
-open Ppdecl_proof
-
-let pr_goal gs =
- let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
- let env = Goal.V82.env sigma g in
- let concl = Goal.V82.concl sigma g in
- let goal =
- Printer.pr_context_of env sigma ++ cut () ++
- str "============================" ++ cut () ++
- str "thesis :=" ++ cut () ++
- Printer.pr_goal_concl_style_env env sigma concl in
- str " *** Declarative Mode ***" ++ fnl () ++ fnl () ++
- str " " ++ v 0 goal
-
-let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
- match gll with
- | [goal] when pr_first ->
- pr_goal { Evd.it = goal ; sigma = sigma }
- | _ ->
- (* spiwack: it's not very nice to have to call proof global
- here, a more robust solution would be to add a hook for
- [Printer.pr_open_subgoals] in proof modes, in order to
- compute the end command. Yet a more robust solution would be
- to have focuses give explanations of their unfocusing
- behaviour. *)
- let p = Proof_global.give_me_the_proof () in
- let close_cmd = Decl_mode.get_end_command p in
- str "Subproof completed, now type " ++ str close_cmd ++ str "."
-
-let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
- Decl_interp.interp_proof_instr
- (Decl_mode.get_info sigma gl)
- (Goal.V82.env sigma gl)
- (sigma)
-
-let vernac_decl_proof () =
- let pf = Proof_global.give_me_the_proof () in
- if Proof.is_done pf then
- CErrors.error "Nothing left to prove here."
- else
- begin
- Decl_proof_instr.go_to_proof_mode () ;
- Proof_global.set_proof_mode "Declarative"
- end
-
-(* spiwack: some bureaucracy is not performed here *)
-let vernac_return () =
- begin
- Decl_proof_instr.return_from_tactic_mode () ;
- Proof_global.set_proof_mode "Declarative"
- end
-
-let vernac_proof_instr instr =
- Decl_proof_instr.proof_instr instr
-
-(* Before we can write an new toplevel command (see below)
- which takes a [proof_instr] as argument, we need to declare
- how to parse it, print it, globalise it and interprete it.
- Normally we could do that easily through ARGUMENT EXTEND,
- but as the parsing is fairly complicated we will do it manually to
- indirect through the [proof_instr] grammar entry. *)
-(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
-
-(* Only declared at raw level, because only used in vernac commands. *)
-let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
- Genarg.make0 "proof_instr"
-
-(* We create a new parser entry [proof_mode]. The Declarative proof mode
- will replace the normal parser entry for tactics with this one. *)
-let proof_mode : vernac_expr Gram.entry =
- Gram.entry_create "vernac:proof_command"
-(* Auxiliary grammar entry. *)
-let proof_instr : raw_proof_instr Gram.entry =
- Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
-
-let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
- pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
-
-let classify_proof_instr = function
- | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
- | _ -> Vernac_classifier.classify_as_proofstep
-
-(* We use the VERNAC EXTEND facility with a custom non-terminal
- to populate [proof_mode] with a new toplevel interpreter.
- The "-" indicates that the rule does not start with a distinguished
- string. *)
-VERNAC proof_mode EXTEND ProofInstr
- [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ]
-END
-
-(* It is useful to use GEXTEND directly to call grammar entries that have been
- defined previously VERNAC EXTEND. In this case we allow, in proof mode,
- the use of commands like Check or Print. VERNAC EXTEND does quite a bit of
- bureaucracy for us, but it is not needed in this sort of case, and it would require
- to have an ARGUMENT EXTEND version of the "proof_mode" grammar entry. *)
-GEXTEND Gram
- GLOBAL: proof_mode ;
-
- proof_mode: LAST
- [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ]
- ;
-END
-
-(* We register a new proof mode here *)
-
-let _ =
- Proof_global.register_proof_mode { Proof_global.
- name = "Declarative" ; (* name for identifying and printing *)
- (* function [set] goes from No Proof Mode to
- Declarative Proof Mode performing side effects *)
- set = begin fun () ->
- (* We set the command non terminal to
- [proof_mode] (which we just defined). *)
- Pcoq.set_command_entry proof_mode ;
- (* We substitute the goal printer, by the one we built
- for the proof mode. *)
- Printer.set_printer_pr { Printer.default_printer_pr with
- Printer.pr_goal = pr_goal;
- pr_subgoals = pr_subgoals; }
- end ;
- (* function [reset] goes back to No Proof Mode from
- Declarative Proof Mode *)
- reset = begin fun () ->
- (* We restore the command non terminal to
- [noedit_mode]. *)
- Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
- (* We restore the goal printer to default *)
- Printer.set_printer_pr Printer.default_printer_pr
- end
- }
-
-VERNAC COMMAND EXTEND DeclProof
-[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
-END
-VERNAC COMMAND EXTEND DeclReturn
-[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ]
-END
-
-let none_is_empty = function
- None -> []
- | Some l -> l
-
-GEXTEND Gram
-GLOBAL: proof_instr;
- thesis :
- [[ "thesis" -> Plain
- | "thesis"; "for"; i=ident -> (For i)
- ]];
- statement :
- [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
- | i=ident -> {st_label=Anonymous;
- st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
- | c=constr -> {st_label=Anonymous;st_it=c}
- ]];
- constr_or_thesis :
- [[ t=thesis -> Thesis t ] |
- [ c=constr -> This c
- ]];
- statement_or_thesis :
- [
- [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ]
- |
- [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
- | i=ident -> {st_label=Anonymous;
- st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
- | c=constr -> {st_label=Anonymous;st_it=This c}
- ]
- ];
- justification_items :
- [[ -> Some []
- | "by"; l=LIST1 constr SEP "," -> Some l
- | "by"; "*" -> None ]]
- ;
- justification_method :
- [[ -> None
- | "using"; tac = tactic -> Some tac ]]
- ;
- simple_cut_or_thesis :
- [[ ls = statement_or_thesis;
- j = justification_items;
- taco = justification_method
- -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
- ;
- simple_cut :
- [[ ls = statement;
- j = justification_items;
- taco = justification_method
- -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
- ;
- elim_type:
- [[ IDENT "induction" -> ET_Induction
- | IDENT "cases" -> ET_Case_analysis ]]
- ;
- block_type :
- [[ IDENT "claim" -> B_claim
- | IDENT "focus" -> B_focus
- | IDENT "proof" -> B_proof
- | et=elim_type -> B_elim et ]]
- ;
- elim_obj:
- [[ IDENT "on"; c=constr -> Real c
- | IDENT "of"; c=simple_cut -> Virtual c ]]
- ;
- elim_step:
- [[ IDENT "consider" ;
- h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
- | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)
- | IDENT "suffices"; ls=suff_clause;
- j = justification_items;
- taco = justification_method
- -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]]
- ;
- rew_step :
- [[ "~=" ; c=simple_cut -> (Rhs,c)
- | "=~" ; c=simple_cut -> (Lhs,c)]]
- ;
- cut_step:
- [[ "then"; tt=elim_step -> Pthen tt
- | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c)
- | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c))
- | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c)
- | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c)
- | tt=elim_step -> tt
- | tt=rew_step -> let s,c=tt in Prew (s,c);
- | IDENT "have"; c=simple_cut_or_thesis -> Pcut c;
- | IDENT "claim"; c=statement -> Pclaim c;
- | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c;
- | "end"; bt = block_type -> Pend bt;
- | IDENT "escape" -> Pescape ]]
- ;
- (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*)
- loc_id:
- [[ id=ident -> fun x -> (!@loc,(id,x)) ]];
- hyp:
- [[ id=loc_id -> id None ;
- | id=loc_id ; ":" ; c=constr -> id (Some c)]]
- ;
- consider_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=consider_vars -> (Hvar name) :: v
- | name=hyp;
- IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h
- ]]
- ;
- consider_hyps:
- [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h
- | st=statement; IDENT "and";
- IDENT "consider" ; v=consider_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]]
- ;
- assume_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=assume_vars -> (Hvar name) :: v
- | name=hyp;
- IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h
- ]]
- ;
- assume_hyps:
- [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h
- | st=statement; IDENT "and";
- IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]]
- ;
- assume_clause:
- [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v
- | h=assume_hyps -> h ]]
- ;
- suff_vars:
- [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
- [Hvar name],c
- | name=hyp; ","; v=suff_vars ->
- let (q,c) = v in ((Hvar name) :: q),c
- | name=hyp;
- IDENT "such"; IDENT "that"; h=suff_hyps ->
- let (q,c) = h in ((Hvar name) :: q),c
- ]];
- suff_hyps:
- [[ st=statement; IDENT "and"; h=suff_hyps ->
- let (q,c) = h in (Hprop st::q),c
- | st=statement; IDENT "and";
- IDENT "to" ; IDENT "have" ; v=suff_vars ->
- let (q,c) = v in (Hprop st::q),c
- | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
- [Hprop st],c
- ]]
- ;
- suff_clause:
- [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v
- | h=suff_hyps -> h ]]
- ;
- let_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=let_vars -> (Hvar name) :: v
- | name=hyp; IDENT "be";
- IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h
- ]]
- ;
- let_hyps:
- [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h
- | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]];
- given_vars:
- [[ name=hyp -> [Hvar name]
- | name=hyp; ","; v=given_vars -> (Hvar name) :: v
- | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h
- ]]
- ;
- given_hyps:
- [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h
- | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v
- | st=statement -> [Hprop st]
- ]];
- suppose_vars:
- [[name=hyp -> [Hvar name]
- |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v
- |name=hyp; OPT[IDENT "be"];
- IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h
- ]]
- ;
- suppose_hyps:
- [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h
- | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have";
- v=suppose_vars -> Hprop st::v
- | st=statement_or_thesis -> [Hprop st]
- ]]
- ;
- suppose_clause:
- [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v;
- | h=suppose_hyps -> h ]]
- ;
- intro_step:
- [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
- | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
- po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ;
- ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] ->
- Pcase (none_is_empty po,c,none_is_empty ho)
- | "let" ; v=let_vars -> Plet v
- | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses
- | IDENT "assume"; h=assume_clause -> Passume h
- | IDENT "given"; h=given_vars -> Pgiven h
- | IDENT "define"; id=ident; args=LIST0 hyp;
- "as"; body=constr -> Pdefine(id,args,body)
- | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ)
- | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ)
- ]]
- ;
- emphasis :
- [[ -> 0
- | "*" -> 1
- | "**" -> 2
- | "***" -> 3
- ]]
- ;
- bare_proof_instr:
- [[ c = cut_step -> c ;
- | i = intro_step -> i ]]
- ;
- proof_instr :
- [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]]
- ;
-END;;
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
deleted file mode 100644
index 92045e775..000000000
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ /dev/null
@@ -1,218 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Pp
-open Decl_expr
-open Names
-open Nameops
-
-let pr_label = function
- Anonymous -> mt ()
- | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
-
-let pr_justification_items pr_constr = function
- Some [] -> mt ()
- | Some (_::_ as l) ->
- spc () ++ str "by" ++ spc () ++
- prlist_with_sep (fun () -> str ",") pr_constr l
- | None -> spc () ++ str "by *"
-
-let pr_justification_method pr_tac = function
- None -> mt ()
- | Some tac ->
- spc () ++ str "using" ++ spc () ++ pr_tac tac
-
-let pr_statement pr_constr st =
- pr_label st.st_label ++ pr_constr st.st_it
-
-let pr_or_thesis pr_this = function
- Thesis Plain -> str "thesis"
- | Thesis (For id) ->
- str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
- | This c -> pr_this c
-
-let pr_cut pr_constr pr_tac pr_it c =
- hov 1 (pr_it c.cut_stat) ++
- pr_justification_items pr_constr c.cut_by ++
- pr_justification_method pr_tac c.cut_using
-
-let type_or_thesis = function
- Thesis _ -> Term.mkProp
- | This c -> c
-
-let _I x = x
-
-let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps =
- let pr_sep = if sep then str "and" ++ spc () else mt () in
- match hyps with
- (Hvar _ ::_) as rest ->
- spc () ++ pr_sep ++ str _have ++
- pr_vars pr_var pr_constr gtyp false _be _have rest
- | Hprop st :: rest ->
- begin
- (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*)
- spc() ++ pr_sep ++ pr_statement pr_constr st ++
- pr_hyps pr_var pr_constr gtyp true _be _have rest
- end
- | [] -> mt ()
-
-and pr_vars pr_var pr_constr gtyp sep _be _have vars =
- match vars with
- Hvar st :: rest ->
- begin
- (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*)
- let pr_sep = if sep then pr_comma () else mt () in
- spc() ++ pr_sep ++
- pr_var st ++
- pr_vars pr_var pr_constr gtyp true _be _have rest
- end
- | (Hprop _ :: _) as rest ->
- let _st = if _be then
- str "be such that"
- else
- str "such that" in
- spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest
- | [] -> mt ()
-
-let pr_suffices_clause pr_var pr_constr (hyps,c) =
- pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++
- str "to show" ++ spc () ++ pr_or_thesis pr_constr c
-
-let pr_elim_type = function
- ET_Case_analysis -> str "cases"
- | ET_Induction -> str "induction"
-
-let pr_block_type = function
- B_elim et -> pr_elim_type et
- | B_proof -> str "proof"
- | B_claim -> str "claim"
- | B_focus -> str "focus"
-
-let pr_casee pr_constr pr_tac =function
- Real c -> str "on" ++ spc () ++ pr_constr c
- | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut
-
-let pr_side = function
- Lhs -> str "=~"
- | Rhs -> str "~="
-
-let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function
- | Pescape -> str "escape"
- | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i
- | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i
- | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i
- | Pcut c ->
- begin
- match _then,_thus with
- false,false -> str "have" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- | false,true -> str "thus" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- | true,false -> str "then" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- | true,true -> str "hence" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- end
- | Psuffices c ->
- str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c
- | Prew (sid,c) ->
- (if _thus then str "thus" else str " ") ++ spc () ++
- pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c
- | Passume hyps ->
- str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps
- | Plet hyps ->
- str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps
- | Pclaim st ->
- str "claim" ++ spc () ++ pr_statement pr_constr st
- | Pfocus st ->
- str "focus on" ++ spc () ++ pr_statement pr_constr st
- | Pconsider (id,hyps) ->
- str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps
- ++ spc () ++ str "from " ++ pr_constr id
- | Pgiven hyps ->
- str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps
- | Ptake witl ->
- str "take" ++ spc () ++
- prlist_with_sep pr_comma pr_constr witl
- | Pdefine (id,args,body) ->
- str "define" ++ spc () ++ pr_id id ++ spc () ++
- prlist_with_sep spc
- (fun st -> str "(" ++
- pr_var st ++ str ")") args ++ spc () ++
- str "as" ++ (pr_constr body)
- | Pcast (id,typ) ->
- str "reconsider" ++ spc () ++
- pr_or_thesis pr_id id ++ spc () ++
- str "as" ++ spc () ++ (pr_constr typ)
- | Psuppose hyps ->
- str "suppose" ++
- pr_hyps pr_var pr_constr _I false false "we have" hyps
- | Pcase (params,pat,hyps) ->
- str "suppose it is" ++ spc () ++ pr_pat pat ++
- (if params = [] then mt () else
- (spc () ++ str "with" ++ spc () ++
- prlist_with_sep spc
- (fun st -> str "(" ++
- pr_var st ++ str ")") params ++ spc ()))
- ++
- (if hyps = [] then mt () else
- (spc () ++ str "and" ++
- pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis
- false false "we have" hyps))
- | Pper (et,c) ->
- str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
- pr_casee pr_constr pr_tac c
- | Pend blk -> str "end" ++ spc () ++ pr_block_type blk
-
-let pr_emph = function
- 0 -> str " "
- | 1 -> str "* "
- | 2 -> str "** "
- | 3 -> str "*** "
- | _ -> anomaly (Pp.str "unknown emphasis")
-
-let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr =
- pr_emph instr.emph ++ spc () ++
- pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr
-
-
-let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) =
- pr_gen_proof_instr
- (fun (_,(id,otyp)) ->
- match otyp with
- None -> pr_id id
- | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")"
- )
- pconstr2
- Ppconstr.pr_cases_pattern_expr
- (ptac Pptactic.ltop)
- instr
-
-let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
- pr_gen_proof_instr
- (fun (_,(id,otyp)) ->
- match otyp with
- None -> pr_id id
- | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")")
- pconstr2
- Ppconstr.pr_cases_pattern_expr
- (ptac Pptactic.ltop)
- instr
-
-let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
- let pconstr1 c = pconstr1 (EConstr.of_constr c) in
- let pconstr2 c = pconstr2 (EConstr.of_constr c) in
- pr_gen_proof_instr
- (fun st -> pr_statement pconstr1 st)
- pconstr2
- (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr)
- (ptac Pptactic.ltop)
- instr
-
diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
deleted file mode 100644
index 678fc0768..000000000
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-
-open Decl_expr
-open Pptactic
-
-val pr_gen_proof_instr :
- ('var -> Pp.std_ppcmds) ->
- ('constr -> Pp.std_ppcmds) ->
- ('pat -> Pp.std_ppcmds) ->
- ('tac -> Pp.std_ppcmds) ->
- ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
-
-val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
-val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
-val pr_proof_instr : proof_instr extra_genarg_printer
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index e28d6aa62..3c0319319 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -159,21 +159,3 @@ END
open Proofview.Notations
open Cc_plugin
-open Decl_mode_plugin
-
-let default_declarative_automation =
- Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
- Tacticals.New.tclORELSE
- (Tacticals.New.tclORELSE (Auto.h_trivial [] None)
- (Cctac.congruence_tac !congruence_depth []))
- (Proofview.V82.tactic (gen_ground_tac true
- (Some (Tacticals.New.tclTHEN
- (snd (default_solver ()))
- (Cctac.congruence_tac !congruence_depth [])))
- [] []))
-
-
-
-let () =
- Decl_proof_instr.register_automation_tac default_declarative_automation
-
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1ec52718a..38fdfb759 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac =
let flags = {
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some Pfedit.solve_by_implicit_tactic;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true
} in
@@ -348,10 +348,10 @@ END
open EConstr
open Vars
-let constr_flags = {
+let constr_flags () = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+ Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true }
@@ -360,7 +360,7 @@ let refine_tac ist simple with_classes c =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags =
- { constr_flags with Pretyping.use_typeclasses = with_classes } in
+ { constr_flags () with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma ->
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index e9a6e9e04..dfa8331ff 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -46,7 +46,7 @@ let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some Pfedit.solve_by_implicit_tactic;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true
} in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 928646bcb..50f43931e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
Proofview.NonLogical.run (db_constr (curr_debug ist) env evd c);
(evd,c)
-let constr_flags = {
+let constr_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = true;
expand_evars = true }
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
- interp_gen kind ist false constr_flags env sigma c
+ interp_gen kind ist false (constr_flags ()) env sigma c
let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
-let open_constr_use_classes_flags = {
+let open_constr_use_classes_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true }
-let open_constr_no_classes_flags = {
+let open_constr_no_classes_flags () = {
use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true }
@@ -679,11 +679,11 @@ let pure_open_constr_flags = {
expand_evars = false }
(* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
let flags =
- if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
- else open_constr_use_classes_flags in
- interp_gen expected_type ist false flags
+ if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
+ else open_constr_use_classes_flags () in
+ interp_gen expected_type ist false flags env sigma c
let interp_pure_open_constr ist =
interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
@@ -1789,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(TacLetTac(na,c,clp,b,eqpat))
(Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
(let_pat_tac b (interp_name ist env sigma na)
- ((sigma,sigma'),c) clp eqpat) sigma')
+ (sigma,c) clp eqpat) sigma')
end }
(* Derived basic tactics *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 44b771283..4bb66b8e9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1222,20 +1222,22 @@ let check_problems_are_solved env evd =
| (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2)
| _ -> ()
+exception MaxUndefined of (Evar.t * evar_info * Constr.t list)
+
let max_undefined_with_candidates evd =
- (* If evar were ordered with highest index first, fold_undefined
- would be going decreasingly and we could use fold_undefined to
- find the undefined evar of maximum index (alternatively,
- max_bindings from ocaml 3.12 could be used); instead we traverse
- the whole map *)
- let l = Evd.fold_undefined
- (fun evk ev_info evars ->
- match ev_info.evar_candidates with
- | None -> evars
- | Some l -> (evk,ev_info,l)::evars) evd [] in
- match l with
- | [] -> None
- | a::l -> Some (List.last (a::l))
+ let fold evk evi () = match evi.evar_candidates with
+ | None -> ()
+ | Some l -> raise (MaxUndefined (evk, evi, l))
+ in
+ (** [fold_right] traverses the undefined map in decreasing order of indices.
+ The evar with candidates of maximum index is thus the first evar with
+ candidates found by a [fold_right] traversal. This has a significant impact on
+ performance. *)
+ try
+ let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in
+ None
+ with MaxUndefined ans ->
+ Some ans
let rec solve_unconstrained_evars_with_candidates ts evd =
(* max_undefined is supposed to return the most recent, hence
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4a73a9e0c..a042b73c2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -263,16 +263,36 @@ type inference_flags = {
[sigma'] into those already in [sigma] or deriving from an evar in
[sigma] by restriction, and the evars properly created in [sigma'] *)
+type frozen =
+| FrozenId of evar_info Evar.Map.t
+ (** No pending evars. We do not put a set here not to reallocate like crazy,
+ but the actual data of the map is not used, only keys matter. All
+ functions operating on this type must have the same behaviour on
+ [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *)
+| FrozenProgress of (Evar.Set.t * Evar.Set.t) Lazy.t
+ (** Proper partition of the evar map as described above. *)
+
let frozen_and_pending_holes (sigma, sigma') =
- let add_derivative_of evk evi acc =
- match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
- let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
- let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
- let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
- (frozen,pending)
+ let undefined0 = Evd.undefined_map sigma in
+ (** Fast path when the undefined evars where not modified *)
+ if undefined0 == Evd.undefined_map sigma' then
+ FrozenId undefined0
+ else
+ let data = lazy begin
+ let add_derivative_of evk evi acc =
+ match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+ let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in
+ let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+ let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+ (frozen, pending)
+ end in
+ FrozenProgress data
let apply_typeclasses env evdref frozen fail_evar =
- let filter_frozen evk = Evar.Set.mem evk frozen in
+ let filter_frozen = match frozen with
+ | FrozenId map -> fun evk -> Evar.Map.mem evk map
+ | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
+ in
evdref := Typeclasses.resolve_typeclasses
~filter:(if Flags.is_program_mode ()
then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -282,7 +302,9 @@ let apply_typeclasses env evdref frozen fail_evar =
evdref := Typeclasses.resolve_typeclasses
~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
-let apply_inference_hook hook evdref pending =
+let apply_inference_hook hook evdref frozen = match frozen with
+| FrozenId _ -> ()
+| FrozenProgress (lazy (_, pending)) ->
evdref := Evar.Set.fold (fun evk sigma ->
if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
then
@@ -305,7 +327,9 @@ let check_typeclasses_instances_are_solved env current_sigma frozen =
(* Naive way, call resolution again with failure flag *)
apply_typeclasses env (ref current_sigma) frozen true
-let check_extra_evars_are_solved env current_sigma pending =
+let check_extra_evars_are_solved env current_sigma frozen = match frozen with
+| FrozenId _ -> ()
+| FrozenProgress (lazy (_, pending)) ->
Evar.Set.iter
(fun evk ->
if not (Evd.is_defined current_sigma evk) then
@@ -330,29 +354,29 @@ let check_evars env initial_sigma sigma c =
| _ -> EConstr.iter sigma proc_rec c
in proc_rec c
-let check_evars_are_solved env current_sigma frozen pending =
+let check_evars_are_solved env current_sigma frozen =
check_typeclasses_instances_are_solved env current_sigma frozen;
check_problems_are_solved env current_sigma;
- check_extra_evars_are_solved env current_sigma pending
+ check_extra_evars_are_solved env current_sigma frozen
(* Try typeclasses, hooks, unification heuristics ... *)
-let solve_remaining_evars flags env current_sigma pending =
- let frozen,pending = frozen_and_pending_holes pending in
+let solve_remaining_evars flags env current_sigma init_sigma =
+ let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
let evdref = ref current_sigma in
if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
if Option.has_some flags.use_hook then
- apply_inference_hook (Option.get flags.use_hook env) evdref pending;
+ apply_inference_hook (Option.get flags.use_hook env) evdref frozen;
if flags.solve_unification_constraints then apply_heuristics env evdref false;
- if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
+ if flags.fail_evar then check_evars_are_solved env !evdref frozen;
!evdref
-let check_evars_are_solved env current_sigma pending =
- let frozen,pending = frozen_and_pending_holes pending in
- check_evars_are_solved env current_sigma frozen pending
+let check_evars_are_solved env current_sigma init_sigma =
+ let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
+ check_evars_are_solved env current_sigma frozen
let process_inference_flags flags env initial_sigma (sigma,c) =
- let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in
+ let sigma = solve_remaining_evars flags env sigma initial_sigma in
let c = if flags.expand_evars then nf_evar sigma c else c in
sigma,c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7284c0655..f13c10b05 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -130,13 +130,13 @@ val type_uconstr :
[pending], however, it can contain more evars than the pending ones. *)
val solve_remaining_evars : inference_flags ->
- env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
+ env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map
(** Checking evars and pending conversion problems are all solved,
reporting an appropriate error message *)
val check_evars_are_solved :
- env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
+ env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit
(** [check_evars env initial_sigma extended_sigma c] fails if some
new unresolved evar remains in [c] *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index eb90dfbdb..532cc8baa 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1571,7 +1571,7 @@ let default_matching_merge_flags sigma =
use_pattern_unification = true;
}
-let default_matching_flags (sigma,_) =
+let default_matching_flags sigma =
let flags = default_matching_core_flags sigma in {
core_unify_flags = flags;
merge_unify_flags = default_matching_merge_flags sigma;
@@ -1709,10 +1709,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
type prefix_of_inductive_support_flag = bool
-type pending_constr = Evd.pending * constr
-
type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * (evar_map * constr) * clause * bool
| AbstractExact of Name.t * constr * types option * clause * bool
type 'r abstraction_result =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 6760283d2..148178f2f 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -71,14 +71,12 @@ exception PatternNotFound
type prefix_of_inductive_support_flag = bool
-type pending_constr = Evd.pending * constr
-
type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool
| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
- env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma
+ env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma
type 'r abstraction_result =
Names.Id.t * named_context_val *
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c1a95878f..7e8ed31d1 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -234,10 +234,10 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac
let clear_implicit_tactic () = implicit_tactic := None
-let solve_by_implicit_tactic env sigma evk =
+let apply_implicit_tactic tac = (); fun env sigma evk ->
let evi = Evd.find_undefined sigma evk in
- match (!implicit_tactic, snd (evar_source evk sigma)) with
- | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
+ match snd (evar_source evk sigma) with
+ | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
when
Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
@@ -252,3 +252,9 @@ let solve_by_implicit_tactic env sigma evk =
sigma, EConstr.of_constr ans
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
+
+let solve_by_implicit_tactic () = match !implicit_tactic with
+| None -> None
+| Some tac -> Some (apply_implicit_tactic tac)
+
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 516125ea1..f9fb0b76d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
val clear_implicit_tactic : unit -> unit
(* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr
+val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8306ac174..e79258582 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1151,7 +1151,7 @@ let run_delayed env sigma c =
let tactic_infer_flags with_evar = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = Some solve_by_implicit_tactic;
+ Pretyping.use_hook = solve_by_implicit_tactic ();
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
@@ -1159,10 +1159,9 @@ let tactic_infer_flags with_evar = {
let onOpenInductionArg env sigma tac = function
| clear_flag,ElimOnConstr f ->
let (cbl, sigma') = run_delayed env sigma f in
- let pending = (sigma,sigma') in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS sigma')
- (tac clear_flag (pending,cbl))
+ (tac clear_flag (sigma,cbl))
| clear_flag,ElimOnAnonHyp n ->
Tacticals.New.tclTHEN
(intros_until_n n)
@@ -1170,8 +1169,7 @@ let onOpenInductionArg env sigma tac = function
(fun c ->
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
- let pending = (sigma,sigma) in
- tac clear_flag (pending,(c,NoBindings))
+ tac clear_flag (sigma,(c,NoBindings))
end }))
| clear_flag,ElimOnIdent (_,id) ->
(* A quantified hypothesis *)
@@ -1179,8 +1177,7 @@ let onOpenInductionArg env sigma tac = function
(try_intros_until_id_check id)
(Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
- let pending = (sigma,sigma) in
- tac clear_flag (pending,(mkVar id,NoBindings))
+ tac clear_flag (sigma,(mkVar id,NoBindings))
end })
let onInductionArg tac = function
@@ -1203,10 +1200,9 @@ let map_destruction_arg f sigma = function
let finish_delayed_evar_resolution with_evars env sigma f =
let ((c, lbind), sigma') = run_delayed env sigma f in
- let pending = (sigma,sigma') in
let sigma' = Sigma.Unsafe.of_evar_map sigma' in
let flags = tactic_infer_flags with_evars in
- let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in
+ let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in
(Sigma.to_evar_map sigma', (c, lbind))
let with_no_bindings (c, lbind) =
@@ -4579,11 +4575,11 @@ let induction_destruct isrec with_evars (lc,elim) =
let induction ev clr c l e =
induction_gen clr true ev e
- (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None
+ ((Evd.empty,(c,NoBindings)),(None,l)) None
let destruct ev clr c l e =
induction_gen clr false ev e
- (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None
+ ((Evd.empty,(c,NoBindings)),(None,l)) None
(* The registered tactic, which calls the default elimination
* if no elimination constant is provided. *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 67e29cf56..ba4a9706d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -386,7 +386,7 @@ val letin_tac : (bool * intro_pattern_naming) option ->
(** Common entry point for user-level "set", "pose" and "remember" *)
val letin_pat_tac : (bool * intro_pattern_naming) option ->
- Name.t -> pending_constr -> clause -> unit Proofview.tactic
+ Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic
(** {6 Generalize tactics. } *)
diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v
deleted file mode 100644
index da0cc68a4..000000000
--- a/test-suite/bugs/closed/2640.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Testing consistency of globalization and interpretation in some
- extreme cases *)
-
-Section sect.
-
- (* Simplification of the initial example *)
- Hypothesis Other: True.
-
- Lemma C2 : True.
- proof.
- Fail have True using Other.
- Abort.
-
- (* Variant of the same problem *)
- Lemma C2 : True.
- Fail clear; Other.
- Abort.
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
deleted file mode 100644
index ea3920551..000000000
--- a/test-suite/ide/undo.v
+++ /dev/null
@@ -1,103 +0,0 @@
-(* Here are a sequences of scripts to test interactively with undo and
- replay in coqide proof sessions *)
-
-(* Undoing arbitrary commands, as first step *)
-
-Theorem a : O=O. (* 2 *)
-Ltac f x := x. (* 1 * 3 *)
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing arbitrary commands, as non-first step *)
-
-Theorem b : O=O.
-assert True by trivial.
-Ltac g x := x.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, as first step *)
-(* was bugged in 8.1 *)
-
-Theorem c : O=O.
-Inductive T : Type := I.
-trivial.
-Qed.
-
-(* Undoing declarations, as first step *)
-(* new in 8.2 *)
-
-Theorem d : O=O.
-Definition e := O.
-Definition f := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, as non-first step *)
-(* new in 8.2 *)
-
-Theorem h : O=O.
-assert True by trivial.
-Definition i := O.
-Definition j := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, interleaved with proof steps *)
-(* new in 8.2 *)
-
-Theorem k : O=O.
-assert True by trivial.
-Definition l := O.
-assert True by trivial.
-Definition m := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, interleaved with proof steps and commands *)
-(* new in 8.2 *)
-
-Theorem n : O=O.
-assert True by trivial.
-Definition o := O.
-Ltac h x := x.
-assert True by trivial.
-Focus.
-Definition p := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, not in proof *)
-
-Definition q := O.
-Definition r := O.
-
-(* Bug 2082 : Follow the numbers *)
-(* Broken due to proof engine rewriting *)
-
-Variable A : Prop.
-Variable B : Prop.
-
-Axiom OR : A \/ B.
-
-Lemma MyLemma2 : True.
-proof.
-per cases of (A \/ B) by OR.
-suppose A.
- then (1 = 1).
- then H1 : thesis. (* 4 *)
- thus thesis by H1. (* 2 *)
-suppose B. (* 1 *) (* 3 *)
- then (1 = 1).
- then H2 : thesis.
- thus thesis by H2.
-end cases.
-end proof.
-Qed. (* 5 if you made it here, there is no regression *)
-
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
deleted file mode 100644
index 0be439b27..000000000
--- a/test-suite/ide/undo011.fake
+++ /dev/null
@@ -1,34 +0,0 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
-# Run it via fake_ide
-#
-# Bug 2082
-# Broken due to proof engine rewriting
-#
-ADD { Variable A : Prop. }
-ADD { Variable B : Prop. }
-ADD { Axiom OR : A \/ B. }
-ADD { Lemma MyLemma2 : True. }
-ADD { proof. }
-ADD { per cases of (A \/ B) by OR. }
-ADD { suppose A. }
-ADD { then (1 = 1). }
-ADD there { then H1 : thesis. }
-ADD here { thus thesis by H1. }
-ADD { suppose B. }
-QUERY { Show. }
-EDIT_AT here
-# <replay>
-ADD { suppose B. }
-# </replay>
-EDIT_AT there
-# <replay>
-ADD { thus thesis by H1. }
-ADD { suppose B. }
-# </replay>
-QUERY { Show. }
-ADD { then (1 = 1). }
-ADD { then H2 : thesis. }
-ADD { thus thesis by H2. }
-ADD { end cases. }
-ADD { end proof. }
-ADD { Qed. }
diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
index 851ecd930..776dfeb55 100644
--- a/test-suite/output/ErrorInModule.out
+++ b/test-suite/output/ErrorInModule.out
@@ -1,2 +1,3 @@
File "stdin", line 3, characters 20-31:
Error: The reference nonexistent was not found in the current environment.
+
diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out
index 851ecd930..776dfeb55 100644
--- a/test-suite/output/ErrorInSection.out
+++ b/test-suite/output/ErrorInSection.out
@@ -1,2 +1,3 @@
File "stdin", line 3, characters 20-31:
Error: The reference nonexistent was not found in the current environment.
+
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
index 9300c3f54..e9c70d1ef 100644
--- a/test-suite/output/qualification.out
+++ b/test-suite/output/qualification.out
@@ -1,3 +1,4 @@
File "stdin", line 19, characters 0-7:
Error: Signature components for label test do not match: expected type
"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
+
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
deleted file mode 100644
index e569bcb49..000000000
--- a/test-suite/success/decl_mode.v
+++ /dev/null
@@ -1,182 +0,0 @@
-(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *)
-
-Set Firstorder Depth 1.
-Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt.
-
-Lemma double_div2: forall n, div2 (double n) = n.
-proof.
- assume n:nat.
- per induction on n.
- suppose it is 0.
- suffices (0=0) to show thesis.
- thus thesis.
- suppose it is (S m) and Hrec:thesis for m.
- have (div2 (double (S m))= div2 (S (S (double m)))).
- ~= (S (div2 (double m))).
- thus ~= (S m) by Hrec.
- end induction.
-end proof.
-Show Script.
-Qed.
-
-Lemma double_inv : forall n m, double n = double m -> n = m .
-proof.
- let n, m be such that H:(double n = double m).
-have (n = div2 (double n)) by double_div2,H.
- ~= (div2 (double m)) by H.
- thus ~= m by double_div2.
-end proof.
-Qed.
-
-Lemma double_mult_l : forall n m, (double (n * m)=n * double m).
-proof.
- assume n:nat and m:nat.
- have (double (n * m) = n*m + n * m).
- ~= (n * (m+m)) by * using ring.
- thus ~= (n * double m).
-end proof.
-Qed.
-
-Lemma double_mult_r : forall n m, (double (n * m)=double n * m).
-proof.
- assume n:nat and m:nat.
- have (double (n * m) = n*m + n * m).
- ~= ((n + n) * m) by * using ring.
- thus ~= (double n * m).
-end proof.
-Qed.
-
-Lemma even_is_even_times_even: forall n, even (n*n) -> even n.
-proof.
- let n be such that H:(even (n*n)).
- per cases of (even n \/ odd n) by even_or_odd.
- suppose (odd n).
- hence thesis by H,even_mult_inv_r.
- end cases.
-end proof.
-Qed.
-
-Lemma main_thm_aux: forall n,even n ->
-double (double (div2 n *div2 n))=n*n.
-proof.
- given n such that H:(even n).
- *** have (double (double (div2 n * div2 n))
- = double (div2 n) * double (div2 n))
- by double_mult_l,double_mult_r.
- thus ~= (n*n) by H,even_double.
-end proof.
-Qed.
-
-Require Import Omega.
-
-Lemma even_double_n: (forall m, even (double m)).
-proof.
- assume m:nat.
- per induction on m.
- suppose it is 0.
- thus thesis.
- suppose it is (S mm) and thesis for mm.
- then H:(even (S (S (mm+mm)))).
- have (S (S (mm + mm)) = S mm + S mm) using omega.
- hence (even (S mm +S mm)) by H.
- end induction.
-end proof.
-Qed.
-
-Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0.
-proof.
- assume n0:nat.
- define P n as (forall p, n*n=double (p*p) -> p=0).
- claim rec_step: (forall n, (forall m,m<n-> P m) -> P n).
- let n be such that H:(forall m : nat, m < n -> P m) and p:nat .
- per cases of ({n=0}+{n<>0}) by eq_nat_dec.
- suppose H1:(n=0).
- per cases on p.
- suppose it is (S p').
- assume (n * n = double (S p' * S p')).
- =~ 0 by H1,mult_n_O.
- ~= (S ( p' + p' * S p' + S p'* S p'))
- by plus_n_Sm.
- hence thesis .
- suppose it is 0.
- thus thesis.
- end cases.
- suppose H1:(n<>0).
- assume H0:(n*n=double (p*p)).
- have (even (double (p*p))) by even_double_n .
- then (even (n*n)) by H0.
- then H2:(even n) by even_is_even_times_even.
- then (double (double (div2 n *div2 n))=n*n)
- by main_thm_aux.
- ~= (double (p*p)) by H0.
- then H':(double (div2 n *div2 n)= p*p) by double_inv.
- have (even (double (div2 n *div2 n))) by even_double_n.
- then (even (p*p)) by even_double_n,H'.
- then H3:(even p) by even_is_even_times_even.
- have (double(double (div2 n * div2 n)) = n*n)
- by H2,main_thm_aux.
- ~= (double (p*p)) by H0.
- ~= (double(double (double (div2 p * div2 p))))
- by H3,main_thm_aux.
- then H'':(div2 n * div2 n = double (div2 p * div2 p))
- by double_inv.
- then (div2 n < n) by lt_div2,neq_O_lt,H1.
- then H4:(div2 p=0) by (H (div2 n)),H''.
- then (double (div2 p) = double 0).
- =~ p by even_double,H3.
- thus ~= 0.
- end cases.
- end claim.
- hence thesis by (lt_wf_ind n0 P).
-end proof.
-Qed.
-
-Require Import Reals Field.
-(*Coercion INR: nat >->R.
-Coercion IZR: Z >->R.*)
-
-Open Scope R_scope.
-
-Lemma square_abs_square:
- forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p).
-proof.
- assume p:Z.
- per cases on p.
- suppose it is (0%Z).
- thus thesis.
- suppose it is (Zpos z).
- thus thesis.
- suppose it is (Zneg z).
- have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) =
- (IZR (Zpos z) * IZR (Zpos z))).
- ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))).
- thus ~= (IZR (Zneg z) * IZR (Zneg z)).
- end cases.
-end proof.
-Admitted.
-
-Definition irrational (x:R):Prop :=
- forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q).
-
-Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)).
-proof.
- let p:Z,q:nat be such that H:(q<>0%nat)
- and H0:(sqrt (INR 2%nat)=(IZR p/INR q)).
- have H_in_R:(INR q<>0:>R) by H.
- have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field.
- have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def.
- have (INR (Z.abs_nat p * Z.abs_nat p)
- = (INR (Z.abs_nat p) * INR (Z.abs_nat p)))
- by mult_INR.
- ~= (IZR p* IZR p) by square_abs_square.
- ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *)
- ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring.
- ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0.
- ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR.
- then (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat.
- ~= ((q*q)+(q*q))%nat.
- ~= (Div2.double (q*q)).
- then (q=0%nat) by main_theorem.
- hence thesis by H.
-end proof.
-Qed.
diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v
deleted file mode 100644
index 46174e481..000000000
--- a/test-suite/success/decl_mode2.v
+++ /dev/null
@@ -1,249 +0,0 @@
-Theorem this_is_trivial: True.
-proof.
- thus thesis.
-end proof.
-Qed.
-
-Theorem T: (True /\ True) /\ True.
- split. split.
-proof. (* first subgoal *)
- thus thesis.
-end proof.
-trivial. (* second subgoal *)
-proof. (* third subgoal *)
- thus thesis.
-end proof.
-Abort.
-
-Theorem this_is_not_so_trivial: False.
-proof.
-end proof. (* here a warning is issued *)
-Fail Qed. (* fails: the proof in incomplete *)
-Admitted. (* Oops! *)
-
-Theorem T: True.
-proof.
-escape.
-auto.
-return.
-Abort.
-
-Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False).
-intros a b.
-proof.
-assume H:(if a then True else False).
-reconsider H as False.
-reconsider thesis as True.
-Abort.
-
-Theorem T: forall x, x=2 -> 2+x=4.
-proof.
-let x be such that H:(x=2).
-have H':(2+x=2+2) by H.
-Abort.
-
-Theorem T: forall x, x=2 -> 2+x=4.
-proof.
-let x be such that H:(x=2).
-then (2+x=2+2).
-Abort.
-
-Theorem T: forall x, x=2 -> x + x = x * x.
-proof.
-let x be such that H:(x=2).
-have (4 = 4).
- ~= (2 * 2).
- ~= (x * x) by H.
- =~ (2 + 2).
- =~ H':(x + x) by H.
-Abort.
-
-Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2.
-proof.
-let x be such that H:(x + x = x * x).
-claim H':((x - 2) * x = 0).
-thus thesis.
-end claim.
-Abort.
-
-Theorem T: forall (A B:Prop), A -> B -> A /\ B.
-intros A B HA HB.
-proof.
-hence B.
-Abort.
-
-Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C.
-intros A B C HA HB HC.
-proof.
-thus B by HB.
-Abort.
-
-Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B.
-intros A B C HA HB HC.
-proof.
-Fail hence C. (* fails *)
-Abort.
-
-Theorem T: forall (A B:Prop), B -> A \/ B.
-intros A B HB.
-proof.
-hence B.
-Abort.
-
-Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D).
-intros A B C D HC HD.
-proof.
-thus C by HC.
-Abort.
-
-Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
-intros P HP.
-proof.
-take 2.
-Abort.
-
-Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
-intros P HP.
-proof.
-hence (P 2).
-Abort.
-
-Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y.
-intros P R HP HR.
-proof.
-thus (P 2) by HP.
-Abort.
-
-Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B.
-intros A B P HP HA.
-proof.
-suffices to have x such that HP':(P x) to show B by HP,HP'.
-Abort.
-
-Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x).
-intros A P HP HA.
-proof.
-(* BUG: the next line fails when it should succeed.
-Waiting for someone to investigate the bug.
-focus on (forall x, x = 2 -> P x).
-let x be such that (x = 2).
-hence thesis by HP.
-end focus.
-*)
-Abort.
-
-Theorem T: forall x, x = 0 -> x + x = x * x.
-proof.
-let x be such that H:(x = 0).
-define sqr x as (x * x).
-reconsider thesis as (x + x = sqr x).
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x:nat.
-assume HP:(P x).
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-Fail let x. (* fails because x's type is not clear *)
-let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x:nat.
-assume (P x). (* temporary name created *)
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x be such that (P x). (* temporary name created *)
-Abort.
-
-Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A.
-proof.
-let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A).
-consider x such that HP:(P x) and HA:A from H.
-Abort.
-
-(* Here is an example with pairs: *)
-
-Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p).
-proof.
-let p:(nat * nat)%type.
-consider x:nat,y:nat from p.
-reconsider thesis as (x >= y \/ x < y).
-Abort.
-
-Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) ->
-(exists m, P m) -> P 0.
-proof.
-let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)).
-given m such that Hm:(P m).
-Abort.
-
-Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C.
-proof.
-let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C).
-assume HAB:(A \/ B).
-per cases on HAB.
-suppose A.
- hence thesis by HAC.
-suppose HB:B.
- thus thesis by HB,HBC.
-end cases.
-Abort.
-
-Section Coq.
-
-Hypothesis EM : forall P:Prop, P \/ ~ P.
-
-Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
-proof.
-let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
-per cases of (A \/ ~A) by EM.
-suppose (~A).
- hence thesis by HNAC.
-suppose A.
- hence thesis by HAC.
-end cases.
-Abort.
-
-Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
-proof.
-let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
-per cases on (EM A).
-suppose (~A).
-Abort.
-End Coq.
-
-Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B.
-proof.
-let A:Prop,B:Prop,x:bool.
-per cases on x.
-suppose it is true.
- assume A.
- hence A.
-suppose it is false.
- assume B.
- hence B.
-end cases.
-Abort.
-
-Theorem T: forall (n:nat), n + 0 = n.
-proof.
-let n:nat.
-per induction on n.
-suppose it is 0.
- thus (0 + 0 = 0).
-suppose it is (S m) and H:thesis for m.
- then (S (m + 0) = S m).
- thus =~ (S m + 0).
-end induction.
-Abort. \ No newline at end of file
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 03f2328de..c58d23dad 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,7 +19,6 @@ Require Export Coq.Init.Tauto.
(* Initially available plugins
(+ nat_syntax_plugin loaded in Datatypes) *)
Declare ML Module "extraction_plugin".
-Declare ML Module "decl_mode_plugin".
Declare ML Module "cc_plugin".
Declare ML Module "ground_plugin".
Declare ML Module "recdef_plugin".
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0cc6ca317..8e6f9ffb5 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -52,7 +52,6 @@ let resynch_buffer ibuf =
to avoid interfering with utf8. Compatibility code removed. *)
let emacs_prompt_startstring() = Printer.emacs_str "<prompt>"
-
let emacs_prompt_endstring() = Printer.emacs_str "</prompt>"
(* Read a char in an input channel, displaying a prompt at every
@@ -83,6 +82,7 @@ let reset_input_buffer ic ibuf =
ibuf.start <- 0
(* Functions to print underlined locations from an input buffer. *)
+module TopErr = struct
(* Given a location, returns the list of locations of each line. The last
line is returned separately. It also checks the location bounds. *)
@@ -124,10 +124,11 @@ let blanch_utf8_string s bp ep = let open Bytes in
done;
Bytes.sub_string s' 0 !j
+let adjust_loc_buf ib loc = let open Loc in
+ { loc with ep = loc.ep - ib.start; bp = loc.bp - ib.start }
+
let print_highlight_location ib loc =
let (bp,ep) = Loc.unloc loc in
- let bp = bp - ib.start
- and ep = ep - ib.start in
let highlight_lines =
match get_bols_of_loc ib (bp,ep) with
| ([],(bl,el)) ->
@@ -147,28 +148,58 @@ let print_highlight_location ib loc =
str sn ++ str dn) in
(l1 ++ li ++ ln)
in
- let loc = Loc.make_loc (bp,ep) in
- (Pp.pr_loc loc ++ highlight_lines ++ fnl ())
-
-(* Functions to report located errors in a file. *)
-
-let print_location_in_file loc =
- let fname = loc.Loc.fname in
- let errstrm = str"Error while reading " ++ str fname in
- if Loc.is_ghost loc then
- hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
- else
- let errstrm = mt ()
- (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *)
- in
- let open Loc in
- hov 0 (* No line break so as to follow emacs error message format *)
- (errstrm ++ Pp.pr_loc loc)
+ highlight_lines
let valid_buffer_loc ib loc =
not (Loc.is_ghost loc) &&
let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
+(* This is specific to the toplevel *)
+let pr_loc loc =
+ if Loc.is_ghost loc then str"<unknown>"
+ else
+ let fname = loc.Loc.fname in
+ if CString.equal fname "" then
+ Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+ str"-" ++ int loc.ep ++ str":")
+ else
+ Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+ str", line " ++ int loc.line_nb ++ str", characters " ++
+ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+ str":")
+
+(* Toplevel error explanation. *)
+let error_info_for_buffer ?loc buf =
+ Option.map (fun loc ->
+ let fname = loc.Loc.fname in
+ let hl, loc =
+ (* We are in the toplevel *)
+ if String.equal fname "" then
+ let nloc = adjust_loc_buf buf loc in
+ if valid_buffer_loc buf loc then
+ (fnl () ++ print_highlight_location buf nloc, nloc)
+ (* in the toplevel, but not a valid buffer *)
+ else (mt (), nloc)
+ (* we are in batch mode, don't adjust location *)
+ else (mt (), loc)
+ in pr_loc loc ++ hl
+ ) loc
+
+(* Actual printing routine *)
+let print_error_for_buffer ?loc lvl msg buf =
+ let pre_hdr = error_info_for_buffer ?loc buf in
+ if !Flags.print_emacs
+ then Topfmt.emacs_logger ?pre_hdr lvl msg
+ else Topfmt.std_logger ?pre_hdr lvl msg
+
+let print_toplevel_parse_error (e, info) buf =
+ let loc = Loc.get_loc info in
+ let lvl = Feedback.Error in
+ let msg = CErrors.iprint (e, info) in
+ print_error_for_buffer ?loc lvl msg buf
+
+end
+
(*s The Coq prompt is the name of the focused proof, if any, and "Coq"
otherwise. We trap all exceptions to prevent the error message printing
from cycling. *)
@@ -178,18 +209,6 @@ let make_prompt () =
with Proof_global.NoCurrentProof ->
"Coq < "
-(*let build_pending_list l =
- let pl = ref ">" in
- let l' = ref l in
- let res =
- while List.length !l' > 1 do
- pl := !pl ^ "|" Names.Id.to_string x;
- l':=List.tl !l'
- done in
- let last = try List.hd !l' with _ -> in
- "<"^l'
-*)
-
(* the coq prompt added to the default one when in emacs mode
The prompt contains the current state label [n] (for global
backtracking) and the current proof state [p] (for proof
@@ -234,27 +253,6 @@ let set_prompt prompt =
^ prompt ()
^ emacs_prompt_endstring())
-(* The following exceptions need not be located. *)
-
-let locate_exn = function
- | Out_of_memory | Stack_overflow | Sys.Break -> false
- | _ -> true
-
-(* Toplevel error explanation. *)
-
-let print_toplevel_error (e, info) =
- let loc = Option.default Loc.ghost (Loc.get_loc info) in
- let fname = loc.Loc.fname in
- let locmsg =
- if Loc.is_ghost loc || String.equal fname "" then
- if locate_exn e && valid_buffer_loc top_buffer loc then
- print_highlight_location top_buffer loc
- else mt ()
- else print_location_in_file loc
- in
- let hdr msg = hov 0 (Topfmt.err_hdr ++ msg) in
- locmsg ++ hdr (CErrors.iprint (e, info))
-
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
let rec dot st = match Compat.get_tok (Stream.next st) with
@@ -283,6 +281,7 @@ let read_sentence input =
with reraise ->
let reraise = CErrors.push reraise in
discard_to_dot ();
+ TopErr.print_toplevel_parse_error reraise top_buffer;
iraise reraise
(** Coqloop Console feedback handler *)
@@ -300,17 +299,8 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
| FileDependency (_,_) -> ()
| FileLoaded (_,_) -> ()
| Custom (_,_,_) -> ()
- | Message (Error,loc,msg) ->
- (* We ignore errors here as we (still) have a different error
- printer for the toplevel. It is hard to solve due the many
- error paths presents, and the different compromise of feedback
- error forwaring in the stm depending on the mode *)
- ()
| Message (lvl,loc,msg) ->
- if !Flags.print_emacs then
- Topfmt.emacs_logger ?loc lvl msg
- else
- Topfmt.std_logger ?loc lvl msg
+ TopErr.print_error_for_buffer ?loc lvl msg top_buffer
(** [do_vernac] reads and executes a toplevel phrase, and print error
messages when an exception is raised, except for the following:
@@ -334,13 +324,13 @@ let do_vernac () =
top_stderr (fnl ()); raise CErrors.Quit
| CErrors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise CErrors.Drop
- else top_stderr (str "There is no ML toplevel.")
- | any ->
- (** Main error printer, note that this didn't it the "emacs"
- legacy path. *)
- let any = CErrors.push any in
- let msg = print_toplevel_error any ++ fnl () in
- top_stderr msg
+ else Feedback.msg_error (str "There is no ML toplevel.")
+ (* Exception printing is done now by the feedback listener. *)
+ (* XXX: We need this hack due to the side effects of the exception
+ printer and the reliance of Stm.define on attaching crutial
+ state to exceptions *)
+ | any -> ignore (CErrors.(iprint (push any)))
+
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -367,7 +357,7 @@ let rec loop () =
| CErrors.Drop -> ()
| CErrors.Quit -> exit 0
| any ->
- top_stderr (str"Anomaly: main loop exited with exception: " ++
+ Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
fnl() ++
str"Please report" ++
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index eb61084e0..8a34ded6d 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -26,12 +26,7 @@ type input_buffer = {
val top_buffer : input_buffer
val set_prompt : (unit -> string) -> unit
-(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D
- May raise only the following exceptions: [Drop] and [End_of_input],
- meaning we get out of the Coq loop. *)
-
-val print_toplevel_error : Exninfo.iexn -> std_ppcmds
-
+(** Toplevel feedback printer. *)
val coqloop_feed : Feedback.feedback -> unit
(** Parse and execute one vernac command. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0cd5498fe..4968804fd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -653,10 +653,10 @@ let init_toplevel arglist =
flush_all();
let msg =
if !batch_mode then mt ()
- else str "Error during initialization:" ++ fnl ()
+ else str "Error during initialization: " ++ CErrors.iprint any ++ fnl ()
in
let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
- fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any))
+ fatal_error msg (is_anomaly (fst any))
end;
if !batch_mode then begin
flush_all();
diff --git a/vernac/command.ml b/vernac/command.ml
index 0393669d4..781bf3223 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -143,7 +143,7 @@ let interp_definition pl bl p red_option c ctypopt =
red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
let check_definition (ce, evd, _, imps) =
- check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
+ check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
let warn_local_declaration =
@@ -305,7 +305,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
((env,ienv),((is_coe,idl),t,imps)))
(env,empty_internalization_env) l
in
- let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
+ let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
(* The universe constraints come from the whole telescope. *)
let evd = Evd.nf_constraints evd in
let ctx = Evd.universe_context_set evd in
@@ -614,7 +614,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
() in
(* Try further to solve evars, and instantiate them *)
- let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in
+ let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in
evdref := sigma;
(* Compute renewed arities *)
let nf,_ = e_nf_evars_and_universes evdref in
@@ -1174,7 +1174,7 @@ let interp_recursive isfix fixl notations =
(env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
- check_evars_are_solved env evd (Evd.empty,evd);
+ check_evars_are_solved env evd Evd.empty;
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
check_mutuality env evd isfix (List.combine fixnames fixdefs)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f5d7a661e..993a2c260 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -463,7 +463,7 @@ let start_proof_com ?inference_hook kind thms hook =
let t', imps' = interp_type_evars_impls ~impls env evdref t in
let flags = all_and_fail_flags in
let flags = { flags with use_hook = inference_hook } in
- evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
+ evdref := solve_remaining_evars flags env !evdref Evd.empty;
let ids = List.map RelDecl.get_name ctx in
(compute_proof_name (pi1 kind) sopt,
(EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
diff --git a/vernac/record.ml b/vernac/record.ml
index 490a2a49d..8b4b7606f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -145,7 +145,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
in
let sigma =
- Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
+ Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
let evars, nf = Evarutil.nf_evars_and_universes sigma in
let arity = nf t' in
let arity, evars =
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index f843484f7..ee5536692 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -108,7 +108,7 @@ end
type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
-let msgnl_with fmt strm =
+let msgnl_with ?pre_hdr fmt strm =
pp_with fmt (strm ++ fnl ());
Format.pp_print_flush fmt ()
@@ -136,20 +136,19 @@ let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc ()
let info_hdr = mt ()
let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
let err_hdr = tag Tag.error (str "Error:") ++ spc ()
+let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc ()
-let make_body quoter info ?loc s =
- let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
- quoter (hov 0 (loc ++ info ++ s))
+let make_body quoter info ?pre_hdr s =
+ pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))
(* Generic logger *)
-let gen_logger dbg err ?loc level msg = match level with
- | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?loc msg)
- | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg)
- (* XXX: What to do with loc here? *)
- | Notice -> msgnl_with !std_ft msg
+let gen_logger dbg err ?pre_hdr level msg = match level with
+ | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg)
+ | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
+ | Notice -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
| Warning -> Flags.if_warn (fun () ->
- msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) ()
- | Error -> msgnl_with !err_ft (make_body err err_hdr ?loc msg)
+ msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) ()
+ | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg)
(** Standard loggers *)
@@ -158,8 +157,8 @@ let gen_logger dbg err ?loc level msg = match level with
*)
let std_logger_cleanup = ref (fun () -> ())
-let std_logger ?loc level msg =
- gen_logger (fun x -> x) (fun x -> x) ?loc level msg;
+let std_logger ?pre_hdr level msg =
+ gen_logger (fun x -> x) (fun x -> x) ?pre_hdr level msg;
!std_logger_cleanup ()
(** Color logging. Moved from Ppstyle, it may need some more refactoring *)
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 1555f80a9..909dd7077 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -38,11 +38,11 @@ val get_margin : unit -> int option
(** Headers for tagging *)
val err_hdr : Pp.std_ppcmds
+val ann_hdr : Pp.std_ppcmds
-(** Console display of feedback *)
-val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
-
-val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+(** Console display of feedback, we may add some location information *)
+val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
+val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
val init_color_output : unit -> unit
val clear_styles : unit -> unit