diff options
50 files changed, 526 insertions, 371 deletions
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) @@ -68,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/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/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/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 ad001012a..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 @@ -144,13 +145,14 @@ def make_diff_table_string(left_times_dict, right_times_dict, for name, lseconds, rseconds in prediff_times) # update to sort by approximate difference, first get_key_abs = make_sorting_key(all_names_dict, descending=descending) - get_key_diff = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + get_key_diff_float = (lambda name: fix_sign_for_sorting(to_seconds(diff_times_dict[name]), descending=descending)) + get_key_diff_absint = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) if sort_by == 'absolute': get_key = get_key_abs elif sort_by == 'diff': - get_key = get_key_diff + get_key = get_key_diff_float else: # sort_by == 'auto' - get_key = (lambda name: (get_key_diff(name), get_key_abs(name))) + get_key = (lambda name: (get_key_diff_absint(name), get_key_abs(name))) names = sorted(all_names_dict.keys(), key=get_key) #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) # set the widths of each of the columns by the longest thing to go in that column @@ -206,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/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 |