diff options
100 files changed, 1402 insertions, 1323 deletions
diff --git a/.gitignore b/.gitignore index b665b2f86d..adbf9dd189 100644 --- a/.gitignore +++ b/.gitignore @@ -184,11 +184,6 @@ plugins/ssr/ssrvernac.ml META.coq # Files automatically generated by Dune. -plugins/*/dune -theories/*/dune -theories/*/*/dune -theories/*/*/*/dune -/user-contrib/Ltac2/dune *.install !Makefile.install diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index acbec54695..837636cbb3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-03-27-V12" + CACHEKEY: "bionic_coq-V2020-03-13-V69" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.ocamlformat b/.ocamlformat index 4480935e3b..62e609fb55 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.13.0 +version=0.14.0 profile=ocamlformat # to enable a whole directory, put "disable=false" in dir/.ocamlformat @@ -11,4 +11,4 @@ cases-exp-indent=2 field-space=loose exp-grouping=preserve break-cases=fit -doc-comments=before +doc-comments-val=before diff --git a/Makefile.doc b/Makefile.doc index 9da175f0e5..effd624cff 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -248,7 +248,7 @@ PLUGIN_MLGS := $(wildcard plugins/*/*.mlg) OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) -DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) +DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst) doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS) $(SHOW)'DOC_GRAM' diff --git a/Makefile.dune b/Makefile.dune index b77e78db69..b002c7709d 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,122 +1,109 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help voboot states world watch check # Main developer targets -.PHONY: coq coqide coqide-server # Package targets -.PHONY: quickbyte quickopt quickide # Partial / quick developer targets +.PHONY: help states world watch check # Main developer targets .PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets -.PHONY: test-suite release # Accessory targets +.PHONY: test-suite .PHONY: fmt ocheck ireport clean # Maintenance targets +.PHONY: voboot release install # Added just not to break old scripts # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short -BOOT_DIR=_build_boot -BOOT_CONTEXT=$(BOOT_DIR)/default - help: - @echo "Welcome to Coq's Dune-based build system. Targets are:" + @echo "Welcome to Coq's Dune-based build system. Common developer targets are:" @echo "" @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - world: build all public binaries and libraries" + @echo " - watch: build all public binaries and libraries [continuous build]" @echo " - check: build all ML files as fast as possible" + @echo " - test-suite: run Coq's test suite" @echo "" - @echo " - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]" - @echo " - coqide-server: build package coqide-server [XML protocol language server]" - @echo " - coqide: build package CoqIDE [gtk application]" + @echo " Note: these targets produce a developer build," + @echo " not suitable for distribution to end-users" @echo "" - @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" - @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" - @echo " - quickide: build main IDE files [client + server + prelude] using the optimizing compiler" + @echo " Documentation targets:" @echo "" - @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" - @echo " - release: build Coq in release mode" + @echo "" + @echo " Miscellaneous targets:" @echo "" @echo " - fmt: run ocamlformat on the codebase" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" + @echo "" + @echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:" + @echo "" + @echo " - use 'dune exec -- dev/shim/app-prelude args'" + @echo "" + @echo " Provided opam/dune packages are:" + @echo "" + @echo " - coq: base Coq package, toplevel compilers, tools, stdlib, no GTK" + @echo " - coqide-server: XML protocol language server" + @echo " - coqide: CoqIDE gtk application" + @echo "" + @echo " To build a package, you can use:" + @echo "" + @echo " - 'dune build package.install' : build package in developer mode" + @echo " - 'dune build -p package' : build package in release mode" + @echo "" + @echo " Packages _must_ be installed using release mode, use: 'dune install -p package'" + @echo " See Dune documentation for more information." -# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work. -plugins/ltac/dune: - @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune - -voboot: plugins/ltac/dune - dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps - dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d +voboot: + @echo "This target is empty and not needed anymore" -states: voboot - dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude +states: + dune build $(DUNEOPT) dev/shim/coqtop-prelude NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install -world: voboot +world: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -coq: voboot - dune build $(DUNEOPT) coq.install - -coqide: voboot - dune build $(DUNEOPT) coqide.install - -coqide-server: voboot - dune build $(DUNEOPT) coqide-server.install - -watch: voboot +watch: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w -check: voboot +check: dune build $(DUNEOPT) @check -COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc -PLUGIN_FILES=$(wildcard plugins/*/*.mlpack) -PRINTER_FILES=dev/top_printers.cma -QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc -QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe - -quickbyte: voboot - dune build $(DUNEOPT) $(QUICKBYTE_TARGETS) - -quickopt: voboot - dune build $(DUNEOPT) $(QUICKOPT_TARGETS) - -quickide: states - dune build $(DUNEOPT) dev/shim/coqide-prelude - -test-suite: voboot +test-suite: dune runtest --no-buffer $(DUNEOPT) -refman-html: voboot +refman-html: dune build @refman-html -refman-pdf: voboot +refman-pdf: dune build @refman-pdf -stdlib-html: voboot +stdlib-html: dune build @stdlib-html -apidoc: voboot +apidoc: dune build $(DUNEOPT) @doc -release: voboot +release: + @echo "release target is deprecated, use dune directly" dune build $(DUNEOPT) -p coq -fmt: voboot +# We define this target as to override Make's built-in one +install: + @echo "To install Coq using dune, use 'dune install -p PACKAGE' where" + @echo "PACKAGE is any of the packages defined by opam files in the root dira" + +fmt: dune build @fmt --auto-promote -ocheck: voboot +ocheck: dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all ireport: dune clean - dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps - dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d dune build $(DUNEOPT) @install --profile=ireport clean: diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 0bc30f0196..770cc5193e 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -6,37 +6,37 @@ variables: NJOBS: "2" jobs: -- job: Windows - pool: - vmImage: 'vs2017-win2016' +#- job: Windows +# pool: +# vmImage: 'vs2017-win2016' - steps: - - checkout: self - fetchDepth: 10 +# steps: +# - checkout: self +# fetchDepth: 10 # cygwin package list not checked for minimality - - script: | - powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" - SET CYGROOT=C:\cygwin64 - SET CYGCACHE=%CYGROOT%\var\cache\setup - setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3 - - SET TARGET_ARCH=x86_64-w64-mingw32 - SET CD_MFMT=%cd:\=/% - SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% - C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh - displayName: 'Install cygwin' - env: - CYGMIRROR: "http://mirror.easyname.at/cygwin" - - - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh - displayName: 'Install opam' - - - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh - displayName: 'Build Coq' - - - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh - displayName: 'Test Coq' +# - script: | +# powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" +# SET CYGROOT=C:\cygwin64 +# SET CYGCACHE=%CYGROOT%\var\cache\setup +# setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3 + +# SET TARGET_ARCH=x86_64-w64-mingw32 +# SET CD_MFMT=%cd:\=/% +# SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% +# C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh +# displayName: 'Install cygwin' +# env: +# CYGMIRROR: "http://mirror.easyname.at/cygwin" + +# - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh +# displayName: 'Install opam' + +# - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh +# displayName: 'Build Coq' + +# - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh +# displayName: 'Test Coq' - job: macOS pool: diff --git a/checker/check.ml b/checker/check.ml index bb3255338f..4212aac6ea 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -305,7 +305,7 @@ let marshal_in_segment ~validate ~value f ch = with _ -> user_err (str "Corrupted file " ++ quote (str f)) in - let () = Validate.validate ~debug:!Flags.debug value v in + let () = Validate.validate value v in let v = Analyze.instantiate v in Obj.obj v, stop, digest else diff --git a/checker/validate.ml b/checker/validate.ml index 66367cb002..20884c4d01 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -208,11 +208,10 @@ let print_frame = function | CtxField i -> Printf.sprintf "fld=%i" i | CtxTag i -> Printf.sprintf "tag=%i" i -let validate ~debug v (o, mem) = +let validate v (o, mem) = try val_gen v mem mt_ec o with ValidObjError(msg,ctx,obj) -> - (if debug then - let ctx = List.rev_map print_frame ctx in - print_endline ("Context: "^String.concat"/"ctx); - pr_obj mem obj); + let rctx = List.rev_map print_frame ctx in + print_endline ("Context: "^String.concat"/"rctx); + pr_obj mem obj; failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")") diff --git a/checker/validate.mli b/checker/validate.mli index 9ddc510e4a..1204b528f9 100644 --- a/checker/validate.mli +++ b/checker/validate.mli @@ -10,4 +10,4 @@ open Analyze -val validate : debug:bool -> Values.value -> data * obj LargeArray.t -> unit +val validate : Values.value -> data * obj LargeArray.t -> unit diff --git a/checker/values.ml b/checker/values.ml index 12f7135cdf..b9efce6948 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -372,6 +372,17 @@ let v_compiled_lib = let v_obj = Dyn +let v_globref = Sum("globref",0,[| + [|v_id|]; + [|v_cst|]; + [|v_ind|]; + [|v_cons|] + |]) + +let v_ext_gref = Sum("extended_global_reference",0,[|[|v_globref|];[|v_kn|]|]) + +let v_open_filter = Sum ("open_filter",1,[|[|v_hset v_ext_gref|]|]) + let rec v_aobjs = Sum("algebraic_objects", 0, [| [|v_libobjs|]; [|v_mp;v_subst|] @@ -383,7 +394,7 @@ and v_libobjt = Sum("Libobject.t",0, [| v_substobjs |]; [| v_aobjs |]; [| v_libobjs |]; - [| List v_mp |]; + [| List (v_pair v_open_filter v_mp)|]; [| v_obj |] |]) @@ -22,13 +22,12 @@ version: "dev" depends: [ "ocaml" { >= "4.05.0" } - "dune" { >= "2.0.0" } + "dune" { >= "2.5.0" } "ocamlfind" { build } "num" ] build: [ [ "./configure" "-prefix" prefix ] - [ "make" "-f" "Makefile.dune" "voboot" ] [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 0c8733c75a..e240ea3ba1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-03-27-V12" +# CACHEKEY: "bionic_coq-V2020-03-13-V69" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. -RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam +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 # Basic OPAM setup ENV NJOBS="2" \ @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.10.2" @@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" + BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh new file mode 100644 index 0000000000..4170799be7 --- /dev/null +++ b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh @@ -0,0 +1,6 @@ +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/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0506216541..8b0bf216e3 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system. -If you want to build the standard libraries and plugins you should -call `make -f Makefile.dune voboot`. It is usually enough to do that -once per-session. - More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. @@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and `coqide` in a fast build. In order to use them, do: ``` -$ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` @@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors: ## Dropping from coqtop: -After doing `make -f Makefile.dune voboot`, the following commands should work: +The following commands should work: ``` dune exec -- dev/shim/coqbyte-prelude > Drop. diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index b8a696ef21..fb84155392 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; - sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; + url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz"; + sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p"; }) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 1f33775a01..cfaa681d20 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -257,7 +257,7 @@ Activating the Printing of Coercions :name: Printing Coercion Specifies a set of qualids for which coercions are always displayed. Use the - :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. + :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. .. _coercions-classes-as-records: diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index d380d83d6c..928378f55e 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -112,13 +112,13 @@ You can override the display format for specified types by adding entries to the :name: Printing Record Specifies a set of qualids which are displayed as records. Use the - :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. + :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. .. table:: Printing Constructor @qualid :name: Printing Constructor Specifies a set of qualids which are displayed as constructors. Use the - :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. + :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. This syntax can also be used for pattern matching. diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index fb762a00f1..36ce2fdd25 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -273,14 +273,14 @@ Declaring Implicit Arguments .. prodn:: smart_qualid ::= @qualid | @by_notation - by_notation ::= @string {? % @ident } + by_notation ::= @string {? % @scope } argument_spec_block ::= @argument_spec | / | & - | ( {+ @argument_spec } ) {? % @ident } - | [ {+ @argument_spec } ] {? % @ident } - | %{ {+ @argument_spec } %} {? % @ident } - argument_spec ::= {? ! } @name {? % @ident } + | ( {+ @argument_spec } ) {? % @scope } + | [ {+ @argument_spec } ] {? % @scope } + | %{ {+ @argument_spec } %} {? % @scope } + argument_spec ::= {? ! } @name {? % @scope } more_implicits_block ::= @name | [ {+ @name } ] | %{ {+ @name } %} diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index a859aa46eb..57c8683aaa 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -238,7 +238,7 @@ written using the first destructuring let syntax. Note that this only applies to pattern matching instances entered with :g:`match`. It doesn't affect pattern matching explicitly entered with a destructuring :g:`let`. - Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. + Use the :cmd:`Add` and :cmd:`Remove` commands to update this set. Printing matching on booleans @@ -252,7 +252,7 @@ which types are written this way: :name: Printing If Specifies a set of qualids for which pattern matching is displayed using - ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add` and :cmd:`Remove` commands to update this set. This example emphasizes what the printing settings offer. @@ -422,7 +422,12 @@ are now available through the dot notation. If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of :token:`module_binder`\s. -.. cmd:: Import {+ @qualid } +.. cmd:: Import {+ @filtered_import } + + .. insertprodn filtered_import filtered_import + + .. prodn:: + filtered_import ::= @qualid {? ( {+, @qualid {? ( .. ) } } ) } If :token:`qualid` denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names. @@ -465,12 +470,50 @@ are now available through the dot notation. Check B.T. -.. cmd:: Export {+ @qualid } + Appending a module name with a parenthesized list of names will + make only those names available with short names, not other names + defined in the module nor will it activate other features. + + The names to import may be constants, inductive types and + constructors, and notation aliases (for instance, Ltac definitions + cannot be selectively imported). If they are from an inner module + to the one being imported, they must be prefixed by the inner path. + + The name of an inductive type may also be followed by ``(..)`` to + import it, its constructors and its eliminators if they exist. For + this purpose "eliminator" means a constant in the same module whose + name is the inductive type's name suffixed by one of ``_sind``, + ``_ind``, ``_rec`` or ``_rect``. + + .. example:: + + .. coqtop:: reset in + + Module A. + Module B. + Inductive T := C. + Definition U := nat. + End B. + Definition Z := Prop. + End A. + Import A(B.T(..), Z). + + .. coqtop:: all + + Check B.T. + Check B.C. + Check Z. + Fail Check B.U. + Check A.B.U. + +.. cmd:: Export {+ @filtered_import } :name: Export Similar to :cmd:`Import`, except that when the module containing this command is imported, the :n:`{+ @qualid }` are imported as well. + The selective import syntax also works with Export. + .. exn:: @qualid is not a module. :undocumented: @@ -719,7 +762,7 @@ accessible, absolute names can never be hidden. Locate nat. -.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`. +.. seealso:: Commands :cmd:`Locate`. .. _libraries-and-filesystem: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index f4592f8f37..ccb236a174 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -161,7 +161,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. one_term ::= @term1 | @ @qualid {? @univ_annot } term1 ::= @term_projection - | @term0 % @ident + | @term0 % @scope | @term0 term0 ::= @qualid {? @univ_annot } | @sort @@ -373,12 +373,10 @@ the propositional implication and function types. Applications ------------ -The expression :n:`@term__fun @term` denotes the application of -:n:`@term__fun` (which is expected to have a function type) to -:token:`term`. +:n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`. -The expression :n:`@term__fun {+ @term__i }` denotes the application -of the term :n:`@term__fun` to the arguments :n:`@term__i`. It is +:n:`@term__fun {+ @term__i }` denotes applying +:n:`@term__fun` to the arguments :n:`@term__i`. It is equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: associativity is to the left. @@ -458,7 +456,7 @@ Definition by cases: match pattern10 ::= @pattern1 as @name | @pattern1 {* @pattern1 } | @ @qualid {* @pattern1 } - pattern1 ::= @pattern0 % @ident + pattern1 ::= @pattern0 % @scope | @pattern0 pattern0 ::= @qualid | %{%| {* @qualid := @pattern } %|%} @@ -636,13 +634,18 @@ co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When The Vernacular ============== -.. insertprodn vernacular vernacular +.. insertprodn vernacular sentence .. prodn:: - vernacular ::= {* {? @all_attrs } {| @command | @ltac_expr } . } - -The top-level input to |Coq| is a series of :production:`command`\s and :production:`tactic`\s, -each terminated with a period + vernacular ::= {* @sentence } + sentence ::= {? @all_attrs } @command . + | {? @all_attrs } {? @num : } @query_command . + | {? @all_attrs } {? @toplevel_selector } @ltac_expr {| . | ... } + | @control_command + +The top-level input to |Coq| is a series of :n:`@sentence`\s, +which are :production:`tactic`\s or :production:`command`\s, +generally terminated with a period and optionally decorated with :ref:`gallina-attributes`. :n:`@ltac_expr` syntax supports both simple and compound tactics. For example: ``split`` is a simple tactic while ``split; auto`` combines two simple tactics. @@ -718,7 +721,7 @@ has type :n:`@type`. :name: @ident already exists. (Axiom) :undocumented: -.. warn:: @ident is declared as a local axiom [local-declaration,scope] +.. warn:: @ident is declared as a local axiom Warning generated when using :cmd:`Variable` or its equivalent instead of :n:`Local Parameter` or its equivalent. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 958d295219..545bba4930 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -380,7 +380,7 @@ Compiled libraries checker (coqchk) ---------------------------------------- The ``coqchk`` command takes a list of library paths as argument, described either -by their logical name or by their physical filename, hich must end in ``.vo``. The +by their logical name or by their physical filename, which must end in ``.vo``. The corresponding compiled libraries (``.vo`` files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type checked. The effect of ``coqchk`` is only to return with diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index d61e5ddce7..921c7bbbf7 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -42,6 +42,8 @@ As of today it is possible to build Coq projects using two tools: - coq_makefile, which is distributed by Coq and is based on generating a makefile, - Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries. +.. _coq_makefile: + Building a |Coq| project with coq_makefile ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b2b426ada5..62708b01ed 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -258,6 +258,9 @@ following form: Goal selectors ~~~~~~~~~~~~~~ +.. todo: mention this applies to Print commands and the Info command + + We can restrict the application of a tactic to a subset of the currently focused goals with: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 03eebc32f9..3b5233502d 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -41,8 +41,8 @@ terms are called *proof terms*. .. _proof-editing-mode: -Switching on/off the proof editing mode -------------------------------------------- +Entering and leaving proof editing mode +--------------------------------------- The proof editing mode is entered by asserting a statement, which typically is the assertion of a theorem using an assertion command like :cmd:`Theorem`. The diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 19573eee43..6a280b74c2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -51,6 +51,11 @@ specified, the default selector is used. tactic_invocation : `toplevel_selector` : `tactic`. : `tactic`. +.. todo: fully describe selectors. At the moment, ltac has a fairly complete description + +.. todo: mention selectors can be applied to some commands, such as + Check, Search, SearchHead, SearchPattern, SearchRewrite. + .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -3032,8 +3037,8 @@ following: For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. -.. tacn:: cbv {* @flag} - lazy {* @flag} +.. tacn:: {? @strategy_flag } + lazy {? @strategy_flag } :name: cbv; lazy These parameterized reduction tactics apply to any goal and perform diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index dacfcb3d5f..7d031b9b7a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -6,18 +6,28 @@ Vernacular commands .. _displaying: Displaying --------------- +---------- .. _Print: -.. cmd:: Print @qualid - :name: Print +.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list } + + .. insertprodn univ_name_list univ_name_list + + .. prodn:: + univ_name_list ::= @%{ {* @name } %} - This command displays on the screen information about the declared or - defined object referred by :n:`@qualid`. + Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`. - Error messages: + * :n:`Term` - a syntactic marker to allow printing a term + that is the same as one of the various :n:`Print` commands. For example, + :cmd:`Print All` is a different command, while :n:`Print Term All` shows + information on the object whose name is ":n:`All`". + + * :n:`@univ_name_list` - locally renames the + polymorphic universes of :n:`@smart_qualid`. + The name `_` means the usual name is printed. .. exn:: @qualid not a defined object. :undocumented: @@ -29,48 +39,22 @@ Displaying :undocumented: - .. cmdv:: Print Term @qualid - :name: Print Term - - This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid` - denotes a global constant. - - .. cmdv:: Print {? Term } @qualid\@@name - - This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the usual name is printed. - - -.. cmd:: About @qualid - :name: About - - This displays various information about the object - denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive, - constructor, abbreviation, …), long name, type, implicit arguments and - argument scopes. It does not print the body of definitions or proofs. - - .. cmdv:: About @qualid\@@name - - This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the usual name is printed. - - .. cmd:: Print All This command displays information about the current state of the environment, including sections and modules. - .. cmdv:: Inspect @num - :name: Inspect +.. cmd:: Inspect @num - This command displays the :n:`@num` last objects of the - current environment, including sections and modules. + This command displays the :n:`@num` last objects of the + current environment, including sections and modules. - .. cmdv:: Print Section @ident +.. cmd:: Print Section @qualid - The name :n:`@ident` should correspond to a currently open section, - this command displays the objects defined since the beginning of this - section. + Displays the objects defined since the beginning of the section named :n:`@qualid`. + + .. todo: "A.B" is permitted but unnecessary for modules/sections. + should the command just take an @ident? .. _flags-options-tables: @@ -81,9 +65,9 @@ Flags, Options and Tables Coq has many settings to control its behavior. Setting types include flags, options and tables: -* A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`. -* An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. -* A :production:`table` contains a set of strings or qualids. +* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`. +* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A *table* contains a set of strings or qualids. * In addition, some commands provide settings, such as :cmd:`Extraction Language`. .. FIXME Convert "Extraction Language" to an option. @@ -91,68 +75,64 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: Set @flag +.. cmd:: Set @setting_name {? {| @int | @string } } :name: Set - Sets :token:`flag` on. + .. insertprodn setting_name setting_name -.. cmd:: Unset @flag - :name: Unset + .. prodn:: + setting_name ::= {+ @ident } - Sets :token:`flag` off. + If :n:`@setting_name` is a flag, no value may be provided; the flag + is set to on. + If :n:`@setting_name` is an option, a value of the appropriate type + must be provided; the option is set to the specified value. -.. cmd:: Test @flag + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here <set_unset_scope_qualifiers>`. - Prints the current value of :token:`flag`. + .. warn:: There is no option @setting_name. + This message also appears for unknown flags. -.. cmd:: Set @option {| @num | @string } - :name: Set @option - - Sets :token:`option` to the specified value. - -.. cmd:: Unset @option - :name: Unset @option - - Sets :token:`option` to its default value. - -.. cmd:: Test @option - - Prints the current value of :token:`option`. - -.. cmd:: Print Options +.. cmd:: Unset @setting_name + :name: Unset - Prints the current value of all flags and options, and the names of all tables. + If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is + set to its default value. + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: Add @table {| @string | @qualid } - :name: Add @table +.. cmd:: Add @setting_name {+ {| @qualid | @string } } - Adds the specified value to :token:`table`. + Adds the specified values to the table :n:`@setting_name`. -.. cmd:: Remove @table {| @string | @qualid } - :name: Remove @table +.. cmd:: Remove @setting_name {+ {| @qualid | @string } } - Removes the specified value from :token:`table`. + Removes the specified value from the table :n:`@setting_name`. -.. cmd:: Test @table for {| @string | @qualid } - :name: Test @table for +.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } } - Reports whether :token:`table` contains the specified value. + If :n:`@setting_name` is a flag or option, prints its current value. + If :n:`@setting_name` is a table: if the `for` clause is specified, reports + whether the table contains each specified value, otherise this is equivalent to + :cmd:`Print Table`. The `for` clause is not valid for flags and options. -.. cmd:: Print Table @table - :name: Print Table @table +.. cmd:: Print Options - Prints the values in :token:`table`. + Prints the current value of all flags and options, and the names of all tables. -.. cmd:: Test @table +.. cmd:: Print Table @setting_name - A synonym for :cmd:`Print Table @table`. + Prints the values in the table :n:`@setting_name`. .. cmd:: Print Tables A synonym for :cmd:`Print Options`. +.. _set_unset_scope_qualifiers: + Locality attributes supported by :cmd:`Set` and :cmd:`Unset` ```````````````````````````````````````````````````````````` @@ -185,194 +165,128 @@ Newly opened modules and sections inherit the current settings. arguments ``-set`` and ``-unset`` for setting flags and options (cf. :ref:`command-line-options`). -.. _requests-to-the-environment: +Query commands +-------------- -Requests to the environment -------------------------------- +Unlike other commands, :production:`query_command`\s may be prefixed with +a goal selector (:n:`@num:`) to specify which goal context it applies to. +If no selector is provided, +the command applies to the current goal. If no proof is open, then the command only applies +to accessible objects. (see Section :ref:`invocation-of-tactics`). -.. cmd:: Check @term +.. cmd:: About @smart_qualid {? @univ_name_list } - This command displays the type of :n:`@term`. When called in proof mode, the - term is checked in the local context of the current subgoal. - - .. cmdv:: @selector: Check @term + Displays information about the :n:`@smart_qualid` object, which, + if a proof is open, may be a hypothesis of the selected goal, + or an accessible theorem, axiom, etc.: + its kind (module, constant, assumption, inductive, + constructor, abbreviation, …), long name, type, implicit arguments and + argument scopes. It does not print the body of definitions or proofs. - This variant specifies on which subgoal to perform typing - (see Section :ref:`invocation-of-tactics`). +.. cmd:: Check @term + Displays the type of :n:`@term`. When called in proof mode, the + term is checked in the local context of the selected goal. .. cmd:: Eval @red_expr in @term - This command performs the specified reduction on :n:`@term`, and displays - the resulting term with its type. The term to be reduced may depend on - hypothesis introduced in the first subgoal (if a proof is in - progress). + Performs the specified reduction on :n:`@term` and displays + the resulting term with its type. If a proof is open, :n:`@term` + may reference hypotheses of the selected goal. .. seealso:: Section :ref:`performingcomputations`. .. cmd:: Compute @term - This command performs a call-by-value evaluation of term by using the - bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in`` - :n:`@term`. + Evaluates :n:`@term` using the bytecode-based virtual machine. + It is a shortcut for :cmd:`Eval` :n:`vm_compute in @term`. .. seealso:: Section :ref:`performingcomputations`. +.. cmd:: Search {+ {? - } @search_item } {? {| inside | outside } {+ @qualid } } -.. cmd:: Print Assumptions @qualid - - This commands display all the assumptions (axioms, parameters and - variables) a theorem or definition depends on. Especially, it informs - on the assumptions with respect to which the validity of a theorem - relies. - - .. cmdv:: Print Opaque Dependencies @qualid - :name: Print Opaque Dependencies - - Displays the set of opaque constants :n:`@qualid` relies on in addition to - the assumptions. - - .. cmdv:: Print Transparent Dependencies @qualid - :name: Print Transparent Dependencies - - Displays the set of transparent constants :n:`@qualid` relies on - in addition to the assumptions. - - .. cmdv:: Print All Dependencies @qualid - :name: Print All Dependencies - - Displays all assumptions and constants :n:`@qualid` relies on. - - -.. cmd:: Search @qualid - - This command displays the name and type of all objects (hypothesis of - the current goal, theorems, axioms, etc) of the current context whose - statement contains :n:`@qualid`. This command is useful to remind the user - of the name of library lemmas. - - .. exn:: The reference @qualid was not found in the current environment. - - There is no constant in the environment named qualid. - - .. cmdv:: Search @string - - If :n:`@string` is a valid identifier, this command - displays the name and type of all objects (theorems, axioms, etc) of - the current context whose name contains string. If string is a - notation’s string denoting some reference :n:`@qualid` (referred to by its - main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or - `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`. - - .. cmdv:: Search @string%@ident - - The string string must be a notation or the main - symbol of a notation which is then interpreted in the scope bound to - the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`). - - .. cmdv:: Search @term_pattern + .. insertprodn search_item search_item - This searches for all statements or types of - definition that contains a subterm that matches the pattern - :token:`term_pattern` (holes of the pattern are either denoted by `_` or by - :n:`?@ident` when non linear patterns are expected). + .. prodn:: + search_item ::= @one_term + | @string {? % @scope } - .. cmdv:: Search {+ {? -}@term_pattern_string} + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context + matching :n:`@search_item`\s. + It's useful for finding the names of library lemmas. - where - :n:`@term_pattern_string` is a term_pattern, a string, or a string followed - by a scope delimiting key `%key`. This generalization of ``Search`` searches - for all objects whose statement or type contains a subterm matching - :n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference - qualid) and whose name contains all string of the request that - correspond to valid identifiers. If a term_pattern or a string is - prefixed by `-`, the search excludes the objects that mention that - term_pattern or that string. + * :n:`@one_term` - Search for objects containing a subterm matching the pattern + :n:`@one_term` in which holes of the pattern are indicated by `_` or :n:`?@ident`. + If the same :n:`?@ident` occurs more than once in the pattern, all occurrences must + match the same value. - .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid } + * :n:`@string` - If :n:`@string` is a substring of a valid identifier, + search for objects whose name contains :n:`@string`. If :n:`@string` is a notation + string associated with a :n:`@qualid`, that's equivalent to :cmd:`Search` :n:`@qualid`. + For example, specifying `"+"` or `"_ + _"`, which are notations for `Nat.add`, are equivalent + to :cmd:`Search` `Nat.add`. - This restricts the search to constructions defined in the modules - named by the given :n:`qualid` sequence. + * :n:`% @scope` - limits the search to the scope bound to + the delimiting key :n:`@scope`, such as, for example, :n:`%nat`. + This clause may be used only if :n:`@string` contains a notation string. + (see Section :ref:`LocalInterpretationRulesForNotations`) - .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid } + If you specify multiple :n:`@search_item`\s, all the conditions must be satisfied + for the object to be displayed. The minus sign `-` excludes objects that contain + the :n:`@search_item`. - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. + Additional clauses: - .. cmdv:: @selector: Search {+ {? -}@term_pattern_string} + * :n:`inside {+ @qualid }` - limit the search to the specified modules + * :n:`outside {+ @qualid }` - exclude the specified modules from the search - This specifies the goal on which to search hypothesis (see - Section :ref:`invocation-of-tactics`). - By default the 1st goal is searched. This variant can - be combined with other variants presented here. + .. exn:: Module/section @qualid not found. - .. example:: + There is no constant in the environment named :n:`@qualid`, where :n:`@qualid` + is in an `inside` or `outside` clause. - .. coqtop:: in + .. example:: :cmd:`Search` examples - Require Import ZArith. + .. coqtop:: in - .. coqtop:: all + Require Import ZArith. - Search Z.mul Z.add "distr". + .. coqtop:: all - Search "+"%Z "*"%Z "distr" -positive -Prop. + Search Z.mul Z.add "distr". + Search "+"%Z "*"%Z "distr" -Prop. + Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - Search (?x * _ + ?x * _)%Z outside OmegaLemmas. +.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } } -.. cmd:: SearchHead @term + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context that have the + form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term` + matches a prefix of `C`. For example, a :n:`@one_term` of `f _ b` + matches `f a b`, which is a prefix of `C` when `C` is `f a b c`. - This command displays the name and type of all hypothesis of the - current goal (if any) and theorems of the current context whose - statement’s conclusion has the form `(term t1 .. tn)`. This command is - useful to remind the user of the name of library lemmas. + See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - .. example:: + .. example:: :cmd:`SearchHead` examples .. coqtop:: reset all SearchHead le. - SearchHead (@eq bool). - .. cmdv:: SearchHead @term inside {+ @qualid } - - This restricts the search to constructions defined in the modules named - by the given :n:`qualid` sequence. - - .. cmdv:: SearchHead @term outside {+ @qualid } - - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. - - .. exn:: Module/section @qualid not found. - - No module :n:`@qualid` has been required (see Section :ref:`compiled-files`). - - .. cmdv:: @selector: SearchHead @term - - This specifies the goal on which to - search hypothesis (see Section :ref:`invocation-of-tactics`). - By default the 1st goal is searched. This variant can be combined - with other variants presented here. +.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } } - .. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``. + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context + ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern + :n:`@one_term`. + See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. -.. cmd:: SearchPattern @term - - This command displays the name and type of all hypothesis of the - current goal (if any) and theorems of the current context whose - statement’s conclusion or last hypothesis and conclusion matches the - expressionterm where holes in the latter are denoted by `_`. - It is a variant of :n:`Search @term_pattern` that does not look for subterms - but searches for statements whose conclusion has exactly the expected - form, or whose statement finishes by the given series of - hypothesis/conclusion. - - .. example:: + .. example:: :cmd:`SearchPattern` examples .. coqtop:: in @@ -381,123 +295,118 @@ Requests to the environment .. coqtop:: all SearchPattern (_ + _ = _ + _). - SearchPattern (nat -> bool). - SearchPattern (forall l : list _, _ l l). - Patterns need not be linear: you can express that the same expression - must occur in two places by using pattern variables `?ident`. - - - .. example:: - .. coqtop:: all SearchPattern (?X1 + _ = _ + ?X1). - .. cmdv:: SearchPattern @term inside {+ @qualid } +.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } } - This restricts the search to constructions defined in the modules - named by the given :n:`qualid` sequence. + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context that have the form + :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term` + matches either `LHS` or `RHS`. - .. cmdv:: SearchPattern @term outside {+ @qualid } + See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. + .. example:: :cmd:`SearchRewrite` examples - .. cmdv:: @selector: SearchPattern @term + .. coqtop:: in - This specifies the goal on which to - search hypothesis (see Section :ref:`invocation-of-tactics`). - By default the 1st goal is - searched. This variant can be combined with other variants presented - here. + Require Import Arith. + .. coqtop:: all -.. cmd:: SearchRewrite @term + SearchRewrite (_ + _ + _). - This command displays the name and type of all hypothesis of the - current goal (if any) and theorems of the current context whose - statement’s conclusion is an equality of which one side matches the - expression term. Holes in term are denoted by “_”. +.. table:: Search Blacklist @string + :name: Search Blacklist - .. example:: + Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, + :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + fully-qualified name contains any of the strings will be excluded from the + search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and + ``Private_``. - .. coqtop:: in + Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of + blacklisted strings. - Require Import Arith. - .. coqtop:: all +.. _requests-to-the-environment: - SearchRewrite (_ + _ + _). +Requests to the environment +------------------------------- - .. cmdv:: SearchRewrite @term inside {+ @qualid } +.. cmd:: Print Assumptions @smart_qualid - This restricts the search to constructions defined in the modules - named by the given :n:`qualid` sequence. + Displays all the assumptions (axioms, parameters and + variables) a theorem or definition depends on. - .. cmdv:: SearchRewrite @term outside {+ @qualid } + The message "Closed under the global context" indicates that the theorem or + definition has no dependencies. - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. +.. cmd:: Print Opaque Dependencies @smart_qualid - .. cmdv:: @selector: SearchRewrite @term + Displays the assumptions and opaque constants that :n:`@smart_qualid` depends on. - This specifies the goal on which to - search hypothesis (see Section :ref:`invocation-of-tactics`). - By default the 1st goal is - searched. This variant can be combined with other variants presented - here. +.. cmd:: Print Transparent Dependencies @smart_qualid -.. note:: + Displays the assumptions and transparent constants that :n:`@smart_qualid` depends on. - .. table:: Search Blacklist @string - :name: Search Blacklist +.. cmd:: Print All Dependencies @smart_qualid - Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, - :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose - fully-qualified name contains any of the strings will be excluded from the - search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and - ``Private_``. + Displays all the assumptions and constants :n:`@smart_qualid` depends on. - Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of - blacklisted strings. +.. cmd:: Locate @smart_qualid -.. cmd:: Locate @qualid + Displays the full name of objects from |Coq|'s various qualified namespaces such as terms, + modules and Ltac. It also displays notation definitions. - This command displays the full name of objects whose name is a prefix - of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in - which they are defined. It searches for objects from the different - qualified namespaces of |Coq|: terms, modules, Ltac, etc. + If the argument is: - .. example:: + * :n:`@qualid` - displays the full name of objects that + end with :n:`@qualid`, thereby showing the module they are defined in. + * :n:`@string {? "%" @ident }` - displays the definition of a notation. :n:`@string` + can be a single token in the notation such as "`->`" or a pattern that matches the + notation. See :ref:`locating-notations`. - .. coqtop:: all + .. todo somewhere we should list all the qualified namespaces - Locate nat. +.. cmd:: Locate Term @smart_qualid - Locate Datatypes.O. + Like :cmd:`Locate`, but limits the search to terms - Locate Init.Datatypes.O. +.. cmd:: Locate Module @qualid - Locate Coq.Init.Datatypes.O. + Like :cmd:`Locate`, but limits the search to modules - Locate I.Dont.Exist. +.. cmd:: Locate Ltac @qualid - .. cmdv:: Locate Term @qualid + Like :cmd:`Locate`, but limits the search to tactics - As Locate but restricted to terms. +.. cmd:: Locate Library @qualid - .. cmdv:: Locate Module @qualid + Displays the full name, status and file system path of the module :n:`@qualid`, whether loaded or not. + +.. cmd:: Locate File @string - As Locate but restricted to modules. + Displays the file system path of the file ending with :n:`@string`. + Typically, :n:`@string` has a suffix such as ``.cmo`` or ``.vo`` or ``.v`` file, such as :n:`Nat.v`. - .. cmdv:: Locate Ltac @qualid + .. todo: also works for directory names such as "Data" (parent of Nat.v) + also "Data/Nat.v" works, but not a substring match - As Locate but restricted to tactics. +.. example:: Locate examples -.. seealso:: Section :ref:`locating-notations` + .. coqtop:: all + + Locate nat. + Locate Datatypes.O. + Locate Init.Datatypes.O. + Locate Coq.Init.Datatypes.O. + Locate I.Dont.Exist. .. _printing-flags: @@ -522,35 +431,32 @@ Loading files |Coq| offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded -files are ASCII files containing sequences of commands for |Coq|’s +files are text files containing sequences of commands for |Coq|’s toplevel. This kind of file is called a *script* for |Coq|. The standard (and default) extension of |Coq|’s script files is .v. -.. cmd:: Load @ident +.. cmd:: Load {? Verbose } {| @string | @ident } - This command loads the file named :n:`ident`.v, searching successively in + Loads a file. If :n:`@ident` is specified, the command loads a file + named :n:`@ident.v`, searching successively in each of the directories specified in the *loadpath*. (see Section :ref:`libraries-and-filesystem`) - Files loaded this way cannot leave proofs open, and the ``Load`` - command cannot be used inside a proof either. - - .. cmdv:: Load @string + If :n:`@string` is specified, it must specify a complete filename. + `~` and .. abbreviations are + allowed as well as shell variables. If no extension is specified, |Coq| + will use the default extension ``.v``. - Loads the file denoted by the string :n:`@string`, where - string is any complete filename. Then the `~` and .. abbreviations are - allowed as well as shell variables. If no extension is specified, |Coq| - will use the default extension ``.v``. + Files loaded this way can't leave proofs open, nor can :cmd:`Load` + be used inside a proof. - .. cmdv:: Load Verbose @ident - Load Verbose @string + We discourage the use of :cmd:`Load`; use :cmd:`Require` instead. + :cmd:`Require` loads `.vo` files that were previously + compiled from `.v` files. - Display, while loading, - the answers of |Coq| to each command (including tactics) contained in - the loaded file. - - .. seealso:: Section :ref:`controlling-display`. + :n:`Verbose` displays the |Coq| output for each command and tactic + in the loaded file, as if the commands and tactics were entered interactively. .. exn:: Can’t find file @ident on loadpath. :undocumented: @@ -568,67 +474,50 @@ Compiled files This section describes the commands used to load compiled files (see Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A compiled -file is a particular case of module called *library file*. - - -.. cmd:: Require @qualid - - This command looks in the loadpath for a file containing module :n:`@qualid` - and adds the corresponding module to the environment of |Coq|. As - library files have dependencies in other library files, the command - :cmd:`Require` :n:`@qualid` recursively requires all library files the module - qualid depends on and adds the corresponding modules to the - environment of |Coq| too. |Coq| assumes that the compiled files have been - produced by a valid |Coq| compiler and their contents are then not - replayed nor rechecked. - - To locate the file in the file system, :n:`@qualid` is decomposed under the - form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical - directory of the file system that is mapped in |Coq| loadpath to the - logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between - physical directories and logical names at the time of requiring the - file must be consistent with the mapping used to compile the file. If - several files match, one of them is picked in an unspecified fashion. +file is a particular case of a module called a *library file*. - .. cmdv:: Require Import @qualid - :name: Require Import +.. cmd:: Require {? {| Import | Export } } {+ @qualid } + :name: Require; Require Import; Require Export - This loads and declares the module :n:`@qualid` - and its dependencies then imports the contents of :n:`@qualid` as described - for :cmd:`Import`. It does not import the modules that - :n:`@qualid` depends on unless these modules were themselves required in module - :n:`@qualid` - using :cmd:`Require Export`, or recursively required - through a series of :cmd:`Require Export`. If the module required has - already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as - :cmd:`Import` :n:`@qualid` would. + Loads compiled modules into the |Coq| environment. For each :n:`@qualid`, which has the form + :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented + by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated + filesystem directory. - .. cmdv:: Require Export @qualid - :name: Require Export + The process is applied recursively to all the loaded files; + if they contain :cmd:`Require` commands, those commands are executed as well. + The compiled files must have been compiled with the same version of |Coq|. + The compiled files are neither replayed nor rechecked. - This command acts as :cmd:`Require Import` :n:`@qualid`, - but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, - then the command :cmd:`Require Import` `A` also imports the module `B.` + * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined + in the module available by their short names + * :n:`Export` - additionally does an :cmd:`Export` on the loaded module, making components defined + in the module available by their short names *and* marking them to be exported by the current + module - .. cmdv:: Require {| Import | Export } {+ @qualid } + If the required module has already been loaded, :n:`Import` and :n:`Export` make the command + equivalent to :cmd:`Import` or :cmd:`Export`. + + The loadpath must contain the same mapping used to compile the file + (see Section :ref:`libraries-and-filesystem`). If + several files match, one of them is picked in an unspecified fashion. + Therefore, library authors should use a unique name for each module and + users are encouraged to use fully-qualified names + or the :cmd:`From ... Require` command to load files. - This loads the - modules named by the :token:`qualid` sequence and their recursive - dependencies. If - ``Import`` or ``Export`` is given, it also imports these modules and - all the recursive dependencies that were marked or transitively marked - as ``Export``. - .. cmdv:: From @dirpath Require @qualid - :name: From ... Require ... + .. todo common user error on dirpaths see https://github.com/coq/coq/pull/11961#discussion_r402852390 - This command acts as :cmd:`Require`, but picks - any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` - for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library - comes from a given package by making explicit its absolute root. + .. cmd:: From @dirpath Require {? {| Import | Export } } {+ @qualid } + :name: From ... Require - .. exn:: Cannot load qualid: no physical path bound to dirpath. + Works like :cmd:`Require`, but loads, for each :n:`@qualid`, + the library whose fully-qualified name matches :n:`@dirpath.{* @ident . }@qualid` + for some :n:`{* @ident . }`. This is useful to ensure that the :n:`@qualid` library + comes from a particular package. + + .. exn:: Cannot load @qualid: no physical path bound to @dirpath. :undocumented: .. exn:: Cannot find library foo in loadpath. @@ -637,7 +526,7 @@ file is a particular case of module called *library file*. file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`). - .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid. + .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library @qualid. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the @@ -651,13 +540,13 @@ file is a particular case of module called *library file*. |Coq| compiled module, or it was compiled with an incompatible version of |Coq|. - .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’. - - The library file :n:`@dirpath’` is indirectly required by the - ``Require`` command but it is bound in the current loadpath to the - file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at - the time it was compiled. + .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2. + The library :n:`@qualid__2` is indirectly required by a :cmd:`Require` or + :cmd:`From ... Require` command. The loadpath maps :n:`@qualid__2` to :n:`@ident.vo`, + which was compiled using a loadpath that bound it to :n:`@qualid__1`. Usually + the appropriate solution is to recompile :n:`@ident.v` using the correct loadpath. + See :ref:`libraries-and-filesystem`. .. warn:: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. @@ -672,27 +561,22 @@ file is a particular case of module called *library file*. .. cmd:: Declare ML Module {+ @string } - This commands loads the OCaml compiled files - with names given by the :token:`string` sequence - (dynamic link). It is mainly used to load tactics dynamically. The - files are searched into the current OCaml loadpath (see the - command :cmd:`Add ML Path`). - Loading of OCaml files is only possible under the bytecode version of - ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter - :ref:`thecoqcommands`), or when |Coq| has been compiled with a - version of OCaml that supports native Dynlink (≥ 3.11). + This commands dynamically loads OCaml compiled code from + a :n:`.mllib` file. + It is used to load plugins dynamically. The + files must be accessible in the current OCaml loadpath (see the + command :cmd:`Add ML Path`). The :n:`.mllib` suffix may be omitted. - .. cmdv:: Local Declare ML Module {+ @string } + This command is reserved for plugin developers, who should provide + a .v file containing the command. Users of the plugins will then generally + load the .v file. - This variant is not exported to the modules that import the module - where they occur, even if outside a section. + This command supports the :attr:`local` attribute. If present, + the listed files are not exported, even if they're outside a section. .. exn:: File not found on loadpath: @string. :undocumented: - .. exn:: Loading of ML object file forbidden in a native Coq. - :undocumented: - .. cmd:: Print ML Modules @@ -707,7 +591,7 @@ Loadpath ------------ Loadpaths are preferably managed using |Coq| command line options (see -Section `libraries-and-filesystem`) but there remain vernacular commands to manage them +Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them for practical purposes. Such commands are only meant to be issued in the toplevel, and using them in source files is discouraged. @@ -717,22 +601,27 @@ the toplevel, and using them in source files is discouraged. This command displays the current working directory. -.. cmd:: Cd @string +.. cmd:: Cd {? @string } - This command changes the current directory according to :token:`string` which - can be any valid path. + If :n:`@string` is specified, changes the current directory according to :token:`string` which + can be any valid path. Otherwise, it displays the current directory. - .. cmdv:: Cd - Is equivalent to Pwd. +.. cmd:: Add LoadPath @string as @dirpath + .. insertprodn dirpath dirpath -.. cmd:: Add LoadPath @string as @dirpath + .. prodn:: + dirpath ::= {* @ident . } @ident This command is equivalent to the command line option - :n:`-Q @string @dirpath`. It adds the physical directory string to the current - |Coq| loadpath and maps it to the logical directory dirpath. + :n:`-Q @string @dirpath`. It adds a mapping to the loadpath from + the logical name :n:`@dirpath` to the file system directory :n:`@string`. + * :n:`@dirpath` is a prefix of a module name. The module name hierarchy + follows the file system hierarchy. On Linux, for example, the prefix + `A.B.C` maps to the directory :n:`@string/B/C`. Avoid using spaces after a `.` in the + path because the parser will interpret that as the end of a command or tactic. .. cmd:: Add Rec LoadPath @string as @dirpath @@ -746,42 +635,24 @@ the toplevel, and using them in source files is discouraged. This command removes the path :n:`@string` from the current |Coq| loadpath. -.. cmd:: Print LoadPath +.. cmd:: Print LoadPath {? @dirpath } - This command displays the current |Coq| loadpath. - - .. cmdv:: Print LoadPath @dirpath - - Works as :cmd:`Print LoadPath` but displays only - the paths that extend the :n:`@dirpath` prefix. + This command displays the current |Coq| loadpath. If :n:`@dirpath` is specified, + displays only the paths that extend that prefix. .. cmd:: Add ML Path @string This command adds the path :n:`@string` to the current OCaml - loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). + loadpath (cf. :cmd:`Declare ML Module`). -.. cmd:: Print ML Path @string +.. cmd:: Print ML Path This command displays the current OCaml loadpath. This command makes sense only under the bytecode version of ``coqtop``, i.e. using option ``-byte`` - (see the command Declare ML Module in Section :ref:`compiled-files`). - -.. _locate-file: - -.. cmd:: Locate File @string - - This command displays the location of file string in the current - loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file. - - -.. cmd:: Locate Library @dirpath - - This command gives the status of the |Coq| module dirpath. It tells if - the module is loaded and if not searches in the load path for a module - of logical name :n:`@dirpath`. + (cf. :cmd:`Declare ML Module`). .. _backtracking: @@ -804,30 +675,22 @@ interactively, they cannot be part of a vernacular file loaded via .. exn:: @ident: no such entry. :undocumented: - .. cmdv:: Reset Initial +.. cmd:: Reset Initial - Goes back to the initial state, just after the start - of the interactive session. + Goes back to the initial state, just after the start + of the interactive session. -.. cmd:: Back +.. cmd:: Back {? @num } - This command undoes all the effects of the last vernacular command. - Commands read from a vernacular file via a :cmd:`Load` are considered as a - single command. Proof management commands are also handled by this - command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than - one command in order to reach a state where the proof management - information is available. For instance, when the last command is a - :cmd:`Qed`, the management information about the closed proof has been - discarded. In this case, :cmd:`Back` will then undo all the proof steps up to - the statement of this proof. - - .. cmdv:: Back @num - - Undo :n:`@num` vernacular commands. As for Back, some extra - commands may be undone in order to reach an adequate state. For - instance Back :n:`@num` will not re-enter a closed proof, but rather go just - before that proof. + Undoes all the effects of the last :n:`@num @sentence`\s. If + :n:`@num` is not specified, the command undoes one sentence. + Sentences read from a `.v` file via a :cmd:`Load` are considered a + single sentence. While :cmd:`Back` can undo tactics and commands executed + within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all + the statements executed within are thereafter considered a single sentence. + :cmd:`Back` immediately following :cmd:`Qed` gets you back to the state + just after the statement of the proof. .. exn:: Invalid backtrack. @@ -848,18 +711,17 @@ interactively, they cannot be part of a vernacular file loaded via Quitting and debugging -------------------------- - .. cmd:: Quit - This command permits to quit |Coq|. + Causes |Coq| to exit. Valid only in coqtop. .. cmd:: Drop - This is used mostly as a debug facility by |Coq|’s implementers and does - not concern the casual user. This command permits to leave |Coq| - temporarily and enter the OCaml toplevel. The OCaml - command: + This command temporarily enters the OCaml toplevel. + It is a debug facility used by |Coq|’s implementers. Valid only in the + bytecode version of coqtop. + The OCaml command: :: @@ -884,49 +746,53 @@ Quitting and debugging (see Section `customization-by-environment-variables`). -.. TODO : command is not a syntax entry - -.. cmd:: Time @command +.. cmd:: Time @sentence - This command executes the vernacular command :n:`@command` and displays the + Executes :n:`@sentence` and displays the time needed to execute it. -.. cmd:: Redirect @string @command +.. cmd:: Redirect @string @sentence - This command executes the vernacular command :n:`@command`, redirecting its - output to ":n:`@string`.out". + Executes :n:`@sentence`, redirecting its + output to the file ":n:`@string`.out". -.. cmd:: Timeout @num @command +.. cmd:: Timeout @num @sentence - This command executes the vernacular command :n:`@command`. If the command - has not terminated after the time specified by the :n:`@num` (time - expressed in seconds), then it is interrupted and an error message is + Executes :n:`@sentence`. If the operation + has not terminated after :n:`@num` seconds, then it is interrupted and an error message is displayed. .. opt:: Default Timeout @num :name: Default Timeout - This option controls a default timeout for subsequent commands, as if they - were passed to a :cmd:`Timeout` command. Commands already starting by a - :cmd:`Timeout` are unaffected. + If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`, + except for :cmd:`Timeout` commands themselves. If unset, + no timeout is applied. -.. cmd:: Fail @command +.. cmd:: Fail @sentence For debugging scripts, sometimes it is desirable to know whether a - command or a tactic fails. If the given :n:`@command` fails, then - :n:`Fail @command` succeeds (excepts in the case of - critical errors, like a "stack overflow"), without changing the - proof state, and in interactive mode, the system prints a message + command or a tactic fails. If :n:`@sentence` fails, then + :n:`Fail @sentence` succeeds (except for + critical errors, such as "stack overflow"), without changing the + proof state. In interactive mode, the system prints a message confirming the failure. .. exn:: The command has not failed! - If the given :n:`@command` succeeds, then :n:`Fail @command` + If the given :n:`@command` succeeds, then :n:`Fail @sentence` fails with this error message. +.. note:: + + :cmd:`Time`, :cmd:`Redirect`, :cmd:`Timeout` and :cmd:`Fail` are + :production:`control_command`\s. For these commands, attributes and goal + selectors, when specified, are part of the :n:`@sentence` argument, and thus come after + the control command prefix and before the inner command or tactic. For + example: `Time #[ local ] Definition foo := 0.` or `Fail Timeout 10 all: auto.` .. _controlling-display: @@ -1008,13 +874,16 @@ as numbers, and for reflection-based tactics. The commands to fine- tune the reduction strategies and the lazy conversion algorithm are described first. -.. cmd:: Opaque {+ @qualid } +.. cmd:: Opaque {+ @smart_qualid } + + This command accepts the :attr:`global` attribute. By default, the scope + of :cmd:`Opaque` is limited to the current section or module. This command has an effect on unfoldable constants, i.e. on constants defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc, or by a proof ended by :cmd:`Defined`. The command tells not to unfold the - constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding + constants in the :n:`@smart_qualid` sequence in tactics using δ-conversion (unfolding a constant is replacing it by its definition). :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling @@ -1022,24 +891,15 @@ described first. has to check the conversion (see Section :ref:`conversion-rules`) of two distinct applied constants. - .. cmdv:: Global Opaque {+ @qualid } - :name: Global Opaque - - The scope of :cmd:`Opaque` is limited to the current section, or current - file, unless the variant :cmd:`Global Opaque` is used. - .. seealso:: Sections :ref:`performingcomputations`, :ref:`tactics-automating`, :ref:`proof-editing-mode` - .. exn:: The reference @qualid was not found in the current environment. - - There is no constant referred by :n:`@qualid` in the environment. - Nevertheless, if you asked :cmd:`Opaque` `foo` `bar` and if `bar` does - not exist, `foo` is set opaque. +.. cmd:: Transparent {+ @smart_qualid } -.. cmd:: Transparent {+ @qualid } + This command accepts the :attr:`global` attribute. By default, the scope + of :cmd:`Transparent` is limited to the current section or module. This command is the converse of :cmd:`Opaque` and it applies on unfoldable constants to restore their unfoldability after an Opaque command. @@ -1052,16 +912,9 @@ described first. the usual defined constants, whose actual values are of course relevant in general. - .. cmdv:: Global Transparent {+ @qualid } - :name: Global Transparent - - The scope of Transparent is limited to the current section, or current - file, unless the variant :cmd:`Global Transparent` is - used. - .. exn:: The reference @qualid was not found in the current environment. - There is no constant referred by :n:`@qualid` in the environment. + There is no constant named :n:`@qualid` in the environment. .. seealso:: @@ -1070,63 +923,66 @@ described first. .. _vernac-strategy: -.. cmd:: Strategy @level [ {+ @qualid } ] +.. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - This command generalizes the behavior of Opaque and Transparent + .. insertprodn strategy_level strategy_level + + .. prodn:: + strategy_level ::= opaque + | @int + | expand + | transparent + + This command accepts the :attr:`local` attribute, which limits its effect + to the current section or module, in which case the section and module + behavior is the same as :cmd:`Opaque` and :cmd:`Transparent` (without :attr:`global`). + + This command generalizes the behavior of the :cmd:`Opaque` and :cmd:`Transparent` commands. It is used to fine-tune the strategy for unfolding constants, both at the tactic level and at the kernel level. This - command associates a level to the qualified names in the :n:`@qualid` + command associates a :n:`@strategy_level` with the qualified names in the :n:`@smart_qualid` sequence. Whenever two expressions with two distinct head constants are compared (for instance, this comparison can be triggered by a type cast), the one with lower level is expanded first. In case of a tie, the second one (appearing in the cast type) is expanded. - .. prodn:: level ::= {| opaque | @num | expand } - Levels can be one of the following (higher to lower): + ``opaque`` : level of opaque constants. They cannot be expanded by tactics (behaves like +∞, see next item). - + :n:`@num` : levels indexed by an integer. Level 0 corresponds to the + + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the default behavior, which corresponds to transparent constants. This - level can also be referred to as transparent. Negative levels + level can also be referred to as ``transparent``. Negative levels correspond to constants to be expanded before normal transparent constants, while positive levels correspond to constants to be expanded after normal transparent constants. + ``expand`` : level of constants that should be expanded first (behaves like −∞) + + ``transparent`` : Equivalent to level 0 - .. cmdv:: Local Strategy @level [ {+ @qualid } ] +.. cmd:: Print Strategy @smart_qualid - These directives survive section and module closure, unless the - command is prefixed by ``Local``. In the latter case, the behavior - regarding sections and modules is the same as for the :cmd:`Transparent` and - :cmd:`Opaque` commands. - - -.. cmd:: Print Strategy @qualid - - This command prints the strategy currently associated to :n:`@qualid`. It - fails if :n:`@qualid` is not an unfoldable reference, that is, neither a + This command prints the strategy currently associated with :n:`@smart_qualid`. It + fails if :n:`@smart_qualid` is not an unfoldable reference, that is, neither a variable nor a constant. .. exn:: The reference is not unfoldable. :undocumented: - .. cmdv:: Print Strategies +.. cmd:: Print Strategies - Print all the currently non-transparent strategies. + Print all the currently non-transparent strategies. .. cmd:: Declare Reduction @ident := @red_expr - This command allows giving a short name to a reduction expression, for + Declares a short name for the reduction expression :n:`@red_expr`, for instance ``lazy beta delta [foo bar]``. This short name can then be used - in :n:`Eval @ident in` or ``eval`` directives. This command - accepts the - ``Local`` modifier, for discarding this reduction name at the end of the - file or module. For the moment, the name is not qualified. In + in :n:`Eval @ident in` or ``eval`` constructs. This command + accepts the :attr:`local` attribute, which indicates that the reduction + will be discarded at the end of the + file or module. The name is not qualified. In particular declaring the same name in several modules or in several functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but @@ -1272,14 +1128,15 @@ in support libraries of plug-ins. .. _exposing-constants-to-ocaml-libraries: Exposing constants to OCaml libraries -```````````````````````````````````````````````````````````````` +````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 - This command exposes the constant :n:`@qualid__1` to OCaml libraries under - the name :n:`@qualid__2`. This constant can then be dynamically located - calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known - where is the constant defined (file, module, library, etc.). + Makes the constant :n:`@qualid__1` accessible to OCaml libraries under + the name :n:`@qualid__2`. The constant can then be dynamically located + in OCaml code by + calling :n:`Coqlib.lib_ref "@qualid__2"`. The OCaml code doesn't need + to know where the constant is defined (what file, module, library, etc.). As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, the constant is exposed to the kernel. For instance, the `Int63` module @@ -1289,27 +1146,41 @@ Exposing constants to OCaml libraries Register bool as kernel.ind_bool. - This makes the kernel aware of what is the type of boolean values. This - information is used for instance to define the return type of the - :g:`#int63_eq` primitive. + This makes the kernel aware of the `bool` type, which is used, for example, + to define the return type of the :g:`#int63_eq` primitive. .. seealso:: :ref:`primitive-integers` Inlining hints for the fast reduction machines -```````````````````````````````````````````````````````````````` +`````````````````````````````````````````````` .. cmd:: Register Inline @qualid - This command gives as a hint to the reduction machines (VM and native) that + Gives a hint to the reduction machines (VM and native) that the body of the constant :n:`@qualid` should be inlined in the generated code. Registering primitive operations ```````````````````````````````` -.. cmd:: Primitive @ident__1 := #@ident__2. +.. cmd:: Primitive @ident {? : @term } := #@ident__prim + + Makes the primitive type or primitive operator :n:`#@ident__prim` defined in OCaml + accessible in |Coq| commands and tactics. + For internal use by implementors of |Coq|'s standard library or standard library + replacements. No space is allowed after the `#`. Invalid values give a syntax + error. + + For example, the standard library files `Int63.v` and `PrimFloat.v` use :cmd:`Primitive` + to support, respectively, the features described in :ref:`primitive-integers` and + :ref:`primitive-floats`. + + The types associated with an operator must be declared to the kernel before declaring operations + that use the type. Do this with :cmd:`Primitive` for primitive types and + :cmd:`Register` with the :g:`kernel` prefix for other types. For example, + in `Int63.v`, `#int63_type` must be declared before the associated operations. + + .. exn:: The type @ident must be registered before this construction can be typechecked. + :undocumented: - Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When - running this command, the type of the primitive should be already known by - the kernel (this is achieved through this command for primitive types and - through the :cmd:`Register` command with the :g:`kernel` name-space for other - types). + The type must be defined with :cmd:`Primitive` command before this + :cmd:`Primitive` command (declaring an operation using the type) will succeed. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 669975ba7e..512378b9fc 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -902,7 +902,7 @@ Syntax of notations +++++++++++++++++++ The different syntactic forms taken by the commands declaring -notations are given below. The optional :production:`scope` is described in +notations are given below. The optional :n:`@scope` is described in :ref:`Scopes`. .. productionlist:: coq @@ -1001,6 +1001,11 @@ Notations disappear when a section is closed. Interpretation scopes ---------------------- + .. insertprodn scope scope + + .. prodn:: + scope ::= @ident + An *interpretation scope* is a set of notations for terms with their interpretations. Interpretation scopes provide a weak, purely syntactical form of notation overloading: the same notation, for @@ -1090,7 +1095,7 @@ Local opening of an interpretation scope It is possible to locally extend the interpretation scope stack using the syntax :n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a -special identifier called *delimiting key* and bound to a given scope. +special identifier called a *delimiting key* and bound to a given scope. In such a situation, the term term, and all its subterms, are interpreted in the scope stack extended with the scope bound to :token:`ident`. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 60b845c4be..5034d9a3c9 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -151,8 +151,7 @@ fields: [ | DELETENT ] dirpath: [ | REPLACE ident LIST0 field -| WITH ident -| dirpath field_ident +| WITH LIST0 ( ident "." ) ident ] binders: [ @@ -220,6 +219,15 @@ tactic_expr0: [ | WITH "[>" tactic_then_gen "]" ] +(* lexer token *) +IDENT: [ +| ident +] + +scope: [ +| IDENT +] + operconstr100: [ | MOVETO term_cast operconstr99 "<:" operconstr200 | MOVETO term_cast operconstr99 "<<:" operconstr200 @@ -240,7 +248,9 @@ operconstr9: [ operconstr1: [ | REPLACE operconstr0 ".(" global LIST0 appl_arg ")" -| WITH operconstr0 ".(" global LIST0 appl_arg ")" +| WITH operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *) +| REPLACE operconstr0 "%" IDENT +| WITH operconstr0 "%" scope | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")" | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" ] @@ -364,6 +374,11 @@ pattern10: [ | DELETE pattern1 ] +pattern1: [ +| REPLACE pattern0 "%" IDENT +| WITH pattern0 "%" scope +] + pattern0: [ | REPLACE "(" pattern200 ")" | WITH "(" LIST1 pattern200 SEP "|" ")" @@ -419,6 +434,8 @@ gallina: [ | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) | REPLACE "Scheme" LIST1 scheme SEP "with" | WITH "Scheme" scheme LIST0 ( "with" scheme ) +| REPLACE "Primitive" identref OPT [ ":" lconstr ] ":=" register_token +| WITH "Primitive" identref OPT [ ":" lconstr ] ":=" "#" identref ] constructor_list_or_record_decl: [ @@ -494,8 +511,10 @@ strategy_flag: [ | OPTINREF ] -export_token: [ -| OPTINREF +filtered_import: [ +| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")" +| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ] +| DELETE global ] functor_app_annot: [ @@ -536,20 +555,23 @@ gallina_ext: [ | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] | WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] +(* don't show Export for Set, Unset *) | REPLACE "Export" "Set" option_table option_setting -| WITH OPT "Export" "Set" option_table option_setting +| WITH "Set" option_table option_setting | REPLACE "Export" "Unset" option_table -| WITH OPT "Export" "Unset" option_table +| WITH "Unset" option_table | REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] +| REPLACE "From" global "Require" export_token LIST1 global +| WITH "From" dirpath "Require" export_token LIST1 global ] -(* lexer stuff *) -IDENT: [ -| ident +export_token: [ +| OPTINREF ] +(* lexer stuff *) integer: [ | DELETENT ] RENAME: [ | integer int (* todo: review uses in .mlg files, some should be "natural" *) @@ -859,6 +881,7 @@ bar_cbrace: [ printable: [ | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string +| DELETE "Term" smart_global OPT univ_name_list (* readded in commands *) | INSERTALL "Print" ] @@ -878,15 +901,18 @@ command: [ | DELETE "Back" | REPLACE "Back" natural | WITH "Back" OPT natural -| REPLACE "Test" option_table "for" LIST1 option_ref_value -| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) -| DELETE "Test" option_table | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ] | WITH "Load" OPT "Verbose" [ ne_string | IDENT ] | DELETE "Unset" option_table -| DELETE "Set" option_table option_setting +| REPLACE "Set" option_table option_setting +| WITH OPT "Export" "Set" option_table (* set flag *) +| REPLACE "Test" option_table "for" LIST1 option_ref_value +| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) +| DELETE "Test" option_table + +(* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Add" IDENT IDENT LIST1 option_ref_value -| WITH "Add" IDENT OPT IDENT LIST1 option_ref_value +| WITH "Add" option_table LIST1 option_ref_value | DELETE "Add" IDENT LIST1 option_ref_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident @@ -941,7 +967,11 @@ command: [ | REPLACE "Preterm" "of" ident | WITH "Preterm" OPT ( "of" ident ) | DELETE "Preterm" -| EDIT "Remove" ADD_OPT IDENT IDENT LIST1 option_ref_value + +(* hide the fact that table names are limited to 2 IDENTs *) +| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value +| WITH "Remove" option_table LIST1 option_ref_value +| DELETE "Remove" IDENT LIST1 option_ref_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string | "Restore" "State" [ IDENT | ne_string ] @@ -976,6 +1006,16 @@ command: [ | REPLACE "Abort" identref | WITH "Abort" OPT [ "All" | identref ] +(* show the locate options as separate commands *) +| DELETE "Locate" locatable +| locatable +| REPLACE "Print" smart_global OPT univ_name_list +| WITH "Print" OPT "Term" smart_global OPT univ_name_list + +] + +option_setting: [ +| OPTINREF ] only_parsing: [ @@ -1062,9 +1102,7 @@ legacy_attr: [ | DELETE "NonCumulative" ] -vernacular: [ -| LIST0 ( OPT all_attrs [ command | tactic ] "." ) -] +sentence: [ ] (* productions defined below *) rec_definition: [ | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations @@ -1124,7 +1162,7 @@ query_command: [ | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" searchabout_query searchabout_queries "." -| WITH "Search" searchabout_query searchabout_queries +| WITH "Search" searchabout_queries ] vernac_toplevel: [ @@ -1142,37 +1180,25 @@ vernac_toplevel: [ | DELETE vernac_control ] -positive_search_mark: [ -| OPTINREF -] - in_or_out_modules: [ | OPTINREF ] -searchabout_queries: [ -| OPTINREF -] - vernac_control: [ (* replacing vernac_control with command is cheating a little; they can't refer to the vernac_toplevel commands. cover this the descriptions of these commands *) | REPLACE "Time" vernac_control -| WITH "Time" command +| WITH "Time" sentence | REPLACE "Redirect" ne_string vernac_control -| WITH "Redirect" ne_string command +| WITH "Redirect" ne_string sentence | REPLACE "Timeout" natural vernac_control -| WITH "Timeout" natural command +| WITH "Timeout" natural sentence | REPLACE "Fail" vernac_control -| WITH "Fail" command +| WITH "Fail" sentence | DELETE decorated_vernac ] -option_setting: [ -| OPTINREF -] - orient: [ | OPTINREF ] @@ -1351,6 +1377,51 @@ module_expr: [ | DELETE module_expr module_expr_atom ] +locatable: [ +| INSERTALL "Locate" +] + +ne_in_or_out_modules: [ +| REPLACE "inside" LIST1 global +| WITH [ "inside" | "outside" ] LIST1 global +| DELETE "outside" LIST1 global +] + +searchabout_query: [ +| REPLACE positive_search_mark ne_string OPT scope_delimiter +| WITH ne_string OPT scope_delimiter +| REPLACE positive_search_mark constr_pattern +| WITH constr_pattern +] + +searchabout_queries: [ +| DELETE ne_in_or_out_modules +| REPLACE searchabout_query searchabout_queries +| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules +| DELETE (* empty *) +] + +positive_search_mark: [ +| OPTINREF +] + +by_notation: [ +| REPLACE ne_string OPT [ "%" IDENT ] +| WITH ne_string OPT [ "%" scope ] +] + +scope_delimiter: [ +| REPLACE "%" IDENT +| WITH "%" scope +] + +(* Don't show these details *) +DELETE: [ +| register_token +| register_prim_token +| register_type_token +] + SPLICE: [ | noedit_mode | bigint @@ -1435,9 +1506,7 @@ SPLICE: [ | mode | mult_pattern | open_constr -| option_table | record_declaration -| register_type_token | tactic | uconstr | impl_ident_head @@ -1466,14 +1535,12 @@ SPLICE: [ | assum_coe | inline | occs -| univ_name_list | ltac_info | field_mods | ltac_production_sep | ltac_tactic_level | printunivs_subgraph | ring_mods -| scope_delimiter | eliminator (* todo: splice or not? *) | quoted_attributes (* todo: splice or not? *) | printable @@ -1486,7 +1553,6 @@ SPLICE: [ | option_ref_value | positive_search_mark | in_or_out_modules -| register_prim_token | option_setting | orient | with_bindings @@ -1518,6 +1584,11 @@ SPLICE: [ | ltac_def_kind | intropatterns | instance_name +| ne_in_or_out_modules +| searchabout_queries +| locatable +| scope_delimiter +| one_import_filter_name ] (* end SPLICE *) RENAME: [ @@ -1567,8 +1638,12 @@ RENAME: [ | record_binder_body field_body | class_rawexpr class | smart_global smart_qualid +| searchabout_query search_item +| option_table setting_name ] +(* todo: positive_search_mark is a lousy name for OPT "-" *) + (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *) clause_dft_concl: [ | OPTINREF @@ -1656,3 +1731,18 @@ SPLICE: [ | tactic_notation_tactics ] (* todo: ssrreflect*.rst ref to fix_body is incorrect *) + +(* not included in insertprodn; defined in rst with :production: *) +control_command: [ ] +query_command: [ ] (* re-add since previously spliced *) + +sentence: [ +| OPT all_attrs command "." +| OPT all_attrs OPT ( num ":" ) query_command "." +| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ] +| control_command +] + +vernacular: [ +| LIST0 sentence +] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index eea1d5081d..f00fda0e8c 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -189,6 +189,9 @@ let rec db_output_prodn = function and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) +(* identify special chars that don't get a trailing space in output *) +let omit_space s = List.mem s ["?"; "."; "#"] + let rec output_prod plist need_semi = function | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s | Snterm s -> @@ -225,7 +228,7 @@ let rec output_prod plist need_semi = function and prod_to_str_r plist prod = match prod with - | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] && plist -> + | Sterm s :: Snterm "ident" :: tl when omit_space s && plist -> (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl) | p :: tl -> let need_semi = @@ -282,7 +285,7 @@ and output_sep sep = and prod_to_prodn_r prod = match prod with - | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] -> + | Sterm s :: Snterm "ident" :: tl when omit_space s -> (sprintf "%s@ident" s) :: (prod_to_prodn_r tl) | p :: tl -> (output_prodn p) :: (prod_to_prodn_r tl) | [] -> [] @@ -1621,6 +1624,7 @@ let open_temp_bin file = open_out_bin (sprintf "%s.new" file) let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+" +let match_subscripts = Str.regexp "__[a-zA-Z0-9]+" let find_longest_match prods str = let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in @@ -1634,19 +1638,26 @@ let find_longest_match prods str = in aux 0 in + let remove_subscrs str = Str.global_replace match_subscripts "" str in let slen = String.length str in let str_pfx = get_pfx str in + let no_subscrs = remove_subscrs str in + let has_subscrs = no_subscrs <> str in let rec longest best multi best_len prods = match prods with | [] -> best, multi, best_len | prod :: tl -> let pstr = String.trim prod in (* todo: should be pretrimmed *) let clen = common_prefix_len str pstr in - if str_pfx = "" || str_pfx <> get_pfx pstr then + if has_subscrs && no_subscrs = pstr then + str, false, clen (* exact match ignoring subscripts *) + else if pstr = str then + pstr, false, clen (* exact match of full line *) + else if str_pfx = "" || str_pfx <> get_pfx pstr then longest best multi best_len tl (* prefixes don't match *) else if clen = slen && slen = String.length pstr then - pstr, false, clen (* exact match *) + pstr, false, clen (* exact match on prefix *) else if clen > best_len then longest pstr false clen tl (* better match *) else if clen = best_len then @@ -1654,7 +1665,11 @@ let find_longest_match prods str = else longest best multi best_len tl (* worse match *) in - longest "" false 0 prods + let mtch, multi, _ = longest "" false 0 prods in + if has_subscrs && mtch <> str then + "", multi, mtch (* no match for subscripted entry *) + else + mtch, multi, "" type seen = { nts: (string * int) NTMap.t; @@ -1753,8 +1768,14 @@ let process_rst g file args seen tac_prods cmd_prods = (* in*) let cmd_replace_files = [ + "doc/sphinx/language/core/records.rst"; + "doc/sphinx/language/core/sections.rst"; + "doc/sphinx/language/extensions/implicit-arguments.rst"; + "doc/sphinx/language/using/libraries/funind.rst"; + "doc/sphinx/language/gallina-specification-language.rst"; - "doc/sphinx/language/gallina-extensions.rst" + "doc/sphinx/language/gallina-extensions.rst"; + "doc/sphinx/proof-engine/vernacular-commands.rst" ] in @@ -1763,11 +1784,14 @@ let process_rst g file args seen tac_prods cmd_prods = if StringSet.is_empty prods || not (List.mem file cmd_replace_files) then rhs (* no change *) else - let mtch, multi, len = find_longest_match prods rhs in + let mtch, multi, best = find_longest_match prods rhs in +(* Printf.printf "mtch = '%s' rhs = '%s'\n" mtch rhs;*) if mtch = rhs then rhs (* no change *) else if mtch = "" then begin warn "%s line %d: NO MATCH `%s`\n" file !linenum rhs; + if best <> "" then + warn "%s line %d: BEST `%s`\n" file !linenum best; rhs end else if multi then begin warn "%s line %d: MULTIMATCH `%s`\n" file !linenum rhs; diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index dc7e0fba37..04c20a7203 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1031,8 +1031,8 @@ gallina_ext: [ | "Collection" identref ":=" section_subset_expr | "Require" export_token LIST1 global | "From" global "Require" export_token LIST1 global -| "Import" LIST1 global -| "Export" LIST1 global +| "Import" LIST1 filtered_import +| "Export" LIST1 filtered_import | "Include" module_type_inl LIST0 ext_module_expr | "Include" "Type" module_type_inl LIST0 ext_module_type | "Transparent" LIST1 smart_global @@ -1057,6 +1057,15 @@ gallina_ext: [ | "Export" "Unset" option_table ] +filtered_import: [ +| global +| global "(" LIST1 one_import_filter_name SEP "," ")" +] + +one_import_filter_name: [ +| global OPT [ "(" ".." ")" ] +] + export_token: [ | "Import" | "Export" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 535976b7d9..e71c80f829 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -47,7 +47,7 @@ one_term: [ term1: [ | term_projection -| term0 "%" ident +| term0 "%" scope | term0 ] @@ -159,7 +159,20 @@ where: [ ] vernacular: [ -| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." ) +| LIST0 sentence +] + +sentence: [ +| OPT all_attrs command "." +| OPT all_attrs OPT ( num ":" ) query_command "." +| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ] +| control_command +] + +control_command: [ +] + +query_command: [ ] tacticals: [ @@ -330,7 +343,7 @@ pattern10: [ ] pattern1: [ -| pattern0 "%" ident +| pattern0 "%" scope | pattern0 ] @@ -367,53 +380,6 @@ decl_notation: [ | string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ] ] -register_token: [ -| "#int63_type" -| "#float64_type" -| "#int63_head0" -| "#int63_tail0" -| "#int63_add" -| "#int63_sub" -| "#int63_mul" -| "#int63_div" -| "#int63_mod" -| "#int63_lsr" -| "#int63_lsl" -| "#int63_land" -| "#int63_lor" -| "#int63_lxor" -| "#int63_addc" -| "#int63_subc" -| "#int63_addcarryc" -| "#int63_subcarryc" -| "#int63_mulc" -| "#int63_diveucl" -| "#int63_div21" -| "#int63_addmuldiv" -| "#int63_eq" -| "#int63_lt" -| "#int63_le" -| "#int63_compare" -| "#float64_opp" -| "#float64_abs" -| "#float64_eq" -| "#float64_lt" -| "#float64_le" -| "#float64_compare" -| "#float64_classify" -| "#float64_add" -| "#float64_sub" -| "#float64_mul" -| "#float64_div" -| "#float64_sqrt" -| "#float64_of_int63" -| "#float64_normfr_mantissa" -| "#float64_frshiftexp" -| "#float64_ldshiftexp" -| "#float64_next_up" -| "#float64_next_down" -] - thm_token: [ | "Theorem" | "Lemma" @@ -531,6 +497,10 @@ constructor: [ | ident LIST0 binder OPT of_type ] +filtered_import: [ +| qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ] +] + cofix_definition: [ | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] @@ -601,20 +571,20 @@ smart_qualid: [ ] by_notation: [ -| string OPT [ "%" ident ] +| string OPT [ "%" scope ] ] argument_spec_block: [ | argument_spec | "/" | "&" -| "(" LIST1 argument_spec ")" OPT ( "%" ident ) -| "[" LIST1 argument_spec "]" OPT ( "%" ident ) -| "{" LIST1 argument_spec "}" OPT ( "%" ident ) +| "(" LIST1 argument_spec ")" OPT ( "%" scope ) +| "[" LIST1 argument_spec "]" OPT ( "%" scope ) +| "{" LIST1 argument_spec "}" OPT ( "%" scope ) ] argument_spec: [ -| OPT "!" name OPT ( "%" ident ) +| OPT "!" name OPT ( "%" scope ) ] more_implicits_block: [ @@ -637,10 +607,14 @@ arguments_modifier: [ | "extra" "scopes" ] +scope: [ +| ident +] + strategy_level: [ -| "expand" | "opaque" | int +| "expand" | "transparent" ] @@ -660,12 +634,16 @@ command: [ | "Cd" OPT string | "Load" OPT "Verbose" [ string | ident ] | "Declare" "ML" "Module" LIST1 string -| "Locate" locatable +| "Locate" smart_qualid +| "Locate" "Term" smart_qualid +| "Locate" "Module" qualid +| "Locate" "Ltac" qualid +| "Locate" "Library" qualid +| "Locate" "File" string | "Add" "LoadPath" string "as" dirpath | "Add" "Rec" "LoadPath" string "as" dirpath | "Remove" "LoadPath" string | "Type" term -| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" ) | "Print" "All" | "Print" "Section" qualid | "Print" "Grammar" ident @@ -702,18 +680,17 @@ command: [ | "Print" "Strategy" smart_qualid | "Print" "Strategies" | "Print" "Registered" -| "Print" smart_qualid OPT ( "@{" LIST0 name "}" ) +| "Print" OPT "Term" smart_qualid OPT univ_name_list | "Print" "Module" "Type" qualid | "Print" "Module" qualid | "Print" "Namespace" dirpath | "Inspect" num | "Add" "ML" "Path" string -| OPT "Export" "Set" LIST1 ident OPT [ int | string ] -| OPT "Export" "Unset" LIST1 ident -| "Print" "Table" LIST1 ident -| "Add" ident OPT ident LIST1 [ qualid | string ] -| "Test" LIST1 ident OPT ( "for" LIST1 [ qualid | string ] ) -| "Remove" OPT ident ident LIST1 [ qualid | string ] +| OPT "Export" "Set" setting_name +| "Print" "Table" setting_name +| "Add" setting_name LIST1 [ qualid | string ] +| "Test" setting_name OPT ( "for" LIST1 [ qualid | string ] ) +| "Remove" setting_name LIST1 [ qualid | string ] | "Write" "State" [ ident | string ] | "Restore" "State" [ ident | string ] | "Reset" "Initial" @@ -806,7 +783,6 @@ command: [ | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid -| "Locate" "Ltac" qualid | "Ltac" tacdef_body LIST0 ( "with" tacdef_body ) | "Print" "Ltac" "Signatures" | "Set" "Firstorder" "Solver" ltac_expr @@ -861,7 +837,7 @@ command: [ | "Combined" "Scheme" ident "from" LIST1 ident SEP "," | "Register" qualid "as" qualid | "Register" "Inline" qualid -| "Primitive" ident OPT [ ":" term ] ":=" register_token +| "Primitive" ident OPT [ ":" term ] ":=" "#" ident | "Universe" LIST1 ident | "Universes" LIST1 ident | "Constraint" LIST1 univ_constraint SEP "," @@ -876,9 +852,9 @@ command: [ | "End" ident | "Collection" ident ":=" section_subset_expr | "Require" OPT [ "Import" | "Export" ] LIST1 qualid -| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid -| "Import" LIST1 qualid -| "Export" LIST1 qualid +| "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid +| "Import" LIST1 filtered_import +| "Export" LIST1 filtered_import | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) | "Include" "Type" LIST1 module_type_inl SEP "<+" | "Transparent" LIST1 smart_qualid @@ -898,6 +874,8 @@ command: [ | "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | "Implicit" [ "Type" | "Types" ] reserv_list | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ] +| "Set" setting_name OPT [ int | string ] +| "Unset" setting_name | "Open" "Scope" ident | "Close" "Scope" ident | "Delimit" "Scope" ident "with" ident @@ -912,15 +890,15 @@ command: [ | "Eval" red_expr "in" term | "Compute" term | "Check" term -| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) -| "SearchHead" one_term OPT ne_in_or_out_modules -| "SearchPattern" one_term OPT ne_in_or_out_modules -| "SearchRewrite" one_term OPT ne_in_or_out_modules -| "Search" searchabout_query OPT searchabout_queries -| "Time" command -| "Redirect" string command -| "Timeout" num command -| "Fail" command +| "About" smart_qualid OPT univ_name_list +| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Time" sentence +| "Redirect" string sentence +| "Timeout" num sentence +| "Fail" sentence | "Drop" | "Quit" | "BackTo" num @@ -959,20 +937,15 @@ starredidentref: [ ] dirpath: [ -| ident -| dirpath field_ident +| LIST0 ( ident "." ) ident ] bignat: [ | numeral ] -locatable: [ -| smart_qualid -| "Term" smart_qualid -| "File" string -| "Library" qualid -| "Module" qualid +setting_name: [ +| LIST1 ident ] comment: [ @@ -981,6 +954,15 @@ comment: [ | num ] +search_item: [ +| one_term +| string OPT ( "%" scope ) +] + +univ_name_list: [ +| "@{" LIST0 name "}" +] + hint: [ | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info | "Resolve" "->" LIST1 qualid OPT num @@ -1068,21 +1050,6 @@ class: [ | smart_qualid ] -ne_in_or_out_modules: [ -| "inside" LIST1 qualid -| "outside" LIST1 qualid -] - -searchabout_query: [ -| OPT "-" string OPT ( "%" ident ) -| OPT "-" one_term -] - -searchabout_queries: [ -| ne_in_or_out_modules -| searchabout_query searchabout_queries -] - level: [ | "level" num | "next" "level" @@ -18,29 +18,10 @@ ; ; (_ (flags :standard -rectypes))) -; Rules for coq_dune -(rule - (targets .vfiles.d) - (deps - (source_tree theories) - (source_tree plugins) - (source_tree user-contrib)) - (action - (with-stdout-to .vfiles.d - (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ - `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \ - `find theories user-contrib -type f -name *.v`")))) - -(alias - (name vodeps) - (deps tools/coq_dune.exe .vfiles.d)) - ; (action (run coq_dune .vfiles.d)))) - (install (section lib) (package coq) - (files - revision)) + (files revision)) (rule (targets revision) diff --git a/dune-project b/dune-project index fa05f5fb41..873d03e8dd 100644 --- a/dune-project +++ b/dune-project @@ -1,11 +1,10 @@ -(lang dune 2.0) +(lang dune 2.5) (name coq) -(using coq 0.1) +(using coq 0.2) (formatting (enabled_for ocaml)) -; We cannot set this to true until as long as the build is not -; properly bootstrapped [that is, we remove the voboot target] +; TODO ; ; (generate_opam_files true) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d4369e9bd1..d6097304ec 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -121,9 +121,10 @@ let rec constr_expr_eq e1 e2 = constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 - | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> + | CAppExpl((proj1,r1,u1),al1), CAppExpl((proj2,r2,u2),al2) -> Option.equal Int.equal proj1 proj2 && qualid_eq r1 r2 && + eq_universes u1 u2 && List.equal constr_expr_eq al1 al2 | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> Option.equal Int.equal proj1 proj2 && @@ -158,8 +159,8 @@ let rec constr_expr_eq e1 e2 = Id.equal id1 id2 && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> Glob_ops.glob_sort_eq s1 s2 - | CCast(t1,c1), CCast(t2,c2) -> - constr_expr_eq t1 t2 && cast_expr_eq c1 c2 + | CCast(t1,c1), CCast(t2,c2) -> + constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> Option.equal notation_with_optional_scope_eq inscope1 inscope2 && notation_eq n1 n2 && diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 905d9f1e5b..45255609e0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -989,7 +989,7 @@ let string_of_ty = function | Variable -> "var" let gvar (loc, id) us = match us with -| None -> DAst.make ?loc @@ GVar id +| None | Some [] -> DAst.make ?loc @@ GVar id | Some _ -> user_err ?loc (str "Variable " ++ Id.print id ++ str " cannot have a universe instance") diff --git a/interp/notation.ml b/interp/notation.ml index 6291a88bb0..0afbb9cd62 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -206,7 +206,7 @@ let classify_scope (local,_,_ as o) = let inScope : bool * bool * scope_item -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; - open_function = open_scope; + open_function = simple_open open_scope; subst_function = subst_scope; discharge_function = discharge_scope; classify_function = classify_scope } @@ -980,9 +980,12 @@ let subst_prim_token_interpretation (subs,infos) = let classify_prim_token_interpretation infos = if infos.pt_local then Dispose else Substitute infos +let open_prim_token_interpretation i o = + if Int.equal i 1 then cache_prim_token_interpretation o + let inPrimTokenInterp : prim_token_infos -> obj = declare_object {(default_object "PRIM-TOKEN-INTERP") with - open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o); + open_function = simple_open open_prim_token_interpretation; cache_function = cache_prim_token_interpretation; subst_function = subst_prim_token_interpretation; classify_function = classify_prim_token_interpretation} diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 767c69e3b6..7184f5ea29 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -67,11 +67,18 @@ let subst_syntax_constant (subst,(local,syndef)) = let classify_syntax_constant (local,_ as o) = if local then Dispose else Substitute o +let filtered_open_syntax_constant f i ((_,kn),_ as o) = + let in_f = match f with + | Unfiltered -> true + | Names ns -> Globnames.(ExtRefSet.mem (SynDef kn) ns) + in + if in_f then open_syntax_constant i o + let in_syntax_constant : (bool * syndef) -> obj = declare_object {(default_object "SYNDEF") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; - open_function = open_syntax_constant; + open_function = filtered_open_syntax_constant; subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 6cfe44c5ff..a5fcfae1fc 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -96,14 +96,14 @@ let mk_accu (a : atom) : t = else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Obj.repr (accumulate data) in - let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in + let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in ans in let acc = { acc_atm = a; acc_arg = [] } in let ans = Obj.repr (accumulate acc) in (** FIXME: use another representation for accumulators, this causes naked pointers. *) - let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in + let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in (Obj.obj ans : t) let get_accu (k : accumulator) = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 181ec4860c..50922ffc52 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -301,6 +301,7 @@ sig type t val repr : t -> side_effect list val empty : t + val is_empty : t -> bool val add : side_effect -> t -> t val concat : t -> t -> t end = @@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t } let repr eff = eff.seff let empty = { seff = []; elts = SeffSet.empty } +let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts let add x es = if SeffSet.mem x es.elts then es else { seff = x :: es.seff; elts = SeffSet.add x es.elts } @@ -349,6 +351,7 @@ let push_private_constants env eff = List.fold_left add_if_undefined env eff let empty_private_constants = SideEffects.empty +let is_empty_private_constants c = SideEffects.is_empty c let concat_private = SideEffects.concat let universes_of_private eff = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f8d5d319a9..b42746a882 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants val empty_private_constants : private_constants +val is_empty_private_constants : private_constants -> bool + val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 466fbacca4..3a89b73bd5 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -12,6 +12,8 @@ open Univ type family = InSProp | InProp | InSet | InType +let all_families = [InSProp; InProp; InSet; InType] + type t = | SProp | Prop diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 49549e224d..fe939b1d95 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -12,6 +12,8 @@ type family = InSProp | InProp | InSet | InType +val all_families : family list + type t = private | SProp | Prop diff --git a/library/globnames.ml b/library/globnames.ml index 9126a467bf..bc24fbf096 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -117,3 +117,10 @@ module ExtRefOrdered = struct | SynDef kn -> combinesmall 2 (KerName.hash kn) end + +module ExtRefMap = HMap.Make(ExtRefOrdered) +module ExtRefSet = ExtRefMap.Set + +let subst_extended_reference sub = function + | SynDef kn -> SynDef (subst_kn sub kn) + | TrueGlobal gr -> TrueGlobal (subst_global_reference sub gr) diff --git a/library/globnames.mli b/library/globnames.mli index fb1583e16c..8acea5ef28 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -61,3 +61,10 @@ module ExtRefOrdered : sig val equal : t -> t -> bool val hash : t -> int end + +module ExtRefSet : CSig.SetS with type elt = extended_global_reference +module ExtRefMap : CMap.ExtS + with type key = extended_global_reference + and module Set := ExtRefSet + +val subst_extended_reference : substitution -> extended_global_reference -> extended_global_reference diff --git a/library/goptions.ml b/library/goptions.ml index 73132868d7..1418407533 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -90,7 +90,7 @@ module MakeTable = let inGo : option_mark * A.t -> obj = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; - Libobject.open_function = load_options; + Libobject.open_function = simple_open load_options; Libobject.cache_function = cache_options; Libobject.subst_function = subst_options; Libobject.classify_function = (fun x -> Substitute x)} @@ -262,7 +262,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) declare_object { (default_object (nickname key)) with load_function = load_options; - open_function = open_options; + open_function = simple_open open_options; cache_function = cache_options; subst_function = subst_options; discharge_function = discharge_options; diff --git a/library/lib.ml b/library/lib.ml index e7e6dc640a..830777003b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -46,7 +46,7 @@ let iter_objects f i prefix = List.iter (fun (id,obj) -> f i (make_oname prefix id, obj)) let load_atomic_objects i pr = iter_objects load_object i pr -let open_atomic_objects i pr = iter_objects open_object i pr +let open_atomic_objects f i pr = iter_objects (open_object f) i pr let subst_atomic_objects subst seg = let subst_one = fun (id,obj as node) -> diff --git a/library/lib.mli b/library/lib.mli index 949b5e26c2..56ea35ec60 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -35,7 +35,8 @@ type lib_objects = (Id.t * Libobject.t) list (** {6 Object iteration functions. } *) -val open_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit +val open_atomic_objects : Libobject.open_filter + -> int -> Nametab.object_prefix -> lib_atomic_objects -> unit val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit val subst_atomic_objects : Mod_subst.substitution -> lib_atomic_objects -> lib_atomic_objects (*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) diff --git a/library/libobject.ml b/library/libobject.ml index 0681e12449..c38e0d891b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -18,11 +18,36 @@ type 'a substitutivity = type object_name = Libnames.full_path * Names.KerName.t +module NSet = Globnames.ExtRefSet + +type open_filter = + | Unfiltered + | Names of NSet.t + +let simple_open f filter i o = match filter with + | Unfiltered -> f i o + | Names _ -> () + +let filter_and f1 f2 = match f1, f2 with + | Unfiltered, f | f, Unfiltered -> Some f + | Names n1, Names n2 -> + let n = NSet.inter n1 n2 in + if NSet.is_empty n then None + else Some (Names n) + +let filter_or f1 f2 = match f1, f2 with + | Unfiltered, f | f, Unfiltered -> Unfiltered + | Names n1, Names n2 -> Names (NSet.union n1 n2) + +let in_filter_ref gr = function + | Unfiltered -> true + | Names ns -> NSet.mem (Globnames.TrueGlobal gr) ns + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; load_function : int -> object_name * 'a -> unit; - open_function : int -> object_name * 'a -> unit; + open_function : open_filter -> int -> object_name * 'a -> unit; classify_function : 'a -> 'a substitutivity; subst_function : Mod_subst.substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; @@ -32,7 +57,7 @@ let default_object s = { object_name = s; cache_function = (fun _ -> ()); load_function = (fun _ _ -> ()); - open_function = (fun _ _ -> ()); + open_function = (fun _ _ _ -> ()); subst_function = (fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); classify_function = (fun atomic_obj -> Keep atomic_obj); @@ -75,7 +100,7 @@ and t = | ModuleTypeObject of substitutive_objects | IncludeObject of algebraic_objects | KeepObject of objects - | ExportObject of { mpl : ModPath.t list } + | ExportObject of { mpl : (open_filter * ModPath.t) list } | AtomicObject of obj and objects = (Names.Id.t * t) list @@ -105,9 +130,9 @@ let load_object i (sp, Dyn.Dyn (tag, v)) = let decl = DynMap.find tag !cache_tab in decl.load_function i (sp, v) -let open_object i (sp, Dyn.Dyn (tag, v)) = +let open_object f i (sp, Dyn.Dyn (tag, v)) = let decl = DynMap.find tag !cache_tab in - decl.open_function i (sp, v) + decl.open_function f i (sp, v) let subst_object (subs, Dyn.Dyn (tag, v)) = let decl = DynMap.find tag !cache_tab in @@ -147,7 +172,7 @@ let global_object_nodischarge s ~cache ~subst = let import i o = if Int.equal i 1 then cache o in { (default_object s) with cache_function = cache; - open_function = import; + open_function = simple_open import; subst_function = (match subst with | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!") | Some subst -> subst; diff --git a/library/libobject.mli b/library/libobject.mli index 24cadc2223..1c82349bb6 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -72,16 +72,28 @@ type 'a substitutivity = type object_name = full_path * Names.KerName.t +type open_filter = Unfiltered | Names of Globnames.ExtRefSet.t + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; load_function : int -> object_name * 'a -> unit; - open_function : int -> object_name * 'a -> unit; + open_function : open_filter -> int -> object_name * 'a -> unit; classify_function : 'a -> 'a substitutivity; subst_function : substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } +val simple_open : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit +(** Combinator for making objects which are only opened by unfiltered Import *) + +val filter_and : open_filter -> open_filter -> open_filter option +(** Returns [None] when the intersection is empty. *) + +val filter_or : open_filter -> open_filter -> open_filter + +val in_filter_ref : Names.GlobRef.t -> open_filter -> bool + (** The default object is a "Keep" object with empty methods. Object creators are advised to use the construction [{(default_object "MY_OBJECT") with @@ -114,7 +126,7 @@ and t = | ModuleTypeObject of substitutive_objects | IncludeObject of algebraic_objects | KeepObject of objects - | ExportObject of { mpl : Names.ModPath.t list } + | ExportObject of { mpl : (open_filter * Names.ModPath.t) list } | AtomicObject of obj and objects = (Names.Id.t * t) list @@ -129,7 +141,7 @@ val declare_object : val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit -val open_object : int -> object_name * obj -> unit +val open_object : open_filter -> int -> object_name * obj -> unit val subst_object : substitution * obj -> obj val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option diff --git a/library/nametab.ml b/library/nametab.ml index 523fe8af50..d9b4dc9122 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -352,10 +352,8 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab) (* Reversed name tables ***************************************************) (* This table translates extended_global_references back to section paths *) -module Globrevtab = HMap.Make(ExtRefOrdered) - -type globrevtab = full_path Globrevtab.t -let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab) +type globrevtab = full_path ExtRefMap.t +let the_globrevtab = Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab) type mprevtab = DirPath.t MPmap.t @@ -386,7 +384,7 @@ let push_xref visibility sp xref = match visibility with | Until _ -> the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - the_globrevtab := Globrevtab.add xref sp !the_globrevtab + the_globrevtab := ExtRefMap.add xref sp !the_globrevtab | _ -> begin if ExtRefTab.exists sp !the_ccitab then @@ -520,7 +518,7 @@ let path_of_global ref = let open GlobRef in match ref with | VarRef id -> make_path DirPath.empty id - | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab + | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab let dirpath_of_global ref = fst (repr_path (path_of_global ref)) @@ -529,7 +527,7 @@ let basename_of_global ref = snd (repr_path (path_of_global ref)) let path_of_syndef kn = - Globrevtab.find (SynDef kn) !the_globrevtab + ExtRefMap.find (SynDef kn) !the_globrevtab let dirpath_of_module mp = MPmap.find mp !the_modrevtab @@ -547,7 +545,7 @@ let shortest_qualid_of_global ?loc ctx ref = match ref with | VarRef id -> make_qualid ?loc DirPath.empty id | _ -> - let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in + let sp = ExtRefMap.find (TrueGlobal ref) !the_globrevtab in ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab let shortest_qualid_of_syndef ?loc ctx kn = diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/dune index 6a024358c3..d2f5b65980 100644 --- a/plugins/btauto/plugin_base.dune +++ b/plugins/btauto/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.btauto) (synopsis "Coq's btauto plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_btauto)) diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/dune index 2a92996d2a..f7fa3adb56 100644 --- a/plugins/cc/plugin_base.dune +++ b/plugins/cc/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.cc) (synopsis "Coq's congruence closure plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_congruence)) diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/dune index ba9cd595ce..1931339471 100644 --- a/plugins/derive/plugin_base.dune +++ b/plugins/derive/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.derive) (synopsis "Coq's derive plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_derive)) diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/dune index 037b0d5053..0c01dcd488 100644 --- a/plugins/extraction/plugin_base.dune +++ b/plugins/extraction/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.extraction) (synopsis "Coq's extraction plugin") (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_extraction)) diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/dune index d88daa23fc..1b05452d8f 100644 --- a/plugins/firstorder/plugin_base.dune +++ b/plugins/firstorder/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.firstorder) (synopsis "Coq's first order logic solver plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ground)) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/dune index 6ccf15df29..e594ffbd02 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.funind) (synopsis "Coq's functional induction plugin") (libraries coq.plugins.extraction)) + +(coq.pp (modules g_indfun)) diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune index 5611f5ba16..6558ecbfe8 100644 --- a/plugins/ltac/plugin_base.dune +++ b/plugins/ltac/dune @@ -11,3 +11,5 @@ (synopsis "Coq's tauto tactic") (modules tauto) (libraries coq.plugins.ltac)) + +(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4127d28bae..9910796d9c 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with - open_function = open_tactic_notation; + open_function = simple_open open_tactic_notation; load_function = load_tactic_notation; cache_function = cache_tactic_notation; subst_function = subst_tactic_notation; diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index ce9189792e..76d47f5482 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr * declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; - open_function = open_md; + open_function = simple_open open_md; subst_function = subst_md; classify_function = classify_md} diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index 4f00f17892..922d2f7792 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -32,7 +32,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = { (default_object name) with cache_function = cache; load_function = (fun _ -> load); - open_function = (fun _ -> load); + open_function = simple_open (fun _ -> load); classify_function = (fun (local, tac) -> if local then Dispose else Substitute (local, tac)); subst_function = subst} diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/dune index 4153d06161..33ad3a0138 100644 --- a/plugins/micromega/plugin_base.dune +++ b/plugins/micromega/dune @@ -20,3 +20,5 @@ (modules g_zify zify) (synopsis "Coq's zify plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_micromega g_zify)) diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/dune index 9da5b39972..b921c9c408 100644 --- a/plugins/nsatz/plugin_base.dune +++ b/plugins/nsatz/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.nsatz) (synopsis "Coq's nsatz solver plugin") (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_nsatz)) diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/dune index f512501c78..0db71ed6fb 100644 --- a/plugins/omega/plugin_base.dune +++ b/plugins/omega/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.omega) (synopsis "Coq's omega plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_omega)) diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/dune index 233845ae0f..43efa0eca5 100644 --- a/plugins/rtauto/plugin_base.dune +++ b/plugins/rtauto/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.rtauto) (synopsis "Coq's rtauto plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_rtauto)) diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/dune index d83857edad..60522cd3f5 100644 --- a/plugins/setoid_ring/plugin_base.dune +++ b/plugins/setoid_ring/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.setoid_ring) (synopsis "Coq's setoid ring plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_newring)) diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/dune index a13524bb52..a117d09a16 100644 --- a/plugins/ssr/plugin_base.dune +++ b/plugins/ssr/dune @@ -5,3 +5,5 @@ (modules_without_implementation ssrast) (flags :standard -open Gramlib) (libraries coq.plugins.ssrmatching)) + +(coq.pp (modules ssrvernac ssrparser)) diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/dune index 06f67c3774..629d723816 100644 --- a/plugins/ssrmatching/plugin_base.dune +++ b/plugins/ssrmatching/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.ssrmatching) (synopsis "Coq ssrmatching plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ssrmatching)) diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/dune index 512752135d..b395695c8a 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/dune @@ -32,3 +32,5 @@ (synopsis "Coq syntax plugin: float") (modules float_syntax) (libraries coq.vernac)) + +(coq.pp (modules g_numeral g_string)) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index a006c82993..cb868e0480 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -60,12 +60,20 @@ let glob_sort_family = let open Sorts in function | UNamed [GSet,0] -> InSet | _ -> raise ComplexSort -let glob_sort_eq u1 u2 = match u1, u2 with +let glob_sort_expr_eq f u1 u2 = + match u1, u2 with | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2 - | UNamed l1, UNamed l2 -> - List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n) l1 l2 + | UNamed l1, UNamed l2 -> f l1 l2 | (UNamed _ | UAnonymous _), _ -> false +let glob_sort_eq u1 u2 = + glob_sort_expr_eq + (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n)) + u1 u2 + +let glob_level_eq u1 u2 = + glob_sort_expr_eq glob_sort_name_eq u1 u2 + let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true | NonMaxImplicit, NonMaxImplicit -> true @@ -123,7 +131,9 @@ let instance_eq f (x1,c1) (x2,c2) = Id.equal x1 x2 && f c1 c2 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with - | GRef (gr1, _), GRef (gr2, _) -> GlobRef.equal gr1 gr2 + | GRef (gr1, u1), GRef (gr2, u2) -> + GlobRef.equal gr1 gr2 && + Option.equal (List.equal glob_level_eq) u1 u2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 14bf2f6764..6da8173dce 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -15,6 +15,8 @@ open Glob_term val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool +val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool (** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 015c26531a..940150b15a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -438,7 +438,15 @@ let pretype_ref ?loc sigma env ref us = match ref with | GlobRef.VarRef id -> (* Section variable *) - (try sigma, make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env)) + (try + let ty = NamedDecl.get_type (lookup_named id !!env) in + (match us with + | None | Some [] -> () + | Some (_ :: _) -> + CErrors.user_err ?loc + Pp.(str "Section variables are not polymorphic:" ++ spc () + ++ str "universe instance should have length 0.")); + sigma, make_judge (mkVar id) ty with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal diff --git a/tactics/declare.ml b/tactics/declare.ml index 324007930a..5135d72f7b 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -93,13 +93,14 @@ let load_constant i ((sp,kn), obj) = Dumpglob.add_constant_kind con obj.cst_kind (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn), obj) = +let open_constant f i ((sp,kn), obj) = (* Never open a local definition *) match obj.cst_locl with | ImportNeedQualified -> () | ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) + if in_filter_ref (GlobRef.ConstRef con) f then + Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) let exists_name id = Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) diff --git a/tactics/hints.ml b/tactics/hints.ml index f8a46fcb1d..2118b4f231 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1163,7 +1163,7 @@ let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; load_function = load_autohint; - open_function = open_autohint; + open_function = simple_open open_autohint; subst_function = subst_autohint; classify_function = classify_autohint; } diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 68de9c7a00..98de0c848b 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -136,17 +136,21 @@ let private_poly_univs = ~value:true (* XXX: This is still separate from close_proof below due to drop_pt in the STM *) -let return_proof { proof } = - let Proof.{name=pid;entry} = Proof.data proof in +(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *) +let prepare_proof ~unsafe_typ { proof } = + let Proof.{name=pid;entry;poly} = Proof.data proof in let initial_goals = Proofview.initial_goals entry in let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in - let proof_opt c = + let to_constr_body c = match EConstr.to_constr_opt evd c with | Some p -> p | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") in + let to_constr_typ t = + if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t + in (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) @@ -159,31 +163,24 @@ let return_proof { proof } = equations and so far there is no code in the CI that will actually call those and do a side-effect, TTBOMK *) (* EJGA: likely the right solution is to attach side effects to the first constant only? *) - let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in + let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in proofs, Evd.evar_universe_context evd let close_proof ~opaque ~keep_body_ucst_separate ps = - let elist, uctx = return_proof ps in + let { section_vars; proof; udecl; initial_euctx } = ps in - let { Proof.name; poly; entry; sigma } = Proof.data proof in + let { Proof.name; poly } = Proof.data proof in + let unsafe_typ = keep_body_ucst_separate && not poly in + let elist, uctx = prepare_proof ~unsafe_typ ps in let opaque = match opaque with Opaque -> true | Transparent -> false in - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in + let make_entry ((body, eff), typ) = - let make_entry (body, eff) (_, typ) = let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) + not poly && + (keep_body_ucst_separate + || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private)) in - (* EJGA: Why are we doing things this way? *) - let typ = EConstr.Unsafe.to_constr typ in - let typ = if allow_deferred then typ else nf typ in - (* EJGA: End "Why are we doing things this way?" *) - let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in let used_univs = Univ.LSet.union used_univs_body used_univs_typ in @@ -218,7 +215,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = in Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in - let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in + let entries = CList.map make_entry elist in { name; entries; uctx } let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = @@ -275,6 +272,10 @@ let return_partial_proof { proof } = let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd +let return_proof ps = + let p, uctx = prepare_proof ~unsafe_typ:false ps in + List.map fst p, uctx + let update_global_env = map_proof (fun p -> let { Proof.sigma } = Proof.data p in diff --git a/test-suite/Makefile b/test-suite/Makefile index eade52b6eb..954a922c8c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -354,8 +354,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primit } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ - $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ + $(coqchk) -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -381,7 +380,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -405,7 +404,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ diff --git a/test-suite/bugs/closed/bug_11935.v b/test-suite/bugs/closed/bug_11935.v new file mode 100644 index 0000000000..ad5ffc68b5 --- /dev/null +++ b/test-suite/bugs/closed/bug_11935.v @@ -0,0 +1,6 @@ +Section S. + Variable A : Prop. + + Fail Check A@{Type}. + Check A@{}. +End S. diff --git a/test-suite/output/UselessSyndef.out b/test-suite/output/UselessSyndef.out new file mode 100644 index 0000000000..ce484889b3 --- /dev/null +++ b/test-suite/output/UselessSyndef.out @@ -0,0 +1,2 @@ +a + : nat diff --git a/test-suite/output/UselessSyndef.v b/test-suite/output/UselessSyndef.v new file mode 100644 index 0000000000..96ad6e9f5c --- /dev/null +++ b/test-suite/output/UselessSyndef.v @@ -0,0 +1,10 @@ +Module M. + Definition a := 0. +End M. +Module N. + Notation a := M.a (only parsing). +End N. + +Import M. Import N. + +Check a. diff --git a/test-suite/output/bug_11934.out b/test-suite/output/bug_11934.out new file mode 100644 index 0000000000..072136c82e --- /dev/null +++ b/test-suite/output/bug_11934.out @@ -0,0 +1,13 @@ +thing = forall x y : foo, bla x y + : Prop +thing = +forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y + : Prop +(* {thing.u1 thing.u0} |= bla.u0 = thing.u0 + bla.u1 = thing.u1 *) +thing = +forall (x : @foo@{thing.u0} True) (y : @foo@{thing.u1} True), +@bla True True x y + : Prop +(* {thing.u1 thing.u0} |= bla.u0 = thing.u0 + bla.u1 = thing.u1 *) diff --git a/test-suite/output/bug_11934.v b/test-suite/output/bug_11934.v new file mode 100644 index 0000000000..fe9772dc62 --- /dev/null +++ b/test-suite/output/bug_11934.v @@ -0,0 +1,13 @@ +Polymorphic Axiom foo@{u} : Prop -> Prop. +Arguments foo {_}. + +Axiom bla : forall {A B}, @foo A -> @foo B -> Prop. +Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y. + +Print thing. (* forall x y : foo, bla x y *) + +Set Printing Universes. +Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *) + +Set Printing Implicit. +Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *) diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v new file mode 100644 index 0000000000..720083aec5 --- /dev/null +++ b/test-suite/success/PartialImport.v @@ -0,0 +1,58 @@ +Module M. + + Definition a := 0. + Definition b := 1. + + Module N. + + Notation c := (a + b). + + End N. + + Inductive even : nat -> Prop := + | even_0 : even 0 + | even_S n : odd n -> even (S n) + with odd : nat -> Set := + odd_S n : even n -> odd (S n). + +End M. + +Module Simple. + + Import M(a). + + Check a. + Fail Check b. + Fail Check N.c. + + (* todo output test: this prints a+M.b since the notation isn't imported *) + Check M.N.c. + + Fail Import M(c). + Fail Import M(M.b). + + Import M(N.c). + Check N.c. + (* interestingly prints N.c (also does with unfiltered Import M) *) + + Import M(even(..)). + Check even. Check even_0. Check even_S. + Check even_sind. Check even_ind. + Fail Check even_rect. (* doesn't exist *) + Fail Check odd. Check M.odd. + Fail Check odd_S. Fail Check odd_sind. + +End Simple. + +Module WithExport. + + Module X. + Export M(a, N.c). + End X. + + Import X. + Check a. + Check N.c. (* also prints N.c *) + Fail Check b. + +End WithExport. diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000000..b9af76d699 --- /dev/null +++ b/theories/dune @@ -0,0 +1,38 @@ +(coq.theory + (name Coq) + (package coq) + (synopsis "Coq's Standard Library") + (flags -q) + ; (mode native) + (boot) + ; (per_file + ; (Init/*.v -> -boot)) + (libraries + coq.plugins.ltac + coq.plugins.tauto + + coq.plugins.cc + coq.plugins.firstorder + + coq.plugins.numeral_notation + coq.plugins.string_notation + coq.plugins.int63_syntax + coq.plugins.r_syntax + coq.plugins.float_syntax + + coq.plugins.btauto + coq.plugins.rtauto + + coq.plugins.setoid_ring + coq.plugins.nsatz + coq.plugins.omega + + coq.plugins.zify + coq.plugins.micromega + + coq.plugins.funind + + coq.plugins.ssreflect + coq.plugins.derive)) + +(include_subdirs qualified) diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml deleted file mode 100644 index 472e6b4948..0000000000 --- a/tools/coq_dune.ml +++ /dev/null @@ -1,301 +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) *) -(************************************************************************) - -(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license: - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - *) - -(* coq_dune: generate dune build rules for .vo files *) -(* *) -(* At some point this file will become a Dune plugin, so it is very *) -(* important that this file can be bootstrapped with: *) -(* *) -(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune *) - -open Format - -(* Keeping this file self-contained as it is a "bootstrap" utility *) -(* Is OCaml missing these basic functions in the stdlib? *) -module Aux = struct - - let option_iter f o = match o with - | Some x -> f x - | None -> () - - let option_cata d f o = match o with - | Some x -> f x - | None -> d - - let list_compare f = let rec lc x y = match x, y with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r - in lc - - let rec pp_list pp sep fmt l = match l with - | [] -> () - | [l] -> fprintf fmt "%a" pp l - | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs - - let rec pmap f l = match l with - | [] -> [] - | x :: xs -> - begin match f x with - | None -> pmap f xs - | Some r -> r :: pmap f xs - end - - let sep fmt () = fprintf fmt "@;" - - (* Creation of paths, aware of the platform separator. *) - let bpath l = String.concat Filename.dir_sep l - - module DirOrd = struct - type t = string list - let compare = list_compare String.compare - end - - module DirMap = Map.Make(DirOrd) - - (* Functions available in newer OCaml versions *) - (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) - module Legacy = struct - - - (* Fix once we move to OCaml >= 4.06.0 *) - let list_init len f = - let rec init_aux i n f = - if i >= n then [] - else let r = f i in r :: init_aux (i+1) n f - in init_aux 0 len f - - (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) - let dirmap_update key f map = - match begin - try f (Some (DirMap.find key map)) - with Not_found -> f None - end with - | None -> DirMap.remove key map - | Some x -> DirMap.add key x map - - end - - let add_map_list key elem map = - (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) - Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map - - let replace_ext ~file ~newext = - Filename.(remove_extension file) ^ newext - -end - -open Aux - -(* Once this is a Dune plugin the flags will be taken from the env *) -module Options = struct - - type flag = { - enabled : bool; - cmd : string; - } - - let all_opts = - [ { enabled = false; cmd = "-debug"; } - ; { enabled = false; cmd = "-native_compiler"; } - ; { enabled = true; cmd = "-w +default"; } - ] - - let build_coq_flags () = - let popt o = if o.enabled then Some o.cmd else None in - String.concat " " @@ pmap popt all_opts -end - -type vodep = { - target: string; - deps : string list; -} - -type ldep = | VO of vodep | MLG of string -type ddir = ldep list DirMap.t - -(* Filter `.vio` etc... *) -let filter_no_vo = - List.filter (fun f -> Filename.check_suffix f ".vo") - -(* We could have coqdep to output dune files directly *) - -let gen_sub n = - (* Move to List.init once we can depend on OCaml >= 4.06.0 *) - bpath @@ Legacy.list_init n (fun _ -> "..") - -let pp_rule fmt targets deps action = - (* Special printing of the first rule *) - let ppl = pp_list pp_print_string sep in - let pp_deps fmt l = match l with - | [] -> - () - | x :: xs -> - fprintf fmt "(:pp-file %s)%a" x sep (); - pp_list pp_print_string sep fmt xs - in - fprintf fmt - "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" - ppl targets pp_deps deps pp_print_string action - -let gen_coqc_targets vo = - [ vo.target - ; replace_ext ~file:vo.target ~newext:".glob" - ; replace_ext ~file:vo.target ~newext:".vos" - ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] - -(* Generate the dune rule: *) -let pp_vo_dep dir fmt vo = - let depth = List.length dir in - let sdir = gen_sub depth in - (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) - let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in - (* Coq flags *) - let cflag = Options.build_coq_flags () in - (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) - let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in - (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in - (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) - let libflag = "-coqlib %{project_root}" in - (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in - let all_targets = gen_coqc_targets vo in - pp_rule fmt all_targets deps action - -let pp_mlg_dep _dir fmt ml = - fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml) - -let pp_dep dir fmt oo = match oo with - | VO vo -> pp_vo_dep dir fmt vo - | MLG f -> pp_mlg_dep dir fmt f - -let out_install fmt dir ff = - let itarget = String.concat "/" dir in - let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" - (pp_list pp_ispec sep) ff - -(* For each directory, we must record two things, the build rules and - the install specification. *) -let record_dune d ff = - let sd = bpath d in - if Sys.file_exists sd && Sys.is_directory sd then - let out = open_out (bpath [sd;"dune"]) in - let fmt = formatter_of_out_channel out in - if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then - fprintf fmt "(include plugin_base.dune)@\n"; - out_install fmt d ff; - List.iter (pp_dep d fmt) ff; - fprintf fmt "%!"; - close_out out - else - eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd - -(* File Scanning *) -let scan_mlg ~root m d = - let dir = [root; d] in - let m = DirMap.add dir [] m in - let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg")) - Array.(to_list @@ readdir (bpath dir))) in - List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg - -let scan_dir ~root m = - let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in - let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in - List.fold_left (scan_mlg ~root) m dirs - -let scan_plugins m = scan_dir ~root:"plugins" m -let scan_usercontrib m = scan_dir ~root:"user-contrib" m - -(* This will be removed when we drop support for Make *) -let fix_cmo_cma file = - if String.equal Filename.(extension file) ".cmo" - then replace_ext ~file ~newext:".cma" - else file - -(* Process .vfiles.d and generate a skeleton for the dune file *) -let parse_coqdep_line l = - match Str.(split (regexp ":") l) with - | [targets;deps] -> - let targets = Str.(split (regexp "[ \t]+") targets) in - let deps = Str.(split (regexp "[ \t]+") deps) in - let targets = filter_no_vo targets in - begin match targets with - | [target] -> - let dir, target = Filename.(dirname target, basename target) in - (* coqdep outputs with the '/' directory separator regardless of - the platform. Anyways, I hope we can link to coqdep instead - of having to parse its output soon, that should solve this - kind of issues *) - let deps = List.map fix_cmo_cma deps in - Some (String.split_on_char '/' dir, VO { target; deps; }) - (* Otherwise a vio file, we ignore *) - | _ -> None - end - (* Strange rule, we ignore *) - | _ -> None - -let rec read_vfiles ic map = - try - let rule = parse_coqdep_line (input_line ic) in - (* Add vo_entry to its corresponding map entry *) - let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in - read_vfiles ic map - with End_of_file -> map - -let out_map map = - DirMap.iter record_dune map - -let exec_ifile f = - match Array.length Sys.argv with - | 1 -> f stdin - | 2 -> - let in_file = Sys.argv.(1) in - begin try - let ic = open_in in_file in - (try f ic - with exn -> - eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); - close_in ic) - with _ -> - eprintf "Error: cannot open input file %s@\n%!" in_file - end - | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 - -let _ = - exec_ifile (fun ic -> - let map = scan_plugins DirMap.empty in - let map = scan_usercontrib map in - let map = read_vfiles ic map in - out_map map) diff --git a/tools/dune b/tools/dune index c0e4e20f72..d591bb0c37 100644 --- a/tools/dune +++ b/tools/dune @@ -49,8 +49,8 @@ (ocamllex coqwc) (executables - (names coq_tex coq_dune) - (public_names coq-tex coq_dune) + (names coq_tex) + (public_names coq-tex) (package coq) - (modules coq_tex coq_dune) + (modules coq_tex) (libraries str)) diff --git a/user-contrib/Ltac2/dune b/user-contrib/Ltac2/dune new file mode 100644 index 0000000000..90869a46a0 --- /dev/null +++ b/user-contrib/Ltac2/dune @@ -0,0 +1,14 @@ +(coq.theory + (name Ltac2) + (package coq) + (synopsis "Ltac2 tactic language") + (libraries coq.plugins.ltac2)) + +(library + (name ltac2_plugin) + (public_name coq.plugins.ltac2) + (synopsis "Ltac2 plugin") + (modules_without_implementation tac2expr tac2qexpr tac2types) + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ltac2)) diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index ebc63ddd01..3e920fcc2d 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -91,7 +91,7 @@ let inTacDef : tacdef -> obj = declare_object {(default_object "TAC2-DEFINITION") with cache_function = cache_tacdef; load_function = load_tacdef; - open_function = open_tacdef; + open_function = simple_open open_tacdef; subst_function = subst_tacdef; classify_function = classify_tacdef} @@ -198,7 +198,7 @@ let inTypDef : typdef -> obj = declare_object {(default_object "TAC2-TYPE-DEFINITION") with cache_function = cache_typdef; load_function = load_typdef; - open_function = open_typdef; + open_function = simple_open open_typdef; subst_function = subst_typdef; classify_function = classify_typdef} @@ -268,7 +268,7 @@ let inTypExt : typext -> obj = declare_object {(default_object "TAC2-TYPE-EXTENSION") with cache_function = cache_typext; load_function = load_typext; - open_function = open_typext; + open_function = simple_open open_typext; subst_function = subst_typext; classify_function = classify_typext} @@ -664,7 +664,7 @@ let classify_synext o = let inTac2Notation : synext -> obj = declare_object {(default_object "TAC2-NOTATION") with cache_function = cache_synext; - open_function = open_synext; + open_function = simple_open open_synext; subst_function = subst_synext; classify_function = classify_synext} @@ -694,7 +694,7 @@ let inTac2Abbreviation : abbreviation -> obj = declare_object {(default_object "TAC2-ABBREVIATION") with cache_function = cache_abbreviation; load_function = load_abbreviation; - open_function = open_abbreviation; + open_function = simple_open open_abbreviation; subst_function = subst_abbreviation; classify_function = classify_abbreviation} @@ -747,7 +747,7 @@ let classify_redefinition o = Substitute o let inTac2Redefinition : redefinition -> obj = declare_object {(default_object "TAC2-REDEFINITION") with cache_function = perform_redefinition; - open_function = (fun _ -> perform_redefinition); + open_function = simple_open (fun _ -> perform_redefinition); subst_function = subst_redefinition; classify_function = classify_redefinition } @@ -962,7 +962,7 @@ let inTac2Init : unit -> obj = declare_object {(default_object "TAC2-INIT") with cache_function = cache_ltac2_init; load_function = load_ltac2_init; - open_function = open_ltac2_init; + open_function = simple_open open_ltac2_init; } let _ = Mltop.declare_cache_obj begin fun () -> diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 390ed62bee..eaa6c84791 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -28,7 +28,7 @@ let discharge_canonical_structure (_,((gref, _ as x), local)) = let inCanonStruc : (GlobRef.t * inductive) * bool -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with - open_function = open_canonical_structure; + open_function = simple_open open_canonical_structure; cache_function = cache_canonical_structure; subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local); classify_function = (fun x -> Substitute x); diff --git a/vernac/classes.ml b/vernac/classes.ml index 3d38713e09..a9425b15d2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -116,7 +116,7 @@ let instance_input : instance -> obj = { (default_object "type classes instances state") with cache_function = cache_instance; load_function = (fun _ x -> cache_instance x); - open_function = (fun _ x -> cache_instance x); + open_function = simple_open (fun _ x -> cache_instance x); classify_function = classify_instance; discharge_function = discharge_instance; rebuild_function = rebuild_instance; @@ -237,7 +237,7 @@ let class_input : typeclass -> obj = { (default_object "type classes state") with cache_function = cache_class; load_function = (fun _ -> cache_class); - open_function = (fun _ -> cache_class); + open_function = simple_open (fun _ -> cache_class); classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_class a)); rebuild_function = rebuild_class; diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index c339c53a9b..4a8e217fc1 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -256,7 +256,7 @@ let classify_coercion obj = let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with - open_function = open_coercion; + open_function = simple_open open_coercion; cache_function = cache_coercion; subst_function = (fun (subst,c) -> subst_coercion subst c); classify_function = classify_coercion; diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1607771598..601e7e060c 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -171,7 +171,7 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let ce = definition_entry ?opaque ?inline ?types ~univs body in let env = Global.env () in let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); + 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 diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 2610f16d92..3e6552c8d2 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -49,9 +49,12 @@ let load_inductive i ((sp, kn), names) = let names = inductive_names sp kn names in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names -let open_inductive i ((sp, kn), names) = +let open_inductive f i ((sp, kn), names) = let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names + List.iter (fun (sp, ref) -> + if Libobject.in_filter_ref ref f then + Nametab.push (Nametab.Exactly i) sp ref) + names let cache_inductive ((sp, kn), names) = let names = inductive_names sp kn names in diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 300dfe6c35..20fa43c8e7 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -56,7 +56,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = { (default_object "Global universe name state") with cache_function = cache_univ_names; load_function = load_univ_names; - open_function = open_univ_names; + open_function = simple_open open_univ_names; discharge_function = discharge_univ_names; subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 4f527b73d0..438509e28a 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -81,6 +81,19 @@ module ModSubstObjs : let sobjs_no_functor (mbids,_) = List.is_empty mbids +let subst_filtered sub (f,mp) = + let f = match f with + | Unfiltered -> Unfiltered + | Names ns -> + let module NSet = Globnames.ExtRefSet in + let ns = + NSet.fold (fun n ns -> NSet.add (Globnames.subst_extended_reference sub n) ns) + ns NSet.empty + in + Names ns + in + f, subst_mp sub mp + let rec subst_aobjs sub = function | Objs o as objs -> let o' = subst_objects sub o in @@ -109,7 +122,7 @@ and subst_objects subst seg = let aobjs' = subst_aobjs subst aobjs in if aobjs' == aobjs then node else (id, IncludeObject aobjs') | ExportObject { mpl } -> - let mpl' = List.map (subst_mp subst) mpl in + let mpl' = List.Smart.map (subst_filtered subst) mpl in if mpl'==mpl then node else (id, ExportObject { mpl = mpl' }) | KeepObject _ -> assert false in @@ -285,86 +298,103 @@ and load_keep i ((sp,kn),kobjs) = (** {6 Implementation of Import and Export commands} *) -let mark_object obj (exports,acc) = - (exports, obj::acc) +let mark_object f obj (exports,acc) = + (exports, (f,obj)::acc) -let rec collect_module_objects mp acc = +let rec collect_module_objects (f,mp) acc = (* May raise Not_found for unknown module and for functors *) let modobjs = ModObjs.get mp in let prefix = modobjs.module_prefix in - let acc = collect_objects 1 prefix modobjs.module_keep_objects acc in - collect_objects 1 prefix modobjs.module_substituted_objects acc + let acc = collect_objects f 1 prefix modobjs.module_keep_objects acc in + collect_objects f 1 prefix modobjs.module_substituted_objects acc -and collect_object i (name, obj as o) acc = +and collect_object f i (name, obj as o) acc = match obj with - | ExportObject { mpl; _ } -> collect_export i mpl acc + | ExportObject { mpl } -> collect_export f i mpl acc | AtomicObject _ | IncludeObject _ | KeepObject _ - | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc + | ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc + +and collect_objects f i prefix objs acc = + List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc + +and collect_one_export f (f',mp) (exports,objs as acc) = + match filter_and f f' with + | None -> acc + | Some f -> + let exports' = MPmap.update mp (function + | None -> Some f + | Some f0 -> Some (filter_or f f0)) + exports + in + (* If the map doesn't change there is nothing new to export. -and collect_objects i prefix objs acc = - List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc + It's possible that [filter_and] or [filter_or] mangled precise + filters such that we repeat uselessly, but the important + [Unfiltered] case is handled correctly. + *) + if exports == exports' then acc + else + collect_module_objects (f,mp) (exports', objs) -and collect_one_export mp (exports,objs as acc) = - if not (MPset.mem mp exports) then - collect_module_objects mp (MPset.add mp exports, objs) - else acc -and collect_export i mpl acc = +and collect_export f i mpl acc = if Int.equal i 1 then - List.fold_right collect_one_export mpl acc + List.fold_right (collect_one_export f) mpl acc else acc -let rec open_object i (name, obj) = +let open_modtype i ((sp,kn),_) = + let mp = mp_of_kn kn in + let mp' = + try Nametab.locate_modtype (qualid_of_path sp) + with Not_found -> + anomaly (pr_path sp ++ str " should already exist!"); + in + assert (ModPath.equal mp mp'); + Nametab.push_modtype (Nametab.Exactly i) sp mp + +let rec open_object f i (name, obj) = match obj with - | AtomicObject o -> Libobject.open_object i (name, o) + | AtomicObject o -> Libobject.open_object f i (name, o) | ModuleObject sobjs -> let dir = dir_of_sp (fst name) in let mp = mp_of_kn (snd name) in - open_module i dir mp sobjs + open_module f i dir mp sobjs | ModuleTypeObject sobjs -> open_modtype i (name, sobjs) - | IncludeObject aobjs -> open_include i (name, aobjs) - | ExportObject { mpl; _ } -> open_export i mpl - | KeepObject objs -> open_keep i (name, objs) + | IncludeObject aobjs -> open_include f i (name, aobjs) + | ExportObject { mpl } -> open_export f i mpl + | KeepObject objs -> open_keep f i (name, objs) -and open_module i obj_dir obj_mp sobjs = +and open_module f i obj_dir obj_mp sobjs = let prefix = Nametab.{ obj_dir ; obj_mp; } in let dirinfo = Nametab.GlobDirRef.DirModule prefix in consistency_checks true obj_dir dirinfo; - Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo; + (match f with + | Unfiltered -> Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo + | Names _ -> ()); (* If we're not a functor, let's iter on the internal components *) if sobjs_no_functor sobjs then begin let modobjs = ModObjs.get obj_mp in - open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects + open_objects f (i+1) modobjs.module_prefix modobjs.module_substituted_objects end -and open_objects i prefix objs = - List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs - -and open_modtype i ((sp,kn),_) = - let mp = mp_of_kn kn in - let mp' = - try Nametab.locate_modtype (qualid_of_path sp) - with Not_found -> - anomaly (pr_path sp ++ str " should already exist!"); - in - assert (ModPath.equal mp mp'); - Nametab.push_modtype (Nametab.Exactly i) sp mp +and open_objects f i prefix objs = + List.iter (fun (id, obj) -> open_object f i (Lib.make_oname prefix id, obj)) objs -and open_include i ((sp,kn), aobjs) = +and open_include f i ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in - open_objects i prefix o + open_objects f i prefix o -and open_export i mpl = - let _,objs = collect_export i mpl (MPset.empty, []) in - List.iter (open_object 1) objs +and open_export f i mpl = + let _,objs = collect_export f i mpl (MPmap.empty, []) in + List.iter (fun (f,o) -> open_object f 1 o) objs -and open_keep i ((sp,kn),kobjs) = +and open_keep f i ((sp,kn),kobjs) = let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in let prefix = Nametab.{ obj_dir; obj_mp; } in - open_objects i prefix kobjs + open_objects f i prefix kobjs let rec cache_object (name, obj) = match obj with @@ -383,7 +413,7 @@ and cache_include ((sp,kn), aobjs) = let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in load_objects 1 prefix o; - open_objects 1 prefix o + open_objects Unfiltered 1 prefix o and cache_keep ((sp,kn),kobjs) = anomaly (Pp.str "This module should not be cached!") @@ -1023,12 +1053,12 @@ let end_library ?except ~output_native_objects dir = cenv,(substitute,keep),ast let import_modules ~export mpl = - let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in - List.iter (open_object 1) objs; + let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in + List.iter (fun (f,o) -> open_object f 1 o) objs; if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl })) -let import_module ~export mp = - import_modules ~export [mp] +let import_module f ~export mp = + import_modules ~export [f,mp] (** {6 Iterators} *) @@ -1073,6 +1103,6 @@ let debug_print_modtab _ = let mod_ops = { - Printmod.import_module = import_module; + Printmod.import_module = import_module Unfiltered; process_module_binding = process_module_binding; } diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index e37299aad6..5e45957e83 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -97,11 +97,11 @@ val append_end_library_hook : (unit -> unit) -> unit or when [mp] corresponds to a functor. If [export] is [true], the module is also opened every time the module containing it is. *) -val import_module : export:bool -> ModPath.t -> unit +val import_module : Libobject.open_filter -> export:bool -> ModPath.t -> unit (** Same as [import_module] but for multiple modules, and more optimized than iterating [import_module]. *) -val import_modules : export:bool -> ModPath.t list -> unit +val import_modules : export:bool -> (Libobject.open_filter * ModPath.t) list -> unit (** Include *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1f52641b82..08ba49f92b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -566,14 +566,21 @@ GRAMMAR EXTEND Gram | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token ; qidl = LIST1 global -> { VernacRequire (Some ns, export, qidl) } - | IDENT "Import"; qidl = LIST1 global -> { VernacImport (false,qidl) } - | IDENT "Export"; qidl = LIST1 global -> { VernacImport (true,qidl) } + | IDENT "Import"; qidl = LIST1 filtered_import -> { VernacImport (false,qidl) } + | IDENT "Export"; qidl = LIST1 filtered_import -> { VernacImport (true,qidl) } | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> { VernacInclude(e::l) } | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> { warn_deprecated_include_type ~loc (); VernacInclude(e::l) } ] ] ; + filtered_import: + [ [ m = global -> { (m, ImportAll) } + | m = global; "("; ns = LIST1 one_import_filter_name SEP ","; ")" -> { (m, ImportNames ns) } ] ] + ; + one_import_filter_name: + [ [ n = global; etc = OPT [ "("; ".."; ")" -> { () } ] -> { n, Option.has_some etc } ] ] + ; export_token: [ [ IDENT "Import" -> { Some false } | IDENT "Export" -> { Some true } diff --git a/vernac/library.ml b/vernac/library.ml index 1b0bd4c0f7..01f5101764 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -335,7 +335,11 @@ let load_require _ (_,(needed,modl,_)) = List.iter register_library needed let open_require i (_,(_,modl,export)) = - Option.iter (fun export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) modl) export + Option.iter (fun export -> + let mpl = List.map (fun m -> Unfiltered, MPfile m) modl in + (* TODO support filters in Require *) + Declaremods.import_modules ~export mpl) + export (* [needed] is the ordered list of libraries not already loaded *) let cache_require o = @@ -370,16 +374,17 @@ let require_library_from_dirpath ~lib_resolver modrefl export = let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPmap.empty) modrefl in let needed = List.rev_map (fun dir -> DPmap.find dir contents) needed in let modrefl = List.map fst modrefl in - if Lib.is_module_or_modtype () then - begin - warn_require_in_module (); - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun export -> - List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modrefl) - export - end - else - add_anonymous_leaf (in_require (needed,modrefl,export)); + if Lib.is_module_or_modtype () then + begin + warn_require_in_module (); + add_anonymous_leaf (in_require (needed,modrefl,None)); + Option.iter (fun export -> + (* TODO import filters *) + List.iter (fun m -> Declaremods.import_module Unfiltered ~export (MPfile m)) modrefl) + export + end + else + add_anonymous_leaf (in_require (needed,modrefl,export)); () (************************************************************************) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 475d5c31f7..3b9c771b93 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -877,9 +877,12 @@ let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) = let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o +let open_syntax_extension i o = + if Int.equal i 1 then cache_syntax_extension o + let inSyntaxExtension : syntax_extension_obj -> obj = declare_object {(default_object "SYNTAX-EXTENSION") with - open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o); + open_function = simple_open open_syntax_extension; cache_function = cache_syntax_extension; subst_function = subst_syntax_extension; classify_function = classify_syntax_definition} @@ -1454,7 +1457,7 @@ let classify_notation nobj = let inNotation : notation_obj -> obj = declare_object {(default_object "NOTATION") with - open_function = open_notation; + open_function = simple_open open_notation; cache_function = cache_notation; subst_function = subst_notation; load_function = load_notation; @@ -1765,7 +1768,7 @@ let classify_scope_command (local, _, _ as o) = let inScopeCommand : locality_flag * scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; - open_function = open_scope_command; + open_function = simple_open open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; classify_function = classify_scope_command} @@ -1831,7 +1834,7 @@ let classify_custom_entry (local,s as o) = let inCustomEntry : locality_flag * string -> obj = declare_object {(default_object "CUSTOM-ENTRIES") with cache_function = cache_custom_entry; - open_function = open_custom_entry; + open_function = simple_open open_custom_entry; load_function = load_custom_entry; subst_function = subst_custom_entry; classify_function = classify_custom_entry} diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 054b60853f..baaf8aa849 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -86,7 +86,13 @@ open Pputils let pr_module = Libnames.pr_qualid - let pr_import_module = Libnames.pr_qualid + let pr_one_import_filter_name (q,etc) = + Libnames.pr_qualid q ++ if etc then str "(..)" else mt() + + let pr_import_module (m,f) = + Libnames.pr_qualid m ++ match f with + | ImportAll -> mt() + | ImportNames ns -> surround (prlist_with_sep pr_comma pr_one_import_filter_name ns) let sep_end = function | VernacBullet _ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3195f339b6..6de14997d4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -872,12 +872,62 @@ let vernac_constraint ~poly l = (**********************) (* Modules *) +let add_subnames_of ns full_n n = + let open GlobRef in + let module NSet = Globnames.ExtRefSet in + let add1 r ns = NSet.add (Globnames.TrueGlobal r) ns in + match n with + | Globnames.SynDef _ | Globnames.TrueGlobal (ConstRef _ | ConstructRef _ | VarRef _) -> + CErrors.user_err Pp.(str "Only inductive types can be used with Import (...).") + | Globnames.TrueGlobal (IndRef (mind,i)) -> + let open Declarations in + let dp = Libnames.dirpath full_n in + let mib = Global.lookup_mind mind in + let mip = mib.mind_packets.(i) in + let ns = add1 (IndRef (mind,i)) ns in + let ns = Array.fold_left_i (fun j ns _ -> add1 (ConstructRef ((mind,i),j+1)) ns) + ns mip.mind_consnames + in + List.fold_left (fun ns f -> + let s = Indrec.elimination_suffix f in + let n_elim = Id.of_string (Id.to_string mip.mind_typename ^ s) in + match Nametab.extended_global_of_path (Libnames.make_path dp n_elim) with + | exception Not_found -> ns + | n_elim -> NSet.add n_elim ns) + ns Sorts.all_families + +let interp_filter_in m = function + | ImportAll -> Libobject.Unfiltered + | ImportNames ns -> + let module NSet = Globnames.ExtRefSet in + let dp_m = Nametab.dirpath_of_module m in + let ns = + List.fold_left (fun ns (n,etc) -> + let full_n = + let dp_n,n = repr_qualid n in + make_path (append_dirpath dp_m dp_n) n + in + let n = try Nametab.extended_global_of_path full_n + with Not_found -> + CErrors.user_err + Pp.(str "Cannot find name " ++ pr_qualid n ++ spc() ++ + str "in module " ++ pr_qualid (Nametab.shortest_qualid_of_module m)) + in + let ns = NSet.add n ns in + if etc then add_subnames_of ns full_n n else ns) + NSet.empty ns + in + Libobject.Names ns + let vernac_import export refl = - let import_mod qid = - try Declaremods.import_module ~export @@ Nametab.locate_module qid - with Not_found -> - CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid) - in + let import_mod (qid,f) = + let m = try Nametab.locate_module qid + with Not_found -> + CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid) + in + let f = interp_filter_in m f in + Declaremods.import_module f ~export m + in List.iter import_mod refl let vernac_declare_module export {loc;v=id} binders_ast mty_ast = @@ -893,7 +943,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); - Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) @@ -914,7 +964,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [qualid_of_ident id]) export + (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -929,14 +979,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [qualid_of_ident id]) + Option.iter (fun export -> vernac_import export [qualid_of_ident id, ImportAll]) export let vernac_end_module export {loc;v=id} = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id, ImportAll]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Global.sections_are_opened () then @@ -957,7 +1007,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [qualid_of_ident ?loc id]) export + (fun export -> vernac_import export [qualid_of_ident ?loc id, ImportAll]) export ) argsexport | _ :: _ -> diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index d6e7a3947a..27663a0681 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -101,7 +101,14 @@ type verbose_flag = bool (* true = Verbose; false = Silent *) type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) + type export_flag = bool (* true = Export; false = Import *) + +type one_import_filter_name = qualid * bool (* import inductive components *) +type import_filter_expr = + | ImportAll + | ImportNames of one_import_filter_name list + type onlyparsing_flag = { onlyparsing : bool } (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -320,7 +327,7 @@ type nonrec vernac_expr = | VernacEndSegment of lident | VernacRequire of qualid option * export_flag option * qualid list - | VernacImport of export_flag * qualid list + | VernacImport of export_flag * (qualid * import_filter_expr) list | VernacCanonical of qualid or_by_notation | VernacCoercion of qualid or_by_notation * class_rawexpr * class_rawexpr |