diff options
175 files changed, 1529 insertions, 914 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2a325f2d71..698452cb2b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -1,10 +1,17 @@ # This file describes the maintainers for the main components. See # `dev/doc/MERGING.md`. -########## GitHub metadata, including this file ########## +########## Contributing process ########## -/.github/ @maximedenes -# Secondary maintainer @Zimmi48 +/.github/ @coq/contributing-process-maintainers + +/CONTRIBUTING.md @coq/contributing-process-maintainers + +/dev/doc/release-process.md @coq/contributing-process-maintainers + +/dev/doc/MERGING.md @coq/pushers +# This ensures that all members of the @coq/pushers +# team are notified when the merging doc changes. ########## Build system ########## @@ -45,19 +52,12 @@ azure-pipelines.yml @coq/ci-maintainers /INSTALL* @Zimmi48 # Secondary maintainer @maximedenes -/CONTRIBUTING.md @Zimmi48 -# Secondary maintainer @maximedenes - /CODE_OF_CONDUCT.md @Zimmi48 # Secondary maintainer @mattam82 /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes -/dev/doc/MERGING.md @coq/pushers -# This ensures that all members of the @coq/pushers -# team are notified when the merging doc changes. - /dev/doc/changes.md @ghost # Trick to avoid getting review requests # each time someone modifies the dev changelog 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/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh new file mode 100644 index 0000000000..21ff60493b --- /dev/null +++ b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then + + coqhammer_CI_REF=errors+private + coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + +fi diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh new file mode 100644 index 0000000000..6dc44aa627 --- /dev/null +++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then + + equations_CI_REF=proofs+declare_unif + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi 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/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..f68b2aaaa2 --- /dev/null +++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst @@ -0,0 +1,4 @@ +- New lemmas on :g:`combine`, :g:`filter`, and :g:`nodup` functions on lists. The lemma + :g:`filter_app` was moved to the :g:`List` module. + + See `#10651 <https://github.com/coq/coq/pull/10651>`_, 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/engine/evarutil.ml b/engine/evarutil.ml index ea71be8e43..c946125d3f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' = in Evd.add_universe_constraints evd soft -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extension of those in [sigma1]. *) -let eq_constr_univs_test sigma1 sigma2 t u = +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +let eq_constr_univs_test ~evd ~extended_evd t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in let t = EConstr.Unsafe.to_constr t @@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u = in let ans = UnivProblem.eq_constr_univs_infer_with - (fun t -> kind_of_term_upto sigma1 t) - (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) fold t u sigma2 + (fun t -> kind_of_term_upto evd t) + (fun u -> kind_of_term_upto extended_evd u) + (universes extended_evd) fold t u extended_evd in match ans with None -> false | Some _ -> true diff --git a/engine/evarutil.mli b/engine/evarutil.mli index e9d579af32..7877b94582 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map -> val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extension of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +val eq_constr_univs_test : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + constr -> + constr -> + bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe 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 bada18feff..3c383b2e00 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system @@ -38,7 +38,6 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e | _ -> raise CErrors.Unhandled @@ -99,7 +98,7 @@ struct let print_char = fun c -> (); fun () -> print_char c let timeout = fun n t -> (); fun () -> - Control.timeout n t () (Exception Timeout) + Control.timeout n t () (Exception Tac_Timeout) let make f = (); fun () -> try f () diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 90c920439a..75920455ce 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system diff --git a/engine/proofview.ml b/engine/proofview.ml index 8b5bd4cd80..1f076470c1 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -849,7 +849,8 @@ let give_up = module Progress = struct - let eq_constr = Evarutil.eq_constr_univs_test + let eq_constr evd extended_evd = + Evarutil.eq_constr_univs_test ~evd ~extended_evd (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = @@ -879,10 +880,10 @@ module Progress = struct eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body (** Equality function on goals *) - let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - eq_evar_info evars1 evars2 evi1 evi2 + let goal_equal ~evd ~extended_evd evar extended_evar = + let evi = Evd.find evd evar in + let extended_evi = Evd.find extended_evd extended_evar in + eq_evar_info evd extended_evd evi extended_evi end @@ -899,17 +900,17 @@ let tclPROGRESS t = let test = quick_test || Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f) + Progress.goal_equal ~evd:initial.solution + ~extended_evd:final.solution (drop_state i) (drop_state f) end initial.comb final.comb in if not test then tclUNIT res else - tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) -exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> raise CErrors.Unhandled end @@ -934,7 +935,8 @@ let tclTIMEOUT n t = end begin let open Logic_monad.NonLogical in function (e, info) -> match e with - | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) + | Logic_monad.Tac_Timeout -> + return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) | e -> Logic_monad.NonLogical.raise ~info e diff --git a/engine/proofview.mli b/engine/proofview.mli index f90f02f3e1..764a4a0058 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -398,14 +398,23 @@ val give_up : unit tactic val tclPROGRESS : 'a tactic -> 'a tactic module Progress : sig - val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool +(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether + the [evar_info] from [evd] corresponding to [evar] is equal to that + from [extended_evd] corresponding to [extended_evar], up to + existential variable instantiation and equalisable universes. The + universe constraints in [extended_evd] are assumed to be an + extension of the universe constraints in [evd]. *) + val goal_equal : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + Evar.t -> + Evar.t -> + bool end (** Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic -exception Timeout - (** [tclTIMEOUT n t] can have only one success. In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic 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/gramlib/grammar.ml b/gramlib/grammar.ml index f86cb0f6f2..ff0b90dcff 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -10,6 +10,9 @@ open Util module type GLexerType = Plexing.Lexer +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -27,8 +30,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules @@ -92,9 +93,6 @@ let tokens con = egram.gtokens; !list -type ty_norec = TyNoRec -type ty_mayrec = TyMayRec - type ('a, 'b, 'c) ty_and_rec = | NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec | MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 658baf1de9..9e48460206 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -19,6 +19,9 @@ module type GLexerType = Plexing.Lexer (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -36,8 +39,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules 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/dumpglob.ml b/interp/dumpglob.ml index 8d6a266c30..41d1da9694 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -20,31 +20,21 @@ let open_glob_file f = let close_glob_file () = close_out !glob_file -type glob_output_t = - | NoGlob - | StdOut - | MultFiles - | Feedback - | File of string +type glob_output = + | NoGlob + | Feedback + | MultFiles + | File of string let glob_output = ref NoGlob -let dump () = !glob_output != NoGlob +let dump () = !glob_output <> NoGlob -let noglob () = glob_output := NoGlob - -let dump_to_dotglob () = glob_output := MultFiles - -let dump_into_file f = - if String.equal f "stdout" then - (glob_output := StdOut; glob_file := stdout) - else - (glob_output := File f; open_glob_file f) - -let feedback_glob () = glob_output := Feedback +let set_glob_output mode = + glob_output := mode let dump_string s = - if dump () && !glob_output != Feedback then + if dump () && !glob_output != Feedback then output_string !glob_file s let start_dump_glob ~vfile ~vofile = @@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | Feedback | StdOut -> + | NoGlob | Feedback -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | Feedback | StdOut -> () + | NoGlob | Feedback -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 60d62a1cb2..2b6a116a01 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -8,19 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val open_glob_file : string -> unit -val close_glob_file : unit -> unit - val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool -val noglob : unit -> unit -val dump_into_file : string -> unit (** special handling of "stdout" *) +type glob_output = + | NoGlob + | Feedback + | MultFiles (* one glob file per .v file *) + | File of string (* Single file for all coqc arguments *) -val dump_to_dotglob : unit -> unit -val feedback_glob : unit -> unit +(* Default "NoGlob" *) +val set_glob_output : glob_output -> unit val pause : unit -> unit val continue : unit -> unit 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/aux_file.mli b/lib/aux_file.mli index 60c8fb4449..b241fdc6cc 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t val aux_file_name_for : string -> string val start_aux_file : aux_file:string -> v_file:string -> unit -val stop_aux_file : unit -> unit +val stop_aux_file : unit -> unit val recording : unit -> bool val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 190de5853d..f09dc48f5d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let record_aux_file = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 1c96796220..185a5f8425 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,10 +31,6 @@ (** Command-line flags *) -(** Set by coqtop to tell the kernel to output to the aux file; will - be eventually removed by cleanups such as PR#1103 *) -val record_aux_file : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool 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/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/extend.ml b/parsing/extend.ml index 63e121c0d1..ed6ebe5aed 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -79,8 +79,10 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) -type norec = NoRec (* just two *) -type mayrec = MayRec (* incompatible types *) +(* Should be merged with gramlib's implementation *) + +type norec = Gramlib.Grammar.ty_norec +type mayrec = Gramlib.Grammar.ty_mayrec type ('self, 'trec, 'a) symbol = | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol @@ -107,15 +109,3 @@ and 'a rules = type 'a production_rule = | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statement = - string option * - (* Level *) - Gramlib.Gramext.g_assoc option * - (* Associativity *) - 'a production_rule list - (* Symbol list with the interpretation function *) - -type 'a extend_statement = - Gramlib.Gramext.position option * - 'a single_extend_statement list diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 3aaba27579..e0d63a723e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -131,73 +131,57 @@ end (** Binding general entry keys to symbol *) -type ('s, 'trec, 'a, 'r) casted_rule = -| CastedRNo : ('s, G.ty_norec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, norec, 'a, 'r) casted_rule -| CastedRMay : ('s, G.ty_mayrec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, mayrec, 'a, 'r) casted_rule - -type ('s, 'trec, 'a) casted_symbol = -| CastedSNo : ('s, G.ty_norec, 'a) G.ty_symbol -> ('s, norec, 'a) casted_symbol -| CastedSMay : ('s, G.ty_mayrec, 'a) G.ty_symbol -> ('s, mayrec, 'a) casted_symbol - -let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) casted_symbol = +let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.ty_symbol = function -| Atoken t -> CastedSNo (G.s_token t) +| Atoken t -> G.s_token t | Alist1 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1 s) - | CastedSMay s -> CastedSMay (G.s_list1 s) end + let s = symbol_of_prod_entry_key s in + G.s_list1 s | Alist1sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list1sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list1sep s sep false | Alist0 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0 s) - | CastedSMay s -> CastedSMay (G.s_list0 s) end + let s = symbol_of_prod_entry_key s in + G.s_list0 s | Alist0sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list0sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list0sep s sep false | Aopt s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_opt s) - | CastedSMay s -> CastedSMay (G.s_opt s) end -| Aself -> CastedSMay G.s_self -| Anext -> CastedSMay G.s_next -| Aentry e -> CastedSNo (G.s_nterm e) -| Aentryl (e, n) -> CastedSNo (G.s_nterml e n) + let s = symbol_of_prod_entry_key s in + G.s_opt s +| Aself -> G.s_self +| Anext -> G.s_next +| Aentry e -> G.s_nterm e +| Aentryl (e, n) -> G.s_nterml e n | Arules rs -> let warning msg = Feedback.msg_warning Pp.(str msg) in - CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)) + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) -and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) casted_rule = function -| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc) +and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.ty_rule = function +| Stop -> + G.r_stop | Next (r, s) -> - begin match symbol_of_rule r, symbol_of_prod_entry_key s with - | CastedRNo (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRNo (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) end + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next r s | NextNoRec (r, s) -> - let CastedRNo (r, cast) = symbol_of_rule r in - let CastedSNo s = symbol_of_prod_entry_key s in - CastedRNo (G.r_next_norec r s, (fun act x -> cast (act x))) + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next_norec r s and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function | Rules (r, act) -> - let CastedRNo (symb, cast) = symbol_of_rule r in - G.rules (symb, cast act) + let symb = symbol_of_rule r in + G.rules (symb,act) (** FIXME: This is a hack around a deficient camlp5 API *) type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> - match symbol_of_rule toks with - | CastedRNo (symb, cast) -> AnyProduction (symb, cast act) - | CastedRMay (symb, cast) -> AnyProduction (symb, cast act) + AnyProduction (symbol_of_rule toks, act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, assoc, List.map of_coq_production_rule rule) @@ -215,6 +199,18 @@ let fix_extend_statement (pos, st) = (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + type extend_rule = | ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule @@ -462,11 +458,10 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end + let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = - let r = - match symbol_of_prod_entry_key e with - | CastedSNo s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) - | CastedSMay s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in + let s = symbol_of_prod_entry_key e in + let r = G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7efeab6ba0..10f78a5a72 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -212,8 +212,19 @@ val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self optio type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) -val grammar_extend : 'a Entry.t -> gram_reinit option -> - 'a Extend.extend_statement -> unit +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + +val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2d5872718f..c57daf0047 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 diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 60717c6eec..570b72136c 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = +let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in (* let time1 = System.get_time () in *) @@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> - name, entry, hook + entry, hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -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 @@ -282,7 +299,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort Sorts.InProp; register_with_sort Sorts.InSet in - let id,entry,hook = + let entry, hook = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -1170,7 +1187,7 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in @@ -1219,9 +1236,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef s::l_schemes -> s,l_schemes | _ -> CErrors.anomaly (Pp.str "") in - let _,const,_ = + let opaque = + let finfos = + match find_Function_infos (fst first_fun) with + | None -> raise Not_found + | Some finfos -> finfos + in + let open Proof_global in + match finfos.equation_lemma with + | None -> Transparent (* non recursive definition *) + | Some equation -> + if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent + in + let entry, _hook = try - build_functional_principle evd false + build_functional_principle ~opaque evd false first_type (Array.of_list sorts) this_block_funs @@ -1233,30 +1262,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in incr i; - let opacity = - let finfos = - match find_Function_infos (fst first_fun) with - | None -> raise Not_found - | Some finfos -> finfos - in - match finfos.equation_lemma with - | None -> false (* non recursive definition *) - | Some equation -> - Declareops.is_opaque (Global.lookup_constant equation) - in - let const = {const with Proof_global.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types - then - [const] + then [entry] else let other_fun_princ_types = let funs = Array.map Constr.mkConstU this_block_funs in let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let open Proof_global in - let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in + let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1283,7 +1298,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let _,const,_ = + let entry, _hook = build_functional_principle evd false @@ -1294,20 +1309,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) (fun _ _ -> ()) in - const + entry with Found_type i -> let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt in - {const with - proof_entry_body = - (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - proof_entry_type = Some scheme_type - } + Declare.definition_entry ~types:scheme_type princ_body ) other_fun_princ_types in - const::other_result + entry::other_result (* [derive_correctness funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] @@ -1358,7 +1369,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) + (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))), + EConstr.of_constr (Option.get entry.Declare.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ddd6ecfb5c..7c17ecdba0 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1252,7 +1252,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError(Some "compute_cst_params", str "Not handled case")) + CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case") ) gt and compute_cst_params_from_app acc (params,rtl) = let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index fbf63c69dd..8abccabae6 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,4 +1,13 @@ -open Pp +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Constr open Glob_term open CErrors @@ -433,7 +442,8 @@ let replace_var_by_term x_id term = replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | GRec _ -> raise (UserError(None,str "Not handled GRec")) + | GRec _ -> + CErrors.user_err (Pp.str "Not handled GRec") | GSort _ | GHole _ as rt -> rt | GInt _ as rt -> rt diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 24b3690138..70211a1860 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Names open Glob_term diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2937ae5d14..a205c0744a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -95,7 +95,8 @@ let functional_induction with_clean c princl pat = (* We need to refresh gl due to the updated evar_map in princ *) Proofview.Goal.enter_one (fun gl -> Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args)) - | _ -> raise (UserError(None,str "functional induction must be used with a function" )) + | _ -> + CErrors.user_err (str "functional induction must be used with a function" ) end | Some ((princ,binding)) -> Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7719705138..80fc64fe65 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -40,7 +40,9 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (CErrors.UserError(None, msg)) + with + | Not_found -> + CErrors.user_err msg let filter_map filter f = @@ -64,8 +66,7 @@ let chop_rlambda_n = | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> - raise (CErrors.UserError(Some "chop_rlambda_n", - str "chop_rlambda_n: Not enough Lambdas")) + CErrors.user_err ~hdr:"chop_rlambda_n" (str "chop_rlambda_n: Not enough Lambdas") in chop_lambda_n [] @@ -76,7 +77,8 @@ let chop_rprod_n = else match DAst.get rt with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> + CErrors.user_err ~hdr:"chop_rprod_n" (str "chop_rprod_n: Not enough products") in chop_prod_n [] @@ -105,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.Proof_global.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 16beaaa3c7..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 Proof_global.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/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..2e97dfea19 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 = 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..b456d2eed2 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -151,7 +151,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 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/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/proofs/goal.ml b/proofs/goal.ml index 888c4785df..f95a904a5f 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -91,7 +91,8 @@ module V82 = struct let weak_progress glss gls = match glss.Evd.it with - | [ g ] -> not (Proofview.Progress.goal_equal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) + | [ g ] -> not (Proofview.Progress.goal_equal ~evd:gls.Evd.sigma + ~extended_evd:glss.Evd.sigma gls.Evd.it g) | _ -> true let progress glss gls = diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 0ce726db25..756fef0511 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,9 +6,7 @@ Proof Logic Goal_select Proof_bullet -Proof_global Refiner Tacmach -Pfedit Clenv Clenvtac diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index fab6767beb..baa7b3570c 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -11,7 +11,6 @@ open Util let check_vio (ts,f_in) = - Dumpglob.noglob (); let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -142,5 +141,3 @@ let schedule_vio_compilation j fs = List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 09d7e0278a..edeb27ab88 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -69,7 +69,7 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Proof_global in + let open Declare in let typ = match const.proof_entry_type with | None -> assert false | Some t -> t @@ -151,7 +151,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in + let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) @@ -160,20 +160,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd in let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Proof_global.proof_entry_universes with + let inst = match const.Declare.proof_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in + let (_, body_uctx), _ = Future.force const.Declare.proof_entry_body in let () = assert (Univ.ContextSet.is_empty body_uctx) in EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let effs = Evd.concat_side_effects eff - Proof_global.(snd (Future.force const.proof_entry_body)) in + (snd (Future.force const.Declare.proof_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/abstract.mli b/tactics/abstract.mli index e278729f89..96ddbea7b2 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P save path *) val shrink_entry : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Proof_global.proof_entry - -> 'c Proof_global.proof_entry * Constr.t list + -> 'c Declare.proof_entry + -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index c280760e84..3a02e5451a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -55,8 +55,20 @@ type constant_obj = { cst_locl : import_status; } +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -174,7 +186,6 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - let open Proof_global in { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); proof_entry_secctx = None; proof_entry_type = types; @@ -184,7 +195,6 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_inline_code = inline} let cast_proof_entry e = - let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in let univs = if Univ.ContextSet.is_empty ctx then e.proof_entry_universes @@ -205,7 +215,6 @@ let cast_proof_entry e = } let cast_opaque_proof_entry e = - let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -224,7 +233,7 @@ let cast_opaque_proof_entry e = let vars = global_vars_set env pf in ids_typ, vars in - let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in + let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in keep_hyps env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in @@ -249,7 +258,6 @@ let is_unsafe_typing_flags () = not (flags.check_universes && flags.check_guarded && flags.check_positive) let define_constant ~side_effect ~name cd = - let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with @@ -299,7 +307,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find @@ -321,7 +329,6 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let open Proof_global in let (body, eff) = Future.force de.proof_entry_body in let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in let eff = get_roles export eff in diff --git a/tactics/declare.mli b/tactics/declare.mli index 4ae9f6c7ae..4cb876cecb 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -19,14 +19,27 @@ open Entries reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) +(** Proof entries *) +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + (** Declaration of local constructions (Variable/Hypothesis/Local) *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -43,7 +56,7 @@ val declare_variable val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified diff --git a/tactics/equality.ml b/tactics/equality.ml index 220b9bc475..1f125a3c59 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -255,7 +255,9 @@ let tclNOTSAMEGOAL tac = Proofview.Goal.goals >>= fun gls -> let check accu gl' = gl' >>= fun gl' -> - let accu = accu || Proofview.Progress.goal_equal sigma ev (project gl') (goal gl') in + let accu = accu || Proofview.Progress.goal_equal + ~evd:sigma ~extended_evd:(project gl') ev (goal gl') + in Proofview.tclUNIT accu in Proofview.Monad.List.fold_left check false gls >>= fun has_same -> diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e2ef05461b..54393dce00 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -124,17 +124,7 @@ let define internal role id c poly univs = let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = { - Proof_global.proof_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), - Evd.empty_side_effects); - proof_entry_secctx = None; - proof_entry_type = None; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - } in + let entry = Declare.definition_entry ~univs c in let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in let () = match internal with | InternalTacticRequest -> () diff --git a/proofs/pfedit.ml b/tactics/pfedit.ml index 99a254652c..5be7b4fa28 100644 --- a/proofs/pfedit.ml +++ b/tactics/pfedit.ml @@ -124,7 +124,7 @@ let build_constant_by_tactic ~name ctx sign ~poly typ tac = let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> - let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in + let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in entry, status, univs | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") @@ -136,7 +136,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Proof_global.proof_entry_body in + let body, eff = Future.force ce.Declare.proof_entry_body in let (cb, ctx) = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) else body diff --git a/proofs/pfedit.mli b/tactics/pfedit.mli index 0626e40047..30514191fa 100644 --- a/proofs/pfedit.mli +++ b/tactics/pfedit.mli @@ -64,7 +64,7 @@ val build_constant_by_tactic -> poly:bool -> EConstr.types -> unit Proofview.tactic - -> Evd.side_effects Proof_global.proof_entry * bool * UState.t + -> Evd.side_effects Declare.proof_entry * bool * UState.t val build_by_tactic : ?side_eff:bool diff --git a/proofs/proof_global.ml b/tactics/proof_global.ml index 851a3d1135..a2929e45cd 100644 --- a/proofs/proof_global.ml +++ b/tactics/proof_global.ml @@ -24,21 +24,9 @@ module NamedDecl = Context.Named.Declaration (*** Proof Global Environment ***) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - type proof_object = { name : Names.Id.t - ; entries : Evd.side_effects proof_entry list + ; entries : Evd.side_effects Declare.proof_entry list ; poly : bool ; universes: UState.t ; udecl : UState.universe_decl @@ -223,7 +211,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let ctx = UState.restrict universes used_univs in let univs = UState.check_univ_decl ~poly ctx udecl in (univs, typ), ((body, Univ.ContextSet.empty), eff) - in + in fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> @@ -250,6 +238,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in + let open Declare in { proof_entry_body = body; proof_entry_secctx = section_vars; diff --git a/proofs/proof_global.mli b/tactics/proof_global.mli index 54d5c2087a..d15e23c2cc 100644 --- a/proofs/proof_global.mli +++ b/tactics/proof_global.mli @@ -27,29 +27,11 @@ val get_initial_euctx : t -> UState.t val compact_the_proof : t -> t -(** When a proof is closed, it is reified into a [proof_object], where - [id] is the name of the proof, [entries] the list of the proof terms - (in a form suitable for definitions). Together with the [terminator] - function which takes a [proof_object] together with a [proof_end] - (i.e. an proof ending command) and registers the appropriate - values. *) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - (** When a proof is closed, it is reified into a [proof_object] *) type proof_object = { name : Names.Id.t (** name of the proof *) - ; entries : Evd.side_effects proof_entry list + ; entries : Evd.side_effects Declare.proof_entry list (** list of the proof terms (in a form suitable for definitions). *) ; poly : bool (** polymorphic status *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2d0806b2e0..b93c4a176f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -546,7 +546,8 @@ module New = struct Proofview.tclOR (Proofview.tclTIMEOUT n t) begin function (e, info) -> match e with - | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) + | Logic_monad.Tac_Timeout as e -> + Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) | e -> Proofview.tclZERO ~info e end diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 6dd749aa0d..c5c7969a09 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,6 @@ Declare +Proof_global +Pfedit Dnet Dn Btermdn 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/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/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/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v new file mode 100644 index 0000000000..30e6d57a7a --- /dev/null +++ b/test-suite/ssr/bang_rewrite.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. + +Require Import ssreflect. + +Axiom mult@{i} : nat -> nat -> nat. +Notation "m * n" := (mult m n). + +Axiom multA : forall a b c, (a * b) * c = a * (b * c). + +(* Previously the following gave a universe error: *) + +Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)). +Proof. by rewrite !multA. Qed. 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/Bool/Bool.v b/theories/Bool/Bool.v index 0c0a1897a8..296c253363 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -822,4 +822,4 @@ Defined. Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b'). Proof. destruct b, b'; now constructor. -Qed. +Defined. 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 1639115cbd..3e0bf1d8ae 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -387,8 +387,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..f45317ba50 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1227,6 +1227,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)) (f : A -> bool), + concat (map filter l) = filter (concat l). + Proof. + induction l as [| v l IHl]; [auto|]. + simpl. rewrite (IHl f). rewrite filter_app. reflexivity. + Qed. + (** [find] *) Fixpoint find (l:list A) : option A := @@ -1309,6 +1323,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 +1908,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 +2072,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 d8a3dbb4bb..fe5361c156 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -108,8 +108,6 @@ let compile opts copts ~echo ~f_in ~f_out = in match copts.compilation_mode with | BuildVo -> - Flags.record_aux_file := true; - let long_f_dot_v, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".v" ".vo" in @@ -124,8 +122,11 @@ let compile opts copts ~echo ~f_in ~f_out = Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); + + Dumpglob.set_glob_output copts.glob_out; Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); + let wall_clock1 = Unix.gettimeofday () in let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in @@ -139,9 +140,6 @@ let compile opts copts ~echo ~f_in ~f_out = Dumpglob.end_dump_glob () | BuildVio -> - Flags.record_aux_file := false; - Dumpglob.noglob (); - let long_f_dot_v, long_f_dot_vio = ensure_exists_with_prefix f_in f_out ".v" ".vio" in @@ -174,9 +172,6 @@ let compile opts copts ~echo ~f_in ~f_out = Stm.reset_task_queue () | Vio2Vo -> - - Flags.record_aux_file := false; - Dumpglob.noglob (); let long_f_dot_vio, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".vio" ".vo" in let sum, lib, univs, tasks, proofs = diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 67d70416c8..0490c35970 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] @@ -59,7 +63,6 @@ type coqargs_config = { debug : bool; diffs_set : bool; time : bool; - glob_opt : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; } @@ -125,7 +128,6 @@ let default_config = { debug = false; diffs_set = false; time = false; - glob_opt = false; print_emacs = false; set_options = []; @@ -380,13 +382,6 @@ let parse_args ~help ~init arglist : t * string list = Flags.compat_version := v; add_compat_require oval v - |"-dump-glob" -> - Dumpglob.dump_into_file (next ()); - { oval with config = { oval.config with glob_opt = true }} - - |"-feedback-glob" -> - Dumpglob.feedback_glob (); oval - |"-exclude-dir" -> System.exclude_directory (next ()); oval @@ -524,7 +519,6 @@ let parse_args ~help ~init arglist : t * string list = |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = true }} |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} @@ -535,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) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index e414888861..26f22386a0 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -35,7 +35,6 @@ type coqargs_config = { debug : bool; diffs_set : bool; time : bool; - glob_opt : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; } diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 5678acb2b1..7658ad68a5 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -11,13 +11,12 @@ 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; System.trust_file_cache := true; - Coqtop.init_color opts.Coqargs.config; - if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob () + Coqtop.init_color opts.Coqargs.config let coqc_specific_usage = Usage.{ executable_name = "coqc"; @@ -54,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 5cced2baac..0b5481fe72 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -23,7 +23,8 @@ type t = ; echo : bool - ; outputstate : string option; + ; outputstate : string option + ; glob_out : Dumpglob.glob_output } let default = @@ -40,6 +41,7 @@ let default = ; echo = false ; outputstate = None + ; glob_out = Dumpglob.MultFiles } let depr opt = @@ -187,6 +189,15 @@ let parse arglist : t = | "-outputstate" -> set_outputstate oval (next ()) + (* Glob options *) + |"-no-glob" | "-noglob" -> + { oval with glob_out = Dumpglob.NoGlob } + + |"-dump-glob" -> + let file = next () in + { oval with glob_out = Dumpglob.File file } + + (* Rest *) | s -> extras := s :: !extras; oval diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index b02eeeb9ee..13bea3bf3e 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -24,6 +24,7 @@ type t = ; echo : bool ; outputstate : string option + ; glob_out : Dumpglob.glob_output } val default : t diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 78640334e2..07466d641e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -438,19 +438,15 @@ let rec loop ~state = loop ~state (* Default toplevel loop *) -let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) let drop_args = ref None + let loop ~opts ~state = drop_args := Some opts; let open Coqargs in print_emacs := opts.config.print_emacs; (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder coqloop_feed in - if Dumpglob.dump () then begin - Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; - Dumpglob.noglob () - end; let _ = loop ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b574179a93..eded9f4bcd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -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/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/comDefinition.ml b/vernac/comDefinition.ml index 57de719cb4..9745358ba2 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.Proof_global.proof_entry_type with + let typ = match ce.Declare.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index db0c102e14..01505d0733 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -41,5 +41,5 @@ val interp_definition -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects Proof_global.proof_entry * + -> Evd.side_effects Declare.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits 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/declareDef.ml b/vernac/declareDef.ml index 5e4f2dcd34..1926faaf0e 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in + let fix_exn = Future.fix_exn_of ce.proof_entry_body in let gr = match scope with | Discharge -> let () = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 606cfade46..54a0c9a7e8 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -45,7 +45,7 @@ val declare_definition -> kind:Decls.definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits -> GlobRef.t @@ -66,7 +66,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Proof_global.proof_entry + Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c5cbb095ca..8fd6bc7eab 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body ty else ([], body, ty, [||]) in - let body = - ((body, Univ.ContextSet.empty), Evd.empty_side_effects) - in - let ce = - Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body - ; proof_entry_secctx = None - ; proof_entry_type = ty - ; proof_entry_universes = uctx - ; proof_entry_opaque = opaque - ; proof_entry_inline_code = false - ; proof_entry_feedback = None } - in + let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in + (* ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant ~name:obl.obl_name @@ -495,12 +485,11 @@ type obligation_qed_info = } let obligation_terminator entries uctx { name; num; auto } = - let open Proof_global in match entries with | [entry] -> let env = Global.env () in - let ty = entry.proof_entry_type in - let body, eff = Future.force entry.proof_entry_body in + let ty = entry.Declare.proof_entry_type in + let body, eff = Future.force entry.Declare.proof_entry_body in let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in @@ -514,7 +503,7 @@ let obligation_terminator entries uctx { name; num; auto } = let obls, rem = prg.prg_obligations in let obl = obls.(num) in let status = - match obl.obl_status, entry.proof_entry_opaque with + match obl.obl_status, entry.Declare.proof_entry_opaque with | (_, Evar_kinds.Expand), true -> err_not_transp () | (true, _), true -> err_not_transp () | (false, _), true -> Evar_kinds.Define true @@ -541,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/vernac/declareObl.mli b/vernac/declareObl.mli index 2a8fa734b3..7d8a112cc6 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -76,7 +76,7 @@ type obligation_qed_info = } val obligation_terminator - : Evd.side_effects Proof_global.proof_entry list + : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit (** [obligation_terminator] part 2 of saving an obligation *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index cf87646905..a6c577a878 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -98,20 +98,11 @@ let () = (* Util *) -let define ~poly name sigma c t = +let define ~poly name sigma c types = let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in - let open Proof_global in - let kn = f ~name - (DefinitionEntry - { proof_entry_body = c; - proof_entry_secctx = None; - proof_entry_type = t; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - }) in + let entry = Declare.definition_entry ~univs ?types c in + let kn = f ~name (DefinitionEntry entry) in definition_message name; kn @@ -412,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in - let cst = define ~poly fi sigma proof_output (Some decltype) in + let cst = define ~poly fi sigma decl (Some decltype) in GlobRef.ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -534,7 +524,6 @@ let do_combined_scheme name schemes = schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in (* It is possible for the constants to have different universe polymorphism from each other, however that is only when the user manually defined at least one of them (as Scheme would pick the @@ -542,7 +531,7 @@ let do_combined_scheme name schemes = some other polymorphism they can also manually define the combined scheme. *) let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in - ignore (define ~poly name.v sigma proof_output (Some typ)); + ignore (define ~poly name.v sigma body (Some typ)); fixpoint_message None [name.v] (**********************************************************************) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7809425a10..42d1a1f3fc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - let open Proof_global in { const with - proof_entry_body = - Future.chain const.proof_entry_body + Declare.proof_entry_body = + Future.chain const.Declare.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.proof_entry_body in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in - let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in + let should_suggest = const.Declare.proof_entry_opaque && + Option.is_empty const.Declare.proof_entry_secctx in let open DeclareDef in let r = match scope with | Discharge -> @@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Proof_global.proof_entry_opaque = false } in + let f_def = { f_def with Declare.proof_entry_opaque = false } in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~entries = let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = - match Proof_global.(lemma_def.proof_entry_type) with + match lemma_def.Declare.proof_entry_type with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = let open Proof_global in + let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = { lemma_def with - proof_entry_body = lemma_body; + Declare.proof_entry_body = lemma_body; proof_entry_type = Some lemma_type } in let lemma_def = Declare.DefinitionEntry lemma_def in @@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info = let { Info.hook; scope; impargs; other_thms } = info in if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true 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 37fe0df0ee..da14b6e979 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Proof_global.proof_entry_body in + let (body, eff) = Future.force entry.Declare.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in @@ -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/proof_using.ml b/vernac/proof_using.ml index 094e2c1184..cfb3248c7b 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -130,7 +130,7 @@ let suggest_common env ppid used ids_typ skip = str "should start with one of the following commands:"++spc()++ v 0 ( prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); - if !Flags.record_aux_file + if Aux_file.recording () then let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in record_proof_using s diff --git a/vernac/record.ml b/vernac/record.ml index 86745212e7..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 @@ -340,26 +351,17 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let open Proof_global in - let entry = { - proof_entry_body = - Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); - proof_entry_secctx = None; - proof_entry_type = Some projtyp; - proof_entry_universes = ctx; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None } in + let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in let kind = Decls.IsDefinition kind in 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; @@ -413,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; @@ -446,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; @@ -463,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 @@ -478,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. *) @@ -493,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) @@ -518,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 @@ -584,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); @@ -688,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 e2bfbf626a..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() @@ -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)) |