diff options
60 files changed, 555 insertions, 2301 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index eb2797101..192a2b181 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -137,8 +137,7 @@ /plugins/derive/ @aspiwack # Secondary maintainer @ppedrot -/plugins/extraction/ @letouzey -# Secondary maintainer @maximedenes +/plugins/extraction/ @maximedenes /plugins/firstorder/ @PierreCorbineau # Secondary maintainer @herbelin @@ -159,10 +158,6 @@ /plugins/nsatz/ @thery # Secondary maintainer @ppedrot -/plugins/omega/ @letouzey - -/plugins/romega/ @letouzey - /plugins/setoid_ring/ @amahboubi # Secondary maintainer @bgregoir @@ -219,44 +214,34 @@ ########## Standard library ########## -/theories/Arith/ @letouzey -# Secondary maintainer @herbelin +/theories/Arith/ @herbelin -/theories/Bool/ @letouzey -# Secondary maintainer @herbelin +/theories/Bool/ @herbelin /theories/Classes/ @mattam82 # Secondary maintainer @herbelin -/theories/FSets/ @letouzey -# Secondary maintainer @herbelin +/theories/FSets/ @herbelin -/theories/Init/ @letouzey -# Secondary maintainer @ppedrot +/theories/Init/ @ppedrot -/theories/Lists/ @letouzey -# Secondary maintainer @ppedrot +/theories/Lists/ @ppedrot /theories/Logic/ @herbelin # Secondary maintainer @ppedrot -/theories/MSets/ @letouzey -# Secondary maintainer @herbelin +/theories/MSets/ @herbelin -/theories/NArith/ @letouzey -# Secondary maintainer @herbelin +/theories/NArith/ @herbelin -/theories/Numbers/ @letouzey -# Secondary maintainer @herbelin +/theories/Numbers/ @herbelin -/theories/PArith/ @letouzey -# Secondary maintainer @herbelin +/theories/PArith/ @herbelin /theories/Program/ @mattam82 # Secondary maintainer @herbelin -/theories/QArith/ @letouzey -# Secondary maintainer @herbelin +/theories/QArith/ @herbelin /theories/Reals/ @silene # Secondary maintainer @ppedrot @@ -267,26 +252,19 @@ /theories/Setoids/ @mattam82 # Secondary maintainer @ppedrot -/theories/Sets/ @letouzey -# Secondary maintainer @herbelin +/theories/Sets/ @herbelin -/theories/Sorting/ @letouzey -# Secondary maintainer @herbelin +/theories/Sorting/ @herbelin -/theories/Strings/ @letouzey -# Secondary maintainer @herbelin +/theories/Strings/ @herbelin -/theories/Structures/ @letouzey -# Secondary maintainer @herbelin +/theories/Structures/ @herbelin -/theories/Unicode/ @letouzey -# Secondary maintainer @herbelin +/theories/Unicode/ @herbelin -/theories/Wellfounded/ @letouzey -# Secondary maintainer @mattam82 +/theories/Wellfounded/ @mattam82 -/theories/ZArith/ @letouzey -# Secondary maintainer @herbelin +/theories/ZArith/ @herbelin /theories/Compat/ @JasonGross # Secondary maintainer @Zimmi48 @@ -331,14 +309,11 @@ ########## Build system ########## -/Makefile* @letouzey -# Secondary maintainer @gares +/Makefile* @gares -/configure* @letouzey -# Secondary maintainer @ejgallego +/configure* @ejgallego /META.coq @ejgallego -# Secondary maintainer @letouzey /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 11614bc38..7c451af26 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -55,7 +55,6 @@ after_script: # TODO figure out how to build doc for installed Coq .build-template: &build-template stage: build - retry: 1 artifacts: name: "$CI_JOB_NAME" paths: diff --git a/.travis.yml b/.travis.yml index 42c41249d..ce178c8a6 100644 --- a/.travis.yml +++ b/.travis.yml @@ -67,12 +67,6 @@ matrix: - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-color" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-compcert" EXTRA_OPAM="menhir" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - if: NOT (type = pull_request) env: @@ -82,9 +76,6 @@ matrix: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-fiat-parsers" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-flocq" - if: NOT (type = pull_request) env: @@ -98,9 +89,6 @@ matrix: - if: NOT (type = pull_request) env: - TEST_TARGET="ci-pidetop" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-sf" - env: - TEST_TARGET="lint" @@ -253,7 +241,7 @@ before_install: install: - if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi -- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib; fi +- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib --allow-unauthenticated; fi - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - opam switch "$COMPILER" && opam update - eval $(opam config env) @@ -45,7 +45,15 @@ Tools COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS). -- Remove the gallina utility (extracts specification from Coq vernacular files). +- Removed the gallina utility (extracts specification from Coq vernacular files). + If you would like to maintain this tool externally, please contact us. + +- Removed the Emacs modes distributed with Coq. You are advised to + use Proof-General <https://proofgeneral.github.io/> (and optionally + Company-Coq <https://github.com/cpitclaudel/company-coq>) instead. + If your use case is not covered by these alternative Emacs modes, + please open an issue. We can help set up external maintenance as part + of Proof-General, or independently as part of coq-community. Vernacular Commands @@ -60,6 +68,8 @@ Vernacular Commands - 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. +- Added generic syntax for “attributes”, as in: + `#[local] Lemma foo : bar.` Coq binaries and process model diff --git a/Makefile.build b/Makefile.build index cd145ae64..2e14dab54 100644 --- a/Makefile.build +++ b/Makefile.build @@ -377,7 +377,7 @@ grammar/grammar.cma : $(GRAMCMO) $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ -grammar/coqpp: $(COQPPCMO) grammar/coqpp_main.ml +$(COQPP): $(COQPPCMO) grammar/coqpp_main.ml $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -o $@ @@ -764,14 +764,14 @@ plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLYACC $<' $(HIDE)$(OCAMLYACC) --strict "$*.mly" -%.ml: %.ml4 $(CAMLP5DEPS) grammar/coqpp +%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP) $(SHOW)'CAMLP5O $<' $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ -%.ml: %.mlg grammar/coqpp +%.ml: %.mlg $(COQPP) $(SHOW)'COQPP $<' - $(HIDE)grammar/coqpp $< + $(HIDE)$(COQPP) $< ########################################################################### # Dependencies of ML code diff --git a/Makefile.common b/Makefile.common index 96d0d2ed8..fdaa94212 100644 --- a/Makefile.common +++ b/Makefile.common @@ -21,6 +21,7 @@ COQTOPEXE:=bin/coqtop$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) COQDEP:=bin/coqdep$(EXE) +COQPP:=bin/coqpp$(EXE) COQDEPBYTE:=bin/coqdep.byte$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE) @@ -40,7 +41,7 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) + $(COQWORKMGR) $(COQPP) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) diff --git a/Makefile.install b/Makefile.install index 91870aff7..be6fe5493 100644 --- a/Makefile.install +++ b/Makefile.install @@ -43,7 +43,6 @@ FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) else @@ -52,14 +51,13 @@ FULLCOQLIB=$(COQLIBINSTALL) FULLCONFIGDIR=$(CONFIGDIR) FULLDATADIR=$(DATADIR) FULLMANDIR=$(MANDIR) -FULLEMACSLIB=$(EMACSLIB) FULLCOQDOCDIR=$(COQDOCDIR) FULLDOCDIR=$(DOCDIR) endif .PHONY: install-coq install-binaries install-byte install-opt .PHONY: install-tools install-library install-devfiles install-merlin -.PHONY: install-coq-info install-coq-manpages install-emacs install-latex +.PHONY: install-coq-info install-coq-manpages install-latex .PHONY: install-meta install-coq: install-binaries install-library install-coq-info install-devfiles @@ -136,7 +134,7 @@ endif rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) -install-coq-info: install-coq-manpages install-emacs install-latex +install-coq-info: install-coq-manpages install-latex MANPAGES:=man/coq-tex.1 man/coqdep.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ @@ -147,10 +145,6 @@ install-coq-manpages: $(MKDIR) $(FULLMANDIR)/man1 $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1 -install-emacs: - $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/inferior-coq.el $(FULLEMACSLIB) - # command to update TeX' kpathsea database #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null diff --git a/configure.ml b/configure.ml index fde0a409c..194f47c49 100644 --- a/configure.ml +++ b/configure.ml @@ -250,7 +250,6 @@ type preferences = { datadir : string option; mandir : string option; docdir : string option; - emacslib : string option; coqdocdir : string option; ocamlfindcmd : string option; lablgtkdir : string option; @@ -288,7 +287,6 @@ let default = { datadir = None; mandir = None; docdir = None; - emacslib = None; coqdocdir = None; ocamlfindcmd = None; lablgtkdir = None; @@ -386,8 +384,6 @@ let args_options = Arg.align [ "<dir> Where to install man files"; "-docdir", arg_string_option (fun p docdir -> { p with docdir }), "<dir> Where to install doc files"; - "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }), - "<dir> Where to install emacs files"; "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }), "<dir> Where to install Coqdoc style files"; "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }), @@ -1008,8 +1004,6 @@ let install = [ Relative "man", Relative "share/man", Relative "man"; "DOCDIR", "the Coq documentation", !prefs.docdir, Relative "doc", Relative "share/doc/coq", Relative "doc"; - "EMACSLIB", "the Coq Emacs mode", !prefs.emacslib, - Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools"; "COQDOCDIR", "the Coqdoc LaTeX files", !prefs.coqdocdir, Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc"; ] diff --git a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh new file mode 100644 index 000000000..9c4c905fa --- /dev/null +++ b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=rm-campl4-remains + +if [ "$CI_PULL_REQUEST" = "7898" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + pidetop_CI_BRANCH="$_OVERLAY_BRANCH" + pidetop_CI_GITURL=https://github.com/ppedrot/pidetop + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6d5023405..1eea2443f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -88,6 +88,11 @@ Primitive number parsers have been split over three files (plugins/syntax/positive_syntax.ml, plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml). +Parsing + +- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules + Pcoq.Entry and Pcoq.Parsable were introduced to replace it. + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index b35571e9c..48671c03b 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -10,9 +10,9 @@ versions of Proof General. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). -OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). +OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). -Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). +Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). * [Commands](#commands) - [About](#command-about) diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index 5205350a6..9864fd4d6 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,11 +1,34 @@ #!/usr/bin/env bash -# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging] - set -e -PRNUM=$1 -OPTION=$2 +if [[ $# == 0 ]]; then + echo "Usage: $0 [--no-conflict] [--no-signature-check] [--stop-before-merging] prnum" + exit 1 +fi + +while [[ $# -gt 0 ]]; do + case "$1" in + --no-conflict) + NO_CONFLICTS="true" + shift + ;; + --no-signature-check) + NO_SIGNATURE_CHECK="true" + shift + ;; + --stop-before-merging) + STOP_BEFORE_MERGING="true" + shift + ;; + *) + if [[ "$PRNUM" != "" ]]; then + echo "PRNUM was already set to $PRNUM and is now being overridden with $1." + fi + PRNUM="$1" + shift + esac +done if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then echo "PR #${PRNUM} does not exist." @@ -14,7 +37,7 @@ fi SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?") git log master --grep "Merge PR #${PRNUM}" --format="%GG" -if [[ "${SIGNATURE_STATUS}" != "G" ]]; then +if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then echo read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r echo @@ -30,6 +53,14 @@ MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merg if git checkout -b "${BRANCH}"; then if ! git cherry-pick -x "${RANGE}"; then + if [[ "$NO_CONFLICTS" == "true" ]]; then + git status + echo "Conflicts! Aborting..." + git cherry-pick --abort + git checkout - + git branch -d "$BRANCH" + exit 1 + fi echo "Please fix the conflicts, then exit." bash while ! git cherry-pick --continue; do @@ -59,7 +90,7 @@ if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then fi fi -if [[ "${OPTION}" == "--stop-before-merging" ]]; then +if [[ "$STOP_BEFORE_MERGING" == "true" ]]; then exit 0 fi diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index e13625286..ac6a20198 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -103,7 +103,7 @@ Special tokens ! % & && ( () ) * + ++ , - -> . .( .. / /\ : :: :< := :> ; < <- <-> <: <= <> = => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |- - || } ~ + || } ~ #[ Lexical ambiguities are resolved according to the “longest match” rule: when a sequence of non alphanumerical characters can be @@ -495,6 +495,7 @@ The Vernacular ============== .. productionlist:: coq + decorated-sentence : [`decoration`] `sentence` sentence : `assumption` : | `definition` : | `inductive` @@ -523,6 +524,11 @@ The Vernacular proof : Proof . … Qed . : | Proof . … Defined . : | Proof . … Admitted . + decoration : #[ `attributes` ] + attributes : [`attribute`, … , `attribute`] + attribute : `ident` + :| `ident` = `string` + :| `ident` ( `attributes` ) .. todo:: This use of … in this grammar is inconsistent What about removing the proof part of this grammar from this chapter @@ -534,6 +540,9 @@ commands of Gallina. A sentence of the vernacular language, like in many natural languages, begins with a capital letter and ends with a dot. +Sentences may be *decorated* with so-called *attributes*, +which are described in the corresponding section (:ref:`gallina-attributes`). + The different kinds of command are described hereafter. They all suppose that the terms occurring in the sentences are well-typed. @@ -1388,3 +1397,53 @@ using the keyword :cmd:`Qed`. .. [2] Except if the inductive type is empty in which case there is no equation that can be used to infer the return type. + +.. _gallina-attributes: + +Attributes +----------- + +Any vernacular command can be decorated with a list of attributes, enclosed +between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) +and separated by commas ``,``. + +Each attribute has a name (an identifier) and may have a value. +A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), +or a list of attributes, enclosed within brackets. + +Currently, +the following attributes names are recognized: + +``monomorphic``, ``polymorphic`` + Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags + (see :ref:`polymorphicuniverses`). + +``program`` + Takes no value, analogous to the ``Program`` flag + (see :ref:`programs`). + +``global``, ``local`` + Take no value, analogous to the ``Global`` and ``Local`` flags + (see :ref:`controlling-locality-of-commands`). + +``deprecated`` + Takes as value the optional attributes ``since`` and ``note``; + both have a string value. + +Here are a few examples: + +.. coqtop:: all reset + + From Coq Require Program. + #[program] Definition one : nat := S _. + Next Obligation. + exact O. + Defined. + + #[deprecated(since="8.9.0", note="use idtac instead")] + Ltac foo := idtac. + + Goal True. + Proof. + now foo. + Abort. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 64d4773a2..bdaa2aa1a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -950,55 +950,6 @@ There are options to produce the |Coq| parts in smaller font, italic, between horizontal rules, etc. See the man page of ``coq-tex`` for more details. -|Coq| and GNU Emacs ------------------------ - - -The |Coq| Emacs mode -~~~~~~~~~~~~~~~~~~~~~~~~~ - -|Coq| comes with a Major mode for GNU Emacs, ``gallina.el``. This mode -provides syntax highlighting and also a rudimentary indentation -facility in the style of the ``Caml`` GNU Emacs mode. - -Add the following lines to your ``.emacs`` file: - -:: - - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) - - -The |Coq| major mode is triggered by visiting a file with extension ``.v``, -or manually with the command ``M-x coq-mode``. It gives you the correct -syntax table for the |Coq| language, and also a rudimentary indentation -facility: - - -+ pressing ``Tab`` at the beginning of a line indents the line like the - line above; -+ extra tabulations increase the indentation level (by 2 spaces by default); -+ ``M-Tab`` decreases the indentation level. - - -An inferior mode to run |Coq| under Emacs, by Marco Maggesi, is also -included in the distribution, in file ``inferior-coq.el``. Instructions to -use it are contained in this file. - - -Proof-General -~~~~~~~~~~~~~ - -Proof-General is a generic interface for proof assistants based on -Emacs. The main idea is that the |Coq| commands you are editing are sent -to a |Coq| toplevel running behind Emacs and the answers of the system -automatically inserted into other Emacs buffers. Thus you don’t need -to copy-paste the |Coq| material from your files to the |Coq| toplevel or -conversely from the |Coq| toplevel to some files. - -Proof-General is developed and distributed independently of the system -|Coq|. It is freely available at `<https://proofgeneral.github.io/>`_. - Man pages --------- diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 45667b099..ec085a71e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1418,7 +1418,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) dependent in the goal after application of :n:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - + If term is a num, then destruct num behaves asintros until num + + If term is a num, then destruct num behaves as intros until num followed by destruct applied to the last introduced hypothesis. .. note:: @@ -4190,7 +4190,7 @@ datatype: see :ref:`quote` for the full details. Happens when quote is not able to perform inversion properly. -.. tacv:: quote ident {* @ident} +.. tacv:: quote @ident {* @ident} All terms that are built only with :n:`{* @ident}` will be considered by quote as constants rather than variables. diff --git a/ide/idetop.ml b/ide/idetop.ml index 6fb004061..0c3328ee0 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -80,7 +80,7 @@ let set_doc doc = ide_doc := Some doc let add ((s,eid),(sid,verbose)) = let doc = get_doc () in - let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let pa = Pcoq.Parsable.make (Stream.of_string s) in let loc_ast = Stm.parse_sentence ~doc sid pa in let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in set_doc doc; @@ -113,14 +113,14 @@ let edit_at id = * be removed in the next version of the protocol. *) let query (route, (s,id)) = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let pa = Pcoq.Parsable.make (Stream.of_string s) in let doc = get_doc () in Stm.query ~at:id ~doc ~route pa let annotate phrase = let doc = get_doc () in let {CAst.loc;v=ast} = - let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in + let pa = Pcoq.Parsable.make (Stream.of_string phrase) in Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa in (* XXX: Width should be a parameter of annotate... *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 997ea78e6..6726603e6 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -86,24 +86,15 @@ module type S = type internal_entry = Tok.t Gramext.g_entry type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statement = - string option * Gramext.g_assoc option * production_rule list - type extend_statement = - Gramext.position option * single_extend_statement list type coq_parsable - val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable + val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit val comment_state : coq_parsable -> ((int * int) * string) list - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a - end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct include Grammar.GMake(CLexer) @@ -112,15 +103,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct type internal_entry = Tok.t Gramext.g_entry type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statement = - string option * Gramext.g_assoc option * production_rule list - type extend_statement = - Gramext.position option * single_extend_statement list type coq_parsable = parsable * CLexer.lexer_state ref - let parsable ?(file=Loc.ToplevelInput) c = + let coq_parsable ?(file=Loc.ToplevelInput) c = let state = ref (CLexer.init_lexer_state file) in CLexer.set_lexer_state !state; let a = parsable c in @@ -145,11 +131,23 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let comment_state (p,state) = CLexer.get_comment_state !state - let entry_print ft x = Entry.print ft x +end + +module Parsable = +struct + type t = G.coq_parsable + let make = G.coq_parsable + let comment_state = G.comment_state +end + +module Entry = +struct + + type 'a t = 'a Grammar.GMake(CLexer).Entry.e - (* Not used *) - let srules' = Gramext.srules - let parse_tokens_after_filter = Entry.parse_token + let create = G.Entry.create + let parse = G.entry_parse + let print = G.Entry.print end @@ -246,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function | Aentryl (e, n) -> Symbols.snterml (G.Entry.obj e, n) | Arules rs -> - G.srules' (List.map symbol_of_rules rs) + Gramext.srules (List.map symbol_of_rules rs) and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function | Stop -> fun accu -> accu @@ -364,14 +362,14 @@ let make_rule r = [None, None, r] (** An entry that checks we reached the end of the input. *) let eoi_entry en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in + let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in let act = Gram.action (fun _ x loc -> x) in uncurry (Gram.extend e) (None, make_rule [symbs, act]); e let map_entry f en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in + let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = [Symbols.snterm (Gram.Entry.obj en)] in let act = Gram.action (fun x loc -> f x) in uncurry (Gram.extend e) (None, make_rule [symbs, act]); @@ -381,7 +379,7 @@ let map_entry f en = (use eoi_entry) *) let parse_string f x = - let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) + let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm) type gram_universe = string @@ -402,14 +400,14 @@ let get_univ u = let new_entry u s = let ename = u ^ ":" ^ s in - let e = Gram.entry_create ename in + let e = Entry.create ename in e let make_gen_entry u s = new_entry u s module GrammarObj = struct - type ('r, _, _) obj = 'r Gram.entry + type ('r, _, _) obj = 'r Entry.t let name = "grammar" let default _ = None end @@ -419,7 +417,7 @@ module Grammar = Register(GrammarObj) let register_grammar = Grammar.register0 let genarg_grammar = Grammar.obj -let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t = let e = new_entry u s in let Rawwit t = etyp in let () = Grammar.register0 t e in @@ -431,38 +429,38 @@ module Prim = struct let gec_gen n = make_gen_entry uprim n - (* Entries that can be referred via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Entry.t table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen "preident" let ident = gec_gen "ident" let natural = gec_gen "natural" let integer = gec_gen "integer" - let bigint = Gram.entry_create "Prim.bigint" + let bigint = Entry.create "Prim.bigint" let string = gec_gen "string" - let lstring = Gram.entry_create "Prim.lstring" + let lstring = Entry.create "Prim.lstring" let reference = make_gen_entry uprim "reference" - let by_notation = Gram.entry_create "by_notation" - let smart_global = Gram.entry_create "smart_global" + let by_notation = Entry.create "by_notation" + let smart_global = Entry.create "smart_global" (* parsed like ident but interpreted as a term *) let var = gec_gen "var" - let name = Gram.entry_create "Prim.name" - let identref = Gram.entry_create "Prim.identref" - let univ_decl = Gram.entry_create "Prim.univ_decl" - let ident_decl = Gram.entry_create "Prim.ident_decl" - let pattern_ident = Gram.entry_create "pattern_ident" - let pattern_identref = Gram.entry_create "pattern_identref" + let name = Entry.create "Prim.name" + let identref = Entry.create "Prim.identref" + let univ_decl = Entry.create "Prim.univ_decl" + let ident_decl = Entry.create "Prim.ident_decl" + let pattern_ident = Entry.create "pattern_ident" + let pattern_identref = Entry.create "pattern_identref" (* A synonym of ident - maybe ident will be located one day *) - let base_ident = Gram.entry_create "Prim.base_ident" + let base_ident = Entry.create "Prim.base_ident" - let qualid = Gram.entry_create "Prim.qualid" - let fullyqualid = Gram.entry_create "Prim.fullyqualid" - let dirpath = Gram.entry_create "Prim.dirpath" + let qualid = Entry.create "Prim.qualid" + let fullyqualid = Entry.create "Prim.fullyqualid" + let dirpath = Entry.create "Prim.dirpath" - let ne_string = Gram.entry_create "Prim.ne_string" - let ne_lstring = Gram.entry_create "Prim.ne_lstring" + let ne_string = Entry.create "Prim.ne_string" + let ne_lstring = Entry.create "Prim.ne_lstring" end @@ -470,7 +468,7 @@ module Constr = struct let gec_constr = make_gen_entry uconstr - (* Entries that can be referred via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Entry.t table *) let constr = gec_constr "constr" let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr @@ -481,29 +479,29 @@ module Constr = let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let sort_family = make_gen_entry uconstr "sort_family" - let pattern = Gram.entry_create "constr:pattern" + let pattern = Entry.create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" - let closed_binder = Gram.entry_create "constr:closed_binder" - let binder = Gram.entry_create "constr:binder" - let binders = Gram.entry_create "constr:binders" - let open_binders = Gram.entry_create "constr:open_binders" - let binders_fixannot = Gram.entry_create "constr:binders_fixannot" - let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint" - let record_declaration = Gram.entry_create "constr:record_declaration" - let appl_arg = Gram.entry_create "constr:appl_arg" + let closed_binder = Entry.create "constr:closed_binder" + let binder = Entry.create "constr:binder" + let binders = Entry.create "constr:binders" + let open_binders = Entry.create "constr:open_binders" + let binders_fixannot = Entry.create "constr:binders_fixannot" + let typeclass_constraint = Entry.create "constr:typeclass_constraint" + let record_declaration = Entry.create "constr:record_declaration" + let appl_arg = Entry.create "constr:appl_arg" end module Module = struct - let module_expr = Gram.entry_create "module_expr" - let module_type = Gram.entry_create "module_type" + let module_expr = Entry.create "module_expr" + let module_type = Entry.create "module_type" end let epsilon_value f e = let r = Rule (Next (Stop, e), fun x _ -> f x) in let ext = of_coq_extend_statement (None, [None, None, [r]]) in - let entry = G.entry_create "epsilon" in + let entry = Gram.entry_create "epsilon" in let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None @@ -608,7 +606,7 @@ let () = (** Registering extra grammar *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Entry.t -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 154de1221..029c43713 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -16,82 +16,40 @@ open Libnames (** The parser of Coq *) +(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE. + We only have it here to work with Camlp5. Handwritten grammar extensions + should use the safe [Pcoq.grammar_extend] function below. *) module Gram : sig include Grammar.S with type te = Tok.t -(* Where Grammar.S is - -module type S = - sig - type te = 'x; - type parsable = 'x; - value parsable : Stream.t char -> parsable; - value tokens : string -> list (string * int); - value glexer : Plexing.lexer te; - value set_algorithm : parse_algorithm -> unit; - module Entry : - sig - type e 'a = 'y; - value create : string -> e 'a; - value parse : e 'a -> parsable -> 'a; - value parse_token : e 'a -> Stream.t te -> 'a; - value name : e 'a -> string; - value of_parser : string -> (Stream.t te -> 'a) -> e 'a; - value print : Format.formatter -> e 'a -> unit; - external obj : e 'a -> Gramext.g_entry te = "%identity"; - end - ; - module Unsafe : - sig - value gram_reinit : Plexing.lexer te -> unit; - value clear_entry : Entry.e 'a -> unit; - end - ; - value extend : - Entry.e 'a -> option Gramext.position -> - list - (option string * option Gramext.g_assoc * - list (list (Gramext.g_symbol te) * Gramext.g_action)) -> - unit; - value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; - end + type 'a entry = 'a Entry.e + [@@ocaml.deprecated "Use [Pcoq.Entry.t]"] -*) + [@@@ocaml.warning "-3"] - type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statement = - string option * Gramext.g_assoc option * production_rule list - type extend_statement = - Gramext.position option * single_extend_statement list - - type coq_parsable - - val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable - val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit - - (* Get comment parsing information from the Lexer *) - val comment_state : coq_parsable -> ((int * int) * string) list + [@@ocaml.deprecated "Use [Pcoq.Entry.create]"] val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit - (* Apparently not used *) - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a + [@@@ocaml.warning "+3"] end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e -module Symbols : sig +module Parsable : +sig + type t + val make : ?file:Loc.source -> char Stream.t -> t + (* Get comment parsing information from the Lexer *) + val comment_state : t -> ((int * int) * string) list +end - val stoken : Tok.t -> Gram.symbol - val snterm : Gram.internal_entry -> Gram.symbol +module Entry : sig + type 'a t = 'a Grammar.GMake(CLexer).Entry.e + val create : string -> 'a t + val parse : 'a t -> Parsable.t -> 'a + val print : Format.formatter -> 'a t -> unit end (** The parser of Coq is built from three kinds of rule declarations: @@ -175,86 +133,86 @@ val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit (** Parse a string *) -val parse_string : 'a Gram.entry -> string -> 'a -val eoi_entry : 'a Gram.entry -> 'a Gram.entry -val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry +val parse_string : 'a Entry.t -> string -> 'a +val eoi_entry : 'a Entry.t -> 'a Entry.t +val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t type gram_universe val get_univ : string -> gram_universe val create_universe : string -> gram_universe -val new_entry : gram_universe -> string -> 'a Gram.entry +val new_entry : gram_universe -> string -> 'a Entry.t val uprim : gram_universe val uconstr : gram_universe val utactic : gram_universe -val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit -val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry +val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit +val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t val create_generic_entry : gram_universe -> string -> - ('a, rlevel) abstract_argument_type -> 'a Gram.entry + ('a, rlevel) abstract_argument_type -> 'a Entry.t module Prim : sig open Names open Libnames - val preident : string Gram.entry - val ident : Id.t Gram.entry - val name : lname Gram.entry - val identref : lident Gram.entry - val univ_decl : universe_decl_expr Gram.entry - val ident_decl : ident_decl Gram.entry - val pattern_ident : Id.t Gram.entry - val pattern_identref : lident Gram.entry - val base_ident : Id.t Gram.entry - val natural : int Gram.entry - val bigint : Constrexpr.raw_natural_number Gram.entry - val integer : int Gram.entry - val string : string Gram.entry - val lstring : lstring Gram.entry - val reference : qualid Gram.entry - val qualid : qualid Gram.entry - val fullyqualid : Id.t list CAst.t Gram.entry - val by_notation : (string * string option) Gram.entry - val smart_global : qualid or_by_notation Gram.entry - val dirpath : DirPath.t Gram.entry - val ne_string : string Gram.entry - val ne_lstring : lstring Gram.entry - val var : lident Gram.entry + val preident : string Entry.t + val ident : Id.t Entry.t + val name : lname Entry.t + val identref : lident Entry.t + val univ_decl : universe_decl_expr Entry.t + val ident_decl : ident_decl Entry.t + val pattern_ident : Id.t Entry.t + val pattern_identref : lident Entry.t + val base_ident : Id.t Entry.t + val natural : int Entry.t + val bigint : Constrexpr.raw_natural_number Entry.t + val integer : int Entry.t + val string : string Entry.t + val lstring : lstring Entry.t + val reference : qualid Entry.t + val qualid : qualid Entry.t + val fullyqualid : Id.t list CAst.t Entry.t + val by_notation : (string * string option) Entry.t + val smart_global : qualid or_by_notation Entry.t + val dirpath : DirPath.t Entry.t + val ne_string : string Entry.t + val ne_lstring : lstring Entry.t + val var : lident Entry.t end module Constr : sig - val constr : constr_expr Gram.entry - val constr_eoi : constr_expr Gram.entry - val lconstr : constr_expr Gram.entry - val binder_constr : constr_expr Gram.entry - val operconstr : constr_expr Gram.entry - val ident : Id.t Gram.entry - val global : qualid Gram.entry - val universe_level : Glob_term.glob_level Gram.entry - val sort : Glob_term.glob_sort Gram.entry - val sort_family : Sorts.family Gram.entry - val pattern : cases_pattern_expr Gram.entry - val constr_pattern : constr_expr Gram.entry - val lconstr_pattern : constr_expr Gram.entry - val closed_binder : local_binder_expr list Gram.entry - val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) - val binders : local_binder_expr list Gram.entry (* list of binder *) - val open_binders : local_binder_expr list Gram.entry - val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (lname * bool * constr_expr) Gram.entry - val record_declaration : constr_expr Gram.entry - val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry + val constr : constr_expr Entry.t + val constr_eoi : constr_expr Entry.t + val lconstr : constr_expr Entry.t + val binder_constr : constr_expr Entry.t + val operconstr : constr_expr Entry.t + val ident : Id.t Entry.t + val global : qualid Entry.t + val universe_level : Glob_term.glob_level Entry.t + val sort : Glob_term.glob_sort Entry.t + val sort_family : Sorts.family Entry.t + val pattern : cases_pattern_expr Entry.t + val constr_pattern : constr_expr Entry.t + val lconstr_pattern : constr_expr Entry.t + val closed_binder : local_binder_expr list Entry.t + val binder : local_binder_expr list Entry.t (* closed_binder or variable *) + val binders : local_binder_expr list Entry.t (* list of binder *) + val open_binders : local_binder_expr list Entry.t + val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t + val typeclass_constraint : (lname * bool * constr_expr) Entry.t + val record_declaration : constr_expr Entry.t + val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t end module Module : sig - val module_expr : module_ast Gram.entry - val module_type : module_ast Gram.entry + val module_expr : module_ast Entry.t + val module_type : module_ast Entry.t end val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option @@ -264,7 +222,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option type gram_reinit = gram_assoc * gram_position (** Type of reinitialization data *) -val grammar_extend : 'a Gram.entry -> gram_reinit option -> +val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a Extend.extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive @@ -280,7 +238,7 @@ type 'a grammar_command marshallable. *) type extend_rule = -| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, @@ -310,7 +268,7 @@ val parser_summary_tag : frozen_t Summary.Dyn.tag (** Registering grammars by name *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 737147884..e477b12cd 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -14,12 +14,12 @@ open Constrexpr open Glob_term val wit_orient : bool Genarg.uniform_genarg_type -val orient : bool Pcoq.Gram.entry +val orient : bool Pcoq.Entry.t val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type -val occurrences : (int list Locus.or_var) Pcoq.Gram.entry +val occurrences : (int list Locus.or_var) Pcoq.Entry.t val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type val pr_occurrences : int list Locus.or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences @@ -46,8 +46,8 @@ val wit_casted_constr : Tacexpr.glob_constr_and_expr, EConstr.t) Genarg.genarg_type -val glob : constr_expr Pcoq.Gram.entry -val lglob : constr_expr Pcoq.Gram.entry +val glob : constr_expr Pcoq.Entry.t +val lglob : constr_expr Pcoq.Entry.t type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location @@ -55,10 +55,10 @@ type loc_place = lident gen_place type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type -val hloc : loc_place Pcoq.Gram.entry +val hloc : loc_place Pcoq.Entry.t val pr_hloc : loc_place -> Pp.t -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t val wit_by_arg_tac : (raw_tactic_expr option, glob_tactic_expr option, @@ -68,13 +68,13 @@ val pr_by_arg_tac : (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t -val test_lpar_id_colon : unit Pcoq.Gram.entry +val test_lpar_id_colon : unit Pcoq.Entry.t val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type (** Spiwack: Primitive for retroknowledge registration *) -val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry +val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type val wit_in_clause : diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 620f14707..9d86f21d4 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -46,10 +46,10 @@ let reference_to_id qid = CErrors.user_err ?loc:qid.CAst.loc (str "This expression should be a simple identifier.") -let tactic_mode = Gram.entry_create "vernac:tactic_command" +let tactic_mode = Entry.create "vernac:tactic_command" let new_entry name = - let e = Gram.entry_create name in + let e = Entry.create name in e let toplevel_selector = new_entry "vernac:toplevel_selector" diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index e9711268c..759bb62fd 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -11,11 +11,10 @@ open Pcoq (* Main entry for extensions *) -let simple_tactic = Gram.entry_create "tactic:simple_tactic" +let simple_tactic = Entry.create "tactic:simple_tactic" -let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name) +let make_gen_entry _ name = Entry.create ("tactic:" ^ name) -(* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = make_gen_entry utactic "open_constr" @@ -23,7 +22,7 @@ let constr_with_bindings = make_gen_entry utactic "constr_with_bindings" let bindings = make_gen_entry utactic "bindings" -let hypident = Gram.entry_create "hypident" +let hypident = Entry.create "hypident" let constr_may_eval = make_gen_entry utactic "constr_may_eval" let constr_eval = make_gen_entry utactic "constr_eval" let uconstr = @@ -40,7 +39,7 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Gram.entry_create "tactic:tactic_arg" +let tactic_arg = Entry.create "tactic:tactic_arg" let tactic_expr = make_gen_entry utactic "tactic_expr" let binder_tactic = make_gen_entry utactic "binder_tactic" diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index c5aa542fd..9bff98b6c 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -17,22 +17,22 @@ open Tacexpr open Genredexpr open Tactypes -val open_constr : constr_expr Gram.entry -val constr_with_bindings : constr_expr with_bindings Gram.entry -val bindings : constr_expr bindings Gram.entry -val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry -val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry -val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry -val uconstr : constr_expr Gram.entry -val quantified_hypothesis : quantified_hypothesis Gram.entry -val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry -val int_or_var : int Locus.or_var Gram.entry -val simple_tactic : raw_tactic_expr Gram.entry -val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry -val in_clause : Names.lident Locus.clause_expr Gram.entry -val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry -val tactic_arg : raw_tactic_arg Gram.entry -val tactic_expr : raw_tactic_expr Gram.entry -val binder_tactic : raw_tactic_expr Gram.entry -val tactic : raw_tactic_expr Gram.entry -val tactic_eoi : raw_tactic_expr Gram.entry +val open_constr : constr_expr Entry.t +val constr_with_bindings : constr_expr with_bindings Entry.t +val bindings : constr_expr bindings Entry.t +val hypident : (Names.lident * Locus.hyp_location_flag) Entry.t +val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t +val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t +val uconstr : constr_expr Entry.t +val quantified_hypothesis : quantified_hypothesis Entry.t +val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t +val int_or_var : int Locus.or_var Entry.t +val simple_tactic : raw_tactic_expr Entry.t +val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t +val in_clause : Names.lident Locus.clause_expr Entry.t +val clause_dft_concl : Names.lident Locus.clause_expr Entry.t +val tactic_arg : raw_tactic_arg Entry.t +val tactic_expr : raw_tactic_expr Entry.t +val binder_tactic : raw_tactic_expr Entry.t +val tactic : raw_tactic_expr Entry.t +val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 9bba9ba71..f873631ff 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -55,7 +55,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int -> (** {5 Tactic Quotations} *) val create_ltac_quotation : string -> - ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit + ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit (** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and generates an argument using [f] on the entry parsed by [e]. *) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 6b183dab1..8b9c94f2d 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1408,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg -let ssrorelse = Gram.entry_create "ssrorelse" +let ssrorelse = Entry.create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 7cd3751ce..862a93765 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -12,11 +12,11 @@ open Ltac_plugin -val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c -val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli index bb5161a0e..588a1a3ea 100644 --- a/plugins/ssrmatching/g_ssrmatching.mli +++ b/plugins/ssrmatching/g_ssrmatching.mli @@ -5,13 +5,13 @@ open Genarg open Ssrmatching (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) -val cpattern : cpattern Pcoq.Gram.entry +val cpattern : cpattern Pcoq.Entry.t val wit_cpattern : cpattern uniform_genarg_type (** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) -val lcpattern : cpattern Pcoq.Gram.entry +val lcpattern : cpattern Pcoq.Entry.t val wit_lcpattern : cpattern uniform_genarg_type (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) -val rpattern : rpattern Pcoq.Gram.entry +val rpattern : rpattern Pcoq.Entry.t val wit_rpattern : rpattern uniform_genarg_type diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 93ca9dc5e..2d72b9db6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1699,7 +1699,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = let ty = get_type_of env !evdref t in Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in - let ty = lift (-k) (aux x ty) in + let dummy_subst = List.init k (fun _ -> mkProp) in + let ty = substl dummy_subst (aux x ty) in let depvl = free_rels !evdref ty in let inst = List.map_i diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 440076c16..c94408050 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -311,7 +311,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in mkLambda(name,dom,body) - | _ -> nf_val env sigma v crazy_type + | _ -> assert false and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in diff --git a/stm/stm.ml b/stm/stm.ml index 0aed88a53..e15b6048b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2976,7 +2976,7 @@ let parse_sentence ~doc sid pa = str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur."); Flags.with_option Flags.we_are_parsing (fun () -> try - match Pcoq.Gram.entry_parse Pvernac.main_entry pa with + match Pcoq.Entry.parse Pvernac.main_entry pa with | None -> raise End_of_input | Some (loc, cmd) -> CAst.make ~loc cmd with e when CErrors.noncritical e -> diff --git a/stm/stm.mli b/stm/stm.mli index aed7274d0..50e7f0609 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -92,11 +92,11 @@ val new_doc : stm_init_options -> doc * Stateid.t (** [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> +val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t -> Vernacexpr.vernac_control CAst.t (* Reminder: A parsable [pa] is constructed using - [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) + [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) exception End_of_input @@ -114,7 +114,7 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : doc:doc -> - at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index e01dcbcb6..6be80d29a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -199,11 +199,8 @@ let classify_vernac e = in let rec static_control_classifier ~poly = function | VernacExpr (f, e) -> - let poly = List.fold_left (fun poly f -> - match f with - | VernacPolymorphic b -> b - | (VernacProgram | VernacLocal _) -> poly - ) poly f in + let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in + let poly = atts.Vernacinterp.polymorphic in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> diff --git a/test-suite/bugs/closed/5719.v b/test-suite/bugs/closed/5719.v new file mode 100644 index 000000000..0fad5f54e --- /dev/null +++ b/test-suite/bugs/closed/5719.v @@ -0,0 +1,9 @@ +Axiom cons_data_one : + forall (Aone : unit -> Set) (i : unit) (a : Aone i), nat. +Axiom P : nat -> Prop. +Axiom children_data_rect3 : forall {Aone : unit -> Set} + (cons_one_case : forall (i : unit) (b : Aone i), + nat -> nat -> P (cons_data_one Aone i b)), + P 0. +Fail Definition decide_children_equality IH := children_data_rect3 + (fun _ '(existT _ _ _) => match IH with tt => _ end). diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v new file mode 100644 index 000000000..83fb3d0c8 --- /dev/null +++ b/test-suite/success/attribute-syntax.v @@ -0,0 +1,23 @@ +From Coq Require Program. + +Section Scope. + +#[local] Coercion nat_of_bool (b: bool) : nat := + if b then 0 else 1. + +Check (refl_equal : true = 0 :> nat). + +End Scope. + +Fail Check 0 = true :> nat. + +#[polymorphic] +Definition ι T (x: T) := x. + +Check ι _ ι. + +#[program] +Fixpoint f (n: nat) {wf lt n} : nat := _. + +#[deprecated(since="8.9.0")] +Ltac foo := foo. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 817581cb2..9d60cf54c 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -459,7 +459,7 @@ Proof. destruct e. reflexivity. Defined. -(** The goupoid structure of equality *) +(** The groupoid structure of equality *) Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e. Proof. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 872a73282..8b6822a4e 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -90,9 +90,9 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts -COQMAKE_ONE_TIME_FILE ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-single-timing-files.py" +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" BEFORE ?= AFTER ?= diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a19618dd9..8564aeff6 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -1,6 +1,7 @@ from __future__ import with_statement from __future__ import division from __future__ import unicode_literals +from __future__ import print_function import os, sys, re from io import open @@ -207,7 +208,11 @@ def make_table_string(times_dict, def print_or_write_table(table, files): if len(files) == 0 or '-' in files: - print(table) + try: + binary_stdout = sys.stdout.buffer + except AttributeError: + binary_stdout = sys.stdout + print(table.encode("utf-8"), file=binary_stdout) for file_name in files: if file_name != '-': with open(file_name, 'w', encoding="utf-8") as f: diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el deleted file mode 100644 index 068e64002..000000000 --- a/tools/coq-font-lock.el +++ /dev/null @@ -1,137 +0,0 @@ -;; coq-font-lock.el --- Coq syntax highlighting for Emacs - compatibilty code -;; Pierre Courtieu, may 2009 -;; -;; Authors: Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> - -;; This is copy paste from ProofGeneral by David Aspinall -;; <David.Aspinall@ed.ac.uk>. ProofGeneral is under GPL and Copyright -;; (C) LFCS Edinburgh. - - -;;; Commentary: -;; This file contains the code necessary to coq-syntax.el and -;; coq-db.el from ProofGeneral. It is also pocked from ProofGeneral. - - -;;; History: -;; First created from ProofGeneral may 28th 2009 - - -;;; Code: - -(setq coq-version-is-V8-1 t) -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -;; Generic font-lock - -(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" - "A regular expression for parsing identifiers.") - -;; For font-lock, we treat ,-separated identifiers as one identifier -;; and refontify commata using \{proof-zap-commas}. - -(defun proof-anchor-regexp (e) - "Anchor (\\`) and group the regexp E." - (concat "\\`\\(" e "\\)")) - -(defun proof-ids (proof-id &optional sepregexp) - "Generate a regular expression for separated lists of identifiers PROOF-ID. -Default is comma separated, or SEPREGEXP if set." - (concat proof-id "\\(\\s-*" (or sepregexp ",") "\\s-*" - proof-id "\\)*")) - -(defun proof-ids-to-regexp (l) - "Maps a non-empty list of tokens `L' to a regexp matching any element." - (if (featurep 'xemacs) - (mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version - (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>"))) - -;; TODO: get rid of this list. Does 'default work widely enough -;; by now? -(defconst pg-defface-window-systems - '(x ;; bog standard - mswindows ;; Windows - w32 ;; Windows - gtk ;; gtk emacs (obsolete?) - mac ;; used by Aquamacs - carbon ;; used by Carbon XEmacs - ns ;; NeXTstep Emacs (Emacs.app) - x-toolkit) ;; possible catch all (but probably not) - "A list of possible values for variable `window-system'. -If you are on a window system and your value of variable -`window-system' is not listed here, you may not get the correct -syntax colouring behaviour.") - -(defmacro proof-face-specs (bl bd ow) - "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w." - `(append - (apply 'append - (mapcar - (lambda (ty) (list - (list (list (list 'type ty) '(class color) - (list 'background 'light)) - (quote ,bl)) - (list (list (list 'type ty) '(class color) - (list 'background 'dark)) - (quote ,bd)))) - pg-defface-window-systems)) - (list (list t (quote ,ow))))) - -;;A new face for tactics -(defface coq-solve-tactics-face - (proof-face-specs - (:foreground "forestgreen" t) ; for bright backgrounds - (:foreground "forestgreen" t) ; for dark backgrounds - ()) ; for black and white - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - (proof-face-specs - (:foreground "red" t) ; for bright backgrounds - (:foreground "red" t) ; for dark backgrounds - ()) ; for black and white - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - -(defconst proof-tactics-name-face 'coq-solve-tactics-face) -(defconst proof-tacticals-name-face 'coq-solve-tactics-face) - -(provide 'coq-font-lock) -;;; coq-font-lock.el ends here diff --git a/tools/gallina-db.el b/tools/gallina-db.el deleted file mode 100644 index 9664f69f8..000000000 --- a/tools/gallina-db.el +++ /dev/null @@ -1,240 +0,0 @@ -;;; gallina-db.el --- coq keywords database utility functions -;; -;; Author: Pierre Courtieu <courtieu@lri.fr> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; - -;;; We store all information on keywords (tactics or command) in big -;; tables (ex: `coq-tactics-db') From there we get: menus including -;; "smart" commands, completions for command coq-insert-... -;; abbrev tables and font-lock keyword - -;;; real value defined below - -;;; Commentary: -;; - -;;; Code: - -;(require 'proof-config) ; for proof-face-specs, a macro -;(require 'holes) - -(defconst coq-syntax-db nil - "Documentation-only variable, for coq keyword databases. -Each element of a keyword database contains the definition of a \"form\", of the -form: - -(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE) - -MENUNAME is the name of form (or form variant) as it should appear in menus or -completion lists. - -ABBREV is the abbreviation for completion via \\[expand-abbrev]. - -INSERT is the complete text of the form, which may contain holes denoted by -\"#\" or \"@{xxx}\". - -If non-nil the optional STATECH specifies that the command is not state -preserving for coq. - -If non-nil the optional KWREG is the regexp to colorize correponding to the -keyword. ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\"). -*WARNING*: A regexp longer than another one should be put FIRST. For example: - - (\"Module Type\" ... ... t \"Module\\s-+Type\") - (\"Module\" ... ... t \"Module\") - -Is ok because the longer regexp is recognized first. - -If non-nil the optional INSERT-FUN is the function to be called when inserting -the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This -allows writing functions asking for more information to assist the user. - -If non-nil the optional HIDE specifies that this form should not appear in the -menu but only in interactive completions. - -Example of what could be in your emacs init file: - -(defvar coq-user-tactics-db - '( - (\"mytac\" \"mt\" \"mytac # #\" t \"mytac\") - (\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\") - )) - -Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, -will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a -new keyword to colorize." ) - -(defun coq-insert-from-db (db prompt) - "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion function is -present for the keyword, call it instead. see `coq-syntax-db' for DB -structure." - (let* ((tac (completing-read (concat prompt " (tab for completion) : ") - db nil nil)) - (infos (cddr (assoc tac db))) - (s (car infos)) ; completion to insert - (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function - (pt (point))) - (if f (funcall f) ; call f if present - (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt) - (indent-according-to-mode)))) - - - -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) - -;; Computes the max length of strings in a list -(defun max-length-db (db) - "Return the length of the longest first element (menu label) of DB. -See `coq-syntax-db' for DB structure." - (let ((l db) (res 0)) - (while l - (let ((lgth (length (car (car l))))) - (setq res (max lgth res)) - (setq l (cdr l)))) - res)) - - - -(defun coq-build-menu-from-db-internal (db lgth menuwidth) - "Take a keyword database DB and return one insertion submenu. -Argument LGTH is the max size of the submenu. Argument MENUWIDTH is the width -of the largest line in the menu (without abbrev and shortcut specifications). -Used by `coq-build-menu-from-db', which you should probably use instead. See -`coq-syntax-db' for DB structure." - (let ((l db) (res ()) (size lgth) - (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) - (while (and l (> size 0)) - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - (e6 (car-safe tl5)) ; e6 = function for smart insertion - (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu - (entry-with (max (- menuwidth (length e1)) 0)) - (spaces (make-string entry-with ? )) - ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) - ) - (when (not e7) ;; if not hidden - (let ((menu-entry - (vector - ;; menu entry label - (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) - ;;insertion function if present otherwise insert completion - (if e6 e6 `(holes-insert-and-expand ,e3)) - t))) - (setq res (nconc res (list menu-entry)))));; append *in place* - (setq l tl) - (setq size (- size 1)))) - res)) - - -(defun coq-build-title-menu (db size) - "Build a title for the first submenu of DB, of size SIZE. -Return the string made of the first and the SIZE nth first element of DB, -separated by \"...\". Used by `coq-build-menu-from-db'. See `coq-syntax-db' -for DB structure." - (concat (car-safe (car-safe db)) - " ... " - (car-safe (car-safe (nthcdr (- size 1) db))))) - -(defun coq-sort-menu-entries (menu) - (sort menu - (lambda (x y) (string< - (downcase (elt x 0)) - (downcase (elt y 0)))))) - -(defun coq-build-menu-from-db (db &optional size) - "Take a keyword database DB and return a list of insertion menus for them. -Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB -structure." - ;; sort is destructive for the list, so copy list before sorting - (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) - (wdth (+ 2 (max-length-db db))) - (sz (or size 30)) (lgth (length l))) - (while l - (if (<= lgth sz) - (setq res ;; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l lgth) - (coq-build-menu-from-db-internal l lgth wdth))))) - (setq res ; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l sz) - (coq-build-menu-from-db-internal l sz wdth)))))) - (setq l (nthcdr sz l)) - (setq lgth (length l))) - res)) - -(defun coq-build-abbrev-table-from-db (db) - "Take a keyword database DB and return an abbrev table. -See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - ) - ;; careful: nconc destructive! - (when e2 - (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) - (setq l tl))) - res)) - - -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - '((t (:background "red"))) - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - - - - -(provide 'gallina-db) - -;;; gallina-db.el ends here - -;** Local Variables: *** -;** fill-column: 80 *** -;** End: *** diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el deleted file mode 100644 index 7c59fb6ae..000000000 --- a/tools/gallina-syntax.el +++ /dev/null @@ -1,979 +0,0 @@ -;; gallina-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997-2007 LFCS Edinburgh. -;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu <courtieu@lri.fr> - -;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp - -;(require 'proof-syntax) -;(require 'proof-utils) ; proof-locate-executable -(require 'gallina-db) - - - - ;;; keyword databases - - -(defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for - syntax. It is not necessary to add your own tactics here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your tactics will be colorized by font-lock - - 2 your tactics will be added to the menu and to completion when - calling \\[coq-insert-tactic] - - 3 you may define an abbreviation for your tactic." - - :type '(repeat sexp) - :group 'coq) - - -(defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defvar coq-tactics-db - (append - coq-user-tactics-db - '( - ("absurd " "abs" "absurd " t "absurd") - ("apply" "ap" "apply " t "apply") - ("assert by" "assb" "assert ( # : # ) by #" t "assert") - ("assert" "ass" "assert ( # : # )" t) - ;; ("assumption" "as" "assumption" t "assumption") - ("auto with arith" "awa" "auto with arith" t) - ("auto with" "aw" "auto with @{db}" t) - ("auto" "a" "auto" t "auto") - ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) - ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) - ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) - ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") - ("case" "c" "case " t "case") - ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") - ("change in" "chi" "change # in #" t) - ("change with in" "chwi" "change # with # in #" t) - ("change with" "chw" "change # with" t) - ("change" "ch" "change " t "change") - ("clear" "cl" "clear" t "clear") - ("clearbody" "cl" "clearbody" t "clearbody") - ("cofix" "cof" "cofix" t "cofix") - ("coinduction" "coind" "coinduction" t "coinduction") - ("compare" "cmpa" "compare # #" t "compare") - ("compute" "cmpu" "compute" t "compute") - ;; ("congruence" "cong" "congruence" t "congruence") - ("constructor" "cons" "constructor" t "constructor") - ;; ("contradiction" "contr" "contradiction" t "contradiction") - ("cut" "cut" "cut" t "cut") - ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") - ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") - ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") - ("decompose" "dec" "decompose [#] #" t "decompose") - ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") - ("dependent inversion with" "depinvw" "dependent inversion # with #" t) - ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") - ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t) - ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite") - ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t) - ("destruct as" "desa" "destruct # as #" t) - ("destruct using" "desu" "destruct # using #" t) - ("destruct" "des" "destruct " t "destruct") - ;; ("discriminate" "dis" "discriminate" t "discriminate") - ("discrR" "discrR" "discrR" t "discrR") - ("double induction" "dind" "double induction # #" t "double\\s-+induction") - ("eapply" "eap" "eapply #" t "eapply") - ("eauto with arith" "eawa" "eauto with arith" t) - ("eauto with" "eaw" "eauto with @{db}" t) - ("eauto" "ea" "eauto" t "eauto") - ("econstructor" "econs" "econstructor" t "econstructor") - ("eexists" "eex" "eexists" t "eexists") - ("eleft" "eleft" "eleft" t "eleft") - ("elim using" "elu" "elim # using #" t) - ("elim" "e" "elim #" t "elim") - ("elimtype" "elt" "elimtype" "elimtype") - ("eright" "erig" "eright" "eright") - ("esplit" "esp" "esplit" t "esplit") - ;; ("exact" "exa" "exact" t "exact") - ("exists" "ex" "exists #" t "exists") - ;; ("fail" "fa" "fail" nil) - ;; ("field" "field" "field" t "field") - ("firstorder" "fsto" "firstorder" t "firstorder") - ("firstorder with" "fsto" "firstorder with #" t) - ("firstorder with using" "fsto" "firstorder # with #" t) - ("fold" "fold" "fold #" t "fold") - ;; ("fourier" "four" "fourier" t "fourier") - ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") - ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") - ("generalize" "g" "generalize #" t "generalize") - ("hnf" "hnf" "hnf" t "hnf") - ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id - ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals - ("induction" "ind" "induction #" t "induction") - ("induction using" "indu" "induction # using #" t) - ("injection" "inj" "injection #" t "injection") - ("instantiate" "inst" "instantiate" t "instantiate") - ("intro" "i" "intro" t "intro") - ("intro after" "ia" "intro # after #" t) - ("intros" "is" "intros #" t "intros") - ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) - ("intros until" "isu" "intros until #" t) - ("intuition" "intu" "intuition #" t "intuition") - ("inversion" "inv" "inversion #" t "inversion") - ("inversion in" "invi" "inversion # in #" t) - ("inversion using" "invu" "inversion # using #" t) - ("inversion using in" "invui" "inversion # using # in #" t) - ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") - ("lapply" "lap" "lapply" t "lapply") - ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") - ("left" "left" "left" t "left") - ("linear" "lin" "linear" t "linear") - ("load" "load" "load" t "load") - ("move after" "mov" "move # after #" t "move") - ("omega" "o" "omega" t "omega") - ("pattern" "pat" "pattern" t "pattern") - ("pattern(s)" "pats" "pattern # , #" t) - ("pattern at" "pata" "pattern # at #" t) - ("pose" "po" "pose ( # := # )" t "pose") - ("prolog" "prol" "prolog" t "prolog") - ("quote" "quote" "quote" t "quote") - ("quote []" "quote2" "quote # [#]" t) - ("red" "red" "red" t "red") - ("refine" "ref" "refine" t "refine") - ;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("rename into" "ren" "rename # into #" t "rename") - ("replace with" "rep" "replace # with #" t "replace") - ("replace with in" "repi" "replace # with # in #" t) - ("rewrite <- in" "ri<" "rewrite <- # in #" t) - ("rewrite <-" "r<" "rewrite <- #" t) - ("rewrite in" "ri" "rewrite # in #" t) - ("rewrite" "r" "rewrite #" t "rewrite") - ("right" "rig" "right" t "right") - ;; ("ring" "ring" "ring #" t "ring") - ("set in * |-" "seth" "set ( # := #) in * |-" t) - ("set in *" "set*" "set ( # := #) in *" t) - ("set in |- *" "setg" "set ( # := #) in |- *" t) - ("set in" "seti" "set ( # := #) in #" t) - ("set" "set" "set ( # := #)" t "set") - ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") - ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") - ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") - ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") - ("simpl" "s" "simpl" t "simpl") - ("simpl" "sa" "simpl # at #" t) - ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") - ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") - ("simple induction" "sind" "simple induction" t "simple\\s-+induction") - ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") - ("specialize" "spec" "specialize" t "specialize") - ("split" "sp" "split" t "split") - ("split_Rabs" "spra" "splitRabs" t "split_Rabs") - ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") - ("stepl" "stl" "stepl #" t "stepl") - ("stepl by" "stlb" "stepl # by #" t) - ("stepr" "str" "stepr #" t "stepr") - ("stepr by" "strb" "stepr # by #" t) - ("subst" "su" "subst #" t "subst") - ("symmetry" "sy" "symmetry" t "symmetry") - ("symmetry in" "syi" "symmetry in #" t) - ;; ("tauto" "ta" "tauto" t "tauto") - ("transitivity" "trans" "transitivity #" t "transitivity") - ("trivial" "t" "trivial" t "trivial") - ("trivial with" "tw" "trivial with @{db}" t) - ("unfold" "u" "unfold #" t "unfold") - ("unfold(s)" "us" "unfold # , #" t) - ("unfold in" "unfi" "unfold # in #" t) - ("unfold at" "unfa" "unfold # at #" t) - )) - "Coq tactics information list. See `coq-syntax-db' for syntax. " - ) - -(defvar coq-solve-tactics-db - (append - coq-user-solve-tactics-db - '( - ("assumption" "as" "assumption" t "assumption") - ("by" "by" "by #" t "by") - ("congruence" "cong" "congruence" t "congruence") - ("contradiction" "contr" "contradiction" t "contradiction") - ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("discriminate" "dis" "discriminate" t "discriminate") - ("exact" "exa" "exact" t "exact") - ("fourier" "four" "fourier" t "fourier") - ("fail" "fa" "fail" nil) - ("field" "field" "field" t "field") - ("omega" "o" "omega" t "omega") - ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("ring" "ring" "ring #" t "ring") - ("solve" nil "solve [ # | # ]" nil "solve") - ("tauto" "ta" "tauto" t "tauto") - )) - "Coq tactic(al)s that solve a subgoal." - ) - - -(defvar coq-tacticals-db - (append - coq-user-tacticals-db - '( - ("info" nil "info #" nil "info") - ("first" nil "first [ # | # ]" nil "first") - ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") - ("do" nil "do @{num} @{tac}" nil "do") - ("idtac" nil "idtac") ; also in tactics - ; ("idtac \"" nil "idtac \"#\"") ; also in tactics - ("fail" "fa" "fail" nil "fail") - ; ("fail \"" "fa\"" "fail" nil) ; - ; ("orelse" nil "orelse #" t "orelse") - ("repeat" nil "repeat #" nil "repeat") - ("try" nil "try #" nil "try") - ("progress" nil "progress #" nil "progress") - ("|" nil "[ # | # ]" nil) - ("||" nil "# || #" nil) - )) - "Coq tacticals information list. See `coq-syntax-db' for syntax.") - - - - -(defvar coq-decl-db - '( - ("Axiom" "ax" "Axiom # : #" t "Axiom") - ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") - ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") - ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") - ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") - ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") - ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) - ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") - ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") - ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") - ("Parameter" "par" "Parameter #: #" t "Parameter") - ("Parameters" "par" "Parameter #: #" t "Parameters") - ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") - ("Variable" "v" "Variable #: #." t "Variable") - ("Variables" "vs" "Variables # , #: #." t "Variables") - ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") - ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." - ) - -(defvar coq-defn-db - '( - ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") - ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") - ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") - ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful - ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) - ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful - ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) - ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful - ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) - ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) - ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? - ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) - ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) - ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") - ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") - ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) - ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") - ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") - ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) - ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) - ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") - ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) - ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) - ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) - ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") - ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") - ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) - ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Variant" "indv" "Variant # : # := # : #." t "Variant") - ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t ) - ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Let" "Let" "Let # : # := #." t "Let") - ("Ltac" "ltac" "Ltac # := #" t "Ltac") - ("Module :=" "mo" "Module # : # := #." t ) ; careful - ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful - ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful - ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful - ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful - ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful - ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") - ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") - ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) - ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) - ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") - ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; modules and section are indented like goal starters -(defvar coq-goal-starters-db - '( - ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") - ("Chapter" "chp" "Chapter # : #." t "Chapter") - ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") - ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) - ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful - ("Fact" "fct" "Fact # : #." t "Fact") - ("Goal" nil "Goal #." t "Goal") - ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") - ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) - ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful - ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful - ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful - ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") - ("Section" "sec" "Section #." t "Section") - ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") - ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") - ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") - ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") - ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; command that are not declarations, definition or goal starters -(defvar coq-other-commands-db - '( - ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu - ("About" nil "About #." nil "About") - ("Add" nil "Add #." nil "Add" nil t) - ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") - ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") - ("Add Field" nil "Add Field #." t "Add\\s-+Field") - ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") - ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") - ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") - ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") - ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") - ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") - ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") - ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") - ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") - ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") - ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") - ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") - ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") - ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") - ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") - ("Cd" nil "Cd #." nil "Cd") - ("Check" nil "Check" nil "Check") - ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") - ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") - ("Comments" nil "Comments #." nil "Comments") - ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) - ("Eval" nil "Eval #." nil "Eval") - ("Export" nil "Export #." t "Export") - ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") - ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") - ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") - ("Extraction" "extr" "Extraction @{id}." nil "Extraction") - ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) - ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") - ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") - ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") - ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") - ("Focus" nil "Focus #." nil "Focus") - ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") - ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") - ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") - ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") - ("Import" nil "Import #." t "Import") - ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Inspect" nil "Inspect #." nil "Inspect") - ("Locate" nil "Locate" nil "Locate") - ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") - ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") - ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) - ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) - ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) - ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) - ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) - ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) - ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") - ("Notation (simple)" "nots" "Notation # := #." t "Notation") - ("Opaque" nil "Opaque #." nil "Opaque") - ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") - ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") - ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") - ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") - ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) - ("Print" "p" "Print #." nil "Print") - ("Qed" nil "Qed." nil "Qed") - ("Pwd" nil "Pwd." nil "Pwd") - ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") - ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") - ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") - ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") - ("Require Export" nil "Require Export #." t "Require\\s-+Export") - ("Require Import" nil "Require Import #." t "Require\\s-+Import") - ("Require" nil "Require #." t "Require") - ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") - ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") - ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") - ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") - ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") - ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") - ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") - ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") - ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") - ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") - ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") - ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") - ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") - ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Show" nil "Show #." nil "Show") - ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") - ("Transparent" nil "Transparent #." nil "Transparent") - ("Unfocus" nil "Unfocus." nil "Unfocus") - ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") - ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") - ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") - ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") - ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") - ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") - ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") - ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") - ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") - ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") - ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") - ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") - ; ("print" "pr" "print #" "print") - ) - "Command that are not declarations, definition or goal starters." - ) - -(defvar coq-commands-db - (append coq-decl-db coq-defn-db coq-goal-starters-db - coq-other-commands-db coq-user-commands-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " - ) - - -(defvar coq-terms-db - '( - ("fun (1 args)" "f" "fun #:# => #" nil "fun") - ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") - ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") - ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") - ("forall" "fo" "forall #:#,#" nil "forall") - ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") - ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") - ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") - ("if" "if" "if # then # else #" nil "if") - ("let in" "li" "let # := # in #" nil "let") - ("match! (from type)" nil "" nil "match" coq-insert-match) - ("match with" "m" "match # with\n| # => #\nend") - ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") - ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") - ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " - ) - - - - - - - - ;;; Goals (and module/sections) starters detection - - -;; ----- keywords for font-lock. - -;; FIXME da: this one function breaks the nice configuration of Proof General: -;; would like to have proof-goal-regexp instead. -;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, -;; so it appears more difficult than just a proof-goal-regexp setting. -;; Future improvement may simply to be allow a function value for -;; proof-goal-regexp. - -;; FIXME Pierre: the right way IMHO here would be to set a span -;; property 'goalcommand when coq prompt says it (if the name of -;; current proof has changed). - -;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry -;; for the french: -;;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de -;; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) -;; -;; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable -;; uniquement hors d'un MT -;; - si :=MEXPR est absent, elle demarre un nouveau module interactif -;; - si :=MEXPR est present, elle definit un module -;; (la fonction vernac_define_module dans toplevel/vernacentries) -;; -;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] -;; est valable uniquement dans un MT -;; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module -;; interactif -;; - si (:=MEXPR absent, :MTYP present) -;; ou (:=MEXPR present, :MTYP absent) -;; elle declare un module. -;; (la fonction vernac_declare_module dans toplevel/vernacentries) - -(defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring - of STRG matching REGEXP. Empty match are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) - (incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) - nbmatch)) - -;; This function is used for amalgamating a proof into a single -;; goal-save region (proof-goal-command-p used in -;; proof-done-advancing-save in generic/proof-script.el) for coq < -;; 8.0. It is the test when looking backward the start of the proof. -;; It is NOT used for coq > v8.1 -;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and -;; lemma names given in the prompt) - -;; compatibility with v8.0, will delete it some day -(defun coq-goal-command-str-v80-p (str) - "See `coq-goal-command-p'." - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - - (and (proof-string-match coq-goal-command-regexp str) - (not ; - (and - (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) - (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) - ) - ) - ) - -;; Module and or section openings are detected syntactically. Module -;; *openings* are difficult to detect because there can be Module -;; ...with X := ... . So we need to count :='s to detect real openings. - -;; TODO: have opened section/chapter in the prompt too, and get rid of -;; syntactical tests everywhere -(defun coq-module-opening-p (str) - "Decide whether STR is a module or section opening or not. -Used by `coq-goal-command-p'" - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match "\\`\\(Module\\)\\>" str) - (= letwith affect)) - )) - -(defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - - -(defun coq-goal-command-str-v81-p (str) - "Decide syntactically whether STR is a goal start or not. Use - `coq-goal-command-p-v81' on a span instead if possible." - (coq-goal-command-str-v80-p str) - ) - -;; This is the function that tests if a SPAN is a goal start. All it -;; has to do is look at the 'goalcmd attribute of the span. -;; It also looks if this is not a module start. - -;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs -;; something in the coq prompt telling the name of all opened modules -;; (like for open goals), and use it to set goalcmd --> no more need -;; to look at Modules and section (actually indentation will still -;; need it) -(defun coq-goal-command-p-v81 (span) - "see `coq-goal-command-p'" - (or (span-property span 'goalcmd) - ;; module and section starts are detected here - (let ((str (or (span-property span 'cmd) ""))) - (or (coq-section-command-p str) - (coq-module-opening-p str)) - ))) - -;; In coq > 8.1 This is used only for indentation. -(defun coq-goal-command-str-p (str) - "Decide whether argument is a goal or not. Use - `coq-goal-command-p' on a span instead if posible." - (cond - (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) - (t (coq-goal-command-str-v80-p str));; this is temporary - )) - -;; This is used for backtracking -(defun coq-goal-command-p (span) - "Decide whether argument is a goal or not." - (cond - (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) - (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary - )) - -(defvar coq-keywords-save-strict - '("Defined" - "Qed" - "End" - "Admitted" - "Abort" - )) - -(defvar coq-keywords-save - (append coq-keywords-save-strict '("Proof")) - ) - -(defun coq-save-command-p (span str) - "Decide whether argument is a Save command or not" - (or (proof-string-match coq-save-command-regexp-strict str) - (and (proof-string-match "\\`Proof\\>" str) - (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) - ) - ) - - -(defvar coq-keywords-kill-goal - '("Abort")) - -;; Following regexps are all state changing -(defvar coq-keywords-state-changing-misc-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) - -(defvar coq-keywords-goal - (coq-build-regexp-list-from-db coq-goal-starters-db)) - -(defvar coq-keywords-decl - (coq-build-regexp-list-from-db coq-decl-db)) - -(defvar coq-keywords-defn - (coq-build-regexp-list-from-db coq-defn-db)) - - -(defvar coq-keywords-state-changing-commands - (append - coq-keywords-state-changing-misc-commands - coq-keywords-decl ; all state changing - coq-keywords-defn ; idem - coq-keywords-goal)) ; idem - - -;; -(defvar coq-keywords-state-preserving-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) - -;; concat this is faster that redoing coq-build-regexp-list-from-db on -;; whole commands-db -(defvar coq-keywords-commands - (append coq-keywords-state-changing-commands - coq-keywords-state-preserving-commands) - "All commands keyword.") - -(defvar coq-solve-tactics - (coq-build-regexp-list-from-db coq-solve-tactics-db) - "Keywords for closing tactic(al)s.") - -(defvar coq-tacticals - (coq-build-regexp-list-from-db coq-tacticals-db) - "Keywords for tacticals in a Coq script.") - - - ;; From JF Monin: -(defvar coq-reserved - (append - coq-user-reserved-db - '( - "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" - "return" "struct" "else" "end" "if" "in" "into" "let" "then" - "using" "with" "beta" "delta" "iota" "zeta" "after" "until" - "at" "Sort" "Time")) - "Reserved keywords of Coq.") - - -(defvar coq-state-changing-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) - -(defvar coq-state-preserving-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) - - -(defvar coq-tactics - (append coq-state-changing-tactics coq-state-preserving-tactics)) - -(defvar coq-retractable-instruct - (append coq-state-changing-tactics coq-keywords-state-changing-commands)) - -(defvar coq-non-retractable-instruct - (append coq-state-preserving-tactics - coq-keywords-state-preserving-commands)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands) - "All keywords in a Coq script.") - - - -(defvar coq-symbols - '("|" - "||" - ":" - ";" - "," - "(" - ")" - "[" - "]" - "{" - "}" - ":=" - "=>" - "->" - ".") - "Punctuation Symbols used by Coq.") - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" - "A regexp indicating that the Coq process has identified an error.") - -(defvar coq-id proof-id) -(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") - -(defvar coq-ids (proof-ids coq-id " ")) - -(defun coq-first-abstr-regexp (paren end) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) - -(defcustom coq-variable-highlight-enable t - "Activates partial bound variable highlighting" - :type 'boolean - :group 'coq) - - -(defvar coq-font-lock-terms - (if coq-variable-highlight-enable - (list - ;; lambda binders - (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - ; (list "\\<forall\\>" - ; (list 0 font-lock-type-face) - ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil - ; (list 0 font-lock-variable-name-face))) - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - )) - "*Font-lock table for Coq terms.") - - - -;; According to Coq, "Definition" is both a declaration and a goal. -;; It is understood here as being a goal. This is important for -;; recognizing global identifiers, see coq-global-p. -(defconst coq-save-command-regexp-strict - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) -(defconst coq-save-command-regexp - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) - "\\)"))) -(defconst coq-save-with-hole-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) - -(defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) - -(defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) - "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) - -(defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) - "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) - -;; (defconst coq-decl-with-hole-regexp -;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) - -(defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)")) - -;; must match: -;; "with f x y :" (followed by = or not) -;; "with f x y (z:" (not followed by =) -;; BUT NOT: -;; "with f ... (x:=" -;; "match ... with .. => " -(defconst coq-with-with-hole-regexp - (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" - coq-id "\\s-*:[^=]\\)")) -;; marche aussi a peu pres -;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) -;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -(defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) - (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) - (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) - (cons "============================" 'font-lock-keyword-face) - (cons "Subtree proved!" 'font-lock-keyword-face) - (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) - (list "^\\([^ \n]+\\) \\(is defined\\)" - (list 2 'font-lock-keyword-face t) - (list 1 'font-lock-function-name-face t)) - - (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) - (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) - (list - (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) - ;; Remove spurious variable and function faces on commas. - '(proof-zap-commas)))) - -(defvar coq-font-lock-keywords coq-font-lock-keywords-1) - -(defun coq-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?\$ ".") - (modify-syntax-entry ?\/ ".") - (modify-syntax-entry ?\\ ".") - (modify-syntax-entry ?+ ".") - (modify-syntax-entry ?- ".") - (modify-syntax-entry ?= ".") - (modify-syntax-entry ?% ".") - (modify-syntax-entry ?< ".") - (modify-syntax-entry ?> ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - -;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug - (modify-syntax-entry ?\. ".") - - (condition-case nil - ;; Try to use Emacs-21's nested comments. - (modify-syntax-entry ?\* ". 23n") - ;; Revert to non-nested comments if that failed. - (error (modify-syntax-entry ?\* ". 23"))) - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - - -(defconst coq-generic-expression - (mapcar (lambda (kw) - (list (capitalize kw) - (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) - 1)) - (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) - -(provide 'gallina-syntax) - ;;; gallina-syntax.el ends here - -; Local Variables: *** -; indent-tabs-mode: nil *** -; End: *** diff --git a/tools/gallina.el b/tools/gallina.el deleted file mode 100644 index cbc13118a..000000000 --- a/tools/gallina.el +++ /dev/null @@ -1,142 +0,0 @@ -;; gallina.el --- Coq mode editing commands for Emacs -;; -;; Jean-Christophe Filliatre, march 1995 -;; Shamelessly copied from caml.el, Xavier Leroy, july 1993. -;; -;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior - -; compatibility code for proofgeneral files -(require 'coq-font-lock) -; ProofGeneral files. remember to remove coq version tests in -; gallina-syntax.el -(require 'gallina-syntax) - -(defvar coq-mode-map nil - "Keymap used in Coq mode.") -(if coq-mode-map - () - (setq coq-mode-map (make-sparse-keymap)) - (define-key coq-mode-map "\t" 'coq-indent-command) - (define-key coq-mode-map "\M-\t" 'coq-unindent-command) - (define-key coq-mode-map "\C-c\C-c" 'compile) -) - -(defvar coq-mode-syntax-table nil - "Syntax table in use in Coq mode buffers.") -(if coq-mode-syntax-table - () - (setq coq-mode-syntax-table (make-syntax-table)) - ; ( is first character of comment start - (modify-syntax-entry ?\( "()1" coq-mode-syntax-table) - ; * is second character of comment start, - ; and first character of comment end - (modify-syntax-entry ?* ". 23" coq-mode-syntax-table) - ; ) is last character of comment end - (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table) - ; quote is a string-like delimiter (for character literals) - (modify-syntax-entry ?' "\"" coq-mode-syntax-table) - ; quote is part of words - (modify-syntax-entry ?' "w" coq-mode-syntax-table) -) - -(defvar coq-mode-indentation 2 - "*Indentation for each extra tab in Coq mode.") - -(defun coq-mode-variables () - (set-syntax-table coq-mode-syntax-table) - (make-local-variable 'paragraph-start) - (setq paragraph-start (concat "^$\\|" page-delimiter)) - (make-local-variable 'paragraph-separate) - (setq paragraph-separate paragraph-start) - (make-local-variable 'paragraph-ignore-fill-prefix) - (setq paragraph-ignore-fill-prefix t) - (make-local-variable 'require-final-newline) - (setq require-final-newline t) - (make-local-variable 'comment-start) - (setq comment-start "(* ") - (make-local-variable 'comment-end) - (setq comment-end " *)") - (make-local-variable 'comment-column) - (setq comment-column 40) - (make-local-variable 'comment-start-skip) - (setq comment-start-skip "(\\*+ *") - (make-local-variable 'parse-sexp-ignore-comments) - (setq parse-sexp-ignore-comments nil) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'coq-indent-command) - (make-local-variable 'font-lock-keywords) - (setq font-lock-defaults '(coq-font-lock-keywords-1))) - -;;; The major mode - -(defun coq-mode () - "Major mode for editing Coq code. -Tab at the beginning of a line indents this line like the line above. -Extra tabs increase the indentation level. -\\{coq-mode-map} -The variable coq-mode-indentation indicates how many spaces are -inserted for each indentation level." - (interactive) - (kill-all-local-variables) - (setq major-mode 'coq-mode) - (setq mode-name "coq") - (use-local-map coq-mode-map) - (coq-mode-variables) - (run-hooks 'coq-mode-hook)) - -;;; Indentation stuff - -(defun coq-in-indentation () - "Tests whether all characters between beginning of line and point -are blanks." - (save-excursion - (skip-chars-backward " \t") - (bolp))) - -(defun coq-indent-command () - "Indent the current line in Coq mode. -When the point is at the beginning of an empty line, indent this line like -the line above. -When the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\), -increase the indentation by one level. -The indentation size is given by the variable coq-mode-indentation. -In all other cases, insert a tabulation (using insert-tab)." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline)) - (previous-indentation - (save-excursion - (if (eq (forward-line -1) 0) (current-indentation) 0)))) - (cond ((and (bolp) - (looking-at "[ \t]*$") - (> previous-indentation 0)) - (indent-to previous-indentation)) - ((coq-in-indentation) - (indent-to (+ current-offset coq-mode-indentation))) - (t - (insert-tab))))) - -(defun coq-unindent-command () - "Decrease indentation by one level in Coq mode. -Works only if the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\). -Does nothing otherwise." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline))) - (if (and (>= current-offset coq-mode-indentation) - (coq-in-indentation)) - (backward-delete-char-untabify coq-mode-indentation)))) - -;;; gallina.el ends here - -(provide 'gallina) diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el deleted file mode 100644 index 453bd1391..000000000 --- a/tools/inferior-coq.el +++ /dev/null @@ -1,324 +0,0 @@ -;;; inferior-coq.el --- Run an inferior Coq process. -;;; -;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it> -;;; Time-stamp: "2002-02-28 12:15:04 maggesi" - - -;; Emacs Lisp Archive Entry -;; Filename: inferior-coq.el -;; Version: 1.0 -;; Keywords: process coq -;; Author: Marco Maggesi <maggesi@math.unifi.it> -;; Maintainer: Marco Maggesi <maggesi@math.unifi.it> -;; Description: Run an inferior Coq process. -;; URL: http://www.math.unifi.it/~maggesi/ -;; Compatibility: Emacs20, Emacs21, XEmacs21 - -;; This is free software; you can redistribute it and/or modify it under -;; the terms of the GNU General Public License as published by the Free -;; Software Foundation; either version 2, or (at your option) any later -;; version. -;; -;; This is distributed in the hope that it will be useful, but WITHOUT -;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or -;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -;; for more details. -;; -;; You should have received a copy of the GNU General Public License -;; along with GNU Emacs; see the file COPYING. If not, write to the -;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, -;; MA 02111-1307, USA. - -;;; Commentary: - -;; Coq is a proof assistant (http://coq.inria.fr/). This code run an -;; inferior Coq process and defines functions to send bits of code -;; from other buffers to the inferior process. This is a -;; customisation of comint-mode (see comint.el). For a more complex -;; and full featured Coq interface under Emacs look at Proof General -;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). -;; -;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly -;; borrowed from emacs cmuscheme.el -;; -;; Please send me bug reports, bug fixes, and extensions, so that I can -;; merge them into the master source. - -;;; Installation: - -;; You need to have gallina.el already installed (it comes with the -;; standard Coq distribution) in order to use this code. Put this -;; file somewhere in you load-path and add the following lines in your -;; "~/.emacs": -;; -;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) -;; (autoload 'run-coq-other-window "inferior-coq" -;; "Run an inferior Coq process in a new window." t) -;; (autoload 'run-coq-other-frame "inferior-coq" -;; "Run an inferior Coq process in a new frame." t) - -;;; Usage: - -;; Call `M-x "run-coq'. -;; -;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): -;; C-return ('M-x coq-send-line) send the current line. -;; C-c C-r (`M-x coq-send-region') send the current region. -;; C-c C-a (`M-x coq-send-abort') send the command "Abort". -;; C-c C-t (`M-x coq-send-restart') send the command "Restart". -;; C-c C-s (`M-x coq-send-show') send the command "Show". -;; C-c C-u (`M-x coq-send-undo') send the command "Undo". -;; C-c C-v (`M-x coq-check-region') run command "Check" on region. -;; C-c . (`M-x coq-come-here') Restart and send until current point. - -;;; Change Log: - -;; From -0.0 to 1.0 brought into existence. - - -(require 'gallina) -(require 'comint) - -(setq coq-program-name "coqtop") - -(defgroup inferior-coq nil - "Run a coq process in a buffer." - :group 'coq) - -(defcustom inferior-coq-mode-hook nil - "*Hook for customising inferior-coq mode." - :type 'hook - :group 'coq) - -(defvar inferior-coq-mode-map - (let ((m (make-sparse-keymap))) - (define-key m "\C-c\C-r" 'coq-send-region) - (define-key m "\C-c\C-a" 'coq-send-abort) - (define-key m "\C-c\C-t" 'coq-send-restart) - (define-key m "\C-c\C-s" 'coq-send-show) - (define-key m "\C-c\C-u" 'coq-send-undo) - (define-key m "\C-c\C-v" 'coq-check-region) - m)) - -;; Install the process communication commands in the coq-mode keymap. -(define-key coq-mode-map [(control return)] 'coq-send-line) -(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) -(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) -(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) -(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) -(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) -(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) -(define-key coq-mode-map "\C-c." 'coq-come-here) - -(defvar coq-buffer) - -(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" - "\ -Major mode for interacting with an inferior Coq process. - -The following commands are available: -\\{inferior-coq-mode-map} - -A Coq process can be fired up with M-x run-coq. - -Customisation: Entry to this mode runs the hooks on comint-mode-hook -and inferior-coq-mode-hook (in that order). - -You can send text to the inferior Coq process from other buffers -containing Coq source. - -Functions and key bindings (Learn more keys with `C-c C-h'): - C-return ('M-x coq-send-line) send the current line. - C-c C-r (`M-x coq-send-region') send the current region. - C-c C-a (`M-x coq-send-abort') send the command \"Abort\". - C-c C-t (`M-x coq-send-restart') send the command \"Restart\". - C-c C-s (`M-x coq-send-show') send the command \"Show\". - C-c C-u (`M-x coq-send-undo') send the command \"Undo\". - C-c C-v (`M-x coq-check-region') run command \"Check\" on region. - C-c . (`M-x coq-come-here') Restart and send until current point. -" - ;; Customise in inferior-coq-mode-hook - (setq comint-prompt-regexp "^[^<]* < *") - (coq-mode-variables) - (setq mode-line-process '(":%s")) - (setq comint-input-filter (function coq-input-filter)) - (setq comint-get-old-input (function coq-get-old-input))) - -(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" - "*Input matching this regexp are not saved on the history list. -Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." - :type 'regexp - :group 'inferior-coq) - -(defun coq-input-filter (str) - "Don't save anything matching `inferior-coq-filter-regexp'." - (not (string-match inferior-coq-filter-regexp str))) - -(defun coq-get-old-input () - "Snarf the sexp ending at point." - (save-excursion - (let ((end (point))) - (backward-sexp) - (buffer-substring (point) end)))) - -(defun coq-args-to-list (string) - (let ((where (string-match "[ \t]" string))) - (cond ((null where) (list string)) - ((not (= where 0)) - (cons (substring string 0 where) - (coq-args-to-list (substring string (+ 1 where) - (length string))))) - (t (let ((pos (string-match "[^ \t]" string))) - (if (null pos) - nil - (coq-args-to-list (substring string pos - (length string))))))))) - -;;;###autoload -(defun run-coq (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -;;;###autoload -(defun run-coq-other-window (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (pop-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -(defun run-coq-other-frame (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer-other-frame "*coq*")) - -(defun switch-to-coq (eob-p) - "Switch to the coq process buffer. -With argument, position cursor at end of buffer." - (interactive "P") - (if (get-buffer coq-buffer) - (pop-to-buffer coq-buffer) - (error "No current process buffer. See variable `coq-buffer'")) - (cond (eob-p - (push-mark) - (goto-char (point-max))))) - -(defun coq-send-region (start end) - "Send the current region to the inferior Coq process." - (interactive "r") - (comint-send-region (coq-proc) start end) - (comint-send-string (coq-proc) "\n")) - -(defun coq-send-line () - "Send the current line to the Coq process." - (interactive) - (save-excursion - (end-of-line) - (let ((end (point))) - (beginning-of-line) - (coq-send-region (point) end))) - (forward-line 1)) - -(defun coq-send-abort () - "Send the command \"Abort.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Abort.\n")) - -(defun coq-send-restart () - "Send the command \"Restart.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Restart.\n")) - -(defun coq-send-undo () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Undo.\n")) - -(defun coq-check-region (start end) - "Run the commmand \"Check\" on the current region." - (interactive "r") - (comint-proc-query (coq-proc) - (concat "Check " - (buffer-substring start end) - ".\n"))) - -(defun coq-send-show () - "Send the command \"Show.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Show.\n")) - -(defun coq-come-here () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Reset Initial.\n") - (coq-send-region 1 (point))) - -(defvar coq-buffer nil "*The current coq process buffer.") - -(defun coq-proc () - "Return the current coq process. See variable `coq-buffer'." - (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) - (current-buffer) - coq-buffer)))) - (or proc - (error "No current process. See variable `coq-buffer'")))) - -(defcustom inferior-coq-load-hook nil - "This hook is run when inferior-coq is loaded in. -This is a good place to put keybindings." - :type 'hook - :group 'inferior-coq) - -(run-hooks 'inferior-coq-load-hook) - -(provide 'inferior-coq) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d7ede1c2e..7ae15ac10 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf)); + ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -228,7 +228,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Pcoq.Gram.parsable (Stream.of_list []); + tokens = Pcoq.Parsable.make (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -253,7 +253,7 @@ let parse_to_dot = let rec discard_to_dot () = try - Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | Stm.End_of_input -> raise Stm.End_of_input diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 5c07a8bf3..b11f13d3c 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -18,7 +18,7 @@ type input_buffer = { mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 53d3eef23..5aba3d6b0 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -21,9 +21,9 @@ type vernac_toplevel = | VernacControl of vernac_control module Toplevel_ : sig - val vernac_toplevel : vernac_toplevel CAst.t Gram.entry + val vernac_toplevel : vernac_toplevel CAst.t Entry.t end = struct - let gec_vernac s = Gram.entry_create ("toplevel:" ^ s) + let gec_vernac s = Entry.create ("toplevel:" ^ s) let vernac_toplevel = gec_vernac "vernac_toplevel" end @@ -49,6 +49,6 @@ END { -let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa +let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa } diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c1bbb20d5..c914bbecf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -121,7 +121,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let in_echo = if echo then Some (open_utf8_file_in file) else None in let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in - let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in + let in_pa = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let rstate = ref state in (* For beautify, list of parsed sids *) let rids = ref [] in @@ -159,12 +159,12 @@ let load_vernac_core ~echo ~check ~interactive ~state file = rstate := state; done; input_cleanup (); - !rstate, !rids, Pcoq.Gram.comment_state in_pa + !rstate, !rids, Pcoq.Parsable.comment_state in_pa with any -> (* whatever the exception *) let (e, info) = CErrors.push any in input_cleanup (); match e with - | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa + | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa | reraise -> iraise (e, info) let process_expr ~state loc_ast = diff --git a/vernac/class.ml b/vernac/class.ml index 133726702..e425e6474 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -303,12 +303,12 @@ let try_add_new_coercion_with_source ref ~local poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false let add_coercion_hook poly local ref = - let stre = match local with + let local = match local with + | Discharge | Local -> true | Global -> false - | Discharge -> assert false in - let () = try_add_new_coercion ref ~local:stre poly in + let () = try_add_new_coercion ref ~local poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 48f225f97..3281b75aa 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -240,14 +240,14 @@ type (_, _) entry = type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry (* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = +let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option = fun forpat level -> match forpat with | ForConstr -> if level = 200 then Constr.binder_constr, None else Constr.operconstr, Some level | ForPattern -> Constr.pattern, Some level -let target_entry : type s. s target -> s Gram.entry = function +let target_entry : type s. s target -> s Entry.t = function | ForConstr -> Constr.operconstr | ForPattern -> Constr.pattern diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 31aa1a989..a5ee036db 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -21,7 +21,7 @@ type 's grammar_prod_item = ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> + Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option -> vernac_expr grammar_prod_item list -> unit val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index cccdbfc91..dacef6e21 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -22,7 +22,7 @@ open Pvernac.Vernac_ let thm_token = G_vernac.thm_token -let hint = Gram.entry_create "hint" +let hint = Entry.create "hint" let warn_deprecated_focus = CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3a01ce6df..a35a1998d 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -37,18 +37,18 @@ let _ = List.iter CLexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -let query_command = Gram.entry_create "vernac:query_command" +let query_command = Entry.create "vernac:query_command" -let subprf = Gram.entry_create "vernac:subprf" +let subprf = Entry.create "vernac:subprf" -let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" -let thm_token = Gram.entry_create "vernac:thm_token" -let def_body = Gram.entry_create "vernac:def_body" -let decl_notation = Gram.entry_create "vernac:decl_notation" -let record_field = Gram.entry_create "vernac:record_field" -let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" -let instance_name = Gram.entry_create "vernac:instance_name" -let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" +let class_rawexpr = Entry.create "vernac:class_rawexpr" +let thm_token = Entry.create "vernac:thm_token" +let def_body = Entry.create "vernac:def_body" +let decl_notation = Entry.create "vernac:decl_notation" +let record_field = Entry.create "vernac:record_field" +let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" +let instance_name = Entry.create "vernac:instance_name" +let section_subset_expr = Entry.create "vernac:section_subset_expr" let make_bullet s = let open Proof_bullet in @@ -79,27 +79,50 @@ GRAMMAR EXTEND Gram | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) } | IDENT "Timeout"; n = natural; v = vernac_control -> { VernacTimeout(n,v) } | IDENT "Fail"; v = vernac_control -> { VernacFail v } - | v = vernac -> { let (f, v) = v in VernacExpr(f, v) } ] + | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ] + ] + ; + decorated_vernac: + [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) } + | fv = vernac -> { fv } ] + ] + ; + attributes: + [ [ "#[" ; a = attribute_list ; "]" -> { a } ] + ] + ; + attribute_list: + [ [ a = LIST0 attribute SEP "," -> { a } ] + ] + ; + attribute: + [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ] + ] + ; + attribute_value: + [ [ "=" ; v = string -> { VernacFlagLeaf v } + | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } + | -> { VernacFlagEmpty } ] ] ; vernac: - [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) } - | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) } + [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) } + | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) } | v = vernac_poly -> { v } ] ] ; vernac_poly: - [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic true :: f, v) } - | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic false :: f, v) } + [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (("polymorphic", VernacFlagEmpty) :: f, v) } + | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (("monomorphic", VernacFlagEmpty) :: f, v) } | v = vernac_aux -> { v } ] ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> { ([VernacProgram], g) } - | IDENT "Program"; g = gallina_ext; "." -> { ([VernacProgram], g) } + [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) } + | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) } | g = gallina; "." -> { ([], g) } | g = gallina_ext; "." -> { ([], g) } | c = command; "." -> { ([], c) } diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 240147c8d..33e6229b2 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -49,7 +49,7 @@ let entry_buf = Buffer.create 64 let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in - let () = Pcoq.Gram.entry_print ft e in + let () = Pcoq.Entry.print ft e in str (Buffer.contents entry_buf) let pr_registered_grammar name = diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 5fbe1f4e4..e5547d9b7 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -153,8 +153,6 @@ open Pputils | SearchAbout sl -> keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b - let pr_locality local = if local then keyword "Local" else keyword "Global" - let pr_option_ref_value = function | QualidRefValue id -> pr_qualid id | StringRefValue s -> qs s @@ -1195,21 +1193,24 @@ open Pputils | VernacEndSubproof -> return (str "}") -let pr_vernac_flag = +let rec pr_vernac_flag (k, v) = + let k = keyword k in + match v with + | VernacFlagEmpty -> k + | VernacFlagLeaf v -> k ++ str " = " ++ qs v + | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )" +and pr_vernac_flags m = + prlist_with_sep (fun () -> str ", ") pr_vernac_flag m + +let pr_vernac_attributes = function - | VernacPolymorphic true -> keyword "Polymorphic" - | VernacPolymorphic false -> keyword "Monomorphic" - | VernacProgram -> keyword "Program" - | VernacLocal local -> pr_locality local + | [] -> mt () + | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr (f, v') -> - List.fold_right - (fun f a -> pr_vernac_flag f ++ spc() ++ a) - f - (pr_vernac_expr v' ++ sep_end v') + | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v' | VernacTime (_,{v}) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, {v}) -> diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index f8b085f3e..74e53bef1 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -178,7 +178,7 @@ let suggest_variable env id = let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us))) +let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) let _ = Goptions.declare_stringopt_option diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index bac882381..b2fa8ec99 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -10,13 +10,11 @@ open Pcoq -let uncurry f (x,y) = f x y - let uvernac = create_universe "vernac" module Vernac_ = struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) + let gec_vernac s = Entry.create ("vernac:" ^ s) (* The different kinds of vernacular commands *) let gallina = gec_vernac "gallina" @@ -28,22 +26,23 @@ module Vernac_ = let red_expr = new_entry utactic "red_expr" let hint_info = gec_vernac "hint_info" (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" + let main_entry = Entry.create "vernac" let noedit_mode = gec_vernac "noedit_command" let () = - let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in + let open Extend in + let act_vernac v loc = Some (loc, v) in + let act_eoi _ loc = None in let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); + Rule (Next (Stop, Atoken Tok.EOI), act_eoi); + Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in - uncurry (Gram.extend main_entry) (None, [None, None, rule]) + Pcoq.grammar_extend main_entry None (None, [None, None, rule]) let command_entry_ref = ref noedit_mode let command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) + (fun strm -> Gram.Entry.parse_token !command_entry_ref strm) end diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 2993a1661..b2f8f7146 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -16,21 +16,21 @@ val uvernac : gram_universe module Vernac_ : sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Hints.hint_info_expr Gram.entry + val gallina : vernac_expr Entry.t + val gallina_ext : vernac_expr Entry.t + val command : vernac_expr Entry.t + val syntax : vernac_expr Entry.t + val vernac_control : vernac_control Entry.t + val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val noedit_mode : vernac_expr Entry.t + val command_entry : vernac_expr Entry.t + val red_expr : raw_red_expr Entry.t + val hint_info : Hints.hint_info_expr Entry.t end (** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Gram.entry +val main_entry : (Loc.t * vernac_control) option Entry.t (** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Gram.entry -val set_command_entry : vernac_expr Gram.entry -> unit +val get_command_entry : unit -> vernac_expr Entry.t +val set_command_entry : vernac_expr Entry.t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5fda1a0da..b6bc76a2e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2040,7 +2040,7 @@ let vernac_load interp fname = interp x in let parse_sentence = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Gram.entry_parse Pvernac.main_entry po with + match Pcoq.Entry.parse Pvernac.main_entry po with | Some x -> x | None -> raise End_of_input) in let fname = @@ -2049,7 +2049,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in + Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in begin try while true do interp (snd (parse_sentence input)) done with End_of_input -> () @@ -2319,32 +2319,62 @@ let with_fail st b f = | _ -> assert false end +let attributes_of_flags f atts = + let assert_empty k v = + if v <> VernacFlagEmpty + then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") + in + List.fold_left + (fun (polymorphism, atts) (k, v) -> + match k with + | "program" when not atts.program -> + assert_empty k v; + (polymorphism, { atts with program = true }) + | "program" -> + user_err Pp.(str "Program mode specified twice") + | "polymorphic" when polymorphism = None -> + assert_empty k v; + (Some true, atts) + | "monomorphic" when polymorphism = None -> + assert_empty k v; + (Some false, atts) + | ("polymorphic" | "monomorphic") -> + user_err Pp.(str "Polymorphism specified twice") + | "local" when Option.is_empty atts.locality -> + assert_empty k v; + (polymorphism, { atts with locality = Some true }) + | "global" when Option.is_empty atts.locality -> + assert_empty k v; + (polymorphism, { atts with locality = Some false }) + | ("local" | "global") -> + user_err Pp.(str "Locality specified twice") + | "deprecated" when Option.is_empty atts.deprecated -> + begin match v with + | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] + | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> + let since = Some since and note = Some note in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) }) + | VernacFlagList [ "since", VernacFlagLeaf since ] -> + let since = Some since in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) }) + | VernacFlagList [ "note", VernacFlagLeaf note ] -> + let note = Some note in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) }) + | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") + end + | "deprecated" -> + user_err Pp.(str "Deprecation specified twice") + | _ -> user_err Pp.(str "Unknown attribute " ++ str k) + ) + (None, atts) + f + let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in - let flags f atts = - List.fold_left - (fun (polymorphism, atts) f -> - match f with - | VernacProgram when not atts.program -> - (polymorphism, { atts with program = true }) - | VernacProgram -> - user_err Pp.(str "Program mode specified twice") - | VernacPolymorphic b when polymorphism = None -> - (Some b, atts) - | VernacPolymorphic _ -> - user_err Pp.(str "Polymorphism specified twice") - | VernacLocal b when Option.is_empty atts.locality -> - (polymorphism, { atts with locality = Some b }) - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") - ) - (None, atts) - f - in let rec control = function | VernacExpr (f, v) -> - let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 02a3b2bd6..79f9c05ad 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -38,3 +38,7 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr Evd.evar_map * Redexpr.red_expr) Hook.t val universe_polymorphism_option_name : string list + +(** Elaborate a [atts] record out of a list of flags. + Also returns whether polymorphism is explicitly (un)set. *) +val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f5f37339c..e97cac818 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -459,13 +459,14 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool +type vernac_flags = (string * vernac_flag_value) list +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr + | VernacExpr of vernac_flags * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) | VernacTime of bool * vernac_control CAst.t diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index d4f2a753f..1bb1414f3 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -12,15 +12,22 @@ open Util open Pp open CErrors -type deprecation = bool +type deprecation = { since : string option ; note : string option } + +let mk_deprecation ?(since=None) ?(note=None) () = + { since ; note } type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; program : bool; + deprecated : deprecation option; } +let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts = + { loc ; locality ; polymorphic ; program ; deprecated } + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list @@ -28,7 +35,7 @@ type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) let vinterp_add depr s f = try diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 935cacf77..46468b309 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -10,21 +10,27 @@ (** Interpretation of extended vernac phrases. *) -type deprecation = bool +type deprecation = { since : string option ; note : string option } + +val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; program : bool; + deprecated : deprecation option; } +val mk_atts : ?loc: Loc.t option -> ?locality: bool option -> + ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list val vinterp_init : unit -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit +val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t |