diff options
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 @@ -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) @@ -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 |