diff options
52 files changed, 1586 insertions, 1619 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f26804e120..4139a0dbe5 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-05-06-V70" + CACHEKEY: "bionic_coq-V2020-05-18-V3" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -366,12 +366,11 @@ pkg:opam: dependencies: [] script: - set -e - - opam pin add --kind=path coq.$COQ_VERSION . - - opam pin add --kind=path coqide-server.$COQ_VERSION . - - opam pin add --kind=path coqide.$COQ_VERSION . + - opam pin add --kind=path coq.dev . + - opam pin add --kind=path coqide-server.dev . + - opam pin add --kind=path coqide.dev . - set +e variables: - COQ_VERSION: "8.13" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci diff --git a/azure-pipelines.yml b/azure-pipelines.yml index e76614a0cf..305c6a627e 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -56,6 +56,7 @@ jobs: MACOSX_DEPLOYMENT_TARGET: '10.11' steps: + - checkout: self fetchDepth: 10 @@ -97,6 +98,7 @@ jobs: - script: | eval $(opam env) + export OCAMLPATH=$(pwd):"$OCAMLPATH" make -j "$NJOBS" test-suite PRINT_LOGS=1 displayName: 'Run Coq Test Suite' diff --git a/clib/cSig.mli b/clib/cSig.mli index ca888f875a..1305be42bd 100644 --- a/clib/cSig.mli +++ b/clib/cSig.mli @@ -83,6 +83,7 @@ sig val min_binding: 'a t -> (key * 'a) val max_binding: 'a t -> (key * 'a) val choose: 'a t -> (key * 'a) + val choose_opt: 'a t -> (key * 'a) option val split: key -> 'a t -> 'a t * 'a option * 'a t val find: key -> 'a t -> 'a val find_opt : key -> 'a t -> 'a option diff --git a/clib/hMap.ml b/clib/hMap.ml index 3baa105fb0..210c48786b 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -356,6 +356,10 @@ struct let (_, m) = Int.Map.choose s in Map.choose m + let choose_opt s = + try Some (choose s) + with Not_found -> None + let find k s = let h = M.hash k in let m = Int.Map.find h s in diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index d5c6096100..801e29ac95 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -179,6 +179,11 @@ but if you wish to save more time you can skip the job by setting This means you will need to change its value when the Docker image needs to be updated. You can do so for a single pipeline by starting -it through the web interface. +it through the web interface. Here is a direct link that you can use +to trigger such a build: +`https://gitlab.com/coq/coq/pipelines/new?var[SKIP_DOCKER]=false&ref=pr-XXXXX`. +Note that this link will give a 404 error if you are not logged in or +a member of the Coq organization on GitLab. To request to join the +Coq organization, go to https://gitlab.com/coq to request access. See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 9ee6496ee5..51a602303a 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-06-V70" +# CACHEKEY: "bionic_coq-V2020-05-18-V3" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -14,12 +14,13 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of stdlib and sphinx doc texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + fonts-freefont-otf \ # Dependencies of source-doc and coq-makefile texlive-science tipa # More dependencies of the sphinx doc -RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ - antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 +RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 # We need to install OPAM 2.0 manually for now. RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh deleted file mode 100644 index c584438b21..0000000000 --- a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then - - quickchick_CI_REF=instance-no-bang - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - -fi diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh deleted file mode 100644 index 8a734feada..0000000000 --- a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then - - quickchick_CI_REF=master+adapting-numTok-new-api-pr11703 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi 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 deleted file mode 100644 index 6928925e54..0000000000 --- a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh +++ /dev/null @@ -1,12 +0,0 @@ -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/ci/user-overlays/11812-ppedrot-export-hint-globality.sh b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh deleted file mode 100644 index 8dae29adb6..0000000000 --- a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11812" ] || [ "$CI_BRANCH" = "export-hint-globality" ]; then - - equations_CI_REF="export-hint-globality" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - fiat_parsers_CI_REF="export-hint-globality" - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat - -fi diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh deleted file mode 100644 index e3a8eb07f3..0000000000 --- a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then - - metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual - metacoq_CI_GITURL=https://github.com/ejgallego/metacoq - - elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh deleted file mode 100644 index 4170799be7..0000000000 --- a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then - - elpi_CI_REF=partial-import - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh deleted file mode 100644 index cd6b408813..0000000000 --- a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh +++ /dev/null @@ -1,24 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then - - coqhammer_CI_REF="evar-inst-list" - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - elpi_CI_REF="evar-inst-list" - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - equations_CI_REF="evar-inst-list" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - metacoq_CI_REF="evar-inst-list" - metacoq_CI_GITURL=https://github.com/ppedrot/metacoq - - mtac2_CI_REF="evar-inst-list" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - - quickchick_CI_REF="evar-inst-list" - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - - unicoq_CI_REF="evar-inst-list" - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - -fi diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh deleted file mode 100644 index 6bee3c7bb6..0000000000 --- a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then - - fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto - - mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - - metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - metacoq_CI_GITURL=https://github.com/herbelin/template-coq - - unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - unimath_CI_GITURL=https://github.com/herbelin/UniMath - -fi diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh deleted file mode 100644 index b5faabcfe1..0000000000 --- a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then - - elpi_CI_REF=no-mod-univs - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh deleted file mode 100644 index 0f8daf418c..0000000000 --- a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then - - equations_CI_REF="refiner-rm-v82" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index af8a4737be..da9f37f666 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -25,7 +25,10 @@ in time. the next branch point with the `--release` flag (see next section). - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the - branch of the previous version. + branch of the previous version. Note that this commit is the first commit + in the first PR merged in master, not the merge commit for that PR. + After tagging double check that `git describe` picks up + the tag you just made (if not, you tagged the wrong commit). - [ ] Create the `X.X+beta1` milestone if it did not already exist. - [ ] Decide the release calendar with the team (freeze date, beta date, final release date) and put this information in the milestone (using the diff --git a/doc/README.md b/doc/README.md index e749bcf5d1..8e1bc85c49 100644 --- a/doc/README.md +++ b/doc/README.md @@ -30,12 +30,12 @@ To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - - sphinx >= 1.8.0 - - sphinx_rtd_theme >= 0.2.5b2 + - sphinx >= 2.3.1 + - sphinx_rtd_theme >= 0.4.3 - beautifulsoup4 >= 4.0.6 - antlr4-python3-runtime >= 4.7.1 - pexpect >= 4.2.1 - - sphinxcontrib-bibtex >= 0.4.0 + - sphinxcontrib-bibtex >= 0.4.2 To install them, you should first install pip and setuptools (for instance, with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: @@ -68,7 +68,7 @@ install them with: Or if you want to use less disk space: apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ - latexmk xindy + latexmk xindy fonts-freefont-otf Compilation ----------- diff --git a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst new file mode 100644 index 0000000000..35a618ea8d --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst @@ -0,0 +1,6 @@ +- **Changed:** + Minimal versions of dependencies for building the reference manual: + now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and + sphinxcontrib-bibtex 0.4.2+ + (`#12224 <https://github.com/coq/coq/pull/12224>`_, + by Jim Fehrle and Théo Zimmermann). diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index e20469bb8b..f91874d74d 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -359,11 +359,14 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de and reference its tokens using ``:token:`…```. ``:gdef:`` Marks the definition of a glossary term inline in the text. Matching :term:`XXX` - constructs will link to it. The term will also appear in the Glossary Index. + constructs will link to it. Use the form :gdef:`text <term>` to display "text" + for the definition of "term", such as when "term" must be capitalized or plural + for grammatical reasons. The term will also appear in the Glossary Index. - Example:: + Examples:: A :gdef:`prime` number is divisible only by itself and 1. + :gdef:`Composite <composite>` numbers are the non-prime numbers. Common mistakes =============== diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 4136b406de..fabf7a519f 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -46,7 +46,7 @@ with open("refman-preamble.rst") as s: # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. -needs_sphinx = '1.8.0' +needs_sphinx = '2.3.1' # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 250a0f0326..68900aa0be 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -267,7 +267,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types Intuitively, types may be viewed as sets containing terms. We say that a type is :gdef:`inhabited` if it contains at least one term (i.e. if we can find a term which is associated with this - type). We call such terms :gdef:`witness`\es. Note that deciding + type). We call such terms :gdef:`witnesses <witness>`. Note that deciding whether a type is inhabited is `undecidable <https://en.wikipedia.org/wiki/Undecidable_problem>`_. diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 8307a02d6d..03581b95dd 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -22,7 +22,7 @@ Sorts | @universe_expr universe_expr ::= @universe_name {? + @num } -The types of types are called :gdef:`sort`\s. +The types of types are called :gdef:`sorts <sort>`. All sorts have a type and there is an infinite well-founded typing hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index df11960403..e59f694aa7 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -27,13 +27,13 @@ from docutils.parsers.rst.roles import code_role #, set_classes from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes -from sphinx.roles import XRefRole -from sphinx.errors import ExtensionError -from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode -from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index -from sphinx.domains.std import token_xrefs +from sphinx.errors import ExtensionError +from sphinx.roles import XRefRole +from sphinx.util.docutils import ReferenceRole +from sphinx.util.logging import getLogger, get_node_location +from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from . import coqdoc from .repl import ansicolors @@ -1162,25 +1162,34 @@ GrammarProductionRole.role_name = "production" def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): """Marks the definition of a glossary term inline in the text. Matching :term:`XXX` - constructs will link to it. The term will also appear in the Glossary Index. + constructs will link to it. Use the form :gdef:`text <term>` to display "text" + for the definition of "term", such as when "term" must be capitalized or plural + for grammatical reasons. The term will also appear in the Glossary Index. - Example:: + Examples:: A :gdef:`prime` number is divisible only by itself and 1. + :gdef:`Composite <composite>` numbers are the non-prime numbers. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env std = env.domaindata['std']['objects'] - key = ('term', text) + m = ReferenceRole.explicit_title_re.match(text) + if m: + (text, term) = m.groups() + text = text.strip() + else: + term = text + key = ('term', term) if key in std: MSG = 'Duplicate object: {}; other is at {}' - msg = MSG.format(text, env.doc2path(std[key][0])) + msg = MSG.format(term, env.doc2path(std[key][0])) inliner.document.reporter.warning(msg, line=lineno) - targetid = nodes.make_id('term-{}'.format(text)) + targetid = nodes.make_id('term-{}'.format(term)) std[key] = (env.docname, targetid) - target = nodes.target('', '', ids=[targetid], names=[text]) + target = nodes.target('', '', ids=[targetid], names=[term]) inliner.document.note_explicit_target(target) node = nodes.inline(rawtext, '', target, nodes.Text(text), classes=['term-defn']) set_role_source_info(inliner, lineno, node) diff --git a/engine/evd.ml b/engine/evd.ml index 5642145f6d..ff13676818 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -697,8 +697,7 @@ let empty = { extras = Store.empty; } -let from_env e = - { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } +let from_env e = { empty with universes = UState.from_env e } let from_ctx ctx = { empty with universes = ctx } @@ -862,9 +861,6 @@ let universe_subst evd = let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'} -let merge_universe_subst evd subst = - {evd with universes = UState.merge_subst evd.universes subst } - let with_context_set ?loc rigid d (a, ctx) = (merge_context_set ?loc rigid d ctx, a) diff --git a/engine/evd.mli b/engine/evd.mli index c6c4a71b22..d9b7bd76e7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -636,7 +636,6 @@ val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map -val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/engine/uState.ml b/engine/uState.ml index 99ac5f2ce8..7c60d8317c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -63,6 +63,8 @@ let make ~lbound u = uctx_universes_lbound = lbound; uctx_initial_universes = u} +let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e) + let is_empty ctx = ContextSet.is_empty ctx.uctx_local && LMap.is_empty ctx.uctx_univ_variables diff --git a/engine/uState.mli b/engine/uState.mli index 533a501b59..45a0f9964e 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -29,6 +29,8 @@ val make : lbound:UGraph.Bound.t -> UGraph.t -> t val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t +val from_env : Environ.env -> t + val is_empty : t -> bool val union : t -> t -> t diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f09b35a6d1..e5665c59b8 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,7 +40,7 @@ let start_deriving f suchthat name : Lemmas.t = TNil sigma)))))) in - let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in + let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in Lemmas.pf_map (Declare.Proof.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p diff --git a/stm/stm.ml b/stm/stm.ml index b296f8f08f..04f08e488b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - DeclareObl.program_tcc_summary_tag + Declare.Obls.State.prg_tag type cached_state = | EmptyState @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + Declare.Obls.State.t type partial_state = [ `Full of Vernacstate.t @@ -1684,7 +1684,9 @@ end = struct (* {{{ *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); - `OK proof + (* Is this name the same than the one in scope? *) + let name = Declare.get_po_name proof in + `OK name end with e -> let (e, info) = Exninfo.capture e in @@ -1723,7 +1725,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK { Declare.name } -> + | `OK name -> let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with @@ -3308,7 +3310,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/test-suite/Makefile b/test-suite/Makefile index afc6080627..5dd4f42af3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -285,8 +285,8 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) # ML files from unit-test framework, not containing tests -UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) -UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) +UNIT_SRCFILES:=$(shell find ./unit-tests/src -name '*.ml') +UNIT_ALLMLFILES:=$(shell find ./unit-tests -name '*.ml') UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) @@ -316,11 +316,6 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test -unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK) - $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \ - -I unit-tests/src $(UNIT_LINK) $< -o $<.test; - $(HIDE)./$<.test ####################################################################### # Other generic tests diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml deleted file mode 100644 index 3082acdf1f..0000000000 --- a/test-suite/unit-tests/ide/lex_tests.ml +++ /dev/null @@ -1,50 +0,0 @@ -open Utest - -let log_out_ch = open_log_out_ch __FILE__ - -let lex s = - let n = - let last = String.length s - 1 in - if s.[last] = '.' then Some last else None in - let stop = ref None in - let f i _ = assert(!stop = None); stop := Some i in - begin try Coq_lex.delimit_sentences f s - with Coq_lex.Unterminated -> () end; - if n <> !stop then begin - let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in - Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop) - end; - n = !stop - -let i2s i = "test at line: " ^ string_of_int i - -let tests = [ - - mk_bool_test (i2s __LINE__) "no quotation" @@ lex - "foo.+1 bar." - ; - mk_bool_test (i2s __LINE__) "quotation" @@ lex - "foo constr:(xxx)." - ; - mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex - "foo constr:(xxx. yyy)." - ; - mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex - "foo constr:((xxx. (foo.+1 ) \")\" yyy))." - ; - mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex - "foo constr:[xxx. (foo.+1 ) \")\" yyy]." - ; - mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex - "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]." - ; - mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex - "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]." - ; - mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex - "bar:{{ foo {{ hello. }} }}." - ; - -] - -let _ = run_tests __FILE__ log_out_ch tests diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index d0b8d21b69..60267cd859 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -76,11 +76,14 @@ let _ = add_test "tokenize_string/diff_mode in lexer" t open Pp +let write_diffs_option s = + Goptions.set_string_option_value Proof_diffs.opt_name s + (* example that was failing from #8922 *) let t () = - Proof_diffs.write_diffs_option "removed"; + write_diffs_option "removed"; ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1"); - Proof_diffs.write_diffs_option "on" + write_diffs_option "on" let _ = add_test "shorten_diff_span failure from #8922" t (* note pp_to_string concatenates adjacent strings, could become one token, @@ -181,7 +184,7 @@ let _ = if false then add_test "diff_pp/add_diff_tags token containing white spa let add_entries map idents rhs_pp = let make_entry() = { idents; rhs_pp; done_ = false } in - List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;; + List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents;; let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps @@ -194,11 +197,11 @@ let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (fl let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["a"]; ["b"]] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["a"] (str " : foo"); add_entries o_hyp_map ["b"] (str " : bar car"); let n_line_idents = [ ["b"]; ["a"]] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["b"] (str " : car"); add_entries n_hyp_map ["a"] (str " : foo bar"); let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ])); @@ -224,11 +227,11 @@ let _ = add_test "diff_hyps simple diffs" t let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["a"]; ["c"; "d"]] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["a"] (str " : nat"); add_entries o_hyp_map ["c"; "d"] (str " : int"); let n_line_idents = [ ["a"; "b"]; ["d"]] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["a"; "b"] (str " : nat"); add_entries n_hyp_map ["d"] (str " : int"); let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ])); @@ -264,12 +267,12 @@ DIFFS let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["a"]; ["b"]; ["c"]] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["a"] (str " : foo"); add_entries o_hyp_map ["b"] (str " : bar"); add_entries o_hyp_map ["c"] (str " : nat"); let n_line_idents = [ ["b"; "a"; "c"] ] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat"); let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))])); flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))])); @@ -302,10 +305,10 @@ DIFFS let t () = write_diffs_option "removed"; (* turn on "removed" option *) let o_line_idents = [ ["b"; "a"; "c"] ] in - let o_hyp_map = ref StringMap.empty in + let o_hyp_map = ref CString.Map.empty in add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat"); let n_line_idents = [ ["a"]; ["b"]; ["c"]] in - let n_hyp_map = ref StringMap.empty in + let n_hyp_map = ref CString.Map.empty in add_entries n_hyp_map ["a"] (str " : foo"); add_entries n_hyp_map ["b"] (str " : bar"); add_entries n_hyp_map ["c"] (str " : nat"); diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 5323c9f1c6..bb640a83f6 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -385,7 +385,7 @@ let build_beq_scheme mode kn = Vars.substl subst cores.(i) in create_input fix), - UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())) + UState.from_env (Global.env ())) let beq_scheme_kind = declare_mutual_scheme_object "_beq" @@ -707,7 +707,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal = compute_bl_goal ind lnamesparrec nparrec in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal @@ -840,7 +840,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal = compute_lb_goal ind lnamesparrec nparrec in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal @@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/classes.ml b/vernac/classes.ml index 55af2e1a7d..21e2afe6a9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -345,7 +345,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in - let _ : DeclareObl.progress = + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 95f3955309..d56917271c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -126,8 +126,8 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in - let _ : DeclareObl.progress = + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls in () diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4e9e24b119..4aa46e0a86 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive ~scope ~poly fixkind fixl = - let cofix = fixkind = DeclareObl.IsCoFixpoint in + let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl in @@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = end in let uctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> Decls.Fixpoint - | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint + | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint + | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind @@ -345,7 +345,7 @@ let do_fixpoint ~scope ~poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let annots = List.map (fun fix -> Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in - let fixkind = DeclareObl.IsFixpoint annots in + let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in do_program_recursive ~scope ~poly fixkind l @@ -355,4 +355,4 @@ let do_fixpoint ~scope ~poly l = let do_cofixpoint ~scope ~poly fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl + do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl diff --git a/vernac/declare.ml b/vernac/declare.ml index c3f95c5297..333b186b22 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -120,7 +120,7 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type import_status = ImportDefaultBehavior | ImportNeedQualified +type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) @@ -155,6 +155,8 @@ type proof_object = ; uctx: UState.t } +let get_po_name { name } = name + let private_poly_univs = Goptions.declare_bool_option_and_ref ~depr:false @@ -847,23 +849,6 @@ let get_current_context pf = let p = get_proof pf in Proof.get_proof_context p -module Proof = struct - type nonrec t = t - let get_proof = get_proof - let get_proof_name = get_proof_name - let get_used_variables = get_used_variables - let get_universe_decl = get_universe_decl - let get_initial_euctx = get_initial_euctx - let map_proof = map_proof - let map_fold_proof = map_fold_proof - let map_fold_proof_endline = map_fold_proof_endline - let set_endline_tactic = set_endline_tactic - let set_used_variables = set_used_variables - let compact = compact_the_proof - let update_global_env = update_global_env - let get_open_goals = get_open_goals -end - let declare_definition_scheme ~internal ~univs ~role ~name c = let kind = Decls.(IsDefinition Scheme) in let entry = pure_definition_entry ~univs c in @@ -876,7 +861,7 @@ let _ = Abstract.declare_abstract := declare_abstract let declare_universe_context = DeclareUctx.declare_universe_context -type locality = Discharge | Global of import_status +type locality = Locality.locality = | Discharge | Global of import_status (* Hooks naturally belong here as they apply to both definitions and lemmas *) module Hook = struct @@ -1022,25 +1007,20 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry -let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = +let prepare_obligation ~name ~types ~body sigma = + let env = Global.env () in + let types = match types with + | Some t -> t + | None -> Retyping.get_type_of env sigma body + in let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false - sigma (fun nf -> nf body, Option.map nf types) + sigma (fun nf -> nf body, nf types) in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let ce = definition_entry ?opaque ?inline ?types ~univs body in - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.proof_entry_body in - assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); RetrieveObl.check_evars env sigma; - let c = EConstr.of_constr c in - let typ = match ce.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env sigma c - in - let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let body, types = EConstr.(of_constr body, of_constr types) in + let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in let uctx = Evd.evar_universe_context sigma in - c, cty, uctx, obls + body, cty, uctx, obls let prepare_parameter ~poly ~udecl ~types sigma = let env = Global.env () in @@ -1053,3 +1033,980 @@ let prepare_parameter ~poly ~udecl ~types sigma = (* Compat: will remove *) exception AlreadyDeclared = DeclareUniv.AlreadyDeclared + +module Obls = struct + +open Constr + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +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 } + + 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 + +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 : locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : 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 *) + +(* XXX: Is this the right place for this? *) +let it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then Term.mkLambda_or_LetIn decl t + else if Vars.noccurn 1 t then Vars.subst1 mkProp t + else Term.mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + +(* XXX: Is this the right place for this? *) +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match (Constr.kind c, Constr.kind ty) with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when Constr.equal b b' && Constr.equal t t' -> + let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in + aux ctx' c ty + | _, LetIn (x', b', t', ty) -> + let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in + aux ctx' (lift 1 c) ty + | LetIn (x, b, t, c), _ -> + let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in + aux ctx' c (lift 1 ty) + | Lambda (x, b, t), Prod (x', b', t') + (* By invariant, must be convertible *) -> + let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in + aux ctx' t t' + | Cast (c, _, _), _ -> aux ctx c ty + | _, _ -> (ctx, c, ty) + in + aux Context.Rel.empty c ty + +(* XXX: What's the relation of this with Abstract.shrink ? *) +let shrink_body c ty = + let ctx, b, ty = + match ty with + | None -> + let ctx, b = Term.decompose_lam_assum c in + (ctx, b, None) + | Some ty -> + let ctx, b, ty = decompose_lam_prod c ty in + (ctx, b, Some ty) + in + let b', ty', n, args = + List.fold_left + (fun (b, ty, i, args) decl -> + if Vars.noccurn 1 b && Option.cata (Vars.noccurn 1) true ty then + (Vars.subst1 mkProp b, Option.map (Vars.subst1 mkProp) ty, succ i, args) + else + let open Context.Rel.Declaration in + let args = if is_local_assum decl then mkRel i :: args else args in + ( Term.mkLambda_or_LetIn decl b + , Option.map (Term.mkProd_or_LetIn decl) ty + , succ i + , args )) + (b, ty, 1, []) ctx + 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) + +(* true = hide obligations *) +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:true + ~key:["Hide"; "Obligations"] + ~value:false + +let declare_obligation prg obl body ty uctx = + let body = prg.prg_reduce body in + let ty = Option.map prg.prg_reduce ty in + match obl.obl_status with + | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) + | force, Evar_kinds.Define opaque -> + let opaque = (not force) && opaque in + let poly = prg.prg_poly in + let ctx, body, ty, args = + if not poly then shrink_body body ty + else ([], body, ty, [||]) + in + let ce = definition_entry ?types:ty ~opaque ~univs:uctx body in + (* ppedrot: seems legit to have obligations as local *) + let constant = + declare_constant ~name:obl.obl_name + ~local:ImportNeedQualified + ~kind:Decls.(IsProof Property) + (DefinitionEntry ce) + in + if not opaque then + add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = + match uctx with + | Entries.Polymorphic_entry (_, uctx) -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Entries.Monomorphic_entry _ -> + Some + (TermObl + (it_mkLambda_or_LetIn_or_clean + (mkApp (mkConst constant, args)) + ctx)) + in + (true, {obl with obl_body = body}) + +(* Updating the obligation meta-info on close *) + +let not_transp_msg = + Pp.( + str "Obligation should be transparent but was declared opaque." + ++ spc () + ++ str "Use 'Defined' instead.") + +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd +let err_not_transp () = pperror not_transp_msg + +module ProgMap = Id.Map + +module StateFunctional = struct + + type t = ProgramDecl.t CEphemeron.key ProgMap.t + + let _empty = ProgMap.empty + + let pending pm = + ProgMap.filter + (fun _ v -> (CEphemeron.get v).prg_obligations.remaining > 0) + pm + + let num_pending pm = pending pm |> ProgMap.cardinal + + let first_pending pm = + pending pm |> ProgMap.choose_opt + |> Option.map (fun (_, v) -> CEphemeron.get v) + + let get_unique_open_prog pm name : (_, Id.t list) result = + match name with + | Some n -> + Option.cata + (fun p -> Ok (CEphemeron.get p)) + (Error []) (ProgMap.find_opt n pm) + | None -> ( + let n = num_pending pm in + match n with + | 0 -> Error [] + | 1 -> Option.cata (fun p -> Ok p) (Error []) (first_pending pm) + | _ -> + let progs = Id.Set.elements (ProgMap.domain pm) in + Error progs ) + + let add t key prg = ProgMap.add key (CEphemeron.create prg) t + + let fold t ~f ~init = + let f k v acc = f k (CEphemeron.get v) acc in + ProgMap.fold f t init + + let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v) + let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get +end + +module State = struct + + type t = StateFunctional.t + + open StateFunctional + + let prg_ref, prg_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" + + let num_pending () = num_pending !prg_ref + let first_pending () = first_pending !prg_ref + let get_unique_open_prog id = get_unique_open_prog !prg_ref id + let add id prg = prg_ref := add !prg_ref id prg + let fold ~f ~init = fold !prg_ref ~f ~init + let all () = all !prg_ref + let find id = find !prg_ref id + +end + +(* In all cases, the use of the map is read-only so we don't expose the ref *) +let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] + +let check_solved_obligations ~what_for : unit = + if not (ProgMap.is_empty !State.prg_ref) then + let keys = map_keys !State.prg_ref in + let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in + CErrors.user_err ~hdr:"Program" + Pp.( + str "Unsolved obligations when closing " + ++ what_for ++ str ":" ++ spc () + ++ prlist_with_sep spc (fun x -> Id.print x) keys + ++ str have_string + ++ str "unsolved obligations" ) + +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) +let progmap_remove pm prg = ProgMap.remove prg.prg_name pm +let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm +let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 + +let obligations_message rem = + Format.asprintf "%s %s remaining" + (if rem > 0 then string_of_int rem else "No more") + (CString.plural rem "obligation") + |> Pp.str |> Flags.if_verbose Feedback.msg_info + +type progress = Remain of int | Dependent | Defined of GlobRef.t + +let get_obligation_body expand obl = + match obl.obl_body with + | None -> None + | Some c -> ( + if expand && snd obl.obl_status == Evar_kinds.Expand then + match c with + | DefinedObl pc -> Some (Environ.constant_value_in (Global.env ()) pc) + | TermObl c -> Some c + else + match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) + +let obl_substitution expand obls deps = + Int.Set.fold + (fun x acc -> + let xobl = obls.(x) in + match get_obligation_body expand xobl with + | None -> acc + | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) + deps [] + +let rec intset_to = function + | -1 -> Int.Set.empty + | n -> Int.Set.add n (intset_to (pred n)) + +let obligation_substitution expand prg = + let obls = prg.prg_obligations.obls in + let ints = intset_to (pred (Array.length obls)) in + obl_substitution expand obls ints + +let hide_obligation () = + Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; + UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref "program.tactics.obligation") + +(* XXX: Is this the right place? *) +let rec prod_app t n = + match + Constr.kind + (EConstr.Unsafe.to_constr + (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) + (* FIXME *) + with + | Prod (_, _, b) -> Vars.subst1 n b + | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n + | _ -> + CErrors.user_err ~hdr:"prod_app" + Pp.(str "Needed a product, but didn't find one" ++ fnl ()) + +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL + +let replace_appvars subst = + let rec aux c = + let f, l = decompose_app c in + if isVar f then + try + let c' = List.map (Constr.map aux) l in + let t, b = Id.List.assoc (destVar f) subst in + mkApp + ( delayed_force hide_obligation + , [|prod_applist t c'; Term.applistc b c'|] ) + with Not_found -> Constr.map aux c + else Constr.map aux c + in + Constr.map aux + +let subst_prog subst prg = + if get_hide_obligations () then + ( replace_appvars subst prg.prg_body + , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) + else + let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in + ( Vars.replace_vars subst' prg.prg_body + , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) + +let stm_get_fix_exn = ref (fun _ x -> x) + +let declare_definition prg = + let varsubst = obligation_substitution true prg in + let sigma = Evd.from_ctx prg.prg_ctx in + let body, types = subst_prog varsubst prg in + let body, types = EConstr.(of_constr body, Some (of_constr types)) in + (* All these should be grouped into a struct a some point *) + let opaque, poly, udecl, hook = + (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook) + in + let name, scope, kind, impargs = + ( prg.prg_name + , prg.prg_scope + , Decls.(IsDefinition prg.prg_kind) + , prg.prg_implicits ) + in + let fix_exn = !stm_get_fix_exn () in + let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in + (* XXX: This is doing normalization twice *) + let kn = + declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + in + let pm = progmap_remove !State.prg_ref prg in + State.prg_ref := pm; + kn + +let rec lam_index n t acc = + match Constr.kind t with + | Lambda ({Context.binder_name = Name n'}, _, _) when Id.equal n n' -> acc + | Lambda (_, _, b) -> lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences n fixbody fixtype = + match n with + | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in + let ctx = fst (Term.decompose_prod_n_assum m fixtype) in + List.map_i (fun i _ -> i) 0 ctx + +let declare_mutual_definition l = + let len = List.length l in + let first = List.hd l in + let defobl x = + let oblsubst = obligation_substitution true x in + let subs, typ = subst_prog oblsubst x in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in + let term = + snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) + in + let typ = + snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) + in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in + let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in + (def, oblsubst) + in + let defs, obls = + List.fold_right + (fun x (defs, obls) -> + let xdef, xobls = defobl x in + (xdef :: defs, xobls @ obls)) + l ([], []) + in + (* let fixdefs = List.map reduce_fix fixdefs in *) + let fixdefs, fixrs, fixtypes, fixitems = + List.fold_right2 + (fun (d, r, typ, impargs) name (a1, a2, a3, a4) -> + ( d :: a1 + , r :: a2 + , typ :: a3 + , Recthm.{name; typ; impargs; args = []} :: a4 )) + defs first.prg_deps ([], [], [], []) + in + let fixkind = Option.get first.prg_fixkind in + let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in + let rvec = Array.of_list fixrs in + let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in + let rec_declaration = (Array.map2 Context.make_annot namevec rvec, arrrec, recvec) in + let possible_indexes = + match fixkind with + | IsFixpoint wfl -> + Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) + | IsCoFixpoint -> None + in + (* In the future we will pack all this in a proper record *) + let poly, scope, ntns, opaque = + (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque) + in + let kind = + if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) + else Decls.(IsDefinition CoFixpoint) + in + (* Declare the recursive definitions *) + let udecl = UState.default_univ_decl in + let kns = + declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns + ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly + ~restrict_ucontext:false fixitems + in + (* Only for the first constant *) + let dref = List.hd kns in + Hook.( + call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref}); + let pm = List.fold_left progmap_remove !State.prg_ref l in + State.prg_ref := pm; + dref + +let update_obls prg obls rem = + let prg_obligations = {obls; remaining = rem} in + let prg' = {prg with prg_obligations} in + let pm = progmap_replace prg' !State.prg_ref in + State.prg_ref := pm; + obligations_message rem; + if rem > 0 then Remain rem + else + match prg'.prg_deps with + | [] -> + let kn = declare_definition prg' in + let pm = progmap_remove !State.prg_ref prg' in + State.prg_ref := pm; + Defined kn + | l -> + let progs = + List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps + in + if List.for_all (fun x -> obligations_solved x) progs then + let kn = declare_mutual_definition progs in + Defined kn + else Dependent + +let dependencies obls n = + let res = ref Int.Set.empty in + Array.iteri + (fun i obl -> + if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then + res := Int.Set.add i !res) + 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 _progress = update_obls prg obls (pred rem) in + let () = + if pred rem > 0 then + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + let _progress = auto (Some prg.prg_name) deps None in + () + else () + else () + in + () + +type obligation_resolver = + Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> progress + +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +let obligation_terminator entries uctx {name; num; auto} = + match entries with + | [entry] -> + let env = Global.env () in + let ty = entry.proof_entry_type in + let body, uctx = 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 *) + let prg = Option.get (State.find name) in + let {obls; remaining = rem} = prg.prg_obligations in + let obl = obls.(num) in + let status = + match (obl.obl_status, entry.proof_entry_opaque) with + | (_, Evar_kinds.Expand), true -> err_not_transp () + | (true, _), true -> err_not_transp () + | (false, _), true -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), false -> Evar_kinds.Define false + | (_, status), false -> status + in + let obl = {obl with obl_status = (false, status)} in + let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in + let defined, obl = declare_obligation prg obl body ty univs in + let prg_ctx = + if prg.prg_poly then + (* Polymorphic *) + (* We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx uctx + else if + (* The first obligation, if defined, + declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + defined + then + UState.from_env (Global.env ()) + else uctx + in + 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 the admitted path; this assumes + the admitted constant was already declared. + + FIXME: There is duplication of this code with obligation_terminator + and Obligations.admit_obligations *) +let obligation_admitted_terminator {name; num; auto} ctx' dref = + let prg = Option.get (State.find name) in + let {obls; remaining = rem} = prg.prg_obligations in + let obl = obls.(num) in + let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in + let transparent = Environ.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.from_env (Global.env ()) 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 + +end + +(************************************************************************) +(* Commom constant saving path, for both Qed and Admitted *) +(************************************************************************) + +(* Support for mutually proved theorems *) + +module Proof_ending = struct + + type t = + | Regular + | End_obligation of Obls.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } + +end + +type lemma_possible_guards = int list list + +module Info = struct + + type t = + { hook : Hook.t option + ; proof_ending : Proof_ending.t CEphemeron.key + (* This could be improved and the CEphemeron removed *) + ; scope : locality + ; kind : Decls.logical_kind + (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) + ; thms : Recthm.t list + ; compute_guard : lemma_possible_guards + } + + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior) + ?(kind=Decls.(IsProof Lemma)) ?(compute_guard=[]) ?(thms=[]) () = + { hook + ; compute_guard + ; proof_ending = CEphemeron.create proof_ending + ; thms + ; scope + ; kind + } + + (* This is used due to a deficiency on the API, should fix *) + let add_first_thm ~info ~name ~typ ~impargs = + let thms = + { Recthm.name + ; impargs + ; typ = EConstr.Unsafe.to_constr typ + ; args = [] } :: info.thms + in + { info with thms } + +end + +(* XXX: this should be unified with the code for non-interactive + mutuals previously on this file. *) +module MutualEntry : sig + + val declare_variable + : info:Info.t + -> uctx:UState.t + -> Entries.parameter_entry + -> Names.GlobRef.t list + + val declare_mutdef + (* Common to all recthms *) + : info:Info.t + -> uctx:UState.t + -> Evd.side_effects proof_entry + -> Names.GlobRef.t list + +end = struct + + (* XXX: Refactor this with the code in [Declare.declare_mutdef] *) + let guess_decreasing env possible_indexes ((body, ctx), eff) = + let open Constr in + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = Pretyping.search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff + + let select_body i t = + let open Constr in + match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | _ -> + CErrors.anomaly + Pp.(str "Not a proof by induction: " ++ + Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") + + let declare_mutdef ~uctx ~info pe i Recthm.{ name; impargs; typ; _} = + let { Info.hook; scope; kind; compute_guard; _ } = info in + (* if i = 0 , we don't touch the type; this is for compat + but not clear it is the right thing to do. + *) + let pe, ubind = + if i > 0 && not (CList.is_empty compute_guard) + then Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders + else pe, UState.universe_binders uctx + in + (* We when compute_guard was [] in the previous step we should not + substitute the body *) + let pe = match compute_guard with + | [] -> pe + | _ -> + Internal.map_entry_body pe + ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) + in + declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe + + let declare_mutdef ~info ~uctx const = + let pe = match info.Info.compute_guard with + | [] -> + (* Not a recursive statement *) + const + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + Internal.map_entry_body const + ~f:(guess_decreasing env possible_indexes) + in + List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms + + let declare_variable ~info ~uctx pe = + let { Info.scope; hook } = info in + List.map_i ( + fun i { Recthm.name; typ; impargs } -> + declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + ) 0 info.Info.thms + +end + +(************************************************************************) +(* Admitting a lemma-like constant *) +(************************************************************************) + +(* Admitted *) +let get_keep_admitted_vars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Keep"; "Admitted"; "Variables"] + ~value:true + +let compute_proof_using_for_admitted proof typ pproofs = + if not (get_keep_admitted_vars ()) then None + else match get_used_variables proof, pproofs with + | Some _ as x, _ -> x + | None, pproof :: _ -> + let env = Global.env () in + let ids_typ = Environ.global_vars_set env typ in + (* [pproof] is evar-normalized by [partial_proof]. We don't + count variables appearing only in the type of evars. *) + let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) + | _ -> None + +let finish_admitted ~info ~uctx pe = + let cst = MutualEntry.declare_variable ~info ~uctx pe in + (* If the constant was an obligation we need to update the program map *) + match CEphemeron.get info.Info.proof_ending with + | Proof_ending.End_obligation oinfo -> + Obls.obligation_admitted_terminator oinfo uctx (List.hd cst) + | _ -> () + +let save_lemma_admitted ~proof ~info = + let udecl = get_universe_decl proof in + let Proof.{ poly; entry } = Proof.data (get_proof proof) in + let typ = match Proofview.initial_goals entry with + | [typ] -> snd typ + | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") + in + let typ = EConstr.Unsafe.to_constr typ in + let iproof = get_proof proof in + let pproofs = Proof.partial_proof iproof in + let sec_vars = compute_proof_using_for_admitted proof typ pproofs in + let uctx = get_initial_euctx proof in + let univs = UState.check_univ_decl ~poly uctx udecl in + finish_admitted ~info ~uctx (sec_vars, (typ, univs), None) + +(************************************************************************) +(* Saving a lemma-like constant *) +(************************************************************************) + +let finish_proved po info = + match po with + | { entries=[const]; uctx } -> + let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in + () + | _ -> + CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") + +let finish_derived ~f ~name ~entries = + (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) + + let f_def, lemma_def = + match entries with + | [_;f_def;lemma_def] -> + f_def, lemma_def + | _ -> assert false + in + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) + let f_def = Internal.set_opacity ~opaque:false f_def in + let f_kind = Decls.(IsDefinition Definition) in + let f_def = DefinitionEntry f_def in + let f_kn = declare_constant ~name:f ~kind:f_kind f_def in + let f_kn_term = Constr.mkConst f_kn in + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) + let substf c = Vars.replace_vars [f,f_kn_term] c in + (* Extracts the type of the proof of [suchthat]. *) + let lemma_pretype typ = + match typ with + | Some t -> Some (substf t) + | None -> assert false (* Declare always sets type here. *) + in + (* The references of [f] are subsituted appropriately. *) + let lemma_def = Internal.map_entry_type lemma_def ~f:lemma_pretype in + (* The same is done in the body of the proof. *) + let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = DefinitionEntry lemma_def in + let _ : Names.Constant.t = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in + () + +let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = + + let obls = ref 1 in + let sigma, recobls = + CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry -> + let id = + match Evd.evar_ident ev sigma0 with + | Some id -> id + | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) + in + let entry, args = Internal.shrink_entry local_context entry in + let cst = declare_constant ~name:id ~kind (DefinitionEntry entry) in + let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in + let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in + sigma, cst) sigma0 + types proof_obj.entries + in + hook recobls sigma + +let finalize_proof proof_obj proof_info = + let open Proof_ending in + match CEphemeron.default proof_info.Info.proof_ending Regular with + | Regular -> + finish_proved proof_obj proof_info + | End_obligation oinfo -> + Obls.obligation_terminator proof_obj.entries proof_obj.uctx oinfo + | End_derive { f ; name } -> + finish_derived ~f ~name ~entries:proof_obj.entries + | End_equations { hook; i; types; sigma } -> + finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma + +let err_save_forbidden_in_place_of_qed () = + CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") + +let process_idopt_for_save ~idopt info = + match idopt with + | None -> info + | Some { CAst.v = save_name } -> + (* Save foo was used; we override the info in the first theorem *) + let thms = + match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with + | [ { Recthm.name; _} as decl ], Proof_ending.Regular -> + [ { decl with Recthm.name = save_name } ] + | _ -> + err_save_forbidden_in_place_of_qed () + in { info with Info.thms } + +let save_lemma_proved ~proof ~info ~opaque ~idopt = + (* Env and sigma are just used for error printing in save_remaining_recthms *) + let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in + let proof_info = process_idopt_for_save ~idopt info in + finalize_proof proof_obj proof_info + +(***********************************************************************) +(* Special case to close a lemma without forcing a proof *) +(***********************************************************************) +let save_lemma_admitted_delayed ~proof ~info = + let { entries; uctx } = proof in + if List.length entries <> 1 then + CErrors.user_err Pp.(str "Admitted does not support multiple statements"); + let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + let poly = match proof_entry_universes with + | Entries.Monomorphic_entry _ -> false + | Entries.Polymorphic_entry (_, _) -> true in + 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 uctx in + let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in + finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None) + +let save_lemma_proved_delayed ~proof ~info ~idopt = + (* vio2vo calls this but with invalid info, we have to workaround + that to add the name to the info structure *) + if CList.is_empty info.Info.thms then + let name = get_po_name proof in + let info = Info.add_first_thm ~info ~name ~typ:EConstr.mkSet ~impargs:[] in + finalize_proof proof info + else + let info = process_idopt_for_save ~idopt info in + finalize_proof proof info + +module Proof = struct + type nonrec t = t + let get_proof = get_proof + let get_proof_name = get_proof_name + let map_proof = map_proof + let map_fold_proof = map_fold_proof + let map_fold_proof_endline = map_fold_proof_endline + let set_endline_tactic = set_endline_tactic + let set_used_variables = set_used_variables + let compact = compact_the_proof + let update_global_env = update_global_env + let get_open_goals = get_open_goals +end diff --git a/vernac/declare.mli b/vernac/declare.mli index 340c035d1d..62bc6a34bf 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -17,9 +17,9 @@ open Entries environment. It also updates some accesory tables such as [Nametab] (name resolution), [Impargs], and [Notations]. *) -(** We provide two kind of fuctions: +(** We provide two kind of functions: - - one go functions, that will register a constant in one go, suited + - one-go functions, that will register a constant in one go, suited for non-interactive definitions where the term is given. - two-phase [start/declare] functions which will create an @@ -29,6 +29,13 @@ open Entries Internally, these functions mainly differ in that usually, the first case doesn't require setting up the tactic engine. + Note that the API in this file is still in a state of flux, don't + hesitate to contact the maintainers if you have any question. + + Additionally, this file does contain some low-level functions, marked + as such; these functions are unstable and should not be used unless you + already know what they are doing. + *) (** [Declare.Proof.t] Construction of constants using interactive proofs. *) @@ -41,11 +48,6 @@ module Proof : sig val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t - (** XXX: These 3 are only used in lemmas *) - val get_used_variables : t -> Names.Id.Set.t option - val get_universe_decl : t -> UState.universe_decl - val get_initial_euctx : t -> UState.t - val map_proof : (Proof.t -> Proof.t) -> t -> t val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a @@ -97,39 +99,33 @@ val start_dependent_proof (** Proof entries represent a proof that has been finished, but still not registered with the kernel. - XXX: Scheduled for removal from public API, don't rely on it *) -type 'a proof_entry = private { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Id.Set.t option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - -(** XXX: Scheduled for removal from public API, don't rely on it *) -type proof_object = private - { name : Names.Id.t - (** name of the proof *) - ; entries : Evd.side_effects proof_entry list - (** list of the proof terms (in a form suitable for definitions). *) - ; uctx: UState.t - (** universe state *) - } + XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) +type 'a proof_entry + +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) +type proof_object + +(** Used by the STM only to store info, should go away *) +val get_po_name : proof_object -> Id.t val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object (** Declaration of local constructions (Variable/Hypothesis/Local) *) -(** XXX: Scheduled for removal from public API, don't rely on it *) +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } -(** XXX: Scheduled for removal from public API, don't rely on it *) +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) type 'a constant_entry = | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry @@ -144,7 +140,9 @@ val declare_variable (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... - XXX: Scheduled for removal from public API, use `DeclareDef` instead *) + XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool @@ -160,7 +158,7 @@ val definition_entry -> constr -> Evd.side_effects proof_entry -type import_status = ImportDefaultBehavior | ImportNeedQualified +type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -169,7 +167,9 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent - XXX: Scheduled for removal from public API, use `DeclareDef` instead *) + XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) val declare_constant : ?local:import_status -> name:Id.t @@ -177,17 +177,6 @@ val declare_constant -> Evd.side_effects constant_entry -> Constant.t -(** [inline_private_constants ~sideff ~uctx env ce] will inline the - constants in [ce]'s body and return the body plus the updated - [UState.t]. - - XXX: Scheduled for removal from public API, don't rely on it *) -val inline_private_constants - : uctx:UState.t - -> Environ.env - -> Evd.side_effects proof_entry - -> Constr.t * UState.t - (** Declaration messages *) (** XXX: Scheduled for removal from public API, do not use *) @@ -201,13 +190,6 @@ val check_exists : Id.t -> unit module Internal : sig - val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry - val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry - (* Overriding opacity is indeed really hacky *) - val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry - - val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list - type constant_obj val objConstant : constant_obj Libobject.Dyn.tag @@ -233,6 +215,7 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Returns [false] if an unsafe tactic has been used. *) val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool +(** Semantics of this function is a bit dubious, use with care *) val build_by_tactic : ?side_eff:bool -> Environ.env @@ -260,7 +243,7 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env environment and empty evar_map. *) val get_current_context : Proof.t -> Evd.evar_map * Environ.env -(** Temporarily re-exported for 3rd party code; don't use *) +(** XXX: Temporarily re-exported for 3rd party code; don't use *) val build_constant_by_tactic : name:Names.Id.t -> ?opaque:opacity_flag -> @@ -270,11 +253,12 @@ val build_constant_by_tactic : EConstr.types -> unit Proofview.tactic -> Evd.side_effects proof_entry * bool * UState.t +[@@ocaml.deprecated "This function is deprecated, used newer API in declare"] val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] -type locality = Discharge | Global of import_status +type locality = Locality.locality = Discharge | Global of import_status (** Declaration hooks *) module Hook : sig @@ -303,7 +287,9 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end -(** Declare an interactively-defined constant *) +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) val declare_entry : name:Id.t -> scope:locality @@ -361,6 +347,8 @@ module Recthm : sig } end +type lemma_possible_guards = int list list + val declare_mutually_recursive : opaque:bool -> scope:locality @@ -370,19 +358,16 @@ val declare_mutually_recursive -> udecl:UState.universe_decl -> ntns:Vernacexpr.decl_notation list -> rec_declaration:Constr.rec_declaration - -> possible_indexes:int list list option + -> possible_indexes:lemma_possible_guards option -> ?restrict_ucontext:bool (** XXX: restrict_ucontext should be always true, this seems like a bug in obligations, so this parameter should go away *) -> Recthm.t list -> Names.GlobRef.t list +(** Prepare API, to be removed once we provide the corresponding 1-step API *) val prepare_obligation - : ?opaque:bool - -> ?inline:bool - -> name:Id.t - -> poly:bool - -> udecl:UState.universe_decl + : name:Id.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map @@ -397,3 +382,214 @@ val prepare_parameter (* Compat: will remove *) exception AlreadyDeclared of (string option * Names.Id.t) + +module Obls : sig + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +module Obligation : sig + 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 + +(* 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 : locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : Hook.t option + ; prg_opaque : bool } + + val make : + ?opaque:bool + -> ?hook:Hook.t + -> Names.Id.t + -> udecl:UState.universe_decl + -> uctx:UState.t + -> impargs:Impargs.manual_implicits + -> poly:bool + -> scope: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 + +(** [declare_obligation] Save an obligation *) +val declare_obligation : + ProgramDecl.t + -> Obligation.t + -> Constr.types + -> Constr.types option + -> Entries.universes_entry + -> bool * Obligation.t + +module State : sig + + val num_pending : unit -> int + val first_pending : unit -> ProgramDecl.t option + + (** Returns [Error duplicate_list] if not a single program is open *) + val get_unique_open_prog : + Id.t option -> (ProgramDecl.t, Id.t list) result + + (** Add a new obligation *) + val add : Id.t -> ProgramDecl.t -> unit + + val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a + + val all : unit -> ProgramDecl.t list + + val find : Id.t -> ProgramDecl.t option + + (* Internal *) + type t + val prg_tag : t Summary.Dyn.tag +end + +val declare_definition : ProgramDecl.t -> Names.GlobRef.t + +(** Resolution status of a program *) +type progress = + | Remain of int (** n obligations remaining *) + | Dependent (** Dependent on other definitions *) + | Defined of GlobRef.t (** Defined as id *) + +type obligation_resolver = + Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> progress + +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +(** [update_obls prg obls n progress] What does this do? *) +val update_obls : + ProgramDecl.t -> Obligation.t array -> int -> progress + +(** Check obligations are properly solved before closing the + [what_for] section / module *) +val check_solved_obligations : what_for:Pp.t -> unit + +(** { 2 Util } *) + +val obl_substitution : + bool + -> Obligation.t array + -> Int.Set.t + -> (Id.t * (Constr.types * Constr.types)) list + +val dependencies : Obligation.t array -> int -> Int.Set.t +val err_not_transp : unit -> 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 + * is not available here, so we provide a side channel to get it *) +val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref + +end + +(** Creating high-level proofs with an associated constant *) +module Proof_ending : sig + + type t = + | Regular + | End_obligation of Obls.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } + +end + +module Info : sig + type t + val make + : ?hook: Hook.t + (** Callback to be executed at the end of the proof *) + -> ?proof_ending : Proof_ending.t + (** Info for special constants *) + -> ?scope : locality + (** locality *) + -> ?kind:Decls.logical_kind + (** Theorem, etc... *) + -> ?compute_guard:lemma_possible_guards + -> ?thms:Recthm.t list + (** Both of those are internal, used by the upper layers but will + become handled natively here in the future *) + -> unit + -> t + + (* Internal; used to initialize non-mutual proofs *) + val add_first_thm : + info:t + -> name:Id.t + -> typ:EConstr.t + -> impargs:Impargs.manual_implicits + -> t +end + +val save_lemma_proved + : proof:Proof.t + -> info:Info.t + -> opaque:opacity_flag + -> idopt:Names.lident option + -> unit + +val save_lemma_admitted : + proof:Proof.t + -> info:Info.t + -> unit + +(** Special cases for delayed proofs, in this case we must provide the + proof information so the proof won't be forced. *) +val save_lemma_admitted_delayed : + proof:proof_object + -> info:Info.t + -> unit + +val save_lemma_proved_delayed + : proof:proof_object + -> info:Info.t + -> idopt:Names.lident option + -> unit diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml deleted file mode 100644 index 9ea54f5d8f..0000000000 --- a/vernac/declareObl.ml +++ /dev/null @@ -1,578 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Names -open Environ -open Context -open Constr -open Vars -open Entries - -type 'a obligation_body = DefinedObl of 'a | TermObl of constr - -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 } - - 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 - -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 : Declare.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : Declare.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 *) - -(* XXX: Is this the right place for this? *) -let it_mkLambda_or_LetIn_or_clean t ctx = - let open Context.Rel.Declaration in - let fold t decl = - if is_local_assum decl then Term.mkLambda_or_LetIn decl t - else if noccurn 1 t then subst1 mkProp t - else Term.mkLambda_or_LetIn decl t - in - Context.Rel.fold_inside fold ctx ~init:t - -(* XXX: Is this the right place for this? *) -let decompose_lam_prod c ty = - let open Context.Rel.Declaration in - let rec aux ctx c ty = - match (Constr.kind c, Constr.kind ty) with - | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when Constr.equal b b' && Constr.equal t t' -> - let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in - aux ctx' c ty - | _, LetIn (x', b', t', ty) -> - let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in - aux ctx' (lift 1 c) ty - | LetIn (x, b, t, c), _ -> - let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in - aux ctx' c (lift 1 ty) - | Lambda (x, b, t), Prod (x', b', t') - (* By invariant, must be convertible *) -> - let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in - aux ctx' t t' - | Cast (c, _, _), _ -> aux ctx c ty - | _, _ -> (ctx, c, ty) - in - aux Context.Rel.empty c ty - -(* XXX: What's the relation of this with Abstract.shrink ? *) -let shrink_body c ty = - let ctx, b, ty = - match ty with - | None -> - let ctx, b = Term.decompose_lam_assum c in - (ctx, b, None) - | Some ty -> - let ctx, b, ty = decompose_lam_prod c ty in - (ctx, b, Some ty) - in - let b', ty', n, args = - List.fold_left - (fun (b, ty, i, args) decl -> - if noccurn 1 b && Option.cata (noccurn 1) true ty then - (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args) - else - let open Context.Rel.Declaration in - let args = if is_local_assum decl then mkRel i :: args else args in - ( Term.mkLambda_or_LetIn decl b - , Option.map (Term.mkProd_or_LetIn decl) ty - , succ i - , args ) ) - (b, ty, 1, []) ctx - 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) - -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true - ~key:["Hide"; "Obligations"] - ~value:false - -let declare_obligation prg obl body ty uctx = - let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in - match obl.obl_status with - | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) - | force, Evar_kinds.Define opaque -> - let opaque = (not force) && opaque in - let poly = prg.prg_poly in - let ctx, body, ty, args = - if not poly then shrink_body body ty - else ([], body, ty, [||]) - in - let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in - - (* ppedrot: seems legit to have obligations as local *) - let constant = - Declare.declare_constant ~name:obl.obl_name - ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property) - (Declare.DefinitionEntry ce) - in - if not opaque then - add_hint (Locality.make_section_locality None) prg constant; - Declare.definition_message obl.obl_name; - let body = - match uctx with - | Polymorphic_entry (_, uctx) -> - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_entry _ -> - Some - (TermObl - (it_mkLambda_or_LetIn_or_clean - (mkApp (mkConst constant, args)) - ctx)) - in - (true, {obl with obl_body = body}) - -(* Updating the obligation meta-info on close *) - -let not_transp_msg = - Pp.( - str "Obligation should be transparent but was declared opaque." - ++ spc () - ++ str "Use 'Defined' instead.") - -let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -let err_not_transp () = pperror not_transp_msg - -module ProgMap = Id.Map - -let from_prg, program_tcc_summary_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - -(* In all cases, the use of the map is read-only so we don't expose the ref *) -let get_prg_info_map () = !from_prg - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let check_can_close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - CErrors.user_err ~hdr:"Program" - Pp.( - str "Unsolved obligations when closing " - ++ Id.print sec ++ str ":" ++ spc () - ++ prlist_with_sep spc (fun x -> Id.print x) keys - ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") - ++ str "unsolved obligations" )) - -let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) -let prgmap_op f = from_prg := f !from_prg -let progmap_remove prg = prgmap_op (ProgMap.remove prg.prg_name) -let progmap_add n prg = prgmap_op (ProgMap.add n prg) -let progmap_replace prg = prgmap_op (map_replace prg.prg_name prg) - -let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 - -let obligations_message rem = - if rem > 0 then - if Int.equal rem 1 then - Flags.if_verbose Feedback.msg_info - Pp.(int rem ++ str " obligation remaining") - else - Flags.if_verbose Feedback.msg_info - Pp.(int rem ++ str " obligations remaining") - else - Flags.if_verbose Feedback.msg_info Pp.(str "No more obligations remaining") - -type progress = Remain of int | Dependent | Defined of GlobRef.t - -let get_obligation_body expand obl = - match obl.obl_body with - | None -> None - | Some c -> ( - if expand && snd obl.obl_status == Evar_kinds.Expand then - match c with - | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) - | TermObl c -> Some c - else - match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) - -let obl_substitution expand obls deps = - Int.Set.fold - (fun x acc -> - let xobl = obls.(x) in - match get_obligation_body expand xobl with - | None -> acc - | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc ) - deps [] - -let rec intset_to = function - | -1 -> Int.Set.empty - | n -> Int.Set.add n (intset_to (pred n)) - -let obligation_substitution expand prg = - let obls = prg.prg_obligations.obls in - let ints = intset_to (pred (Array.length obls)) in - obl_substitution expand obls ints - -let hide_obligation () = - Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; - UnivGen.constr_of_monomorphic_global - (Coqlib.lib_ref "program.tactics.obligation") - -(* XXX: Is this the right place? *) -let rec prod_app t n = - match - Constr.kind - (EConstr.Unsafe.to_constr - (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) - (* FIXME *) - with - | Prod (_, _, b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - CErrors.user_err ~hdr:"prod_app" - Pp.(str "Needed a product, but didn't find one" ++ fnl ()) - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let t, b = Id.List.assoc (destVar f) subst in - mkApp - ( delayed_force hide_obligation - , [|prod_applist t c'; Term.applistc b c'|] ) - with Not_found -> Constr.map aux c - else Constr.map aux c - in - Constr.map aux - -let subst_prog subst prg = - if get_hide_obligations () then - ( replace_appvars subst prg.prg_body - , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) - else - let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in - ( Vars.replace_vars subst' prg.prg_body - , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) - -let get_fix_exn, stm_get_fix_exn = Hook.make () - -let declare_definition prg = - let varsubst = obligation_substitution true prg in - let sigma = Evd.from_ctx prg.prg_ctx in - let body, types = subst_prog varsubst prg in - let body, types = EConstr.(of_constr body, Some (of_constr types)) in - (* All these should be grouped into a struct a some point *) - let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in - let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in - let fix_exn = Hook.get get_fix_exn () in - let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in - (* XXX: This is doing normalization twice *) - let () = progmap_remove prg in - let kn = - Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls - ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma - in - kn - -let rec lam_index n t acc = - match Constr.kind t with - | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc - | Lambda (_, _, b) -> lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences n fixbody fixtype = - match n with - | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = - Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) - (* FIXME *) - in - let ctx = fst (Term.decompose_prod_n_assum m fixtype) in - List.map_i (fun i _ -> i) 0 ctx - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let defobl x = - let oblsubst = obligation_substitution true x in - let subs, typ = subst_prog oblsubst x in - let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in - let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in - let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in - let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in - let term = EConstr.to_constr sigma term in - let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in - let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in - def, oblsubst - in - let defs, obls = - List.fold_right (fun x (defs, obls) -> - let xdef, xobls = defobl x in - (xdef :: defs, xobls @ obls)) l ([], []) - in - (* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs, fixtypes, fixitems = - List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) -> - d :: a1, r :: a2, typ :: a3, - Declare.Recthm.{ name; typ; impargs; args = [] } :: a4 - ) defs first.prg_deps ([],[],[],[]) - in - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in - let rvec = Array.of_list fixrs in - let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let possible_indexes = - match fixkind with - | IsFixpoint wfl -> - Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) - | IsCoFixpoint -> None - in - (* In the future we will pack all this in a proper record *) - let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in - (* Declare the recursive definitions *) - let udecl = UState.default_univ_decl in - let kns = - Declare.declare_mutually_recursive ~scope ~opaque ~kind - ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly - ~restrict_ucontext:false fixitems - in - (* Only for the first constant *) - let dref = List.hd kns in - Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); - List.iter progmap_remove l; - dref - -let update_obls prg obls rem = - 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 - else - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = - List.map - (fun x -> CEphemeron.get (ProgMap.find x !from_prg)) - prg'.prg_deps - in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent - -let dependencies obls n = - let res = ref Int.Set.empty in - Array.iteri - (fun i obl -> - if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then - res := Int.Set.add i !res ) - 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 - ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress - } - -let obligation_terminator entries uctx { name; num; auto } = - match entries with - | [entry] -> - let env = Global.env () in - let ty = entry.Declare.proof_entry_type 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 *) - let prg = CEphemeron.get (ProgMap.find name !from_prg) 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 - | (_, Evar_kinds.Expand), true -> err_not_transp () - | (true, _), true -> err_not_transp () - | (false, _), true -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), false -> - Evar_kinds.Define false - | (_, status), false -> status - in - let obl = { obl with obl_status = false, status } in - let uctx = - if prg.prg_poly then uctx - else UState.union prg.prg_ctx uctx - in - let univs = UState.univ_entry ~poly:prg.prg_poly uctx in - let (defined, obl) = declare_obligation prg obl body ty univs in - let prg_ctx = - if prg.prg_poly then (* Polymorphic *) - (* We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx uctx - else - (* The first obligation, if defined, - declares the univs of the constant, - each subsequent obligation declares its own additional - universes and constraints if any *) - if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) - else uctx - in - 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 { Declare.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 deleted file mode 100644 index 03f0a57bcb..0000000000 --- a/vernac/declareObl.mli +++ /dev/null @@ -1,164 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr - -type 'a obligation_body = DefinedObl of 'a | TermObl of constr - -module Obligation : sig - - 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 - -(* 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 : Declare.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : Declare.Hook.t option - ; prg_opaque : bool - } - - val make : - ?opaque:bool - -> ?hook:Declare.Hook.t - -> Names.Id.t - -> udecl:UState.universe_decl - -> uctx:UState.t - -> impargs:Impargs.manual_implicits - -> poly:bool - -> scope:Declare.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 : - ProgramDecl.t - -> Obligation.t - -> Constr.types - -> Constr.types option - -> Entries.universes_entry - -> 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 : ProgramDecl.t -> Names.GlobRef.t - -(** Resolution status of a program *) -type progress = - | Remain of int - (** n obligations remaining *) - | Dependent - (** Dependent on other definitions *) - | Defined of GlobRef.t - (** Defined as id *) - -type obligation_qed_info = - { name : Id.t - ; num : int - ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress - } - -val obligation_terminator - : Evd.side_effects Declare.proof_entry list - -> UState.t - -> obligation_qed_info -> unit -(** [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) - -> Declare.Hook.S.t - -> unit -(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *) - -val update_obls : - ProgramDecl.t - -> Obligation.t array - -> int - -> progress -(** [update_obls prg obls n progress] What does this do? *) - -(** { 2 Util } *) - -(** Check obligations are properly solved before closing a section *) -val check_can_close : Id.t -> unit - -val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t - -val program_tcc_summary_tag : - ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag - -val obl_substitution : - bool - -> Obligation.t array - -> Int.Set.t - -> (ProgMap.key * (Constr.types * Constr.types)) list - -val dependencies : Obligation.t array -> int -> Int.Set.t - -val err_not_transp : unit -> 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 - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 838496c595..10d63ff2ff 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -12,7 +12,6 @@ file command.ml, Aug 2009 *) open Util -open Names module NamedDecl = Context.Named.Declaration @@ -21,44 +20,8 @@ module NamedDecl = Context.Named.Declaration type lemma_possible_guards = int list list -module Proof_ending = struct - - type t = - | Regular - | End_obligation of DeclareObl.obligation_qed_info - | End_derive of { f : Id.t; name : Id.t } - | End_equations of - { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; sigma : Evd.evar_map - } - -end - -module Info = struct - - type t = - { hook : Declare.Hook.t option - ; proof_ending : Proof_ending.t CEphemeron.key - (* This could be improved and the CEphemeron removed *) - ; scope : Declare.locality - ; kind : Decls.logical_kind - (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) - ; thms : Declare.Recthm.t list - ; compute_guard : lemma_possible_guards - } - - let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Declare.Global Declare.ImportDefaultBehavior) - ?(kind=Decls.(IsProof Lemma)) () = - { hook - ; compute_guard = [] - ; proof_ending = CEphemeron.create proof_ending - ; thms = [] - ; scope - ; kind - } -end +module Proof_ending = Declare.Proof_ending +module Info = Declare.Info (* Proofs with a save constant function *) type t = @@ -96,15 +59,6 @@ let initialize_named_context_for_proof () = let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let add_first_thm ~info ~name ~typ ~impargs = - let thms = - { Declare.Recthm.name - ; impargs - ; typ = EConstr.Unsafe.to_constr typ - ; args = [] } :: info.Info.thms - in - { info with Info.thms } - (* Starting a goal *) let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) @@ -114,7 +68,7 @@ let start_lemma ~name ~poly let sign = initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in let proof = Declare.start_proof sigma ~name ~udecl ~poly goals in - let info = add_first_thm ~info ~name ~typ:c ~impargs in + let info = Declare.Info.add_first_thm ~info ~name ~typ:c ~impargs in { proof; info } (* Note that proofs opened by start_dependent lemma cannot be closed @@ -162,276 +116,15 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") | { Declare.Recthm.name; typ; impargs; _} :: thms -> - let info = - Info.{ hook - ; compute_guard - ; proof_ending = CEphemeron.create Proof_ending.Regular - ; thms - ; scope - ; kind - } in + let info = Info.make ?hook ~scope ~kind ~compute_guard ~thms () in (* start_lemma has the responsibility to add (name, impargs, typ) to thms, once Info.t is more refined this won't be necessary *) let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Declare.Proof.map_proof (fun p -> pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma -(************************************************************************) -(* Commom constant saving path, for both Qed and Admitted *) -(************************************************************************) - -(* Support for mutually proved theorems *) - -(* XXX: Most of this does belong to Declare, due to proof_entry manip *) -module MutualEntry : sig - - val declare_variable - : info:Info.t - -> uctx:UState.t - -> Entries.parameter_entry - -> Names.GlobRef.t list - - val declare_mutdef - (* Common to all recthms *) - : info:Info.t - -> uctx:UState.t - -> Evd.side_effects Declare.proof_entry - -> Names.GlobRef.t list - -end = struct - - (* XXX: Refactor this with the code in [Declare.declare_mutdef] *) - let guess_decreasing env possible_indexes ((body, ctx), eff) = - let open Constr in - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = Pretyping.search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff - - let select_body i t = - let open Constr in - match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | _ -> - CErrors.anomaly - Pp.(str "Not a proof by induction: " ++ - Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - - let declare_mutdef ~uctx ~info pe i Declare.Recthm.{ name; impargs; typ; _} = - let { Info.hook; scope; kind; compute_guard; _ } = info in - (* if i = 0 , we don't touch the type; this is for compat - but not clear it is the right thing to do. - *) - let pe, ubind = - if i > 0 && not (CList.is_empty compute_guard) - then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders - else pe, UState.universe_binders uctx - in - (* We when compute_guard was [] in the previous step we should not - substitute the body *) - let pe = match compute_guard with - | [] -> pe - | _ -> - Declare.Internal.map_entry_body pe - ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) - in - Declare.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe - - let declare_mutdef ~info ~uctx const = - let pe = match info.Info.compute_guard with - | [] -> - (* Not a recursive statement *) - const - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - Declare.Internal.map_entry_body const - ~f:(guess_decreasing env possible_indexes) - in - List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms - - let declare_variable ~info ~uctx pe = - let { Info.scope; hook } = info in - List.map_i ( - fun i { Declare.Recthm.name; typ; impargs } -> - Declare.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe - ) 0 info.Info.thms - -end - -(************************************************************************) -(* Admitting a lemma-like constant *) -(************************************************************************) - -(* Admitted *) -let get_keep_admitted_vars = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Keep"; "Admitted"; "Variables"] - ~value:true - -let compute_proof_using_for_admitted proof typ pproofs = - if not (get_keep_admitted_vars ()) then None - else match Declare.Proof.get_used_variables proof, pproofs with - | Some _ as x, _ -> x - | None, pproof :: _ -> - let env = Global.env () in - let ids_typ = Environ.global_vars_set env typ in - (* [pproof] is evar-normalized by [partial_proof]. We don't - count variables appearing only in the type of evars. *) - let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in - Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) - | _ -> None - -let finish_admitted ~info ~uctx pe = - let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx pe in - () - -let save_lemma_admitted ~(lemma : t) : unit = - let udecl = Declare.Proof.get_universe_decl lemma.proof in - let Proof.{ poly; entry } = Proof.data (Declare.Proof.get_proof lemma.proof) in - let typ = match Proofview.initial_goals entry with - | [typ] -> snd typ - | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") - in - let typ = EConstr.Unsafe.to_constr typ in - let proof = Declare.Proof.get_proof lemma.proof in - let pproofs = Proof.partial_proof proof in - let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in - let uctx = Declare.Proof.get_initial_euctx lemma.proof in - let univs = UState.check_univ_decl ~poly uctx udecl in - finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None) - -(************************************************************************) -(* Saving a lemma-like constant *) -(************************************************************************) - -let finish_proved po info = - let open Declare in - match po with - | { entries=[const]; uctx } -> - let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in - () - | _ -> - CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") - -let finish_derived ~f ~name ~entries = - (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) - - let f_def, lemma_def = - match entries with - | [_;f_def;lemma_def] -> - f_def, lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = Declare.Internal.set_opacity ~opaque:false f_def in - let f_kind = Decls.(IsDefinition Definition) in - let f_def = Declare.DefinitionEntry f_def in - let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in - let f_kn_term = Constr.mkConst f_kn in - (* In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype typ = - match typ with - | Some t -> Some (substf t) - | None -> assert false (* Declare always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = Declare.DefinitionEntry lemma_def in - let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in - () - -let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = - - let obls = ref 1 in - let sigma, recobls = - CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry -> - let id = - match Evd.evar_ident ev sigma0 with - | Some id -> id - | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) - in - let entry, args = Declare.Internal.shrink_entry local_context entry in - let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in - let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in - let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in - sigma, cst) sigma0 - types proof_obj.Declare.entries - in - hook recobls sigma - -let finalize_proof proof_obj proof_info = - let open Declare in - let open Proof_ending in - match CEphemeron.default proof_info.Info.proof_ending Regular with - | Regular -> - finish_proved proof_obj proof_info - | End_obligation oinfo -> - DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo - | End_derive { f ; name } -> - finish_derived ~f ~name ~entries:proof_obj.entries - | End_equations { hook; i; types; sigma } -> - finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma - -let err_save_forbidden_in_place_of_qed () = - CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") - -let process_idopt_for_save ~idopt info = - match idopt with - | None -> info - | Some { CAst.v = save_name } -> - (* Save foo was used; we override the info in the first theorem *) - let thms = - match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with - | [ { Declare.Recthm.name; _} as decl ], Proof_ending.Regular -> - [ { decl with Declare.Recthm.name = save_name } ] - | _ -> - err_save_forbidden_in_place_of_qed () - in { info with Info.thms } +let save_lemma_admitted ~lemma = + Declare.save_lemma_admitted ~proof:lemma.proof ~info:lemma.info let save_lemma_proved ~lemma ~opaque ~idopt = - (* Env and sigma are just used for error printing in save_remaining_recthms *) - let proof_obj = Declare.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in - let proof_info = process_idopt_for_save ~idopt lemma.info in - finalize_proof proof_obj proof_info - -(***********************************************************************) -(* Special case to close a lemma without forcing a proof *) -(***********************************************************************) -let save_lemma_admitted_delayed ~proof ~info = - let open Declare in - let { entries; uctx } = 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 - let poly = match proof_entry_universes with - | Entries.Monomorphic_entry _ -> false - | Entries.Polymorphic_entry (_, _) -> true in - 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 uctx in - let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None) - -let save_lemma_proved_delayed ~proof ~info ~idopt = - (* vio2vo calls this but with invalid info, we have to workaround - that to add the name to the info structure *) - if CList.is_empty info.Info.thms then - let info = add_first_thm ~info ~name:proof.Declare.name ~typ:EConstr.mkSet ~impargs:[] in - finalize_proof proof info - else - let info = process_idopt_for_save ~idopt info in - finalize_proof proof info + Declare.save_lemma_proved ~proof:lemma.proof ~info:lemma.info ~opaque ~idopt diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index b1462f1ce5..4787a940da 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -28,39 +28,8 @@ val pf_fold : (Declare.Proof.t -> 'a) -> t -> 'a val by : unit Proofview.tactic -> t -> t * bool (** [by tac l] apply a tactic to [l] *) -(** Creating high-level proofs with an associated constant *) -module Proof_ending : sig - - type t = - | Regular - | End_obligation of DeclareObl.obligation_qed_info - | End_derive of { f : Id.t; name : Id.t } - | End_equations of - { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; sigma : Evd.evar_map - } - -end - -module Info : sig - - type t - - val make - : ?hook: Declare.Hook.t - (** Callback to be executed at the end of the proof *) - -> ?proof_ending : Proof_ending.t - (** Info for special constants *) - -> ?scope : Declare.locality - (** locality *) - -> ?kind:Decls.logical_kind - (** Theorem, etc... *) - -> unit - -> t - -end +module Proof_ending = Declare.Proof_ending +module Info = Declare.Info (** Starts the proof of a constant *) val start_lemma @@ -99,6 +68,7 @@ val start_lemma_with_initialization (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit + val save_lemma_proved : lemma:t -> opaque:Declare.opacity_flag @@ -110,12 +80,3 @@ module Internal : sig val get_info : t -> Info.t (** Only needed due to the Declare compatibility layer. *) end - -(** Special cases for delayed proofs, in this case we must provide the - proof information so the proof won't be forced. *) -val save_lemma_admitted_delayed : proof:Declare.proof_object -> info:Info.t -> unit -val save_lemma_proved_delayed - : proof:Declare.proof_object - -> info:Info.t - -> idopt:Names.lident option - -> unit diff --git a/vernac/locality.ml b/vernac/locality.ml index f62eed5e41..3953e54f52 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -10,9 +10,12 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + let importability_of_bool = function - | true -> Declare.ImportNeedQualified - | false -> Declare.ImportDefaultBehavior + | true -> ImportNeedQualified + | false -> ImportDefaultBehavior (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -34,15 +37,14 @@ let warn_local_declaration = strbrk "available without qualification when imported.") let enforce_locality_exp locality_flag discharge = - let open Declare in let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) - | None, NoDischarge -> Global Declare.ImportDefaultBehavior + | None, NoDischarge -> Global ImportDefaultBehavior | None, DoDischarge when not (Global.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); - Global Declare.ImportNeedQualified + Global ImportNeedQualified | None, DoDischarge -> Discharge | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") diff --git a/vernac/locality.mli b/vernac/locality.mli index bf65579efd..81da895568 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -10,6 +10,9 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -20,7 +23,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 30ebf425d0..bbc20d5e30 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -9,39 +9,57 @@ (************************************************************************) open Printf - open Names open Pp -open CErrors open Util (* For the records fields, opens should go away one these types are private *) -open DeclareObl -open DeclareObl.Obligation -open DeclareObl.ProgramDecl - -let pperror ?info cmd = CErrors.user_err ~hdr:"Program" ?info cmd -let error s = pperror (str s) +open Declare.Obls +open Declare.Obls.Obligation +open Declare.Obls.ProgramDecl let reduce c = let env = Global.env () in let sigma = Evd.from_env env in EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c)) -exception NoObligations of Id.t option - let explain_no_obligations = function Some ident -> str "No obligations for program " ++ Id.print ident | None -> str "No obligations remaining" -let assumption_message = Declare.assumption_message +module Error = struct + + let no_obligations n = + CErrors.user_err (explain_no_obligations n) + + let ambiguous_program id ids = + CErrors.user_err + Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"") + + let unknown_obligation num = + CErrors.user_err (Pp.str (sprintf "Unknown obligation number %i" (succ num))) + let already_solved num = + CErrors.user_err + ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc () + ++ str "solved." ) + + let depends num rem = + CErrors.user_err + ( str "Obligation " ++ int num + ++ str " depends on obligation(s) " + ++ pr_sequence (fun x -> int (succ x)) rem) + +end + +let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) let subst_deps expand obls deps t = - let osubst = DeclareObl.obl_substitution expand obls deps in + let osubst = Declare.Obls.obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let subst_deps_obl obls obl = @@ -50,62 +68,6 @@ let subst_deps_obl obls obl = open Evd -let map_cardinal m = - let i = ref 0 in - ProgMap.iter (fun _ v -> - if (CEphemeron.get v).prg_obligations.remaining > 0 then incr i) m; - !i - -exception Found of ProgramDecl.t CEphemeron.key - -let map_first m = - try - ProgMap.iter (fun _ v -> - if (CEphemeron.get v).prg_obligations.remaining > 0 then - raise (Found v)) m; - assert(false) - with Found x -> x - -let get_prog name = - let prg_infos = get_prg_info_map () in - match name with - Some n -> - (try CEphemeron.get (ProgMap.find n prg_infos) - with Not_found -> raise (NoObligations (Some n))) - | None -> - (let n = map_cardinal prg_infos in - match n with - 0 -> raise (NoObligations None) - | 1 -> CEphemeron.get (map_first prg_infos) - | _ -> - let progs = Id.Set.elements (ProgMap.domain prg_infos) in - let prog = List.hd progs in - let progs = prlist_with_sep pr_comma Id.print progs in - user_err - (str "More than one program with unsolved obligations: " ++ progs - ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) - -let get_any_prog () = - let prg_infos = get_prg_info_map () in - let n = map_cardinal prg_infos in - if n > 0 then CEphemeron.get (map_first prg_infos) - else raise (NoObligations None) - -let get_prog_err n = - try get_prog n - with NoObligations id as exn -> - let _, info = Exninfo.capture exn in - pperror ~info (explain_no_obligations id) - -let get_any_prog_err () = - try get_any_prog () - with NoObligations id as exn -> - let _, info = Exninfo.capture exn in - pperror ~info (explain_no_obligations id) - -let all_programs () = - ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) [] - let is_defined obls x = not (Option.is_empty obls.(x).obl_body) let deps_remaining obls deps = @@ -115,7 +77,6 @@ let deps_remaining obls deps = else x :: acc) deps [] - let goal_kind = Decls.(IsDefinition Definition) let goal_proof_kind = Decls.(IsProof Lemma) @@ -125,19 +86,19 @@ let kind_of_obligation o = | Evar_kinds.Expand -> goal_kind | _ -> goal_proof_kind -let rec string_of_list sep f = function - [] -> "" - | x :: [] -> f x - | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl - (* Solve an obligation using tactics, return the corresponding proof term *) -let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err -> - Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); - str "This will become an error in the future"]) +let warn_solve_errored = + CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" + (fun err -> + 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 uctx = + (* the status is dropped. *) try - (* the status is dropped. *) let env = Global.env () in let body, types, _univs, _, uctx = Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in @@ -146,7 +107,7 @@ let solve_by_tac ?loc name evi t poly uctx = with | Refiner.FailError (_, s) as exn -> let _ = Exninfo.capture exn in - user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) + CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) (* If the proof is open we absorb the error and leave the obligation open *) | Proof.OpenProof _ -> None @@ -155,17 +116,24 @@ let solve_by_tac ?loc name evi t poly uctx = warn_solve_errored ?loc err; None +let get_unique_prog prg = + match State.get_unique_open_prog prg with + | Ok prg -> prg + | Error [] -> + Error.no_obligations None + | Error ((id :: _) as ids) -> + Error.ambiguous_program id ids + let rec solve_obligation prg num tac = let user_num = succ num in let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let remaining = deps_remaining obls obl.obl_deps in let () = - if not (Option.is_empty obl.obl_body) then - pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved."); - if not (List.is_empty remaining) then - pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); + if not (Option.is_empty obl.obl_body) + then Error.already_solved user_num; + if not (List.is_empty remaining) + then Error.depends user_num remaining in let obl = subst_deps_obl obls obl in let scope = Declare.(Global Declare.ImportNeedQualified) in @@ -173,9 +141,11 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in 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 = Declare.Hook.make (DeclareObl.obligation_hook prg obl num auto) in - let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in + let proof_ending = + Declare.Proof_ending.End_obligation + {Declare.Obls.name = prg.prg_name; num; auto} + in + let info = Lemmas.Info.make ~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 let lemma = fst @@ Lemmas.by !default_tactic lemma in @@ -184,15 +154,14 @@ 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 prg = get_unique_prog name 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 - | None -> solve_obligation prg num tac - | Some r -> error "Obligation already solved" - else error (sprintf "Unknown obligation number %i" (succ num)) - + if num >= 0 && num < Array.length obls then + let obl = obls.(num) in + match obl.obl_body with + | None -> solve_obligation prg num tac + | Some r -> Error.already_solved num + else Error.unknown_obligation num and solve_obligation_by_tac prg obls i tac = let obl = obls.(i) in @@ -222,10 +191,9 @@ and solve_obligation_by_tac prg obls i tac = obls.(i) <- obl'; if def && not prg.prg_poly then ( (* Declare the term constraints with the first obligation only *) - 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 (ProgramDecl.set_uctx ~uctx:ctx' prg)) + let uctx = UState.from_env (Global.env ()) in + let uctx = UState.merge_subst uctx (UState.subst ctx) in + Some (ProgramDecl.set_uctx ~uctx prg)) else Some prg else None @@ -239,45 +207,53 @@ and solve_prg_obligations prg ?oblset tac = | Some s -> set := s; (fun i -> Int.Set.mem i !set) in - let prg = - Array.fold_left_i (fun i prg x -> - if p i then - 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' + let (), prg = + Array.fold_left_i + (fun i ((), prg) x -> + if p i then ( + 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 prg obls' !rem and solve_obligations n tac = - let prg = get_prog_err n in + let prg = get_unique_prog n in solve_prg_obligations prg tac and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ()) + State.fold ~init:() ~f:(fun k v () -> + let _ = solve_prg_obligations v tac in ()) and try_solve_obligation n prg tac = - let prg = get_prog prg in + let prg = get_unique_prog prg 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 remaining)) - | None -> () + match solve_obligation_by_tac prg obls' n tac with + | Some prg' -> + let _r = update_obls prg' obls' (pred remaining) in + () + | None -> () and try_solve_obligations n tac = - try ignore (solve_obligations n tac) with NoObligations _ -> () + let _ = solve_obligations n tac in + () and auto_solve_obligations n ?oblset tac : progress = - Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically..."); - try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent + Flags.if_verbose Feedback.msg_info + (str "Solving obligations automatically..."); + let prg = get_unique_prog n in + solve_prg_obligations prg ?oblset tac open Pp -let show_obligations_of_prg ?(msg=true) prg = + +let show_obligations_of_prg ?(msg = true) prg = let n = prg.prg_name in let {obls; remaining} = prg.prg_obligations in let showed = ref 5 in @@ -290,70 +266,99 @@ let show_obligations_of_prg ?(msg=true) prg = let x = subst_deps_obl obls x in let env = Global.env () in let sigma = Evd.from_env env in - Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ - str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++ - hov 1 (Printer.pr_constr_env env sigma x.obl_type ++ - str "." ++ fnl ()))) + Feedback.msg_info + ( str "Obligation" ++ spc () + ++ int (succ i) + ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () + ++ hov 1 + ( Printer.pr_constr_env env sigma x.obl_type + ++ str "." ++ fnl () ) ) ) | Some _ -> ()) obls -let show_obligations ?(msg=true) n = - let progs = match n with - | None -> all_programs () +let show_obligations ?(msg = true) n = + let progs = + match n with + | None -> + State.all () | Some n -> - try [ProgMap.find n (get_prg_info_map ())] - with Not_found -> raise (NoObligations (Some n)) - in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs + (match State.find n with + | Some prg -> [prg] + | None -> Error.no_obligations (Some n)) + in + List.iter (fun x -> show_obligations_of_prg ~msg x) progs let show_term n = - let prg = get_prog_err n in + let prg = get_unique_prog n in let n = prg.prg_name in let env = Global.env () in let sigma = Evd.from_env env in - (Id.print n ++ spc () ++ str":" ++ spc () ++ - Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () - ++ Printer.pr_constr_env env sigma prg.prg_body) + Id.print n ++ spc () ++ str ":" ++ spc () + ++ 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 ~uctx ?(udecl=UState.default_univ_decl) - ?(impargs=[]) ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic - ?(reduce=reduce) ?hook ?(opaque = false) obls = +let msg_generating_obl name obls = + let len = Array.length obls in let info = Id.print name ++ str " has type-checked" in + Feedback.msg_info + (if len = 0 then info ++ str "." + else + info ++ str ", generating " ++ int len ++ + str (String.plural len " obligation")) + +let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) + ?(impargs = []) ~poly + ?(scope = Declare.Global Declare.ImportDefaultBehavior) + ?(kind = Decls.Definition) ?tactic ?(reduce = reduce) ?hook + ?(opaque = false) obls = 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 + Flags.if_verbose (msg_generating_obl name) obls; + let cst = Declare.Obls.declare_definition prg in Defined cst) - else ( - let len = Array.length obls in - let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in - progmap_add name (CEphemeron.create prg); - let res = auto_solve_obligations (Some name) tactic in - match res with - | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res - | _ -> res) - -let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic - ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) - ?hook ?(opaque = false) notations fixkind = - let deps = List.map (fun ({ Declare.Recthm.name; _ }, _, _) -> name) l in - List.iter - (fun ({ Declare.Recthm.name; typ; impargs; _ }, b, obls) -> - let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind) - notations obls ~impargs ~poly ~scope ~kind reduce ?hook - in progmap_add name (CEphemeron.create prg)) l; - let _defined = - List.fold_left (fun finished x -> - if finished then finished + else + let () = Flags.if_verbose (msg_generating_obl name) obls in + let () = State.add name prg in + let res = auto_solve_obligations (Some name) tactic in + match res with + | Remain rem -> + Flags.if_verbose (show_obligations ~msg:false) (Some name); + res + | _ -> res + +let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl) + ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior) + ?(kind = Decls.Definition) ?(reduce = reduce) ?hook ?(opaque = false) + notations fixkind = + let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in + let pm = + List.fold_left + (fun () ({Declare.Recthm.name; typ; impargs; _}, b, obls) -> + let prg = + ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps + (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce + ?hook + in + State.add name prg) + () l + in + let pm, _defined = + List.fold_left + (fun (pm, finished) x -> + if finished then (pm, finished) else let res = auto_solve_obligations (Some x) tactic in - match res with - | Defined _ -> - (* If one definition is turned into a constant, - the whole block is defined. *) true - | _ -> false) - false deps - in () + match res with + | Defined _ -> + (* If one definition is turned into a constant, + the whole block is defined. *) + (pm, true) + | _ -> (pm, false)) + (pm, false) deps + in + pm let admit_prog prg = let {obls; remaining} = prg.prg_obligations in @@ -365,39 +370,41 @@ let admit_prog prg = let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified - (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural) + (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; - ignore(DeclareObl.update_obls prg obls 0) + Declare.Obls.update_obls prg obls 0 +(* get_any_prog *) let rec admit_all_obligations () = - let prg = try Some (get_any_prog ()) with NoObligations _ -> None in + let prg = State.first_pending () in match prg with | None -> () | Some prg -> - admit_prog prg; + let _prog = admit_prog prg in admit_all_obligations () let admit_obligations n = match n with | None -> admit_all_obligations () | Some _ -> - let prg = get_prog_err n in - admit_prog prg + let prg = get_unique_prog n in + let _ = admit_prog prg in + () let next_obligation n tac = let prg = match n with - | None -> get_any_prog_err () - | Some _ -> get_prog_err n + | None -> State.first_pending () |> Option.get + | Some _ -> get_unique_prog n 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 - | None -> anomaly (Pp.str "Could not find a solvable obligation.") + | Some i -> i + | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.") in solve_obligation prg i tac diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 89ed4c3498..102a17b216 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -84,7 +84,7 @@ val add_definition : -> ?hook:Declare.Hook.t -> ?opaque:bool -> RetrieveObl.obligation_info - -> DeclareObl.progress + -> Declare.Obls.progress (* XXX: unify with MutualEntry *) @@ -102,7 +102,7 @@ val add_mutual_definitions : -> ?hook:Declare.Hook.t -> ?opaque:bool -> Vernacexpr.decl_notation list - -> DeclareObl.fixpoint_kind + -> Declare.Obls.fixpoint_kind -> unit (** Implementation of the [Obligation] command *) @@ -117,7 +117,7 @@ val next_obligation : (** Implementation of the [Solve Obligation] command *) val solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress + Names.Id.t option -> unit Proofview.tactic option -> Declare.Obls.progress val solve_all_obligations : unit Proofview.tactic option -> unit @@ -132,7 +132,5 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit val show_term : Names.Id.t option -> Pp.t val admit_obligations : Names.Id.t option -> unit -exception NoObligations of Names.Id.t option - val explain_no_obligations : Names.Id.t option -> Pp.t val check_program_libraries : unit -> unit diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml index e6c66ee503..150311ffaa 100644 --- a/vernac/pfedit.ml +++ b/vernac/pfedit.ml @@ -15,5 +15,5 @@ let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac = b, t, safe, uctx [@@ocaml.deprecated "Use [Proof.build_by_tactic]"] -let build_constant_by_tactic = Declare.build_constant_by_tactic +let build_constant_by_tactic = Declare.build_constant_by_tactic [@ocaml.warning "-3"] [@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"] diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml index 54d1db44a4..0c5bc39020 100644 --- a/vernac/proof_global.ml +++ b/vernac/proof_global.ml @@ -10,3 +10,4 @@ let get_proof = Declare.Proof.get_proof type opacity_flag = Declare.opacity_flag = | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"] | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"] +[@@ocaml.deprecated "Use [Declare.opacity_flag]"] diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index a09a473afe..1cad052bce 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -16,7 +16,6 @@ Metasyntax DeclareUniv RetrieveObl Declare -DeclareObl ComHints Canonical RecLemmas diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 35e625859b..106fed124e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -576,10 +576,14 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt let env = Global.env () in let sigma = Evd.from_env env in Some (snd (Hook.get f_interp_redexp env sigma r)) in - let do_definition = - ComDefinition.(if program_mode then do_definition_program else do_definition) in - do_definition ~name:name.v - ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook + if program_mode then + ComDefinition.do_definition_program ~name:name.v + ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook + else + let () = + ComDefinition.do_definition ~name:name.v + ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in + () (* NB: pstate argument to use combinators easily *) let vernac_start_proof ~atts kind l = @@ -1054,10 +1058,21 @@ let vernac_end_section {CAst.loc; v} = let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) +let msg_of_subsection ss id = + let kind = + match ss with + | Lib.OpenedModule (false,_,_,_) -> "module" + | Lib.OpenedModule (true,_,_,_) -> "module type" + | Lib.OpenedSection _ -> "section" + | _ -> "unknown" + in + Pp.str kind ++ spc () ++ Id.print id let vernac_end_segment ({v=id} as lid) = - DeclareObl.check_can_close lid.v; - match Lib.find_opening_node id with + let ss = Lib.find_opening_node id in + let what_for = msg_of_subsection ss lid.v in + Declare.Obls.check_solved_obligations ~what_for; + match ss with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid | Lib.OpenedSection _ -> vernac_end_section lid diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 19d41c4770..7d25e6b852 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -225,9 +225,9 @@ let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in let () = match pe with | Admitted -> - Lemmas.save_lemma_admitted_delayed ~proof ~info + Declare.save_lemma_admitted_delayed ~proof ~info | Proved (_,idopt) -> - Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in + Declare.save_lemma_proved_delayed ~proof ~info ~idopt in stack let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = |