diff options
154 files changed, 1441 insertions, 767 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ce0c1d9af7..c644059af0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -15,7 +15,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-07-06-V22" + CACHEKEY: "bionic_coq-V2019-08-08-V01" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -9,7 +9,7 @@ WHAT DO YOU NEED ? - OCaml (version >= 4.05.0) (available at https://ocaml.org/) - (This version of Coq has been tested up to OCaml 4.08.0) + (This version of Coq has been tested up to OCaml 4.08.1) - The Num package, which used to be part of the OCaml standard library, if you are using an OCaml version >= 4.06.0 diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 862c54900f..84f080cc73 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -72,7 +72,7 @@ jobs: opam list displayName: 'Install OCaml dependencies' env: - COMPILER: "4.08.0" + COMPILER: "4.08.1" FINDLIB_VER: ".1.8.0" OPAMYES: "true" diff --git a/checker/values.ml b/checker/values.ml index ac9bc26344..cc9ac1f834 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -219,7 +219,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 34d748e1cc..03ce5a6b5d 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.08.0+mingw64c +OPAM_VARIANT=ocaml-variants.4.08.1+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 011c7fbdec..7175b5ffd5 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-07-06-V22" +# CACHEKEY: "bionic_coq-V2019-08-08-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.08.0" \ +ENV COMPILER_EDGE="4.08.1" \ COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \ BASE_OPAM_EDGE="dune-release.1.3.1" diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 01c2b574a2..d00c8cb11a 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -119,6 +119,16 @@ Universes GH issue number: #8341 risk: unlikely to be activated by chance (requires a plugin) + component: template polymorphism + summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though) + impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found + impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit) + fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau) + found by: Gilbert using explicit sharing of universes, exploit found for 8.5-8.9 by Pédrot, other variants generating sharing using sections, or using ltac tricks by Sozeau, exploit in 8.4 by Herbelin and Jason Gross by adding new tricks to Sozeau's variants + exploit: test-suite/failure/Template.v + GH issue number: #9294 + risk: moderate risk to be activated by chance + Primitive projections component: primitive projections, guard condition diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index c7f36ee964..7e53f13e45 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.08.0))) -(context (opam (switch 4.08.0+flambda))) +(context (opam (switch 4.08.1))) +(context (opam (switch 4.08.1+flambda))) diff --git a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst new file mode 100644 index 0000000000..87e89a70f1 --- /dev/null +++ b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst @@ -0,0 +1,30 @@ +- Fix soundness issue with template polymorphism (`#9294 + <https://github.com/coq/coq/issues/9294>`_) + + Declarations of template-polymorphic inductive types ignored the + provenance of the universes they were abstracting on and did not + detect if they should be greater or equal to :math:`\Set` in + general. Previous universes and universes introduced by the inductive + definition could have constraints that prevented their instantiation + with e.g. :math:`\Prop`, resulting in unsound instantiations later. The + implemented fix only allows abstraction over universes introduced by + the inductive declaration, and properly records all their constraints + by making them by default only :math:`>= \Prop`. It is also checked + that a template polymorphic inductive actually is polymorphic on at + least one universe. + + This prevents inductive declarations in sections to be universe + polymorphic over section parameters. For a backward compatible fix, + simply hoist the inductive definition out of the section. + An alternative is to declare the inductive as universe-polymorphic and + cumulative in a universe-polymorphic section: all universes and + constraints will be properly gathered in this case. + See :ref:`Template-polymorphism` for a detailed exposition of the + rules governing template-polymorphic types. + + To help users incrementally fix this issue, a command line option + `-no-template-check` and a global flag :flag:`Template Check` are + available to selectively disable the new check. Use at your own risk. + + (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau + and Maxime Dénès). diff --git a/doc/changelog/08-tools/10577-extraction-dependent-projections.rst b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst new file mode 100644 index 0000000000..4d52355542 --- /dev/null +++ b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst @@ -0,0 +1,9 @@ +- Fix a printing bug of OCaml extraction on dependent record projections, which + produced improper `assert false`. This change makes the OCaml extractor + internally inline record projections by default; thus the monolithic OCaml + extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not + produce record projection constants anymore except for record projections + explicitly instructed to extract, and records declared in opaque modules + (`#10577 <https://github.com/coq/coq/pull/10577>`_, + fixes `#7348 <https://github.com/coq/coq/issues/7348>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst new file mode 100644 index 0000000000..864c4e6a7e --- /dev/null +++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst @@ -0,0 +1,6 @@ +- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the + :g:`List` module. + + See `#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index ef183174d7..1611e9dd52 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -70,7 +70,7 @@ and function types over these sorts. Formally, we call :math:`\Sort` the set of sorts which is defined by: .. math:: - + \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and @@ -436,7 +436,7 @@ instance the identity function over a given type :math:`T` can be written this a *reduction* (or a *conversion*) rule we call :math:`β`: .. math:: - + E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u} We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of @@ -474,14 +474,14 @@ with its value, that is to expand (or unfold) it into its value. This reduction is called δ-reduction and shows as follows. .. inference:: Delta-Local - + \WFE{\Gamma} (x:=t:T) ∈ Γ -------------- E[Γ] ⊢ x~\triangleright_Δ~t .. inference:: Delta-Global - + \WFE{\Gamma} (c:=t:T) ∈ E -------------- @@ -499,7 +499,7 @@ destroyed, this reduction differs from δ-reduction. It is called ζ-reduction and shows as follows. .. inference:: Zeta - + \WFE{\Gamma} \WTEG{u}{U} \WTE{\Gamma::(x:=u:U)}{t}{T} @@ -533,17 +533,17 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. .. math:: f ~:~ ∀ x:\Type(2),~\Type(1) - + then .. math:: λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1) - + We could not allow .. math:: λ x:\Type(1).~(f~x) ~\triangleright_η~ f - + because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. @@ -665,7 +665,7 @@ a *subtyping* relation inductively defined by: .. math:: [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ] - + respectively then .. math:: @@ -695,7 +695,7 @@ a *subtyping* relation inductively defined by: The conversion rule up to subtyping is now exactly: .. inference:: Conv - + E[Γ] ⊢ U : s E[Γ] ⊢ t : T E[Γ] ⊢ T ≤_{βδιζη} U @@ -716,13 +716,13 @@ that :math:`t_0` is :math:`λ x:T.~u_0` then one step of β-head reduction of :m .. math:: λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~ λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n ) - + Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the *β-head normal form* of :math:`t`: .. math:: t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m ) - + where :math:`v` is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some :math:`u_i` can be reducible. Similar notions of head-normal forms involving δ, ι @@ -828,7 +828,7 @@ We have to give the type of constants in a global environment :math:`E` which contains an inductive definition. .. inference:: Ind - + \WFE{Γ} \ind{p}{Γ_I}{Γ_C} ∈ E (a:A)∈Γ_I @@ -836,7 +836,7 @@ contains an inductive definition. E[Γ] ⊢ a : A .. inference:: Constr - + \WFE{Γ} \ind{p}{Γ_I}{Γ_C} ∈ E (c:C)∈Γ_C @@ -917,7 +917,7 @@ condition* for a constant :math:`X` in the following cases: + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i` + :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the positivity condition for :math:`X`. - + Strict positivity +++++++++++++++++ @@ -931,10 +931,10 @@ cases: strictly positively in type :math:`V` + :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an inductive definition of the form - + .. math:: \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n} - + (in particular, it is not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in any of the :math:`t_i`, and the (instantiated) types of constructor @@ -998,7 +998,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]` (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} - + provided that the following side conditions hold: @@ -1052,30 +1052,10 @@ between universes for inductive types in the Type hierarchy. Template polymorphism +++++++++++++++++++++ -Inductive types can be made polymorphic over their arguments -in :math:`\Type`. - -.. flag:: Auto Template Polymorphism - - This option, enabled by default, makes every inductive type declared - at level :math:`\Type` (without annotations or hiding it behind a - definition) template polymorphic. - - This can be prevented using the ``notemplate`` attribute. - - An inductive type can be forced to be template polymorphic using the - ``template`` attribute. - - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. - -.. warn:: Automatically declaring @ident as template polymorphic. - - Warning ``auto-template`` can be used to find which types are - implicitly declared template polymorphic by :flag:`Auto Template - Polymorphism`. +Inductive types can be made polymorphic over the universes introduced by +their parameters in :math:`\Type`, if the minimal inferred sort of the +inductive declarations either mention some of those parameter universes +or is computed to be :math:`\Prop` or :math:`\Set`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. @@ -1117,10 +1097,11 @@ provided that the following side conditions hold: + there are sorts :math:`s_i`, for :math:`1 ≤ i ≤ k` such that, for :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ; - + the sorts :math:`s_i` are such that all eliminations, to - :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed - (see Section :ref:`Destructors`). - + + the sorts :math:`s_i` are all introduced by the inductive + declaration and have no universe constraints beside being greater + than or equal to :math:`\Prop`, and such that all + eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, + are allowed (see Section :ref:`Destructors`). Notice that if :math:`I_j~q_1 … q_r` is typable using the rules **Ind-Const** and @@ -1141,6 +1122,61 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or :math:`C_i~q_1 … q_r` is mapped to the names chosen in the specific instance of :math:`\ind{p}{Γ_I}{Γ_C}`. +.. warning:: + + The restriction that sorts are introduced by the inductive + declaration prevents inductive types declared in sections to be + template-polymorphic on universes introduced previously in the + section: they cannot parameterize over the universes introduced with + section variables that become parameters at section closing time, as + these may be shared with other definitions from the same section + which can impose constraints on them. + +.. flag:: Auto Template Polymorphism + + This option, enabled by default, makes every inductive type declared + at level :math:`\Type` (without annotations or hiding it behind a + definition) template polymorphic if possible. + + This can be prevented using the ``notemplate`` attribute. + +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + + An inductive type can be forced to be template polymorphic using the + ``template`` attribute: it should then fullfill the criterion to + be template polymorphic or an error is raised. + +.. exn:: Inductive @ident cannot be made template polymorphic. + + This error is raised when the `#[universes(template)]` attribute is + on but the inductive cannot be made polymorphic on any universe or be + inferred to live in :math:`\Prop` or :math:`\Set`. + + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. + +.. flag:: Template Check + + Unsetting option :flag:`Template Check` disables the check of + locality of the sorts when abstracting the inductive over its + parameters. This is a deprecated and *unsafe* flag that can introduce + inconsistencies, it is only meant to help users incrementally update + code from Coq versions < 8.10 which did not implement this check. + The `Coq89.v` compatibility file sets this flag globally. A global + ``-no-template-check`` command line option is also available. Use at + your own risk. Use of this flag is recorded in the typing flags + associated to a definition but is *not* supported by the |Coq| + checker (`coqchk`). It will appear in :g:`Print Assumptions` and + :g:`About @ident` output involving inductive declarations that were + (potentially unsoundly) assumed to be template polymorphic. + + In practice, the rule **Ind-Family** is used by |Coq| only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over @@ -1154,10 +1190,10 @@ inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicativ Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_), and otherwise in the Type hierarchy. -Note that the side-condition about allowed elimination sorts in the -rule **Ind-Family** is just to avoid to recompute the allowed elimination -sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As -an example, let us consider the following definition: +Note that the side-condition about allowed elimination sorts in the rule +**Ind-Family** avoids to recompute the allowed elimination sorts at each +instance of a pattern matching (see Section :ref:`Destructors`). As an +example, let us consider the following definition: .. example:: @@ -1320,7 +1356,7 @@ using the syntax: \Match~m~\as~x~\In~I~\_~a~\return~P~\with~ (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend - + The :math:`\as` part can be omitted if either the result type does not depend on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m` can occur in :math:`P` where it is considered a bound variable). The :math:`\In` part @@ -1360,7 +1396,7 @@ There is no restriction on the sort of the predicate to be eliminated. ----------------------- [I:∀ x:A,~A′|∀ x:A,~B′] - + .. inference:: Set & Type s_1 ∈ \{\Set,\Type(j)\} @@ -1376,7 +1412,7 @@ is also of sort :math:`\Prop` or is of the morally smaller sort :math:`\SProp`. .. inference:: Prop - + s ∈ \{\SProp,\Prop\} -------------------- [I:\Prop|I→s] @@ -1404,7 +1440,7 @@ the proof of :g:`or A B` is not accepted: Fail Definition choice (A B: Prop) (x:or A B) := match x with or_introl _ _ a => true | or_intror _ _ b => false end. - + From the computational point of view, the structure of the proof of :g:`(or A B)` in this term is needed for computing the boolean value. @@ -1441,7 +1477,7 @@ this type. :math:`\Prop` for which more eliminations are allowed. .. inference:: Prop-extended - + I~\kw{is an empty or singleton definition} s ∈ \Sort ------------------------------------- @@ -1589,7 +1625,7 @@ An ι-redex is a term of the following form: .. math:: \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) - + with :math:`c_{p_i}` the :math:`i`-th constructor of the inductive type :math:`I` with :math:`r` parameters. @@ -1636,7 +1672,7 @@ Typing rule The typing rule is the expected one for a fixpoint. .. inference:: Fix - + (E[Γ] ⊢ A_i : s_i )_{i=1… n} (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} ------------------------------------------------------- @@ -1749,7 +1785,7 @@ The reduction for fixpoints is: .. math:: (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} - + when :math:`a_{k_i}` starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction for primitive recursive operators. The following reductions are now @@ -1808,11 +1844,11 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} {\subst{Γ}{c′}{(c′~c)}}} - + .. math:: \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}} - + .. math:: \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ @@ -1853,7 +1889,7 @@ One can consequently derive the following property. .. _First-pruning-property: .. inference:: First pruning property: - + \WF{E;~c:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- @@ -1933,5 +1969,3 @@ impredicative system for sort :math:`\Set` become: s ∈ \{\Type(i)\} ---------------- [I:\Set|I→ s] - - diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c391cc949d..2885d6dc33 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -627,6 +627,7 @@ file is a particular case of module called *library file*. as ``Export``. .. cmdv:: From @dirpath Require @qualid + :name: From ... Require ... This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` diff --git a/engine/evd.ml b/engine/evd.ml index b621a3fe2f..6a721a1a8a 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -702,7 +702,7 @@ let empty = { } let from_env e = - { empty with universes = UState.make (Environ.universes e) } + { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } let from_ctx ctx = { empty with universes = ctx } diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index e3a5676942..3c383b2e00 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -107,7 +107,7 @@ struct Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Feedback.msg_info s) + let print_debug s = make (fun _ -> Feedback.msg_debug s) let print_info s = make (fun _ -> Feedback.msg_info s) let print_warning s = make (fun _ -> Feedback.msg_warning s) let print_notice s = make (fun _ -> Feedback.msg_notice s) diff --git a/engine/uState.ml b/engine/uState.ml index 5ed016e0d0..cb40e6eadd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -34,6 +34,7 @@ type t = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) uctx_weak_constraints : UPairSet.t } @@ -47,6 +48,7 @@ let empty = uctx_univ_variables = LMap.empty; uctx_univ_algebraic = LSet.empty; uctx_universes = initial_sprop_cumulative; + uctx_universes_lbound = Univ.Level.set; uctx_initial_universes = initial_sprop_cumulative; uctx_weak_constraints = UPairSet.empty; } @@ -54,10 +56,12 @@ let elaboration_sprop_cumul = Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true -let make u = +let make ~lbound u = let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; uctx_initial_universes = u} + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -83,7 +87,7 @@ let union ctx ctx' = let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = - LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g in let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); @@ -99,6 +103,7 @@ let union ctx ctx' = else let cstrsr = ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_universes_lbound = ctx.uctx_universes_lbound; uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -431,18 +436,19 @@ let check_univ_decl ~poly uctx decl = (ContextSet.constraints uctx.uctx_local); ctx -let restrict_universe_context (univs, csts) keep = +let restrict_universe_context ~lbound (univs, csts) keep = let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in let g = UGraph.initial_universes in - let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in + let g = LSet.fold (fun v g -> if Level.is_small v then g else + UGraph.add_universe v ~lbound ~strict:false g) allunivs g in let g = UGraph.merge_constraints csts g in let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in let csts = Constraint.filter (fun (l,d,r) -> - not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in + not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -450,7 +456,7 @@ let restrict ctx vars = let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) (fst ctx.uctx_names) vars in - let uctx' = restrict_universe_context ctx.uctx_local vars in + let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in { ctx with uctx_local = uctx' } let demote_seff_univs universes uctx = @@ -497,7 +503,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe u false g + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g with UGraph.AlreadyDeclared when sideff -> g) levels g in @@ -544,16 +550,17 @@ let new_univ_variable ?loc rigid name | None -> add_uctx_loc u loc uctx.uctx_names in let initial = - UGraph.add_universe u false uctx.uctx_initial_universes + UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe u false uctx.uctx_universes; + uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false + u uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -let make_with_initial_binders e us = - let uctx = make e in +let make_with_initial_binders ~lbound e us = + let uctx = make ~lbound e in List.fold_left (fun uctx { CAst.loc; v = id } -> fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) @@ -561,10 +568,10 @@ let make_with_initial_binders e us = let add_global_univ uctx u = let initial = - UGraph.add_universe u true uctx.uctx_initial_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes in let univs = - UGraph.add_universe u true uctx.uctx_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes in { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; @@ -679,8 +686,9 @@ let refresh_undefined_univ_variables uctx = uctx.uctx_univ_variables LMap.empty in let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g) - (ContextSet.levels ctx') g in + let lbound = uctx.uctx_universes_lbound in + let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) + (ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; @@ -688,14 +696,16 @@ let refresh_undefined_univ_variables uctx = uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; + uctx_universes_lbound = lbound; uctx_initial_universes = initial; uctx_weak_constraints = weak; } in uctx', subst let minimize uctx = let open UnivMinim in + let lbound = uctx.uctx_universes_lbound in let ((vars',algs'), us') = - normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables + normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in if ContextSet.equal us' uctx.uctx_local then uctx @@ -709,6 +719,7 @@ let minimize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; + uctx_universes_lbound = lbound; uctx_initial_universes = uctx.uctx_initial_universes; uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } diff --git a/engine/uState.mli b/engine/uState.mli index 9689f2e961..52e48c4eeb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -25,9 +25,9 @@ type t val empty : t -val make : UGraph.t -> t +val make : lbound:Univ.Level.t -> UGraph.t -> t -val make_with_initial_binders : UGraph.t -> lident list -> t +val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t val is_empty : t -> bool @@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t (** {5 Unification} *) -(** [restrict_universe_context (univs,csts) keep] restricts [univs] to +(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so that transitive constraints between remaining universes (those in [keep] and those not in [univs]) are preserved. *) -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t (** [restrict uctx ctx] restricts the local universes of [uctx] to [ctx] extended by local named universes and side effect universes diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 1b7c33b9c1..30fdd28997 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) (* TODO check is_small/sprop *) -let normalize_context_set g ctx us algs weak = +let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles @@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak = let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) ctx UGraph.initial_universes in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) - then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g else g in let g = Constraint.fold @@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak = (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 21f6efe86a..72b432e62f 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> diff --git a/engine/univops.mli b/engine/univops.mli index 6cc7868a38..1f1edbed16 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -15,5 +15,5 @@ open Univ val universes_of_constr : constr -> LSet.t [@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t [@@ocaml.deprecated "Use [UState.restrict_universe_context]"] diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3f216b0d63..b4798127f9 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -625,7 +625,8 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open UState in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env) + (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; diff --git a/interp/notation.ml b/interp/notation.ml index a78bc60e83..ea2173860d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1205,7 +1205,7 @@ let interp_notation ?loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in - Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation; + Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation; n.not_interp, (n.not_location, sc) with Not_found -> user_err ?loc diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 302bb6ece2..9dded8656c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -100,7 +100,7 @@ let warn_deprecated_syntactic_definition = let search_syntactic_definition ?loc kn = let syndef = KNmap.find kn !syntax_table in let def = out_pat syndef.syndef_pattern in - Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; + Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; def let search_filtered_syntactic_definition ?loc filter kn = @@ -108,5 +108,5 @@ let search_filtered_syntactic_definition ?loc filter kn = let def = out_pat syndef.syndef_pattern in let res = filter def in if Option.has_some res then - Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; + Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; res diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8d32684b09..44676c9da5 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,6 +87,11 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) + + check_template : bool; + (* If [false] then we don't check that the universes template-polymorphic + inductive parameterize on are necessarily local and unbounded from below. + This potentially introduces inconsistencies. *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 391b139496..7225671a1e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,6 +26,7 @@ let safe_flags oracle = { enable_VM = true; enable_native_compiler = true; indices_matter = true; + check_template = true; } (** {6 Arities } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 655094e88b..4a2aeea22d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -59,8 +59,9 @@ type globals = { type stratification = { env_universes : UGraph.t; - env_engagement : engagement; env_sprop_allowed : bool; + env_universes_lbound : Univ.Level.t; + env_engagement : engagement } type val_kind = @@ -119,9 +120,9 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet; env_sprop_allowed = false; - }; + env_universes_lbound = Univ.Level.set; + env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab; @@ -262,8 +263,15 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter +let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes +let universes_lbound env = env.env_stratification.env_universes_lbound + +let set_universes_lbound env lbound = + let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in + { env with env_stratification } + let named_context env = env.env_named_context.env_named_ctx let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context.env_rel_ctx @@ -382,29 +390,30 @@ let check_constraints c env = let push_constraints_to_env (_,univs) env = add_constraints univs env -let add_universes strict ctx g = +let add_universes ~lbound ~strict ctx g = let g = Array.fold_left - (fun g v -> UGraph.add_universe v strict g) + (fun g v -> UGraph.add_universe ~lbound ~strict v g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = - map_universes (add_universes strict ctx) env + map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env -let add_universes_set strict ctx g = +let add_universes_set ~lbound ~strict ctx g = let g = Univ.LSet.fold (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = - map_universes (add_universes_set strict ctx) env + map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env let push_subgraph (levels,csts) env = + let lbound = universes_lbound env in let add_subgraph g = - let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in let newg = UGraph.merge_constraints csts newg in (if not (Univ.Constraint.is_empty csts) then let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in @@ -428,6 +437,7 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; + check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -436,7 +446,8 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler + enable_native_compiler == alt.enable_native_compiler && + check_template == alt.check_template [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -568,11 +579,20 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes +let template_checked_ind (mind,_i) env = + (lookup_mind mind env).mind_typing_flags.check_template + let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true | RegularArity _ -> false +let template_polymorphic_variables (mind,i) env = + match (lookup_mind mind env).mind_packets.(i).mind_arity with + | TemplateArity { Declarations.template_param_levels = l; _ } -> + List.map_filter (fun level -> level) l + | RegularArity _ -> [] + let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env @@ -762,6 +782,22 @@ let is_template_polymorphic env r = | IndRef ind -> template_polymorphic_ind ind env | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env +let get_template_polymorphic_variables env r = + let open Names.GlobRef in + match r with + | VarRef _id -> [] + | ConstRef _c -> [] + | IndRef ind -> template_polymorphic_variables ind env + | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env + +let is_template_checked env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_checked_ind ind env + | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env + let is_type_in_type env r = let open Names.GlobRef in match r with diff --git a/kernel/environ.mli b/kernel/environ.mli index e6d814ac7d..f7de98dcfb 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -51,8 +51,9 @@ type globals type stratification = { env_universes : UGraph.t; - env_engagement : engagement; env_sprop_allowed : bool; + env_universes_lbound : Univ.Level.t; + env_engagement : engagement } type named_context_val = private { @@ -85,6 +86,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t +val universes_lbound : env -> Univ.Level.t +val set_universes_lbound : env -> Univ.Level.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val @@ -99,6 +102,7 @@ val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool +val check_template : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool @@ -254,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool (** Old-style polymorphism *) val template_polymorphic_ind : inductive -> env -> bool +val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool +val template_checked_ind : inductive -> env -> bool (** {5 Modules } *) @@ -346,6 +352,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool +val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list +val is_template_checked : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool (** Native compiler *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index c8e04b9fee..06d2e1bb21 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} if not ind_squashed then InType else Sorts.family (Sorts.sort_of_univ ind_univ) +(* For a level to be template polymorphic, it must be introduced + by the definition (so have no constraint except lbound <= l) + and not to be constrained from below, so any universe l' <= l + can be used as an instance of l. All bounds from above, i.e. + l <=/< r will be valid for any l' <= l. *) +let unbounded_from_below u cstrs = + Univ.Constraint.for_all (fun (l, d, r) -> + match d with + | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u) + | Lt | Le -> not (Univ.Level.equal r u)) + cstrs + (* Returns the list [x_1, ..., x_n] of levels contributing to template - polymorphism. The elements x_k is None if the k-th parameter (starting - from the most recent and ignoring let-definitions) is not contributing - or is Some u_k if its level is u_k and is contributing. *) -let param_ccls paramsctxt = + polymorphism. The elements x_k is None if the k-th parameter + (starting from the most recent and ignoring let-definitions) is not + contributing to the inductive type's sort or is Some u_k if its level + is u_k and is contributing. *) +let template_polymorphic_univs ~template_check uctx paramsctxt concl = + let check_level l = + if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + unbounded_from_below l (Univ.ContextSet.constraints uctx) then + Some l + else None + in + let univs = Univ.Universe.levels concl in + let univs = + if template_check then + Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs + else univs (* Doesn't check the universes can be generalized *) + in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with - | Sort (Type u) -> Univ.Universe.level u + | Sort (Type u) -> + if template_check then + (match Univ.Universe.level u with + | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None + | None -> None) + else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in - List.fold_left fold [] paramsctxt + let params = List.fold_left fold [] paramsctxt in + params, univs -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = let arity = Vars.subst_univs_level_constr usubst arity in let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in let indices = Vars.subst_univs_level_context usubst indices in @@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in let arity = match univ_info.ind_min_univ with - | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ} + | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} | Some min_univ -> - ((match univs with - | Monomorphic _ -> () + let ctx = match univs with + | Monomorphic ctx -> ctx | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")); - TemplateArity {template_param_levels=param_ccls params; template_level=min_univ}) + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in + if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + && Univ.LSet.is_empty concl_levels then + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + else + TemplateArity {template_param_levels = param_levels; template_level = min_univ} in let kelim = allowed_sorts univ_info in @@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); + let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + (* universes *) let env_univs = match mie.mind_entry_universes with - | Monomorphic_entry ctx -> push_context_set ctx env + | Monomorphic_entry ctx -> + let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in + push_context_set ctx env | Polymorphic_entry (_, ctx) -> push_context ctx env in @@ -335,7 +376,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let data = List.map (abstract_packets univs usubst params) data in + let template_check = Environ.check_template env in + let data = List.map (abstract_packets ~template_check univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index aaa0d6a149..8da4e2885c 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry -> (Constr.rel_context * (Constr.rel_context * Constr.types) array) * Sorts.family) array + +(* Utility function to compute the actual universe parameters + of a template polymorphic inductive *) +val template_polymorphic_univs : + template_check:bool -> + Univ.ContextSet.t -> + Constr.rel_context -> + Univ.Universe.t -> + Univ.Level.t option list * Univ.LSet.t diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 9305a91731..ccc218771a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = c', Monomorphic Univ.ContextSet.empty, cst | Polymorphic uctx, Some ctx -> let () = - if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then + if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env) + (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab in (** Terms are compared in a context with De Bruijn universe indices *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 53f228c618..327cb2efeb 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type _u, Prop -> raise NotConvertible + | Type u, Prop -> infer_pb u Univ.type0m_univ | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d47dc0c6e1..d22ec3b7ca 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -97,7 +97,8 @@ let check_universes error env u1 u2 = match u1, u2 with | Monomorphic _, Monomorphic _ -> env | Polymorphic auctx1, Polymorphic auctx2 -> - if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + let lbound = Environ.universes_lbound env in + if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) else Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 6fde6e9c5f..33336079bb 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -149,10 +149,10 @@ let enforce_leq_alg u v g = cg exception AlreadyDeclared = G.AlreadyDeclared -let add_universe u strict g = +let add_universe u ~lbound ~strict g = let graph = G.add u g.graph in let d = if strict then Lt else Le in - enforce_constraint (Level.set,d,u) {g with graph} + enforce_constraint (lbound,d,u) {g with graph} let add_universe_unconstrained u g = {g with graph=G.add u g.graph} @@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k (** Subtyping of polymorphic contexts *) -let check_subtype univs ctxT ctx = +let check_subtype ~lbound univs ctxT ctx = if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in - let push accu v = add_universe v false accu in + let push accu v = add_universe v ~lbound ~strict:false accu in let univs = Array.fold_left push univs (Instance.to_array inst) in let univs = merge_constraints cstT univs in check_constraints cst univs diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e1b5868d55..d90f01d8d1 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> bool -> t -> t +val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : AUContext.t check_function +val check_subtype : lbound:Level.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/lib/feedback.mli b/lib/feedback.mli index dc8449ed71..5375d97d57 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -74,13 +74,8 @@ val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_conte (** [set_id_for_feedback route id] Set the defaults for feedback *) val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit -(** {6 output functions} +(** {6 output functions} *) -[msg_notice] do not put any decoration on output by default. If -possible don't mix it with goal output (prefer msg_info or -msg_warning) so that interfaces can dispatch outputs easily. Once all -interfaces use the xml-like protocol this constraint can be -relaxed. *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) diff --git a/lib/system.ml b/lib/system.ml index b1a9efccfc..8c333ec267 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -300,13 +300,13 @@ let with_time ~batch ~header f x = let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) diff --git a/library/coqlib.ml b/library/coqlib.ml index b1e4ef2b00..11d053624c 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -104,8 +104,10 @@ let gen_reference_in_modules locstr dirs s = let check_required_library d = let dir = make_dir d in - if Library.library_is_loaded dir then () - else + try + let _ : Declarations.module_body = Global.lookup_module (ModPath.MPfile dir) in + () + with Not_found -> let in_current_dir = match Lib.current_mp () with | MPfile dp -> DirPath.equal dir dp | _ -> false diff --git a/library/global.ml b/library/global.ml index 0fc9e11364..6bb4614aa4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -119,6 +119,7 @@ let add_module_parameter mbid mte inl = (** Queries on the global environment *) let universes () = universes (env()) +let universes_lbound () = universes_lbound (env()) let named_context () = named_context (env()) let named_context_val () = named_context_val (env()) @@ -181,6 +182,10 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r +let is_template_checked r = is_template_checked (env ()) r + +let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r + let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = diff --git a/library/global.mli b/library/global.mli index b089b7dd80..d0bd556d70 100644 --- a/library/global.mli +++ b/library/global.mli @@ -22,6 +22,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool val universes : unit -> UGraph.t +val universes_lbound : unit -> Univ.Level.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Constr.named_context @@ -136,6 +137,8 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool +val is_template_checked : GlobRef.t -> bool +val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool (** {6 Retroknowledge } *) diff --git a/library/goptions.ml b/library/goptions.ml index c7024ca81d..0973944fb5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -398,9 +398,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/library/library.mllib b/library/library.mllib index 3b75438ccd..c34d8911e8 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -6,7 +6,6 @@ Nametab Global Lib Declaremods -Library States Kindops Goptions diff --git a/library/states.ml b/library/states.ml index a73f16957d..0be153d96a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -9,7 +9,6 @@ (************************************************************************) open Util -open System type state = Lib.frozen * Summary.frozen @@ -25,13 +24,6 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let extern_state s = - System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true) - -let intern_state s = - unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); - Library.overwrite_library_filenames s - (* Rollback. *) let with_state_protection f x = diff --git a/library/states.mli b/library/states.mli index c4f3eae49d..4870f48fc3 100644 --- a/library/states.mli +++ b/library/states.mli @@ -15,9 +15,6 @@ freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) -val intern_state : string -> unit -val extern_state : string -> unit - type state val freeze : marshallable:bool -> state val unfreeze : state -> unit diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index de23f05a9e..7f0d768d3f 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -436,7 +436,7 @@ let comment_stop ep = let bp = match !comment_begin with Some bp -> bp | None -> - Feedback.msg_notice + Feedback.msg_debug (str "No begin location for comment '" ++ str current_s ++str"' ending at " ++ int ep); diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 3ed843649e..b5be1cdd89 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -437,30 +437,25 @@ let cc_tactic depth additionnal_terms = let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> - let open Glob_term in - let env = Proofview.Goal.env gl in - let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in - let pr_missing (c, missing) = - let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in - let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) - in - Feedback.msg_info - (Pp.str "Goal is solvable by congruence but some arguments are missing."); - Feedback.msg_info - (Pp.str " Try " ++ - hov 8 - begin - str "\"congruence with (" ++ - prlist_with_sep - (fun () -> str ")" ++ spc () ++ str "(") - pr_missing - terms_to_complete ++ - str ")\"," - end ++ - Pp.str " replacing metavariables by arbitrary terms."); - Tacticals.New.tclFAIL 0 (str "Incomplete") + let open Glob_term in + let env = Proofview.Goal.env gl in + let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in + let pr_missing (c, missing) = + let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in + let holes = List.init missing (fun _ -> hole) in + Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) + in + let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing." + ++ fnl () ++ + str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") + pr_missing terms_to_complete ++ str ")\"," + end ++ + str " replacing metavariables by arbitrary terms.") in + Tacticals.New.tclFAIL 0 msg | Contradiction dis -> let env = Proofview.Goal.env gl in let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 78c6255c1e..cca212f332 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -754,18 +754,6 @@ and extract_cst_app env sg mle mlt kn args = let la = List.length args in (* The ml arguments, already expunged from known logical ones *) let mla = make_mlargs env sg mle s args metas in - let mla = - if magic1 || lang () != Ocaml then mla - else - try - (* for better optimisations later, we discard dependent args - of projections and replace them by fake args that will be - removed during final pretty-print. *) - let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in - if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' - else mla - with e when CErrors.noncritical e -> mla - in (* For strict languages, purely logical signatures lead to a dummy lam (except when [Kill Ktype] everywhere). So a [MLdummy] is left accordingly. *) diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index e222fbc808..4f077b08b6 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -128,7 +128,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> {Feedback. msg_info (print_extraction_inline ()) } + -> {Feedback.msg_notice (print_extraction_inline ()) } END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF @@ -150,7 +150,7 @@ END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> { Feedback.msg_info (print_extraction_blacklist ()) } + -> { Feedback.msg_notice (print_extraction_blacklist ()) } END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2d5872718f..000df26858 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -779,7 +779,7 @@ let eta_red e = else e | _ -> e -(* Performs an eta-reduction when the core is atomic, +(* Performs an eta-reduction when the core is atomic and value, or otherwise returns None *) let atomic_eta_red e = @@ -789,7 +789,7 @@ let atomic_eta_red e = | MLapp (f,a) when test_eta_args_lift 0 n a -> (match f with | MLrel k when k>n -> Some (MLrel (k-n)) - | MLglob _ | MLexn _ | MLdummy _ -> Some f + | MLglob _ | MLdummy _ -> Some f | _ -> None) | _ -> None @@ -1547,6 +1547,7 @@ let inline r t = not (to_keep r) (* The user DOES want to keep it *) && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) - || (lang () != Haskell && not (is_projection r) && - (is_recursor r || manual_inline r || inline_test r t))) + || (lang () != Haskell && + (is_projection r || is_recursor r || + manual_inline r || inline_test r t))) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 75fb35192b..e7004fe9af 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -229,12 +229,7 @@ let rec pp_expr par env args = and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2)) - | MLglob r -> - (try - let args = List.skipn (projection_arity r) args in - let record = List.hd args in - pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with e when CErrors.noncritical e -> apply (pp_global Term r)) + | MLglob r -> apply (pp_global Term r) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -324,10 +319,14 @@ and pp_record_proj par env typ t pv args = let n = List.length ids in let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in let rel_i,a = match body with - | MLrel i when i <= n -> i,[] - | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a + | MLrel i | MLmagic(MLrel i) when i <= n -> i,[] + | MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a)) + | MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a | _ -> raise Impossible in + let magic = + match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false + in let rec lookup_rel i idx = function | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l | Pwild :: l -> lookup_rel i (idx+1) l @@ -343,7 +342,10 @@ and pp_record_proj par env typ t pv args = let pp_args = (List.map (pp_expr true env' []) a) @ args in let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx in - pp_apply pp_head par pp_args + if magic then + pp_apply (str "Obj.magic") par (pp_head :: pp_args) + else + pp_apply pp_head par pp_args and pp_record_pat (fields, args) = str "{ " ++ @@ -579,14 +581,10 @@ let pp_decl = function | Dterm (r, a, t) -> let def = if is_custom r then str (" = " ^ find_custom r) - else if is_projection r then - (prvect str (Array.make (projection_arity r) " _")) ++ - str " x = x." else pp_function (empty_env ()) a in let name = pp_global Term r in - let postdef = if is_projection r then name else mt () in - pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ()) | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 8a5c32b8b5..35cd10a1ff 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -83,7 +83,7 @@ END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY | [ "Print" "Firstorder" "Solver" ] -> { - Feedback.msg_info + Feedback.msg_notice (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) } END diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 92b7f2accf..570b72136c 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -234,6 +234,23 @@ let change_property_sort evd toSort princ princName = ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params) +(* XXX: To be cleaned up soon in favor of common save path. *) +let save name const ?hook uctx scope kind = + let open Declare in + let open DeclareDef in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in + let r = match scope with + | Discharge -> + let c = SectionLocalDef const in + let () = declare_variable ~name ~kind c in + GlobRef.VarRef name + | Global local -> + let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in + GlobRef.ConstRef kn + in + DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); + definition_message name + let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof old_princ_type sorts new_princ_name funs i proof_tac diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6d91c2a348..80fc64fe65 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -107,29 +107,6 @@ let find_reference sl s = let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) -(*****************************************************************) -(* Copy of the standard save mechanism but without the much too *) -(* slow reduction function *) -(*****************************************************************) -open Declare -open DeclareDef - -let definition_message = Declare.definition_message - -let save name const ?hook uctx scope kind = - let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in - let r = match scope with - | Discharge -> - let c = SectionLocalDef const in - let () = declare_variable ~name ~kind c in - GlobRef.VarRef name - | Global local -> - let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in - GlobRef.ConstRef kn - in - DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); - definition_message name - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 34fb10bb67..cd5202a6c7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,15 +42,6 @@ val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val make_eq : unit -> EConstr.constr -val save - : Id.t - -> Evd.side_effects Declare.proof_entry - -> ?hook:DeclareDef.Hook.t - -> UState.t - -> DeclareDef.locality - -> Decls.logical_kind - -> unit - (* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 21d61d1f97..f7215a9d13 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1100,7 +1100,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY -| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) } +| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 455c8ab003..61cc77c42a 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -145,7 +145,7 @@ open Pp VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY | [ "Show" "Obligation" "Tactic" ] -> { - Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) } + Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) } END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY @@ -154,8 +154,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) } -| [ "Preterm" ] -> { Feedback.msg_info (show_term None) } +| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) } +| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) } END { diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9d46bbc74e..fe5ebf1172 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -417,7 +417,7 @@ let get_timer name = let finish_timing ~prefix name = let tend = System.get_time () in let tstart = get_timer name in - Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++ + Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++ System.fmt_time_difference tstart tend) (* ******************** *) @@ -431,7 +431,7 @@ let print_results_filter ~cutoff ~filter = let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in - Feedback.msg_info (to_string ~cutoff ~filter results) + Feedback.msg_notice (to_string ~cutoff ~filter results) ;; let print_results ~cutoff = diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 78bfe480b3..2762bb6b32 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -19,6 +19,47 @@ Require Export Ring_theory. Local Open Scope positive_scope. Import RingSyntax. +(** Definition of polynomial expressions *) +#[universes(template)] +Inductive PExpr {C} : Type := +| PEc : C -> PExpr +| PEX : positive -> PExpr +| PEadd : PExpr -> PExpr -> PExpr +| PEsub : PExpr -> PExpr -> PExpr +| PEmul : PExpr -> PExpr -> PExpr +| PEopp : PExpr -> PExpr +| PEpow : PExpr -> N -> PExpr. +Arguments PExpr : clear implicits. + + (* Definition of multivariable polynomials with coefficients in C : + Type [Pol] represents [X1 ... Xn]. + The representation is Horner's where a [n] variable polynomial + (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients + are polynomials with [n-1] variables (C[X2..Xn]). + There are several optimisations to make the repr compacter: + - [Pc c] is the constant polynomial of value c + == c*X1^0*..*Xn^0 + - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. + variable indices are shifted of j in Q. + == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} + - [PX P i Q] is an optimised Horner form of P*X^i + Q + with P not the null polynomial + == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + + In addition: + - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden + since they can be represented by the simpler form (PX P (i+j) Q) + - (Pinj i (Pinj j P)) is (Pinj (i+j) P) + - (Pinj i (Pc c)) is (Pc c) + *) + +#[universes(template)] +Inductive Pol {C} : Type := +| Pc : C -> Pol +| Pinj : positive -> Pol -> Pol +| PX : Pol -> positive -> Pol -> Pol. +Arguments Pol : clear implicits. + Section MakeRingPol. (* Ring elements *) @@ -96,33 +137,11 @@ Section MakeRingPol. match goal with |- ?t == _ => mul_permut_rec t end). - (* Definition of multivariable polynomials with coefficients in C : - Type [Pol] represents [X1 ... Xn]. - The representation is Horner's where a [n] variable polynomial - (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients - are polynomials with [n-1] variables (C[X2..Xn]). - There are several optimisations to make the repr compacter: - - [Pc c] is the constant polynomial of value c - == c*X1^0*..*Xn^0 - - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. - variable indices are shifted of j in Q. - == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} - - [PX P i Q] is an optimised Horner form of P*X^i + Q - with P not the null polynomial - == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + Notation PExpr := (PExpr C). + Notation Pol := (Pol C). - In addition: - - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden - since they can be represented by the simpler form (PX P (i+j) Q) - - (Pinj i (Pinj j P)) is (Pinj (i+j) P) - - (Pinj i (Pc c)) is (Pc c) - *) - - #[universes(template)] - Inductive Pol : Type := - | Pc : C -> Pol - | Pinj : positive -> Pol -> Pol - | PX : Pol -> positive -> Pol -> Pol. + Implicit Types pe : PExpr. + Implicit Types P : Pol. Definition P0 := Pc cO. Definition P1 := Pc cI. @@ -152,7 +171,7 @@ Section MakeRingPol. | _ => Pinj j P end. - Definition mkPinj_pred j P:= + Definition mkPinj_pred j P := match j with | xH => P | xO j => Pinj (Pos.pred_double j) P @@ -938,18 +957,6 @@ Qed. rewrite <- IHm; auto. Qed. - (** Definition of polynomial expressions *) - - #[universes(template)] - Inductive PExpr : Type := - | PEc : C -> PExpr - | PEX : positive -> PExpr - | PEadd : PExpr -> PExpr -> PExpr - | PEsub : PExpr -> PExpr -> PExpr - | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr - | PEpow : PExpr -> N -> PExpr. - (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index a99f21ad47..3c72d3268f 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -68,7 +68,7 @@ Require Import EnvRing. Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := match e with | PEc c => c - | PEX _ j => env j + | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) @@ -80,7 +80,7 @@ Lemma Qeval_expr_simpl : forall env e, Qeval_expr env e = match e with | PEc c => c - | PEX _ j => env j + | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 75801162a7..cddc140f51 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -289,7 +289,6 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor). now apply (Rplus_nonneg_nonneg sor). Qed. -#[universes(template)] Inductive Psatz : Type := | PsatzIn : nat -> Psatz | PsatzSquare : PolC -> Psatz @@ -892,7 +891,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C := | Pc c => PEc c | Pinj j p => xdenorm (Pos.add j jmp ) p | PX p j q => PEadd - (PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j))) + (PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j))) (xdenorm (Pos.succ jmp) q) end. @@ -961,7 +960,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). Fixpoint map_PExpr (e : PExpr S) : PExpr C := match e with | PEc c => PEc (C_of_S c) - | PEX _ p => PEX _ p + | PEX p => PEX p | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 56032befba..d6ccf582ae 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -27,7 +27,6 @@ Section S. Context {AA : Type}. (* type of annotations for atoms *) Context {AF : Type}. (* type of formulae identifiers *) - #[universes(template)] Inductive GFormula : Type := | TT : GFormula | FF : GFormula diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 79cb6a3a3e..f93fe021f9 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -27,16 +27,18 @@ Set Implicit Arguments. * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up. *) +Inductive t {A} : Type := +| Empty : t +| Elt : A -> t +| Branch : t -> A -> t -> t . +Arguments t : clear implicits. + Section MakeVarMap. Variable A : Type. Variable default : A. - #[universes(template)] - Inductive t : Type := - | Empty : t - | Elt : A -> t - | Branch : t -> A -> t -> t . + Notation t := (t A). Fixpoint find (vm : t) (p:positive) {struct vm} : A := match vm with @@ -49,7 +51,6 @@ Section MakeVarMap. end end. - Fixpoint singleton (x:positive) (v : A) : t := match x with | xH => Elt v diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 3ea7635244..c0d22486b5 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -65,7 +65,7 @@ Qed. Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := match e with | PEc c => c - | PEX _ x => env x + | PEX x => env x | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2 | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2 | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n) @@ -78,7 +78,7 @@ Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x Fixpoint Zeval_const (e: PExpr Z) : option Z := match e with | PEc c => Some c - | PEX _ x => None + | PEX x => None | PEadd e1 e2 => map_option2 (fun x y => Some (x + y)) (Zeval_const e1) (Zeval_const e2) | PEmul e1 e2 => map_option2 (fun x y => Some (x * y)) @@ -742,7 +742,7 @@ Module Vars. Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t := match e with | PEc _ => Vars.empty - | PEX _ x => Vars.singleton x + | PEX x => Vars.singleton x | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 => let v1 := vars_of_pexpr e1 in let v2 := vars_of_pexpr e2 in @@ -774,10 +774,10 @@ Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type} end. Definition bound_var (v : positive) : Formula Z := - Build_Formula (PEX _ v) OpGe (PEc 0). + Build_Formula (PEX v) OpGe (PEc 0). Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := - Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)). + Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)). Section BOUND. Context {TX TG ID : Type}. diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index a64a5a84b3..cd620bd4a9 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -556,6 +556,15 @@ let zeq_bool x y = | Eq -> true | _ -> false +type 'c pExpr = +| PEc of 'c +| PEX of positive +| PEadd of 'c pExpr * 'c pExpr +| PEsub of 'c pExpr * 'c pExpr +| PEmul of 'c pExpr * 'c pExpr +| PEopp of 'c pExpr +| PEpow of 'c pExpr * n + type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -868,15 +877,6 @@ let rec psquare cO cI cadd cmul ceqb = function let p3 = psquare cO cI cadd cmul ceqb p2 in mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 -type 'c pExpr = -| PEc of 'c -| PEX of positive -| PEadd of 'c pExpr * 'c pExpr -| PEsub of 'c pExpr * 'c pExpr -| PEmul of 'c pExpr * 'c pExpr -| PEopp of 'c pExpr -| PEpow of 'c pExpr * n - (** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **) let mk_X cO cI j = @@ -1568,14 +1568,6 @@ module PositiveSet = type q = { qnum : z; qden : positive } -(** val qnum : q -> z **) - -let qnum x = x.qnum - -(** val qden : q -> positive **) - -let qden x = x.qden - (** val qeq_bool : q -> q -> bool **) let qeq_bool x y = diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 64cb3a8355..6da0c754f4 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -446,10 +446,6 @@ module PositiveSet : type q = { qnum : z; qden : positive } -val qnum : q -> z - -val qden : q -> positive - val qeq_bool : q -> q -> bool val qle_bool : q -> q -> bool diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 0ca0d0c12d..6b92445326 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -77,20 +77,24 @@ Lget i (l ++ delta) = Some a. induction l;destruct i;simpl;try congruence;auto. Qed. -Section Store. - -Variable A:Type. - -#[universes(template)] -Inductive Poption : Type:= +Inductive Poption {A} : Type:= PSome : A -> Poption | PNone : Poption. +Arguments Poption : clear implicits. -#[universes(template)] -Inductive Tree : Type := +Inductive Tree {A} : Type := Tempty : Tree | Branch0 : Tree -> Tree -> Tree | Branch1 : A -> Tree -> Tree -> Tree. +Arguments Tree : clear implicits. + +Section Store. + +Variable A:Type. + +Notation Poption := (Poption A). +Notation Tree := (Tree A). + Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := match T with @@ -179,7 +183,6 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*; destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. Qed. -#[universes(template)] Record Store : Type := mkStore {index:positive;contents:Tree}. @@ -194,7 +197,6 @@ Lemma get_empty : forall i, get i empty = PNone. intro i; case i; unfold empty,get; simpl;reflexivity. Qed. -#[universes(template)] Inductive Full : Store -> Type:= F_empty : Full empty | F_push : forall a S, Full S -> Full (push a S). diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index b4300da4d5..3736bc47a5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -730,7 +730,6 @@ Qed. (* The input: syntax of a field expression *) -#[universes(template)] Inductive FExpr : Type := | FEO : FExpr | FEI : FExpr @@ -763,7 +762,6 @@ Strategy expand [FEeval]. (* The result of the normalisation *) -#[universes(template)] Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -946,7 +944,6 @@ induction e2; intros p1 p2; now rewrite <- PEpow_mul_r. Qed. -#[universes(template)] Record rsplit : Type := mk_rsplit { rsplit_left : PExpr C; rsplit_common : PExpr C; diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index b024f65988..a98a963207 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -740,7 +740,6 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. -#[universes(template)] Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 6a8c514a7b..048c8eecf9 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) -#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 9d56084fd4..092114ff0b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -121,7 +121,6 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) - #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -909,7 +908,6 @@ Section MakeRingPol. (** Definition of polynomial expressions *) - #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 8f24b281c6..dc45853458 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -540,7 +540,6 @@ Section AddRing. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). Variable req : R -> R -> Prop. *) -#[universes(template)] Inductive ring_kind : Type := | Abstract | Computational diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index eb75fca0a1..76c393450b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -18,7 +18,6 @@ open EConstr open Vars open CClosure open Environ -open Libnames open Globnames open Glob_term open Locus @@ -151,7 +150,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in - let univs = UState.restrict_universe_context univs vars in + let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in @@ -326,19 +325,18 @@ let _ = add_map "ring" module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" -let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" let print_rings () = Feedback.msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> + Cmap.iter (fun _carrier ring -> let env = Global.env () in let sigma = Evd.from_env env in Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name + (Ppconstr.pr_id ring.ring_name ++ spc() ++ + str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req)) + ) !from_carrier let ring_for_carrier r = Cmap.find r !from_carrier @@ -361,9 +359,7 @@ let find_ring_structure env sigma l = | [] -> assert false let add_entry (sp,_kn) e = - from_carrier := Cmap.add e.ring_carrier e !from_carrier; - from_name := Spmap.add sp e !from_name - + from_carrier := Cmap.add e.ring_carrier e !from_carrier let subst_th (subst,th) = let c' = subst_mps subst th.ring_carrier in @@ -391,7 +387,8 @@ let subst_th (subst,th) = pretac' == th.ring_pre_tac && posttac' == th.ring_post_tac then th else - { ring_carrier = c'; + { ring_name = th.ring_name; + ring_carrier = c'; ring_req = eq'; ring_setoid = set'; ring_ext = ext'; @@ -428,59 +425,6 @@ let op_morph r add mul opp req m1 m2 m3 = let op_smorph r add mul req m1 m2 = lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -(* let default_ring_equality (r,add,mul,opp,req) = *) -(* let is_setoid = function *) -(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) -(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) -(* | _ -> false in *) -(* match default_relation_for_carrier ~filter:is_setoid r with *) -(* Leibniz _ -> *) -(* let setoid = lapp coq_eq_setoid [|r|] in *) -(* let op_morph = *) -(* match opp with *) -(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *) -(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *) -(* (setoid,op_morph) *) -(* | Relation rel -> *) -(* let setoid = setoid_of_relation rel in *) -(* let is_endomorphism = function *) -(* { args=args } -> List.for_all *) -(* (function (var,Relation rel) -> *) -(* var=None && eq_constr_nounivs req rel *) -(* | _ -> false) args in *) -(* let add_m = *) -(* try default_morphism ~filter:is_endomorphism add *) -(* with Not_found -> *) -(* error "ring addition should be declared as a morphism" in *) -(* let mul_m = *) -(* try default_morphism ~filter:is_endomorphism mul *) -(* with Not_found -> *) -(* error "ring multiplication should be declared as a morphism" in *) -(* let op_morph = *) -(* match opp with *) -(* | Some opp -> *) -(* (let opp_m = *) -(* try default_morphism ~filter:is_endomorphism opp *) -(* with Not_found -> *) -(* error "ring opposite should be declared as a morphism" in *) -(* let op_morph = *) -(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *) -(* msgnl *) -(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *) -(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) -(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *) -(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *) -(* str"\""); *) -(* op_morph) *) -(* | None -> *) -(* (msgnl *) -(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *) -(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) -(* str"\""++spc()++str"and \""++ *) -(* pr_constr mul_m.morphism_theory++str"\""); *) -(* op_smorph r add mul req add_m.lem mul_m.lem) in *) -(* (setoid,op_morph) *) - let ring_equality env evd (r,add,mul,opp,req) = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> @@ -657,7 +601,8 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div let _ = Lib.add_leaf name (theory_to_obj - { ring_carrier = r; + { ring_name = name; + ring_carrier = r; ring_req = req; ring_setoid = sth; ring_ext = params.(1); @@ -835,19 +780,18 @@ let dest_field env evd th_spec = | _ -> error "bad field structure" let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" -let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" let print_fields () = Feedback.msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> + Cmap.iter (fun _carrier fi -> let env = Global.env () in let sigma = Evd.from_env env in Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + (Id.print fi.field_name ++ spc() ++ str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name + ) !field_from_carrier let field_for_carrier r = Cmap.find r !field_from_carrier @@ -871,8 +815,7 @@ let find_field_structure env sigma l = | [] -> assert false let add_field_entry (sp,_kn) e = - field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier; - field_from_name := Spmap.add sp e !field_from_name + field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier let subst_th (subst,th) = let c' = subst_mps subst th.field_carrier in @@ -898,7 +841,8 @@ let subst_th (subst,th) = pretac' == th.field_pre_tac && posttac' == th.field_post_tac then th else - { field_carrier = c'; + { field_name = th.field_name; + field_carrier = c'; field_req = eq'; field_cst_tac = tac'; field_pow_tac = pow_tac'; @@ -983,7 +927,8 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od let _ = Lib.add_leaf name (ftheory_to_obj - { field_carrier = r; + { field_name = name; + field_carrier = r; field_req = req; field_cst_tac = cst_tac; field_pow_tac = pow_tac; diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index 0a3e7bd9ca..b81f5f7d14 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -40,7 +40,8 @@ type 'constr field_mod = | Inject of constr_expr type ring_info = - { ring_carrier : types; + { ring_name : Names.Id.t; + ring_carrier : types; ring_req : constr; ring_setoid : constr; ring_ext : constr; @@ -54,7 +55,8 @@ type ring_info = ring_post_tac : glob_tactic_expr } type field_info = - { field_carrier : types; + { field_name : Names.Id.t; + field_carrier : types; field_req : constr; field_cst_tac : glob_tactic_expr; field_pow_tac : glob_tactic_expr; diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 0a3e7bd9ca..b81f5f7d14 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -40,7 +40,8 @@ type 'constr field_mod = | Inject of constr_expr type ring_info = - { ring_carrier : types; + { ring_name : Names.Id.t; + ring_carrier : types; ring_req : constr; ring_setoid : constr; ring_ext : constr; @@ -54,7 +55,8 @@ type ring_info = ring_post_tac : glob_tactic_expr } type field_info = - { field_carrier : types; + { field_name : Names.Id.t; + field_carrier : types; field_req : constr; field_cst_tac : glob_tactic_expr; field_pow_tac : glob_tactic_expr; diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index bf0761d3ae..376410658a 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed. (** Variant of simpl_pred specialised to the membership operator. **) -#[universes(template)] Variant mem_pred T := Mem of pred T. (** @@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T). Definition Acoll : collective_pred T := [pred x | ...]. as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl. **) -#[universes(template)] Structure registered_applicative_pred p := RegisteredApplicativePred { applicative_pred_value :> pred T; _ : applicative_pred_value = p @@ -1473,21 +1471,18 @@ Definition ApplicativePred p := RegisteredApplicativePred (erefl p). Canonical applicative_pred_applicative sp := ApplicativePred (applicative_pred_of_simpl sp). -#[universes(template)] Structure manifest_simpl_pred p := ManifestSimplPred { simpl_pred_value :> simpl_pred T; _ : simpl_pred_value = SimplPred p }. Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)). -#[universes(template)] Structure manifest_mem_pred p := ManifestMemPred { mem_pred_value :> mem_pred T; _ : mem_pred_value = Mem [eta p] }. Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])). -#[universes(template)] Structure applicative_mem_pred p := ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}. Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) := @@ -1538,7 +1533,6 @@ End PredicateSimplification. (** Qualifiers and keyed predicates. **) -#[universes(template)] Variant qualifier (q : nat) T := Qualifier of {pred T}. Coercion has_quality n T (q : qualifier n T) : {pred T} := @@ -1573,7 +1567,6 @@ Variable T : Type. Variant pred_key (p : {pred T}) := DefaultPredKey. Variable p : {pred T}. -#[universes(template)] Structure keyed_pred (k : pred_key p) := PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}. @@ -1605,7 +1598,6 @@ Section KeyedQualifier. Variables (T : Type) (n : nat) (q : qualifier n T). -#[universes(template)] Structure keyed_qualifier (k : pred_key q) := PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}. Definition KeyedQualifier k := PackKeyedQualifier k (erefl q). diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 473612fda7..dbb60e6712 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -680,6 +680,10 @@ let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty +let pfe_new_type gl = + let sigma, env, it = project gl, pf_env gl, sig_it gl in + let sigma,t = Evarutil.new_Type sigma in + re_sig it sigma, t let pfe_type_relevance_of gl t = let gl, ty = pfe_type_of gl t in gl, ty, pf_apply Retyping.relevance_of_term gl t diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e920bc318a..db1d2d456e 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -205,6 +205,7 @@ val pf_type_of : val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types +val pfe_new_type : Goal.goal Evd.sigma -> Goal.goal Evd.sigma * EConstr.types val pfe_type_relevance_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 71abafc22f..9ebdf71329 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key. Register abstract as plugins.ssreflect.abstract. (** Constants for tactic-views **) -#[universes(template)] Inductive external_view : Type := tactic_view of Type. (** diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 4c6b7cdcb6..742890637a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -109,6 +109,11 @@ let congrtac ((n, t), ty) ist gl = loop 1 in tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl +let pf_typecheck t gl = + let it = sig_it gl in + let sigma,_ = pf_type_of gl t in + re_sig [it] sigma + let newssrcongrtac arg ist gl = ppdebug(lazy Pp.(str"===newcongr===")); ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); @@ -134,10 +139,17 @@ let newssrcongrtac arg ist gl = tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> - let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in + let gl', t_lhs = pfe_new_type gl in + let gl', t_rhs = pfe_new_type gl' in + let lhs, gl' = mk_evar gl' t_lhs in + let rhs, gl' = mk_evar gl' t_rhs in let arrow = EConstr.mkArrow lhs Sorts.Relevant (EConstr.Vars.lift 1 rhs) in tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|]) - (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist)) + (fun lr -> + let a = ssr_congr lr in + tclTHENLIST [ pf_typecheck a + ; Proofview.V82.of_tactic (Tactics.apply a) + ; congrtac (arg, mkRType) ist ]) (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow"))) gl diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 5e600362b4..0ce3752a51 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -391,19 +391,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope. Definitions and notation for explicit functions with simplification, i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) +#[universes(template)] +Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT. + Section SimplFun. Variables aT rT : Type. -#[universes(template)] -Variant simpl_fun := SimplFun of aT -> rT. +Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x. -Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. +End SimplFun. Coercion fun_of_simpl : simpl_fun >-> Funclass. -End SimplFun. - Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope. Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope. Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope. diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index f3f1d713e9..064ea0a3e3 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -279,7 +279,7 @@ let interp_search_notation ?loc tag okey = Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns')) end; ntn | [ntn] -> - Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn + Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn | ntns' -> let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in @@ -297,7 +297,7 @@ let interp_search_notation ?loc tag okey = let rbody = glob_constr_of_notation_constr ?loc body in let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in - Feedback.msg_info (hov 0 m) in + Feedback.msg_notice (hov 0 m) in if List.length !scs > 1 then let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in @@ -464,7 +464,7 @@ let interp_modloc mr = let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in - Feedback.msg_info (hov 2 pr_res ++ fnl ()) + Feedback.msg_notice (hov 2 pr_res ++ fnl ()) } @@ -559,7 +559,7 @@ END let print_view_hints env sigma kind l = let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in let pp_hints = pr_list spc (pr_rawhintref env sigma) l in - Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) + Feedback.msg_notice (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) } diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index be21a3a60d..288a349b8b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -773,7 +773,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in + Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> @@ -1569,7 +1569,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ + Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7362955eb7..df161b747a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -918,7 +918,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let () = if !debug_RAKAM then let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_notice + Feedback.msg_debug (h 0 (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ @@ -927,7 +927,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let c0 = EConstr.kind sigma x in let fold () = let () = if !debug_RAKAM then - let open Pp in Feedback.msg_notice (str "<><><><><>") in + let open Pp in Feedback.msg_debug (str "<><><><><>") in ((EConstr.of_kind c0, stack),cst_l) in match c0 with diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f82b9cef68..fb0b1eca8d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,14 +35,14 @@ module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -221,14 +221,22 @@ let print_if_is_coercion ref = (*******************) (* *) +let pr_template_variables = function + | [] -> mt () + | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - [ pr_global ref ++ str " is " ++ str - (if poly then "universe polymorphic" + let template_checked = Global.is_template_checked ref in + let template_variables = Global.get_template_polymorphic_variables ref in + [ pr_global ref ++ str " is " ++ + (if poly then str "universe polymorphic" else if template_poly then - "template universe polymorphic" - else "not universe polymorphic") ] + (if not template_checked then str "assumed " else mt()) ++ + str "template universe polymorphic " + ++ h 0 (pr_template_variables template_variables) + else str "not universe polymorphic") ] let print_type_in_type ref = let unsafe = Global.is_type_in_type ref in @@ -552,10 +560,10 @@ let print_instance sigma cb = let inst = Univ.make_abstract_instance univs in pr_universe_instance sigma inst else mt() - -let print_constant with_values sep sp udecl = + +let print_constant indirect_accessor with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in + let val_0 = Global.body_of_constant_body indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -563,7 +571,7 @@ let print_constant with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -593,8 +601,8 @@ let print_constant with_values sep sp udecl = (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos sp udecl = - print_constant true " = " sp udecl ++ +let gallina_print_constant_with_infos indirect_accessor sp udecl = + print_constant indirect_accessor true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -610,7 +618,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -621,7 +629,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant with_values sep (Constant.make1 kn) None) + Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| @@ -637,24 +645,24 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = Some (print_modtype (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry env sigma with_values ent = +let gallina_print_library_entry indirect_accessor env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry env sigma with_values (oname,lobj) + gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> - Some (str " >>>>>>> Section " ++ pr_name oname) + Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> - Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> - Some (str " >>>>>>> Module " ++ pr_name oname) + Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context env sigma with_values = +let gallina_print_context indirect_accessor env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry env sigma with_values h with - | None -> prec n rest - | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) + (match gallina_print_library_entry indirect_accessor env sigma with_values h with + | None -> prec n rest + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec @@ -712,10 +720,10 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context env sigma = print_context env sigma true None (Lib.contents ()) -let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) +let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) -let print_full_pure_context env sigma = +let print_full_pure_context ~library_accessor env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -731,8 +739,8 @@ let print_full_pure_context env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)) - | Def c -> + str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ pr_lconstr_env env sigma (Mod_subst.force_constr c) @@ -779,11 +787,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context env sigma sec = - print_context env sigma true None (read_sec_context sec) +let print_sec_context indirect_accessor env sigma sec = + print_context indirect_accessor env sigma true None (read_sec_context sec) -let print_sec_context_typ env sigma sec = - print_context env sigma false None (read_sec_context sec) +let print_sec_context_typ indirect_accessor env sigma sec = + print_context indirect_accessor env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -793,11 +801,11 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name env sigma na udecl = +let print_any_name indirect_accessor env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos sp udecl + | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp @@ -816,34 +824,34 @@ let print_any_name env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name env sigma na udecl = +let print_name indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + print_any_name indirect_accessor env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) - udecl + udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name env sigma (locate_any_name ref) udecl + print_any_name indirect_accessor env sigma (locate_any_name ref) udecl -let print_opaque_name env sigma qid = +let print_opaque_name indirect_accessor env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> - let cb = Global.lookup_constant cst in - if Declareops.constant_has_body cb then - print_constant_with_infos cst None - else - user_err Pp.(str "Not a defined constant.") + let cb = Global.lookup_constant cst in + if Declareops.constant_has_body cb then + print_constant_with_infos indirect_accessor cst None + else + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> - print_inductive sp None + print_inductive sp None | ConstructRef cstr as gr -> - let ty, ctx = Typeops.type_of_global_in_context env gr in - let ty = EConstr.of_constr ty in - let open EConstr in - print_typed_value_in_env env sigma (mkConstruct cstr, ty) + let ty, ctx = Typeops.type_of_global_in_context env gr in + let ty = EConstr.of_constr ty in + let open EConstr in + print_typed_value_in_env env sigma (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> print_named_decl env sigma + env |> lookup_named id |> print_named_decl env sigma let print_about_any ?loc env sigma k udecl = maybe_error_reject_univ_decl k udecl; @@ -880,9 +888,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect env sigma depth = - print_context env sigma false (Some depth) (Lib.contents ()) - +let inspect indirect_accessor env sigma depth = + print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 7485f4bd19..4299bcc880 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -18,22 +18,41 @@ open Libnames val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context : env -> Evd.evar_map -> Pp.t -val print_full_context_typ : env -> Evd.evar_map -> Pp.t -val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t +val print_context + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t +val print_full_context_typ + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + +val print_full_pure_context + : library_accessor:Opaqueproof.indirect_accessor + -> env + -> Evd.evar_map + -> Pp.t + +val print_sec_context + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> - UnivNames.univ_name_list option -> Pp.t -val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t +val print_name + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option -> Pp.t +val print_opaque_name + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -50,7 +69,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : env -> Evd.evar_map -> int -> Pp.t +val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -83,14 +102,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/printing/printer.ml b/printing/printer.ml index e3225fadd5..328082fbc2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -854,6 +854,8 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -873,10 +875,13 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 + | TemplatePolymorphic m1, TemplatePolymorphic m2 -> + MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 + | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -937,6 +942,9 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TemplatePolymorphic m -> + hov 2 (safe_pr_inductive env m ++ spc () ++ + strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in diff --git a/printing/printer.mli b/printing/printer.mli index 788f303aee..d62d3789d3 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -192,6 +192,8 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = diff --git a/stm/stm.ml b/stm/stm.ml index 7f0632bd7c..1042061021 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2617,13 +2617,10 @@ let dirpath_of_file f = let new_doc { doc_type ; iload_path; require_libs; stm_options } = - let load_objs libs = - let rq_file (dir, from, exp) = - let mp = Libnames.qualid_of_string dir in - let mfrom = Option.map Libnames.qualid_of_string from in - Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - List.(iter rq_file (rev libs)) - in + let require_file (dir, from, exp) = + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2662,7 +2659,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = end; (* Import initial libraries. *) - load_objs require_libs; + List.iter require_file require_libs; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; diff --git a/tactics/auto.ml b/tactics/auto.ml index 67f49f0074..0b465418f2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -220,13 +220,13 @@ let tclLOG (dbg,_,depth,trace) pp tac = tac >>= fun v -> tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*success*)"); + Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*success*)"); tclUNIT v ) tclUNIT (fun (exn, info) -> tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)"); + Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)"); tclZERO ~info exn)) | Info -> (* For "info (trivial/auto)", we store a log trace *) @@ -260,19 +260,19 @@ let pr_info_atom env sigma (d,pp) = let pr_info_trace env sigma = function | (Info,_,_,{contents=(d,Some pp)::l}) -> - Feedback.msg_info (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l)) + Feedback.msg_notice (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l)) | _ -> () let pr_info_nop = function - | (Info,_,_,_) -> Feedback.msg_info (str "idtac.") + | (Info,_,_,_) -> Feedback.msg_notice (str "idtac.") | _ -> () let pr_dbg_header = function | (Off,_,_,_) -> () - | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)") - | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") - | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)") - | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)") + | (Debug,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* debug trivial: *)") + | (Debug,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* debug auto: *)") + | (Info,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* info trivial: *)") + | (Info,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* info auto: *)") let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index d4e4322bef..2ce32b309a 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -351,13 +351,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> Feedback.msg_info (str "idtac.") + | Info -> Feedback.msg_notice (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () - | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") - | Info -> Feedback.msg_info (str "(* info eauto: *)") + | Debug -> Feedback.msg_notice (str "(* debug eauto: *)") + | Info -> Feedback.msg_notice (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () @@ -368,7 +368,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_notice (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v new file mode 100644 index 0000000000..a079d672d3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9294.v @@ -0,0 +1,29 @@ +Set Printing Universes. + +Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A. +Arguments foo {_} _. +Print Universes Subgraph (Foo.i). +Definition bar : Foo True -> Set := fun '(foo x) => x. + +Definition foo_bar (n : Foo True) : foo (bar n) = n. +Proof. destruct n;reflexivity. Qed. + +Definition bar_foo (n : Set) : bar (foo n) = n. +Proof. reflexivity. Qed. + +Require Import Hurkens. + +Inductive box (A : Set) : Prop := Box : A -> box A. + +Definition Paradox : False. +Proof. +Fail unshelve refine ( + NoRetractFromSmallPropositionToProp.paradox + (Foo True) + (fun A => foo A) + (fun A => box (bar A)) + _ + _ + False +). +Abort. diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v index bc5cd0fb68..4b6916af55 100644 --- a/test-suite/coqchk/inductive_functor_template.v +++ b/test-suite/coqchk/inductive_functor_template.v @@ -2,7 +2,7 @@ Module Type E. Parameter T : Type. End E. Module F (X:E). - #[universes(template)] Inductive foo := box : X.T -> foo. + Inductive foo := box : X.T -> foo. End F. Module ME. Definition T := nat. End ME. diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v new file mode 100644 index 0000000000..75b2a56169 --- /dev/null +++ b/test-suite/failure/Template.v @@ -0,0 +1,32 @@ +(* +Module TestUnsetTemplateCheck. + Unset Template Check. + + Section Foo. + + Context (A : Type). + + Definition cstr := nat : ltac:(let ty := type of A in exact ty). + + Inductive myind := + | cons : A -> myind. + End Foo. + + (* Can only succeed if no template check is performed *) + Check myind True : Prop. + + Print Assumptions myind. + (* + Axioms: + myind is template polymorphic on all its universe parameters. + *) + About myind. +(* +myind : Type@{Top.60} -> Type@{Top.60} + +myind is assumed template universe polymorphic on Top.60 +Argument scope is [type_scope] +Expands to: Inductive Top.TestUnsetTemplateCheck.myind +*) +End TestUnsetTemplateCheck. +*) diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4e949dcb04..a040b69b44 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -84,7 +84,6 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) -#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 6976f35a88..0e84bf3966 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f9398fdca9..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - #[universes(template)] Inductive decoder_result : Type := + Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 9b25c2dbd3..61ae4edbd1 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -#[universes(template)] CoInductive Inf := S { projS : Inf }. +CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 29614c032a..aeebc0f98b 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -#[universes(template)] Inductive ftele : Type := +Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0c1b08f5a3..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. +Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index ab4172711e..e788977fb7 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,6 +1,6 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} -existT is template universe polymorphic +existT is template universe polymorphic on sigT.u0 sigT.u1 Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 35f36e87d7..14d63d39c4 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -6,7 +6,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - #[universes(template)] Record store := { store_funcs : host_func }. + Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 4fe7b051f8..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -#[universes(template)] Record N := C { T : Type; _ : True }. +Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -#[universes(template)] Record M := D { U : Type; a := 0; q : True }. +Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 99183f2064..9cf6ad35b8 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - #[universes(template)] Inductive foo := f. + Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - #[universes(template)] Inductive foo := f. + Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. End B. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 222a808768..a89fd64999 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -68,9 +68,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.32} in -let ff := Type@{UnivBinders.34} in tt -> ff - : Type@{max(UnivBinders.31,UnivBinders.33)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -143,16 +143,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axfoo@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axbar@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axbar is universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 0eb5db1733..7465442cab 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -#[universes(template)] Record A := { B:Type; b:B->B }. +Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out index 2761b87b02..5e81b43504 100644 --- a/test-suite/output/auto.out +++ b/test-suite/output/auto.out @@ -2,18 +2,18 @@ simple apply or_intror (in core). intro. assumption. -Debug: (* debug auto: *) -Debug: * assumption. (*fail*) -Debug: * intro. (*fail*) -Debug: * simple apply or_intror (in core). (*success*) -Debug: ** assumption. (*fail*) -Debug: ** intro. (*success*) -Debug: ** assumption. (*success*) +(* debug auto: *) +* assumption. (*fail*) +* intro. (*fail*) +* simple apply or_intror (in core). (*success*) +** assumption. (*fail*) +** intro. (*success*) +** assumption. (*success*) (* info eauto: *) simple apply or_intror. intro. exact H. -Debug: (* debug eauto: *) +(* debug eauto: *) Debug: 1 depth=5 Debug: 1.1 depth=4 simple apply or_intror Debug: 1.1.1 depth=4 intro diff --git a/test-suite/output/bug7191.out b/test-suite/output/bug7191.out new file mode 100644 index 0000000000..005455e30c --- /dev/null +++ b/test-suite/output/bug7191.out @@ -0,0 +1,9 @@ + +type unit0 = +| Tt + +(** val f : unit0 -> unit0 **) + +let f _ = + assert false (* absurd case *) + diff --git a/test-suite/output/bug7191.v b/test-suite/output/bug7191.v new file mode 100644 index 0000000000..1aa4625b6c --- /dev/null +++ b/test-suite/output/bug7191.v @@ -0,0 +1,3 @@ +Require Extraction. +Definition f (x : False) : unit -> unit := match x with end. +Recursive Extraction f. diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out new file mode 100644 index 0000000000..325ee95ae2 --- /dev/null +++ b/test-suite/output/bug7348.out @@ -0,0 +1,45 @@ +Extracted code successfully compiled + +type __ = Obj.t + +type unit0 = +| Tt + +type bool = +| True +| False + +module Case1 = + struct + type coq_rec = { f : bool } + + (** val f : bool -> coq_rec -> bool **) + + let f _ r = + r.f + + (** val silly : bool -> coq_rec -> __ **) + + let silly x b = + match x with + | True -> Obj.magic b.f + | False -> Obj.magic Tt + end + +module Case2 = + struct + type coq_rec = { f : (bool -> bool) } + + (** val f : bool -> coq_rec -> bool -> bool **) + + let f _ r = + r.f + + (** val silly : bool -> coq_rec -> __ **) + + let silly x b = + match x with + | True -> Obj.magic b.f False + | False -> Obj.magic Tt + end + diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v new file mode 100644 index 0000000000..782b27ce96 --- /dev/null +++ b/test-suite/output/bug7348.v @@ -0,0 +1,25 @@ +Require Extraction. + +Extraction Language OCaml. +Set Extraction KeepSingleton. + +Module Case1. + +Record rec (x : bool) := { f : bool }. + +Definition silly x (b : rec x) := + if x return (if x then bool else unit) then f x b else tt. + +End Case1. + +Module Case2. + +Record rec (x : bool) := { f : bool -> bool }. + +Definition silly x (b : rec x) := + if x return (if x then bool else unit) then f x b false else tt. + +End Case2. + +Extraction TestCompile Case1.silly Case2.silly. +Recursive Extraction Case1.silly Case2.silly. diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 209fedc343..57a4739e9f 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -#[universes(template)] Inductive T (n:nat) : Type := A : T n. +Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v index 026f7538e8..f85791b00b 100644 --- a/test-suite/ssr/congr.v +++ b/test-suite/ssr/congr.v @@ -32,3 +32,11 @@ Coercion f : nat >-> Equality.sort. Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a). Proof. move=> a b Eba; congr (_ + _); exact: Eba. Qed. + +Open Scope type_scope. + +Lemma test5 : forall (P Q Q' : Type) (h : Q = Q'), P * Q = P * Q'. +Proof. move=>*; by congr (_ * _). Qed. + +Lemma test6 : forall (P Q Q' : Type) (h : Q = Q'), P * Q -> P * Q'. +Proof. move=> P Q Q' h; by congr (_ * _). Qed. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index cfc25c3346..656362b8fc 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -46,3 +46,129 @@ Module No. Definition j_lebox (A:Type@{j}) := Box A. Fail Definition box_lti A := Box A : Type@{i}. End No. + +Module DefaultProp. + Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a. + + (* By default template polymorphism does not interact with inductives + which naturally fall in Prop *) + Check (identity nat 0 0 : Prop). +End DefaultProp. + +Module ExplicitTemplate. + #[universes(template)] + Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a. + + (* Weird interaction of template polymorphism and inductive types + which naturally fall in Prop: this one is template polymorphic but not on i: + it just lives in any universe *) + Check (identity Type nat nat : Prop). +End ExplicitTemplate. + +Polymorphic Definition f@{i} : Type@{i} := nat. +Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x. + +Section Foo. + Universe u. + Context (A : Type@{u}). + + Inductive Bar := + | bar : A -> Bar. + + Set Universe Minimization ToSet. + Inductive Baz := + | cbaz : A -> baz Baz -> Baz. + + Inductive Baz' := + | cbaz' : A -> baz@{Set} nat -> Baz'. + + (* 2 constructors, at least in Set *) + Inductive Bazset@{v} := + | cbaz1 : A -> baz@{v} Bazset -> Bazset + | cbaz2 : Bazset. + + Eval compute in ltac:(let T := type of A in exact T). + + Inductive Foo : Type := + | foo : A -> f -> Foo. + +End Foo. + +Set Printing Universes. +(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *) +Fail Check Bar True : Prop. +Fail Check Bar nat : Set. +About Baz. + +Check cbaz True I. + +(** Neither can it be Set *) +Fail Check Baz nat : Set. + +(** No longer possible for Baz' which contains a type in Set *) +Fail Check Baz' True : Prop. +Fail Check Baz' nat : Set. + +Fail Check Bazset True : Prop. +Fail Check Bazset True : Set. + +(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *) +Constraint u = Bazset.v. +(** As u is global it is already > Set, so: *) +Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}. + +(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *) +Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X. + +(** Would otherwise break singleton elimination and extraction. *) +Fail Check Foo True : Prop. +Fail Check Foo True : Set. + +Definition foo_proj {A} (f : Foo A) : nat := + match f with foo _ _ n => n end. + +Definition ex : Foo True := foo _ I 0. +Check foo_proj ex. + +(** See failure/Template.v for a test of the unsafe Unset Template Check usage *) + +Module AutoTemplateTest. +Set Warnings "+auto-template". +Section Foo. + Universe u'. + Context (A : Type@{u'}). + + (* Not failing as Bar cannot be made template polymorphic at all *) + Inductive Bar := + | bar : A -> Bar. +End Foo. +End AutoTemplateTest. + +Module TestTemplateAttribute. + Section Foo. + Universe u. + Context (A : Type@{u}). + + (* Failing as Bar cannot be made template polymorphic at all *) + Fail #[universes(template)] Inductive Bar := + | bar : A -> Bar. + + End Foo. +End TestTemplateAttribute. + +Module SharingWithoutSection. +Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty)) + := foo : S A -> Foo A. +Fail Check Foo True : Prop. +End SharingWithoutSection. + +Module OkNotCovered. +(* Here it happens that box is safe but we don't see it *) +Section S. +Universe u. +Variable A : Type@{u}. +Inductive box (A:Type@{u}) := Box : A -> box A. +Definition B := Set : Type@{u}. +End S. +Fail Check box True : Prop. +End OkNotCovered. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 428af5fcfe..69bd1e6c96 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -286,7 +286,6 @@ Local Open Scope list_scope. (** A compact representation of non-dependent arities, with the codomain singled-out. *) (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) -#[universes(template)] Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist. Local Infix "::" := Tcons. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 071810acdc..6858706cb3 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -27,7 +27,6 @@ Require Export Coq.Classes.Morphisms. (** A setoid wraps an equivalence. *) -#[universes(template)] Class Setoid A := { equiv : relation A ; setoid_equiv :> Equivalence equiv }. @@ -129,7 +128,6 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper ( (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) -#[universes(template)] Class PartialSetoid (A : Type) := { pequiv : relation A ; pequiv_prf :> PER pequiv }. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 5025bce093..274cb4afd3 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -14,3 +14,6 @@ Local Set Warnings "-deprecated". Require Export Coq.Compat.Coq810. Unset Private Polymorphic Universes. + +(** Unsafe flag, can hide inconsistencies. *) +Global Unset Template Check. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 801be79ba4..8627ff7353 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -45,20 +45,23 @@ Hint Transparent key : core. (** * Trees *) -Section Elt. - -Variable elt : Type. - (** * Trees The fifth field of [Node] is the height of the tree *) #[universes(template)] -Inductive tree := +Inductive tree {elt : Type} := | Leaf : tree | Node : tree -> key -> elt -> tree -> int -> tree. +Arguments tree : clear implicits. -Notation t := tree. +Section Elt. + +Variable elt : Type. + +Notation t := (tree elt). + +Implicit Types m : t. (** * Basic functions on trees: height and cardinal *) @@ -76,7 +79,7 @@ Fixpoint cardinal (m : t) : nat := (** * Empty Map *) -Definition empty := Leaf. +Definition empty : t := Leaf. (** * Emptyness test *) @@ -236,7 +239,6 @@ Fixpoint join l : key -> elt -> t -> t := - [o] is the result of [find x m]. *) -#[universes(template)] Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }. Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). @@ -293,7 +295,6 @@ Variable cmp : elt->elt->bool. (** ** Enumeration of the elements of a tree *) -#[universes(template)] Inductive enumeration := | End : enumeration | More : key -> elt -> t -> enumeration -> enumeration. @@ -338,6 +339,9 @@ Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End). End Elt. Notation t := tree. +Arguments Leaf : clear implicits. +Arguments Node [elt]. + Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). Notation "t #o" := (t_opt t) (at level 9, format "t '#o'"). diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 2af6e5c6a4..b21d809059 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -1024,7 +1024,6 @@ Module E := X. Definition key := E.t. -#[universes(template)] Record slist (elt:Type) := {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}. Definition t (elt:Type) : Type := slist elt. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 0c04437581..b9a8b0a73d 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -868,8 +868,6 @@ Module Make (X: DecidableType) <: WS with Module E:=X. Module E := X. Definition key := E.t. - -#[universes(template)] Record slist (elt:Type) := {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}. Definition t (elt:Type) := slist elt. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 38e5470e59..6984a7c2b6 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -400,8 +400,10 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined. (** [identity A a] is the family of datatypes on [A] whose sole non-empty member is the singleton datatype [identity A a a] whose sole inhabitant is denoted [identity_refl A a] *) +(** Beware: this inductive actually falls into [Prop], as the sole + constructor has no arguments and [-indices-matter] is not + activated in the standard library. *) -#[universes(template)] Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. Hint Resolve identity_refl: core. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 7f36edf5bb..38723e291f 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -536,6 +536,26 @@ Section Elts. simpl in *. apply IHn. auto with arith. Qed. + (** Results directly relating [nth] and [nth_error] *) + + Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A), + nth_error l n = Some x -> nth n l d = x. + Proof. + intros l n x d H. + apply nth_error_split in H. destruct H as [l1 [l2 [H H']]]. + subst. rewrite app_nth2; [|auto]. + rewrite Nat.sub_diag. reflexivity. + Qed. + + Lemma nth_error_nth' : forall (l : list A) (n : nat) (d : A), + n < length l -> nth_error l n = Some (nth n l d). + Proof. + intros l n d H. + apply nth_split with (d:=d) in H. destruct H as [l1 [l2 [H H']]]. + subst. rewrite H. rewrite nth_error_app2; [|auto]. + rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity. + Qed. + (*****************) (** ** Remove *) (*****************) @@ -1227,6 +1247,20 @@ End Fold_Right_Recursor. case_eq (f a); intros; simpl; intuition congruence. Qed. + Lemma filter_app (l l':list A) : + filter (l ++ l') = filter l ++ filter l'. + Proof. + induction l as [|x l IH]; simpl; trivial. + destruct (f x); simpl; now rewrite IH. + Qed. + + Lemma concat_filter_map : forall (l : list (list A)), + concat (map filter l) = filter (concat l). + Proof. + induction l as [| v l IHl]; [auto|]. + simpl. rewrite IHl. rewrite filter_app. reflexivity. + Qed. + (** [find] *) Fixpoint find (l:list A) : option A := @@ -1309,6 +1343,55 @@ End Fold_Right_Recursor. End Bool. + (*******************************) + (** ** Further filtering facts *) + (*******************************) + + Section Filtering. + Variables (A : Type). + + Lemma filter_map : forall (f g : A -> bool) (l : list A), + filter f l = filter g l <-> map f l = map g l. + Proof. + induction l as [| a l IHl]; [firstorder|]. + simpl. destruct (f a) eqn:Hfa; destruct (g a) eqn:Hga; split; intros H. + - inversion H. apply IHl in H1. rewrite H1. reflexivity. + - inversion H. apply IHl in H1. rewrite H1. reflexivity. + - assert (Ha : In a (filter g l)). { rewrite <- H. apply in_eq. } + apply filter_In in Ha. destruct Ha as [_ Hga']. rewrite Hga in Hga'. inversion Hga'. + - inversion H. + - assert (Ha : In a (filter f l)). { rewrite H. apply in_eq. } + apply filter_In in Ha. destruct Ha as [_ Hfa']. rewrite Hfa in Hfa'. inversion Hfa'. + - inversion H. + - rewrite IHl in H. rewrite H. reflexivity. + - inversion H. apply IHl. assumption. + Qed. + + Lemma filter_ext_in : forall (f g : A -> bool) (l : list A), + (forall a, In a l -> f a = g a) -> filter f l = filter g l. + Proof. + intros f g l H. rewrite filter_map. apply map_ext_in. auto. + Qed. + + Lemma ext_in_filter : forall (f g : A -> bool) (l : list A), + filter f l = filter g l -> (forall a, In a l -> f a = g a). + Proof. + intros f g l H. rewrite filter_map in H. apply ext_in_map. assumption. + Qed. + + Lemma filter_ext_in_iff : forall (f g : A -> bool) (l : list A), + filter f l = filter g l <-> (forall a, In a l -> f a = g a). + Proof. + split; [apply ext_in_filter | apply filter_ext_in]. + Qed. + + Lemma filter_ext : forall (f g : A -> bool), + (forall a, f a = g a) -> forall l, filter f l = filter g l. + Proof. + intros f g H l. rewrite filter_map. apply map_ext. assumption. + Qed. + + End Filtering. (******************************************************) @@ -1845,6 +1928,56 @@ Section Cutting. End Cutting. +(**************************************************************) +(** ** Combining pairs of lists of possibly-different lengths *) +(**************************************************************) + +Section Combining. + Variables (A B : Type). + + Lemma combine_nil : forall (l : list A), + combine l (@nil B) = @nil (A*B). + Proof. + intros l. + apply length_zero_iff_nil. + rewrite combine_length. simpl. rewrite Nat.min_0_r. + reflexivity. + Qed. + + Lemma combine_firstn_l : forall (l : list A) (l' : list B), + combine l l' = combine l (firstn (length l) l'). + Proof. + induction l as [| x l IHl]; intros l'; [reflexivity|]. + destruct l' as [| x' l']; [reflexivity|]. + simpl. specialize IHl with (l':=l'). rewrite <- IHl. + reflexivity. + Qed. + + Lemma combine_firstn_r : forall (l : list A) (l' : list B), + combine l l' = combine (firstn (length l') l) l'. + Proof. + intros l l'. generalize dependent l. + induction l' as [| x' l' IHl']; intros l. + - simpl. apply combine_nil. + - destruct l as [| x l]; [reflexivity|]. + simpl. specialize IHl' with (l:=l). rewrite <- IHl'. + reflexivity. + Qed. + + Lemma combine_firstn : forall (l : list A) (l' : list B) (n : nat), + firstn n (combine l l') = combine (firstn n l) (firstn n l'). + Proof. + induction l as [| x l IHl]; intros l' n. + - simpl. repeat (rewrite firstn_nil). reflexivity. + - destruct l' as [| x' l']. + + simpl. repeat (rewrite firstn_nil). rewrite combine_nil. reflexivity. + + simpl. destruct n as [| n]; [reflexivity|]. + repeat (rewrite firstn_cons). simpl. + rewrite IHl. reflexivity. + Qed. + +End Combining. + (**********************************************************************) (** ** Predicate for List addition/removal (no need for decidability) *) (**********************************************************************) @@ -1959,6 +2092,15 @@ Section ReDun. | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs) end. + Lemma nodup_fixed_point : forall (l : list A), + NoDup l -> nodup l = l. + Proof. + induction l as [| x l IHl]; [auto|]. intros H. + simpl. destruct (in_dec decA x l) as [Hx | Hx]; rewrite NoDup_cons_iff in H. + - destruct H as [H' _]. contradiction. + - destruct H as [_ H']. apply IHl in H'. rewrite -> H'. reflexivity. + Qed. + Lemma nodup_In l x : In x (nodup l) <-> In x l. Proof. induction l as [|a l' Hrec]; simpl. diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index c11a0941fa..4c6520feb3 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -73,14 +73,17 @@ End MemoFunction. reused thanks to a temporary hiding of the dependency in a "container" [memo_val]. *) +#[universes(template)] +Inductive memo_val {A : nat -> Type} : Type := + memo_mval: forall n, A n -> memo_val. +Arguments memo_val : clear implicits. + Section DependentMemoFunction. Variable A: nat -> Type. Variable f: forall n, A n. -#[universes(template)] -Inductive memo_val: Type := - memo_mval: forall n, A n -> memo_val. +Notation memo_val := (memo_val A). Fixpoint is_eq (n m : nat) : {n = m} + {True} := match n, m return {n = m} + {True} with diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 407a7ae45d..0daae0391c 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -12,13 +12,13 @@ Set Implicit Arguments. (** Streams *) -Section Streams. +CoInductive Stream (A : Type) := + Cons : A -> Stream A -> Stream A. -Variable A : Type. +Section Streams. + Variable A : Type. -#[universes(template)] -CoInductive Stream : Type := - Cons : A -> Stream -> Stream. + Notation Stream := (Stream A). Definition hd (x:Stream) := match x with diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 4442108ffc..8a71158f4c 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -208,7 +208,6 @@ Definition concat s1 s2 := - [present] is [true] if and only if [s] contains [x]. *) -#[universes(template)] Record triple := mktriple { t_left:t; t_in:bool; t_right:t }. Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 37a169b02e..bf6336ae47 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -48,7 +48,6 @@ Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. Hint Transparent elt : core. -#[universes(template)] Inductive tree : Type := | Leaf : tree | Node : Info.t -> tree -> X.t -> tree -> tree. @@ -168,7 +167,6 @@ end. (** Enumeration of the elements of a tree. This corresponds to the "samefringe" notion in the literature. *) -#[universes(template)] Inductive enumeration := | End : enumeration | More : elt -> tree -> enumeration -> enumeration. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 29c84d0d1a..33f6b1050c 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -439,7 +439,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. Definition elt := E.t. -#[universes(template)] Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}. Definition t := t_. Arguments Mkt this {is_ok}. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index a3e0ec5884..b5389e9121 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -1049,12 +1049,8 @@ Qed. (** ** Filter *) -Lemma filter_app A f (l l':list A) : - List.filter f (l ++ l') = List.filter f l ++ List.filter f l'. -Proof. - induction l as [|x l IH]; simpl; trivial. - destruct (f x); simpl; now rewrite IH. -Qed. +#[deprecated(since="8.11",note="Lemma filter_app has been moved to module List.")] +Notation filter_app := List.filter_app. Lemma filter_aux_elements s f acc : filter_aux f s acc = List.filter f (elements s) ++ acc. @@ -1062,7 +1058,7 @@ Proof. revert acc. induction s as [|c l IHl x r IHr]; trivial. intros acc. - rewrite elements_node, filter_app. simpl. + rewrite elements_node, List.filter_app. simpl. destruct (f x); now rewrite IHl, IHr, app_ass. Qed. diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index 83e9c29b13..6e08378df4 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -18,46 +18,34 @@ Local Open Scope Z_scope. Definition base digits := Z.pow 2 (Zpos digits). Arguments base digits: simpl never. -Section Carry. +#[universes(template)] +Variant carry (A : Type) := +| C0 : A -> carry A +| C1 : A -> carry A. - Variable A : Type. - - #[universes(template)] - Variant carry := - | C0 : A -> carry - | C1 : A -> carry. - - Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c := +Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c := match c with | C0 x => interp x | C1 x => sign*B + interp x end. -End Carry. - -Section Zn2Z. - - Variable znz : Type. - - (** From a type [znz] representing a cyclic structure Z/nZ, - we produce a representation of Z/2nZ by pairs of elements of [znz] - (plus a special case for zero). High half of the new number comes - first. +(** From a type [znz] representing a cyclic structure Z/nZ, + we produce a representation of Z/2nZ by pairs of elements of [znz] + (plus a special case for zero). High half of the new number comes + first. *) +#[universes(template)] +Variant zn2z {znz : Type} := +| W0 : zn2z +| WW : znz -> znz -> zn2z. +Arguments zn2z : clear implicits. - #[universes(template)] - Variant zn2z := - | W0 : zn2z - | WW : znz -> znz -> zn2z. - - Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) := +Definition zn2z_to_Z znz (wB:Z) (w_to_Z:znz->Z) (x:zn2z znz) := match x with | W0 => 0 | WW xh xl => w_to_Z xh * wB + w_to_Z xl end. -End Zn2Z. - Arguments W0 {znz}. (** From a cyclic representation [w], we iterate the [zn2z] construct diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 128ee286b8..6da0fe3966 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -137,7 +137,6 @@ Definition IsStepFun (f:R -> R) (a b:R) : Type := { l:Rlist & is_subdivision f a b l }. (** ** Class of step functions *) -#[universes(template)] Record StepFun (a b:R) : Type := mkStepFun {fe :> R -> R; pre : IsStepFun fe a b}. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 5443ff68ed..c94a373ca0 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -116,7 +116,6 @@ Qed. (*******************************) (*********) -#[universes(template)] Record Metric_Space : Type := {Base : Type; dist : Base -> Base -> R; diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index cfcc82d765..d21042884e 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -380,7 +380,6 @@ Proof. apply Rinv_0_lt_compat; prove_sup0. Qed. -#[universes(template)] Record family : Type := mkfamily {ind : R -> Prop; f :> R -> R -> Prop; diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index e1d7d37e42..745db25a54 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -100,11 +100,9 @@ Hint Resolve Totally_ordered_definition Upper_Bound_definition Section Specific_orders. Variable U : Type. - #[universes(template)] Record Cpo : Type := Definition_of_cpo {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}. - #[universes(template)] Record Chain : Type := Definition_of_chain {PO_of_chain : PO U; Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index e9233a34e7..6aefcf32c0 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -22,7 +22,6 @@ Section multiset_defs. Hypothesis eqA_equiv : Equivalence eqA. Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. - #[universes(template)] Inductive multiset : Type := Bag : (A -> nat) -> multiset. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index d2fae6db28..e23d9c2f55 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -36,7 +36,6 @@ Section Partial_orders. Definition Rel := Relation U. - #[universes(template)] Record PO : Type := Definition_of_PO { Carrier_of : Ensemble U; Rel_of : Relation U; diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 76e555ed5a..48a852052e 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -42,7 +42,6 @@ Section defs. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. - #[universes(template)] Inductive Tree := | Tree_Leaf : Tree | Tree_Node : A -> Tree -> Tree -> Tree. @@ -129,8 +128,7 @@ Section defs. (** ** Merging two sorted lists *) - #[universes(template)] - Inductive merge_lem (l1 l2:list A) : Type := + Inductive merge_lem (l1 l2:list A) : Type := merge_exist : forall l:list A, Sorted leA l -> @@ -203,7 +201,6 @@ Section defs. (** ** Specification of heap insertion *) - #[universes(template)] Inductive insert_spec (a:A) (T:Tree) : Type := insert_exist : forall T1:Tree, @@ -237,7 +234,6 @@ Section defs. (** ** Building a heap from a list *) - #[universes(template)] Inductive build_heap (l:list A) : Type := heap_exist : forall T:Tree, @@ -262,7 +258,6 @@ Section defs. (** ** Building the sorted list *) - #[universes(template)] Inductive flat_spec (T:Tree) : Type := flat_exist : forall l:list A, diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index d747258f56..6ddbc8e214 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -14,17 +14,18 @@ Require Import Eqdep. +#[universes(template)] +Inductive WO (A : Type) (B : A -> Type) : Type := + sup : forall (a:A) (f:B a -> WO A B), WO A B. + Section WellOrdering. Variable A : Type. Variable B : A -> Type. - #[universes(template)] - Inductive WO : Type := - sup : forall (a:A) (f:B a -> WO), WO. - + Notation WO := (WO A B). Inductive le_WO : WO -> WO -> Prop := - le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f). + le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup _ _ a f). Theorem wf_WO : well_founded le_WO. Proof. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 577544f971..fee928430c 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -212,7 +212,6 @@ Module MoreInt (Import I:Int). | EZofI : ExprI -> ExprZ | EZraw : Z -> ExprZ. - #[universes(template)] Inductive ExprP : Type := | EPeq : ExprZ -> ExprZ -> ExprP | EPlt : ExprZ -> ExprZ -> ExprP diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index fe5361c156..3600658e23 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -39,7 +39,7 @@ let load_vernacular opts ~state = if !Flags.beautify then Flags.with_option Flags.beautify_file load_vernac f_in else load_vernac s - ) state (List.rev opts.pre.load_vernacular_list) + ) state opts.pre.load_vernacular_list let load_init_vernaculars opts ~state = let state = load_init_file opts ~state in @@ -193,7 +193,7 @@ let compile_file opts copts (f_in, echo) = compile opts copts ~echo ~f_in ~f_out let compile_files opts copts = - let compile_list = List.rev copts.compile_list in + let compile_list = copts.compile_list in List.iter (compile_file opts copts) compile_list (******************************************************************************) @@ -205,7 +205,7 @@ let check_vio_tasks copts = let f_in = ensure ".vio" f f in ensure_exists f_in; Vio_checking.check_vio (n,f_in) && acc) - true (List.rev copts.vio_tasks) in + true copts.vio_tasks in if not rc then fatal_error Pp.(str "VIO Task Check failed") (* vio files *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 64c1da20b6..113b1fb5d7 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -32,6 +32,10 @@ let set_type_in_type () = let typing_flags = Environ.typing_flags (Global.env ()) in Global.set_typing_flags { typing_flags with Declarations.check_universes = false } +let set_no_template_check () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_template = false } + (******************************************************************************) type color = [`ON | `AUTO | `EMACS | `OFF] @@ -525,6 +529,7 @@ let parse_args ~help ~init arglist : t * string list = |"-list-tags" -> set_query oval PrintTags |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval + |"-no-template-check" -> set_no_template_check (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) @@ -542,6 +547,23 @@ let parse_args ~help ~init arglist : t * string list = parse init with any -> fatal_error any +(* We need to reverse a few lists *) +let parse_args ~help ~init args = + let opts, extra = parse_args ~help ~init args in + let opts = + { opts with + pre = { opts.pre with + ml_includes = List.rev opts.pre.ml_includes + ; vo_includes = List.rev opts.pre.vo_includes + ; vo_requires = List.rev opts.pre.vo_requires + ; load_vernacular_list = List.rev opts.pre.load_vernacular_list + } + ; config = { opts.config with + set_options = List.rev opts.config.set_options + } ; + } in + opts, extra + (******************************************************************************) (* Startup LoadPath and Modules *) (******************************************************************************) @@ -552,7 +574,7 @@ let require_libs opts = if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires let cmdline_load_path opts = - List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes) + opts.pre.ml_includes @ opts.pre.vo_includes let build_load_path opts = Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @ diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 019577ac85..7658ad68a5 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -11,7 +11,7 @@ let outputstate opts = Option.iter (fun ostate_file -> let fname = CUnix.make_suffix ostate_file ".coq" in - States.extern_state fname) opts.Coqcargs.outputstate + Library.extern_state fname) opts.Coqcargs.outputstate let coqc_init _copts ~opts = Flags.quiet := true; @@ -53,7 +53,8 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) + let library_accessor = Library.indirect_accessor in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 0b5481fe72..c4e3571281 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -210,3 +210,11 @@ let parse arglist : t = check_compilation_output_name_consistency args; args with any -> fatal_error any + +let parse args = + let opts = parse args in + { opts with + compile_list = List.rev opts.compile_list + ; vio_tasks = List.rev opts.vio_tasks + ; vio_files = List.rev opts.vio_files + } diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f09d202edf..eded9f4bcd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,7 +30,7 @@ let get_version_date () = let print_header () = let (ver,rev) = get_version_date () in - Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); + Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () let print_memory_stat () = @@ -87,7 +87,7 @@ let set_options = List.iter set_option let inputstate opts = Option.iter (fun istate_file -> let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in - States.intern_state fname) opts.inputstate + Library.intern_state fname) opts.inputstate (******************************************************************************) (* Fatal Errors *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index cdb2e36fbd..8555d78156 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -82,6 +82,7 @@ let print_usage_common co command = \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -no-template-check disable checking of universes constraints on universes parameterizing template polymorphic inductive types\ \n -mangle-names x mangle auto-generated names using prefix x\ \n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ \n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index e9d8263b85..bca6b48499 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -169,6 +169,6 @@ let beautify_pass ~doc ~comments ~ids ~filename = let load_vernac ~echo ~check ~interactive ~state filename = let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in (* Pass for beautify *) - if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename; + if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:(List.rev ids) ~filename; (* End pass *) ostate diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index a72e43de01..cb034bdff6 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -353,6 +353,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in - accu - + if not mind.mind_typing_flags.check_template then + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu + else accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index d414d57c0d..98fe436a22 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -345,7 +345,7 @@ let build_beq_scheme mode kn = Vars.substl subst cores.(i) in create_input fix), - UState.make (Global.universes ())), + UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -690,7 +690,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal @@ -820,7 +820,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal @@ -996,7 +996,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index adbe196699..98b869d72e 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -114,20 +114,22 @@ let mk_mltype_data sigma env assums arity indname = inductives which are recognized when a "Type" appears at the end of the conlusion in the source syntax. *) -let rec check_anonymous_type ind = +let rec check_type_conclusion ind = let open Glob_term in match DAst.get ind with - | GSort (UAnonymous {rigid=true}) -> true + | GSort (UAnonymous {rigid=true}) -> (Some true) + | GSort (UNamed _) -> (Some false) | GProd ( _, _, _, e) | GLetIn (_, _, _, e) | GLambda (_, _, _, e) | GApp (e, _) - | GCast (e, _) -> check_anonymous_type e - | _ -> false + | GCast (e, _) -> check_type_conclusion e + | _ -> None -let make_conclusion_flexible sigma = function +let make_anonymous_conclusion_flexible sigma = function | None -> sigma - | Some s -> + | Some (false, _) -> sigma + | Some (true, s) -> (match EConstr.ESorts.kind sigma s with | Type u -> (match Univ.universe_level u with @@ -136,17 +138,23 @@ let make_conclusion_flexible sigma = function | None -> sigma) | _ -> sigma) -let interp_ind_arity env sigma ind = +let intern_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + let pseudo_poly = check_type_conclusion c in + (constr_loc ind.ind_arity, c, impls, pseudo_poly) + +let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) = let sigma,t = understand_tcc env sigma ~expected_type:IsType c in - let pseudo_poly = check_anonymous_type c in match Reductionops.sort_of_arity env sigma t with | exception Invalid_argument _ -> - user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") + user_err ?loc (str "Not an arity") | s -> - let concl = if pseudo_poly then Some s else None in - sigma, (t, Retyping.relevance_of_sort s, concl, impls) + let concl = match pseudo_poly with + | Some b -> Some (b, s) + | None -> None + in + sigma, (t, Retyping.relevance_of_sort s, concl, impls) let interp_cstrs env sigma impls mldata arity ind = let cnames,ctyps = List.split ind.ind_lc in @@ -251,7 +259,7 @@ let solve_constraints_system levels level_bounds = done; v -let inductive_levels env evd poly arities inds = +let inductive_levels env evd arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> if Sorts.is_prop a || Sorts.is_sprop a then None @@ -286,7 +294,7 @@ let inductive_levels env evd poly arities inds = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative_sort env du then (* Any product is allowed here. *) - evd, arity :: arities + evd, (false, arity) :: arities else (* If in a predicative sort, or asked to infer the type, we take the max of: - indices (if in indices-matter mode) @@ -300,7 +308,6 @@ let inductive_levels env evd poly arities inds = raise (InductiveError LargeNonPropInductiveNotInType) else evd else evd - (* Evd.set_leq_sort env evd (Type cu) du *) in let evd = if len >= 2 && Univ.is_type0m_univ cu then @@ -311,14 +318,14 @@ let inductive_levels env evd poly arities inds = else evd in let duu = Sorts.univ_of_sort du in - let evd = + let template_prop, evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd Sorts.prop du - else evd - else Evd.set_eq_sort env evd (sort_of_univ cu) du + true, Evd.set_eq_sort env evd Sorts.prop du + else false, evd + else false, Evd.set_eq_sort env evd (sort_of_univ cu) du in - (evd, arity :: arities)) + (evd, (template_prop, arity) :: arities)) (evd,[]) (Array.to_list levels') destarities sizes in evd, List.rev arities @@ -328,6 +335,17 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg +let template_polymorphism_candidate env uctx params concl = + match uctx with + | Entries.Monomorphic_entry uctx -> + let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in + if not concltemplate then false + else + let template_check = Environ.check_template env in + let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in + let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in + not (template_check && Univ.LSet.is_empty conclunivs) + | Entries.Polymorphic_entry _ -> false let check_param = function | CLocalDef (na, _, _) -> check_named na @@ -345,25 +363,46 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - check_all_names_different indl; - List.iter check_param paramsl; - if not (List.is_empty uparamsl) && not (List.is_empty notations) - then user_err (str "Inductives with uniform parameters may not have attached notations."); - let sigma, udecl = interp_univ_decl_opt env0 udecl in +let interp_params env udecl uparamsl paramsl = + let sigma, udecl = interp_univ_decl_opt env udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = - interp_context_evars ~program_mode:false env0 sigma uparamsl in + interp_context_evars ~program_mode:false env sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl in - let indnames = List.map (fun ind -> ind.ind_name) indl in - (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> Name.get_id) assums in + sigma, env_params, (ctx_params, env_uparams, ctx_uparams, + List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl) + +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = + check_all_names_different indl; + List.iter check_param paramsl; + if not (List.is_empty uparamsl) && not (List.is_empty notations) + then user_err (str "Inductives with uniform parameters may not have attached notations."); + + let indnames = List.map (fun ind -> ind.ind_name) indl in + let sigma, env_params, infos = + interp_params env0 udecl uparamsl paramsl + in (* Interpret the arities *) - let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in + let arities = List.map (intern_ind_arity env_params sigma) indl in + + let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template = + let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in + if not poly && is_template then + (* In case of template polymorphism, we need to compute more constraints *) + let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in + let sigma, env_params, infos = + interp_params env0 udecl uparamsl paramsl + in + let arities = List.map (intern_ind_arity env_params sigma) indl in + sigma, env_params, infos, arities, is_template + else sigma, env_params, infos, arities, is_template + in + + let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in let arities, relevances, arityconcl, indimpls = List.split4 arities in let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in @@ -410,31 +449,36 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in - let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in - let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in + let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in + let sigma, arities = inductive_levels env_ar_params sigma arities constructors in let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in - let arities = List.map nf arities in + let arities = List.map (fun (template, arity) -> template, nf arity) arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in - let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in - let sigma = restrict_inductive_universes sigma ctx_params arities constructors in + let arityconcl = List.map (Option.map (fun (anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in + let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; + List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) - let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) -> + let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) -> + let template_candidate () = + templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in let template = match template with | Some template -> - if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); + if poly && template then user_err + Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); + if template && not (template_candidate ()) then + user_err Pp.(strbrk "Inductive " ++ Id.print ind.ind_name ++ + str" cannot be made template polymorphic."); template | None -> - should_auto_template ind.ind_name (not poly && - Option.cata (fun s -> not (Sorts.is_small s)) false concl) + should_auto_template ind.ind_name (template_candidate ()) in { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 285be8cd51..7587bd165f 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -62,3 +62,17 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) + +val template_polymorphism_candidate : + Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool +(** [template_polymorphism_candidate env uctx params conclsort] is + [true] iff an inductive with params [params] and conclusion + [conclsort] would be definable as template polymorphic. It should + have at least one universe in its monomorphic universe context that + can be made parametric in its conclusion sort, if one is given. + If the [Template Check] flag is false we just check that the conclusion sort + is not small. *) + +val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t +(** [sign_level env sigma ctx] computes the universe level of the context [ctx] + as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index e3cffa8523..8fd6bc7eab 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -530,7 +530,7 @@ let obligation_terminator entries uctx { name; num; auto } = declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - if defined then UState.make (Global.universes ()) + if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) else ctx in let prg = {prg with prg_ctx} in diff --git a/library/library.ml b/vernac/library.ml index 0faef7bf84..e91cb965f5 100644 --- a/library/library.ml +++ b/vernac/library.ml @@ -474,10 +474,10 @@ let require_library_from_dirpath ~lib_resolver modrefl export = if Lib.is_module_or_modtype () then begin warn_require_in_module (); - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - add_anonymous_leaf (in_import_library (modrefl,exp))) - export + add_anonymous_leaf (in_require (needed,modrefl,None)); + Option.iter (fun exp -> + add_anonymous_leaf (in_import_library (modrefl,exp))) + export end else add_anonymous_leaf (in_require (needed,modrefl,export)); @@ -547,7 +547,7 @@ let current_deps () = let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = - user_err + user_err (strbrk "Unable to use logical name " ++ DirPath.print dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") @@ -640,3 +640,12 @@ let get_used_load_paths () = StringSet.empty !libraries_loaded_list) let _ = Nativelib.get_load_paths := get_used_load_paths + +(* These commands may not be very safe due to ML-side plugin loading + etc... use at your own risk *) +let extern_state s = + System.extern_state Coq_config.state_magic_number s (States.freeze ~marshallable:true) + +let intern_state s = + States.unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + overwrite_library_filenames s diff --git a/library/library.mli b/vernac/library.mli index bb6c42e393..973b369226 100644 --- a/library/library.mli +++ b/vernac/library.mli @@ -75,3 +75,7 @@ val native_name_from_filename : string -> string (** {6 Opaque accessors} *) val indirect_accessor : Opaqueproof.indirect_accessor + +(** Low-level state overwriting, not very safe *) +val intern_state : string -> unit +val extern_state : string -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5d153fa8be..da14b6e979 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -454,7 +454,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } if not prg.prg_poly (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let ctx' = UState.merge_subst ctx (UState.subst ctx') in Univ.Instance.empty, ctx' else diff --git a/vernac/record.ml b/vernac/record.ml index 11237f3873..831fb53549 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -85,10 +85,10 @@ let interp_fields_evars env sigma impls_env nots l = let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> - let univ = + let univ = if is_local_assum d then let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in - Univ.sup (univ_of_sort s) univ + Univ.sup (univ_of_sort s) univ else univ in (EConstr.push_rel d env, univ)) l (env, Univ.Universe.sprop) @@ -101,8 +101,19 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl +let check_anonymous_type ind = + match ind with + | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true + | _ -> false + let typecheck_params_and_fields finite def poly pl ps records = let env0 = Global.env () in + (* Special case elaboration for template-polymorphic inductives, + lower bound on introduced universes is Prop so that we do not miss + any Set <= i constraint for universes that might actually be instantiated with Prop. *) + let is_template = + List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in + let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let () = let error bk {CAst.loc; v=name} = @@ -111,15 +122,15 @@ let typecheck_params_and_fields finite def poly pl ps records = user_err ?loc ~hdr:"record" (str "Record parameters must be named") | _ -> () in - List.iter + List.iter (function CLocalDef (b, _, _) -> error default_binder_kind b | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps - in + in let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in let fold (sigma, template) (_, t, _, _) = match t with - | Some t -> + | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = match t with @@ -138,7 +149,7 @@ let typecheck_params_and_fields finite def poly pl ps records = (sigma, false), (s, s') else (sigma, false), (s, s')) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) - | None -> + | None -> let uvarkind = Evd.univ_flexible_alg in let sigma, s = Evd.new_sort_variable uvarkind sigma in (sigma, template), (EConstr.mkSort s, s) @@ -168,23 +179,23 @@ let typecheck_params_and_fields finite def poly pl ps records = let _, univ = compute_constructor_level sigma env_ar newfs in let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in if not def && is_impredicative_sort env0 sort then - sigma, typ + sigma, (univ, typ) else let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in if Univ.is_small_univ univ && Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ) - else sigma, typ + Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ)) + else sigma, (univ, typ) in let (sigma, typs) = List.fold_left2_map fold sigma typs data in let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf -> let newps = List.map (RelDecl.map_constr_het nf) newps in - let map (impls, newfs) typ = + let map (impls, newfs) (univ, typ) = let newfs = List.map (RelDecl.map_constr_het nf) newfs in let typ = nf typ in - (typ, impls, newfs) + (univ, typ, impls, newfs) in let ans = List.map2 map data typs in newps, ans) @@ -295,7 +306,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let x = make_annot (Name binder_name) mip.mind_relevance in let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in - let primitive = + let primitive = match mib.mind_record with | PrimRecord _ -> true | FakeRecord | NotRecord -> false @@ -310,7 +321,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f | Anonymous -> (None::sp_projs,i,NoProjection fi::subst) | Name fid -> try - let kn, term = + let kn, term = if is_local_assum decl && primitive then let p = Projection.Repr.make indsp ~proj_npars:mib.mind_nparams @@ -345,12 +356,12 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - applist (mkConstU (kn,u),proj_args) + applist (mkConstU (kn,u),proj_args) in Declare.definition_message fid; kn, constr_fip with Type_errors.TypeError (ctx,te) -> - raise (NotDefinable (BadTypedProj (fid,ctx,te))) + raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = GlobRef.ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; @@ -404,29 +415,33 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let binder_name = match name with | None -> - let map (id, _, _, _, _, _, _) = + let map (id, _, _, _, _, _, _, _) = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in Array.map_of_list map record_data | Some n -> n in let ntypes = List.length record_data in - let mk_block i (id, idbuild, arity, _, fields, _, _) = + let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) = let nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let template = + let template_candidate () = + ComInductive.template_polymorphism_candidate (Global.env ()) univs params + (Some (Sorts.sort_of_univ min_univ)) + in match template with | Some template, _ -> (* templateness explicitly requested *) if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); + if template && not (template_candidate ()) then + user_err Pp.(strbrk "record cannot be made template polymorphic on any universe"); template | None, template -> (* auto detect template *) - ComInductive.should_auto_template id (template && not poly && - let _, s = Reduction.dest_arity (Global.env()) arity in - not (Sorts.is_small s)) + ComInductive.should_auto_template id (template && template_candidate ()) in { mind_entry_typename = id; mind_entry_arity = arity; @@ -437,7 +452,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let blocks = List.mapi mk_block record_data in let primitive = !primitive_flag && - List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data + List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data in let mie = { mind_entry_params = params; @@ -454,7 +469,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in - let map i (_, _, _, fieldimpls, fields, is_coe, coers) = + let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in @@ -469,7 +484,7 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cumulative ubinders univs id idbuild paramimpls params arity +let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -484,7 +499,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari let binder = {binder with binder_name=Name binder_name} in let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in - let class_entry = + let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant ~name:id (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) @@ -509,18 +524,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls); Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with - | Some b -> Some ((if b then Backward else Forward), List.hd priorities) - | None -> None + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None in [cref, [Name proj_name, sub, Some proj_cst]] | _ -> - let record_data = [id, idbuild, arity, fieldimpls, fields, false, + let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false, List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls params template ~kind:Decls.Method ~name:[|binder_name|] record_data in - let coers = List.map2 (fun coe pri -> - Option.map (fun b -> + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) coers priorities in @@ -575,7 +590,7 @@ let add_constant_class env sigma cst = let ctx, _ = decompose_prod_assum ty in let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in - let tc = + let tc = { cl_univs = univs; cl_impl = GlobRef.ConstRef cst; cl_context = (List.map (const None) ctx, ctx); @@ -679,24 +694,24 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records = let template = template, auto_template in match kind with | Class def -> - let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with | [r], [d] -> r, d | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") in let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in declare_class def cumulative ubinders univs id.CAst.v idbuild - implpars params arity template implfs fields coers priorities + implpars params univ arity template implfs fields coers priorities | _ -> let map impls = implpars @ [CAst.make None] @ impls in - let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in - let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = + let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in + let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> { pf_subclass = not (Option.is_empty rf_subclass); pf_canonical = rf_canonical }) cfs in - id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe + id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 20de6b4ff2..cd13f83e96 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -16,6 +16,7 @@ DeclareDef DeclareObl Canonical RecLemmas +Library Lemmas Class Auto_ind_decl diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4ae9d6d54f..3d14e8d510 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -606,6 +606,24 @@ let vernac_assumption ~atts discharge kind l nl = | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l +let set_template_check b = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_template = b } + +let is_template_check () = + let typing_flags = Environ.typing_flags (Global.env ()) in + typing_flags.Declarations.check_template + +let () = + let tccheck = + { optdepr = true; + optname = "Template universe check"; + optkey = ["Template"; "Check"]; + optread = (fun () -> is_template_check ()); + optwrite = (fun b -> set_template_check b)} + in + declare_bool_option tccheck + let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false ~name:"Polymorphic inductive cumulativity" @@ -1161,11 +1179,11 @@ let vernac_chdir = function let vernac_write_state file = let file = CUnix.make_suffix file ".coq" in - States.extern_state file + Library.extern_state file let vernac_restore_state file = let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in - States.intern_state file + Library.intern_state file (************) (* Commands *) @@ -1954,9 +1972,9 @@ let vernac_print ~pstate ~atts = function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ env sigma - | PrintSectionContext qid -> print_sec_context_typ env sigma qid - | PrintInspect n -> inspect env sigma n + | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma + | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid + | PrintInspect n -> inspect Library.indirect_accessor env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir @@ -1969,7 +1987,7 @@ let vernac_print ~pstate ~atts = | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name env sigma qid udecl + print_name Library.indirect_accessor env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() @@ -2267,7 +2285,7 @@ let with_fail ~st f = user_err ~hdr:"Fail" (str "The command has not failed!") | Ok msg -> if not !Flags.quiet || !test_mode - then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) + then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg) let locate_if_not_already ?loc (e, info) = match Loc.get_loc info with @@ -2538,7 +2556,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> - VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) + VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> VtDefault(fun () -> with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) |