diff options
84 files changed, 1355 insertions, 1032 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5e6c380f4b..cf1dc47fab 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-03-19-V93" + CACHEKEY: "bionic_coq-V2020-03-19-V29" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -69,6 +69,7 @@ before_script: - _install_ci - config/Makefile - config/coq_config.py + - config/coq_config.ml - test-suite/misc/universes/all_stdlib.v expire_in: 1 week script: @@ -172,7 +173,7 @@ before_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all + - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -425,7 +426,16 @@ doc:refman:dune: artifacts: paths: - _build/log - - _build/default/doc/sphinx_build/html + - _build/default/doc/refman-html + +doc:refman-pdf:dune: + extends: .dune-ci-template + variables: + DUNE_TARGET: refman-pdf + artifacts: + paths: + - _build/log + - _build/default/doc/refman-pdf doc:stdlib:dune: extends: .dune-ci-template @@ -531,7 +541,7 @@ test-suite:base+async: needs: - build:base variables: - COQFLAGS: "-async-proofs on -async-proofs-cache force" + COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force" timeout: 100m allow_failure: true only: @@ -721,10 +731,24 @@ plugin:ci-elpi: plugin:ci-equations: extends: .ci-template + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci plugin:ci-fiat_parsers: extends: .ci-template +plugin:ci-metacoq: + extends: .ci-template + stage: stage-3 + needs: + - build:base + - plugin:ci-equations + dependencies: + - build:base + - plugin:ci-equations + plugin:ci-mtac2: extends: .ci-template diff --git a/.ocamlformat b/.ocamlformat index 59883180e5..d5608839fb 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,3 +1,4 @@ +version=0.13.0 profile=ocamlformat module-item-spacing=compact sequence-style=terminator diff --git a/Makefile.ci b/Makefile.ci index dfb3f69a8c..f58dd9f37a 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -33,6 +33,7 @@ CI_TARGETS= \ ci-iris-lambda-rust \ ci-math-classes \ ci-math-comp \ + ci-metacoq \ ci-mtac2 \ ci-paramcoq \ ci-perennial \ @@ -72,6 +73,8 @@ ci-fiat-crypto: ci-coqprime ci-rewriter ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io +ci-metacoq: ci-equations + # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/Makefile.dune b/Makefile.dune index b433ed1b94..0520d43da9 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,7 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt quickide # Partial / quick developer targets -.PHONY: refman-html stdlib-html apidoc # Documentation targets +.PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accessory targets .PHONY: fmt ocheck ireport clean # Maintenance targets @@ -32,6 +32,7 @@ help: @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @@ -92,6 +93,9 @@ test-suite: voboot refman-html: voboot dune build @refman-html +refman-pdf: voboot + dune build @refman-pdf + stdlib-html: voboot dune build @stdlib-html @@ -102,7 +106,7 @@ release: voboot dune build $(DUNEOPT) -p coq fmt: voboot - dune build @fmt + dune build @fmt --auto-promote ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all diff --git a/coq-refman.opam b/coq-doc.opam index 937c4b08d3..2f4072955f 100644 --- a/coq-refman.opam +++ b/coq-doc.opam @@ -27,7 +27,7 @@ build-env: [ ] build: [ - [ "dune" "build" "@refman" "-j" jobs ] + [ "dune" "build" "-p" name "-j" jobs ] ] # Would be better to have a *-conf package? diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index bd7ee46358..70e3fe5c69 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -330,3 +330,10 @@ : "${perennial_CI_REF:=master}" : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" + +######################################################################## +# metacoq +######################################################################## +: "${metacoq_CI_REF:=master}" +: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" +: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 871d033f5b..30047e624b 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download equations -( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci) +( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh new file mode 100755 index 0000000000..1302065961 --- /dev/null +++ b/dev/ci/ci-metacoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download metacoq + +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index e14f634073..e56e4d38ea 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-03-19-V93" +# CACHEKEY: "bionic_coq-V2020-03-19-V29" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.09.1" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12" + BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh new file mode 100644 index 0000000000..6928925e54 --- /dev/null +++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then + + equations_CI_REF=proof+more_naming_unif + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + rewriter_CI_REF=proof+more_naming_unif + rewriter_CI_GITURL=https://github.com/ejgallego/rewriter + + elpi_CI_REF=proof+more_naming_unif + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9088df6856..b82388675c 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,19 +1,19 @@ ## Changes between Coq 8.11 and Coq 8.12 -### ML API +### Code formatting -Refiner.catchable_exception is deprecated, use instead -CErrors.noncritical in try-with block. Note that nothing is needed in -tclORELSE block since the exceptions there are supposed to be -non-critical by construction. +- The automatic code formatting tool `ocamlformat` is enabled now for + the micromega codebase. Version 0.13.0 is required. See + `ocalmformat`'s documentation for more details on integration with + your editor. ### ML API -Types `precedence`, `parenRelation`, `tolerability` in -`notgram_ops.ml` have been reworked. See `entry_level` and -`entry_relative_level` in `constrexpr.ml`. +Notations: -### ML API +- Types `precedence`, `parenRelation`, `tolerability` in + `notgram_ops.ml` have been reworked. See `entry_level` and + `entry_relative_level` in `constrexpr.ml`. Exception handling: @@ -28,6 +28,11 @@ Exception handling: + printers are of type `exn -> Pp.t option` [`None` == not handled] + it is forbidden for exception printers to raise. +- Refiner.catchable_exception is deprecated, use instead + CErrors.noncritical in try-with block. Note that nothing is needed in + tclORELSE block since the exceptions there are supposed to be + non-critical by construction. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst index 79879c78d5..20d48929f2 100644 --- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -1,5 +1,8 @@ - **Fixed:** - Regression of :tacn:`lia` due to more powerful :tacn:`zify` + :tacn:`zify` now handles :g:`Z.pow_pos` by default. + In Coq 8.11, this was the case only when loading module + :g:`ZifyPow` because this triggered a regression of :tacn:`lia`. + The regression is now fixed, and the module kept only for compatibility (`#11362 <https://github.com/coq/coq/pull/11362>`_, fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, by Frédéric Besson). diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst index 638222fbe1..b89e047153 100644 --- a/doc/changelog/07-commands-and-options/11162-local-cs.rst +++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst @@ -1,3 +1,3 @@ -- **Added:** Handle the ``#[local]`` attribute in :g:`Canonical +- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical Structure` declarations (`#11162 <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst new file mode 100644 index 0000000000..d134aeae8b --- /dev/null +++ b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst @@ -0,0 +1,5 @@ +- **Removed:** Deprecated unsound compatibility ``Template Check`` + flag that was introduced in 8.10 to help users gradually move their + template polymorphic inductive type definitions outside sections + (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie + Pédrot). diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst index 1f8dcd3992..419d683037 100644 --- a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst +++ b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst @@ -1,5 +1,6 @@ - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use them as sub-attributes of the ``universes`` attribute (`#11663 - <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). + Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + :attr:`universes(template)` and :attr:`universes(notemplate)` instead + (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst new file mode 100644 index 0000000000..b6a034941d --- /dev/null +++ b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst @@ -0,0 +1,12 @@ +- **Added:** + New attributes supported when defining an inductive type + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)`, which correspond to legacy attributes + ``Cumulative``, ``NonCumulative``, and the so far undocumented + ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by + Théo Zimmermann). + +- **Changed:** + Legacy attributes can now be passed in any order. See + :ref:`gallina-attributes` (`#11665 + <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann). diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst new file mode 100644 index 0000000000..a07e48d2d8 --- /dev/null +++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst @@ -0,0 +1,6 @@ +- **Changed:** + The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc. + and the option set flags `-set`, `-unset` are processed have been reversed. + In the new behavior, require/load flags are processed before option flags. + (`#11851 <https://github.com/coq/coq/pull/11851>`_, + by Lasse Blaauwbroek). @@ -1,5 +1,10 @@ (rule - (targets sphinx_build) + (targets unreleased.rst) + (deps (source_tree changelog)) + (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + +(alias + (name refman-deps) (deps ; We could use finer dependencies here so the build is faster: ; @@ -10,23 +15,34 @@ ; + tools/coqdoc/coqdoc.css (package coq) (source_tree sphinx) - (source_tree tools) + (source_tree tools/coqrst) unreleased.rst - (env_var SPHINXWARNOPT)) - (action - (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (env_var SPHINXWARNOPT))) -(alias - (name refman-html) - (deps sphinx_build)) +(rule + (targets refman-html) + (alias refman-html) + (package coq-doc) + (deps (alias refman-deps)) + (action + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets}))) (rule - (targets unreleased.rst) - (deps (source_tree changelog)) - (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + (targets refman-pdf) + (alias refman-pdf) + (package coq-doc) + (deps (alias refman-deps)) + (action + (progn + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets}) + (chdir %{targets} (run make))))) + +; Installable directories are not yet fully supported by Dune. See +; ocaml/dune#1868. Yet, this makes coq-doc.install a valid target to +; generate the whole Coq documentation. And the result under +; _build/install/default/doc/coq-doc looks just right! -; The install target still needs more work. -; (install -; (section doc) -; (package coq-refman) -; (files sphinx_build)) +(install + (files (refman-html as html/refman) (refman-pdf as pdf/refman)) + (section doc) + (package coq-doc)) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 307214089f..2fdca15552 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,12 +1,12 @@ -let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false - ~opaque ~poly sigma udecl ~types:tyopt ~body in + ~opaque ~poly sigma ~udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in - let ubinders = Evd.universe_binders sigma in + let ubind = Evd.universe_binders sigma in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None [] + ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 549249d25c..cbb5c0db8a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -98,10 +98,17 @@ coercions. .. flag:: Program Mode Enables the program mode, in which 1) typechecking allows subset coercions and - 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and - :cmd:`Program Definition` act - like Program Fixpoint/Definition, generating obligations if there are - unresolved holes after typechecking. + 2) the elaboration of pattern matching of :cmd:`Fixpoint` and + :cmd:`Definition` act as if the :attr:`program` attribute had been + used, generating obligations if there are unresolved holes after + typechecking. + +.. attr:: program + + This attribute allows to use the Program mode on a specific + definition. An alternative syntax is to use the legacy ``Program`` + prefix (cf. :n:`@legacy_attr`) as documented in the rest of this + chapter. .. _syntactic_control: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 7abeca7815..bd4c276571 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,7 +47,7 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using the attribute ``refine``, if the term is not sufficient to +Using the :attr:`refine` attribute, if the term is not sufficient to finish the definition (e.g. due to a missing field or non-inferable hole) it must be finished in proof mode. If it is sufficient a trivial proof mode with no open goals is started. @@ -77,9 +77,9 @@ remaining fields, e.g.: Defined. One has to take care that the transparency of every field is -determined by the transparency of the :cmd:`Instance` proof. One can use -alternatively the :cmd:`Program Instance` variant which has richer facilities -for dealing with obligations. +determined by the transparency of the :cmd:`Instance` proof. One can +use alternatively the :attr:`program` attribute to get richer +facilities for dealing with obligations. Binding classes @@ -174,7 +174,7 @@ For example: .. coqtop:: in - Global Program Instance option_eqb : EqDec (option A) := + #[ global, program ] Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true @@ -188,7 +188,7 @@ For example: About option_eqb. -Here the :cmd:`Global` modifier redeclares the instance at the end of the +Here the :attr:`global` attribute redeclares the instance at the end of the section, once it has been generalized by the context variables it uses. @@ -300,9 +300,11 @@ Summary of the commands The :cmd:`Class` command is used to declare a typeclass with parameters :token:`binders` and fields the declared record fields. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + Like any command declaring a record, this command supports the + :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)` attributes. .. _singleton-class: @@ -341,6 +343,25 @@ Summary of the commands :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. + This command supports the :attr:`global` attribute that can be + used on instances declared in a section so that their + generalization is automatically redeclared after the section is + closed. + + Like :cmd:`Definition`, it also supports the :attr:`program` + attribute to switch the type checking to `Program` (chapter + :ref:`programs`) and use the obligation mechanism to manage missing + fields. + + Finally, it supports the lighter :attr:`refine` attribute: + + .. attr:: refine + + This attribute can be used to leave holes or not provide all + fields in the definition of an instance and open the tactic mode + to fill them. It works exactly as if no body had been given and + the :tacn:`refine` tactic has been used first. + .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or @@ -348,19 +369,6 @@ Summary of the commands {+ @term}`. One need not even mention the unique field name for singleton classes. - .. cmdv:: Global Instance - :name: Global Instance - - One can use the :cmd:`Global` modifier on instances declared in a - section so that their generalization is automatically redeclared - after the section is closed. - - .. cmdv:: Program Instance - :name: Program Instance - - Switches the type checking to `Program` (chapter :ref:`programs`) and - uses the obligation mechanism to manage missing fields. - .. cmdv:: Declare Instance :name: Declare Instance diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 0e326f45d2..a08495badd 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,62 +122,92 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. cmd:: Polymorphic @definition +.. attr:: universes(polymorphic) - As shown in the examples, polymorphic definitions and inductives can be - declared using the ``Polymorphic`` prefix. + This attribute can be used to declare universe polymorphic + definitions and inductive types. There is also a legacy syntax + using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. .. flag:: Universe Polymorphism - Once enabled, this flag will implicitly prepend ``Polymorphic`` to any - definition of the user. + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(monomorphic)` attribute is + used. -.. cmd:: Monomorphic @definition +.. attr:: universes(monomorphic) - When the :flag:`Universe Polymorphism` flag is set, to make a definition - producing global universe constraints, one can use the ``Monomorphic`` prefix. + This attribute can be used to declare universe monomorphic + definitions and inductive types (i.e. global universe constraints + are produced), even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). -Many other commands support the ``Polymorphic`` flag, including: +Many other commands can be used to declare universe polymorphic or +monomorphic constants depending on whether the :flag:`Universe +Polymorphism` flag is on or the :attr:`universes(polymorphic)` or +:attr:`universes(monomorphic)` attributes are used: -.. TODO add links on each of these? +- :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe + polymorphic constants. -- ``Lemma``, ``Axiom``, and all the other “definition” keywords support - polymorphism. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Section` command will locally set the polymorphism flag inside + the section. -- :cmd:`Section` will locally set the polymorphism flag inside the section. +- :cmd:`Variable`, :cmd:`Context`, :cmd:`Universe` and + :cmd:`Constraint` in a section support polymorphism. See + :ref:`universe-polymorphism-in-sections` for more details. -- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - -- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint - polymorphically, not at a single instance. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Hint Resolve` or :cmd:`Hint Rewrite` commands will make + :tacn:`auto` / :tacn:`rewrite` use the hint polymorphically, not at + a single instance. .. _cumulative: Cumulative, NonCumulative ------------------------- -Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the :g:`Cumulative` prefix. +.. attr:: universes(cumulative) + + Polymorphic inductive types, coinductive types, variants and + records can be declared cumulative using this attribute or the + legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. -.. cmd:: Cumulative @inductive + This means that two instances of the same inductive type (family) + are convertible based on the universe variances; they do not need + to be equal. - Declares the inductive as cumulative + .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. -Alternatively, there is a :flag:`Polymorphic Inductive -Cumulativity` flag which when set, makes all subsequent *polymorphic* -inductive definitions cumulative. When set, inductive types and the -like can be enforced to be non-cumulative using the :g:`NonCumulative` -prefix. + Using this attribute requires being in a polymorphic context, + i.e. either having the :flag:`Universe Polymorphism` flag on, or + having used the :attr:`universes(polymorphic)` attribute as + well. -.. cmd:: NonCumulative @inductive + .. note:: - Declares the inductive as non-cumulative + ``#[ universes(polymorphic), universes(cumulative) ]`` can be + abbreviated into ``#[ universes(polymorphic, cumulative) ]``. .. flag:: Polymorphic Inductive Cumulativity - When this flag is on, it sets all following polymorphic inductive - types as cumulative (it is off by default). + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(noncumulative)` attribute is used. It has no + effect on *monomorphic* inductive definitions. + +.. attr:: universes(noncumulative) + + Declares the inductive type as non-cumulative even if the + :flag:`Polymorphic Inductive Cumulativity` flag is on. There is + also a legacy syntax using the ``NonCumulative`` prefix (see + :n:`@legacy_attr`). + + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. Consider the examples below. @@ -220,34 +250,10 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -Cumulative inductive types, coinductive types, variants and records -only make sense when they are universe polymorphic. Therefore, an -error is issued whenever the user uses the :g:`Cumulative` or -:g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag. -That is, this flag, when set, makes all subsequent *polymorphic* -inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) -but has no effect on *monomorphic* inductive declarations. - -Consider the following examples. - -.. coqtop:: all reset - - Fail Monomorphic Cumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Fail Monomorphic NonCumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Set Polymorphic Inductive Cumulativity. - Inductive Unit := unit. - An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. coqtop:: in +.. coqtop:: in reset Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. @@ -368,10 +374,14 @@ to universes and explicitly instantiate polymorphic definitions. In the monorphic case, this command declares a new global universe named :g:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The - command supports the ``Polymorphic`` flag only in sections, meaning the - universe quantification will be discharged on each section definition + command supports the :attr:`universes(polymorphic)` attribute (or + the ``Polymorphic`` prefix) only in sections, meaning the universe + quantification will be discharged on each section definition independently. + .. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead. + :undocumented: + .. cmd:: Constraint @univ_constraint Polymorphic Constraint @univ_constraint @@ -379,9 +389,10 @@ to universes and explicitly instantiate polymorphic definitions. If consistent, the constraint is then enforced in the global environment. Like :cmd:`Universe`, it can be used with the - ``Polymorphic`` prefix in sections only to declare constraints - discharged at section closing time. One cannot declare a global - constraint on polymorphic universes. + :attr:`universes(polymorphic)` attribute (or the ``Polymorphic`` + prefix) in sections only to declare constraints discharged at + section closing time. One cannot declare a global constraint on + polymorphic universes. .. exn:: Undeclared universe @ident. :undocumented: @@ -389,6 +400,9 @@ to universes and explicitly instantiate polymorphic definitions. .. exn:: Universe inconsistency. :undocumented: + .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead + :undocumented: + Polymorphic definitions ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 4e94240c32..f76b60097a 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -222,7 +222,7 @@ Changes in 8.11+beta1 .. _811RefineInstance: -- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more +- **Added:** :attr:`refine` attribute for :cmd:`Instance`, a more predictable version of the old ``Refine Instance Mode`` which unconditionally opens a proof (`#10996 <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). @@ -1316,7 +1316,7 @@ Changes in 8.10+beta3 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 + `-no-template-check` and a global 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 diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 4bf1a6f3a9..2ed9ec21b3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -186,9 +186,7 @@ nitpick_ignore = [ ('token', token) for token in [ 'assums', 'binders', 'collection', - 'definition', 'dirpath', - 'inductive', 'ind_body', 'modpath', 'module', diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 4beaff70f5..b0acd09af6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1200,45 +1200,47 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the ``universes(notemplate)`` + This can be prevented using the :attr:`universes(notemplate)` attribute. + Template polymorphism and full universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the latter is + enabled (through the :flag:`Universe Polymorphism` flag or the + :attr:`universes(polymorphic)` attribute) it will prevail over + automatic template polymorphism. + .. 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`. + Warning ``auto-template`` can be used (it is off by default) 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 ``universes(template)`` attribute: it should then fulfill 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 ``universes(template)`` attribute. - -.. flag:: Template Check - - This flag is on by default. Turning it off 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. + the :attr:`universes(template)` attribute: in this case, the + warning is not emitted. + +.. attr:: universes(template) + + This attribute can be used to explicitly declare an inductive type + as template polymorphic, whether the :flag:`Auto Template + Polymorphism` flag is on or off. + + .. exn:: template and polymorphism not compatible + + This attribute cannot be used in a full universe polymorphic + context, i.e. if the :flag:`Universe Polymorphism` flag is on or + if the :attr:`universes(polymorphic)` attribute is used. + + .. exn:: Ill-formed template inductive declaration: not polymorphic on any universe. + + The attribute was used but the inductive definition does not + satisfy the criterion to be template polymorphic. + +.. attr:: universes(notemplate) + This attribute can be used to prevent an inductive type to be + template polymorphic, even if the :flag:`Auto Template + Polymorphism` flag is on. 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 diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index b9e181dd94..eff5eb60eb 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -42,9 +42,11 @@ expressions. In this sense, the :cmd:`Record` construction allows defining :cmd:`Record` and :cmd:`Structure` are synonyms. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: @@ -2053,12 +2055,15 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid +.. cmd:: Canonical {? Structure } @qualid :name: Canonical Structure This command declares :token:`qualid` as a canonical instance of a - structure (a record). When the :g:`#[local]` attribute is given the effect - stops at the end of the :g:`Section` containig it. + structure (a record). + + This command supports the :attr:`local` attribute. When used, the + structure stops being a canonical instance at the end of the + :cmd:`Section` containing it. Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -2106,9 +2111,12 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. note:: - To prevent a field from being involved in the inference of canonical instances, - its declaration can be annotated with the :g:`#[canonical(false)]` attribute. + .. attr:: canonical(false) + + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with the + :attr:`canonical(false)` attribute (cf. the syntax of + :n:`@record_field`). .. example:: @@ -2121,11 +2129,17 @@ in :ref:`canonicalstructures`; here only a simple example is given. See :ref:`canonicalstructures` for a more realistic example. - .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. +.. attr:: canonical + + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. + .. cmd:: Print Canonical Projections {* @ident} This displays the list of global names that are components of some diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 4f0cf5f815..e710e19c12 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -767,6 +767,10 @@ Section :ref:`typing-rules`. If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified computation on :n:`@term`. + These commands also support the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`program` and + :attr:`canonical` attributes. + If :n:`@term` is omitted, Coq enters the proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant @@ -821,9 +825,11 @@ Inductive types may be impossible to derive (for example, when :n:`@ident` is a proposition). - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -851,9 +857,9 @@ Inductive types :n:`@ident` being defined (or :n:`@ident` applied to arguments in the case of annotated inductive types — cf. next section). -The following subsections show examples of simple inductive types, simple annotated -inductive types, simple parametric inductive types and mutually inductive -types. +The following subsections show examples of simple inductive types, +simple annotated inductive types, simple parametric inductive types, +mutually inductive types and private (matching) inductive types. .. _simple-inductive-types: @@ -1122,6 +1128,31 @@ Mutually defined inductive types A generic command :cmd:`Scheme` is useful to build automatically various mutual induction principles. +Private (matching) inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. attr:: private(matching) + + This attribute can be used to forbid the use of the :g:`match` + construct on objects of this inductive type outside of the module + where it is defined. There is also a legacy syntax using the + ``Private`` prefix (cf. :n:`@legacy_attr`). + + The main use case of private (matching) inductive types is to emulate + quotient types / higher-order inductive types in projects such as + the `HoTT library <https://github.com/HoTT/HoTT>`_. + +.. example:: + + .. coqtop:: all + + Module Foo. + #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat. + Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + End Foo. + Import Foo. + Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + Variants ~~~~~~~~ @@ -1132,9 +1163,11 @@ Variants be defined using :cmd:`Variant`). No induction scheme is generated for this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. .. exn:: The @num th argument of @ident must be @ident in @type. :undocumented: @@ -1160,9 +1193,11 @@ of the type. type, since such principles only make sense for inductive types. For co-inductive types, the only elimination principle is case analysis. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. .. example:: @@ -1607,14 +1642,21 @@ the proof and adds it to the environment. Attributes ----------- -.. insertprodn all_attrs legacy_attrs +.. insertprodn all_attrs legacy_attr .. prodn:: - all_attrs ::= {* #[ {*, @attr } ] } {? @legacy_attrs } + all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr } attr ::= @ident {? @attr_value } attr_value ::= = @string | ( {*, @attr } ) - legacy_attrs ::= {? {| Local | Global } } {? {| Polymorphic | Monomorphic } } {? Program } {? {| Cumulative | NonCumulative } } {? Private } + legacy_attr ::= Local + | Global + | Polymorphic + | Monomorphic + | Cumulative + | NonCumulative + | Private + | Program Attributes modify the behavior of a command or tactic. Syntactically, most commands and tactics can be decorated with attributes, but @@ -1623,7 +1665,7 @@ attributes not supported by the command or tactic will be flagged as errors. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. -The legacy attributes (:n:`@legacy_attrs`) provide an older, alternate syntax +The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: ================ ================================ @@ -1633,65 +1675,12 @@ Legacy attribute New attribute `Global` :attr:`global` `Polymorphic` :attr:`universes(polymorphic)` `Monomorphic` :attr:`universes(monomorphic)` -`Cumulative` none -`NonCumulative` none -`Private` none +`Cumulative` :attr:`universes(cumulative)` +`NonCumulative` :attr:`universes(noncumulative)` +`Private` :attr:`private(matching)` `Program` :attr:`program` ================ ================================ -Some attributes are specific to a command, and so are described with -that command. Currently, the following attributes are recognized: - -.. attr:: universes(monomorphic) - :name: universes(monomorphic) - - See :ref:`polymorphicuniverses`. - -.. attr:: universes(polymorphic) - :name: universes(polymorphic) - - See :ref:`polymorphicuniverses`. - -.. attr:: universes(template) - :name: universes(template) - - See :ref:`Template-polymorphism` - -.. attr:: universes(notemplate) - :name: universes(notemplate) - - See :ref:`Template-polymorphism` - -.. attr:: program - - See :ref:`programs`. - -.. attr:: global - - See :ref:`controlling-locality-of-commands`. - -.. attr:: local - - See :ref:`controlling-locality-of-commands`. - -.. attr:: Cumulative - - Legacy attribute, only allowed in a polymorphic context. - Specifies that two instances of the same inductive type (family) are convertible - based on the universe variances; they do not need to be equal. - See :ref:`cumulative`. - -.. attr:: NonCumulative - - Legacy attribute, only allowed in a polymorphic context. - Specifies that two instances of the same inductive type (family) are convertible - only if all the universes are equal. - See :ref:`cumulative`. - -.. attr:: Private - - Legacy attribute. Documentation to be added. - .. attr:: deprecated ( {? since = @string , } {? note = @string } ) :name: deprecated @@ -1703,46 +1692,24 @@ that command. Currently, the following attributes are recognized: It can trigger the following warnings: - .. warn:: Tactic @qualid is deprecated since @string. @string. - :undocumented: - - .. warn:: Tactic Notation @qualid is deprecated since @string. @string. - :undocumented: - - .. warn:: Notation @string__1 is deprecated since @string__2. @string__3. - - :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, - :n:`@string__3` is the note. - -.. attr:: canonical + .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. + Tactic Notation @qualid is deprecated since @string__since. @string__note. + Notation @string is deprecated since @string__since. @string__note. - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. - - This attribute can take the value ``false`` when decorating a record field - declaration with the effect of preventing the field from being involved in - the inference of canonical instances. - - See also :ref:`canonical-structure-declaration`. - -.. example:: + :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, + :n:`@string__note` is the note (usually explains the replacement). - .. coqtop:: all reset warn + .. example:: - From Coq Require Program. - #[program] Definition one : nat := S _. - Next Obligation. - exact O. - Defined. + .. coqtop:: all reset warn - #[deprecated(since="8.9.0", note="Use idtac instead.")] - Ltac foo := idtac. + #[deprecated(since="8.9.0", note="Use idtac instead.")] + Ltac foo := idtac. - Goal True. - Proof. + Goal True. + Proof. now foo. - Abort. + Abort. .. warn:: Unsupported attribute diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 98d222e317..aa4b6edd7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -227,7 +227,10 @@ and ``coqtop``, unless stated otherwise: type of the option. For flags ``Option Name`` is equivalent to ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. + shell syntax, Coq does not see them. Flags are processed after initialization + of the document. This includes the `Prelude` if loaded and any libraries loaded + through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` + options. :-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 514353e39b..e5ff26520a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -499,6 +499,40 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use (``.PHONY`` or not) please use ``CoqMakefile.local``. +Precompiling for ``native_compute`` ++++++++++++++++++++++++++++++++++++ + +To compile files for ``native_compute``, one can use the +``-native-compiler yes`` option of |Coq|, for instance by putting the +following in a :ref:`coqmakefilelocal` file: + +:: + + COQEXTRAFLAGS += -native-compiler yes + +The generated ``CoqMakefile`` installation target will then take care +of installing the extra ``.coq-native`` directories. + +.. note:: + + As an alternative to modifying any file, one can set the + environment variable when calling ``make``: + + :: + + COQEXTRAFLAGS="-native-compiler yes" make + + This can be useful when files cannot be modified, for instance when + installing via OPAM a package built with ``coq_makefile``: + + :: + + COQEXTRAFLAGS="-native-compiler yes" opam install coq-package + +.. note:: + + This requires all dependencies to be themselves compiled with + ``-native-compiler yes``. Building a |Coq| project with Dune ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4401f8fa2f..895886605d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,34 +91,30 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? {| Local | Global | Export } } Set @flag +.. cmd:: Set @flag :name: Set - Sets :token:`flag` on. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` on. -.. cmd:: {? {| Local | Global | Export } } Unset @flag +.. cmd:: Unset @flag :name: Unset - Sets :token:`flag` off. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` off. .. cmd:: Test @flag Prints the current value of :token:`flag`. -.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } +.. cmd:: Set @option {| @num | @string } :name: Set @option - Sets :token:`option` to the specified value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to the specified value. -.. cmd:: {? {| Local | Global | Export } } Unset @option +.. cmd:: Unset @option :name: Unset @option - Sets :token:`option` to its default value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to its default value. .. cmd:: Test @option @@ -157,27 +153,37 @@ capital letter. A synonym for :cmd:`Print Options`. -.. _set_unset_scope_qualifiers: +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. -Scope qualifiers for :cmd:`Set` and :cmd:`Unset` -````````````````````````````````````````````````` - -:n:`{? {| Local | Global | Export } }` - -Flag and option settings can be global in scope or local to nested scopes created by -:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - -* no qualifier: the original setting is *not* restored at the end of the current module or section. -* **Local**: the setting is applied within the current scope. The original value of the option - or flag is restored at the end of the current module or section. -* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current - module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing - the file sets the option. -* **Export**: similar to **Local**, the original value of the option or flag is restored at the - end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing - the file sets the option. +.. note:: -Newly opened scopes inherit the current settings. + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. If your goal is to define + project-wide settings, you should rather use the command-line + arguments ``-set`` and ``-unset`` for setting flags and options + (cf. :ref:`command-line-options`). .. _requests-to-the-environment: @@ -1152,49 +1158,51 @@ described first. Controlling the locality of commands ----------------------------------------- +.. attr:: global + local -.. cmd:: Local @command - Global @command - - Some commands support a Local or Global prefix modifier to control the - scope of their effect. There are four kinds of commands: - + Some commands support a :attr:`local` or :attr:`global` attribute + to control the scope of their effect. There is also a legacy (and + much more commonly used) syntax using the ``Local`` or ``Global`` + prefixes (see :n:`@legacy_attr`). There are four kinds of + commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these - commands, the Local modifier limits the effect of the command to the + commands, the :attr:`local` attribute limits the effect of the command to the current section or module it occurs in. As an example, the :cmd:`Coercion` and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the Local modifier limits the + library file they occur in. For these commands, the :attr:`local` attribute limits the effect of the command to the current module if the command does not occur in a - section and the Global modifier extends the effect outside the current + section and the :attr:`global` attribute extends the effect outside the current sections and current module if the command occurs in a section. As an example, the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global modifier is not + extension of their scope outside sections at all and the :attr:`global` attribute is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the ``Global`` - modifier extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` - (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + of the section or module they occur in. For these commands, the :attr:`global` + attribute extends their effect outside the sections and modules they + occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the Local modifier - limits the effect to the current section or module while the Global - modifier extends the effect outside the module even when the command + when no section contains them. For these commands, the :attr:`local` attribute + limits the effect to the current section or module while the :attr:`global` + attribute extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. .. attr:: export - Some commands support an :attr:`export` attribute. The effect of the attribute - is to make the effect of the command available when the module containing it - is imported. The :cmd:`Hint` command accepts it for instance. + Some commands support an :attr:`export` attribute. The effect of + the attribute is to make the effect of the command available when + the module containing it is imported. It is supported in + particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + commands. .. _controlling-typing-flags: diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 093c7a62b2..0b6ca5f178 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -13,6 +13,8 @@ (rule (targets html) + (alias stdlib-html) + (package coq-doc) (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) @@ -31,6 +33,12 @@ (progn (cat %{header}) (cat index-list.html) (cat %{footer}))) (run cp _index.html html/index.html)))) -(alias - (name stdlib-html) - (deps html)) +; Installable directories are not yet fully supported by Dune. See +; ocaml/dune#1868. Yet, this makes coq-doc.install a valid target to +; generate the whole Coq documentation. And the result under +; _build/install/default/doc/coq-doc looks just right! + +(install + (files (html as html/stdlib)) + (section doc) + (package coq-doc)) diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 60d6039b0f..67d0b37e81 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -50,6 +50,7 @@ theories/micromega/ZifyInst.v theories/micromega/ZifyBool.v theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v +theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/Nsatz.v theories/omega/Omega.v diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 84f32e187b..0b94b0d675 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -519,7 +519,7 @@ class ProductionObject(CoqObject): row = nodes.inline(classes=['prodn-row']) entry = nodes.inline(classes=['prodn-cell-nonterminal']) if lhs != "": - target_name = 'grammar-token-' + lhs + target_name = 'grammar-token-' + nodes.make_id(lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) # putting prodn-target on the target node won't appear in the tex file inline = nodes.inline(classes=['prodn-target']) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index fe2e68a517..5bf122078d 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -140,10 +140,10 @@ field_ident: [ | "." ident ] -basequalid: [ -| REPLACE ident fields -| WITH ident LIST0 field_ident -| DELETE ident +qualid: [ | DELETENT ] + +qualid: [ +| ident LIST0 field_ident ] field: [ | DELETENT ] @@ -387,7 +387,7 @@ gallina: [ | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ] | DELETE assumptions_token inline assum_list -| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| REPLACE finite_token LIST1 inductive_definition SEP "with" | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) | "Variant" inductive_definition LIST0 ( "with" inductive_definition ) @@ -405,11 +405,6 @@ gallina: [ | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] -DELETE: [ -| private_token -| cumulativity_token -] - constructor_list_or_record_decl: [ | OPTINREF ] @@ -737,12 +732,8 @@ assumption_token: [ | WITH [ "Variable" | "Variables" ] ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" -] - all_attrs: [ -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr ] vernacular: [ @@ -842,7 +833,6 @@ SPLICE: [ | ne_lstring | ne_string | lstring -| basequalid | fullyqualid | global | reference diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 6897437457..2fabf92b7f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -386,11 +386,6 @@ fullyqualid: [ | ident ] -basequalid: [ -| ident fields -| ident -] - name: [ | "_" | ident @@ -401,6 +396,10 @@ reference: [ | ident ] +qualid: [ +| reference +] + by_notation: [ | ne_string OPT [ "%" IDENT ] ] @@ -410,10 +409,6 @@ smart_global: [ | by_notation ] -qualid: [ -| basequalid -] - ne_string: [ | STRING ] @@ -436,7 +431,7 @@ lstring: [ integer: [ | NUMERAL -| "-" NUMERAL +| test_minus_nat "-" NUMERAL ] natural: [ @@ -735,21 +730,22 @@ attribute_value: [ | ] -vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +vernac: [ +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." @@ -774,7 +770,7 @@ gallina: [ | assumptions_token inline assum_list | def_token ident_decl def_body | "Let" identref def_body -| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| finite_token LIST1 inductive_definition SEP "with" | "Fixpoint" LIST1 rec_definition SEP "with" | "Let" "Fixpoint" LIST1 rec_definition SEP "with" | "CoFixpoint" LIST1 corec_definition SEP "with" @@ -903,16 +899,6 @@ finite_token: [ | "Class" ] -cumulativity_token: [ -| "Cumulative" -| "NonCumulative" -] - -private_token: [ -| "Private" -| -] - def_body: [ | binders ":=" reduce lconstr | binders ":" lconstr ":=" reduce lconstr diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f26a174722..c3634466cc 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -172,7 +172,7 @@ vernacular: [ ] all_attrs: [ -| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr ] attr: [ @@ -184,8 +184,15 @@ attr_value: [ | "(" LIST0 attr SEP "," ")" ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] sort: [ @@ -338,20 +345,10 @@ pattern0: [ ] vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly -] - -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 275468ad3d..163645b719 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -63,14 +63,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in + let args,_ = decompose_prod_assum (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in let real_args = if princ_type_info.indarg_in_concl then List.tl args else args in Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl), - Term.compose_prod real_args (mkSort new_sort)) + Term.it_mkProd_or_LetIn (mkSort new_sort) real_args) in let new_predicates = List.map_i diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 7bddbc994f..446026c4c8 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -295,8 +295,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) ~name:new_princ_name ~hook_data ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) - UnivNames.empty_binders - entry [] in + ~ubind:UnivNames.empty_binders + ~impargs:[] + entry in () with e when CErrors.noncritical e -> raise (Defining_principle e) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c7dfe69fb1..e08ad9af3a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1517,7 +1517,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1532,7 +1532,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 87778f7f7b..82f8b5b3e2 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1279,7 +1279,8 @@ module M = struct let dump_expr i e = let rec dump_expr = function | Mc.PEX n -> - EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) + EConstr.mkRel + (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx) | Mc.PEc z -> dexpr.dump_cst z | Mc.PEadd (e1, e2) -> EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) @@ -1294,7 +1295,9 @@ module M = struct dump_expr e in let mkop op e1 e2 = - try EConstr.mkApp (List.assoc op dexpr.dump_op, [|e1; e2|]) + try + EConstr.mkApp + (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|]) with Not_found -> EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|]) in @@ -1480,7 +1483,8 @@ type ('synt_c, 'prf) domain_spec = ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) dump_coeff : 'synt_c -> EConstr.constr ; proof_typ : EConstr.constr - ; dump_proof : 'prf -> EConstr.constr } + ; dump_proof : 'prf -> EConstr.constr + ; coeff_eq : 'synt_c -> 'synt_c -> bool } (** * The datastructures that aggregate theory-dependent proof values. *) @@ -1491,7 +1495,8 @@ let zz_domain_spec = ; coeff = Lazy.force coq_Z ; dump_coeff = dump_z ; proof_typ = Lazy.force coq_proofTerm - ; dump_proof = dump_proof_term } + ; dump_proof = dump_proof_term + ; coeff_eq = Mc.zeq_bool } let qq_domain_spec = lazy @@ -1499,7 +1504,8 @@ let qq_domain_spec = ; coeff = Lazy.force coq_Q ; dump_coeff = dump_q ; proof_typ = Lazy.force coq_QWitness - ; dump_proof = dump_psatz coq_Q dump_q } + ; dump_proof = dump_psatz coq_Q dump_q + ; coeff_eq = Mc.qeq_bool } let max_tag f = 1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0)) @@ -1603,7 +1609,12 @@ let witness_list_tags p g = witness_list p g * Prune the proof object, according to the 'diff' between two cnf formulas. *) -let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) = +let compact_proofs (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res + (cnf_ff' : 'cst cnf) = + let eq_formula (p1, o1) (p2, o2) = + let open Mutils.Hash in + eq_pol eq_cst p1 p2 && eq_op1 o1 o2 + in let compact_proof (old_cl : 'cst clause) (prf, prover) (new_cl : 'cst clause) = let new_cl = List.mapi (fun i (f, _) -> (f, i)) new_cl in @@ -1611,7 +1622,7 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) = let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in - List.assoc formula new_cl + CList.assoc_f eq_formula formula new_cl in (* if debug then begin @@ -1641,7 +1652,13 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) = (new_cl : 'cst clause) = let hyps_idx = prover.hyps prf in let hyps = selecti hyps_idx old_cl in - is_sublist ( = ) hyps new_cl + let eq (f1, (t1, e1)) (f2, (t2, e2)) = + Int.equal (Tag.compare t1 t2) 0 + && eq_formula f1 f2 + && (e1 : EConstr.t) = (e2 : EConstr.t) + (* FIXME: what equality should we use here? *) + in + is_sublist eq hyps new_cl in let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *) @@ -1798,7 +1815,7 @@ let micromega_tauto pre_process cnf spec prover env | None -> failwith "abstraction is wrong" | Some res -> () end ; *) - let res' = compact_proofs cnf_ff res cnf_ff' in + let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in let res' = dump_list spec.proof_typ spec.dump_proof res' in Prf (ids, ff', res') @@ -1946,7 +1963,8 @@ let micromega_genr prover tac = ; coeff = Lazy.force coq_Rcst ; dump_coeff = dump_q ; proof_typ = Lazy.force coq_QWitness - ; dump_proof = dump_psatz coq_Q dump_q } + ; dump_proof = dump_psatz coq_Q dump_q + ; coeff_eq = Mc.qeq_bool } in Proofview.Goal.enter (fun gl -> let sigma = Tacmach.New.project gl in @@ -1979,7 +1997,7 @@ let micromega_genr prover tac = | Prf (ids, ff', res') -> let ff, ids = formula_hyps_concl - (List.filter (fun (n, _) -> List.mem n ids) hyps) + (List.filter (fun (n, _) -> CList.mem_f Id.equal n ids) hyps) concl in let ff' = abstract_wrt_formula ff' ff in diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index f9a23751bf..27b917383b 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -385,7 +385,13 @@ module Hash = struct let int_of_eq_op1 = Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3) - let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2 + let int_of_eq_op2 = + Mc.( + function + | OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5) + + let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2) + let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2) let hash_op1 h o = combine h (int_of_eq_op1 o) let rec eq_positive p1 p2 = diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 5e0c913996..146860ca00 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -43,6 +43,7 @@ module Tag : sig val max : t -> t -> t val from : int -> t val to_int : t -> int + val compare : t -> t -> int end module TagSet : CSig.SetS with type elt = Tag.t @@ -73,6 +74,7 @@ end module Hash : sig val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool + val eq_op2 : Micromega.op2 -> Micromega.op2 -> bool val eq_positive : Micromega.positive -> Micromega.positive -> bool val eq_z : Micromega.z -> Micromega.z -> bool val eq_q : Micromega.q -> Micromega.q -> bool diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 1742f81b34..15f37868f7 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -19,7 +19,8 @@ type var = int - values are all non-zero *) -type t = (var * Q.t) list +type mono = {var : var; coe : Q.t} +type t = mono list type vector = t (** [equal v1 v2 = true] if the vectors are syntactically equal. *) @@ -29,21 +30,25 @@ let rec equal v1 v2 = | [], [] -> true | [], _ -> false | _ :: _, [] -> false - | (i1, n1) :: v1, (i2, n2) :: v2 -> Int.equal i1 i2 && n1 =/ n2 && equal v1 v2 + | {var = i1; coe = n1} :: v1, {var = i2; coe = n2} :: v2 -> + Int.equal i1 i2 && n1 =/ n2 && equal v1 v2 let hash v = let rec hash i = function | [] -> i - | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l + | {var = vr; coe = vl} :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l in Hashtbl.hash (hash 0 v) let null = [] let is_null v = - match v with [] -> true | [(0, x)] when Q.zero =/ x -> true | _ -> false + match v with + | [] -> true + | [{var = 0; coe = x}] when Q.zero =/ x -> true + | _ -> false -let pp_var_num pp_var o (v, n) = +let pp_var_num pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v @@ -51,7 +56,7 @@ let pp_var_num pp_var o (v, n) = else if Q.zero =/ n then () else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v -let pp_var_num_smt pp_var o (v, n) = +let pp_var_num_smt pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v @@ -79,7 +84,7 @@ let from_list (l : Q.t list) = match l with | [] -> [] | e :: l -> - if e <>/ Q.zero then (i, e) :: xfrom_list (i + 1) l + if e <>/ Q.zero then {var = i; coe = e} :: xfrom_list (i + 1) l else xfrom_list (i + 1) l in xfrom_list 0 l @@ -88,68 +93,71 @@ let to_list m = let rec xto_list i l = match l with | [] -> [] - | (x, v) :: l' -> - if i = x then v :: xto_list (i + 1) l' else Q.zero :: xto_list (i + 1) l + | {var = x; coe = v} :: l' -> + if Int.equal i x then v :: xto_list (i + 1) l' + else Q.zero :: xto_list (i + 1) l in xto_list 0 m -let cons i v rst = if v =/ Q.zero then rst else (i, v) :: rst +let cons i v rst = if v =/ Q.zero then rst else {var = i; coe = v} :: rst let rec update i f t = match t with | [] -> cons i (f Q.zero) [] - | (k, v) :: l -> ( - match Int.compare i k with - | 0 -> cons k (f v) l + | x :: l -> ( + match Int.compare i x.var with + | 0 -> cons x.var (f x.coe) l | -1 -> cons i (f Q.zero) t - | 1 -> (k, v) :: update i f l + | 1 -> x :: update i f l | _ -> failwith "compare_num" ) let rec set i n t = match t with | [] -> cons i n [] - | (k, v) :: l -> ( - match Int.compare i k with - | 0 -> cons k n l + | x :: l -> ( + match Int.compare i x.var with + | 0 -> cons x.var n l | -1 -> cons i n t - | 1 -> (k, v) :: set i n l + | 1 -> x :: set i n l | _ -> failwith "compare_num" ) -let cst n = if n =/ Q.zero then [] else [(0, n)] +let cst n = if n =/ Q.zero then [] else [{var = 0; coe = n}] let mul z t = if z =/ Q.zero then [] else if z =/ Q.one then t - else List.map (fun (i, n) -> (i, z */ n)) t + else List.map (fun {var = i; coe = n} -> {var = i; coe = z */ n}) t let div z t = - if z <>/ Q.one then List.map (fun (x, nx) -> (x, nx // z)) t else t + if z <>/ Q.one then + List.map (fun {var = x; coe = nx} -> {var = x; coe = nx // z}) t + else t -let uminus t = List.map (fun (i, n) -> (i, Q.neg n)) t +let uminus t = List.map (fun {var = i; coe = n} -> {var = i; coe = Q.neg n}) t let rec add (ve1 : t) (ve2 : t) = match (ve1, ve2) with | [], v | v, [] -> v - | (v1, c1) :: l1, (v2, c2) :: l2 -> + | {var = v1; coe = c1} :: l1, {var = v2; coe = c2} :: l2 -> let cmp = Int.compare v1 v2 in if cmp == 0 then let s = c1 +/ c2 in - if Q.zero =/ s then add l1 l2 else (v1, s) :: add l1 l2 - else if cmp < 0 then (v1, c1) :: add l1 ve2 - else (v2, c2) :: add l2 ve1 + if Q.zero =/ s then add l1 l2 else {var = v1; coe = s} :: add l1 l2 + else if cmp < 0 then {var = v1; coe = c1} :: add l1 ve2 + else {var = v2; coe = c2} :: add l2 ve1 let rec xmul_add (n1 : Q.t) (ve1 : t) (n2 : Q.t) (ve2 : t) = match (ve1, ve2) with | [], _ -> mul n2 ve2 | _, [] -> mul n1 ve1 - | (v1, c1) :: l1, (v2, c2) :: l2 -> + | {var = v1; coe = c1} :: l1, {var = v2; coe = c2} :: l2 -> let cmp = Int.compare v1 v2 in if cmp == 0 then let s = (n1 */ c1) +/ (n2 */ c2) in if Q.zero =/ s then xmul_add n1 l1 n2 l2 - else (v1, s) :: xmul_add n1 l1 n2 l2 - else if cmp < 0 then (v1, n1 */ c1) :: xmul_add n1 l1 n2 ve2 - else (v2, n2 */ c2) :: xmul_add n1 ve1 n2 l2 + else {var = v1; coe = s} :: xmul_add n1 l1 n2 l2 + else if cmp < 0 then {var = v1; coe = n1 */ c1} :: xmul_add n1 l1 n2 ve2 + else {var = v2; coe = n2 */ c2} :: xmul_add n1 ve1 n2 l2 let mul_add n1 ve1 n2 ve2 = if n1 =/ Q.one && n2 =/ Q.one then add ve1 ve2 else xmul_add n1 ve1 n2 ve2 @@ -157,8 +165,7 @@ let mul_add n1 ve1 n2 ve2 = let compare : t -> t -> int = Mutils.Cmp.compare_list (fun x y -> Mutils.Cmp.compare_lexical - [ (fun () -> Int.compare (fst x) (fst y)) - ; (fun () -> Q.compare (snd x) (snd y)) ]) + [(fun () -> Int.compare x.var y.var); (fun () -> Q.compare x.coe y.coe)]) (** [tail v vect] returns - [None] if [v] is not a variable of the vector [vect] @@ -169,7 +176,7 @@ let compare : t -> t -> int = let rec tail (v : var) (vect : t) = match vect with | [] -> None - | (v', vl) :: vect' -> ( + | {var = v'; coe = vl} :: vect' -> ( match Int.compare v' v with | 0 -> Some (vl, vect) (* Ok, found *) | -1 -> tail v vect' (* Might be in the tail *) @@ -178,38 +185,49 @@ let rec tail (v : var) (vect : t) = (* Hopeless *) let get v vect = match tail v vect with None -> Q.zero | Some (vl, _) -> vl -let is_constant v = match v with [] | [(0, _)] -> true | _ -> false -let get_cst vect = match vect with (0, v) :: _ -> v | _ -> Q.zero -let choose v = match v with [] -> None | (vr, vl) :: rst -> Some (vr, vl, rst) -let rec fresh v = match v with [] -> 1 | [(v, _)] -> v + 1 | _ :: v -> fresh v -let variables v = List.fold_left (fun acc (x, _) -> ISet.add x acc) ISet.empty v -let decomp_cst v = match v with (0, vl) :: v -> (vl, v) | _ -> (Q.zero, v) +let is_constant v = match v with [] | [{var = 0}] -> true | _ -> false +let get_cst vect = match vect with {var = 0; coe = v} :: _ -> v | _ -> Q.zero + +let choose v = + match v with [] -> None | {var = vr; coe = vl} :: rst -> Some (vr, vl, rst) + +let rec fresh v = + match v with [] -> 1 | [{var = v}] -> v + 1 | _ :: v -> fresh v + +let variables v = + List.fold_left (fun acc {var = x} -> ISet.add x acc) ISet.empty v + +let decomp_cst v = + match v with {var = 0; coe = vl} :: v -> (vl, v) | _ -> (Q.zero, v) let rec decomp_at i v = match v with | [] -> (Q.zero, null) - | (vr, vl) :: r -> - if i = vr then (vl, r) else if i < vr then (Q.zero, v) else decomp_at i r + | {var = vr; coe = vl} :: r -> + if Int.equal i vr then (vl, r) + else if i < vr then (Q.zero, v) + else decomp_at i r -let decomp_fst v = match v with [] -> ((0, Q.zero), []) | x :: v -> (x, v) +let decomp_fst v = + match v with [] -> ((0, Q.zero), []) | x :: v -> ((x.var, x.coe), v) let rec subst (vr : int) (e : t) (v : t) = match v with | [] -> [] - | (x, n) :: v' -> ( + | {var = x; coe = n} :: v' -> ( match Int.compare vr x with | 0 -> mul_add n e Q.one v' | -1 -> v - | 1 -> add [(x, n)] (subst vr e v') + | 1 -> add [{var = x; coe = n}] (subst vr e v') | _ -> assert false ) -let fold f acc v = List.fold_left (fun acc (v, i) -> f acc v i) acc v +let fold f acc v = List.fold_left (fun acc x -> f acc x.var x.coe) acc v let fold_error f acc v = let rec fold acc v = match v with | [] -> Some acc - | (x, i) :: v' -> ( + | {var = x; coe = i} :: v' -> ( match f acc x i with None -> None | Some acc' -> fold acc' v' ) in fold acc v @@ -217,11 +235,12 @@ let fold_error f acc v = let rec find p v = match v with | [] -> None - | (v, n) :: v' -> ( match p v n with None -> find p v' | Some r -> Some r ) + | {var = v; coe = n} :: v' -> ( + match p v n with None -> find p v' | Some r -> Some r ) -let for_all p l = List.for_all (fun (v, n) -> p v n) l -let decr_var i v = List.map (fun (v, n) -> (v - i, n)) v -let incr_var i v = List.map (fun (v, n) -> (v + i, n)) v +let for_all p l = List.for_all (fun {var = v; coe = n} -> p v n) l +let decr_var i v = List.map (fun x -> {x with var = x.var - i}) v +let incr_var i v = List.map (fun x -> {x with var = x.var + i}) v let gcd v = let res = @@ -239,12 +258,15 @@ let normalise v = let gcd = fold (fun c _ n -> Z.gcd c (Q.num n)) Z.zero v in if Int.equal (Z.compare gcd Z.zero) 0 then Z.one else gcd in - List.map (fun (x, v) -> (x, v */ Q.of_bigint ppcm // Q.of_bigint gcd)) v + List.map + (fun {var = x; coe = v} -> + {var = x; coe = v */ Q.of_bigint ppcm // Q.of_bigint gcd}) + v let rec exists2 p vect1 vect2 = match (vect1, vect2) with | _, [] | [], _ -> None - | (v1, n1) :: vect1', (v2, n2) :: vect2' -> + | {var = v1; coe = n1} :: vect1', {var = v2; coe = n2} :: vect2' -> if Int.equal v1 v2 then if p n1 n2 then Some (v1, n1, n2) else exists2 p vect1' vect2' else if v1 < v2 then exists2 p vect1' vect2 @@ -254,26 +276,26 @@ let dotproduct v1 v2 = let rec dot acc v1 v2 = match (v1, v2) with | [], _ | _, [] -> acc - | (x1, n1) :: v1', (x2, n2) :: v2' -> - if x1 == x2 then dot (acc +/ (n1 */ n2)) v1' v2' + | {var = x1; coe = n1} :: v1', {var = x2; coe = n2} :: v2' -> + if Int.equal x1 x2 then dot (acc +/ (n1 */ n2)) v1' v2' else if x1 < x2 then dot acc v1' v2 else dot acc v1 v2' in dot Q.zero v1 v2 -let map f v = List.map (fun (x, v) -> f x v) v +let map f v = List.map (fun {var = x; coe = v} -> f x v) v let abs_min_elt v = match v with | [] -> None - | (v, vl) :: r -> + | {var = v; coe = vl} :: r -> Some (List.fold_left - (fun (v1, vl1) (v2, vl2) -> + (fun (v1, vl1) {var = v2; coe = vl2} -> if Q.abs vl1 </ Q.abs vl2 then (v1, vl1) else (v2, vl2)) (v, vl) r) -let partition p = List.partition (fun (vr, vl) -> p vr vl) +let partition p = List.partition (fun {var = vr; coe = vl} -> p vr vl) let mkvar x = set x Q.one null module Bound = struct @@ -281,7 +303,9 @@ module Bound = struct let of_vect (v : vector) = match v with - | [(x, v)] -> if x = 0 then None else Some {cst = Q.zero; var = x; coeff = v} - | [(0, v); (x, v')] -> Some {cst = v; var = x; coeff = v'} + | [{var = x; coe = v}] -> + if Int.equal x 0 then None else Some {cst = Q.zero; var = x; coeff = v} + | [{var = 0; coe = v}; {var = x; coe = v'}] -> + Some {cst = v; var = x; coeff = v'} | _ -> None end diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c92c9a75a0..b5d81f762a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -530,22 +530,25 @@ let change_sort_arity sort = corresponding eta-expanded term *) let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in - let rec drec np elim = + let rec drec ctx np elim = match kind elim with | Prod (n,t,c) -> + let ctx = LocalAssum (n, t) :: ctx in if Int.equal np 0 then let osort, t' = change_sort_arity sort t in evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort; mkProd (n, t', c), - mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) + mkLambda (n, t', mkApp(term, Context.Rel.to_extended_vect mkRel 0 ctx)) else - let c',term' = drec (np-1) c in + let c',term' = drec ctx (np-1) c in mkProd (n, t, c'), mkLambda (n, t, term') - | LetIn (n,b,t,c) -> let c',term' = drec np c in - mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') + | LetIn (n,b,t,c) -> + let ctx = LocalDef (n, b, t) :: ctx in + let c',term' = drec ctx np c in + mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in - let ty, term = drec npars ty in + let ty, term = drec [] npars ty in !evdref, ty, term (**********************************************************************) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4bab3bd6ea..ded159e484 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -187,7 +187,7 @@ let interp_sort_info ?loc evd l = in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l -type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option type inference_flags = { use_typeclasses : bool; @@ -247,17 +247,16 @@ let apply_typeclasses ~program_mode env sigma frozen fail_evar = else sigma in sigma -let apply_inference_hook hook env sigma frozen = match frozen with +let apply_inference_hook (hook : inference_hook) env sigma frozen = match frozen with | FrozenId _ -> sigma | FrozenProgress (lazy (_, pending)) -> Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then - try - let sigma, c = hook env sigma evk in + match hook env sigma evk with + | Some (sigma, c) -> Evd.define evk c sigma - with Exit -> - sigma + | None -> sigma else sigma) pending sigma diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 700ca93c33..abbb745161 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -44,8 +44,6 @@ type typing_constraint = | OfType of types (** A term of the expected type *) | WithoutTypeConstraint (** A term of unknown expected type *) -type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr - type inference_flags = { use_typeclasses : bool; solve_unification_constraints : bool; @@ -103,13 +101,17 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context +(** [hook env sigma ev] returns [Some (sigma', term)] if [ev] can be + instantiated with a solution, [None] otherwise. Used to extend + [solve_remaining_evars] below. *) +type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option + (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) (* For simplicity, it is assumed that current map has no other evars with candidate and no other conversion problems that the one in [pending], however, it can contain more evars than the pending ones. *) - val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map diff --git a/stm/stm.ml b/stm/stm.ml index 73356c42f1..62556d38ff 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 15e839c612..567acb1c73 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -130,7 +130,7 @@ let classify_vernac e = | VernacPrimitive (id,_,_) -> VtSideff ([id.CAst.v], VtLater) | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) - | VernacInductive (_, _,_,l) -> + | VernacInductive (_,l) -> let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 9b0a323078..e85d94cd72 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -91,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context sigma in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it diff --git a/tactics/declare.ml b/tactics/declare.ml index de3c731d9b..5e6f78be6f 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -351,11 +351,11 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let inline_private_constants ~univs env ce = +let inline_private_constants ~uctx env ce = let body, eff = Future.force ce.proof_entry_body in let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in - cb, univs + let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in + cb, uctx (** Declaration of section variables and local definitions *) type variable_declaration = @@ -382,13 +382,13 @@ 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 ((body, uctx), eff) = Future.force de.proof_entry_body in + let ((body, body_ui), eff) = Future.force de.proof_entry_body in let () = export_side_effects eff in - let poly, univs = match de.proof_entry_universes with + let poly, entry_ui = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in - let univs = Univ.ContextSet.union uctx univs in + let univs = Univ.ContextSet.union body_ui entry_ui in (* We must declare the universe constraints before type-checking the term. *) let () = declare_universe_context ~poly univs in diff --git a/tactics/declare.mli b/tactics/declare.mli index f87d08fc8b..0068b9842a 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -108,11 +108,11 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects -(** [inline_private_constants ~sideff ~univs env ce] will inline the +(** [inline_private_constants ~sideff ~uctx env ce] will inline the constants in [ce]'s body and return the body plus the updated [UState.t]. *) val inline_private_constants - : univs:UState.t + : uctx:UState.t -> Environ.env -> Evd.side_effects proof_entry -> Constr.t * UState.t diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 438892e75e..b228a04298 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -116,31 +116,31 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac = - let evd = Evd.from_ctx ctx in +let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac = + let evd = Evd.from_ctx uctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> - entry, status, universes + entry, status, uctx | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") -let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = +let build_by_tactic ?(side_eff=true) env ~uctx ~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 cb, univs = - if side_eff then Declare.inline_private_constants ~univs env ce + let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in + let cb, uctx = + if side_eff then Declare.inline_private_constants ~uctx env ce else (* GG: side effects won't get reset: no need to treat their universes specially *) let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in - cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx + cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx in - cb, status, univs + cb, ce.Declare.proof_entry_type, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = (* Save the initial side-effects to restore them afterwards. We set the diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 3cf3a13262..c49e997757 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -64,8 +64,8 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : name:Id.t -> ?opaque:Proof_global.opacity_flag - -> UState.t - -> named_context_val + -> uctx:UState.t + -> sign:named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic @@ -74,11 +74,11 @@ val build_constant_by_tactic val build_by_tactic : ?side_eff:bool -> env - -> UState.t + -> uctx:UState.t -> poly:bool - -> EConstr.types + -> typ:EConstr.types -> unit Proofview.tactic - -> constr * bool * UState.t + -> constr * types option * bool * UState.t val refine_by_tactic : name:Id.t diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 7d59a18494..7fd1634dcf 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -27,8 +27,7 @@ module NamedDecl = Context.Named.Declaration type proof_object = { name : Names.Id.t ; entries : Evd.side_effects Declare.proof_entry list - ; poly : bool - ; universes: UState.t + ; uctx: UState.t ; udecl : UState.universe_decl } @@ -159,7 +158,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx in let fpl, univs = Future.split2 fpl in - let universes = if poly || now then Future.force univs else initial_euctx in + let uctx = if poly || now then Future.force univs else initial_euctx in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -167,7 +166,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let { Proof.sigma } = Proof.data proof in Evd.existential_opt_value0 sigma k in let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst universes) in + (UState.subst uctx) in let make_body = if poly || now then @@ -182,7 +181,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Vars.universes_of_constr typ in if allow_deferred then let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables universes in + let ctx = constrain_variables uctx in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) @@ -192,7 +191,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (initunivs, typ), ((body, univs), eff) else if poly && opaque && private_poly_univs () then let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict universes used_univs in + let universes = UState.restrict uctx used_univs in let typus = UState.restrict universes used_univs_typ in let udecl = UState.check_univ_decl ~poly typus udecl in let ubody = Univ.ContextSet.diff @@ -207,7 +206,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now the actually used universes. TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict universes used_univs in + let ctx = UState.restrict uctx used_univs in let univs = UState.check_univ_decl ~poly ctx udecl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in @@ -215,7 +214,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now else fun t p -> (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = UState.univ_entry ~poly:false universes in + let univctx = UState.univ_entry ~poly:false uctx in let t = nf t in Future.from_val (univctx, t), Future.chain p (fun (pt,eff) -> @@ -240,7 +239,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in - { name; entries; poly; universes; udecl } + { name; entries; uctx; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index 8c1bc0def1..f1281d1291 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -33,9 +33,7 @@ type proof_object = (** name of the proof *) ; entries : Evd.side_effects Declare.proof_entry list (** list of the proof terms (in a form suitable for definitions). *) - ; poly : bool - (** polymorphic status *) - ; universes: UState.t + ; uctx: UState.t (** universe state *) ; udecl : UState.universe_decl (** universe declaration *) diff --git a/test-suite/Makefile b/test-suite/Makefile index aca7ab0b28..6696f1431e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -49,7 +49,8 @@ endif endif # exists ../_build export COQLIB -COQFLAGS?= +COQEXTRAFLAGS?= +COQFLAGS?=$(COQEXTRAFLAGS) coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -R prerequisite TestSuite diff --git a/test-suite/bugs/closed/bug_11846.v b/test-suite/bugs/closed/bug_11846.v new file mode 100644 index 0000000000..53517e7703 --- /dev/null +++ b/test-suite/bugs/closed/bug_11846.v @@ -0,0 +1,16 @@ +Require Import FunInd. + +Inductive tree : Type := +| Node : unit -> tree. + +Definition height (s : tree) : unit := +match s with +| Node h => h +end. + +Definition bal : forall l, let h := height l in tree := fun l => + let h := height l in + Node h. + +Set Warnings "+all". +Functional Scheme bal_ind := Induction for bal Sort Prop. diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 8f9ab9a711..3ffe831b3c 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash -NATIVECOMP=$(grep "let no_native_compiler = false" ../../../config/coq_config.ml)||true -if [[ $(which ocamlopt) && $NATIVECOMP ]]; then +NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then . ../template/init.sh diff --git a/test-suite/coq-makefile/native2/_CoqProject b/test-suite/coq-makefile/native2/_CoqProject new file mode 100644 index 0000000000..61136e82f0 --- /dev/null +++ b/test-suite/coq-makefile/native2/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.mlg +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh new file mode 100755 index 0000000000..857f70fdff --- /dev/null +++ b/test-suite/coq-makefile/native2/run.sh @@ -0,0 +1,33 @@ +#!/usr/bin/env bash + +NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +COQEXTRAFLAGS="-native-compiler yes" make +make html mlihtml +make install DSTROOT="$PWD/tmp" +#make debug +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual +sort > desired <<EOT +. +./test +./test/test.glob +./test/test_plugin.cmi +./test/test_plugin.cmx +./test/test_plugin.cmxa +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs +EOT +exec diff -u desired actual + +fi +exit 0 # test skipped diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index 4717759dec..b403fc120c 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -36,3 +36,10 @@ Check M.zed@{_}. Fail Check zed. Check M.kats@{_}. Fail Check kats. + +Export Set Foo. + +#[ export ] Set Foo. + +Fail #[ export ] Export Foo. +(* Attribute for Locality specified twice *) diff --git a/theories/micromega/ZifyPow.v b/theories/micromega/ZifyPow.v new file mode 100644 index 0000000000..d208696c0f --- /dev/null +++ b/theories/micromega/ZifyPow.v @@ -0,0 +1 @@ +Require Export ZifyInst. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index d0d6b8b0a3..a7a9b77b56 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -92,6 +92,41 @@ let create_empty_file filename = let f = open_out filename in close_out f +let interp_set_option opt v old = + let open Goptions in + let err expect = + let opt = String.concat " " opt in + let got = v in (* avoid colliding with Pp.v *) + CErrors.user_err + Pp.(str "-set: " ++ str opt ++ + str" expects " ++ str expect ++ + str" but got " ++ str got) + in + match old with + | BoolValue _ -> + let v = match String.trim v with + | "true" -> true + | "false" | "" -> false + | _ -> err "a boolean" + in + BoolValue v + | IntValue _ -> + let v = String.trim v in + let v = match int_of_string_opt v with + | Some _ as v -> v + | None -> if v = "" then None else err "an int" + in + IntValue v + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) + +let set_option = let open Goptions in function + | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt + | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v + +let set_options = List.iter set_option + (* Compile a vernac file *) let compile opts copts ~echo ~f_in ~f_out = let open Vernac.State in @@ -134,6 +169,7 @@ let compile opts copts ~echo ~f_in ~f_out = } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in + set_options opts.config.set_options; let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_out) @@ -187,6 +223,7 @@ let compile opts copts ~echo ~f_in ~f_out = let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in + set_options opts.config.set_options; let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in let doc = Stm.finish ~doc:state.doc in diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 8c154488d0..eb66dbaafc 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -17,3 +17,5 @@ val compile_files : Coqargs.t -> Coqcargs.t -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> unit + +val set_options : (Goptions.option_name * Coqargs.option_command) list -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8d9b9411dd..a63cff3e6f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -46,41 +46,6 @@ let print_memory_stat () = close_out oc with _ -> () -let interp_set_option opt v old = - let open Goptions in - let err expect = - let opt = String.concat " " opt in - let got = v in (* avoid colliding with Pp.v *) - CErrors.user_err - Pp.(str "-set: " ++ str opt ++ - str" expects " ++ str expect ++ - str" but got " ++ str got) - in - match old with - | BoolValue _ -> - let v = match String.trim v with - | "true" -> true - | "false" | "" -> false - | _ -> err "a boolean" - in - BoolValue v - | IntValue _ -> - let v = String.trim v in - let v = match int_of_string_opt v with - | Some _ as v -> v - | None -> if v = "" then None else err "an int" - in - IntValue v - | StringValue _ -> StringValue v - | StringOptValue _ -> StringOptValue (Some v) - -let set_option = let open Goptions in function - | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt - | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true - | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v - -let set_options = List.iter set_option - (******************************************************************************) (* Input/Output State *) (******************************************************************************) @@ -236,8 +201,6 @@ let init_execution opts custom_init = Global.set_allow_sprop opts.config.logic.allow_sprop; if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative (); - set_options opts.config.set_options; - (* Native output dir *) Nativelib.output_dir := opts.config.native_output_dir; Nativelib.include_dirs := opts.config.native_include_dirs; @@ -311,6 +274,7 @@ type run_mode = Interactive | Batch let init_toploop opts = let state = init_document opts in let state = Ccompile.load_init_vernaculars opts ~state in + Ccompile.set_options opts.config.set_options; state let coqtop_init run_mode ~opts = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8fc1e03589..e69b21a195 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -41,7 +41,7 @@ let print_usage_common co command = \n -l f (idem)\ \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ \n -lv f (idem)\ -\n -load-vernac-object lib, -r lib\ +\n -load-vernac-object lib\ \n load Coq library lib (Require lib)\ \n -rfrom root lib load Coq library lib (From root Require lib.)\ \n -require-import lib, -ri lib\ diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9ed371bcfb..0c9b9c7255 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -691,10 +691,10 @@ 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 ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = 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 + let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -821,10 +821,10 @@ 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 ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = 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 + let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -997,13 +997,13 @@ 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 ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = 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 - let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx - (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) - (compute_dec_tact ind lnamesparrec nparrec) + let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx + ~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) + (compute_dec_tact ind lnamesparrec nparrec) in ([|ans|], ctx), Evd.empty_side_effects diff --git a/vernac/classes.ml b/vernac/classes.ml index b1f7b2a0c3..dafd1cc5e4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -312,29 +312,29 @@ let instance_hook info global imps ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook name decl poly sigma term termtype = +let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition - ~allow_evars:false ~poly sigma decl ~types:(Some termtype) ~body:term in + ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (GlobRef.ConstRef kn) -let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = +let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in + let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global imps (GlobRef.ConstRef cst) + instance_hook pri global impargs (GlobRef.ConstRef cst) -let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false dref imps; @@ -345,10 +345,10 @@ let declare_instance_program env sigma ~global ~poly name pri imps univdecl term in let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in - let ctx = Evd.evar_universe_context sigma in + let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~univdecl ~scope ~poly ~kind ~hook typ ctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8eff26bae5..dc9c8e2d3c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -204,7 +204,7 @@ let context_insection sigma ~poly ctx = in let entry = Declare.definition_entry ~univs ~types:t b in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry [] + ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry in () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 8a0d0c9d81..ba2c1ac115 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -70,7 +70,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode - ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in + ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in (ce, evd, udecl, imps) @@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = - let (ce, evd, univdecl, imps as def) = - interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt +let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let (ce, evd, udecl, impargs as def) = + interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in if program_mode then let env = Global.env () in @@ -97,12 +97,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o let obls, _, c, cty = Obligations.eterm_obligations env name evd 0 c typ in - let ctx = Evd.evar_universe_context evd in + let uctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition - ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) + ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls) else let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in let kind = Decls.IsDefinition kind in - ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) + ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 8c050b800a..0a70954dd2 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -9,22 +9,9 @@ (************************************************************************) open Pp -open CErrors open Util -open Constr -open Context -open Vars -open Termops -open Declare open Names -open Constrexpr -open Constrexpr_ops open Constrintern -open Pretyping -open Evarutil -open Evarconv - -module RelDecl = Context.Rel.Declaration (* 3c| Fixpoints and co-fixpoints *) @@ -99,7 +86,7 @@ let check_mutuality env evd isfix fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) -> - (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names)) + (id, List.filter (fun id' -> not (Id.equal id id') && Termops.occur_var env evd id' def) names)) fixl in let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with @@ -110,13 +97,13 @@ let check_mutuality env evd isfix fixl = let interp_fix_context ~program_mode ~cofix env sigma fix = let before, after = if not cofix - then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order + then Constrexpr_ops.split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order else [], fix.Vernacexpr.binders in let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in - let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in + let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl ~program_mode sigma impls (env,_) fix = @@ -134,8 +121,8 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx let prepare_recursive_declaration fixnames fixrs fixtypes fixdefs = - let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in - let names = List.map2 (fun id r -> make_annot (Name id) r) fixnames fixrs in + let defs = List.map (Vars.subst_vars (List.rev fixnames)) fixdefs in + let names = List.map2 (fun id r -> Context.make_annot (Name id) r) fixnames fixrs in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) (* Jump over let-bindings. *) @@ -154,7 +141,7 @@ let compute_possible_guardness_evidences (ctx,_,recindex) = List.interval 0 (Context.Rel.nhyps ctx - 1) type recursive_preentry = - Id.t list * Sorts.relevance list * constr option list * types list + Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list (* Wellfounded definition *) @@ -177,9 +164,9 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis let open UState in let lsu = ls.univdecl_instance and usu = us.univdecl_instance in if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then - user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); + CErrors.user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let sigma, decl = interp_univ_decl_opt env all_universes in + let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in @@ -188,7 +175,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis on_snd List.split3 @@ List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in + let fixtypes = List.map (fun c -> Evarutil.nf_evar sigma c) fixtypes in let fiximps = List.map3 (fun ctximps cclimps (_,ctx) -> ctximps@cclimps) fixctximps fixcclimps fixctxs in @@ -204,8 +191,8 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in - sigma, LocalAssum (make_annot id Sorts.Relevant,fixprot) :: env' - else sigma, LocalAssum (make_annot id Sorts.Relevant,t) :: env') + sigma, LocalAssum (Context.make_annot id Sorts.Relevant,fixprot) :: env' + else sigma, LocalAssum (Context.make_annot id Sorts.Relevant,t) :: env') (sigma,[]) fixnames fixtypes in let env_rec = push_named_context rec_sign env in @@ -224,7 +211,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis () in (* Instantiate evars and check all are resolved *) - let sigma = solve_unif_constraints_with_heuristics env_rec sigma in + let sigma = Evarconv.solve_unif_constraints_with_heuristics env_rec sigma in let sigma = Evd.minimize_universes sigma in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in @@ -238,7 +225,7 @@ let check_recursive isfix env evd (fixnames,_,fixdefs,_) = end let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = - check_evars_are_solved ~program_mode:false env evd; + Pretyping.check_evars_are_solved ~program_mode:false env evd; let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) @@ -257,14 +244,13 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let thms = List.map3 (fun name typ (ctx,impargs,_) -> { Lemmas.Recthm.name; typ - ; args = List.map RelDecl.get_name ctx; impargs}) + ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) fixnames fixtypes fiximps in - let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in + let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl - evd (Some(cofix,indexes,init_tac)) thms None in + evd (Some(cofix,indexes,init_terms)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma @@ -281,12 +267,12 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let vars, fixdecls, gidx = if not cofix then let env = Global.env() in - let indexes = search_guard env indexes fixdecls in - let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in - let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + let indexes = Pretyping.search_guard env indexes fixdecls in + let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in + let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in vars, fixdecls, Some indexes else (* cofix *) - let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in let vars = Vars.universes_of_constr (List.hd fixdecls) in vars, fixdecls, None in @@ -294,29 +280,33 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let ctx = Evd.check_univ_decl ~poly evd pl in - let udecl = Evd.universe_binders evd in + let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - List.map4 (fun name body types imps -> + List.map4 (fun name body types impargs -> let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in - DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps) + DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce) fixnames fixdecls fixtypes fiximps in - recursive_message (not cofix) gidx fixnames; + Declare.recursive_message (not cofix) gidx fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () -let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with +let extract_decreasing_argument ~structonly { CAst.v = v; _ } = + let open Constrexpr in + match v with | CStructRec na -> na | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na | CMeasureRec (None,_,_) when not structonly -> - user_err Pp.(str "Decreasing argument must be specified in measure clause.") - | _ -> user_err Pp.(str - "Well-founded induction requires Program Fixpoint or Function.") + CErrors.user_err Pp.(str "Decreasing argument must be specified in measure clause.") + | _ -> + CErrors.user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") (* This is a special case: if there's only one binder, we pick it as the recursive argument if none is provided. *) let adjust_rec_order ~structonly binders rec_order = - let rec_order = Option.map (fun rec_order -> match binders, rec_order with + let rec_order = Option.map (fun rec_order -> + let open Constrexpr in + match binders, rec_order with | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4f9c247b71..3bac0419ef 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -115,7 +115,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in - let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in + let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in @@ -234,7 +234,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.check_univ_decl ~poly sigma decl in + let univs = Evd.check_univ_decl ~poly sigma udecl in (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in (* FIXME: include locality *) @@ -258,9 +258,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname sigma 0 def typ in - let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl - ~poly evars_typ ctx evars ~hook) + let uctx = Evd.evar_universe_context sigma in + ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl + ~poly evars_typ ~uctx evars ~hook) let out_def = function | Some def -> def @@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty = let do_program_recursive ~scope ~poly fixkind fixl = let cofix = fixkind = DeclareObl.IsCoFixpoint in - let (env, rec_sign, pl, evd), fix, info = + let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl in (* Program-specific code *) @@ -311,13 +311,13 @@ let do_program_recursive ~scope ~poly fixkind fixl = ((indexes,i),fixdecls)) fixl end in - let ctx = Evd.evar_universe_context evd in + let uctx = Evd.evar_universe_context evd in let kind = match fixkind with | DeclareObl.IsFixpoint _ -> Decls.Fixpoint | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in - Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind + Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index a032ebf3f9..09582f4ef2 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,7 +43,7 @@ module Hook = struct end (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = +let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = let fix_exn = Declare.Internal.get_fix_exn ce in let should_suggest = ce.Declare.proof_entry_opaque && Option.is_empty ce.Declare.proof_entry_secctx in @@ -56,10 +56,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in let gr = Names.GlobRef.ConstRef kn in if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; - let () = DeclareUniv.declare_univ_binders gr udecl in + let () = DeclareUniv.declare_univ_binders gr ubind in gr in - let () = maybe_declare_manual_implicits false dref imps in + let () = maybe_declare_manual_implicits false dref impargs in let () = definition_message name in begin match hook_data with @@ -95,7 +95,7 @@ let check_definition_evars ~allow_evars sigma = let env = Global.env () in if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma -let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body = +let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma = check_definition_evars ~allow_evars sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) sigma (fun nf -> nf body, Option.map nf types) @@ -103,10 +103,10 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~bo let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, definition_entry ?opaque ?inline ?types ~univs body -let prepare_parameter ~allow_evars ~poly sigma udecl typ = +let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma = check_definition_evars ~allow_evars sigma; let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) - sigma (fun nf -> nf typ) + sigma (fun nf -> nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, (None(*proof using*), (typ, univs), None(*inline*)) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1ff2145c0d..fb1fc9242c 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -44,9 +44,9 @@ val declare_definition -> scope:locality -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> UnivNames.universe_binders + -> ubind:UnivNames.universe_binders + -> impargs:Impargs.manual_implicits -> Evd.side_effects Declare.proof_entry - -> Impargs.manual_implicits -> GlobRef.t val declare_assumption @@ -64,12 +64,16 @@ val prepare_definition -> ?opaque:bool -> ?inline:bool -> poly:bool - -> Evd.evar_map - -> UState.universe_decl + -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t + -> Evd.evar_map -> 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 -> - Evd.evar_map * Entries.parameter_entry +val prepare_parameter + : allow_evars:bool + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.types + -> Evd.evar_map + -> Evd.evar_map * Entries.parameter_entry diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index a081aa3dae..626dcd5d34 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -18,39 +18,96 @@ open Entries type 'a obligation_body = DefinedObl of 'a | TermObl of constr -type obligation = - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } +module Obligation = struct + type t = + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } -type obligations = obligation array * int + let set_type ~typ obl = { obl with obl_type = typ } + let set_body ~body obl = { obl with obl_body = Some body } + +end + +type obligations = + { obls : Obligation.t array + ; remaining : int } type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint -type program_info = - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : DeclareDef.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option - ; prg_opaque : bool - } +module ProgramDecl = struct + + type t = + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : DeclareDef.locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : DeclareDef.Hook.t option + ; prg_opaque : bool + } + + open Obligation + + let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs + ~poly ~scope ~kind b t deps fixkind notations obls reduce = + let obls', b = + match b with + | None -> + assert(Int.equal (Array.length obls) 0); + let n = Nameops.add_suffix n "_obligation" in + [| { obl_name = n; obl_body = None; + obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; + obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; + obl_tac = None } |], + mkVar n + | Some b -> + Array.mapi + (fun i (n, t, l, o, d, tac) -> + { obl_name = n ; obl_body = None; + obl_location = l; obl_type = t; obl_status = o; + obl_deps = d; obl_tac = tac }) + obls, b + in + let ctx = UState.make_flexible_nonalgebraic uctx in + { prg_name = n + ; prg_body = b + ; prg_type = reduce t + ; prg_ctx = ctx + ; prg_univdecl = udecl + ; prg_obligations = { obls = obls' ; remaining = Array.length obls' } + ; prg_deps = deps + ; prg_fixkind = fixkind + ; prg_notations = notations + ; prg_implicits = impargs + ; prg_poly = poly + ; prg_scope = scope + ; prg_kind = kind + ; prg_reduce = reduce + ; prg_hook = hook + ; prg_opaque = opaque + } + + let set_uctx ~uctx prg = {prg with prg_ctx = uctx} +end + +open Obligation +open ProgramDecl (* Saving an obligation *) @@ -120,16 +177,16 @@ let shrink_body c ty = in (ctx, b', ty', Array.of_list args) +(***********************************************************************) +(* Saving an obligation *) +(***********************************************************************) + let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = let locality = if local then Goptions.OptLocal else Goptions.OptExport in Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) -(***********************************************************************) -(* Saving an obligation *) -(***********************************************************************) - (* true = hide obligations *) let get_hide_obligations = Goptions.declare_bool_option_and_ref @@ -205,7 +262,7 @@ let close sec = ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ str "unsolved obligations" )) -let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj = +let input : ProgramDecl.t CEphemeron.key ProgMap.t -> Libobject.obj = let open Libobject in declare_object { (default_object "Program state") with @@ -232,7 +289,7 @@ let progmap_add n prg = let progmap_replace prg' = Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) -let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 +let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 let obligations_message rem = if rem > 0 then @@ -272,7 +329,7 @@ let rec intset_to = function | n -> Int.Set.add n (intset_to (pred n)) let obligation_substitution expand prg = - let obls, _ = prg.prg_obligations in + let obls = prg.prg_obligations.obls in let ints = intset_to (pred (Array.length obls)) in obl_substitution expand obls ints @@ -348,12 +405,12 @@ let declare_definition prg = in let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in - let ubinders = UState.universe_binders uctx in + let ubind = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in DeclareDef.declare_definition - ~name:prg.prg_name ~scope:prg.prg_scope ubinders + ~name:prg.prg_name ~scope:prg.prg_scope ~ubind ~kind:Decls.(IsDefinition prg.prg_kind) ce - prg.prg_implicits ?hook_data + ~impargs:prg.prg_implicits ?hook_data let rec lam_index n t acc = match Constr.kind t with @@ -429,12 +486,12 @@ let declare_mutual_definition l = let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in - let udecl = UnivNames.empty_binders in + let ubind = UnivNames.empty_binders in let kns = List.map4 - (fun name body types imps -> + (fun name body types impargs -> let ce = Declare.definition_entry ~opaque ~types ~univs body in - DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps) + DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce) fixnames fixdecls fixtypes fiximps in (* Declare notations *) @@ -448,7 +505,8 @@ let declare_mutual_definition l = dref let update_obls prg obls rem = - let prg' = {prg with prg_obligations = (obls, rem)} in + let prg_obligations = { obls; remaining = rem } in + let prg' = {prg with prg_obligations} in progmap_replace prg'; obligations_message rem; if rem > 0 then Remain rem @@ -478,6 +536,17 @@ let dependencies obls n = obls; !res +let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = + let obls = Array.copy obls in + let () = obls.(num) <- obl in + let prg = { prg with prg_ctx = uctx } in + let () = ignore (update_obls prg obls (pred rem)) in + if pred rem > 0 then begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some prg.prg_name) deps None) + end + type obligation_qed_info = { name : Id.t ; num : int @@ -489,7 +558,7 @@ let obligation_terminator entries uctx { name; num; auto } = | [entry] -> let env = Global.env () in let ty = entry.Declare.proof_entry_type in - let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in + let body, uctx = Declare.inline_private_constants ~uctx env entry in let sigma = Evd.from_ctx uctx in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) @@ -498,7 +567,7 @@ let obligation_terminator entries uctx { name; num; auto } = let body = EConstr.to_constr sigma (EConstr.of_constr body) in let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in let ctx = Evd.evar_universe_context sigma in - let obls, rem = prg.prg_obligations in + let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let status = match obl.obl_status, entry.Declare.proof_entry_opaque with @@ -516,8 +585,6 @@ let obligation_terminator entries uctx { name; num; auto } = in let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let () = obls.(num) <- obl in let prg_ctx = if prg.prg_poly then (* Polymorphic *) (* We merge the new universes and constraints of the @@ -531,15 +598,38 @@ let obligation_terminator entries uctx { name; num; auto } = if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) else ctx in - let prg = {prg with prg_ctx} in - ignore (update_obls prg obls (pred rem)); - if pred rem > 0 then - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) deps None) + update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto | _ -> CErrors.anomaly Pp.( str "[obligation_terminator] close_proof returned more than one proof \ term") + +(* Similar to the terminator but for interactive paths, as the + terminator is only called in interactive proof mode *) +let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = + let { obls; remaining=rem } = prg.prg_obligations in + let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in + let transparent = evaluable_constant cst (Global.env ()) in + let () = match obl.obl_status with + (true, Evar_kinds.Expand) + | (true, Evar_kinds.Define true) -> + if not transparent then err_not_transp () + | _ -> () + in + let inst, ctx' = + 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 ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let ctx' = UState.merge_subst ctx (UState.subst ctx') in + Univ.Instance.empty, ctx' + else + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in + Univ.UContext.instance uctx, ctx' + in + let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in + let () = if transparent then add_hint true prg cst in + update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 6e7700a28a..4e20c7c192 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -13,61 +13,101 @@ open Constr type 'a obligation_body = DefinedObl of 'a | TermObl of constr -type obligation = - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } +module Obligation : sig -type obligations = obligation array * int + type t = private + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + + val set_type : typ:Constr.types -> t -> t + val set_body : body:pconstant obligation_body -> t -> t + +end + +type obligations = + { obls : Obligation.t array + ; remaining : int } type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint -type program_info = - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : DeclareDef.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option - ; prg_opaque : bool - } +(* Information about a single [Program {Definition,Lemma,..}] declaration *) +module ProgramDecl : sig + + type t = private + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : DeclareDef.locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : DeclareDef.Hook.t option + ; prg_opaque : bool + } + + val make : + ?opaque:bool + -> ?hook:DeclareDef.Hook.t + -> Names.Id.t + -> udecl:UState.universe_decl + -> uctx:UState.t + -> impargs:Impargs.manual_implicits + -> poly:bool + -> scope:DeclareDef.locality + -> kind:Decls.definition_object_kind + -> Constr.constr option + -> Constr.types + -> Names.Id.t list + -> fixpoint_kind option + -> Vernacexpr.decl_notation list + -> ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array + -> (Constr.constr -> Constr.constr) + -> t + + val set_uctx : uctx:UState.t -> t -> t +end val declare_obligation : - program_info - -> obligation + ProgramDecl.t + -> Obligation.t -> Constr.types -> Constr.types option -> Entries.universes_entry - -> bool * obligation + -> bool * Obligation.t (** [declare_obligation] Save an obligation *) module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set -val declare_definition : program_info -> Names.GlobRef.t +val declare_definition : ProgramDecl.t -> Names.GlobRef.t +(** Resolution status of a program *) type progress = - (* Resolution status of a program *) | Remain of int - (* n obligations remaining *) + (** n obligations remaining *) | Dependent - (* Dependent on other definitions *) + (** Dependent on other definitions *) | Defined of GlobRef.t - (* Defined as id *) + (** Defined as id *) type obligation_qed_info = { name : Id.t @@ -79,32 +119,41 @@ val obligation_terminator : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit -(** [obligation_terminator] part 2 of saving an obligation *) +(** [obligation_terminator] part 2 of saving an obligation, proof mode *) + +val obligation_hook + : ProgramDecl.t + -> Obligation.t + -> Int.t + -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b) + -> DeclareDef.Hook.S.t + -> unit +(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *) val update_obls : - program_info - -> obligation array + ProgramDecl.t + -> Obligation.t array -> int -> progress (** [update_obls prg obls n progress] What does this do? *) (** { 2 Util } *) -val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t +val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t val program_tcc_summary_tag : - program_info CEphemeron.key Id.Map.t Summary.Dyn.tag + ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag val obl_substitution : bool - -> obligation array + -> Obligation.t array -> Int.Set.t -> (ProgMap.key * (Constr.types * Constr.types)) list -val dependencies : obligation array -> int -> Int.Set.t +val dependencies : Obligation.t array -> int -> Int.Set.t val err_not_transp : unit -> unit -val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit +val progmap_add : ProgMap.key -> ProgramDecl.t CEphemeron.key -> unit (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 77423fbadf..dd75693c5b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -107,35 +107,40 @@ GRAMMAR EXTEND Gram | -> { VernacFlagEmpty } ] ] ; - vernac: - [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) } - | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) } - - | v = vernac_poly -> { v } ] - ] + legacy_attr: + [ [ IDENT "Local" -> + { ("local", VernacFlagEmpty) } + | IDENT "Global" -> + { ("global", VernacFlagEmpty) } + | IDENT "Polymorphic" -> + { Attributes.vernac_polymorphic_flag } + | IDENT "Monomorphic" -> + { Attributes.vernac_monomorphic_flag } + | IDENT "Cumulative" -> + { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) } + | IDENT "NonCumulative" -> + { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) } + | IDENT "Private" -> + { ("private", VernacFlagList ["matching", VernacFlagEmpty]) } + | IDENT "Program" -> + { ("program", VernacFlagEmpty) } + ] ] ; - vernac_poly: - [ [ IDENT "Polymorphic"; v = vernac_aux -> - { let (f, v) = v in (Attributes.vernac_polymorphic_flag :: f, v) } - | IDENT "Monomorphic"; v = vernac_aux -> - { let (f, v) = v in (Attributes.vernac_monomorphic_flag :: f, v) } - | v = vernac_aux -> { v } ] - ] + vernac: + [ [ attrs = LIST0 legacy_attr; v = vernac_aux -> { (attrs, v) } ] ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) } - | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) } - | g = gallina; "." -> { ([], g) } - | g = gallina_ext; "." -> { ([], g) } - | c = command; "." -> { ([], c) } - | c = syntax; "." -> { ([], c) } - | c = subprf -> { ([], c) } + [ [ g = gallina; "." -> { g } + | g = gallina_ext; "." -> { g } + | c = command; "." -> { c } + | c = syntax; "." -> { c } + | c = subprf -> { c } ] ] ; vernac_aux: LAST - [ [ prfcom = command_entry -> { ([], prfcom) } ] ] + [ [ prfcom = command_entry -> { prfcom } ] ] ; noedit_mode: [ [ c = query_command -> { c None } ] ] @@ -197,9 +202,8 @@ GRAMMAR EXTEND Gram | IDENT "Let"; id = identref; b = def_body -> { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) } (* Gallina inductive declarations *) - | cum = OPT cumulativity_token; priv = private_token; f = finite_token; - indl = LIST1 inductive_definition SEP "with" -> - { VernacInductive (cum, priv, f, indl) } + | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> + { VernacInductive (f, indl) } | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> { VernacFixpoint (NoDischarge, recs) } | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -341,13 +345,6 @@ GRAMMAR EXTEND Gram | IDENT "Structure" -> { Structure } | IDENT "Class" -> { Class true } ] ] ; - cumulativity_token: - [ [ IDENT "Cumulative" -> { VernacCumulative } - | IDENT "NonCumulative" -> { VernacNonCumulative } ] ] - ; - private_token: - [ [ IDENT "Private" -> { true } | -> { false } ] ] - ; (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index c2cf7a5ec4..7782ff8ac9 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -144,18 +144,22 @@ let rec_tac_initializer finite guard thms snl = let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with - | Some (finite,guard,init_tac) -> + | Some (finite,guard,init_terms) -> let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - | Some tacl -> - Tacticals.New.tclTHENS rec_tac - List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms) - ),guard + let term_tac = + match init_terms with + | None -> + List.map intro_tac thms + | Some init_terms -> + (* This is the case for hybrid proof mode / definition + fixpoint, where terms for some constants are given with := *) + let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in + List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms + in + Tacticals.New.tclTHENS rec_tac term_tac, guard | None -> let () = match thms with [_] -> () | _ -> assert false in - Some (intro_tac (List.hd thms)), [] in + intro_tac (List.hd thms), [] in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") | { Recthm.name; typ; impargs; _}::other_thms -> @@ -170,9 +174,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua } in let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Proof_global.map_proof (fun p -> - match init_tac with - | None -> p - | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma + pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma (************************************************************************) (* Commom constant saving path, for both Qed and Admitted *) @@ -196,10 +198,8 @@ module MutualEntry : sig val declare_mutdef (* Common to all recthms *) : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> poly:bool -> uctx:UState.t -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list - -> udecl:UState.universe_decl (* Only for the first constant, introduced by compat *) -> ubind:UnivNames.universe_binders -> name:Id.t @@ -259,7 +259,7 @@ end = struct Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name ?typ ~impargs ~info mutpe i = + let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name ?typ ~impargs ~info mutpe i = let { Info.hook; compute_guard; scope; kind; _ } = info in match mutpe with | NoBody pe -> @@ -267,7 +267,7 @@ end = struct | Single pe -> (* We'd like to do [assert (i = 0)] here, however this codepath is used when declaring mutual cofixpoints *) - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe | Mutual pe -> (* if typ = None , we don't touch the type; used in the base case *) let pe = @@ -278,19 +278,20 @@ end = struct in let pe = Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name { entry; info } = + let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name { entry; info } = + (* At some point make this a single iteration *) (* At some point make this a single iteration *) (* impargs here are special too, fixed in upcoming PRs *) let impargs = info.Info.impargs in - let r = declare_mutdef ?fix_exn ~poly ~info ~udecl ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in + let r = declare_mutdef ?fix_exn ~info ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in (* Before we used to do this, check if that's right *) let ubind = UnivNames.empty_binders in let rs = List.map_i ( fun i { Recthm.name; typ; impargs } -> - declare_mutdef ?fix_exn ~poly ~udecl ~info ~ubind ?hook_data ~uctx ~name ~typ ~impargs entry i) 1 info.Info.other_thms + declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms in r :: rs end @@ -318,11 +319,11 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~name ~poly ~info ~uctx ~udecl pe = +let finish_admitted ~name ~info ~uctx pe = let mutpe = MutualEntry.variable ~info pe in let ubind = UnivNames.empty_binders in let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~uctx ~poly ~udecl ~ubind ~name mutpe in + MutualEntry.declare_mutdef ~uctx ~ubind ~name mutpe in () let save_lemma_admitted ~(lemma : t) : unit = @@ -338,7 +339,7 @@ let save_lemma_admitted ~(lemma : t) : unit = let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted ~name ~poly ~info:lemma.info ~uctx:universes ~udecl (sec_vars, (typ, ctx), None) + finish_admitted ~name ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None) (************************************************************************) (* Saving a lemma-like constant *) @@ -354,17 +355,17 @@ let finish_proved idopt po info = let open Proof_global in let { Info.hook } = info in match po with - | { name; entries=[const]; universes; udecl; poly } -> + | { name; entries=[const]; uctx; udecl } -> let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in let fix_exn = Declare.Internal.get_fix_exn const in let () = try let mutpe = MutualEntry.adjust_guardness_conditions ~info const in - let hook_data = Option.map (fun hook -> hook, universes, []) hook in - let ubind = UState.universe_binders universes in + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + let ubind = UState.universe_binders uctx in let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~fix_exn ~uctx:universes ~poly ~udecl ?hook_data ~ubind ~name mutpe + MutualEntry.declare_mutdef ~fix_exn ~uctx ?hook_data ~ubind ~name mutpe in () with e when CErrors.noncritical e -> let e = Exninfo.capture e in @@ -437,7 +438,7 @@ let finalize_proof idopt proof_obj proof_info = | Regular -> finish_proved idopt proof_obj proof_info | End_obligation oinfo -> - DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo + DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> @@ -453,7 +454,7 @@ let save_lemma_proved ~lemma ~opaque ~idopt = (***********************************************************************) let save_lemma_admitted_delayed ~proof ~info = let open Proof_global in - let { name; entries; universes; udecl; poly } = proof in + let { name; entries; uctx; udecl } = proof in if List.length entries <> 1 then CErrors.user_err Pp.(str "Admitted does not support multiple statements"); let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in @@ -463,8 +464,8 @@ let save_lemma_admitted_delayed ~proof ~info = let typ = match proof_entry_type with | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); | Some typ -> typ in - let ctx = UState.univ_entry ~poly universes in + let ctx = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~name ~poly ~uctx:universes ~udecl ~info (sec_vars, (typ, ctx), None) + finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None) let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 79fdfe37de..471c955311 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -95,7 +95,7 @@ val start_dependent_lemma type lemma_possible_guards = int list list -(** Pretty much internal, only used in ComFixpoint *) +(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *) val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t -> poly:bool @@ -103,7 +103,7 @@ val start_lemma_with_initialization -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map - -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option + -> (bool * lemma_possible_guards * Constr.t option list option) option -> Recthm.t list -> int list option -> t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index d6ce1036b9..f449cb02f1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -28,7 +28,10 @@ open Util module NamedDecl = Context.Named.Declaration +(* For the records fields, opens should go away one these types are private *) open DeclareObl +open DeclareObl.Obligation +open DeclareObl.ProgramDecl let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -189,8 +192,6 @@ let sort_dependencies evl = | [] -> List.rev list in aux evl Evar.Set.empty [] -open Environ - let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in @@ -284,72 +285,28 @@ let default_tactic = ref (Proofview.tclUNIT ()) let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) let subst_deps expand obls deps t = - let osubst = obl_substitution expand obls deps in + let osubst = DeclareObl.obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in - { obl with obl_type = t' } + Obligation.set_type ~typ:t' obl open Evd -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] - -let add_local_hint prg cst = - Hints.add_hints ~locality:Goptions.OptLocal [Id.to_string prg.prg_name] (unfold_entry cst) - -let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind - notations obls impls ~scope ~poly ~kind reduce = - let obls', b = - match b with - | None -> - assert(Int.equal (Array.length obls) 0); - let n = Nameops.add_suffix n "_obligation" in - [| { obl_name = n; obl_body = None; - obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; - obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; - obl_tac = None } |], - mkVar n - | Some b -> - Array.mapi - (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls, b - in - let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n - ; prg_body = b - ; prg_type = reduce t - ; prg_ctx = ctx - ; prg_univdecl = udecl - ; prg_obligations = (obls', Array.length obls') - ; prg_deps = deps - ; prg_fixkind = fixkind - ; prg_notations = notations - ; prg_implicits = impls - ; prg_poly = poly - ; prg_scope = scope - ; prg_kind = kind - ; prg_reduce = reduce - ; prg_hook = hook - ; prg_opaque = opaque - } - let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; + if (CEphemeron.get v).prg_obligations.remaining > 0 then incr i) m; !i -exception Found of program_info CEphemeron.key +exception Found of ProgramDecl.t CEphemeron.key let map_first m = try ProgMap.iter (fun _ v -> - if snd (CEphemeron.get v).prg_obligations > 0 then - raise (Found v)) m; + if (CEphemeron.get v).prg_obligations.remaining > 0 then + raise (Found v)) m; assert(false) with Found x -> x @@ -416,16 +373,14 @@ let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~catego Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); str "This will become an error in the future"]) -let solve_by_tac ?loc name evi t poly ctx = - (* spiwack: the status is dropped. *) +let solve_by_tac ?loc name evi t poly uctx = try - let (entry,_,ctx') = - Pfedit.build_constant_by_tactic - ~name ~poly ctx evi.evar_hyps evi.evar_concl t in + (* the status is dropped. *) let env = Global.env () in - let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in - Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body); - Some (body, entry.Declare.proof_entry_type, ctx') + let body, types, _, uctx = + Pfedit.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in + Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body); + Some (body, types, uctx) with | Refiner.FailError (_, s) as exn -> let _ = Exninfo.capture exn in @@ -438,43 +393,9 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = - let obls, rem = prg.prg_obligations in - let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in - let transparent = evaluable_constant cst (Global.env ()) in - let () = match obl.obl_status with - (true, Evar_kinds.Expand) - | (true, Evar_kinds.Define true) -> - if not transparent then err_not_transp () - | _ -> () - in - let inst, ctx' = - 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 ~lbound:(Global.universes_lbound ()) (Global.universes ()) in - let ctx' = UState.merge_subst ctx (UState.subst ctx') in - Univ.Instance.empty, ctx' - else - (* We get the right order somehow, but surely it could be enforced in a clearer way. *) - let uctx = UState.context ctx' in - Univ.UContext.instance uctx, ctx' - in - let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in - let () = if transparent then add_local_hint prg cst in - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg = { prg with prg_ctx = ctx' } in - let () = ignore (update_obls prg obls (pred rem)) in - if pred rem > 0 then begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some prg.prg_name) deps None) - end - let rec solve_obligation prg num tac = let user_num = succ num in - let obls, rem = prg.prg_obligations in + let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let remaining = deps_remaining obls obl.obl_deps in let () = @@ -491,7 +412,7 @@ let rec solve_obligation prg num tac = let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in - let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in + let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in @@ -502,7 +423,7 @@ let rec solve_obligation prg num tac = and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in - let obls, rem = prg.prg_obligations in + let { obls; remaining } = prg.prg_obligations in if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with @@ -532,8 +453,9 @@ and solve_obligation_by_tac prg obls i tac = prg.prg_poly (Evd.evar_universe_context evd) with | None -> None | Some (t, ty, ctx) -> + let prg = ProgramDecl.set_uctx ~uctx:ctx prg in + (* Why is uctx not used above? *) let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; if def && not prg.prg_poly then ( @@ -541,13 +463,13 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_env (Global.env ()) in let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in let ctx' = Evd.evar_universe_context evd in - Some {prg with prg_ctx = ctx'}) + Some (ProgramDecl.set_uctx ~uctx:ctx' prg)) else Some prg else None and solve_prg_obligations prg ?oblset tac = - let obls, rem = prg.prg_obligations in - let rem = ref rem in + let { obls; remaining } = prg.prg_obligations in + let rem = ref remaining in let obls' = Array.copy obls in let set = ref Int.Set.empty in let p = match oblset with @@ -555,20 +477,20 @@ and solve_prg_obligations prg ?oblset tac = | Some s -> set := s; (fun i -> Int.Set.mem i !set) in - let prgref = ref prg in - let () = - Array.iteri (fun i x -> + let prg = + Array.fold_left_i (fun i prg x -> if p i then - match solve_obligation_by_tac !prgref obls' i tac with - | None -> () - | Some prg' -> - prgref := prg'; - let deps = dependencies obls i in - (set := Int.Set.union !set deps; - decr rem)) - obls' + match solve_obligation_by_tac prg obls' i tac with + | None -> prg + | Some prg -> + let deps = dependencies obls i in + set := Int.Set.union !set deps; + decr rem; + prg + else prg) + prg obls' in - update_obls !prgref obls' !rem + update_obls prg obls' !rem and solve_obligations n tac = let prg = get_prog_err n in @@ -579,10 +501,10 @@ and solve_all_obligations tac = and try_solve_obligation n prg tac = let prg = get_prog prg in - let obls, rem = prg.prg_obligations in + let {obls; remaining } = prg.prg_obligations in let obls' = Array.copy obls in match solve_obligation_by_tac prg obls' n tac with - | Some prg' -> ignore(update_obls prg' obls' (pred rem)) + | Some prg' -> ignore(update_obls prg' obls' (pred remaining)) | None -> () and try_solve_obligations n tac = @@ -595,9 +517,9 @@ and auto_solve_obligations n ?oblset tac : progress = open Pp let show_obligations_of_prg ?(msg=true) prg = let n = prg.prg_name in - let obls, rem = prg.prg_obligations in + let {obls; remaining} = prg.prg_obligations in let showed = ref 5 in - if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: "); + if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with | None -> @@ -630,12 +552,12 @@ let show_term n = Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env env sigma prg.prg_body) -let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic +let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) + ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let info = Id.print name ++ str " has type-checked" in - let prg = init_prog_info ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in - let obls,_ = prg.prg_obligations in + let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in + let {obls;_} = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); let cst = DeclareObl.declare_definition prg in @@ -649,14 +571,14 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res | _ -> res) -let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic +let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter - (fun (n, b, t, imps, obls) -> - let prg = init_prog_info ~opaque n univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps ~poly ~scope ~kind reduce ?hook + (fun (n, b, t, impargs, obls) -> + let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind) + notations obls ~impargs ~poly ~scope ~kind reduce ?hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> @@ -672,7 +594,7 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic in () let admit_prog prg = - let obls, rem = prg.prg_obligations in + let {obls; remaining} = prg.prg_obligations in let obls = Array.copy obls in Array.iteri (fun i x -> @@ -684,10 +606,10 @@ let admit_prog prg = (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural) in assumption_message x.obl_name; - obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } + obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; - ignore(update_obls prg obls 0) + ignore(DeclareObl.update_obls prg obls 0) let rec admit_all_obligations () = let prg = try Some (get_any_prog ()) with NoObligations _ -> None in @@ -709,7 +631,7 @@ let next_obligation n tac = | None -> get_any_prog_err () | Some _ -> get_prog_err n in - let obls, rem = prg.prg_obligations in + let {obls; remaining} = prg.prg_obligations in let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in let i = match Array.findi is_open obls with | Some i -> i diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 6a2eb1472e..101958072a 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -51,9 +51,9 @@ val default_tactic : unit Proofview.tactic ref val add_definition : name:Names.Id.t -> ?term:constr -> types - -> UState.t - -> ?univdecl:UState.universe_decl (* Universe binders and constraints *) - -> ?implicits:Impargs.manual_implicits + -> uctx:UState.t + -> ?udecl:UState.universe_decl (* Universe binders and constraints *) + -> ?impargs:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality -> ?kind:Decls.definition_object_kind @@ -65,9 +65,10 @@ val add_definition -> DeclareObl.progress val add_mutual_definitions + (* XXX: unify with MutualEntry *) : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list - -> UState.t - -> ?univdecl:UState.universe_decl + -> uctx:UState.t + -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 5808c55cfc..a3de88d4dc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -804,7 +804,7 @@ let string_of_definition_object_kind = let open Decls in function let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (cum, p,f,l) -> + | VernacInductive (f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -830,24 +830,14 @@ let string_of_definition_object_kind = let open Decls in function str" :=") ++ pr_constructor_list lc ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn in - let key = - let kind = - match f with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" - in - if p then - let cm = - match cum with - | Some VernacCumulative -> "Cumulative" - | Some VernacNonCumulative -> "NonCumulative" - | None -> "" - in - cm ^ " " ^ kind - else kind + let kind = + match f with + | Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" in return ( - hov 1 (pr_oneind key (List.hd l)) ++ + hov 1 (pr_oneind kind (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b5ecd62dad..8a4522296f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -473,11 +473,14 @@ let program_inference_hook env sigma ev = let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && Evarutil.is_ground_term sigma concl) - then raise Exit; - let c, _, ctx = - Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac - in Evd.set_universe_context sigma ctx, EConstr.of_constr c - with Logic_monad.TacticFailure e when noncritical e -> + then None + else + let c, _, _, ctx = + Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac + in + Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c) + with + | Logic_monad.TacticFailure e when noncritical e -> user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") @@ -493,15 +496,10 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in let ids = List.map Context.Rel.Declaration.get_name ctx in check_name_freshness scope id; - (* XXX: The nf_evar is critical !! *) - evd, (id.CAst.v, - (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), - (ids, imps @ imps')))) + evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps')))) evd thms in let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in - (* XXX: This nf_evar is critical too!! We are normalizing twice if - you look at the previous lines... *) let thms = List.map (fun (name, (typ, (args, impargs))) -> { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in let () = @@ -604,17 +602,39 @@ let vernac_assumption ~atts discharge kind l nl = let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false - ~key:["Polymorphic"; "Inductive"; "Cumulativity"] - -let should_treat_as_cumulative cum poly = - match cum with - | Some VernacCumulative -> - if poly then true - else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") - | Some VernacNonCumulative -> - if poly then false - else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") - | None -> poly && is_polymorphic_inductive_cumulativity () + ~key:["Polymorphic";"Inductive";"Cumulativity"] + +let polymorphic_cumulative = + let error_poly_context () = + user_err + Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context."); + in + let open Attributes in + let open Notations in + qualify_attribute "universes" + (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" + ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative") + >>= function + | Some poly, Some cum -> + (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive + and #[ universes(polymorphic|monomorphic,cumulative|noncumulative) ] Inductive *) + if poly then return (true, cum) + else error_poly_context () + | Some poly, None -> + (* Case of Polymorphic|Monomorphic Inductive + and #[ universes(polymorphic|monomorphic) ] Inductive *) + if poly then return (true, is_polymorphic_inductive_cumulativity ()) + else return (false, false) + | None, Some cum -> + (* Case of Cumulative|NonCumulative Inductive *) + if is_universe_polymorphism () then return (true, cum) + else error_poly_context () + | None, None -> + (* Case of Inductive *) + if is_universe_polymorphism () then + return (true, is_polymorphic_inductive_cumulativity ()) + else + return (false, false) let get_uniform_inductive_parameters = Goptions.declare_bool_option_and_ref @@ -627,8 +647,7 @@ let should_treat_as_uniform () = then ComInductive.UniformParameters else ComInductive.NonUniformParameters -let vernac_record ~template udecl cum k poly finite records = - let cumulative = should_treat_as_cumulative cum poly in +let vernac_record ~template udecl ~cumulative k ~poly finite records = let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with | None -> Nameops.add_prefix "Build_" id.v @@ -668,12 +687,21 @@ let finite_of_kind = let open Declarations in function | CoInductive -> CoFinite | Variant | Record | Structure | Class _ -> BiFinite -(** When [poly] is true the type is declared polymorphic. When [lo] is true, - then the type is declared private (as per the [Private] keyword). [finite] - indicates whether the type is inductive, co-inductive or - neither. *) -let vernac_inductive ~atts cum lo kind indl = - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in +let private_ind = + let open Attributes in + let open Notations in + attribute_of_list + [ "matching" + , single_key_parser ~name:"Private (matching) inductive type" ~key:"matching" () + ] + |> qualify_attribute "private" + >>= function + | Some () -> return true + | None -> return false + +let vernac_inductive ~atts kind indl = + let (template, (poly, cumulative)), private_ind = Attributes.( + parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then @@ -710,7 +738,7 @@ let vernac_inductive ~atts cum lo kind indl = let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in - vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] + vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) let () = match kind with @@ -735,7 +763,7 @@ let vernac_inductive ~atts cum lo kind indl = in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - vernac_record ~template udecl cum kind poly finite recordl + vernac_record ~template udecl ~cumulative kind ~poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) let () = match kind with @@ -758,9 +786,8 @@ let vernac_inductive ~atts cum lo kind indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let cumulative = should_treat_as_cumulative cum poly in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") @@ -1464,40 +1491,29 @@ let vernac_set_opacity ~local (v,l) = let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] -let get_option_locality export local = - if export then - if Option.is_empty local then OptExport - else user_err Pp.(str "Locality modifiers forbidden with Export") - else match local with - | Some true -> OptLocal - | Some false -> OptGlobal - | None -> OptDefault - -let vernac_set_option0 ~local export key opt = - let locality = get_option_locality export local in +let vernac_set_option0 ~locality key opt = match opt with | OptionUnset -> unset_option_value_gen ~locality key | OptionSetString s -> set_string_option_value_gen ~locality key s | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n) | OptionSetTrue -> set_bool_option_value_gen ~locality key true -let vernac_set_append_option ~local export key s = - let locality = get_option_locality export local in +let vernac_set_append_option ~locality key s = set_string_option_append_value_gen ~locality key s -let vernac_set_option ~local export table v = match v with +let vernac_set_option ~locality table v = match v with | OptionSetString s -> (* We make a special case for warnings because appending is their natural semantics *) if CString.List.equal table ["Warnings"] then - vernac_set_append_option ~local export table s + vernac_set_append_option ~locality table s else let (last, prefix) = List.sep_last table in if String.equal last "Append" && not (List.is_empty prefix) then - vernac_set_append_option ~local export prefix s + vernac_set_append_option ~locality prefix s else - vernac_set_option0 ~local export table v -| _ -> vernac_set_option0 ~local export table v + vernac_set_option0 ~locality table v +| _ -> vernac_set_option0 ~locality table v let vernac_add_option key lv = let f = function @@ -1605,12 +1621,11 @@ let get_nth_goal ~pstate n = let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl -exception NoHyp - (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = + let exception NoHyp in let open Context.Named.Declaration in try (* Fallback early to globals *) @@ -2008,8 +2023,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with vernac_declare_module_type lid bl mtys mtyo) | VernacAssumption ((discharge,kind),nl,l) -> VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl) - | VernacInductive (cum, priv, finite, l) -> - VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) + | VernacInductive (finite, l) -> + VtDefault(fun () -> vernac_inductive ~atts finite l) | VernacFixpoint (discharge, l) -> let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then @@ -2164,9 +2179,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl) | VernacSetStrategy l -> VtDefault(fun () -> with_locality ~atts vernac_set_strategy l) - | VernacSetOption (export, key,v) -> + | VernacSetOption (export,key,v) -> + let atts = if export then ("export", VernacFlagEmpty) :: atts else atts in VtDefault(fun () -> - vernac_set_option ~local:(only_locality atts) export key v) + vernac_set_option ~locality:(parse option_locality atts) key v) | VernacRemoveOption (key,v) -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index efae1b8dfd..b7c6d3c490 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -250,10 +250,6 @@ type register_kind = type module_ast_inl = module_ast * Declaremods.inline type module_binder = bool option * lident list * module_ast_inl -(** [Some b] if locally enabled/disabled according to [b], [None] if - we should use the global flag. *) -type vernac_cumulative = VernacCumulative | VernacNonCumulative - (** {6 The type of vernacular expressions} *) type vernac_one_argument_status = { @@ -312,7 +308,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list + | VernacInductive of inductive_kind * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * fixpoint_expr list | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list @@ -403,7 +399,7 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list - | VernacSetOption of export_flag * Goptions.option_name * option_setting + | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list |