diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | CONTRIBUTING.md | 3 | ||||
| -rw-r--r-- | default.nix | 3 | ||||
| -rw-r--r-- | dev/README | 50 | ||||
| -rw-r--r-- | dev/README.md | 46 | ||||
| -rw-r--r-- | dev/doc/README.md | 77 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 269 | ||||
| -rw-r--r-- | dev/doc/translate.txt | 495 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 27 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 206 | ||||
| -rw-r--r-- | lib/envars.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/uniform_inductive_parameters.v | 13 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 49 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 7 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 20 |
17 files changed, 349 insertions, 937 deletions
@@ -52,6 +52,9 @@ Vernacular Commands - Nested proofs may be enabled through the option `Nested Proofs Allowed`. By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. +- Added option Uniform Inductive Parameters which abstracts over parameters + before typechecking constructors, allowing to write for example + `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` - New Set Hint Variables/Constants Opaque/Transparent commands for setting globally the opacity flag of variables and constants in hint databases, overwritting the opacity set of the hint database. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2dffd2019..9bd3d0b7c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -20,6 +20,9 @@ If you want to minimize your bug (or help minimize someone else's) for more extr ## Pull requests +**Beginner's guide to hacking Coq: [`dev/doc/README.md`](dev/doc/README.md)** \ +**Development information and tools: [`dev/README.md`](dev/README.md)** + If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the [GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) to get your changes reviewed and pulled into the Coq source repository. Documentation for getting started with the Coq sources is located in various diff --git a/default.nix b/default.nix index 91d963604..a2645f4fc 100644 --- a/default.nix +++ b/default.nix @@ -71,7 +71,8 @@ stdenv.mkDerivation rec { ] else []) ++ (if lib.inNixShell then [ ocamlPackages.merlin - ocamlPackages.ocpIndent + ocamlPackages.ocp-indent + ocamlPackages.ocp-index # Dependencies of the merging script jq diff --git a/dev/README b/dev/README deleted file mode 100644 index 453f85f0d..000000000 --- a/dev/README +++ /dev/null @@ -1,50 +0,0 @@ -This directory contains information and tools to help develop the - Coq system - ====================== - - -Debugging and profiling (in current directory - see doc/debugging.txt) ------------------------ - -ocamldebug-coq: to launch ocaml debugger (generated by the configure script) - -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger - -include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) -base_include: to install raw pretty-printers from ocaml toplevel - -vm_printers.ml, top_printers.ml: ML pretty-printers for debugging - - -Miscellaneous information about the code (directory doc) ------------------------------------------ - -changes.md: (partial) per-version summary of the evolution of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.md: help for debugging or profiling -universes.txt: help for debugging universes -translate.txt: help for using coq translator -extensions.txt: some help about TACTIC EXTEND - -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation - - -Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) ----------------------------------------- -"make mli-doc" in coq root directory. - - -Other development tools (directory tools) ------------------------ - -coqdev.el: helper customizations for everyday Coq development, eg - making `compile' work in subdirectories - -objects.el: various development utilities at emacs level - -anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse - location of Anomaly backtraces and jump to them conveniently from - the Emacs *compilation* output. diff --git a/dev/README.md b/dev/README.md new file mode 100644 index 000000000..4642aaf06 --- /dev/null +++ b/dev/README.md @@ -0,0 +1,46 @@ +# This directory contains information and tools to help develop the Coq system + + +## Debugging and profiling (`dev/`) +**More info on debugging: [`doc/debugging.md`](doc/debugging.md)** + +| File | Description | +| ---- | ----------- | +| dev/ocamldebug-coq | To launch ocaml debugger (generated by the configure script) | +| dev/db | To install pretty-printers from ocaml debugger | +| dev/base_db | To install raw pretty-printers from ocaml debugger | +| dev/include | To install pretty-printers from ocaml toplevel (use with the coq Drop command) | +| dev/base_include | To install raw pretty-printers from ocaml toplevel | +| dev/vm_printers.ml, top_printers.ml | ML pretty-printers for debugging | + + +## Miscellaneous information about the code (`dev/doc`) +**Beginner's guide to hacking Coq: [`dev/doc/README.md`](doc/README.md)** + +| File | Description | +| ---- | ----------- | +| [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source | +| [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files | +| [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling | +| [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | +| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | +| [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | +| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation | +| [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | +| [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | +| [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | +| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate | +| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | +| [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | + + +## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`) +`make mli-doc` in coq root directory. + + +## Other development tools (`dev/tools`) + +| File | Description | +| ---- | ----------- | +| [`dev/tools/coqdev.el`](tools/coqdev.el) | Helper customizations for everyday Coq development, eg making `compile` work in subdirectories +| [`dev/tools/objects.el`](tools/objects.el) | Various development utilities at emacs level | diff --git a/dev/doc/README.md b/dev/doc/README.md new file mode 100644 index 000000000..1a4e40f68 --- /dev/null +++ b/dev/doc/README.md @@ -0,0 +1,77 @@ +# Beginner's guide to hacking Coq + +## Getting dependencies + +Assuming one is running Ubuntu (if not, replace `apt` with the package manager of choice) + +``` +$ sudo apt-get install make opam git + +# At the time of writing, <latest-ocaml-version> is 4.06.1. +# The latest version number is available at: https://ocaml.org/releases/ + +$ opam init --comp <latest-ocaml-version> + +# Then follow the advice displayed at the end as how to update your + ~/.bashrc and ~/.ocamlinit files. + +$ source ~/.bashrc +$ opam install camlp5 + +# needed if you want to build "coqide" target + +$ sudo apt-get install liblablgtksourceview2-ocaml-dev \ + libgtk2.0-dev libgtksourceview2.0-dev +$ opam install lablgtk +``` + +## Building `coqtop` +The general workflow is to first setup a development environment with +the correct `configure` settings, then hacking on Coq, make-ing, and testing. + + +This document will use `$JOBS` to refer to the number of parallel jobs one +is willing to have with `make`. + + +``` +$ git clone git clone https://github.com/coq/coq.git +$ cd coq +$ ./configure -profile devel +$ make -j $JOBS # Make once for `merlin`(autocompletion tool) + +<hack> + +$ make -j $JOBS states # builds just enough to run coqtop +$ bin/coqtop -compile <test_file_name.v> +<goto hack until stuff works> + +<run test-suite> +``` + +To learn how to run the test suite, you can read +[`test-suite/README.md`](../../test-suite/README.md). + +## Coq functions of interest +- `Coqtop.start`: This function is the main entry point of coqtop. +- `Coqtop.parse_args `: This function is responsible for parsing command-line arguments. +- `Coqloop.loop`: This function implements the read-eval-print loop. +- `Vernacentries.interp`: This function is called to execute the Vernacular command user have typed. + It dispatches the control to specific functions handling different Vernacular command. +- `Vernacentries.vernac_check_may_eval`: This function handles the `Check ...` command. + + +## Development environment + tooling +- [`Merlin`](https://github.com/ocaml/merlin) for autocomplete. +- [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup) + +## A note about rlwrap + +When using `rlwrap coqtop` make sure the version of `rlwrap` is at least +`0.42`, otherwise you will get + +``` +rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory +``` + +If this happens either update or use an alternate readline wrapper like `ledit`. diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt deleted file mode 100644 index c48c2d5d1..000000000 --- a/dev/doc/setup.txt +++ /dev/null @@ -1,269 +0,0 @@ -This document provides detailed guidance on how to: -- compile Coq -- take advantage of Merlin in Emacs -- enable auto-completion for Ocaml source-code -- use ocamldebug in Emacs for debugging coqtop -The instructions were tested with Debian 8.3 (Jessie). - -The procedure is somewhat tedious, but the final results are (still) worth the effort. - -How to compile Coq ------------------- - -Getting build dependencies: - - sudo apt-get install make opam git - opam init --comp 4.02.3 - # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. - - source ~/.bashrc - - # needed if you want to build "coqtop" target - opam install camlp5 - - # needed if you want to build "coqide" target - sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev - opam install lablgtk - - # needed if you want to build "doc" target - sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \ - hevea texlive-latex-extra latex-xcolor - -Cloning Coq: - - # Go to the directory where you want to clone Coq's source-code. E.g.: - cd ~/git - - git clone https://github.com/coq/coq.git - -Building coqtop: - - cd ~/git/coq - git checkout trunk - make distclean - ./configure -profile devel - make clean - make -j4 coqide printers - -The "-profile devel" enables all options recommended for developers (like -warnings, support for Merlin, etc). Moreover Coq is configured so that -it can be run without installing it (i.e. from the current directory). - -Once the compilation is over check if -- bin/coqtop -- bin/coqide -behave as expected. - - -A note about rlwrap -------------------- - -When using "rlwrap coqtop" make sure the version of rlwrap is at least -0.42, otherwise you will get - - rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory - -If this happens either update or use an alternate readline wrapper like "ledit". - - -How to install and configure Merlin (for Emacs) ------------------------------------------------ - - sudo apt-get install emacs - - opam install tuareg - # Follow the advice displayed at the end as how to update your ~/.emacs file. - - opam install merlin - # Follow the advice displayed at the end as how to update your ~/.emacs file. - -Then add this: - - (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path) ; directory containing merlin.el - (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin") ; needed only if ocamlmerlin not already in your PATH - (autoload 'merlin-mode "merlin" "Merlin mode" t) - (add-hook 'tuareg-mode-hook 'merlin-mode) - (add-hook 'caml-mode-hook 'merlin-mode) - (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file") - - ;; Do not use TABs. These confuse Merlin. - (setq-default indent-tabs-mode nil) - -to your ~/.emacs file. - -Further Emacs configuration when we start it for the first time. - -Try to open some *.ml file in Emacs, e.g.: - - cd ~/git/coq - emacs toplevel/coqtop.ml & - -Emacs display the following strange message: - - The local variables list in ~/git/coq - contains values that may be safe (*). - - Do you want to apply it? - -Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe." - -Emacs then shows two windows: -- one window that shows the contents of the "toplevel/coqtop.ml" file -- and the other window that shows greetings for new Emacs users. - -If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen." - -The default key-bindings are described here: - - https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch - -If you want, you can customize them by replacing the following lines: - - (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next) - (define-key merlin-map (kbd "C-c C-l") 'merlin-locate) - (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack) - (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing) - -in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want. -In the text below we assume that you changed the origin key-bindings in the following way: - - (define-key merlin-map (kbd "C-n") 'merlin-error-next) - (define-key merlin-map (kbd "C-l") 'merlin-locate) - (define-key merlin-map (kbd "C-b") 'merlin-pop-stack) - (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing) - -Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window. -If you prefer to jump to the definition within the same window, do this: - - <Alt+X> customize-group <ENTER> merlin <ENTER> - - Merlin Locate In New Window - - Value Menu - - Never Open In New Window - - State - - Set For Future Sessions - -Testing (Merlin): - - cd ~/git/coq - emacs toplevel/coqtop.ml & - -Go to the end of the file where you will see the "start" function. - -Go to a line where "init_toplevel" function is called. - -If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>. - -If you want to jump back, type: <Ctrl+B> - -If you want to learn the type of the value at current cursor's position, type: <Ctrl+T> - - -Enabling auto-completion in emacs ---------------------------------- - -In Emacs, type: <Alt+M> list-packages <ENTER> - -In the list that is displayed, click on "company". - -A new window appears where just click on "Install" and then answer "Yes". - -These lines: - - (package-initialize) - (require 'company) - ; Make company aware of merlin - (add-to-list 'company-backends 'merlin-company-backend) - ; Enable company on merlin managed buffers - (add-hook 'merlin-mode-hook 'company-mode) - (global-set-key [C-tab] 'company-complete) - -then need to be added to your "~/.emacs" file. - -Next time when you start emacs and partially type some identifier, -emacs will offer the corresponding completions. -Auto-completion can also be manually invoked by typing <Ctrl+TAB>. -Description of various other shortcuts is here. - - http://company-mode.github.io/ - - -Getting along with ocamldebug ------------------------------ - -The default ocamldebug key-bindings are described here. - - http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369 - -If you want, you can customize them by putting the following commands: - - (global-set-key (kbd "<f5>") 'ocamldebug-break) - (global-set-key (kbd "<f6>") 'ocamldebug-run) - (global-set-key (kbd "<f7>") 'ocamldebug-next) - (global-set-key (kbd "<f8>") 'ocamldebug-step) - (global-set-key (kbd "<f9>") 'ocamldebug-finish) - (global-set-key (kbd "<f10>") 'ocamldebug-print) - (global-set-key (kbd "<f12>") 'camldebug) - -to your "~/.emacs" file. - -Let us try whether ocamldebug in Emacs works for us. -(If necessary, re-)compile coqtop: - - cd ~/git/coq - make -j4 coqide printers - -open Emacs: - - emacs toplevel/coqtop.ml & - -and type: - - <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER> - -As a result, a new window is open at the bottom where you should see: - - (ocd) - -i.e. an ocamldebug shell. - - 1. Switch to the window that contains the "coqtop.ml" file. - 2. Go to the end of the file. - 3. Find the definition of the "start" function. - 4. Go to the "let" keyword that is at the beginning of the first line. - 5. By pressing <F5> you set a breakpoint to the cursor's position. - 6. By pressing <F6> you start the bin/coqtop process. - 7. Then you can: - - step over function calls: <F7> - - step into function calls: <F8> - - or finish execution of the current function until it returns: <F9>. - -Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell. - -The points at which the execution of Ocaml program can stop are defined here: - - http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350 - - -Installing printers to ocamldebug ---------------------------------- - -There is a pretty comprehensive set of printers defined for many common data types. -You can load them by switching to the window holding the "ocamldebug" shell and typing: - - (ocd) source "../dev/db" - - -Some of the functions were you might want to set a breakpoint and see what happens next ---------------------------------------------------------------------------------------- - -- Coqtop.start : This function is the main entry point of coqtop. -- Coqtop.parse_args : This function is responsible for parsing command-line arguments. -- Coqloop.loop : This function implements the read-eval-print loop. -- Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ - It dispatches the control to specific functions handling different Vernacular command. -- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command. diff --git a/dev/doc/translate.txt b/dev/doc/translate.txt deleted file mode 100644 index 5b372c96c..000000000 --- a/dev/doc/translate.txt +++ /dev/null @@ -1,495 +0,0 @@ - - How to use the translator - ========================= - - (temporary version to be included in the official - TeX document describing the translator) - -The translator is a smart, robust and powerful tool to improve the -readibility of your script. The current document describes the -possibilities of the translator. - -In case of problem recompiling the translated files, don't waste time -to modify the translated file by hand, read first the following -document telling on how to modify the original files to get a smooth -uniform safe translation. All 60000 lines of Coq lines on our -user-contributions server have been translated without any change -afterwards, and 0,5 % of the lines of the original files (mainly -notations) had to be modified beforehand to get this result. - -Table of contents ------------------ - -I) Implicit Arguments - 1) Strict Implicit Arguments - 2) Implicit Arguments in standard library - -II) Notations - 1) Translating a V7 notation as it was - 2) Translating a V7 notation which conflicts with the new syntax - a) Associativity conflicts - b) Conflicts with other notations - b1) A notation hides another notation - b2) A notation conflicts with the V8 grammar - b3) My notation is already defined at another level - c) How to use V8only with Distfix ? - d) Can I overload a notation in V8, e.g. use "*" and "+" ? - 3) Using the translator to have simplest notations - 4) Setting the translator to automatically use new notations that - wasn't used in old syntax - 5) Defining a construction and its notation simultaneously - -III) Various pitfalls - 1) New keywords - 2) Old "Case" and "Match" - 3) Change of definition or theorem names - 4) Change of tactic names - ---------------------------------------------------------------------- - -I) Implicit Arguments - ------------------ - -1) Strict Implicit Arguments - - "Set Implicit Arguments" changes its meaning in V8: the default is -to turn implicit only the arguments that are _strictly_ implicit (or -rigid), i.e. that remains inferable whatever the other arguments -are. E.g "x" inferable from "P x" is not strictly inferable since it -can disappears if "P" is instanciated by a term which erase "x". - - To respect the old semantics, the default behaviour of the -translator is to replace each occurrence "Set Implicit Arguments" by - - Set Implicit Arguments. - Unset Strict Implicits. - - However, you may wish to adopt the new semantics of "Set Implicit -Arguments" (for instance because you think that the choice of -arguments it setsimplicit is more "natural" for you). In this case, -add the option -strict-implicit to the translator. - - Warning: Changing the number of implicit arguments can break the -notations. Then use the V8only modifier of Notations. - -2) Implicit Arguments in standard library - - Main definitions of standard library have now implicit -arguments. These arguments are dropped in the translated files. This -can exceptionally be a source of incompatibilities which has to be -solved by hand (it typically happens for polymorphic functions applied -to "nil" or "None"). - -II) Notations - --------- - - Grammar (on constr) and Syntax are no longer supported. Replace them by -Notation before translation. - - Precedence levels are now from 0 to 200. In V8, the precedence and -associativity of an operator cannot be redefined. Typical level are -(refer to the chapter on notations in the Reference Manual for the -full list): - - <-> : 95 (no associativity) - -> : 90 (right associativity) - \/ : 85 (right associativity) - /\ : 80 (right associativity) - ~ : 75 (right associativity) - =, <, >, <=, >=, <> : 70 (no associativity) - +, - : 50 (left associativity) - *, / : 40 (left associativity) - ^ : 30 (right associativity) - -1) Translating a V7 notation as it was - - By default, the translator keeps the associativity given in V7 while -the levels are mapped according to the following table: - - the V7 levels [ 0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10] - are resp. mapped in V8 to [ 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100] - with predefined assoc [ No; L; R; L; L; No; R; R; R; No; L] - - If this is OK for you, just simply apply the translator. - -2) Translating a V7 notation which conflicts with the new syntax - -a) Associativity conflict - - Since the associativity of the levels obtained by translating a V7 -level (as shown on table above) cannot be changed, you have to choose -another level with a compatible associativity. - - You can choose any level between 0 and 200, knowing that the -standard operators are already set at the levels shown on the list -above. - -Example 1: Assume you have a notation - -Infix NONA 2 "=_S" my_setoid_eq. - -By default, the translator moves it to level 30 which is right -associative, hence a conflict with the expected no associativity. - -To solve the problem, just add the "V8only" modifier to reset the -level and enforce the associativity as follows: - -Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity). - -The translator now knows that it has to translate "=_S" at level 70 -with no associativity. - -Rem: 70 is the "natural" level for relations, hence the choice of 70 -here, but any other level accepting a no-associativity would have been -OK. - -Example 2: Assume you have a notation - -Infix RIGHTA 1 "o" my_comp. - -By default, the translator moves it to level 20 which is left -associative, hence a conflict with the expected right associativity. - -To solve the problem, just add the "V8only" modifier to reset the -level and enforce the associativity as follows: - -Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity). - -The translator now knows that it has to translate "o" at level 20 -which has the correct "right associativity". - -Rem: We assumed here that the user wants a strong precedence for -composition, in such a way, say, that "f o g + h" is parsed as -"(f o g) + h". To get "o" binding less than the arithmetical operators, -an appropriated level would have been close of 70, and below, e.g. 65. - -b) Conflicts with other notations - -Since the new syntax comes with new keywords and new predefined -symbols, new conflicts can occur. Again, you can use the option V8only -to inform the translator of the new syntax to use. - -b1) A notation hides another notation - -Rem: use Print Grammar constr in V8 to diagnose the overlap and see the -section on factorization in the chapter on notations of the Reference -Manual for hints on how to factorize. - -Example: - -Notation "{ x }" := (my_embedding x) (at level 1). - -overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at -level 99. The conflicts can be solved by left-factorizing the notation -as follows: - -Notation "{ x }" := (my_embedding x) (at level 1) - V8only (at level 0, x at level 99). - -b2) A notation conflicts with the V8 grammar. - -Again, use the V8only modifier to tell the translator to automatically -take in charge the new syntax. - -Example: - -Infix 3 "@" app. - -Since "@" is used in the new syntax for deactivating the implicit -arguments, another symbol has to be used, e.g. "@@". This is done via -the V8only option as follows: - -Infix 3 "@" app V8only "@@" (at level 40, left associativity). - -or, alternatively by - -Notation "x @ y" := (app x y) (at level 3, left associativity) - V8only "x @@ y" (at level 40, left associativity). - -b3) My notation is already defined at another level (or with another -associativity) - -In V8, the level and associativity of a given notation can no longer -be changed. Then, either you adopt the standard reserved levels and -associativity for this notation (as given on the list above) or you -change your notation. - -- To change the notation, follow the directions in section b2. - -- To adopt the standard level, just use V8only without any argument. - -Example. - -Infix 6 "*" my_mult. - -is not accepted as such in V8. Write - -Infix 6 "*" my_mult V8only. - -to tell the translator to use "*" at the reserved level (i.e. 40 with -left associativity). Even better, use interpretation scopes (look at -the Reference Manual). - -c) How to use V8only with Distfix ? - -You can't, use Notation instead of Distfix. - -d) Can I overload a notation in V8, e.g. use "*" and "+" for my own -algebraic operations ? - -Yes, using interpretation scopes (see the corresponding chapter in the -Reference Manual). - -3) Using the translator to have simplest notations - -Thanks to the new syntax, * has now the expected left associativity, -and the symbols <, >, <= and >= are now available. - -Thanks to the interpretation scopes, you can overload the -interpretation of these operators with the default interpretation -provided in Coq. - -This may be a motivation to use the translator to automatically change -the notations while switching to the new syntax. - -See sections b) and d) above for examples. - -4) Setting the translator to automatically use new notations that -wasn't used in old syntax - -Thanks to the "Notation" mechanism, defining symbolic notations is -simpler than in the previous versions of Coq. - -Thanks to the new syntax and interpretation scopes, new symbols and -overloading is available. - -This may be a motivation for using the translator to automatically change -the notations while switching to the new syntax. - -Use for that the commands V8Notation and V8Infix. - -Examples: - -V8Infix "==>" my_relation (at level 65, right associativity). - -tells the translator to write an infix "==>" instead of my_relation in -the translated files. - -V8Infix ">=" my_ge. - -tells the translator to write an infix ">=" instead of my_ge in the -translated files and that the level and associativity are the standard -one (as defined in the chart above). - -V8Infix ">=" my_ge : my_scope. - -tells the translator to write an infix ">=" instead of my_ge in the -translated files, that the level and associativity are the standard -one (as defined in the chart above), but only if scope my_scope is -open or if a delimiting key is available for "my_scope" (see the -Reference Manual). - -5) Defining a construction and its notation simultaneously - -This is permitted by the new syntax. Look at the Reference Manual for -explanation. The translator is not fully able to take this in charge... - -III) Various pitfalls - ---------------- - -1) New keywords - - The following identifiers are new keywords - - "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then"; - "else"; "return"; "mod"; "at"; "let"; "_"; ".(" - - The translator automatically add a "_" to names clashing with a -keyword, except for files. Hence users may need to rename the files -whose name clashes with a keyword. - - Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type" - were already keywords - -2) Old "Case" and "Match" - - "Case" and "Match" are normally automatically translated into - "match" or "match" and "fix", but sometimes it fails to do so. It - typically fails when the Case or Match is argument of a tactic whose - typing context is unknown because of a preceding Intro/Intros, as e.g. in - - Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end) - - The solution is then to replace the invocation of the sequence of - tactics into several invocation of the elementary tactics as follows - - Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end) - ^^^ - -3) Change of definition or theorem names - - Type "entier" from fast_integer.v is renamed into "N" by the -translator. As a consequence, user-defined objects of same name "N" -are systematically qualified even tough it may not be necessary. The -same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST -TO GIVE]. - -4) Change of tactics names - - Since tactics names are now lowercase, this can clash with -user-defined tactic definitions. To pally this, clashing names are -renamed by adding an extra "_" to their name. - -====================================================================== -Main examples for new syntax ----------------------------- - -1) Constructions - - Applicative terms don't any longer require to be surrounded by parentheses as -e.g in - - "x = f y -> S x = S (f y)" - - - Product is written - - "forall x y : T, U" - "forall x y, U" - "forall (x y : T) z (v w : V), U" - etc. - - Abstraction is written - - "fun x y : T, U" - "fun x y, U" - "fun (x y : T) z (v w : V), U" - etc. - - Pattern-matching is written - - "match x with c1 x1 x2 => t | c2 y as z => u end" - "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end" - "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with - c1 x1 x2, _ => t | c2 y, d z => u end" - - The last example is the new form of what was written - - "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of - (c1 x1 x2) _ => t | (c2 y) (d z) => u end" - - Pattern-matching of type with one constructors and no dependencies -of the arguments in the resulting type can be written - - "let (x,y,z) as u return P u := t in v" - - Local fixpoints are written - - "fix f (n m:nat) z (x : X) {struct m} : nat := ... - with ..." - - and "struct" tells which argument is structurally decreasing. - - Explicitation of implicit arguments is written - - "f @1:=u v @3:=w t" - "@f u v w t" - -2) Tactics - - The main change is that tactics names are now lowercase. Besides -this, the following renaming are applied: - - "NewDestruct" -> "destruct" - "NewInduction" -> "induction" - "Induction" -> "simple induction" - "Destruct" -> "simple destruct" - - For tactics with occurrences, the occurrences now comes after and - repeated use is separated by comma as in - - "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4" - "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4" - "Simpl 1 3 e" -> "simpl e at 1 3" - -3) Tactic language - - Definitions are now introduced with keyword "Ltac" (instead of -"Tactic"/"Meta" "Definition") and are implicitly recursive -("Recursive" is no longer used). - - The new rule for distinguishing terms from ltac expressions is: - - Write "ltac:" in front of any tactic in argument position and - "constr:" in front of any construction in head position - -4) Vernacular language - -a) Assumptions - - The syntax for commands is mainly unchanged. Declaration of -assumptions is now done as follows - - Variable m : t. - Variables m n p : t. - Variables (m n : t) (u v : s) (w : r). - -b) Definitions - - Definitions are done as follows - - Definition f m n : t := ... . - Definition f m n := ... . - Definition f m n := ... : t. - Definition f (m n : u) : t := ... . - Definition f (m n : u) := ... : t. - Definition f (m n : u) := ... . - Definition f a b (p q : v) r s (m n : t) : t := ... . - Definition f a b (p q : v) r s (m n : t) := ... . - Definition f a b (p q : v) r s (m n : t) := ... : t. - -c) Fixpoints - - Fixpoints are done this way - - Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... . - Fixpoint f x : v := ... . - Fixpoint f (x : t) : v := ... . - - It is possible to give a concrete notation to a fixpoint as follows - - Fixpoint plus (n m:nat) {struct n} : nat as "n + m" := - match n with - | O => m - | S p => S (p + m) - end. - -d) Inductive types - - The syntax for inductive types is as follows - - Inductive t (a b : u) (d : e) : v := - c1 : w1 | c2 : w2 | ... . - - Inductive t (a b : u) (d : e) : v := - c1 : w1 | c2 : w2 | ... . - - Inductive t (a b : u) (d : e) : v := - c1 (x y : t) : w1 | c2 (z : r) : w2 | ... . - - As seen in the last example, arguments of the constructors can be -given before the colon. If the type itself is omitted (allowed only in -case the inductive type has no real arguments), this yields an -ML-style notation as follows - - Inductive nat : Set := O | S (n:nat). - Inductive bool : Set := true | false. - - It is even possible to define a syntax at the same time, as follows: - - Inductive or (A B:Prop) : Prop as "A \/ B":= - | or_introl (a:A) : A \/ B - | or_intror (b:B) : A \/ B. - - Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B). - diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8fbd2ea4e..509ac92f8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1349,7 +1349,7 @@ folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding to invalid |Coq| identifiers are skipped, and, by convention, subdirectories named ``CVS`` or ``_darcs`` are skipped too. -Thanks to this mechanism, .vo files are made available through the +Thanks to this mechanism, ``.vo`` files are made available through the logical name of the folder they are in, extended with their own basename. For example, the name associated to the file ``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for @@ -1360,17 +1360,17 @@ wrong loadpath afterwards. Some folders have a special status and are automatically put in the path. |Coq| commands associate automatically a logical path to files in the repository trees rooted at the directory from where the command is -launched, coqlib/user-contrib/, the directories listed in the -`$COQPATH`, `${XDG_DATA_HOME}/coq/` and `${XDG_DATA_DIRS}/coq/` -environment variables (see`http://standards.freedesktop.org/basedir- -spec/basedir-spec-latest.html`_) with the same physical-to-logical -translation and with an empty logical prefix. +launched, ``coqlib/user-contrib/``, the directories listed in the +``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/`` +environment variables (see `XDG base directory specification +<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_) +with the same physical-to-logical translation and with an empty logical prefix. The command line option ``-R`` is a variant of ``-Q`` which has the strictly same behavior regarding loadpaths, but which also makes the corresponding ``.vo`` files available through their short names in a way not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib`` -associates to the ``filepath/fOO/Bar/File.vo`` the logical name +associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name ``Lib.fOO.Bar.File``, but allows this file to be accessed through the short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with identical base name are present in different subdirectories of a diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index c26ae2a93..e13625286 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -38,6 +38,7 @@ At the end, the notation “``[entry sep … sep entry]``” stands for a possibly empty sequence of expressions parsed by the “``entry``” entry, separated by the literal “``sep``”. +.. _lexical-conventions: Lexical conventions =================== @@ -905,6 +906,32 @@ Parametrized inductive types sort for the inductive definition and will produce a less convenient rule for case elimination. +.. opt:: Uniform Inductive Parameters + + When this option is set (it is off by default), + inductive definitions are abstracted over their parameters + before typechecking constructors, allowing to write: + + .. coqtop:: all undo + + Set Uniform Inductive Parameters. + Inductive list3 (A:Set) : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + + This behavior is essentially equivalent to starting a new section + and using :cmd:`Context` to give the uniform parameters, like so + (cf. :ref:`section-mechanism`): + + .. coqtop:: all undo + + Section list3. + Context (A:Set). + Inductive list3 : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + End list3. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3b95a37ed..dcefa293b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -10,15 +10,14 @@ parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. The main commands to provide custom symbolic notations for terms are -``Notation`` and ``Infix``. They are described in section :ref:`Notations`. There is also a -variant of ``Notation`` which does not modify the parser. This provides with a -form of abbreviation and it is described in Section :ref:`Abbreviations`. It is +:cmd:`Notation` and :cmd:`Infix`; they will be described in the +:ref:`next section <Notations>`. There is also a +variant of :cmd:`Notation` which does not modify the parser; this provides a +form of :ref:`abbreviation <Abbreviations>`. It is sometimes expected that the same symbolic notation has different meanings in -different contexts. To achieve this form of overloading, |Coq| offers a notion -of interpretation scope. This is described in Section :ref:`Scopes`. - -The main command to provide custom notations for tactics is ``Tactic Notation``. -It is described in Section :ref:`TacticNotation`. +different contexts; to achieve this form of overloading, |Coq| offers a notion +of :ref:`interpretation scopes <Scopes>`. +The main command to provide custom notations for tactics is :cmd:`Tactic Notation`. .. coqtop:: none @@ -44,7 +43,7 @@ logical conjunction (and). Such a notation is declared by Notation "A /\ B" := (and A B). -The expression :g:`(and A B)` is the abbreviated term and the string ``"A /\ B"`` +The expression :g:`(and A B)` is the abbreviated term and the string :g:`"A /\ B"` (called a *notation*) tells how it is symbolically written. A notation is always surrounded by double quotes (except when the @@ -66,15 +65,15 @@ example. A notation binds a syntactic expression to a term. Unless the parser and pretty-printer of Coq already know how to deal with the syntactic -expression (see 12.1.7), explicit precedences and associativity rules -have to be given. +expression (see :ref:`ReservingNotations`), explicit precedences and +associativity rules have to be given. .. note:: The right-hand side of a notation is interpreted at the time the notation is - given. In particular, disambiguation of constants, implicit arguments (see - Section :ref:`ImplicitArguments`), coercions (see Section :ref:`Coercions`), - etc. are resolved at the time of the declaration of the notation. + given. In particular, disambiguation of constants, :ref:`implicit arguments + <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the + time of the declaration of the notation. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -106,13 +105,13 @@ is 100, for example 85 for disjunction and 80 for conjunction [#and_or_levels]_. Similarly, an associativity is needed to decide whether :g:`True /\ False /\ False` defaults to :g:`True /\ (False /\ False)` (right associativity) or to :g:`(True /\ False) /\ False` (left associativity). We may even consider that the -expression is not well- formed and that parentheses are mandatory (this is a “no +expression is not well-formed and that parentheses are mandatory (this is a “no associativity”) [#no_associativity]_. We do not know of a special convention of the associativity of disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of Coq). Precedence levels and associativity rules of notations have to be -given between parentheses in a list of modifiers that the ``Notation`` +given between parentheses in a list of modifiers that the :cmd:`Notation` command understands. Here is how the previous examples refine. .. coqtop:: in @@ -122,9 +121,10 @@ command understands. Here is how the previous examples refine. By default, a notation is considered non associative, but the precedence level is mandatory (except for special cases whose level is -canonical). The level is either a number or the phrase `next level` -whose meaning is obvious. The list of levels already assigned is on -Figure 3.1. +canonical). The level is either a number or the phrase ``next level`` +whose meaning is obvious. +Some :ref:`associativities are predefined <init-notations>` in the +``Notations`` module. .. TODO I don't find it obvious -- CPC @@ -162,7 +162,7 @@ One can also define notations for binders. In the last case though, there is a conflict with the notation for type casts. The notation for types casts, as shown by the command :cmd:`Print Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, -it is necessary to put x at a level below 100, typically 99. Hence, a correct +it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: .. coqtop:: all @@ -176,7 +176,7 @@ Simple factorization rules ~~~~~~~~~~~~~~~~~~~~~~~~~~ Coq extensible parsing is performed by *Camlp5* which is essentially a LL1 -parser: it decides which notation to parse by looking tokens from left to right. +parser: it decides which notation to parse by looking at tokens from left to right. Hence, some care has to be taken not to hide already existing rules by new rules. Some simple left factorization work has to be done. Here is an example. @@ -186,11 +186,11 @@ rules. Some simple left factorization work has to be done. Here is an example. Notation "x < y < z" := (x < y /\ y < z) (at level 70). In order to factorize the left part of the rules, the subexpression -referred by y has to be at the same level in both rules. However the -default behavior puts y at the next level below 70 in the first rule -(no associativity is the default), and at the level 200 in the second -rule (level 200 is the default for inner expressions). To fix this, we -need to force the parsing level of y, as follows. +referred by ``y`` has to be at the same level in both rules. However the +default behavior puts ``y`` at the next level below 70 in the first rule +(``no associativity`` is the default), and at the level 200 in the second +rule (``level 200`` is the default for inner expressions). To fix this, we +need to force the parsing level of ``y``, as follows. .. coqtop:: all @@ -198,9 +198,9 @@ need to force the parsing level of y, as follows. Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). For the sake of factorization with Coq predefined rules, simple rules -have to be observed for notations starting with a symbol: e.g. rules -starting with “{” or “(” should be put at level 0. The list of Coq -predefined notations can be found in Chapter :ref:`thecoqlibrary`. +have to be observed for notations starting with a symbol, e.g., rules +starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list +of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. .. cmd:: Print Grammar constr. @@ -215,7 +215,7 @@ predefined notations can be found in Chapter :ref:`thecoqlibrary`. Displaying symbolic notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The command ``Notation`` has an effect both on the Coq parser and on the +The command :cmd:`Notation` has an effect both on the Coq parser and on the Coq printer. For example: .. coqtop:: all @@ -301,7 +301,7 @@ at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do so, the option ``only parsing`` is allowed in the list of modifiers - of ``Notation``. Conversely, the ``only printing`` modifier can be + of :cmd:`Notation`. Conversely, the ``only printing`` modifier can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -309,7 +309,7 @@ at the time of use of the notation. The Infix command ~~~~~~~~~~~~~~~~~~ -The ``Infix`` command is a shortening for declaring notations of infix +The :cmd:`Infix` command is a shortening for declaring notations of infix symbols. .. cmd:: Infix "@symbol" := @term ({+, @modifier}). @@ -324,6 +324,8 @@ symbols. Infix "/\" := and (at level 80, right associativity). +.. _ReservingNotations: + Reserving notations ~~~~~~~~~~~~~~~~~~~ @@ -341,7 +343,7 @@ state of Coq. Reserving a notation is also useful for simultaneously defining an inductive type or a recursive constant and a notation for it. -.. note:: The notations mentioned on Figure 3.1 are reserved. Hence +.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence their precedence and associativity cannot be changed. Simultaneous definition of terms and notations @@ -391,7 +393,7 @@ Locating notations To know to which notations a given symbol belongs to, use the :cmd:`Locate` command. You can call it on any (composite) symbol surrounded by double quotes. To locate a particular notation, use a string where the variables of the -notation are replaced by “_” and where possible single quotes inserted around +notation are replaced by “``_``” and where possible single quotes inserted around identifiers or tokens starting with a single quote are dropped. .. coqtop:: all @@ -404,7 +406,7 @@ Notations and binders Notations can include binders. This section lists different ways to deal with binders. For further examples, see also -Section :ref:`RecursiveNotationsWithBinders`. +:ref:`RecursiveNotationsWithBinders`. Binders bound in the notation and parsed as identifiers +++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -490,7 +492,7 @@ the following: This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the -constant :g:`sumbool` (see Section :ref:`specification`). +constant :g:`sumbool` (see :ref:`specification`). Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for @@ -545,7 +547,7 @@ the next command fails because p does not bind in the instance of n. Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). -.. _RecursiveNotationsWithBinders: +.. _RecursiveNotations: Notations with recursive patterns ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -563,7 +565,7 @@ confused with the three-dots notation “``…``” used in this manual to denot a sequence of arbitrary size. On the left-hand side, the part “``x s .. s y``” of the notation parses -any number of time (but at least one time) a sequence of expressions +any number of times (but at least one time) a sequence of expressions separated by the sequence of tokens ``s`` (in the example, ``s`` is just “``;``”). The right-hand side must contain a subterm of the form either @@ -572,7 +574,7 @@ called the *iterator* of the recursive notation is an arbitrary expression with distinguished placeholders and where :math:`t` is called the *terminating expression* of the recursive notation. In the example, we choose the names :math:`x` and :math:`y` but in practice they can of course be chosen -arbitrarily. Not atht the placeholder :math:`[~]_I` has to occur only once but +arbitrarily. Note that the placeholder :math:`[~]_I` has to occur only once but :math:`[~]_E` can occur several times. Parsing the notation produces a list of expressions which are used to @@ -595,9 +597,10 @@ and the terminating expression is ``nil``. Here are other examples: (t at level 39). Notations with recursive patterns can be reserved like standard -notations, they can also be declared within interpretation scopes (see -section 12.2). +notations, they can also be declared within +:ref:`interpretation scopes <Scopes>`. +.. _RecursiveNotationsWithBinders: Notations with recursive patterns involving binders ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -611,7 +614,8 @@ is: (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, y binder, right associativity). -The principle is the same as in Section 12.1.12 except that in the iterator +The principle is the same as in :ref:`RecursiveNotations` +except that in the iterator :math:`φ([~]_E , [~]_I)`, the placeholder :math:`[~]_E` can also occur in position of the binding variable of a ``fun`` or a ``forall``. @@ -620,8 +624,8 @@ binders, ``x`` and ``y`` must be marked as ``binder`` in the list of modifiers of the notation. The binders of the parsed sequence are used to fill the occurrences of the first placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the -generalization operator ``'`` (see Section 2.7.19) is used in the binding list, -the added binders are taken into account too. +generalization operator ``'`` (see :ref:`implicit-generalization`) is +used in the binding list, the added binders are taken into account too. Binders parsing exist in two flavors. If ``x`` and ``y`` are marked as binder, then a sequence such as :g:`a b c : T` will be accepted and interpreted as @@ -678,7 +682,7 @@ position of :g:`x`: In addition to ``global``, one can restrict the syntax of a sub-expression by using the entry names ``ident`` or ``pattern`` -already seen in Section :ref:`NotationsWithBinders`, even when the +already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: @@ -690,10 +694,14 @@ side. E.g.: Summary ~~~~~~~ -**Syntax of notations** +.. _NotationSyntax: + +Syntax of notations ++++++++++++++++++++ The different syntactic variants of the command Notation are given on the -following figure. The optional :token:`scope` is described in the Section 12.2. +following figure. The optional :production:`scope` is described in +:ref:`Scopes`. .. productionlist:: coq notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. @@ -743,14 +751,15 @@ following figure. The optional :token:`scope` is described in the Section 12.2. given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). -**Persistence of notations** +Persistence of notations +++++++++++++++++++++++++ Notations do not survive the end of sections. .. cmd:: Local Notation @notation Notations survive modules unless the command ``Local Notation`` is used instead - of ``Notation``. + of :cmd:`Notation`. .. _Scopes: @@ -762,13 +771,13 @@ interpretation. Interpretation scopes provide a weak, purely syntactical form of notations overloading: the same notation, for instance the infix symbol ``+`` can be used to denote distinct definitions of the additive operator. Depending on which interpretation -scopes is currently open, the interpretation is different. +scopes are currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See Figure 12.1 for the syntax of notations including the possibility -to declare them in a given scope. Here is a typical example which +See :ref:`above <NotationSyntax>` for the syntax of notations including the +possibility to declare them in a given scope. Here is a typical example which declares the notation for conjunction in the scope ``type_scope``. .. coqdoc:: @@ -892,27 +901,27 @@ Binding arguments of a constant to an interpretation scope turn to be themselves arguments of a reference are interpreted accordingly to the arguments scopes bound to this reference. -.. cmdv:: Arguments @qualid : clear scopes + .. cmdv:: Arguments @qualid : clear scopes - Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. + Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. -.. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes + .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes - Defines extra argument scopes, to be used in case of coercion to Funclass - (see Chapter :ref:`implicitcoercions`) or with a computed type. + Defines extra argument scopes, to be used in case of coercion to ``Funclass`` + (see the :ref:`implicitcoercions` chapter) or with a computed type. -.. cmdv:: Global Arguments @qualid {+ @name%@scope} + .. cmdv:: Global Arguments @qualid {+ @name%@scope} - This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a - section is closed instead of stopping working at section closing. Without the - ``Global`` modifier, the effect of the command stops when the section it belongs - to ends. + This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a + section is closed instead of stopping working at section closing. Without the + ``Global`` modifier, the effect of the command stops when the section it belongs + to ends. -.. cmdv:: Local Arguments @qualid {+ @name%@scope} + .. cmdv:: Local Arguments @qualid {+ @name%@scope} - This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not - survive modules and files. Without the ``Local`` modifier, the effect of the - command is visible from within other modules or files. + This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not + survive modules and files. Without the ``Local`` modifier, the effect of the + command is visible from within other modules or files. .. seealso:: @@ -947,18 +956,18 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it - to this type. When a scope ``scope`` is bound to a type type, any new function - defined later on gets its arguments of type type interpreted by default in + to this type. When a scope ``scope`` is bound to a type ``type``, any new function + defined later on gets its arguments of type ``type`` interpreted by default in scope scope (this default behavior can however be overwritten by explicitly - using the command ``Arguments``). + using the command :cmd:`Arguments`). Whether the argument of a function has some type ``type`` is determined - statically. For instance, if f is a polymorphic function of type :g:`forall - X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, then :g:`a` of - type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted - in scope ``scope``. + statically. For instance, if ``f`` is a polymorphic function of type + :g:`forall X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, + then :g:`a` of type :g:`t` in :g:`f t a` is not recognized as an argument to + be interpreted in scope ``scope``. - More generally, any coercion :n:`@class` (see Chapter :ref:`implicitcoercions`) + More generally, any coercion :n:`@class` (see the :ref:`implicitcoercions` chapter) can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` @@ -980,12 +989,6 @@ Binding types of arguments to an interpretation scope .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. -.. seealso:: - - :cmd:`About` - The command to show the scopes bound to the arguments of a - function is described in Section 2. - The ``type_scope`` interpretation scope ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -996,7 +999,7 @@ scope which is temporarily activated each time a subterm of an expression is expected to be a type. It is delimited by the key ``type``, and bound to the coercion class ``Sortclass``. It is also used in certain situations where an expression is statically known to be a type, including the conclusion and the -type of hypotheses within an Ltac goal match (see Section +type of hypotheses within an Ltac goal match (see :ref:`ltac-match-goal`), the statement of a theorem, the type of a definition, the type of a binder, the domain and codomain of implication, the codomain of products, and more generally any type argument of a declared or defined @@ -1017,8 +1020,8 @@ Interpretation scopes used in the standard library of Coq ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We give an overview of the scopes used in the standard library of Coq. -For a complete list of notations in each scope, use the commands Print -Scopes or Print Scope scope. +For a complete list of notations in each scope, use the commands :cmd:`Print +Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It @@ -1084,7 +1087,7 @@ Scopes or Print Scope scope. ``string_scope`` This scope includes notation for strings as elements of the type string. Special characters and escaping follow Coq conventions on strings (see - Section 1.1). Especially, there is no convention to visualize non + :ref:`lexical-conventions`). Especially, there is no convention to visualize non printable characters of a string. The file :file:`String.v` shows an example that contains quotes, a newline and a beep (i.e. the ASCII character of code 7). @@ -1093,8 +1096,8 @@ Scopes or Print Scope scope. This scope includes interpretation for all strings of the form ``"c"`` where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is a three-digits number (possibly with leading 0's), or of the form - ``""""``. Their respective denotations are the ASCII code of c, the - decimal ASCII code nnn, or the ascii code of the character ``"`` (i.e. + ``""""``. Their respective denotations are the ASCII code of :g:`c`, the + decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e. the ASCII code 34), all of them being represented in the type :g:`ascii`. @@ -1109,25 +1112,26 @@ Displaying informations about scopes by the same notation in a more recently open scope are not displayed. Hence each notation is displayed only once. -.. cmdv:: Print Visibility scope - - This displays the current stack of notations in scopes and lonely - notations assuming that scope is pushed on top of the stack. This is - useful to know how a subterm locally occurring in the scope ofscope is - interpreted. - -.. cmdv:: Print Scope scope + .. cmdv:: Print Visibility @scope - This displays all the notations defined in interpretation scopescope. - It also displays the delimiting key if any and the class to which the - scope is bound, if any. + This displays the current stack of notations in scopes and lonely + notations assuming that :token:`scope` is pushed on top of the stack. This is + useful to know how a subterm locally occurring in the scope :token:`scope` is + interpreted. -.. cmdv:: Print Scopes +.. cmd:: Print Scopes This displays all the notations, delimiting keys and corresponding class of all the existing interpretation scopes. It also displays the lonely notations. + .. cmdv:: Print Scope @scope + :name: Print Scope + + This displays all the notations defined in interpretation scope :token:`scope`. + It also displays the delimiting key if any and the class to which the + scope is bound, if any. + .. _Abbreviations: Abbreviations @@ -1324,7 +1328,7 @@ tactic language. Tactic notations obey the following syntax: .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as no associative but the parser on +.. [#no_associativity] Coq accepts notations declared as ``no associative`` but the parser on which Coq is built, namely Camlp4, currently does not implement the - no-associativity and replaces it by a left associativity; hence it is - the same for Coq: no-associativity is in fact left associativity + ``no associativity`` and replaces it by a ``left associativity``; hence it is + the same for Coq: ``no associativity`` is in fact ``left associativity``. diff --git a/lib/envars.ml b/lib/envars.ml index be82bfe9b..3ee0c7106 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,6 +110,7 @@ let check_file_else ~dir ~file oth = if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = + getenv_else "COQLIB" (fun () -> let prelude = "theories/Init/Prelude.vo" in check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude (fun () -> @@ -117,6 +118,7 @@ let guess_coqlib fail = then Coq_config.coqlib else fail "cannot guess a path for Coq libraries; please use -coqlib option") + ) (** coqlib is now computed once during coqtop initialization *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6b9b10312..5fc4293cb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1499,7 +1499,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v new file mode 100644 index 000000000..42236a531 --- /dev/null +++ b/test-suite/success/uniform_inductive_parameters.v @@ -0,0 +1,13 @@ +Set Uniform Inductive Parameters. + +Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. +Check (list : Type -> Type). +Check (cons : forall A, A -> list A -> list A). + +Inductive list2 (A : Type) (A' := prod A A) := + | nil2 : list2 + | cons2 : A' -> list2 -> list2. +Check (list2 : Type -> Type). +Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 0387b32ba..ad1ffa35a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -146,7 +146,6 @@ let interp_cstrs env sigma impls mldata arity ind = let sigma, (ctyps'', cimpls) = on_snd List.split @@ List.fold_left_map (fun sigma l -> - on_snd (on_fst EConstr.Unsafe.to_constr) @@ interp_type_evars_impls env sigma ~impls l) sigma ctyps' in sigma, (cnames, ctyps'', cimpls) @@ -327,14 +326,17 @@ let check_param = function | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") -let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = +let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; - let env0 = Global.env() in + if not (List.is_empty uparamsl) && not (List.is_empty notations) + then user_err (str "Inductives with uniform parameters may not have attached notations."); let pl = (List.hd indl).ind_univs in let sigma, decl = interp_univ_decl_opt env0 pl in + let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = + interp_context_evars env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = - interp_context_evars env0 sigma paramsl + interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -346,15 +348,15 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in - let env_ar = push_types env0 indnames fullarities in + let env_ar = push_types env_uparams indnames fullarities in let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env0 sigma (Inductive (params,true)) indnames fullarities indimpls in + let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in let sigma, constructors = @@ -365,6 +367,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl) () in + (* generalize over the uniform parameters *) + let nparams = Context.Rel.length ctx_params in + let nuparams = Context.Rel.length ctx_uparams in + let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in + let uparam_subst = + List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs)) + @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in + let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in + let constructors = List.map (fun (cnames,ctypes,cimpls) -> + (cnames,List.map generalize_constructor ctypes,cimpls)) + constructors + in + let ctx_params = ctx_params @ ctx_uparams in + let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in + let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in + let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in + let env_ar = push_types env0 indnames fullarities in + let env_ar_params = EConstr.push_rel_context ctx_params env_ar in + (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in (* Compute renewed arities *) @@ -423,6 +444,9 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = + interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite + (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 @@ -505,10 +529,15 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl cum poly prv finite = - let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + +let do_mutual_inductive indl cum poly prv ~uniform finite = + let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in + let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7ae8e8f71..4e30ed7de 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -19,9 +19,14 @@ open Decl_kinds (** Entry points for the vernacular commands Inductive and CoInductive *) +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + polymorphic -> private_flag -> uniform:uniform_inductive_flag -> + Declarations.recursivity_kind -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6d1abeca1..5fda1a0da 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -537,6 +537,13 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () +let uniform_inductive_parameters = ref false + +let should_treat_as_uniform () = + if !uniform_inductive_parameters + then ComInductive.UniformParameters + else ComInductive.NonUniformParameters + let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = @@ -642,7 +649,8 @@ let vernac_inductive ~atts cum lo finite indl = in let indl = List.map unpack indl in let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -1471,6 +1479,14 @@ let _ = optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = + declare_bool_option + { optdepr = false; + optname = "Uniform inductive parameters"; + optkey = ["Uniform"; "Inductive"; "Parameters"]; + optread = (fun () -> !uniform_inductive_parameters); + optwrite = (fun b -> uniform_inductive_parameters := b) } + +let _ = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; @@ -2089,7 +2105,7 @@ let interp ?proof ~atts ~st c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption ((discharge,kind),nl,l) -> vernac_assumption ~atts discharge kind l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l |