diff options
67 files changed, 1451 insertions, 637 deletions
diff --git a/.gitignore b/.gitignore index 4acd9930e3..bea12162c4 100644 --- a/.gitignore +++ b/.gitignore @@ -52,9 +52,9 @@ dev/ocamldebug-coq plugins/micromega/csdpcert kernel/byterun/dllcoqrun.so coqdoc.sty -csdp.cache -test-suite/lia.cache -test-suite/nra.cache +.csdp.cache +test-suite/.lia.cache +test-suite/.nra.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -68,7 +68,7 @@ doc/faq/axioms.eps_t doc/faq/axioms.pdf doc/faq/axioms.pdf_t doc/faq/axioms.png -doc/refman/csdp.cache +doc/refman/.csdp.cache doc/refman/trace doc/refman/Reference-Manual.pdf doc/refman/Reference-Manual.ps @@ -135,7 +135,7 @@ kernel/copcodes.ml tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt -lia.cache +.lia.cache checker/names.ml checker/names.mli checker/esubst.ml @@ -111,6 +111,7 @@ Changes from V8.5pl2 to V8.5pl3 =============================== Critical bugfix + - #4876: Guard checker incompleteness when using primitive projections Other bugfixes @@ -119,7 +120,50 @@ Other bugfixes - #4673: regression in setoid_rewrite, unfolding let-ins for type unification. - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. - #4769: Anomaly with universe polymorphic schemes defined inside sections. -- #3886: Program: duplicate obligations of mutual fixpoints +- #3886: Program: duplicate obligations of mutual fixpoints. +- #4994: Documentation typo. +- #5008: Use the "md5" command on OpenBSD. +- #5007: Do not assume the "TERM" environment variable is always set. +- #4606: Output a break before a list only if there was an empty line. +- #5001: metas not cleaned properly in clenv_refine_in. +- #2336: incorrect glob data for module symbols (bug #2336). +- #4832: Remove extraneous dot in error message. +- Anomaly in printing a unification error message. +- #4947: Options which take string arguments are not backwards compatible. +- #4156: micromega cache files are now hidden files. +- #4871: interrupting par:abstract kills coqtop. +- #5043: [Admitted] lemmas pick up section variables. +- Fix name of internal refine ("simple refine"). +- #5062: probably a typo in Strict Proofs mode. +- #5065: Anomaly: Not a proof by induction. +- Restore native compiler optimizations, they were disabled since 8.5! +- #5077: failure on typing a fixpoint with evars in its type. +- Fix recursive notation bug. +- #5095: non relevant too strict test in let-in abstraction. +- Ensuring that the evar name is preserved by "rename". +- #4887: confusion between using and with in documentation of firstorder. +- Bug in subst with let-ins. +- #4762: eauto weaker than auto. +- Remove if_then_else (was buggy). Use tryif instead. +- #4970: confusion between special "{" and non special "{{" in notations. +- #4529: primitive projections unfolding. +- #4416: Incorrect "Error: Incorrect number of goals". +- #4863: abstract in typeclass hint fails. +- #5123: unshelve can impact typeclass resolution +- Fix a collision about the meta-variable ".." in recursive notations. +- Fix printing of info_auto. +- #3209: Not_found due to an occur-check cycle. +- #5097: status of evars refined by "clear" in ltac: closed wrt evars. +- #5150: Missing dependency of the test-suite subsystems in prerequisite. +- Fix a bug in error printing of unif constraints +- #3941: Do not stop propagation of signals when Coq is busy. +- #4822: Incorrect assertion in cbn. +- #3479 parsing of "{" and "}" when a keyword starts with "{" or "}". +- #5127: Memory corruption with the VM. +- #5102: bullets parsing broken by calls to parse_entry. + +Various documentation improvements + Changes from V8.5pl1 to V8.5pl2 =============================== diff --git a/META.coq b/META.coq new file mode 100644 index 0000000000..5be69d5fdc --- /dev/null +++ b/META.coq @@ -0,0 +1,249 @@ +description = "The Coq Proof Assistant Plugin API" +version = "8.6" + +directory = "" +requires = "camlp5" + +package "config" ( + + description = "Coq Configuration Variables" + version = "8.6" + + directory = "config" + +) + +package "lib" ( + + description = "Base Coq Library" + version = "8.6" + + directory = "lib" + + requires = "coq.config" + + archive(byte) = "clib.cma" + archive(byte) += "lib.cma" + + archive(native) = "clib.cmxa" + archive(native) += "lib.cmxa" + +) + +package "vm" ( + + description = "Coq VM" + + version = "8.6" + +# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq +# install. In a local one we'll want kernel/byterun, in a non-local +# one we want to set it to coqlib. We should thus generate this file +# at configure time, but let's hear for some more feedback from +# experts. + +# Enable for local native & byte builds +# directory = "kernel/byterun" + +# Enable for local byte builds and set up properly +# linkopts(byte) = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun" + +# Disable for local byte builds + linkopts(byte) = "-dllib -lcoqrun" + linkopts(native) = "-cclib -lcoqrun" + +) + +package "kernel" ( + + description = "The Coq's Kernel" + version = "8.6" + + directory = "kernel" + + requires = "coq.lib, coq.vm" + + archive(byte) = "kernel.cma" + archive(native) = "kernel.cmxa" + +) + +package "library" ( + + description = "Coq Libraries (vo) support" + version = "8.6" + + requires = "coq.kernel" + + directory = "library" + + archive(byte) = "library.cma" + archive(native) = "library.cmxa" + +) + +package "intf" ( + + description = "Coq Public Data Types" + version = "8.6" + + requires = "coq.library" + + directory = "intf" + +) + +package "engine" ( + + description = "Coq Libraries (vo) support" + version = "8.6" + + requires = "coq.library" + directory = "engine" + + archive(byte) = "engine.cma" + archive(native) = "engine.cmxa" + +) + +package "pretyping" ( + + description = "Coq Pretyper" + version = "8.6" + + requires = "coq.engine" + directory = "pretyping" + + archive(byte) = "pretyping.cma" + archive(native) = "pretyping.cmxa" + +) + +package "interp" ( + + description = "Coq Term Interpretation" + version = "8.6" + + requires = "coq.pretyping" + directory = "interp" + + archive(byte) = "interp.cma" + archive(native) = "interp.cmxa" + +) + +package "grammar" ( + + description = "Coq Base Grammar" + version = "8.6" + + requires = "coq.interp" + directory = "grammar" + + archive(byte) = "grammar.cma" + archive(native) = "grammar.cmxa" +) + +package "proofs" ( + + description = "Coq Proof Engine" + version = "8.6" + + requires = "coq.interp" + directory = "proofs" + + archive(byte) = "proofs.cma" + archive(native) = "proofs.cmxa" + +) + +package "parsing" ( + + description = "Coq Parsing Engine" + version = "8.6" + + requires = "coq.proofs" + directory = "parsing" + + archive(byte) = "parsing.cma" + archive(native) = "parsing.cmxa" + +) + +package "printing" ( + + description = "Coq Printing Libraries" + version = "8.6" + + requires = "coq.parsing" + directory = "printing" + + archive(byte) = "printing.cma" + archive(native) = "printing.cmxa" + +) + +package "tactics" ( + + description = "Coq Tactics" + version = "8.6" + + requires = "coq.printing" + directory = "tactics" + + archive(byte) = "tactics.cma" + archive(native) = "tactics.cmxa" + +) + +package "stm" ( + + description = "Coq State Transactional Machine" + version = "8.6" + + requires = "coq.tactics" + directory = "stm" + + archive(byte) = "stm.cma" + archive(native) = "stm.cmxa" + +) + +package "toplevel" ( + + description = "Coq Toplevel" + version = "8.6" + + requires = "coq.stm" + directory = "toplevel" + + archive(byte) = "toplevel.cma" + archive(native) = "toplevel.cmxa" + +) + +package "highparsing" ( + + description = "Coq Extra Parsing" + version = "8.6" + + requires = "coq.toplevel" + directory = "parsing" + + archive(byte) = "highparsing.cma" + archive(native) = "highparsing.cmxa" + +) + +package "ltac" ( + + description = "Coq LTAC Plugin" + version = "8.6" + + requires = "coq.highparsing" + directory = "ltac" + + archive(byte) = "ltac.cma" + archive(native) = "ltac.cmxa" + +) diff --git a/Makefile.install b/Makefile.install index 4dad8cf0d4..4800ea0b96 100644 --- a/Makefile.install +++ b/Makefile.install @@ -18,7 +18,7 @@ ifeq ($(LOCAL),true) install: @echo "Nothing to install in a local build!" else -install: install-coq install-coqide install-doc-$(WITHDOC) +install: install-coq install-coqide install-doc-$(WITHDOC) install-meta endif # NOTA: for install-coqide, see Makefile.ide @@ -58,6 +58,7 @@ endif .PHONY: install-coq install-binaries install-byte install-opt .PHONY: install-tools install-library install-devfiles .PHONY: install-coq-info install-coq-manpages install-emacs install-latex +.PHONY: install-meta install-coq: install-binaries install-library install-coq-info install-devfiles @@ -140,6 +141,9 @@ install-latex: $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) +install-meta: META.coq + $(INSTALLLIB) META.coq $(FULLCOQLIB)/META + # For emacs: # Local Variables: # mode: makefile diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 6f85849888..c1e552a5da 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -199,6 +199,12 @@ The following command-line options are recognized by the commands {\tt available for {\tt coqc} only; it is the counterpart of {\tt -compile-verbose}. + \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ % + + Configure the display of warnings. This option expects {\tt all}, {\tt none} + or a comma-separated list of warning names or categories (see + Section~\ref{SetWarnings}). + %Mostly unused in the code %\item[{\tt -debug}]\ % % diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 919e7b5cdc..3a9db5ead2 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -914,6 +914,19 @@ This command turns off the normal displaying. \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}} This command turns the normal display on. +\subsection[\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,% + \nterm{w}$_n$).]{{\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,% + \nterm{w}$_n$)}.\optindex{Warnings}} +\label{SetWarnings} +This command configures the display of warnings. It is experimental, and expects +\texttt{all}, \texttt{none} or a comma-separated list of warning names or +categories. Adding~\texttt{-} in front of a warning disables it, +adding~\texttt{+} makes it an error. It is possible to use the special categories +\texttt{all} and \texttt{default}, the latter containing the warnings enabled by +default. The flags are interpreted from left to right, so in case of an overlap, +the flags on the right have higher priority, meaning that \texttt{A,-A} is +equivalent to \texttt{-A}. + \subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only} \label{Search-Output-Name-Only} \index{Search Output Name Only mode}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 0aabaf6a87..656ae57b95 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3489,7 +3489,7 @@ hints of the database named {\tt core}. Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See Section~\ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a - database. This option can be combined with the previous one. + database. \item {\tt auto with *} @@ -3502,9 +3502,17 @@ hints of the database named {\tt core}. $lemma_i$ is an inductive type, it is the collection of its constructors which is added as hints. -\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$ +\item {\tt info\_auto} - This combines the effects of the {\tt using} and {\tt with} options. + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. \item {\tt trivial}\tacindex{trivial} @@ -3516,6 +3524,14 @@ hints of the database named {\tt core}. \item \texttt{trivial with *} +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leaves it @@ -3529,8 +3545,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail. This tactic generalizes {\tt auto}. While {\tt auto} does not try resolution hints which would leave existential variables in the goal, -{\tt eauto} does try them (informally speaking, it uses {\tt eapply} -where {\tt auto} uses {\tt apply}). +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3545,8 +3561,17 @@ eauto. Abort. \end{coq_eval} -Note that {\tt ex\_intro} should be declared as an -hint. +Note that {\tt ex\_intro} should be declared as a hint. + +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} \SeeAlso Section~\ref{Hints-databases} @@ -3700,11 +3725,12 @@ The {\hintdef} is one of the following expressions: the number of subgoals generated by {\tt simple apply {\term}}. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - % Is it really needed? - %% In case the inferred type of \term\ does not start with a product - %% the tactic added in the hint list is {\tt exact {\term}}. In case - %% this type can however be reduced to a type starting with a product, - %% the tactic {\tt apply {\term}} is also stored in the hints list. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. If the inferred type of \term\ contains a dependent quantification on a variable which occurs only in the premisses of the type and not @@ -3734,6 +3760,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} diff --git a/engine/evd.ml b/engine/evd.ml index 291c089784..aa91fc5222 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -641,6 +641,7 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = + (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -1411,7 +1412,16 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = - let env = Namegen.make_all_name_different env in + let env = + (** We currently allow evar instances to refer to anonymous de + Bruijn indices, so we protect the error printing code in this + case by giving names to every de Bruijn variable in the + rel_context of the conversion problem. MS: we should rather + stop depending on anonymous variables, they can be used to + indicate independency. Also, this depends on a strategy for + naming/renaming. *) + Namegen.make_all_name_different env + in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ print_constr_env env t1 ++ spc () ++ str (match pbty with diff --git a/engine/termops.ml b/engine/termops.ml index 17e56ec31e..35cacc65b2 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -599,6 +599,10 @@ let collect_vars c = | _ -> fold_constr aux vars c in aux Id.Set.empty c +let vars_of_global_reference env gr = + let c, _ = Universes.unsafe_constr_of_global gr in + vars_of_global (Global.env ()) c + (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) diff --git a/engine/termops.mli b/engine/termops.mli index 0a7ac1f266..fd8edafbcf 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -121,6 +121,7 @@ val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Id.Set.t (** for visible vars only *) +val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t val occur_term : constr -> constr -> bool (** Synonymous of dependent Substitution of metavariables *) diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index a1b3f4f255..683a7e2f71 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -48,7 +48,7 @@ let make_fun_clauses loc s l = let map c = GramCompat.make_fun loc [make_clause c] in mlexpr_of_list map l -let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> +let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> let rec mlexpr_of_symbol = function | Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7b520c1c11..0c5393cf41 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -248,6 +248,10 @@ let check_is_hole id = function GHole _ -> () | t -> let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' +type recursive_pattern_kind = +| RecursiveTerms of bool (* associativity *) +| RecursiveBinders of glob_constr * glob_constr + let compare_recursive_parts found f f' (iterator,subc) = let diff = ref None in let terminator = ref None in @@ -269,18 +273,16 @@ let compare_recursive_parts found f f' (iterator,subc) = let x,y = if lassoc then y,x else x,y in begin match !diff with | None -> - let () = diff := Some (x, y, Some lassoc) in + let () = diff := Some (x, y, RecursiveTerms lassoc) in true | Some _ -> false end | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> (* We found a binding position where it differs *) - check_is_hole x t_x; - check_is_hole y t_y; begin match !diff with | None -> - let () = diff := Some (x, y, None) in + let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in aux c term | Some _ -> false end @@ -294,7 +296,7 @@ let compare_recursive_parts found f f' (iterator,subc) = (* Here, we would need a loc made of several parts ... *) user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") - | Some (x,y,Some lassoc) -> + | Some (x,y,RecursiveTerms lassoc) -> let newfound,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) @@ -312,11 +314,13 @@ let compare_recursive_parts found f f' (iterator,subc) = (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,None) -> + | Some (x,y,RecursiveBinders (t_x,t_y)) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; + check_is_hole x t_x; + check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator)) else raise Not_found diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8572870407..1336c92b6f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -416,10 +416,12 @@ type vernac_expr = | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * - (vernac_argument_status list) list * - int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | - `DefaultImplicits ] list + vernac_argument_status list (* Main arguments status list *) * + (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * + int option (* Number of args to trigger reduction *) * + [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `DefaultImplicits ] list | VernacArgumentsScope of reference or_by_notation * scope_name option list | VernacReserve of simple_binder list @@ -479,11 +481,13 @@ and tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) +and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + and vernac_argument_status = { name : Name.t; recarg_like : bool; notation_scope : (Loc.t * string) option; - implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit]; + implicit_status : vernac_implicit_status; } (* A vernac classifier has to tell if a command: diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 29e33d349b..d5feafbf91 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -57,7 +57,7 @@ void init_arity () { arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= - arity[BRANCH]=arity[ISCONST]= 1; + arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[ARECONST]=arity[PROJ]=2; @@ -79,7 +79,7 @@ void * coq_stat_alloc (asize_t sz) value coq_makeaccu (value i) { code_t q; - code_t res = coq_stat_alloc(8); + code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); @@ -91,13 +91,13 @@ value coq_pushpop (value i) { int n; n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(4); + res = coq_stat_alloc(sizeof(opcode_t)); *res = VALINSTR(STOP); return (value)res; } else { code_t q; - res = coq_stat_alloc(12); + res = coq_stat_alloc(3 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 885594ac7b..d92e85fdf8 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -39,6 +39,7 @@ enum instructions { GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, PROJ, + ENSURESTACKCAPACITY, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, ACCUMULATE, diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index ddf40e2eb9..792a311fcf 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -76,6 +76,14 @@ sp is a local copy of the global variable extern_sp. */ # define print_lint(i) #endif +#define CHECK_STACK(num_args) { \ +if (sp - num_args < coq_stack_threshold) { \ + coq_sp = sp; \ + realloc_coq_stack(num_args + Coq_stack_threshold / sizeof(value)); \ + sp = coq_sp; \ + } \ +} + /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -198,6 +206,9 @@ value coq_interprete sp = coq_sp; pc = coq_pc; accu = coq_accu; + + CHECK_STACK(0); + #ifdef THREADED_CODE goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */ #else @@ -354,7 +365,7 @@ value coq_interprete coq_extra_args = *pc - 1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPLY1) { value arg1 = sp[0]; @@ -371,7 +382,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 0; - goto check_stacks; + goto check_stack; } Instruct(APPLY2) { value arg1 = sp[0]; @@ -386,7 +397,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 1; - goto check_stacks; + goto check_stack; } Instruct(APPLY3) { value arg1 = sp[0]; @@ -403,17 +414,13 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 2; - goto check_stacks; + goto check_stack; } /* Stack checks */ - check_stacks: - print_instr("check_stacks"); - if (sp < coq_stack_threshold) { - coq_sp = sp; - realloc_coq_stack(Coq_stack_threshold); - sp = coq_sp; - } + check_stack: + print_instr("check_stack"); + CHECK_STACK(0); /* We also check for signals */ if (caml_signals_are_pending) { /* If there's a Ctrl-C, we reset the vm */ @@ -422,6 +429,16 @@ value coq_interprete } Next; + Instruct(ENSURESTACKCAPACITY) { + print_instr("ENSURESTACKCAPACITY"); + int size = *pc++; + /* CHECK_STACK may trigger here a useless allocation because of the + threshold, but check_stack: often does it anyway, so we prefer to + factorize the code. */ + CHECK_STACK(size); + Next; + } + Instruct(APPTERM) { int nargs = *pc++; int slotsize = *pc; @@ -436,7 +453,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += nargs - 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM1) { value arg1 = sp[0]; @@ -445,7 +462,7 @@ value coq_interprete sp[0] = arg1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPTERM2) { value arg1 = sp[0]; @@ -458,7 +475,7 @@ value coq_interprete print_lint(accu); coq_env = accu; coq_extra_args += 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM3) { value arg1 = sp[0]; @@ -472,7 +489,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += 2; - goto check_stacks; + goto check_stack; } Instruct(RETURN) { @@ -503,6 +520,7 @@ value coq_interprete int num_args = Wosize_val(coq_env) - 2; int i; print_instr("RESTART"); + CHECK_STACK(num_args); sp -= num_args; for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2); coq_env = Field(coq_env, 1); @@ -863,29 +881,7 @@ value coq_interprete sp++; Next; } - - /* *sp = accu; - * Netoyage des cofix * - size = Wosize_val(accu); - for (i = 2; i < size; i++) { - accu = Field(*sp, i); - if (IS_EVALUATED_COFIX(accu)) { - size_aux = Wosize_val(accu); - *--sp = accu; - Alloc_small(accu, size_aux, Accu_tag); - for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j); - *sp = accu; - Alloc_small(accu, 1, ATOM_COFIX_TAG); - Field(accu, 0) = Field(Field(*sp, 1), 0); - caml_modify(&Field(*sp, 1), accu); - accu = *sp; sp++; - caml_modify(&Field(*sp, i), accu); - } - } - sp++; - Next; - } */ - + Instruct(SETFIELD){ print_instr("SETFIELD"); caml_modify(&Field(accu, *pc),*sp); @@ -979,28 +975,31 @@ value coq_interprete } Instruct(MAKESWITCHBLOCK) { print_instr("MAKESWITCHBLOCK"); - *--sp = accu; - accu = Field(accu,1); + *--sp = accu; // Save matched block on stack + accu = Field(accu,1); // Save atom to accu register switch (Tag_val(accu)) { - case ATOM_COFIX_TAG: + case ATOM_COFIX_TAG: // We are forcing a cofix { mlsize_t i, nargs; print_instr("COFIX_TAG"); sp-=2; pc++; + // Push the return address sp[0] = (value) (pc + *pc); sp[1] = coq_env; - coq_env = Field(accu,0); - accu = sp[2]; - sp[2] = Val_long(coq_extra_args); - nargs = Wosize_val(accu) - 2; + coq_env = Field(accu,0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs+1); sp -= nargs; - for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; - pc = Code_val(coq_env); - goto check_stacks; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; } case ATOM_COFIXEVALUATED_TAG: { @@ -1458,26 +1457,32 @@ value coq_push_val(value v) { value coq_push_arguments(value args) { int nargs,i; + value * sp = coq_sp; nargs = Wosize_val(args) - 2; + CHECK_STACK(nargs); coq_sp -= nargs; print_instr("push_args");print_int(nargs); for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2); return Val_unit; } -value coq_push_vstack(value stk) { +value coq_push_vstack(value stk, value max_stack_size) { int len,i; + value * sp = coq_sp; len = Wosize_val(stk); + CHECK_STACK(len); coq_sp -= len; print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); + sp = coq_sp; + CHECK_STACK(uint32_of_value(max_stack_size)); return Val_unit; } value coq_interprete_ml(value tcode, value a, value e, value ea) { print_instr("coq_interprete"); return coq_interprete((code_t)tcode, a, e, Long_val(ea)); - print_instr("end coq_interprete"); + print_instr("end coq_interprete"); } value coq_eval_tcode (value tcode, value e) { diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index c9bcdc32ff..45cfae509d 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -130,6 +130,7 @@ value init_coq_vm(value unit) /* ML */ return Val_unit;; } +/* [required_space] is a size in words */ void realloc_coq_stack(asize_t required_space) { asize_t size; diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 8d4de523a1..810c346990 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -43,7 +43,7 @@ type structured_constant = type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label = struct @@ -87,6 +87,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (* index of the projected argument, name of projection *) + | Kensurestackcapacity of int (* spiwack: instructions concerning integers *) | Kbranch of Label.t (* jump to label *) | Kaddint31 (* adds the int31 in the accu @@ -264,6 +265,8 @@ let rec pp_instr i = | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p + | Kensurestackcapacity size -> str "growstack " ++ int size + | Kaddint31 -> str "addint31" | Kaddcint31 -> str "addcint31" | Kaddcarrycint31 -> str "addcarrycint31" diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5f1f09d00c..b8de7619cf 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -39,7 +39,7 @@ val pp_struct_const : structured_constant -> Pp.std_ppcmds type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label : sig @@ -84,6 +84,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (** index of the projected argument, name of projection *) + | Kensurestackcapacity of int (** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7d08f9e2d9..b1fc0c85de 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -91,6 +91,11 @@ open Pre_env (* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) (* conversion of cofixpoints (which is intentional). *) +module Config = struct + let stack_threshold = 256 (* see byterun/coq_memory.h *) + let stack_safety_margin = 15 +end + type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } @@ -112,6 +117,26 @@ let empty_comp_env ?(univs=0) ()= in_env = ref empty_fv } +(* Maximal stack size reached during the current function body. Used to + reallocate the stack if we lack space. *) +let max_stack_size = ref 0 + +let set_max_stack_size stack_size = + if stack_size > !max_stack_size then + max_stack_size := stack_size + +let ensure_stack_capacity f x = + let old = !max_stack_size in + max_stack_size := 0; + let code = f x in + let used_safe = + !max_stack_size + Config.stack_safety_margin + in + max_stack_size := old; + if used_safe > Config.stack_threshold then + Kensurestackcapacity used_safe :: code + else code + (*i Creation functions for comp_env *) let rec add_param n sz l = @@ -370,14 +395,28 @@ let const_bn tag args = else Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args) - -let code_makeblock arity tag cont = +(* +If [tag] hits the OCaml limitation for non constant constructors, we switch to +another representation for the remaining constructors: +[last_variant_tag|tag - last_variant_tag|args] + +We subtract last_variant_tag for efficiency of match interpretation. + *) + +let nest_block tag arity cont = + Kconst (Const_b0 (tag - last_variant_tag)) :: + Kmakeblock(arity+1, last_variant_tag) :: cont + +let code_makeblock ~stack_size ~arity ~tag cont = if tag < last_variant_tag then Kmakeblock(arity, tag) :: cont - else - Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) :: - Kmakeblock(arity+1, last_variant_tag) :: cont + else begin + set_max_stack_size (stack_size + 1); + Kpush :: nest_block tag arity cont + end +(* [code_construct] compiles an abstracted constructor dropping parameters and + updates [fun_code] *) (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = let f_cont = @@ -386,11 +425,11 @@ let code_construct tag nparams arity cont = [Kconst (Const_b0 tag); Kreturn 0] else if tag < last_variant_tag then [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0] - else - [Kconst (Const_b0 (tag - last_variant_tag)); - Kmakeblock(arity+1, last_variant_tag); Kreturn 0]) + else + nest_block tag arity [Kreturn 0]) in let lbl = Label.create() in + (* No need to grow the stack here, as the function does not push stuff. *) fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; Kclosure(lbl,0) :: cont @@ -536,11 +575,12 @@ let compile_fv_elem reloc fv sz cont = let rec compile_fv reloc l sz cont = match l with | [] -> cont - | [fvn] -> compile_fv_elem reloc fvn sz cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont | fvn :: tl -> compile_fv_elem reloc fvn sz (Kpush :: compile_fv reloc tl (sz + 1) cont) + (* Compiling constants *) let rec get_alias env kn = @@ -555,6 +595,7 @@ let rec get_alias env kn = (* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = + set_max_stack_size sz; match kind_of_term c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" @@ -603,6 +644,7 @@ let rec compile_constr reloc c sz cont = compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont else let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc @@ -622,7 +664,8 @@ let rec compile_constr reloc c sz cont = let r_fun = comp_env_fun arity in let lbl_fun = Label.create() in let cont_fun = - compile_constr r_fun body arity [Kreturn arity] in + ensure_stack_capacity (compile_constr r_fun body arity) [Kreturn arity] + in fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) @@ -642,9 +685,10 @@ let rec compile_constr reloc c sz cont = (* Compilation des types *) let env_type = comp_env_fix_type rfv in for i = 0 to ndef - 1 do - let lbl,fcode = - label_code - (compile_constr env_type type_bodies.(i) 0 [Kstop]) in + let fcode = + ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -654,7 +698,8 @@ let rec compile_constr reloc c sz cont = let arity = List.length params in let env_body = comp_env_fix ndef i arity rfv in let cont1 = - compile_constr env_body body arity [Kreturn arity] in + ensure_stack_capacity (compile_constr env_body body arity) [Kreturn arity] + in let lbl = Label.create () in lbl_bodies.(i) <- lbl; let fcode = add_grabrec rec_args.(i) arity lbl cont1 in @@ -672,9 +717,10 @@ let rec compile_constr reloc c sz cont = let rfv = ref empty_fv in let env_type = comp_env_cofix_type ndef rfv in for i = 0 to ndef - 1 do - let lbl,fcode = - label_code - (compile_constr env_type type_bodies.(i) 0 [Kstop]) in + let fcode = + ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -684,14 +730,17 @@ let rec compile_constr reloc c sz cont = let arity = List.length params in let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in - let cont1 = - compile_constr env_body body (arity+1) (cont_cofix arity) in - let cont2 = - add_grab (arity+1) lbl cont1 in + let comp arity = + (* 4 stack slots are needed to update the cofix when forced *) + set_max_stack_size (arity + 4); + compile_constr env_body body (arity+1) (cont_cofix arity) + in + let cont = ensure_stack_capacity comp arity in lbl_bodies.(i) <- lbl; - fun_code := [Ksequence(cont2,!fun_code)]; + fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; done; let fv = !rfv in + set_max_stack_size (sz + fv.size + ndef + 2); compile_fv reloc fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) @@ -709,9 +758,11 @@ let rec compile_constr reloc c sz cont = let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) - let lbl_typ,fcode = - label_code (compile_constr reloc t sz [Kpop sz; Kstop]) - in fun_code := [Ksequence(fcode,!fun_code)]; + let fcode = + ensure_stack_capacity (compile_constr reloc t sz) [Kpop sz; Kstop] + in + let lbl_typ,fcode = label_code fcode in + fun_code := [Ksequence(fcode,!fun_code)]; (* Compiling branches *) let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = @@ -721,14 +772,9 @@ let rec compile_constr reloc c sz cont = sz, branch1, true | _ -> sz+3, Kjump, false in - let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in - (* Compiling branch for accumulators *) - let lbl_accu, code_accu = - label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont) - in - lbl_blocks.(0) <- lbl_accu; - let c = ref code_accu in - (* perform the extra match if needed (to many block constructors) *) + + let c = ref cont in + (* Perform the extra match if needed (too many block constructors) *) if neblock <> 0 then begin let lbl_b, code_b = label_code ( @@ -758,14 +804,34 @@ let rec compile_constr reloc c sz cont = compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c) in let code_b = - if tag < last_variant_tag then Kpushfields arity :: code_b - else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in + if tag < last_variant_tag then begin + set_max_stack_size (sz_b + arity); + Kpushfields arity :: code_b + end + else begin + set_max_stack_size (sz_b + arity + 1); + Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b + end + in let lbl_b,code_b = label_code code_b in if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; c := code_b done; - c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; + + let annot = + {ci = ci; rtbl = tbl; tailcall = is_tailcall; + max_stack_size = !max_stack_size - sz} + in + + (* Compiling branch for accumulators *) + let lbl_accu, code_accu = + set_max_stack_size (sz+3); + label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c) + in + lbl_blocks.(0) <- lbl_accu; + + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu; let code_sw = match branch1 with (* spiwack : branch1 can't be a lbl anymore it's a Branch instead @@ -782,12 +848,14 @@ let rec compile_constr reloc c sz cont = code_sw) and compile_str_cst reloc sc sz cont = + set_max_stack_size sz; match sc with | Bconstr c -> compile_constr reloc c sz cont | Bstrconst sc -> Kconst sc :: cont | Bmakeblock(tag,args) -> - let nargs = Array.length args in - comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont) + let arity = Array.length args in + let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in + comp_args compile_str_cst reloc args sz cont | Bconstruct_app(tag,nparams,arity,args) -> if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont @@ -801,6 +869,7 @@ and compile_str_cst reloc sc sz cont = (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) and compile_get_global reloc (kn,u) sz cont = + set_max_stack_size sz; let kn = get_alias !global_env kn in if Univ.Instance.is_empty u then Kgetglobal kn :: cont @@ -809,11 +878,13 @@ and compile_get_global reloc (kn,u) sz cont = compile_universe reloc () (Univ.Instance.to_array u) sz cont and compile_universe reloc uni sz cont = + set_max_stack_size sz; match Univ.Level.var_index uni with | None -> Kconst (Const_univ_level uni) :: cont | Some idx -> pos_universe_var idx reloc sz :: cont and compile_const reloc kn u args sz cont = + set_max_stack_size sz; let nargs = Array.length args in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function @@ -875,7 +946,7 @@ let compile fail_on_error ?universes:(universes=0) env c = let reloc, init_code = if Int.equal universes 0 then let reloc = empty_comp_env () in - reloc, compile_constr reloc c 0 cont + reloc, ensure_stack_capacity (compile_constr reloc c 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. @@ -892,11 +963,16 @@ let compile fail_on_error ?universes:(universes=0) env c = let r_fun = comp_env_fun ~univs:universes arity in let lbl_fun = Label.create () in let cont_fun = - compile_constr r_fun body full_arity [Kreturn full_arity] + ensure_stack_capacity (compile_constr r_fun body full_arity) + [Kreturn full_arity] in fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in - reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont) + let init_code = + ensure_stack_capacity (compile_fv reloc fv.fv_rev 0) + (Kclosure(lbl_fun,fv.size) :: cont) + in + reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in (if !Flags.dump_bytecode then diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index d779a81ff6..ad7a41a347 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -234,6 +234,7 @@ let emit_instr = function else (out opSETFIELD;out_int n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) + | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size (* spiwack *) | Kbranch lbl -> out opBRANCH; out_label lbl | Kaddint31 -> out opADDINT31 diff --git a/kernel/vm.ml b/kernel/vm.ml index eb992ef892..53483a2220 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -170,7 +170,7 @@ type whd = external push_ra : tcode -> unit = "coq_push_ra" external push_val : values -> unit = "coq_push_val" external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" +external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) @@ -206,7 +206,9 @@ let apply_varray vf varray = else begin push_ra stop; - push_vstack varray; + (* The fun code of [vf] will make sure we have enough stack, so we put 0 + here. *) + push_vstack varray 0; interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end @@ -560,7 +562,9 @@ let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci let type_of_switch sw = - push_vstack sw.sw_stk; + (* The fun code of types will make sure we have enough stack, so we put 0 + here. *) + push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = @@ -580,9 +584,10 @@ let branch_arg k (tag,arity) = let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then - (push_ra stop;push_vstack sw.sw_stk) + (push_ra stop;push_vstack sw.sw_stk sw.sw_annot.max_stack_size) else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + (push_vstack sw.sw_stk sw.sw_annot.max_stack_size; + push_ra (popstop_code (Array.length sw.sw_stk))); interprete sw.sw_code arg sw.sw_env 0 let branch_of_switch k sw = diff --git a/lib/cErrors.ml b/lib/cErrors.ml index c69c7e4001..5c56192fc5 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -16,6 +16,16 @@ let push = Backtrace.add_backtrace exception Anomaly of string option * std_ppcmds (* System errors *) +(* XXX: To move to common tagging functions in Pp, blocked on tag + * system cleanup as we cannot define generic error tags now. + * + * Anyways, tagging should not happen here, but in the specific + * listener to the msg_* stuff. + *) +let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc () +let err_str = tag_err_str "Error:" +let ann_str = tag_err_str "Anomaly:" + let _ = let pr = function | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"") @@ -93,7 +103,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ + hov 0 (ann_str ++ raw_anomaly e ++ spc () ++ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else @@ -115,7 +125,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (str "Error: " ++ where (Some s) ++ pps) + hov 0 (err_str ++ where (Some s) ++ pps) | _ -> raise Unhandled end diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 720f54606c..1a1944d61f 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 let current_loc = ref Loc.ghost -let flags = ref "default" +let flags = ref "" let set_current_loc = (:=) current_loc @@ -62,7 +62,7 @@ let set_warning_status ~name status = try let w = Hashtbl.find warnings name in Hashtbl.replace warnings name { w with status = status } - with Not_found -> warn_unknown_warning name + with Not_found -> () let reset_default_warnings () = Hashtbl.iter (fun name w -> @@ -74,6 +74,13 @@ let set_all_warnings_status status = Hashtbl.replace warnings name { w with status }) warnings +let set_category_status ~name status = + let names = Hashtbl.find categories name in + List.iter (fun name -> set_warning_status name status) names + +let is_all_keyword name = CString.equal name "all" +let is_none_keyword s = CString.equal s "none" + let parse_flag s = if String.length s > 1 then match String.get s 0 with @@ -82,39 +89,94 @@ let parse_flag s = | _ -> (Enabled, s) else CErrors.error "Invalid warnings flag" -let rec do_all_keyword = function - | [] -> [] - | (status, name as item) :: items -> - if CString.equal name "all" then - (set_all_warnings_status status; do_all_keyword items) - else item :: do_all_keyword items - -let rec do_categories = function - | [] -> [] - | (status, name as item) :: items -> - try - let names = Hashtbl.find categories name in - List.iter (fun name -> set_warning_status name status) names; - do_categories items - with Not_found -> item :: do_categories items +let string_of_flag (status,name) = + match status with + | AsError -> "+" ^ name + | Disabled -> "-" ^ name + | Enabled -> name + +let string_of_flags flags = + String.concat "," (List.map string_of_flag flags) + +let set_status ~name status = + if is_all_keyword name then + set_all_warnings_status status + else + try + set_category_status ~name status + with Not_found -> + try + set_warning_status ~name status + with Not_found -> () + +let split_flags s = + let reg = Str.regexp "[ ,]+" in Str.split reg s + +let check_warning ~silent (_status,name) = + is_all_keyword name || + Hashtbl.mem categories name || + Hashtbl.mem warnings name || + (if not silent then warn_unknown_warning name; false) + +(** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the + "all" flag, and reverses the list. *) +let rec cut_before_all_rev acc = function + | [] -> acc + | (_status,name as w) :: warnings -> + cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings + +let cut_before_all_rev warnings = cut_before_all_rev [] warnings + +(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of + themselves or their categories, and reverses the list. *) +let uniquize_flags_rev flags = + let rec aux acc visited = function + | (_,name as flag)::flags -> + if CString.Set.mem name visited then aux acc visited flags else + let visited = + try + let warnings = Hashtbl.find categories name in + List.fold_left (fun v w -> CString.Set.add w v) visited warnings + with Not_found -> + visited + in + aux (flag::acc) (CString.Set.add name visited) flags + | [] -> acc + in aux [] CString.Set.empty flags + +(** [normalize_flags] removes unknown or redundant warnings. If [silent] is + true, it emits a warning when an unknown warning is met. *) +let normalize_flags ~silent warnings = + let warnings = List.filter (check_warning ~silent) warnings in + let warnings = cut_before_all_rev warnings in + uniquize_flags_rev warnings + +let flags_of_string s = List.map parse_flag (split_flags s) + +let normalize_flags_string s = + if is_none_keyword s then s + else + let flags = flags_of_string s in + let flags = normalize_flags ~silent:false flags in + string_of_flags flags let rec parse_warnings items = - List.iter (fun (status, name) -> set_warning_status ~name status) items + CList.iter (fun (status, name) -> set_status ~name status) items (* For compatibility, we accept "none" *) -let parse_flags s = - if CString.equal s "none" then begin +let parse_flags s = + if is_none_keyword s then begin Flags.make_warn false; - set_all_warnings_status Disabled + set_all_warnings_status Disabled; + "none" end else begin Flags.make_warn true; - let reg = Str.regexp "[ ,]+" in - let items = List.map parse_flag (Str.split reg s) in - let items = do_all_keyword items in - let items = do_categories items in - parse_warnings items + let flags = flags_of_string s in + let flags = normalize_flags ~silent:true flags in + parse_warnings flags; + string_of_flags flags end let set_flags s = - flags := s; reset_default_warnings (); parse_flags s + reset_default_warnings (); let s = parse_flags s in flags := s diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index 3515542840..3f6cee31b7 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -6,29 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type status = - Disabled | Enabled | AsError - -(* -type 'a repr = { - print : 'a -> Pp.std_ppcmds; - kind : string; - enabled : bool; -} - *) +type status = Disabled | Enabled | AsError val set_current_loc : Loc.t -> unit val create : name:string -> category:string -> ?default:status -> ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit -(* -val emit : 'a t -> 'a -> unit - -type any = Any : string * string * 'a repr -> any - -val dump : unit -> any list - *) - val get_flags : unit -> string val set_flags : string -> unit + +(** Cleans up a user provided warnings status string, e.g. removing unknown + warnings (in which case a warning is emitted) or subsumed warnings . *) +val normalize_flags_string : string -> string diff --git a/lib/stateid.ml b/lib/stateid.ml index 500581a39e..ae25735c5f 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -22,7 +22,7 @@ let to_int id = id let newer_than id1 id2 = id1 > id2 let state_id_info : (t * t) Exninfo.t = Exninfo.make () -let add exn ?(valid = initial) id = +let add exn ~valid id = Exninfo.add exn state_id_info (valid, id) let get exn = Exninfo.get exn state_id_info diff --git a/lib/stateid.mli b/lib/stateid.mli index cd8fddf0ce..1d87a343b3 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -26,9 +26,8 @@ val newer_than : t -> t -> bool (* Attaches to an exception the concerned state id, plus an optional * state id that is a valid state id before the error. - * Backtracking to the valid id is safe. - * The initial_state_id is assumed to be safe. *) -val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info + * Backtracking to the valid id is safe. *) +val add : Exninfo.info -> valid:t -> t -> Exninfo.info val get : Exninfo.info -> (t * t) option type ('a,'b) request = { diff --git a/library/goptions.ml b/library/goptions.ml index 35616558a6..9dc0f40588 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -247,7 +247,7 @@ let get_locality = function | Some false -> OptGlobal | None -> OptDefault -let declare_option cast uncast append +let declare_option cast uncast append ?(preprocess = fun x -> x) { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in @@ -275,10 +275,11 @@ let declare_option cast uncast append subst_function = subst_options; discharge_function = discharge_options; classify_function = classify_options } in - (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v))) + (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) else (fun _ m v -> - match m with + let v = preprocess v in + match m with | OptSet -> write v | OptAppend -> write (append (read ()) v)) in @@ -381,9 +382,9 @@ let msg_option_value (name,v) = | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" - | StringValue s -> str s + | StringValue s -> str "\"" ++ str s ++ str "\"" | StringOptValue None -> str"undefined" - | StringOptValue (Some s) -> str s + | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\"" (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = diff --git a/library/goptions.mli b/library/goptions.mli index ca2df07104..3b3651f393 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -122,13 +122,19 @@ type 'a option_sig = { (** When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) +(** The [preprocess] function is triggered before setting the option. It can be + used to emit a warning on certain values, and clean-up the final value. *) type 'a write_function = 'a -> unit -val declare_int_option : int option option_sig -> int option write_function -val declare_bool_option : bool option_sig -> bool write_function -val declare_string_option: string option_sig -> string write_function -val declare_stringopt_option: string option option_sig -> string option write_function +val declare_int_option : ?preprocess:(int option -> int option) -> + int option option_sig -> int option write_function +val declare_bool_option : ?preprocess:(bool -> bool) -> + bool option_sig -> bool write_function +val declare_string_option: ?preprocess:(string -> string) -> + string option_sig -> string write_function +val declare_stringopt_option: ?preprocess:(string option -> string option) -> + string option option_sig -> string option write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/library/impargs.ml b/library/impargs.ml index bce7a15cbe..828d652c83 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -491,13 +491,15 @@ let implicits_of_global ref = let l = Refmap.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in - let rename imp name = match imp, name with - | Some (_, x,y), Name id -> Some (id, x,y) - | _ -> imp in - List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l + let rec rename implicits names = match implicits, names with + | [], _ -> [] + | _, [] -> implicits + | Some (_, x,y) :: implicits, Name id :: names -> + Some (id, x,y) :: rename implicits names + | imp :: implicits, _ :: names -> imp :: rename implicits names + in + List.map (fun (t, il) -> t, rename il rename_l) l with Not_found -> l - | Invalid_argument _ -> - anomaly (Pp.str "renamings list and implicits list have different lenghts") with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = @@ -657,7 +659,7 @@ let check_inclusion l = let rec aux = function | n1::(n2::_ as nl) -> if n1 <= n2 then - error "Sequences of implicit arguments must be of different lengths"; + error "Sequences of implicit arguments must be of different lengths."; aux nl | _ -> () in aux (List.map (fun (imps,_) -> List.length imps) l) diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index e1c9fed637..5cbddc7f64 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -385,6 +385,8 @@ let skip_extensions trace = | [] -> [] in List.rev (aux (List.rev trace)) +let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 + let extract_ltac_trace trace eloc = let trace = skip_extensions trace in let (loc,c),tail = List.sep_last trace in @@ -392,11 +394,10 @@ let extract_ltac_trace trace eloc = (* We entered a user-defined tactic, we display the trace with location of the call *) let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in - Some msg, loc + Some msg, if finer_loc eloc loc then eloc else loc else (* We entered a primitive tactic, we don't display trace but report on the finest location *) - let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 in let best_loc = (* trace is with innermost call coming first *) let rec aux best_loc = function diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 8a8e41956a..a0cf631ea8 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -105,7 +105,7 @@ module Error = struct Printf.sprintf "Unsupported Unicode character (0x%x)" x) (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) + let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x)) end open Error @@ -573,7 +573,7 @@ let rec next_token loc = parser bp comment_stop bp; between_commands := new_between_commands; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in - comment_stop bp; (t, set_loc_pos loc ep bp) + comment_stop bp; (t, set_loc_pos loc bp ep) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail loc (store 0 c); s >] ep -> let id = get_buff len in @@ -593,6 +593,12 @@ let rec next_token loc = parser bp let loc = comment loc bp s in next_token loc s | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> t + | [< ' ('{' | '}' as c); s >] ep -> + let t,new_between_commands = + if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true + else process_chars loc bp c s, false + in + comment_stop bp; between_commands := new_between_commands; t | [< s >] -> match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, n) -> @@ -603,9 +609,7 @@ let rec next_token loc = parser bp (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) -> let t = process_chars loc bp (Stream.next s) s in - let new_between_commands = match t with - (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in - comment_stop bp; between_commands := new_between_commands; t + comment_stop bp; t | EmptyStream -> comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index bc02a46218..8f86abcf3d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -580,6 +580,12 @@ let warn_deprecated_implicit_arguments = CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") +let warn_deprecated_arguments_syntax = + CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated" + (fun () -> strbrk "The \"/\" modifier has an effect only in the first " + ++ strbrk "arguments list. The syntax allowing it to appear" + ++ strbrk " in other lists is deprecated.") + (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name; @@ -651,58 +657,32 @@ GEXTEND Gram (* Arguments *) | IDENT "Arguments"; qid = smart_global; - impl = LIST1 [ l = LIST0 - [ item = argument_spec -> - let name, recarg_like, notation_scope = item in - [`Id { name=name; recarg_like=recarg_like; - notation_scope=notation_scope; - implicit_status = `NotImplicit}] - | "/" -> [`Slash] - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = `NotImplicit}) items - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = `Implicit}) items - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = `MaximallyImplicit}) items - ] -> l ] SEP ","; + args = LIST0 argument_spec_block; + more_implicits = OPT + [ ","; impl = LIST1 + [ impl = LIST0 more_implicits_block -> + let warn_slash = List.exists fst impl in + if warn_slash then warn_deprecated_arguments_syntax ~loc:!@loc (); + List.flatten (List.map snd impl)] + SEP "," -> impl + ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in - let impl = List.map List.flatten impl in - let rec aux n (narg, impl) = function - | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl - | `Slash :: tl -> aux (n+1) (n, impl) tl - | [] -> narg, impl in - let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in - let nargs, rest = List.hd nargs, List.tl nargs in - if List.exists (fun arg -> not (Int.equal arg nargs)) rest then - error "All arguments lists must have the same length"; - let err_incompat x y = - error ("Options \""^x^"\" and \""^y^"\" are incompatible") in - if nargs > 0 && List.mem `ReductionNeverUnfold mods then - err_incompat "simpl never" "/"; - if List.mem `ReductionNeverUnfold mods && - List.mem `ReductionDontExposeCase mods then - err_incompat "simpl never" "simpl nomatch"; - VernacArguments (qid, impl, nargs, mods) - + let slash_position = ref None in + let rec parse_args i = function + | [] -> [] + | `Id x :: args -> x :: parse_args (i+1) args + | `Slash :: args -> + if Option.is_empty !slash_position then + (slash_position := Some i; parse_args i args) + else + error "The \"/\" modifier can occur only once" + in + let args = parse_args 0 (List.flatten args) in + let more_implicits = Option.default [] more_implicits in + VernacArguments (qid, args, more_implicits, !slash_position, mods) + + (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> @@ -759,6 +739,50 @@ GEXTEND Gram snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s ] ]; + (* List of arguments implicit status, scope, modifiers *) + argument_spec_block: [ + [ item = argument_spec -> + let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = NotImplicit}] + | "/" -> [`Slash] + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = NotImplicit}) items + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = Implicit}) items + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = MaximallyImplicit}) items + ] + ]; + (* Same as [argument_spec_block], but with only implicit status and names *) + more_implicits_block: [ + [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)]) + | "/" -> (true (* Should warn about deprecated syntax *), []) + | "["; items = LIST1 name; "]" -> + (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items) + | "{"; items = LIST1 name; "}" -> + (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items) + ] + ]; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque @@ -852,11 +876,16 @@ GEXTEND Gram | "Set"; table = option_table; v = option_value -> begin match v with | StringValue s -> - let (last, prefix) = List.sep_last table in - if String.equal last "Append" && not (List.is_empty prefix) then - VernacSetAppendOption (prefix, s) + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + VernacSetAppendOption (table, s) else - VernacSetOption (table, v) + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) | _ -> VernacSetOption (table, v) end | "Set"; table = option_table -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62f3071151..fa84e4ddf3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1538,7 +1538,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num begin if do_observe () then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) - else anomaly (Pp.str "Cannot create equation Lemma") + else CErrors.errorlabstrm "Cannot create equation Lemma" + (str "Cannot create equation lemma." ++ spc () ++ + str "This may be because the function is nested-recursive.") ; true end diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae7..cf9a429455 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -112,8 +112,7 @@ let guard_term ch1 s i = match s.[i] with (* The call 'guard s i' should return true if the contents of s *) (* starting at i need bracketing to avoid ambiguities. *) let pr_guarded guard prc c = - msg_with Format.str_formatter (prc c); - let s = Format.flush_str_formatter () ^ "$" in + let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) let pr_constr = pr_constr @@ -908,9 +907,47 @@ let glob_ssrterm gs = function fst x, Some c | ct -> ct +(* This piece of code asserts the following notations are reserved *) +(* Reserved Notation "( a 'in' b )" (at level 0). *) +(* Reserved Notation "( a 'as' b )" (at level 0). *) +(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) +(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) +let glob_cpattern gs p = + pp(lazy(str"globbing pattern: " ++ pr_term p)); + let glob x = snd (glob_ssrterm gs (mk_lterm x)) in + let encode k s l = + let name = Name (id_of_string ("_ssrpat_" ^ s)) in + k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in + let bind_in t1 t2 = + let d = dummy_loc in let n = Name (destCVar t1) in + fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in + let check_var t2 = if not (isCVar t2) then + loc_error (constr_loc t2) "Only identifiers are allowed here" in + match p with + | _, (_, None) as x -> x + | k, (v, Some t) as orig -> + if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else + match t with + | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> + (try match glob t1, glob t2 with + | (r1, None), (r2, None) -> encode k "In" [r1;r2] + | (r1, Some _), (r2, Some _) when isCVar t1 -> + encode k "In" [r1; r2; bind_in t1 t2] + | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] + | _ -> CErrors.anomaly (str"where are we?") + with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) + | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] + | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> + encode k "As" [fst (glob t1); fst (glob t2)] + | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] + | _ -> glob_ssrterm gs orig +;; + let glob_rpattern s p = match p with - | T t -> T (glob_ssrterm s t) + | T t -> T (glob_cpattern s t) | In_T t -> In_T (glob_ssrterm s t) | X_In_T(x,t) -> X_In_T (x,glob_ssrterm s t) | In_X_In_T(x,t) -> In_X_In_T (x,glob_ssrterm s t) @@ -995,44 +1032,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with | _ -> ' ' let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind -(* This piece of code asserts the following notations are reserved *) -(* Reserved Notation "( a 'in' b )" (at level 0). *) -(* Reserved Notation "( a 'as' b )" (at level 0). *) -(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) -(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) -let glob_cpattern gs p = - pp(lazy(str"globbing pattern: " ++ pr_term p)); - let glob x = snd (glob_ssrterm gs (mk_lterm x)) in - let encode k s l = - let name = Name (id_of_string ("_ssrpat_" ^ s)) in - k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in - let bind_in t1 t2 = - let d = dummy_loc in let n = Name (destCVar t1) in - fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in - let check_var t2 = if not (isCVar t2) then - loc_error (constr_loc t2) "Only identifiers are allowed here" in - match p with - | _, (_, None) as x -> x - | k, (v, Some t) as orig -> - if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else - match t with - | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> - (try match glob t1, glob t2 with - | (r1, None), (r2, None) -> encode k "In" [r1;r2] - | (r1, Some _), (r2, Some _) when isCVar t1 -> - encode k "In" [r1; r2; bind_in t1 t2] - | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> CErrors.anomaly (str"where are we?") - with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> - check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> - encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> - check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] - | _ -> glob_ssrterm gs orig -;; - let interp_ssrterm _ gl t = Tacmach.project gl, t ARGUMENT EXTEND cpattern diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ca1d0b7fba..e18aece090 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -16,12 +16,12 @@ open Libobject (*i*) let name_table = - Summary.ref (Refmap.empty : Name.t list list Refmap.t) + Summary.ref (Refmap.empty : Name.t list Refmap.t) ~name:"rename-arguments" type req = | ReqLocal - | ReqGlobal of global_reference * Name.t list list + | ReqGlobal of global_reference * Name.t list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table @@ -49,7 +49,7 @@ let discharge_rename_args = function let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in + let names' = var_names @ names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) | _ -> None @@ -83,7 +83,7 @@ let rec rename_prod c = function | _ -> c let rename_type ty ref = - try rename_prod ty (List.hd (arguments_names ref)) + try rename_prod ty (arguments_names ref) with Not_found -> ty let rename_type_of_constant env c = diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index a334055011..e123e77862 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -11,10 +11,10 @@ open Globnames open Environ open Term -val rename_arguments : bool -> global_reference -> Name.t list list -> unit +val rename_arguments : bool -> global_reference -> Name.t list -> unit -(** [Not_found] is raised is no names are defined for [r] *) -val arguments_names : global_reference -> Name.t list list +(** [Not_found] is raised if no names are defined for [r] *) +val arguments_names : global_reference -> Name.t list val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5c9ce2624c..aa24733d9f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -64,10 +64,11 @@ let error_wrong_numarg_inductive_loc loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> + let e = CErrors.push e in aux (e::errors) t in aux [] l diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3680cd777a..28600ad153 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1175,9 +1175,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 +let error_cannot_unify env evd pb ?reason t1 t2 = + Pretype_errors.error_cannot_unify_loc + (loc_of_conv_pb evd pb) env + evd ?reason (t1, t2) + let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () let max_undefined_with_candidates evd = @@ -1246,17 +1251,15 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd ~reason (t1, t2)) + error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd (t1, t2) + (* There remains stuck problems *) + error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cfb4e79f03..5455ab891a 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1023,7 +1023,7 @@ module Make str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") impls) ) - | VernacArguments (q, impl, nargs, mods) -> + | VernacArguments (q, args, more_implicits, nargs, mods) -> return ( hov 2 ( keyword "Arguments" ++ spc() ++ @@ -1031,19 +1031,28 @@ module Make let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in let pr_if b x = if b then x else str "" in let pr_br imp x = match imp with - | `Implicit -> str "[" ++ x ++ str "]" - | `MaximallyImplicit -> str "{" ++ x ++ str "}" - | `NotImplicit -> x in - let rec aux n l = + | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" + | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}" + | Vernacexpr.NotImplicit -> x in + let rec print_arguments n l = match n, l with - | 0, l -> spc () ++ str"/" ++ aux ~-1 l + | Some 0, l -> spc () ++ str"/" ++ print_arguments None l | _, [] -> mt() | n, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ - aux (n-1) tl in - prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ + print_arguments (Option.map pred n) tl + in + let rec print_implicits = function + | [] -> mt () + | (name, impl) :: rest -> + spc() ++ pr_br impl (pr_name name) ++ print_implicits rest + in + print_arguments nargs args ++ + if not (List.is_empty more_implicits) then + str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function | `ReductionDontExposeCase -> keyword "simpl nomatch" diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9a..b590a8c930 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -241,7 +241,7 @@ let print_name_infos ref = let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in let renames = - try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in + try Arguments_renaming.arguments_names ref with Not_found -> [] in let type_info_for_implicit = if need_expansion (select_impargs_size 0 impls) ref then (* Need to reduce since implicits are computed with products flattened *) @@ -281,7 +281,7 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids (fun r -> - try List.hd (Arguments_renaming.arguments_names r) with Not_found -> []) + try Arguments_renaming.arguments_names r with Not_found -> []) ((!=) Anonymous) print_renames_list diff --git a/stm/stm.ml b/stm/stm.ml index 32185247f2..e387e6322f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -746,7 +746,7 @@ module State : sig val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool - val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn + val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn (* to send states across worker/master *) type frozen_state val get_cached : Stateid.t -> frozen_state @@ -854,14 +854,14 @@ end = struct (* {{{ *) VCS.set_state id (Valid s) with VCS.Expired -> () - let exn_on id ?valid (e, info) = + let exn_on id ~valid (e, info) = match Stateid.get info with | Some _ -> (e, info) | None -> let loc = Option.default Loc.ghost (Loc.get_loc info) in let (e, info) = Hooks.(call_process_error_once (e, info)) in Hooks.(call execution_error id loc (iprint (e, info))); - (e, Stateid.add info ?valid id) + (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = let s1 = States.summary_of_state s1 in @@ -2354,7 +2354,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 -let merge_proof_branch ?valid ?id qast keep brname = +let merge_proof_branch ~valid ?id qast keep brname = let brinfo = VCS.get_branch brname in let qed fproof = { qast; keep; brname; brinfo; fproof } in match brinfo with @@ -2377,7 +2377,7 @@ let merge_proof_branch ?valid ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) + iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) @@ -2446,9 +2446,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in + let valid = VCS.get_branch_pos head in List.iter (fun branch -> if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch x VtDrop branch)) + ignore(merge_proof_branch ~valid x VtDrop branch)) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); let head = VCS.current_branch () in @@ -2543,8 +2544,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty detect_proof_block id cblock; *) Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> - let valid = if tty then Some(VCS.get_branch_pos head) else None in - let rc = merge_proof_branch ?valid ~id:newtip x keep head in + let valid = VCS.get_branch_pos head in + let rc = merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); rc diff --git a/tactics/auto.ml b/tactics/auto.ml index 0f5b74d9da..bc6448577f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -35,6 +35,10 @@ open Hints let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l +let compute_secvars gl = + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + secvars_of_hyps hyps + (* tell auto not to reuse already instantiated metas in unification (for compatibility, since otherwise, apply succeeds oftener) *) @@ -260,19 +264,19 @@ let pr_info_atom (d,pp) = let pr_info_trace = function | (Info,_,{contents=(d,Some pp)::l}) -> - Feedback.msg_debug (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) + Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) | _ -> () let pr_info_nop = function - | (Info,_,_) -> Feedback.msg_debug (str "idtac.") + | (Info,_,_) -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function | (Off,_,_) -> () | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)") | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") - | (Info,0,_) -> Feedback.msg_debug (str "(* info trivial: *)") - | (Info,_,_) -> Feedback.msg_debug (str "(* info auto: *)") + | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)") + | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)") let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in @@ -295,12 +299,13 @@ let flags_of_state st = let auto_flags_of_state st = auto_unif_flags_of full_transparent_state st false -let hintmap_of hdc concl = +let hintmap_of secvars hdc concl = match hdc with - | None -> Hint_db.map_none + | None -> Hint_db.map_none ~secvars | Some hdc -> - if occur_existential concl then Hint_db.map_existential hdc concl - else Hint_db.map_auto hdc concl + if occur_existential concl then + Hint_db.map_existential ~secvars hdc concl + else Hint_db.map_auto ~secvars hdc concl let exists_evaluable_reference env = function | EvalConstRef _ -> true @@ -325,22 +330,23 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = in Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in + let secvars = compute_secvars gl in Tacticals.New.tclFIRST ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE - (trivial_resolve dbg mod_delta db_list local_db concl))) + (trivial_resolve dbg mod_delta db_list local_db secvars concl))) end } -and my_find_search_nodelta db_list local_db hdc concl = +and my_find_search_nodelta db_list local_db secvars hdc concl = List.map (fun hint -> (None,hint)) - (List.map_append (hintmap_of hdc concl) (local_db::db_list)) + (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list)) and my_find_search mod_delta = if mod_delta then my_find_search_delta else my_find_search_nodelta -and my_find_search_delta db_list local_db hdc concl = - let f = hintmap_of hdc concl in +and my_find_search_delta db_list local_db secvars hdc concl = + let f = hintmap_of secvars hdc concl in if occur_existential concl then List.map_append (fun db -> @@ -360,11 +366,11 @@ and my_find_search_delta db_list local_db hdc concl = let (ids, csts as st) = Hint_db.transparent_state db in let flags, l = let l = - match hdc with None -> Hint_db.map_none db + match hdc with None -> Hint_db.map_none ~secvars db | Some hdc -> if (Id.Pred.is_empty ids && Cpred.is_empty csts) - then Hint_db.map_auto hdc concl db - else Hint_db.map_existential hdc concl db + then Hint_db.map_auto ~secvars hdc concl db + else Hint_db.map_existential ~secvars hdc concl db in auto_flags_of_state st, l in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) @@ -397,7 +403,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= in tclLOG dbg pr_hint (run_hint t tactic) -and trivial_resolve dbg mod_delta db_list local_db cl = +and trivial_resolve dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound cl in @@ -406,7 +412,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl = in List.map (tac_of_hint dbg db_list local_db cl) (priority - (my_find_search mod_delta db_list local_db head cl)) + (my_find_search mod_delta db_list local_db secvars head cl)) with Not_found -> [] (** The use of the "core" database can be de-activated by passing @@ -444,7 +450,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l (* The classical Auto tactic *) (**************************************************************************) -let possible_resolve dbg mod_delta db_list local_db cl = +let possible_resolve dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound cl in @@ -452,7 +458,7 @@ let possible_resolve dbg mod_delta db_list local_db cl = with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) - (my_find_search mod_delta db_list local_db head cl) + (my_find_search mod_delta db_list local_db secvars head cl) with Not_found -> [] let extend_local_db decl db gl = @@ -483,11 +489,12 @@ let search d n mod_delta db_list local_db = (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) ( Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in + let secvars = compute_secvars gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) - (possible_resolve d mod_delta db_list local_db concl)) + (possible_resolve d mod_delta db_list local_db secvars concl)) end })) end [] in diff --git a/tactics/auto.mli b/tactics/auto.mli index 04791a526e..3befaaadeb 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -15,6 +15,8 @@ open Pattern open Decl_kinds open Hints +val compute_secvars : ('a,'b) Proofview.Goal.t -> Id.Pred.t + val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0944cbe38f..9cb6b7fe78 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -280,11 +280,11 @@ let clenv_of_prods poly nprods (c, clenv) gl = let ty = Retyping.get_type_of (Proofview.Goal.env gl) (Sigma.to_evar_map (Proofview.Goal.sigma gl)) c in let diff = nb_prod ty - nprods in - if Pervasives.(>=) diff 0 then - (* Was Some clenv... *) - Some (Some diff, - Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) - else None + if Pervasives.(>=) diff 0 then + (* Was Some clenv... *) + Some (Some diff, + Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) + else None let with_prods nprods poly (c, clenv) f = if get_typeclasses_limit_intros () then @@ -339,7 +339,7 @@ let shelve_dependencies gls = shelve_goals gls) (** Hack to properly solve dependent evars that are typeclasses *) -let rec e_trivial_fail_db only_classes db_list local_db = +let rec e_trivial_fail_db only_classes db_list local_db secvars = let open Tacticals.New in let open Tacmach.New in let trivial_fail = @@ -350,13 +350,13 @@ let rec e_trivial_fail_db only_classes db_list local_db = let d = pf_last_hyp gl in let hintl = make_resolve_hyp env sigma d in let hints = Hint_db.add_list env sigma hintl local_db in - e_trivial_fail_db only_classes db_list hints + e_trivial_fail_db only_classes db_list hints secvars end } in let trivial_resolve = Proofview.Goal.nf_enter { enter = begin fun gl -> - let tacs = e_trivial_resolve db_list local_db only_classes + let tacs = e_trivial_resolve db_list local_db secvars only_classes (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end} @@ -367,7 +367,7 @@ let rec e_trivial_fail_db only_classes db_list local_db = in tclFIRST (List.map tclCOMPLETE tacl) -and e_my_find_search db_list local_db hdc complete only_classes sigma concl = +and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl = let open Proofview.Notations in let prods, concl = decompose_prod_assum concl in let nprods = List.length prods in @@ -384,15 +384,15 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = (fun db -> let tacs = if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto hdc concl db - else Hint_db.map_existential hdc concl db + Hint_db.map_eauto secvars hdc concl db + else Hint_db.map_existential secvars hdc concl db in let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) tacs) (local_db::db_list) in let tac_of_hint = - fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> + fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) -> let tac = function | Res_pf (term,cl) -> if get_typeclasses_filtered_unification () then @@ -429,7 +429,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = | Res_pf_THEN_trivial_fail (term,cl) -> let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in let snd = if complete then Tacticals.New.tclIDTAC - else e_trivial_fail_db only_classes db_list local_db in + else e_trivial_fail_db only_classes db_list local_db secvars in Tacticals.New.tclTHEN fst snd | Unfold_nth c -> let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in @@ -449,15 +449,15 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp)) in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db only_classes sigma concl = +and e_trivial_resolve db_list local_db secvars only_classes sigma concl = try - e_my_find_search db_list local_db + e_my_find_search db_list local_db secvars (decompose_app_bound concl) true only_classes sigma concl with Bound | Not_found -> [] -let e_possible_resolve db_list local_db only_classes sigma concl = +let e_possible_resolve db_list local_db secvars only_classes sigma concl = try - e_my_find_search db_list local_db + e_my_find_search db_list local_db secvars (decompose_app_bound concl) false only_classes sigma concl with Bound | Not_found -> [] @@ -673,7 +673,8 @@ module V85 = struct let env = Goal.V82.env s gl in let concl = Goal.V82.concl s gl in let tacgl = {it = gl; sigma = s;} in - let poss = e_possible_resolve hints info.hints info.only_classes s concl in + let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in + let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in let unique = is_unique env concl in let rec aux i foundone = function | (tac, _, extern, name, pp) :: tl -> @@ -1004,8 +1005,9 @@ module Search = struct Printer.pr_constr_env (Goal.env gl) s concl ++ (if backtrack then str" with backtracking" else str" without backtracking")); + let secvars = compute_secvars gl in let poss = - e_possible_resolve hints info.search_hints info.search_only_classes s concl in + e_possible_resolve hints info.search_hints secvars info.search_only_classes s concl in (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 480185337b..23ff582253 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -119,12 +119,13 @@ let unify_e_resolve poly flags (c,clenv) = (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls) end } -let hintmap_of hdc concl = +let hintmap_of secvars hdc concl = match hdc with - | None -> fun db -> Hint_db.map_none db + | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> - if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db) - else (fun db -> Hint_db.map_auto hdc concl db) + if occur_existential concl then + (fun db -> Hint_db.map_existential ~secvars hdc concl db) + else (fun db -> Hint_db.map_auto ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) let e_exact poly flags (c,clenv) = @@ -142,16 +143,17 @@ let rec e_trivial_fail_db db_list local_db = e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db) end } in Proofview.Goal.enter { enter = begin fun gl -> + let secvars = compute_secvars gl in let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) + (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end } -and e_my_find_search db_list local_db hdc concl = - let hint_of_db = hintmap_of hdc concl in +and e_my_find_search db_list local_db secvars hdc concl = + let hint_of_db = hintmap_of secvars hdc concl in let hintl = List.map_append (fun db -> let flags = auto_flags_of_state (Hint_db.transparent_state db) in @@ -179,14 +181,15 @@ and e_my_find_search db_list local_db hdc concl = in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db gl = +and e_trivial_resolve db_list local_db secvars gl = let hd = try Some (decompose_app_bound gl) with Bound -> None in - try priority (e_my_find_search db_list local_db hd gl) + try priority (e_my_find_search db_list local_db secvars hd gl) with Not_found -> [] -let e_possible_resolve db_list local_db gl = +let e_possible_resolve db_list local_db secvars gl = let hd = try Some (decompose_app_bound gl) with Bound -> None in - try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl) + try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) + (e_my_find_search db_list local_db secvars hd gl) with Not_found -> [] let find_first_goal gls = @@ -255,9 +258,11 @@ module SearchProblem = struct let nbgl = List.length (sig_it lg) in assert (nbgl > 0); let g = find_first_goal lg in + let hyps = pf_ids_of_hyps g in + let secvars = secvars_of_hyps (pf_hyps g) in let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in let assumption_tacs = - let tacs = List.map map_assum (pf_ids_of_hyps g) in + let tacs = List.map map_assum hyps in let l = filter_tactics s.tacres tacs in List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; last_tactic = pp; dblist = s.dblist; @@ -283,7 +288,8 @@ module SearchProblem = struct let rec_tacs = let l = let concl = Reductionops.nf_evar (project g)(pf_concl g) in - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl) + filter_tactics s.tacres + (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl) in List.map (fun (lgls, cost, pp) -> @@ -346,13 +352,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> Feedback.msg_debug (str "idtac.") + | Info -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") - | Info -> Feedback.msg_debug (str "(* info eauto: *)") + | Info -> Feedback.msg_info (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () @@ -363,7 +369,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) diff --git a/tactics/hints.ml b/tactics/hints.ml index 1ebd32c378..ba92b74dfe 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -66,6 +66,24 @@ let decompose_app_bound t = | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args | _ -> raise Bound +(** Compute the set of section variables that remain in the named context. + Starts from the top to the bottom of the context, stops at the first + different declaration between the named hyps and the section context. *) +let secvars_of_hyps hyps = + let secctx = Global.named_context () in + let pred, all = + List.fold_left (fun (pred,all) decl -> + try let _ = Context.Named.lookup (get_id decl) hyps in + (* Approximation, it might be an hypothesis reintroduced with same name and unconvertible types, + we must allow it currently, as comparing the declarations for syntactic equality is too + strong a check (e.g. an unfold in a section variable would make it unusable). *) + (Id.Pred.add (get_id decl) pred, all) + with Not_found -> (pred, false)) + (Id.Pred.empty,true) secctx + in + if all then Id.Pred.full (* If the whole section context is available *) + else pred + (************************************************************************) (* The Type of Constructions Autotactic Hints *) (************************************************************************) @@ -104,12 +122,13 @@ type raw_hint = constr * types * Univ.universe_context_set type hint = (raw_hint * clausenv) hint_ast with_uid type 'a with_metadata = { - pri : int; (* A number lower is higher priority *) - poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) - pat : constr_pattern option; (* A pattern for the concl of the Goal *) - name : hints_path_atom; (* A potential name to refer to the hint *) + pri : int; (* A number lower is higher priority *) + poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) + pat : constr_pattern option; (* A pattern for the concl of the Goal *) + name : hints_path_atom; (* A potential name to refer to the hint *) db : string option; (** The database from which the hint comes *) - code : 'a; (* the tactic to apply when the concl matches pat *) + secvars : Id.Pred.t; (* The set of section variables the hint depends on *) + code : 'a; (* the tactic to apply when the concl matches pat *) } type full_hint = hint with_metadata @@ -418,11 +437,14 @@ sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t val find : global_reference -> t -> search_entry -val map_none : t -> full_hint list -val map_all : global_reference -> t -> full_hint list -val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list -val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list -val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list +val map_none : secvars:Id.Pred.t -> t -> full_hint list +val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list +val map_existential : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list +val map_eauto : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list +val map_auto : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t val remove_one : global_reference -> t -> t @@ -471,7 +493,11 @@ struct try Constr_map.find key db.hintdb_map with Not_found -> empty_se - let realize_tac (id,tac) = tac + let realize_tac secvars (id,tac) = + if Id.Pred.subset tac.secvars secvars then Some tac + else + (** Warn about no longer typable hint? *) + None let match_mode m arg = match m with @@ -489,40 +515,40 @@ struct if List.is_empty modes then true else List.exists (matches_mode args) modes - let merge_entry db nopat pat = + let merge_entry secvars db nopat pat = let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in let h = List.merge pri_order_int h nopat in let h = List.merge pri_order_int h pat in - List.map realize_tac h + List.map_filter (realize_tac secvars) h - let map_none db = - merge_entry db [] [] + let map_none ~secvars db = + merge_entry secvars db [] [] - let map_all k db = + let map_all ~secvars k db = let se = find k db in - merge_entry db se.sentry_nopat se.sentry_pat + merge_entry secvars db se.sentry_nopat se.sentry_pat (** Precondition: concl has no existentials *) - let map_auto (k,args) concl db = + let map_auto ~secvars (k,args) concl db = let se = find k db in let st = if db.use_dn then (Some db.hintdb_state) else None in let pat = lookup_tacs concl st se in - merge_entry db [] pat + merge_entry secvars db [] pat - let map_existential (k,args) concl db = + let map_existential ~secvars (k,args) concl db = let se = find k db in if matches_modes args se.sentry_mode then - merge_entry db se.sentry_nopat se.sentry_pat - else merge_entry db [] [] + merge_entry secvars db se.sentry_nopat se.sentry_pat + else merge_entry secvars db [] [] (* [c] contains an existential *) - let map_eauto (k,args) concl db = + let map_eauto ~secvars (k,args) concl db = let se = find k db in if matches_modes args se.sentry_mode then let st = if db.use_dn then Some db.hintdb_state else None in let pat = lookup_tacs concl st se in - merge_entry db [] pat - else merge_entry db [] [] + merge_entry secvars db [] pat + else merge_entry secvars db [] [] let is_exact = function | Give_exact _ -> true @@ -598,11 +624,11 @@ struct let get_entry se = let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in - List.map realize_tac h + List.map snd h let iter f db = let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in - f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat); + f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat); Constr_map.iter iter_se db.hintdb_map let fold f db accu = @@ -697,7 +723,20 @@ let try_head_pattern c = let with_uid c = { obj = c; uid = fresh_key () } +let secvars_of_idset s = + Id.Set.fold (fun id p -> + if is_section_variable id then + Id.Pred.add id p + else p) s Id.Pred.empty + +let secvars_of_constr env c = + secvars_of_idset (global_vars_set env c) + +let secvars_of_global env gr = + secvars_of_idset (vars_of_global_reference env gr) + let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = + let secvars = secvars_of_constr env c in let cty = strip_outer_cast cty in match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" @@ -713,6 +752,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = pat = Some pat; name = name; db = None; + secvars; code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = @@ -727,6 +767,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in let nmiss = List.length (clenv_missing ce) in + let secvars = secvars_of_constr env c in if Int.equal nmiss 0 then (Some hd, { pri = (match pri with None -> nb_hyp cty | Some p -> p); @@ -734,6 +775,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, pat = Some pat; name = name; db = None; + secvars; code = with_uid (Res_pf(c,cty,ctx)); }) else begin if not eapply then failwith "make_apply_entry"; @@ -746,6 +788,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, pat = Some pat; name = name; db = None; + secvars; code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -802,7 +845,8 @@ let make_resolves env sigma flags pri poly ?name cr = let try_apply f = try Some (f (c, cty, ctx)) with Failure _ -> None in let ents = List.map_filter try_apply - [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name] + [make_exact_entry env sigma pri poly ?name; + make_apply_entry env sigma flags pri poly ?name] in if List.is_empty ents then errorlabstrm "Hint" @@ -814,15 +858,17 @@ let make_resolves env sigma flags pri poly ?name cr = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma decl = let hname = get_id decl in + let c = mkVar hname in try [make_apply_entry env sigma (true, true, false) None false ~name:(PathHints [VarRef hname]) - (mkVar hname, get_type decl, Univ.ContextSet.empty)] + (c, get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") (* REM : in most cases hintname = id *) + let make_unfold eref = let g = global_of_evaluable_reference eref in (Some g, @@ -831,6 +877,7 @@ let make_unfold eref = pat = None; name = PathHints [g]; db = None; + secvars = secvars_of_global (Global.env ()) g; code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = @@ -842,6 +889,7 @@ let make_extern pri pat tacast = pat = pat; name = PathAny; db = None; + secvars = Id.Pred.empty; (* Approximation *) code = with_uid (Extern tacast) }) let make_mode ref m = @@ -866,6 +914,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); name = name; db = None; + secvars = secvars_of_constr env c; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -1326,7 +1375,7 @@ let pr_hints_db (name,db,hintlist) = let pr_hint_list_for_head c = let dbs = current_db () in let validate (name, db) = - let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in + let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in (name, db, hints) in let valid_dbs = List.map validate dbs in @@ -1348,9 +1397,9 @@ let pr_hint_term cl = let fn = try let hdc = decompose_app_bound cl in if occur_existential cl then - Hint_db.map_existential hdc cl - else Hint_db.map_auto hdc cl - with Bound -> Hint_db.map_none + Hint_db.map_existential ~secvars:Id.Pred.full hdc cl + else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl + with Bound -> Hint_db.map_none ~secvars:Id.Pred.full in let fn db = List.map (fun x -> 0, x) (fn db) in List.map (fun (name, db) -> (name, db, fn db)) dbs diff --git a/tactics/hints.mli b/tactics/hints.mli index 411540aa1b..8145ae1936 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -25,6 +25,8 @@ exception Bound val decompose_app_bound : constr -> global_reference * constr array +val secvars_of_hyps : Context.Named.t -> Id.Pred.t + (** Pre-created hint databases *) type 'a hint_ast = @@ -51,7 +53,8 @@ type 'a with_metadata = private { pat : constr_pattern option; (** A pattern for the concl of the Goal *) name : hints_path_atom; (** A potential name to refer to the hint *) db : hint_db_name option; - code : 'a; (** the tactic to apply when the concl matches pat *) + secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *) + code : 'a; (** the tactic to apply when the concl matches pat *) } type full_hint = hint with_metadata @@ -82,22 +85,28 @@ module Hint_db : type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t val find : global_reference -> t -> search_entry - val map_none : t -> full_hint list + + (** All hints which have no pattern. + * [secvars] represent the set of section variables that + * can be used in the hint. *) + val map_none : secvars:Id.Pred.t -> t -> full_hint list (** All hints associated to the reference *) - val map_all : global_reference -> t -> full_hint list + val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) - val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list + val map_existential : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list + val map_eauto : secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) - val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list + val map_auto : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t @@ -160,19 +169,20 @@ val prepare_hint : bool (* Check no remaining evars *) -> (bool * bool) (* polymorphic or monomorphic, local or global *) -> env -> evar_map -> open_constr -> hint_term -(** [make_exact_entry pri (c, ctyp)]. +(** [make_exact_entry pri (c, ctyp, ctx, secvars)]. [c] is the term given as an exact proof to solve the goal; - [ctyp] is the type of [c]. *) - + [ctyp] is the type of [c]. + [ctx] is its (refreshable) universe context. *) val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom -> (constr * types * Univ.universe_context_set) -> hint_entry -(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)]. +(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)]. [eapply] is true if this hint will be used only with EApply; [hnf] should be true if we should expand the head of cty before searching for products; [c] is the term given as an exact proof to solve the goal; - [cty] is the type of [c]. *) + [cty] is the type of [c]. + [ctx] is its (refreshable) universe context. *) val make_apply_entry : env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 893f33f1a8..d2e5d8525d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4975,7 +4975,7 @@ module New = struct let reduce_after_refine = reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=Some []; concl_occs=AllOccurrences } + {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = Refine.refine ?unsafe c <*> diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b8c07512f3..ba85286dd3 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/Makefile b/test-suite/Makefile index 10eb2df390..c10cd4ed44 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -88,6 +88,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +PREREQUISITELOG = prerequisite/admit.v.log \ + prerequisite/make_local.v.log prerequisite/make_notation.v.log + ####################################################################### # Phony targets ####################################################################### @@ -102,7 +105,7 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace lia.cache + rm -f trace .lia.cache $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>" $(HIDE)find . \( \ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \ @@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -257,7 +260,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -330,7 +333,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out rm $$tmpexpected; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -348,7 +351,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -379,7 +382,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v new file mode 100644 index 0000000000..831e8fb507 --- /dev/null +++ b/test-suite/bugs/closed/5127.v @@ -0,0 +1,15 @@ +Fixpoint arrow (n: nat) := + match n with + | S n => bool -> arrow n + | O => bool + end. + +Fixpoint apply (n : nat) : arrow n -> bool := + match n return arrow n -> bool with + | S n => fun f => apply _ (f true) + | O => fun x => x + end. + +Axiom f : arrow 10000. +Definition v : bool := Eval compute in apply _ f. +Definition w : bool := Eval vm_compute in v. diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v new file mode 100644 index 0000000000..d28303b8ab --- /dev/null +++ b/test-suite/bugs/closed/5161.v @@ -0,0 +1,27 @@ +(* Check that the presence of binders with type annotation do not + prevent the recursive binder part to be found *) + +From Coq Require Import Utf8. + +Delimit Scope C_scope with C. +Global Open Scope C_scope. + +Delimit Scope uPred_scope with I. + +Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x. + +Notation "∀ x .. y , P" := + (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. +Infix "∧" := and : uPred_scope. + +(* The next command fails with + In recursive notation with binders, Φ is expected to come without type. + I would expect this notation to work fine, since the ∀ does support + type annotation. +*) +Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := + (∀ Φ : _ → _, + (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I + (at level 20, x closed binder, y closed binder, + format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 2c7b04c62a..a2ee2d4c8e 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra argument _. +Error: Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad9765..9d90de47cb 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,12 @@ -File "stdin", line 1, characters 0-36: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: -Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] -File "stdin", line 2, characters 0-25: -Warning: This command is just asserting the number and names of arguments of -identity. If this is what you want add ': assert' to silence the warning. If -you want to clear implicit arguments add ': clear implicits'. If you want to -clear notation scopes add ': clear scopes' [arguments-assert,vernacular] -File "stdin", line 4, characters 0-40: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Warning: This command is just asserting the names of arguments of identity. +If this is what you want add ': assert' to silence the warning. If you want +to clear implicit arguments add ': clear implicits'. If you want to clear +notation scopes add ': clear scopes' [arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -112,18 +104,16 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: All arguments lists must declare the same names. +Error: Arguments lists should agree on names they provide. The command has indeed failed with message: -Error: The following arguments are not declared: x. +Error: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Error: Arguments names must be distinct. The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra argument y. -File "stdin", line 53, characters 0-26: -Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Error: Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index e42c983361..2d14c94ac8 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,5 +1,5 @@ Fail Arguments eq_refl {B y}, [B] y. -Arguments identity T _ _. +Arguments identity A _ _. Arguments eq_refl A x : assert. Arguments eq_refl {B y}, [B] y : rename. @@ -46,9 +46,9 @@ About myplus. Check @myplus. Fail Arguments eq_refl {F g}, [H] k. -Fail Arguments eq_refl {F}, [F]. +Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F. -Fail Arguments eq {F} x [z]. +Fail Arguments eq {F} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index a62f4312ed..1ff09e3af6 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,6 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Error: +Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z @@ -27,3 +28,7 @@ In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. Error: No primitive equality found. Hx +nat +nat +0 +0 diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index fb1dab7994..76c37625aa 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -48,3 +48,12 @@ Fail h H. Ltac m H := idtac H; exact H. Goal True. let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. + +(* Check consistency of interpretation scopes (#4398) *) + +Goal nat*(0*0=0) -> nat*(0*0=0). intro. +match goal with H: ?x*?y |- _ => idtac x end. +match goal with |- ?x*?y => idtac x end. +match goal with H: context [?x*?y] |- _ => idtac x end. +match goal with |- context [?x*?y] => idtac x end. +Abort. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 30abd961b1..07bbb60c40 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -115,3 +115,16 @@ Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). Require Import Coq.Vectors.VectorDef. Import VectorNotations. Goal True. idtac; []. (* important for test: no space here *) constructor. Qed. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. +Check |- {{ 0 }} 0. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index 976bec7371..e25510cf09 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True. reflexivity. Qed. +Class A. + +Section Foo. + + Variable a : A. + + Goal A. + solve [typeclasses eauto]. + Undo 1. + clear a. + try typeclasses eauto. + assert(a:=Build_A). + solve [ typeclasses eauto ]. + Undo 2. + assert(b:=Build_A). + solve [ typeclasses eauto ]. + Qed. +End Foo.
\ No newline at end of file diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 4007536442..1bc6fee0c4 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -12,6 +12,10 @@ are likely needed to make them behave like Coq 8.5. *) Require Export Coq.Compat.Coq86. +(** We use some deprecated options in this file, so we disable the + corresponding warning, to silence the build of this file. *) +Local Set Warnings "-deprecated-option". + (* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not behave as "intros [H|H]" but leave instead hypotheses quantified in the goal, here producing subgoals A->C and B->C. *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index f0f8f18641..e9771cfa40 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -13,7 +13,7 @@ open Flags open Vernac open Pcoq -let top_stderr x = msg_with !Pp_control.err_ft x +let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 56b4779555..f98505c362 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -756,7 +756,7 @@ let pr_constraints printenv env sigma evars cstrs = let evs = prlist (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr_env env' sigma evi.evar_concl) l + str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l in h 0 (pe ++ evs ++ pr_evar_constraints cstrs) else diff --git a/toplevel/record.ml b/toplevel/record.ml index 9c4d41ea50..ba9e7ee22f 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -517,10 +517,6 @@ let add_inductive_class ind = let k = let ctx = oneind.mind_arity_ctxt in let inst = Univ.UContext.instance mind.mind_universes in - let map = function - | LocalDef _ -> None - | LocalAssum (_, t) -> Some (lazy t) - in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index de41f7b190..2bde1dc46b 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -62,7 +62,7 @@ let print_usage_channel co command = \n -list-tags print highlight color tags known by Coq and exit\ \n\ \n -quiet unset display of extra information (implies -w none)\ -\n -w (all|none) configure display of warnings\ +\n -w (all|none|w1,..,wn) configure display of warnings\ \n -color (yes|no|auto) configure color output\ \n\ \n -q skip loading of rcfile\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b453dbc469..de45090bfc 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -143,7 +143,7 @@ let pr_new_syntax_in_context loc chan_beautify ocom = | None -> mt() in let after = comment (CLexer.extract_comments (snd loc)) in if !beautify_file then - Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) + Pp.msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (hov 0 (before ++ com ++ after)) else Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; @@ -181,7 +181,7 @@ let pp_cmd_header loc com = and take control of the console. *) let print_cmd_header loc com = - Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com); + Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Pp_control.std_ft () let rec interp_vernac po chan_beautify checknav (loc,com) = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69bac437e..c03f183ff5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -973,182 +973,255 @@ let vernac_declare_implicits locality r l = let warn_arguments_assert = CWarnings.create ~name:"arguments-assert" ~category:"vernacular" (fun sr -> - strbrk "This command is just asserting the number and names of arguments of " ++ + strbrk "This command is just asserting the names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add " ++ strbrk "': assert' to silence the warning. If you want " ++ strbrk "to clear implicit arguments add ': clear implicits'. " ++ strbrk "If you want to clear notation scopes add ': clear scopes'") - -let warn_renaming_nonimplicit = - CWarnings.create ~name:"arguments-ignore-rename-nonimpl" - ~category:"vernacular" - (fun (oldn, newn) -> - strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++ - strbrk ". Only implicit arguments can be renamed.") - -let vernac_declare_arguments locality r l nargs flags = - let extra_scope_flag = List.mem `ExtraScopes flags in - let names = List.map (List.map (fun { name } -> name)) l in - let names, rest = List.hd names, List.tl names in - let scopes = List.map (List.map (fun { notation_scope = s } -> s)) l in - if List.exists (fun na -> not (List.equal Name.equal na names)) rest then - error "All arguments lists must declare the same names."; - if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) - then error "Arguments names must be distinct."; - let sr = smart_global r in + +(* [nargs_for_red] is the number of arguments required to trigger reduction, + [args] is the main list of arguments statuses, + [more_implicits] is a list of extra lists of implicit statuses *) +let vernac_arguments locality reference args more_implicits nargs_for_red flags = + let assert_flag = List.mem `Assert flags in + let rename_flag = List.mem `Rename flags in + let clear_scopes_flag = List.mem `ClearScopes flags in + let extra_scopes_flag = List.mem `ExtraScopes flags in + let clear_implicits_flag = List.mem `ClearImplicits flags in + let default_implicits_flag = List.mem `DefaultImplicits flags in + let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + + let err_incompat x y = + error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in + + if assert_flag && rename_flag then + err_incompat "assert" "rename"; + if Option.has_some nargs_for_red && never_unfold_flag then + err_incompat "simpl never" "/"; + if never_unfold_flag && List.mem `ReductionDontExposeCase flags then + err_incompat "simpl never" "simpl nomatch"; + if clear_scopes_flag && extra_scopes_flag then + err_incompat "clear scopes" "extra scopes"; + if clear_implicits_flag && default_implicits_flag then + err_incompat "clear implicits" "default implicits"; + + let sr = smart_global reference in let inf_names = let ty = Global.type_of_global_unsafe sr in - Impargs.compute_implicits_names (Global.env ()) ty in - let rec check li ld ls = match li, ld, ls with - | [], [], [] -> () - | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls - | [], _::_, (Some _)::ls when extra_scope_flag -> - error "Extra notation scopes can be set on anonymous arguments only" - | [], x::_, _ -> errorlabstrm "vernac_declare_arguments" - (str "Extra argument " ++ pr_name x ++ str ".") - | l, [], _ -> errorlabstrm "vernac_declare_arguments" - (str "The following arguments are not declared: " ++ - prlist_with_sep pr_comma pr_name l ++ str ".") - | _::li, _::ld, _::ls -> check li ld ls - | _ -> assert false in - let () = match l with - | [[]] when List.exists ((<>) `Assert) flags || - (* Arguments f /. used to be allowed by mistake *) - (Flags.version_less_or_equal Flags.V8_5 && nargs >= 0) -> () - | _ -> - List.iter2 (check inf_names) (names :: rest) scopes + Impargs.compute_implicits_names (Global.env ()) ty in - (* we take extra scopes apart, and we check they are consistent *) - let l, scopes = - let scopes, rest = List.hd scopes, List.tl scopes in - if List.exists (List.exists ((!=) None)) rest then - error "Notation scopes can be given only once"; - if not extra_scope_flag then l, scopes else - let l, _ = List.split (List.map (List.chop (List.length inf_names)) l) in - l, scopes in - (* we interpret _ as the inferred names *) - let l = match l with - | [[]] -> l - | _ -> - let name_anons = function - | { name = Anonymous } as x, Name id -> { x with name = Name id } - | x, _ -> x in - List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in - let names_decl = List.map (List.map (fun { name } -> name)) l in - let renamed_arg = ref None in - let set_renamed a b = - if Option.is_empty !renamed_arg && not (Id.equal a b) then - renamed_arg := Some(b,a) + let prev_names = + try Arguments_renaming.arguments_names sr with Not_found -> inf_names in - let some_renaming_specified = - try - let names = Arguments_renaming.arguments_names sr in - not (List.equal (List.equal Name.equal) names names_decl) - with Not_found -> false in - let some_renaming_specified, implicits = - match l with - | [[]] -> false, [[]] + let num_args = List.length inf_names in + assert (Int.equal num_args (List.length prev_names)); + + let names_of args = List.map (fun a -> a.name) args in + + (* Checks *) + + let err_extra_args names = + errorlabstrm "vernac_declare_arguments" + (strbrk "Extra arguments: " ++ + prlist_with_sep pr_comma pr_name names ++ str ".") + in + let err_missing_args names = + errorlabstrm "vernac_declare_arguments" + (strbrk "The following arguments are not declared: " ++ + prlist_with_sep pr_comma pr_name names ++ str ".") + in + + let rec check_extra_args extra_args = + match extra_args with + | [] -> () + | { notation_scope = None } :: _ -> err_extra_args (names_of extra_args) + | { name = Anonymous; notation_scope = Some _ } :: args -> + check_extra_args args | _ -> - let some_renaming = ref some_renaming_specified in - let rec aux il = - match il with - | [] -> [] - | il :: ils -> aux_single il inf_names :: aux ils - and aux_single impl inf_names = - match impl, inf_names with - | [], _ -> [] - | { name = Anonymous; - implicit_status = (`Implicit|`MaximallyImplicit)} :: _, - Name id :: _ -> - assert false - | { name = Name x; - implicit_status = (`Implicit|`MaximallyImplicit)} :: _, - Anonymous :: _ -> - errorlabstrm "vernac_declare_arguments" - (str"Argument "++ pr_id x ++str " cannot be declared implicit.") - | { name = Name iid; - implicit_status = (`Implicit|`MaximallyImplicit as i)} :: impl, - Name id :: inf_names -> - let max = i = `MaximallyImplicit in - set_renamed iid id; - some_renaming := !some_renaming || not (Id.equal iid id); - (ExplByName id,max,false) :: aux_single impl inf_names - | { name = Name iid } :: impl, - Name id :: inf_names when not (Id.equal iid id) -> - warn_renaming_nonimplicit (id, iid); - aux_single impl inf_names - | { name = Name iid } :: impl, Name id :: inf_names - when not (Id.equal iid id) -> - aux_single impl inf_names - | { name = Name iid } :: impl, Name id :: inf_names -> - set_renamed iid id; - some_renaming := !some_renaming || not (Id.equal iid id); - aux_single impl inf_names - | _ :: impl, _ :: inf_names -> - (* no rename, no implicit status *) aux_single impl inf_names - | _ :: _, [] -> assert false (* checked before in check() *) - in - !some_renaming, aux l in - (* We check if renamed arguments do match previously declared imp args, - * since the system has this invariant *) - let some_implicits_specified = - match implicits with [[]] -> false | _ -> true in - if some_renaming_specified then - if not (List.mem `Rename flags) then - errorlabstrm "vernac_declare_arguments" - (str "To rename arguments the \"rename\" flag must be specified." ++ - match !renamed_arg with - | None -> mt () - | Some (o,n) -> - str "\nArgument " ++ pr_id o ++ - str " renamed to " ++ pr_id n ++ str ".") - else - Arguments_renaming.rename_arguments - (make_section_locality locality) sr names_decl; - (* All other infos are in the first item of l *) - let l = List.hd l in - let scopes = List.map (function - | None -> None - | Some (o, k) -> - try ignore (Notation.find_scope k); Some k - with UserError _ -> - Some (Notation.find_delimiters_scope o k)) scopes + error "Extra notation scopes can be set on anonymous and explicit arguments only." + in + + let args, scopes = + let scopes = List.map (fun { notation_scope = s } -> s) args in + if List.length args > num_args then + let args, extra_args = List.chop num_args args in + if extra_scopes_flag then + (check_extra_args extra_args; (args, scopes)) + else err_extra_args (names_of extra_args) + else args, scopes + in + + if Option.cata (fun n -> n > num_args) false nargs_for_red then + error "The \"/\" modifier should be put before any extra scope."; + + let scopes_specified = List.exists Option.has_some scopes in + + if scopes_specified && clear_scopes_flag then + error "The \"clear scopes\" flag is incompatible with scope annotations."; + + let names = List.map (fun { name } -> name) args in + let names = names :: List.map (List.map fst) more_implicits in + + let rename_flag_required = ref false in + let example_renaming = ref None in + let save_example_renaming renaming = + rename_flag_required := !rename_flag_required + || not (Name.equal (fst renaming) Anonymous); + if Option.is_empty !example_renaming then + example_renaming := Some renaming + in + + let rec names_union names1 names2 = + match names1, names2 with + | [], [] -> [] + | _ :: _, [] -> names1 + | [], _ :: _ -> names2 + | (Name _ as name) :: names1, Anonymous :: names2 + | Anonymous :: names1, (Name _ as name) :: names2 -> + name :: names_union names1 names2 + | name1 :: names1, name2 :: names2 -> + if Name.equal name1 name2 then + name1 :: names_union names1 names2 + else error "Arguments lists should agree on names they provide." + in + + let initial = List.make num_args Anonymous in + let names = List.fold_left names_union initial names in + + let rec rename prev_names names = + match prev_names, names with + | [], [] -> [] + | [], _ :: _ -> err_extra_args names + | _ :: _, [] when assert_flag -> + (* Error messages are expressed in terms of original names, not + renamed ones. *) + err_missing_args (List.lastn (List.length prev_names) inf_names) + | _ :: _, [] -> prev_names + | prev :: prev_names, Anonymous :: names -> + prev :: rename prev_names names + | prev :: prev_names, (Name id as name) :: names -> + if not (Name.equal prev name) then save_example_renaming (prev,name); + name :: rename prev_names names + in + + let names = rename prev_names names in + let renaming_specified = Option.has_some !example_renaming in + + if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) then + error "Arguments names must be distinct."; + + if !rename_flag_required && not rename_flag then + errorlabstrm "vernac_declare_arguments" + (strbrk "To rename arguments the \"rename\" flag must be specified." + ++ + match !example_renaming with + | None -> mt () + | Some (o,n) -> + str "\nArgument " ++ pr_name o ++ + str " renamed to " ++ pr_name n ++ str "."); + + + (* Parts of this code are overly complicated because the implicit arguments + API is completely crazy: positions (ExplByPos) are elaborated to + names. This is broken by design, since not all arguments have names. So + eventhough we eventually want to map only positions to implicit statuses, + we have to check whether the corresponding arguments have names, not to + trigger an error in the impargs code. Even better, the names we have to + check are not the current ones (after previous renamings), but the original + ones (inferred from the type). *) + + let implicits = + List.map (fun { name; implicit_status = i } -> (name,i)) args + in + let implicits = implicits :: more_implicits in + + let open Vernacexpr in + let rec build_implicits inf_names implicits = + match inf_names, implicits with + | _, [] -> [] + | _ :: inf_names, (_, NotImplicit) :: implicits -> + build_implicits inf_names implicits + + (* With the current impargs API, it is impossible to make an originally + anonymous argument implicit *) + | Anonymous :: _, (name, _) :: _ -> + errorlabstrm "vernac_declare_arguments" + (strbrk"Argument "++ pr_name name ++ + strbrk " cannot be declared implicit.") + + | Name id :: inf_names, (name, impl) :: implicits -> + let max = impl = MaximallyImplicit in + (ExplByName id,max,false) :: build_implicits inf_names implicits + + | _ -> assert false (* already checked in [names_union] *) in - let some_scopes_specified = List.exists ((!=) None) scopes in + + let implicits = List.map (build_implicits inf_names) implicits in + let implicits_specified = match implicits with [[]] -> false | _ -> true in + + if implicits_specified && clear_implicits_flag then + error "The \"clear implicits\" flag is incompatible with implicit annotations"; + + if implicits_specified && default_implicits_flag then + error "The \"default implicits\" flag is incompatible with implicit annotations"; + let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 l) in - if some_scopes_specified || List.mem `ClearScopes flags then - vernac_arguments_scope locality r scopes; - if not some_implicits_specified && List.mem `DefaultImplicits flags then - vernac_declare_implicits locality r [] - else if some_implicits_specified || List.mem `ClearImplicits flags then - vernac_declare_implicits locality r implicits; - if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then - error "The \"/\" option must be placed after the last \"!\"."; - let no_flags = List.is_empty flags in + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) + in + let rec narrow = function | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl - | [] -> [] | _ :: tl -> narrow tl in - let flags = narrow flags in - let some_simpl_flags_specified = - not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) in - if some_simpl_flags_specified then begin + | [] -> [] | _ :: tl -> narrow tl + in + let red_flags = narrow flags in + let red_modifiers_specified = + not (List.is_empty rargs) || Option.has_some nargs_for_red + || not (List.is_empty red_flags) + in + + if not (List.is_empty rargs) && never_unfold_flag then + err_incompat "simpl never" "!"; + + + (* Actions *) + + if renaming_specified then begin + let local = make_section_locality locality in + Arguments_renaming.rename_arguments local sr names + end; + + if scopes_specified || clear_scopes_flag then begin + let scopes = List.map (Option.map (fun (o,k) -> + try ignore (Notation.find_scope k); k + with UserError _ -> + Notation.find_delimiters_scope o k)) scopes + in + vernac_arguments_scope locality reference scopes + end; + + if implicits_specified || clear_implicits_flag then + vernac_declare_implicits locality reference implicits; + + if default_implicits_flag then + vernac_declare_implicits locality reference []; + + if red_modifiers_specified then begin match sr with | ConstRef _ as c -> Reductionops.ReductionBehaviour.set - (make_section_locality locality) c (rargs, nargs, flags) + (make_section_locality locality) c + (rargs, Option.default ~-1 nargs_for_red, red_flags) | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic "++ strbrk "are relevant for constants only.") end; - if not (some_renaming_specified || - some_implicits_specified || - some_scopes_specified || - some_simpl_flags_specified) && - no_flags then - warn_arguments_assert sr + if not (renaming_specified || + implicits_specified || + scopes_specified || + red_modifiers_specified) && (List.is_empty flags) then + warn_arguments_assert sr let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; @@ -1418,7 +1491,7 @@ let _ = optwrite = (fun b -> Constrintern.parsing_explicit := b) } let _ = - declare_string_option + declare_string_option ~preprocess:CWarnings.normalize_flags_string { optsync = true; optdepr = false; optname = "warnings display"; @@ -1951,8 +2024,8 @@ let interp ?proof ~loc locality poly c = vernac_syntactic_definition locality id c local b | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits locality qid l - | VernacArguments (qid, l, narg, flags) -> - vernac_declare_arguments locality qid l narg flags + | VernacArguments (qid, args, more_implicits, nargs, flags) -> + vernac_arguments locality qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl | VernacGeneralizable gen -> vernac_generalizable locality gen | VernacSetOpacity qidl -> vernac_set_opacity locality qidl |