diff options
90 files changed, 903 insertions, 537 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 52b03e455b..a2d62fe43d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -806,6 +806,13 @@ library:ci-math_classes: library:ci-mathcomp: extends: .ci-template-flambda +library:ci-mczify: + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp + library:ci-sf: extends: .ci-template diff --git a/Makefile.build b/Makefile.build index 2b626506a3..d0948baf07 100644 --- a/Makefile.build +++ b/Makefile.build @@ -621,7 +621,6 @@ gramlib/.pack: # gramlib.ml contents gramlib/.pack/gramlib.ml: | gramlib/.pack echo " \ -module Ploc = Gramlib__Ploc \ module Plexing = Gramlib__Plexing \ module Gramext = Gramlib__Gramext \ module Grammar = Gramlib__Grammar" > $@ diff --git a/Makefile.ci b/Makefile.ci index f7c2943cc2..6eeb7581fe 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -44,6 +44,7 @@ CI_TARGETS= \ ci-iris \ ci-math_classes \ ci-mathcomp \ + ci-mczify \ ci-menhir \ ci-metacoq \ ci-mtac2 \ @@ -89,6 +90,7 @@ ci-interval: ci-mathcomp ci-flocq ci-coquelicot ci-bignums ci-fourcolor: ci-mathcomp ci-oddorder: ci-mathcomp ci-fcsl_pcm: ci-mathcomp +ci-mczify: ci-mathcomp ci-geocoq: ci-mathcomp diff --git a/Makefile.make b/Makefile.make index dc123820ee..c68a71a832 100644 --- a/Makefile.make +++ b/Makefile.make @@ -101,7 +101,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated # GRAMFILES must be in linking order -GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) +GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Plexing Gramext Grammar) GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 0093b5fca2..41ba182a4d 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -48,6 +48,8 @@ project fourcolor "https://github.com/math-comp/fourcolor" "master" project oddorder "https://github.com/math-comp/odd-order" "master" +project mczify "https://github.com/math-comp/mczify" "master" + ######################################################################## # UniMath ######################################################################## diff --git a/dev/ci/ci-mczify.sh b/dev/ci/ci-mczify.sh new file mode 100755 index 0000000000..2d98906c3e --- /dev/null +++ b/dev/ci/ci-mczify.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download mczify + +( cd "${CI_BUILD_DIR}/mczify" && make ) diff --git a/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh b/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh new file mode 100644 index 0000000000..29f2386797 --- /dev/null +++ b/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh @@ -0,0 +1,2 @@ +overlay equations https://github.com/Zimmi48/Coq-Equations coq-13911 13911 remove_type_cast +overlay elpi https://github.com/Zimmi48/coq-elpi patch-1 13911 remove_type_cast diff --git a/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh new file mode 100644 index 0000000000..decb093b71 --- /dev/null +++ b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh @@ -0,0 +1,3 @@ +overlay equations https://github.com/gares/Coq-Equations syndef-principal-scope 13965 +overlay elpi https://github.com/gares/coq-elpi syndef-principal-scope 13965 +overlay paramcoq https://github.com/gares/paramcoq syndef-principal-scope 13965 diff --git a/dev/ci/user-overlays/14075-herbelin-master+new-level-abstraction-streams-with-location.sh b/dev/ci/user-overlays/14075-herbelin-master+new-level-abstraction-streams-with-location.sh new file mode 100644 index 0000000000..a85ee6d2d0 --- /dev/null +++ b/dev/ci/user-overlays/14075-herbelin-master+new-level-abstraction-streams-with-location.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr14075-new-module-lstream-change-of_parser 14075 diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 26c4b01c9f..b61c7d3423 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,9 @@ +## Changes between Coq 8.13 and Coq 8.14 + +Gramlib + +- A few functions change their interfaces to take benefit of a new abstraction level `LStream` for streams with location function. + ## Changes between Coq 8.12 and Coq 8.13 ### Code formatting diff --git a/doc/changelog/02-specification-language/13911-master.rst b/doc/changelog/02-specification-language/13911-master.rst new file mode 100644 index 0000000000..a0b37dd2d9 --- /dev/null +++ b/doc/changelog/02-specification-language/13911-master.rst @@ -0,0 +1,4 @@ +- **Removed:** + The little used `:>` type cast, which was only interpreted in Program-mode + (`#13911 <https://github.com/coq/coq/pull/13911>`_, + by Jim Fehrle and Théo Zimmermann). diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst new file mode 100644 index 0000000000..448dbbe3c7 --- /dev/null +++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst @@ -0,0 +1,12 @@ +- **Added:** + Let the user specify a scope for abbreviation arguments, e.g. + ``Notation abbr X := t (X in scope my_scope)``. + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). +- **Changed:** + The error ``Argument X was previously inferred to be in scope + XXX_scope but is here used in YYY_scope.`` is now the warning + ``[inconsistent-scopes,syntax]`` and can be silenced by + specifying the scope of the argument + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). diff --git a/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst new file mode 100644 index 0000000000..41bc3329c1 --- /dev/null +++ b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Ltac2 notations now correctly take into account their assigned level + (`#14094 <https://github.com/coq/coq/pull/14094>`_, + fixes `#11866 <https://github.com/coq/coq/issues/11866>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst b/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst new file mode 100644 index 0000000000..17eb710344 --- /dev/null +++ b/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst @@ -0,0 +1,5 @@ +- **Changed:** + Renamed Ltac2 Bool.eq into Bool.equal for uniformity. + The old function is now a deprecated alias + (`#14128 <https://github.com/coq/coq/pull/14128>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/12-misc/14041-cs_lambda.rst b/doc/changelog/12-misc/14041-cs_lambda.rst new file mode 100644 index 0000000000..872b1f09eb --- /dev/null +++ b/doc/changelog/12-misc/14041-cs_lambda.rst @@ -0,0 +1,6 @@ +- **Added:** + Enable canonical `fun _ => _` projections, + see :ref:`canonicalstructures` for details. + (`#14041 <https://github.com/coq/coq/pull/14041>`_, + by Jan-Oliver Kaiser and Pierre Roux, + reviewed by Cyril Cohen and Enrico Tassi). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a011c81f15..52e47b52ae 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in: The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not produce an equality, contrary to the let pattern construct :g:`let '(x1,..., xn) := t in b`. -Also, :g:`term :>` explicitly asks the system to -coerce term to its support type. It can be useful in notations, for -example: - -.. coqtop:: all - - Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). - -This notation denotes equality on subset types using equality on their -support types, avoiding uses of proof-irrelevance that would come up -when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts :cmd:`Definition` and :cmd:`Fixpoint` diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index fcf61a5bf4..1a729ced4e 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -42,7 +42,6 @@ Type cast term_cast ::= @term10 : @type | @term10 <: @type | @term10 <<: @type - | @term10 :> The expression :n:`@term10 : @type` is a type cast expression. It enforces the type of :n:`@term10` to be :n:`@type`. @@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`). :n:`@term10 <<: @type` specifies that compilation to OCaml will be used to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`). -:n:`@term10 :>` casts to the support type in Program mode. -See :ref:`syntactic_control`. - .. _gallina-definitions: Top-level definitions diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index fbba6c30b8..e3b014d8d5 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -41,12 +41,54 @@ in :ref:`canonicalstructures`; here only a simple example is given. This command supports the :attr:`local` attribute. When used, the structure is canonical only within the :cmd:`Section` containing it. - Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the - structure :g:`struct` of which the fields are |x_1|, …, |x_n|. - Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be + :token:`qualid` (in :token:`reference`) denotes an object :n:`(Build_struct c__1 … c__n)` in the + structure :g:`struct` for which the fields are :n:`x__1, …, x__n`. + Then, each time an equation of the form :n:`(x__i _)` |eq_beta_delta_iota_zeta| :n:`c__i` has to be solved during the type checking process, :token:`qualid` is used as a solution. - Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| - into a complete structure built on |c_i|. + Otherwise said, :token:`qualid` is canonically used to extend the field :n:`x__i` + into a complete structure built on :n:`c__i` when :n:`c__i` unifies with :n:`(x__i _)`. + + The following kinds of terms are supported for the fields :n:`c__i` of :token:`qualid`: + + * :term:`Constants <constant>` and section variables of an active section, + applied to zero or more arguments. + * :token:`sort`\s. + * Literal functions: `fun … => …`. + * Literal, non-dependent function types, i.e. implications: `… -> …`. + * Variables bound in :token:`qualid`. + + Only the head symbol of an existing instance's field :n:`c__i` + is considered when searching for a canonical extension. + We call this head symbol the *key* and we say ":token:`qualid` *keys* the field :n:`x__i` to :n:`k`" when :n:`c__i`'s + head symbol is :n:`k`. + Keys are the only piece of information that is used for canonical extension. + The keys corresponding to the kinds of terms listed above are: + + * For constants and section variables, potentially applied to arguments: + the constant or variable itself, disregarding any arguments. + * For sorts: the sort itself. + * For literal functions: skip the abstractions and use the key of the body. + * For literal functions types: a disembodied implication key denoted `_ -> _`, disregarding both its + domain and codomain. + * For variables bound in :token:`qualid`: a catch-all key denoted `_`. + + This means that, for example, `(some_constant x1)` and `(some_constant (other_constant y1 y2) x2)` + are not distinct keys. + + Variables bound in :token:`qualid` match any term for the purpose of canonical extension. + This has two major consequences for a field :n:`c__i` keyed to a variable of :token:`qualid`: + + 1. Unless another key—and, thus, instance—matches :n:`c__i`, the instance will always be considered by + unification. + 2. :n:`c__i` will be considered overlapping not distinct from any other canonical instance + that keys :n:`x__i` to one of its own variables. + + A record field :n:`x__i` can only be keyed once to each key. + Coq prints a warning when :token:`qualid` keys :n:`x__i` to a term + whose head symbol is already keyed by an existing canonical instance. + In this case, Coq will not register that :token:`qualid` as a canonical + extension. + (The remaining fields of the instance can still be used for canonical extension.) Canonical structures are particularly useful when mixed with coercions and strict implicit arguments. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 25ac72069b..52cf565998 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1251,6 +1251,10 @@ Notations This command supports the :attr:`deprecated` attribute. + .. exn:: Notation levels must range between 0 and 6. + + The level of a notation must be an integer between 0 and 6 inclusive. + Abbreviations ~~~~~~~~~~~~~ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d212256765..f65361bc64 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1182,7 +1182,7 @@ Here are the syntax elements used by the various notation commands. .. prodn:: syntax_modifier ::= at level @natural | in custom @ident {? at level @natural } - | {+, @ident } at @level + | {+, @ident } {| at @level | in scope @ident } | @ident at @level {? @binder_interp } | @ident @explicit_subentry | @ident @binder_interp @@ -1374,6 +1374,10 @@ interpreted in the scope stack extended with the scope bound to :n:`@scope_key`. Removes the delimiting keys associated with a scope. +The arguments of an :ref:`abbreviation <Abbreviations>` can be interpreted +in a scope stack locally extended with a given scope by using the modifier +:n:`{+, @ident } in scope @scope_name`.s + Binding types or coercion classes to a notation scope ++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1567,7 +1571,7 @@ Displaying information about scopes Abbreviations -------------- -.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( only parsing ) } +.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( {+, @syntax_modifier } ) } :name: Notation (abbreviation) .. todo: for some reason, Sphinx doesn't complain about a duplicate name if diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index fd1c3c0260..48d399dfd3 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -365,7 +365,6 @@ term100: [ | REPLACE term99 ":" term200 | WITH term99 ":" type | MOVETO term_cast term99 ":" type -| MOVETO term_cast term99 ":>" ] constr: [ @@ -1410,8 +1409,9 @@ syntax_modifier: [ | DELETE "in" "custom" IDENT | REPLACE "in" "custom" IDENT; "at" "level" natural | WITH "in" "custom" IDENT OPT ( "at" "level" natural ) -| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level -| WITH LIST1 IDENT SEP "," "at" level +| DELETE IDENT; "in" "scope" IDENT +| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] +| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] ] explicit_subentry: [ @@ -2643,7 +2643,6 @@ SPLICE: [ | quoted_attributes (* todo: splice or not? *) | printable | hint -| only_parsing | record_fields | constructor_type | record_binder diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 0c8980b1bd..b5a234a86a 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,6 +1,15 @@ (* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) DOC_GRAMMAR +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry +] + Constr.ident: [ | Prim.ident ] @@ -75,7 +84,6 @@ term100: [ | term99 "<:" term200 | term99 "<<:" term200 | term99 ":" term200 -| term99 ":>" | term99 ] @@ -478,15 +486,6 @@ strategy_level: [ | "transparent" ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry -] - opt_hintbases: [ | | ":" LIST1 IDENT @@ -1401,18 +1400,13 @@ syntax: [ | "Undelimit" "Scope" IDENT | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr | "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] -| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" identref LIST0 ident ":=" constr syntax_modifiers | "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | "Format" "Notation" STRING STRING STRING | "Reserved" "Infix" ne_lstring syntax_modifiers | "Reserved" "Notation" ne_lstring syntax_modifiers ] -only_parsing: [ -| "(" "only" "parsing" ")" -| -] - level: [ | "level" natural | "next" "level" @@ -1428,8 +1422,9 @@ syntax_modifier: [ | "only" "printing" | "only" "parsing" | "format" STRING OPT STRING -| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] | IDENT; "at" level OPT binder_interp +| IDENT; "in" "scope" IDENT | IDENT binder_interp | IDENT explicit_subentry ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 40bb980e90..cd96693bf0 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -553,7 +553,6 @@ term_cast: [ | term10 ":" type | term10 "<:" type | term10 "<<:" type -| term10 ":>" ] term_match: [ @@ -1096,7 +1095,7 @@ command: [ | "Undelimit" "Scope" scope_name | "Bind" "Scope" scope_name "with" LIST1 class | "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] -| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) | "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] | "Format" "Notation" string string string | "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) @@ -1540,7 +1539,7 @@ class: [ syntax_modifier: [ | "at" "level" natural | "in" "custom" ident OPT ( "at" "level" natural ) -| LIST1 ident SEP "," "at" level +| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ] | ident "at" level OPT binder_interp | ident explicit_subentry | ident binder_interp diff --git a/gramlib/gramlib.mllib b/gramlib/gramlib.mllib index 4c915b2b05..e7e08f8ae1 100644 --- a/gramlib/gramlib.mllib +++ b/gramlib/gramlib.mllib @@ -1,4 +1,3 @@ -Ploc Plexing Gramext Grammar diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index fd3ff25fc1..77444b991a 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -17,7 +17,7 @@ module type S = sig module Parsable : sig type t - val make : ?loc:Loc.t -> char Stream.t -> t + val make : ?source:Loc.source -> char Stream.t -> t val comments : t -> ((int * int) * string) list end @@ -29,8 +29,9 @@ module type S = sig val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val name : 'a t -> string - val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t - val parse_token_stream : 'a t -> te Stream.t -> 'a + type 'a parser_fun = { parser_fun : te LStream.t -> 'a } + val of_parser : string -> 'a parser_fun -> 'a t + val parse_token_stream : 'a t -> te LStream.t -> 'a val print : Format.formatter -> 'a t -> unit end @@ -114,7 +115,7 @@ module GMake (L : Plexing.S) = struct type te = L.te type 'c pattern = 'c L.pattern -type 'a parser_t = L.te Stream.t -> 'a +type 'a parser_t = L.te LStream.t -> 'a type grammar = { gtokens : (string * string option, int ref) Hashtbl.t } @@ -148,7 +149,7 @@ type 'a ty_entry = { and 'a ty_desc = | Dlevels of 'a ty_level list -| Dparser of (Plexing.location_function -> 'a parser_t) +| Dparser of 'a parser_t and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level @@ -956,14 +957,6 @@ let print_entry ppf e = end; fprintf ppf " ]@]" -let floc = ref (fun _ -> failwith "internal error when computing location") - -let loc_of_token_interval bp ep = - if bp == ep then - if bp == 0 then Ploc.dummy else Ploc.after (!floc (bp - 1)) 0 1 - else - let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2 - let name_of_symbol : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> string = fun entry -> function @@ -1115,10 +1108,10 @@ let top_tree : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> (s, tr, a) ty_tr | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure let skip_if_empty bp p strm = - if Stream.count strm == bp then fun a -> p strm + if LStream.count strm == bp then fun a -> p strm else raise Stream.Failure -let continue entry bp a symb son p1 (strm__ : _ Stream.t) = +let continue entry bp a symb son p1 (strm__ : _ LStream.t) = let a = (entry_of_symb entry symb).econtinue 0 bp a strm__ in let act = try p1 strm__ with @@ -1129,7 +1122,7 @@ let continue entry bp a symb son p1 (strm__ : _ Stream.t) = (** Recover from a success on [symb] with result [a] followed by a failure on [son] in a rule of the form [a = symb; son] *) let do_recover parser_of_tree entry nlevn alevn bp a symb son - (strm__ : _ Stream.t) = + (strm__ : _ LStream.t) = try (* Try to replay the son with the top occurrence of NEXT (by default at level nlevn) and trailing SELF (by default at alevn) @@ -1148,7 +1141,7 @@ let do_recover parser_of_tree entry nlevn alevn bp a symb son « OPT "!"; ident » fails to see an ident and the OPT was resolved into the empty sequence, with application e.g. to being able to safely write « LIST1 [ OPT "!"; id = ident -> id] ». *) - skip_if_empty bp (fun (strm__ : _ Stream.t) -> raise Stream.Failure) + skip_if_empty bp (fun (strm__ : _ LStream.t) -> raise Stream.Failure) strm__ with Stream.Failure -> (* In case of success on just SELF, NEXT or an explicit call to @@ -1164,19 +1157,6 @@ let do_recover parser_of_tree entry nlevn alevn bp a symb son let recover parser_of_tree entry nlevn alevn bp a symb son strm = do_recover parser_of_tree entry nlevn alevn bp a symb son strm -let token_count = ref 0 - -let peek_nth n strm = - let list = Stream.npeek n strm in - token_count := Stream.count strm + n; - let rec loop list n = - match list, n with - x :: _, 1 -> Some x - | _ :: l, n -> loop l (n - 1) - | [], _ -> None - in - loop list n - let item_skipped = ref false let call_and_push ps al strm = @@ -1184,7 +1164,7 @@ let call_and_push ps al strm = let a = ps strm in let al = if !item_skipped then al else a :: al in item_skipped := false; al -let token_ematch gram tok = +let token_ematch tok = let tematch = L.tok_match tok in fun tok -> tematch tok @@ -1196,16 +1176,16 @@ let token_ematch gram tok = let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_tree -> r parser_t = fun entry nlevn alevn -> function - DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure) - | LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act) + DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure) + | LocAct (act, _) -> (fun (strm__ : _ LStream.t) -> act) | Node (_, {node = Sself; son = LocAct (act, _); brother = DeadEnd}) -> (* SELF on the right-hand side of the last rule *) - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> let a = entry.estart alevn strm__ in act a) | Node (_, {node = Sself; son = LocAct (act, _); brother = bro}) -> (* SELF on the right-hand side of a rule *) let p2 = parser_of_tree entry nlevn alevn bro in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> match try Some (entry.estart alevn strm__) with Stream.Failure -> None with @@ -1222,8 +1202,8 @@ let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_ let ps = parser_of_symbol entry nlevn s in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn s son in - (fun (strm__ : _ Stream.t) -> - let bp = Stream.count strm__ in + (fun (strm__ : _ LStream.t) -> + let bp = LStream.count strm__ in let a = ps strm__ in let act = try p1 bp a strm__ with @@ -1249,8 +1229,8 @@ let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_ let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn s son in let p2 = parser_of_tree entry nlevn alevn bro in - (fun (strm : _ Stream.t) -> - let bp = Stream.count strm in + (fun (strm : _ LStream.t) -> + let bp = LStream.count strm in match try Some (ps strm) with Stream.Failure -> None with Some a -> begin match @@ -1268,11 +1248,11 @@ let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_ let p1 = parser_of_token_list entry son p1 rev_tokl last_tok in - fun (strm__ : _ Stream.t) -> + fun (strm__ : _ LStream.t) -> try p1 strm__ with Stream.Failure -> p2 strm__ and parser_cont : type s tr tr' a r. (a -> r) parser_t -> s ty_entry -> int -> int -> (s, tr, a) ty_symbol -> (s, tr', a -> r) ty_tree -> int -> a -> (a -> r) parser_t = - fun p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) -> + fun p1 entry nlevn alevn s son bp a (strm__ : _ LStream.t) -> try p1 strm__ with Stream.Failure -> recover parser_of_tree entry nlevn alevn bp a s son strm__ @@ -1280,18 +1260,15 @@ and parser_of_token_list : type s tr lt r f. s ty_entry -> (s, tr, lt -> r) ty_tree -> (int -> lt -> (lt -> r) parser_t) -> (r, f) tok_list -> lt pattern -> f parser_t = fun entry son p1 rev_tokl last_tok -> - let n = tok_list_length rev_tokl + 1 in + let n = tok_list_length rev_tokl in let plast : r parser_t = - let tematch = token_ematch egram last_tok in + let tematch = token_ematch last_tok in let ps strm = - match peek_nth n strm with - Some tok -> - let r = tematch tok in - for _i = 1 to n do Stream.junk strm done; r - | None -> raise Stream.Failure + let r = tematch (LStream.peek_nth n strm) in + for _i = 0 to n do LStream.junk strm done; r in - fun (strm : _ Stream.t) -> - let bp = Stream.count strm in + fun (strm : _ LStream.t) -> + let bp = LStream.count strm in let a = ps strm in match try Some (p1 bp a strm) with Stream.Failure -> None with Some act -> act a @@ -1301,13 +1278,9 @@ and parser_of_token_list : type s tr lt r f. fun n tokl plast -> match tokl with | TokNil -> plast | TokCns (tok, tokl) -> - let tematch = token_ematch egram tok in - let ps strm = - match peek_nth n strm with - Some tok -> tematch tok - | None -> raise Stream.Failure - in - let plast = fun (strm : _ Stream.t) -> + let tematch = token_ematch tok in + let ps strm = tematch (LStream.peek_nth n strm) in + let plast = fun (strm : _ LStream.t) -> let a = ps strm in let act = plast strm in act a in loop (n - 1) tokl plast in loop (n - 1) rev_tokl plast @@ -1317,17 +1290,17 @@ and parser_of_symbol : type s tr a. function | Slist0 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in - let rec loop al (strm__ : _ Stream.t) = + let rec loop al (strm__ : _ LStream.t) = match try Some (ps al strm__) with Stream.Failure -> None with Some al -> loop al strm__ | _ -> al in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> let a = loop [] strm__ in List.rev a) | Slist0sep (symb, sep, false) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in - let rec kont al (strm__ : _ Stream.t) = + let rec kont al (strm__ : _ LStream.t) = match try Some (pt strm__) with Stream.Failure -> None with Some v -> let al = @@ -1338,14 +1311,14 @@ and parser_of_symbol : type s tr a. kont al strm__ | _ -> al in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> match try Some (ps [] strm__) with Stream.Failure -> None with Some al -> let a = kont al strm__ in List.rev a | _ -> []) | Slist0sep (symb, sep, true) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in - let rec kont al (strm__ : _ Stream.t) = + let rec kont al (strm__ : _ LStream.t) = match try Some (pt strm__) with Stream.Failure -> None with Some v -> begin match @@ -1356,24 +1329,24 @@ and parser_of_symbol : type s tr a. end | _ -> al in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> match try Some (ps [] strm__) with Stream.Failure -> None with Some al -> let a = kont al strm__ in List.rev a | _ -> []) | Slist1 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in - let rec loop al (strm__ : _ Stream.t) = + let rec loop al (strm__ : _ LStream.t) = match try Some (ps al strm__) with Stream.Failure -> None with Some al -> loop al strm__ | _ -> al in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> let al = ps [] strm__ in let a = loop al strm__ in List.rev a) | Slist1sep (symb, sep, false) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in - let rec kont al (strm__ : _ Stream.t) = + let rec kont al (strm__ : _ LStream.t) = match try Some (pt strm__) with Stream.Failure -> None with Some v -> let al = @@ -1389,13 +1362,13 @@ and parser_of_symbol : type s tr a. kont al strm__ | _ -> al in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> let al = ps [] strm__ in let a = kont al strm__ in List.rev a) | Slist1sep (symb, sep, true) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in - let rec kont al (strm__ : _ Stream.t) = + let rec kont al (strm__ : _ LStream.t) = match try Some (pt strm__) with Stream.Failure -> None with Some v -> begin match @@ -1412,35 +1385,35 @@ and parser_of_symbol : type s tr a. end | _ -> al in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> let al = ps [] strm__ in let a = kont al strm__ in List.rev a) | Sopt s -> let ps = parser_of_symbol entry nlevn s in - (fun (strm__ : _ Stream.t) -> + (fun (strm__ : _ LStream.t) -> match try Some (ps strm__) with Stream.Failure -> None with Some a -> Some a | _ -> None) | Stree t -> let pt = parser_of_tree entry 1 0 t in - (fun (strm__ : _ Stream.t) -> - let bp = Stream.count strm__ in + (fun (strm__ : _ LStream.t) -> + let bp = LStream.count strm__ in let a = pt strm__ in - let ep = Stream.count strm__ in - let loc = loc_of_token_interval bp ep in a loc) - | Snterm e -> (fun (strm__ : _ Stream.t) -> e.estart 0 strm__) + let ep = LStream.count strm__ in + let loc = LStream.interval_loc bp ep strm__ in a loc) + | Snterm e -> (fun (strm__ : _ LStream.t) -> e.estart 0 strm__) | Snterml (e, l) -> - (fun (strm__ : _ Stream.t) -> e.estart (level_number e l) strm__) - | Sself -> (fun (strm__ : _ Stream.t) -> entry.estart 0 strm__) - | Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__) + (fun (strm__ : _ LStream.t) -> e.estart (level_number e l) strm__) + | Sself -> (fun (strm__ : _ LStream.t) -> entry.estart 0 strm__) + | Snext -> (fun (strm__ : _ LStream.t) -> entry.estart nlevn strm__) | Stoken tok -> parser_of_token entry tok and parser_of_token : type s a. s ty_entry -> a pattern -> a parser_t = fun entry tok -> let f = L.tok_match tok in fun strm -> - match Stream.peek strm with - Some tok -> let r = f tok in Stream.junk strm; r + match LStream.peek strm with + Some tok -> let r = f tok in LStream.junk strm; r | None -> raise Stream.Failure and parse_top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a parser_t = fun entry symb -> @@ -1475,7 +1448,7 @@ and parse_top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a parser let rec start_parser_of_levels entry clevn = function - [] -> (fun levn (strm__ : _ Stream.t) -> raise Stream.Failure) + [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure) | Level lev :: levs -> let p1 = start_parser_of_levels entry (succ clevn) levs in match lev.lprefix with @@ -1497,11 +1470,11 @@ let rec start_parser_of_levels entry clevn = if levn > clevn then match strm with parser [] else *) - let (strm__ : _ Stream.t) = strm in - let bp = Stream.count strm__ in + let (strm__ : _ LStream.t) = strm in + let bp = LStream.count strm__ in let act = p2 strm__ in - let ep = Stream.count strm__ in - let a = act (loc_of_token_interval bp ep) in + let ep = LStream.count strm__ in + let a = act (LStream.interval_loc bp ep strm__) in entry.econtinue levn bp a strm) | _ -> fun levn strm -> @@ -1509,12 +1482,12 @@ let rec start_parser_of_levels entry clevn = (* Skip rules before [levn] *) p1 levn strm else - let (strm__ : _ Stream.t) = strm in - let bp = Stream.count strm__ in + let (strm__ : _ LStream.t) = strm in + let bp = LStream.count strm__ in match try Some (p2 strm__) with Stream.Failure -> None with Some act -> - let ep = Stream.count strm__ in - let a = act (loc_of_token_interval bp ep) in + let ep = LStream.count strm__ in + let a = act (LStream.interval_loc bp ep strm__) in entry.econtinue levn bp a strm | _ -> p1 levn strm__ @@ -1532,7 +1505,7 @@ let rec start_parser_of_levels entry clevn = let rec continue_parser_of_levels entry clevn = function - [] -> (fun levn bp a (strm__ : _ Stream.t) -> raise Stream.Failure) + [] -> (fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure) | Level lev :: levs -> let p1 = continue_parser_of_levels entry (succ clevn) levs in match lev.lsuffix with @@ -1549,21 +1522,21 @@ let rec continue_parser_of_levels entry clevn = (* Skip rules before [levn] *) p1 levn bp a strm else - let (strm__ : _ Stream.t) = strm in + let (strm__ : _ LStream.t) = strm in try p1 levn bp a strm__ with Stream.Failure -> let act = p2 strm__ in - let ep = Stream.count strm__ in - let a = act a (loc_of_token_interval bp ep) in + let ep = LStream.count strm__ in + let a = act a (LStream.interval_loc bp ep strm__) in entry.econtinue levn bp a strm let continue_parser_of_entry entry = match entry.edesc with Dlevels elev -> let p = continue_parser_of_levels entry 0 elev in - (fun levn bp a (strm__ : _ Stream.t) -> + (fun levn bp a (strm__ : _ LStream.t) -> try p levn bp a strm__ with Stream.Failure -> a) - | Dparser p -> fun levn bp a (strm__ : _ Stream.t) -> raise Stream.Failure + | Dparser p -> fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure let empty_entry ename levn strm = raise (Stream.Error ("entry [" ^ ename ^ "] is empty")) @@ -1572,7 +1545,7 @@ let start_parser_of_entry entry = match entry.edesc with Dlevels [] -> empty_entry entry.ename | Dlevels elev -> start_parser_of_levels entry 0 elev - | Dparser p -> fun levn strm -> p !floc strm + | Dparser p -> fun levn strm -> p strm (* Extend syntax *) @@ -1611,51 +1584,31 @@ let delete_rule entry sl = module Parsable = struct type t = - { pa_chr_strm : char Stream.t - ; pa_tok_strm : L.te Stream.t - ; pa_loc_func : Plexing.location_function + { pa_tok_strm : L.te LStream.t ; lexer_state : L.State.t ref } let parse_parsable entry p = let efun = entry.estart 0 in let ts = p.pa_tok_strm in - let cs = p.pa_chr_strm in - let fun_loc = p.pa_loc_func in - let restore = - let old_floc = !floc in - let old_tc = !token_count in - fun () -> floc := old_floc; token_count := old_tc - in let get_loc () = - try - let cnt = Stream.count ts in - (* Ensure that the token at location cnt has been peeked so that - the location function knows about it *) - let _ = Stream.peek ts in - let loc = fun_loc cnt in - if !token_count - 1 <= cnt then loc - else Loc.merge loc (fun_loc (!token_count - 1)) - with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1) + let loc = LStream.get_loc (LStream.count ts) ts in + let loc' = LStream.max_peek_loc ts in + Loc.merge loc loc' in - floc := fun_loc; - token_count := 0; - try let r = efun ts in restore (); r with + try efun ts with Stream.Failure -> let loc = get_loc () in - restore (); Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename)) | Stream.Error _ as exc -> - let loc = get_loc () in restore (); + let loc = get_loc () in Loc.raise ~loc exc | exc -> let exc,info = Exninfo.capture exc in - let loc = Stream.count cs, Stream.count cs + 1 in - restore (); (* If the original exn had a loc, keep it *) let info = match Loc.get_loc info with | Some _ -> info - | None -> Loc.add_loc info (Ploc.make_unlined loc) + | None -> Loc.add_loc info (get_loc ()) in Exninfo.iraise (exc,info) @@ -1670,12 +1623,12 @@ module Parsable = struct L.State.drop (); Exninfo.iraise (exn,info) - let make ?loc cs = + let make ?source cs = let lexer_state = ref (L.State.init ()) in L.State.set !lexer_state; - let (ts, lf) = L.tok_func ?loc cs in + let ts = L.tok_func ?source cs in lexer_state := L.State.get (); - {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf; lexer_state} + {pa_tok_strm = ts; lexer_state} let comments p = L.State.get_comments !(p.lexer_state) @@ -1686,7 +1639,7 @@ module Entry = struct let make n = { ename = n; estart = empty_entry n; econtinue = - (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); + (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); edesc = Dlevels []} let create = make let parse (e : 'a t) p : 'a = @@ -1694,11 +1647,12 @@ module Entry = struct let parse_token_stream (e : 'a t) ts : 'a = e.estart 0 ts let name e = e.ename - let of_parser n (p : Plexing.location_function -> te Stream.t -> 'a) : 'a t = + type 'a parser_fun = { parser_fun : te LStream.t -> 'a } + let of_parser n { parser_fun = (p : te LStream.t -> 'a) } : 'a t = { ename = n; - estart = (fun _ -> p !floc); + estart = (fun _ -> p); econtinue = - (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); + (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); edesc = Dparser p} let print ppf e = fprintf ppf "%a@." print_entry e end @@ -1780,8 +1734,8 @@ end module Unsafe = struct let clear_entry e = - e.estart <- (fun _ (strm__ : _ Stream.t) -> raise Stream.Failure); - e.econtinue <- (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); + e.estart <- (fun _ (strm__ : _ LStream.t) -> raise Stream.Failure); + e.econtinue <- (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); match e.edesc with Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 33006f6f65..c1605486cf 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -27,7 +27,7 @@ module type S = sig module Parsable : sig type t - val make : ?loc:Loc.t -> char Stream.t -> t + val make : ?source:Loc.source -> char Stream.t -> t val comments : t -> ((int * int) * string) list end @@ -39,8 +39,9 @@ module type S = sig val create : string -> 'a t (* compat *) val parse : 'a t -> Parsable.t -> 'a val name : 'a t -> string - val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t - val parse_token_stream : 'a t -> te Stream.t -> 'a + type 'a parser_fun = { parser_fun : te LStream.t -> 'a } + val of_parser : string -> 'a parser_fun -> 'a t + val parse_token_stream : 'a t -> te LStream.t -> 'a val print : Format.formatter -> 'a t -> unit end diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index ce3e38ff08..d6be29ccea 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -2,8 +2,7 @@ (* plexing.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -type location_function = int -> Loc.t -type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function +type 'te lexer_func = ?source:Loc.source -> char Stream.t -> 'te LStream.t module type S = sig type te diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 0c190af635..84bdc53f0b 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -10,10 +10,8 @@ (** Lexer type *) -type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function -and location_function = int -> Loc.t - (** The type of a function giving the location of a token in the - source from the token number in the stream (starting from zero). *) +(** Returning a stream equipped with a location function *) +type 'te lexer_func = ?source:Loc.source -> char Stream.t -> 'te LStream.t module type S = sig type te diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml deleted file mode 100644 index e121342c94..0000000000 --- a/gramlib/ploc.ml +++ /dev/null @@ -1,18 +0,0 @@ -(* camlp5r *) -(* ploc.ml,v *) -(* Copyright (c) INRIA 2007-2017 *) - -open Loc - -let make_unlined (bp, ep) = - {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = bp; ep = ep; } - -let dummy = - {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = 0; ep = 0; } - -(* *) - -let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} -let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli deleted file mode 100644 index 4b865110c3..0000000000 --- a/gramlib/ploc.mli +++ /dev/null @@ -1,23 +0,0 @@ -(* camlp5r *) -(* ploc.mli,v *) -(* Copyright (c) INRIA 2007-2017 *) - -val make_unlined : int * int -> Loc.t - (** [Ploc.make_unlined] is like [Ploc.make] except that the line number - is not provided (to be used e.g. when the line number is unknown. *) - -val dummy : Loc.t - (** [Ploc.dummy] is a dummy location, used in situations when location - has no meaning. *) - -(* combining locations *) - -val sub : Loc.t -> int -> int -> Loc.t - (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh] - characters and with length [len]. The previous ending position - of the location is lost. *) - -val after : Loc.t -> int -> int -> Loc.t - (** [Ploc.after loc sh len] is the location just after loc (starting at - the end position of [loc]) shifted with [sh] characters and of length - [len]. *) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index f02874253e..ddd689bee0 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -261,11 +261,9 @@ and cast_expr_eq c1 c2 = match c1, c2 with | CastConv t1, CastConv t2 | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> constr_expr_eq t1 t2 -| CastCoerce, CastCoerce -> true | CastConv _, _ | CastVM _, _ -| CastNative _, _ -| CastCoerce, _ -> false +| CastNative _, _ -> false let constr_loc c = CAst.(c.loc) let cases_pattern_expr_loc cp = CAst.(cp.loc) @@ -283,10 +281,13 @@ let local_binders_loc bll = match bll with (** Folds and maps *) let is_constructor id = - try Globnames.isConstructRef - (Smartlocate.global_of_extended_global - (Nametab.locate_extended (qualid_of_ident id))) - with Not_found -> false + match + Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id)) + with + | exception Not_found -> false + | None -> false + | Some gref -> Globnames.isConstructRef gref let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with | CPatRecord l -> @@ -343,7 +344,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CLetIn (na,a,t,b) -> f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 958e1408f8..68dd96e44b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -273,40 +273,54 @@ let make_current_scope tmp scopes = match tmp, scopes with | Some tmp_scope, scopes -> tmp_scope :: scopes | None, scopes -> scopes -let pr_scope_stack = function - | [] -> str "the empty scope stack" - | [a] -> str "scope " ++ str a - | l -> str "scope stack " ++ +let pr_scope_stack begin_of_sentence l = + let bstr x = + if begin_of_sentence then str (CString.capitalize_ascii x) else str x in + match l with + | [] -> bstr "the empty scope stack" + | [a] -> bstr "scope " ++ str a + | l -> bstr "scope stack " ++ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" -let error_inconsistent_scope ?loc id scopes1 scopes2 = - user_err ?loc ~hdr:"set_var_scope" - (Id.print id ++ str " is here used in " ++ - pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ - pr_scope_stack scopes1) +let warn_inconsistent_scope = + CWarnings.create ~name:"inconsistent-scopes" ~category:"syntax" + (fun (id,scopes1,scopes2) -> + (str "Argument " ++ Id.print id ++ + strbrk " was previously inferred to be in " ++ + pr_scope_stack false scopes1 ++ + strbrk " but is here used in " ++ + pr_scope_stack false scopes2 ++ + strbrk ". " ++ + pr_scope_stack true scopes1 ++ + strbrk " will be used at parsing time unless you override it by" ++ + strbrk " annotating the argument with an explicit scope of choice.")) let error_expect_binder_notation_type ?loc id = user_err ?loc (Id.print id ++ str " is expected to occur in binding position in the right-hand side.") -let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = +let set_notation_var_scope ?loc id (tmp_scope,subscopes as scopes) ntnvars = try - let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in - if istermvar then begin - (* scopes have no effect on the interpretation of identifiers *) - (match !idscopes with + let _,idscopes,typ = Id.Map.find id ntnvars in + match typ with + | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id + | Notation_term.NtnInternTypeAny principal -> + match !idscopes with | None -> idscopes := Some scopes | Some (tmp_scope', subscopes') -> let s' = make_current_scope tmp_scope' subscopes' in let s = make_current_scope tmp_scope subscopes in - if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s); - (match typ with - | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id - | Notation_term.NtnInternTypeAny -> ()) - end - else - used_as_binder := true + if Option.is_empty principal && not (List.equal String.equal s' s) then + warn_inconsistent_scope ?loc (id,s',s) + with Not_found -> + (* Not in a notation *) + () + +let set_var_is_binder ?loc id ntnvars = + try + let used_as_binder,_,_ = Id.Map.find id ntnvars in + used_as_binder := true with Not_found -> (* Not in a notation *) () @@ -484,7 +498,7 @@ let push_name_env ntnvars implargs env = | { loc; v = Name id } -> if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; - set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; + set_var_is_binder ?loc id ntnvars; let uid = var_uid id in Dumpglob.dump_binding ?loc uid; pure_push_name_env (id,(Variable,implargs,[],uid)) env @@ -1064,7 +1078,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin - if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; + if not (Id.Map.mem id env.impls) then set_notation_var_scope ?loc id (env.tmp_scope,env.scopes) ntnvars; gvar (loc,id) us end else @@ -1130,14 +1144,54 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + +let intern_name_alias = function + | { CAst.v = CRef(qid,u) } -> + let r = + try Some (intern_extended_global_of_qualid qid) + with Not_found -> None + in + Option.bind r Smartlocate.global_of_extended_global |> + Option.map (fun r -> r, intern_instance ~local_univs:empty_local_univs u) + | _ -> None + let intern_projection qid = - try - match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with - | GlobRef.ConstRef c as gr -> - (gr, Structure.find_from_projection c) - | _ -> raise Not_found - with Not_found -> - Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + match + Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) |> + Option.map (function + | GlobRef.ConstRef c as x -> x, Structure.find_from_projection c + | _ -> raise Not_found) + with + | exception Not_found -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + | None -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + | Some x -> x (**********************************************************************) (* Interpreting references *) @@ -1182,37 +1236,6 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] -let intern_sort_name ~local_univs = function - | CSProp -> GSProp - | CProp -> GProp - | CSet -> GSet - | CRawType u -> GRawUniv u - | CType qid -> - let is_id = qualid_is_ident qid in - let local = if not is_id then None - else Id.Map.find_opt (qualid_basename qid) local_univs.bound - in - match local with - | Some u -> GUniv u - | None -> - try GUniv (Univ.Level.make (Nametab.locate_universe qid)) - with Not_found -> - if is_id && local_univs.unb_univs - then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) - else - CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") - -let intern_sort ~local_univs s = - map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s - -let intern_instance ~local_univs us = - Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us - -let try_interp_name_alias = function - | [], { CAst.v = CRef (ref,u) } -> - NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u) - | _ -> raise Not_found - (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1843,7 +1866,7 @@ let rec intern_pat genv ntnvars aliases pat = intern_cstr_with_all_args loc c true [] pl | RCPatAtom (Some ({loc;v=id},scopes)) -> let aliases = merge_aliases aliases (make ?loc @@ Name id) in - set_var_scope ?loc id false scopes ntnvars; + set_var_is_binder ?loc id ntnvars; (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom None -> let { alias_ids = ids; alias_map = asubst; } = aliases in @@ -2561,7 +2584,11 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (function + | (NtnInternTypeAny None | NtnInternTypeOnlyBinder) as typ -> (ref false, ref None, typ) + | NtnInternTypeAny (Some scope) as typ -> + (ref false, ref (Some (Some scope,[])), typ) + ) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env {ids; unb = false; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 65b63962d0..379bd61070 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -147,12 +147,13 @@ val interp_constr_pattern : env -> evar_map -> ?expected_type:typing_constraint -> constr_pattern_expr -> constr_pattern -(** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : qualid -> GlobRef.t +(** Returns None if it's a syndef not bound to a name, raises an error + if not existing *) +val intern_reference : qualid -> GlobRef.t option -(** For syntactic definitions: check if abbreviation to a name - and avoid early insertion of maximal implicit arguments *) -val try_interp_name_alias : 'a list * constr_expr -> notation_constr +(** Returns None if not a reference or a syndef not bound to a name *) +val intern_name_alias : + constr_expr -> (GlobRef.t * Glob_term.glob_level list option) option (** Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> qualid -> glob_constr @@ -174,7 +175,7 @@ val interp_context_evars : (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) -val locate_reference : Libnames.qualid -> GlobRef.t +val locate_reference : Libnames.qualid -> GlobRef.t option val is_global : Id.t -> bool (** Interprets a term as the left-hand side of a notation. The returned map is diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ea5e2a1ad4..313a9e85a4 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -35,9 +35,8 @@ let rec alpha_var id1 id2 = function let cast_type_iter2 f t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> f t1 t2 | CastVM t1, CastVM t2 -> f t1 t2 - | CastCoerce, CastCoerce -> () | CastNative t1, CastNative t2 -> f t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit + | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit (* used to update the notation variable with the local variables used in NList and NBinderList, since the iterator has its own variable *) @@ -681,7 +680,7 @@ let check_variables_and_reversibility nenv str " position as part of a recursive pattern.") in let check_type x typ = match typ with - | NtnInternTypeAny -> + | NtnInternTypeAny _ -> begin try check_pair "term" x (Id.Map.find x recvars) foundrec with Not_found -> check_bound x @@ -1319,12 +1318,9 @@ let match_cast match_fun sigma c1 c2 = | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> match_fun sigma t1 t2 - | CastCoerce, CastCoerce -> - sigma | CastConv _, _ | CastVM _, _ - | CastNative _, _ - | CastCoerce, _ -> raise No_match + | CastNative _, _ -> raise No_match let does_not_come_from_already_eta_expanded_var glob = (* This is hack to avoid looping on a rule with rhs of the form *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 2979447cf8..ec7165f854 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -91,7 +91,8 @@ type notation_var_instance_type = in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeAny | NtnInternTypeOnlyBinder + | NtnInternTypeAny of scope_name option + | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91d05f7317..56b3cd9815 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -33,7 +33,7 @@ let global_of_extended_global_head = function | _ -> raise Not_found in head_of syn_def -let global_of_extended_global = function +let global_of_extended_global_exn = function | TrueGlobal ref -> ref | SynDef kn -> match search_syntactic_definition kn with @@ -45,11 +45,15 @@ let locate_global_with_alias ?(head=false) qid = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref - else global_of_extended_global ref + else global_of_extended_global_exn ref with Not_found -> user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") +let global_of_extended_global x = + try Some (global_of_extended_global_exn x) + with Not_found -> None + let global_constant_with_alias qid = try match locate_global_with_alias qid with | Names.GlobRef.ConstRef c -> c diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 26f2a4f36d..abf9839c9e 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -19,8 +19,9 @@ open Globnames val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t -(** Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> GlobRef.t +(** Extract a global_reference from a reference that can be an "alias". + If the reference points to a more complex term, we return None *) +val global_of_extended_global : extended_global_reference -> GlobRef.t option (** Locate a reference taking into account possible "alias" notations. May raise [Nametab.GlobalizationError _] for an unknown reference, diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ddbd5fa0a7..13044958dc 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -23,7 +23,7 @@ open Context.Rel.Declaration type mind_specif = mutual_inductive_body * one_inductive_body -(* raise Not_found if not an inductive type *) +(* raises an anomaly if not an inductive type *) let lookup_mind_specif env (kn,tyi) = let mib = Environ.lookup_mind kn env in if tyi >= Array.length mib.mind_packets then diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 5808a3fa65..4afc7c439a 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -30,7 +30,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body (** {6 ... } *) (** Fetching information in the environment about an inductive type. - Raises [Not_found] if the inductive type is not found. *) + Raises an anomaly if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) diff --git a/lib/lStream.ml b/lib/lStream.ml new file mode 100644 index 0000000000..169cc7cf3e --- /dev/null +++ b/lib/lStream.ml @@ -0,0 +1,79 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Streams equipped with a (non-canonical) location function *) + +type 'a t = { + strm : 'a Stream.t; + (* Give the loc of i-th element (counting from 1) and the empty initial interval if 0 *) + fun_loc : int -> Loc.t; + (* Remember max token peeked *) + mutable max_peek : int; +} + +let from ?(source=Loc.ToplevelInput) f = + let loct = Hashtbl.create 207 in + let loct_func loct i = Hashtbl.find loct i in + let loct_add loct i loc = Hashtbl.add loct i loc in + let strm = + Stream.from + (fun i -> + match f i with + | None -> None + | Some (a,loc) -> + loct_add loct i loc; Some a) in + let initial = Loc.initial source in + let fun_loc i = if i = 0 then initial else loct_func loct (i - 1) in + { strm; max_peek = 0; fun_loc } + +let count strm = Stream.count strm.strm + +let current_loc strm = + strm.fun_loc (Stream.count strm.strm) + +let max_peek_loc strm = + strm.fun_loc strm.max_peek + +let interval_loc bp ep strm = + assert (bp <= ep); + if ep > strm.max_peek then failwith "Not peeked position"; + if bp == ep then + Loc.after (strm.fun_loc bp) 0 0 + else + let loc1 = strm.fun_loc (bp + 1) in + let loc2 = strm.fun_loc ep in + Loc.merge loc1 loc2 + +let get_loc n strm = + strm.fun_loc (n + 1) + +let peek strm = + let a = Stream.peek strm.strm in + if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek; + a + +let npeek n strm = + let l = Stream.npeek n strm.strm in + strm.max_peek <- max (Stream.count strm.strm + List.length l) strm.max_peek; + l + +let peek_nth n strm = + let list = Stream.npeek (n + 1) strm.strm in + let rec loop list p = + match list, p with + x :: _, 0 -> strm.max_peek <- Stream.count strm.strm + n + 1; x + | _ :: l, p -> loop l (p - 1) + | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure + in + loop list n + +let junk strm = Stream.junk strm.strm + +let next strm = Stream.next strm.strm diff --git a/lib/lStream.mli b/lib/lStream.mli new file mode 100644 index 0000000000..fc9b5b5ce1 --- /dev/null +++ b/lib/lStream.mli @@ -0,0 +1,55 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extending streams with a (non-canonical) location function *) + +type 'a t +val from : ?source:Loc.source -> (int -> ('a * Loc.t) option) -> 'a t + +(** Returning the loc of the last consumed element or the initial loc + if no element is consumed *) +val current_loc : 'a t -> Loc.t + +(** Returning the loc of the max visited element or the initial loc + if no element is consumed *) +val max_peek_loc : 'a t -> Loc.t + +(** Returning the loc starting after element [bp] (counting from 0) + and spanning up to already peeked element at position [ep], under + the assumption that [bp] <= [ep]; returns an empty interval if + [bp] = [ep]; returns the empty initial interval if additionally + [bp] = 0; fails if the elements have not been peeked yet *) +val interval_loc : int -> int -> 'a t -> Loc.t + +(** Return location of an already peeked element at some position counting from 0; + fails if the element has not been peeked yet *) +val get_loc : int -> 'a t -> Loc.t + +(** Lifted usual function on streams *) + +val count : 'a t -> int + +val peek : 'a t -> 'a option + +val npeek : int -> 'a t -> 'a list + +val junk : 'a t -> unit + (** consumes the next element if there is one *) + +val next : 'a t -> 'a + (** [next strm] returns and consumes the next element; + raise [Stream.Failure] if the stream is empty *) + +(** Other functions *) + +val peek_nth : int -> 'a t -> 'a + (** [peek_nth n strm] returns the nth element counting from 0 without + consuming the stream; raises [Stream.Failure] if not enough + elements *) diff --git a/lib/lib.mllib b/lib/lib.mllib index bbc9966498..a318db64be 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -12,6 +12,8 @@ CErrors CWarnings CDebug +LStream + AcyclicGraph Rtree System diff --git a/lib/loc.ml b/lib/loc.ml index 09fa45a884..512555b554 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -68,6 +68,10 @@ let merge_opt l1 l2 = match l1, l2 with | None, Some l -> Some l | Some l1, Some l2 -> Some (merge l1 l2) +let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} + +let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} + let finer l1 l2 = match l1, l2 with | None, _ -> false | Some l , None -> true @@ -78,6 +82,7 @@ let unloc loc = (loc.bp, loc.ep) let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } (** Located type *) + type 'a located = t option * 'a let tag ?loc x = loc, x @@ -96,4 +101,3 @@ let raise ?loc e = | Some loc -> let info = Exninfo.add Exninfo.null location loc in Exninfo.iraise (e, info) - diff --git a/lib/loc.mli b/lib/loc.mli index c54a837bb4..2bbfaa5cce 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -45,6 +45,15 @@ val merge : t -> t -> t val merge_opt : t option -> t option -> t option (** Merge locations, usually generating the largest possible span *) +val sub : t -> int -> int -> t +(** [sub loc sh len] is the location [loc] shifted with [sh] + characters and with length [len]. The previous ending position + of the location is lost. *) + +val after : t -> int -> int -> t +(** [after loc sh len] is the location just after loc (starting at the + end position of [loc]) shifted with [sh] characters and of length [len]. *) + val finer : t option -> t option -> bool (** Answers [true] when the first location is more defined, or, when both defined, included in the second one *) diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index d8d2f2a2ef..bb1797ee02 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -11,7 +11,6 @@ open Pp open Util open Tok -open Gramlib (* Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. *) @@ -115,7 +114,7 @@ let bad_token str = raise (Error.E (Bad_token str)) (* Update a loc without allocating an intermediate pair *) let set_loc_pos loc bp ep = - Ploc.sub loc (bp - loc.Loc.bp) (ep - bp) + Loc.sub loc (bp - loc.Loc.bp) (ep - bp) (* Increase line number by 1 and update position of beginning of line *) let bump_loc_line loc bol_pos = @@ -216,7 +215,9 @@ let lookup_utf8 loc cs = | Some ('\x80'..'\xFF' as c) -> lookup_utf8_tail loc c cs | None -> EmptyStream -let unlocated f x = f x +let unlocated f x = + let dummy_loc = Loc.(initial ToplevelInput) in + f dummy_loc x (** FIXME: should we still unloc the exception? *) (* try f x with Loc.Exc_located (_, exc) -> raise exc *) @@ -226,7 +227,7 @@ let check_keyword str = Stream.junk s; bad_token str | _ -> - match unlocated lookup_utf8 Ploc.dummy s with + match unlocated lookup_utf8 s with | Utf8Token (_,n) -> njunk n s; loop_symb s | AsciiChar -> Stream.junk s; loop_symb s | EmptyStream -> () @@ -242,7 +243,7 @@ let check_ident str = Stream.junk s; loop_id true s | _ -> - match unlocated lookup_utf8 Ploc.dummy s with + match unlocated lookup_utf8 s with | Utf8Token (st, n) when not intail && Unicode.is_valid_ident_initial st -> njunk n s; loop_id true s | Utf8Token (st, n) when intail && Unicode.is_valid_ident_trailing st -> njunk n s; @@ -793,20 +794,6 @@ let next_token ~diff_mode loc s = Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t); r *) -(* Location table system for creating tables associating a token count - to its location in a char stream (the source) *) - -let locerr i = - let m = "Lexer: location function called on token "^string_of_int i in - invalid_arg m - -let loct_create () = Hashtbl.create 207 - -let loct_func loct i = - try Hashtbl.find loct i with Not_found -> locerr i - -let loct_add loct i loc = Hashtbl.add loct i loc - (** {6 The lexer of Coq} *) (** Note: removing a token. @@ -837,17 +824,13 @@ let token_text : type c. c Tok.p -> string = function | PBULLET (Some s) -> "BULLET \"" ^ s ^ "\"" | PQUOTATION lbl -> "QUOTATION \"" ^ lbl ^ "\"" -let func next_token ?loc cs = - let loct = loct_create () in - let cur_loc = ref (Option.default Loc.(initial ToplevelInput) loc) in - let ts = - Stream.from - (fun i -> - let (tok, loc) = next_token !cur_loc cs in - cur_loc := after loc; - loct_add loct i loc; Some tok) - in - (ts, loct_func loct) +let func next_token ?(source=Loc.ToplevelInput) cs = + let cur_loc = ref (Loc.initial source) in + LStream.from ~source + (fun i -> + let (tok, loc) = next_token !cur_loc cs in + cur_loc := after loc; + Some (tok,loc)) module MakeLexer (Diff : sig val mode : bool end) = struct type te = Tok.t diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index efe4bfd7f6..d0d1071c26 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -151,9 +151,7 @@ GRAMMAR EXTEND Gram | c1 = term; "<<:"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } | c1 = term; ":"; c2 = term LEVEL "200" -> - { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = term; ":>" -> - { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] + { CAst.make ~loc @@ CCast(c1, CastConv c2) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index cc9e1bb31d..3393bdab7b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -21,49 +21,49 @@ struct let err () = raise Stream.Failure - type t = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option + type t = int -> Tok.t LStream.t -> int option - let rec contiguous tok n m = + let rec contiguous n m strm = n == m || - let (_, ep) = Loc.unloc (tok n) in - let (bp, _) = Loc.unloc (tok (n + 1)) in - Int.equal ep bp && contiguous tok (succ n) m + let (_, ep) = Loc.unloc (LStream.get_loc n strm) in + let (bp, _) = Loc.unloc (LStream.get_loc (n + 1) strm) in + Int.equal ep bp && contiguous (succ n) m strm - let check_no_space tok m strm = - let n = Stream.count strm in - if contiguous tok n (n+m-1) then Some m else None + let check_no_space m strm = + let n = LStream.count strm in + if contiguous n (n+m-1) strm then Some m else None let to_entry s (lk : t) = - let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in - Entry.of_parser s run + let run strm = match lk 0 strm with None -> err () | Some _ -> () in + Entry.(of_parser s { parser_fun = run }) - let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with + let (>>) (lk1 : t) lk2 n strm = match lk1 n strm with | None -> None - | Some n -> lk2 tok n strm + | Some n -> lk2 n strm - let (<+>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with - | None -> lk2 tok n strm + let (<+>) (lk1 : t) lk2 n strm = match lk1 n strm with + | None -> lk2 n strm | Some n -> Some n - let lk_empty tok n strm = Some n + let lk_empty n strm = Some n - let lk_kw kw tok n strm = match stream_nth n strm with + let lk_kw kw n strm = match LStream.peek_nth n strm with | Tok.KEYWORD kw' | Tok.IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None | _ -> None - let lk_kws kws tok n strm = match stream_nth n strm with + let lk_kws kws n strm = match LStream.peek_nth n strm with | Tok.KEYWORD kw | Tok.IDENT kw -> if List.mem_f String.equal kw kws then Some (n + 1) else None | _ -> None - let lk_ident tok n strm = match stream_nth n strm with + let lk_ident n strm = match LStream.peek_nth n strm with | Tok.IDENT _ -> Some (n + 1) | _ -> None - let lk_ident_except idents tok n strm = match stream_nth n strm with + let lk_ident_except idents n strm = match LStream.peek_nth n strm with | Tok.IDENT ident when not (List.mem_f String.equal ident idents) -> Some (n + 1) | _ -> None - let lk_nat tok n strm = match stream_nth n strm with + let lk_nat n strm = match LStream.peek_nth n strm with | Tok.NUMBER p when NumTok.Unsigned.is_nat p -> Some (n + 1) | _ -> None @@ -191,9 +191,9 @@ let eoi_entry en = (* Parse a string, does NOT check if the entire string was read (use eoi_entry) *) -let parse_string f ?loc x = +let parse_string f ?source x = let strm = Stream.of_string x in - Entry.parse f (Parsable.make ?loc strm) + Entry.parse f (Parsable.make ?source strm) (* universes not used by Coq build but still used by some plugins *) type gram_universe = string diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 06d05a4797..d9165ff5a6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -119,7 +119,7 @@ end (** Parse a string *) -val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a +val parse_string : 'a Entry.t -> ?source:Loc.source -> string -> 'a val eoi_entry : 'a Entry.t -> 'a Entry.t type gram_universe [@@deprecated "Deprecated in 8.13"] diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index cfdaac710b..268d4bf9e9 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1525,8 +1525,7 @@ let inline_test r t = else let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in let has_body = - try constant_has_body (Global.lookup_constant c) - with Not_found -> false + Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c) in has_body && (let t1 = eta_red t in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3234d40f73..7d19c443e9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -930,8 +930,8 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) let evd', res = Evd.fresh_global (Global.env ()) !evd - (Constrintern.locate_reference - (qualid_of_ident equation_lemma_id)) + (Option.get (Constrintern.locate_reference + (qualid_of_ident equation_lemma_id))) in evd := evd'; let sigma, _ = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index cbdebb7bbc..f1a3cb6af8 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -241,7 +241,7 @@ let change_property_sort evd toSort princ princName = in let evd, princName_as_constr = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident princName))) in let init = let nargs = @@ -408,8 +408,8 @@ let register_struct is_rec fixpoint_exprl = (fun (evd, l) {Vernacexpr.fname} -> let evd, c = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference - (Libnames.qualid_of_ident fname.CAst.v)) + (Option.get (Constrintern.locate_reference + (Libnames.qualid_of_ident fname.CAst.v))) in let cst, u = destConst evd c in let u = EInstance.kind evd u in @@ -427,8 +427,8 @@ let register_struct is_rec fixpoint_exprl = (fun (evd, l) {Vernacexpr.fname} -> let evd, c = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference - (Libnames.qualid_of_ident fname.CAst.v)) + (Option.get (Constrintern.locate_reference + (Libnames.qualid_of_ident fname.CAst.v))) in let cst, u = destConst evd c in let u = EInstance.kind evd u in @@ -1522,7 +1522,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _, lem_cst_constr = Evd.fresh_global (Global.env ()) !evd - (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))) in let lem_cst, _ = EConstr.destConst !evd lem_cst_constr in update_Function {finfo with correctness_lemma = Some lem_cst}) @@ -1592,7 +1592,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) in let _, lem_cst_constr = Evd.fresh_global (Global.env ()) !evd - (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))) in let lem_cst, _ = destConst !evd lem_cst_constr in update_Function {finfo with completeness_lemma = Some lem_cst}) @@ -1615,7 +1615,7 @@ let derive_inversion fix_names = (fun id (evd, l) -> let evd, c = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference (Libnames.qualid_of_ident id)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident id))) in let cst, u = EConstr.destConst evd c in (evd, (cst, EConstr.EInstance.kind evd u) :: l)) @@ -1635,8 +1635,8 @@ let derive_inversion fix_names = (fun id (evd, l) -> let evd, id = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference - (Libnames.qualid_of_ident (mk_rel_id id))) + (Option.get (Constrintern.locate_reference + (Libnames.qualid_of_ident (mk_rel_id id)))) in (evd, fst (EConstr.destInd evd id) :: l)) fix_names (evd', []) @@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) = let sigma = Evd.from_env env in let c, c_body = match f_ref with - | GlobRef.ConstRef c -> ( - try (c, Global.lookup_constant c) - with Not_found -> + | GlobRef.ConstRef c -> + if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else CErrors.user_err Pp.( str "Cannot find " - ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) ) + ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) | _ -> CErrors.user_err Pp.(str "Not a function reference") in match Global.body_of_constant_body Library.indirect_accessor c_body with diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 164a446fe3..fb00d2f202 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -342,7 +342,7 @@ let is_free_in id = | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false | GHole _ -> false | GCast (b, (CastConv t | CastVM t | CastNative t)) -> - is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b + is_free_in b || is_free_in t | GInt _ | GFloat _ -> false | GArray (_u, t, def, ty) -> Array.exists is_free_in t || is_free_in def || is_free_in ty) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 4e0e2dc501..1221ad0bda 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -80,10 +80,12 @@ let functional_induction with_clean c princl pat = (elimination_sort_of_goal gl) in let princ_ref = - try + match Constrintern.locate_reference (Libnames.qualid_of_ident princ_name) - with Not_found -> + with + | Some r -> r + | None -> user_err ( str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') ) diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index cb430efb40..9dec55e020 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -59,28 +59,28 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = - Pcoq.Entry.of_parser "lpar_id_colon" - (fun _ strm -> + Pcoq.Entry.(of_parser "lpar_id_colon" + { parser_fun = fun strm -> let rec skip_to_rpar p n = - match List.last (Stream.npeek n strm) with + match List.last (LStream.npeek n strm) with | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1) | KEYWORD "." -> err () | _ -> skip_to_rpar p (n+1) in let rec skip_names n = - match List.last (Stream.npeek n strm) with + match List.last (LStream.npeek n strm) with | IDENT _ | KEYWORD "_" -> skip_names (n+1) | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) | _ -> err () in let rec skip_binders n = - match List.last (Stream.npeek n strm) with + match List.last (LStream.npeek n strm) with | KEYWORD "(" -> skip_binders (skip_names (n+1)) | IDENT _ | KEYWORD "_" -> skip_binders (n+1) | KEYWORD ":=" -> () | _ -> err () in - match stream_nth 0 strm with + match LStream.peek_nth 0 strm with | KEYWORD "(" -> skip_binders 2 - | _ -> err ()) + | _ -> err () }) let lookup_at_as_comma = let open Pcoq.Lookahead in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index ad85f68b03..04341fad91 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -249,25 +249,25 @@ let pr_ssrsimpl _ _ _ = pr_simpl let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl) -let test_ssrslashnum b1 b2 _ strm = - match Util.stream_nth 0 strm with +let test_ssrslashnum b1 b2 strm = + match LStream.peek_nth 0 strm with | Tok.KEYWORD "/" -> - (match Util.stream_nth 1 strm with + (match LStream.peek_nth 1 strm with | Tok.NUMBER _ when b1 -> - (match Util.stream_nth 2 strm with + (match LStream.peek_nth 2 strm with | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> () | Tok.KEYWORD "/" -> if not b2 then () else begin - match Util.stream_nth 3 strm with + match LStream.peek_nth 3 strm with | Tok.NUMBER _ -> () | _ -> raise Stream.Failure end | _ -> raise Stream.Failure) | Tok.KEYWORD "/" when not b1 -> - (match Util.stream_nth 2 strm with + (match LStream.peek_nth 2 strm with | Tok.KEYWORD "=" when not b2 -> () | Tok.NUMBER _ when b2 -> - (match Util.stream_nth 3 strm with + (match LStream.peek_nth 3 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) | _ when not b2 -> () @@ -275,10 +275,10 @@ let test_ssrslashnum b1 b2 _ strm = | Tok.KEYWORD "=" when not b1 && not b2 -> () | _ -> raise Stream.Failure) | Tok.KEYWORD "//" when not b1 -> - (match Util.stream_nth 1 strm with + (match LStream.peek_nth 1 strm with | Tok.KEYWORD "=" when not b2 -> () | Tok.NUMBER _ when b2 -> - (match Util.stream_nth 2 strm with + (match LStream.peek_nth 2 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) | _ when not b2 -> () @@ -290,23 +290,23 @@ let test_ssrslashnum11 = test_ssrslashnum true true let test_ssrslashnum01 = test_ssrslashnum false true let test_ssrslashnum00 = test_ssrslashnum false false -let negate_parser f tok x = - let rc = try Some (f tok x) with Stream.Failure -> None in +let negate_parser f x = + let rc = try Some (f x) with Stream.Failure -> None in match rc with | None -> () | Some _ -> raise Stream.Failure let test_not_ssrslashnum = - Pcoq.Entry.of_parser - "test_not_ssrslashnum" (negate_parser test_ssrslashnum10) + Pcoq.Entry.(of_parser + "test_not_ssrslashnum" { parser_fun = negate_parser test_ssrslashnum10 }) let test_ssrslashnum00 = - Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 + Pcoq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum00 }) let test_ssrslashnum10 = - Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 + Pcoq.Entry.(of_parser "test_ssrslashnum10" { parser_fun = test_ssrslashnum10 }) let test_ssrslashnum11 = - Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 + Pcoq.Entry.(of_parser "test_ssrslashnum11" { parser_fun = test_ssrslashnum11 }) let test_ssrslashnum01 = - Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 + Pcoq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum01 }) } @@ -488,23 +488,23 @@ END (* Old kinds of terms *) -let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with +let input_ssrtermkind strm = match LStream.peek_nth 0 strm with | Tok.KEYWORD "(" -> InParens | Tok.KEYWORD "@" -> WithAt | _ -> NoFlag -let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.(of_parser "ssrtermkind" { parser_fun = input_ssrtermkind }) (* New kinds of terms *) -let input_term_annotation _ strm = - match Stream.npeek 2 strm with +let input_term_annotation strm = + match LStream.npeek 2 strm with | Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens | Tok.KEYWORD "(" :: _ -> `Parens | Tok.KEYWORD "@" :: _ -> `At | _ -> `None let term_annotation = - Pcoq.Entry.of_parser "term_annotation" input_term_annotation + Pcoq.Entry.(of_parser "term_annotation" { parser_fun = input_term_annotation }) (* terms *) @@ -837,29 +837,29 @@ END { -let reject_ssrhid _ strm = - match Util.stream_nth 0 strm with +let reject_ssrhid strm = + match LStream.peek_nth 0 strm with | Tok.KEYWORD "[" -> - (match Util.stream_nth 1 strm with + (match LStream.peek_nth 1 strm with | Tok.KEYWORD ":" -> raise Stream.Failure | _ -> ()) | _ -> () -let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid +let test_nohidden = Pcoq.Entry.(of_parser "test_ssrhid" { parser_fun = reject_ssrhid }) -let rec reject_binder crossed_paren k tok s = +let rec reject_binder crossed_paren k s = match - try Some (Util.stream_nth k s) + try Some (LStream.peek_nth k s) with Stream.Failure -> None with - | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s - | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s + | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s + | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s | Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren -> raise Stream.Failure | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure | _ -> if crossed_paren then () else raise Stream.Failure -let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0) +let _test_nobinder = Pcoq.Entry.(of_parser "test_nobinder" { parser_fun = reject_binder false 0 }) } @@ -1673,7 +1673,7 @@ let ssr_id_of_string loc s = ^ "Scripts with explicit references to anonymous variables are fragile.")) end; Id.of_string s -let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ()) +let ssr_null_entry = Pcoq.Entry.(of_parser "ssr_null" { parser_fun = fun _ -> () }) } @@ -2407,13 +2407,13 @@ let lbrace = Char.chr 123 (** Workaround to a limitation of coqpp *) let test_ssr_rw_syntax = - let test _ strm = + let test strm = if not !ssr_rw_syntax then raise Stream.Failure else if is_ssr_loaded () then () else - match Util.stream_nth 0 strm with + match LStream.peek_nth 0 strm with | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> () | _ -> raise Stream.Failure in - Pcoq.Entry.of_parser "test_ssr_rw_syntax" test + Pcoq.Entry.(of_parser "test_ssr_rw_syntax" { parser_fun = test }) } diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 7022949ab6..b917e43b7c 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -66,11 +66,11 @@ END { -let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with +let input_ssrtermkind strm = match LStream.peek_nth 0 strm with | Tok.KEYWORD "(" -> InParens | Tok.KEYWORD "@" -> WithAt | _ -> NoFlag -let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.(of_parser "ssrtermkind" { parser_fun = input_ssrtermkind }) } diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 5eb8a88698..d6ba84d0bf 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -232,7 +232,17 @@ let occur_rigidly flags env evd (evk,_) t = let check_conv_record env sigma (t1,sk1) (t2,sk2) = let open ValuePattern in let (proji, u), arg = Termops.global_app_of_constr sigma t1 in + let t2, sk2' = decompose_app_vect sigma (shrink_eta env t2) in + let sk2 = Stack.append_app sk2' sk2 in let (sigma, solution), sk2_effective = + let t2 = + let rec remove_lambda t2 = + match EConstr.kind sigma t2 with + | Lambda (_,_,t2) -> remove_lambda t2 + | Cast (t2,_,_) -> remove_lambda t2 + | App (t2,_) -> t2 + | _ -> t2 in + if Stack.is_empty sk2 then remove_lambda t2 else t2 in try match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 86d2cc78e0..5a8ac32ffa 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -104,9 +104,8 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with let cast_type_eq eq t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> eq t1 t2 | CastVM t1, CastVM t2 -> eq t1 t2 - | CastCoerce, CastCoerce -> true | CastNative t1, CastNative t2 -> eq t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + | (CastConv _ | CastVM _ | CastNative _), _ -> false let matching_var_kind_eq k1 k2 = match k1, k2 with | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 @@ -188,14 +187,12 @@ let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce | CastNative a -> CastNative (f a) let smartmap_cast_type f c = match c with | CastConv a -> let a' = f a in if a' == a then c else CastConv a' | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce | CastNative a -> let a' = f a in if a' == a then c else CastNative a' let map_glob_constr_left_to_right f = DAst.map (function @@ -275,7 +272,7 @@ let fold_glob_constr f acc = DAst.with_val (function Array.fold_left f (Array.fold_left f acc tyl) bv | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f acc t in f acc c | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc @@ -318,7 +315,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function Array.fold_left_i f' acc idl | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f v acc t in f v acc c | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 9f93e5e6c1..d480c12834 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -57,7 +57,6 @@ and glob_fix_kind = type 'a cast_type = | CastConv of 'a | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) | CastNative of 'a (** The kind of patterns that occurs in "match ... with ... end" diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 21b2137f09..4c2fc26b45 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1166,9 +1166,6 @@ struct let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = match k with - | CastCoerce -> - let sigma, cj = pretype empty_tycon env sigma c in - Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in diff --git a/pretyping/structures.ml b/pretyping/structures.ml index 3ef6e98373..145663d3b9 100644 --- a/pretyping/structures.ml +++ b/pretyping/structures.ml @@ -161,6 +161,7 @@ let rec of_constr env t = let patt, n, args = of_constr env f in patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] + | Lambda (_, _, b) -> let patt, _, _ = of_constr env b in patt, None, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] @@ -222,6 +223,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let lpj = keep_true_projections lpj in let nenv = Termops.push_rels_assum sign env in List.fold_left2 (fun acc (spopt, canonical) t -> + let t = EConstr.Unsafe.to_constr (shrink_eta env (EConstr.of_constr t)) in if canonical then Option.cata (fun proji_sp -> diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4c410c3170..e08a494c2e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -673,8 +673,7 @@ let tag_var = tag Tag.variable match b with | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b - | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b - | CastCoerce -> str ":>"), + | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b), lcast ) | CNotation (_,(_,"( _ )"),([t],[],[],[])) -> diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 9bf765717f..804fbdea85 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -91,7 +91,7 @@ let tokenize_string s = But I don't understand how it's used--it looks like things get appended to it but it never gets cleared. *) let rec stream_tok acc str = - let e = Stream.next str in + let e = LStream.next str in if Tok.(equal e EOI) then List.rev acc else @@ -101,7 +101,7 @@ let tokenize_string s = try let istr = Stream.of_string s in let lex = CLexer.LexerDiff.tok_func istr in - let toks = stream_tok [] (fst lex) in + let toks = stream_tok [] lex in CLexer.Lexer.State.set st; toks with exn -> @@ -529,7 +529,6 @@ let match_goals ot nt = | CastVM a, CastVM a2 | CastNative a, CastNative a2 -> constr_expr ogname a a2 - | CastCoerce, CastCoerce -> () | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)")) | CNotation (_,ntn,args), CNotation (_,ntn2,args2) -> constr_notation_substitution ogname args args2 diff --git a/tactics/equality.ml b/tactics/equality.ml index 633b9da053..497ce4ae1a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -379,11 +379,10 @@ let find_elim hdcncl lft2rgt dep cls ot = let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - try - let _ = Global.lookup_constant c1' in c1' - with Not_found -> + if not (Environ.mem_constant c1' (Global.env ())) then user_err ~hdr:"Equality.find_elim" - (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") + (str "Cannot find rewrite principle " ++ Label.print l' ++ str "."); + c1' end | _ -> begin match if is_eq then eq_elimination_ref false sort else None with diff --git a/test-suite/Makefile b/test-suite/Makefile index 2a2f62e23f..f06439a863 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -517,6 +517,17 @@ approve-output: output output-coqtop output-coqchk echo "Updated $${f%.real}!"; \ done +approve-coqdoc: coqdoc + $(HIDE)(cd coqdoc; \ + for f in *.html.out; do \ + cp "Coqdoc.$${f%.out}" "$$f"; \ + echo "Updated $$f!"; \ + done; \ + for f in *.tex.out; do \ + cat "Coqdoc.$${f%.out}" | grep -v "^%%" > "$$f"; \ + echo "Updated $$f!"; \ + done) + # the expected output for the MExtraction test is # /plugins/micromega/micromega.ml except with additional newline output/MExtraction.out: ../plugins/micromega/micromega.ml diff --git a/test-suite/bugs/closed/bug_11866.v b/test-suite/bugs/closed/bug_11866.v new file mode 100644 index 0000000000..5a47f3833e --- /dev/null +++ b/test-suite/bugs/closed/bug_11866.v @@ -0,0 +1,43 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Notation "ex0" x(tactic(0)) := (). +Ltac2 Notation "ex1" x(tactic(1)) := (). +Ltac2 Notation "ex2" x(tactic(2)) := (). +Ltac2 Notation "ex3" x(tactic(3)) := (). +Ltac2 Notation "ex4" x(tactic(4)) := (). +Ltac2 Notation "ex5" x(tactic(5)) := (). +Ltac2 Notation "ex6" x(tactic(6)) := (). + +Ltac2 Notation ":::0" x(tactic) "+0" y(tactic) : 0 := (). +Ltac2 Notation ":::1" x(tactic) "+1" y(tactic) : 1 := (). +Ltac2 Notation ":::2" x(tactic) "+2" y(tactic) : 2 := (). +Ltac2 Notation ":::3" x(tactic) "+3" y(tactic) : 3 := (). +Ltac2 Notation ":::4" x(tactic) "+4" y(tactic) : 4 := (). +Ltac2 Notation ":::5" x(tactic) "+5" y(tactic) : 5 := (). +Ltac2 Notation ":::6" x(tactic) "+6" y(tactic) : 6 := (). +Fail Ltac2 Notation ":::7" x(tactic) "+7" y(tactic) : 7 := (). +Goal True. + ex0 :::0 0 +0 0. + ex1 :::0 0 +0 0. + (*ex2 :::0 0 +0 0.*) (* fails with an anomaly, cf COQBUG(https://github.com/coq/coq/issues/12807) *) + (*ex3 :::0 0 +0 0.*) + ex4 :::0 0 +0 0. + ex5 :::0 0 +0 0. + ex6 :::0 0 +0 0. + + ex0 :::1 0 +1 0. + ex1 :::1 0 +1 0. + (*ex2 :::1 0 +1 0.*) + (*ex3 :::1 0 +1 0.*) + ex4 :::1 0 +1 0. + ex5 :::1 0 +1 0. + ex6 :::1 0 +1 0. + + ex0 :::6 0 +6 0. + ex1 :::6 0 +6 0. + (*ex2 :::6 0 +6 0.*) + (*ex3 :::6 0 +6 0.*) + ex4 :::6 0 +6 0. + ex5 :::6 0 +6 0. + ex6 :::6 0 +6 0. +Abort. diff --git a/test-suite/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v new file mode 100644 index 0000000000..611464458e --- /dev/null +++ b/test-suite/bugs/closed/bug_14131.v @@ -0,0 +1,19 @@ +Set Implicit Arguments. +Unset Elimination Schemes. + +Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := + JMeq_refl : JMeq x x. + +Set Elimination Schemes. + +Register JMeq as core.JMeq.type. + +Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq x y -> P y. + +Register JMeq_ind as core.JMeq.ind. + +Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq y x -> P y. +Proof. intros. try rewrite H0. +Abort. diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v index 6ff394bca6..8d7d97d7aa 100644 --- a/test-suite/bugs/closed/bug_3468.v +++ b/test-suite/bugs/closed/bug_3468.v @@ -26,4 +26,5 @@ Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope. Definition test := (& (@4))%my. (* Check inconsistent scopes *) +Set Warnings "+inconsistent-scopes". Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing). diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out index a70f8ca45a..23119bab97 100644 --- a/test-suite/output/Warnings.out +++ b/test-suite/output/Warnings.out @@ -1,3 +1,4 @@ File "stdin", line 4, characters 0-22: -Warning: Projection value has no head constant: fun x : B => x in canonical -instance a of b, ignoring it. [projection-no-head-constant,typechecker] +Warning: Projection value has no head constant: forall x : nat, x > 0 in +canonical instance a of b, ignoring it. +[projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 7465442cab..ce92bcbbb2 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -Record A := { B:Type; b:B->B }. -Definition a B := {| B:=B; b:=fun x => x |}. +Record A := { B:Type; b:Prop }. +Definition a B := {| B:=B; b:=forall x, x > 0 |}. Canonical Structure a. diff --git a/test-suite/output/notation_principal_scope.out b/test-suite/output/notation_principal_scope.out new file mode 100644 index 0000000000..5ccee259b0 --- /dev/null +++ b/test-suite/output/notation_principal_scope.out @@ -0,0 +1,20 @@ +The command has indeed failed with message: +Argument X was previously inferred to be in scope function_scope but is here +used in the empty scope stack. Scope function_scope will be used at parsing +time unless you override it by annotating the argument with an explicit scope +of choice. [inconsistent-scopes,syntax] +The command has indeed failed with message: +Simple notations don't support only printing +The command has indeed failed with message: +The reference nonexisting was not found in the current environment. +The command has indeed failed with message: +Notation scope for argument X can be specified only once. +pp I + : True /\ True +The command has indeed failed with message: +Illegal application (Non-functional construction): +The expression "I" of type "True" cannot be applied to the term + "I" : "True" +File "stdin", line 21, characters 0-50: +Warning: This notation will not be used for printing as it is bound to a +single variable. [notation-bound-to-variable,parsing] diff --git a/test-suite/output/notation_principal_scope.v b/test-suite/output/notation_principal_scope.v new file mode 100644 index 0000000000..6bd911501d --- /dev/null +++ b/test-suite/output/notation_principal_scope.v @@ -0,0 +1,23 @@ +Arguments conj {_ _} _ _%function. + +Set Warnings "+inconsistent-scopes". +Fail Notation pp X := (conj X X). + +Fail Notation pp := 1 (only printing). + +Fail Notation pp X := nonexisting. + +Fail Notation pp X := (conj X X) (X, X in scope nat_scope). + +Notation pp X := (conj X X) (X in scope nat_scope). + +Notation "$" := I (only parsing) : nat_scope. +Notation "$" := (I I) (only parsing) : bool_scope. + +Open Scope bool_scope. +Check pp $. +Fail Check pp (id $). + +Notation pp1 X := (X%nat) (X in scope bool_scope). +Notation pp2 X := ((X + X)%type) (X in scope bool_scope). +Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope). diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index 88702a6e80..a833dd0bd6 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -70,3 +70,35 @@ Section W. Check (refl_equal _ : l _ = x2). End W. Fail Check (refl_equal _ : l _ = x2). + +(* Lambda keys *) +Section L1. + Structure cs_lambda := { cs_lambda_key : nat -> nat }. + #[local] Canonical Structure cs_lambda_func := + {| cs_lambda_key := fun x => x + 1 |}. + Check (refl_equal _ : cs_lambda_key _ = fun _ => _ + _). +End L1. + +Section L2. + #[local] Canonical Structure cs_lambda_func2 := + {| cs_lambda_key := fun x => 1 + x |}. + Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x). +End L2. + +Section L3. + #[local] Canonical Structure cs_lambda_func3 := + {| cs_lambda_key := fun x => 1 + x |}. + Check (refl_equal _ : cs_lambda_key _ = Nat.add 1). +End L3. + +Section L4. + #[local] Canonical Structure cs_lambda_func4 := + {| cs_lambda_key := Nat.add 1 |}. + Check (refl_equal _ : cs_lambda_key _ = Nat.add 1). +End L4. + +Section L5. + #[local] Canonical Structure cs_lambda_func5 := + {| cs_lambda_key := Nat.add 1 |}. + Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x). +End L5. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index a1a4da6f37..575d773c77 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -43,7 +43,7 @@ Class EqDec A R {equiv : Equivalence R} := take precedence of [==] defined in the type scope, hence we can have both at the same time. *) -Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. +Notation " x == y " := (equiv_dec x y) (no associativity, at level 70) : equiv_scope. Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index f4220e3aa1..435dacbd4c 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -42,7 +42,7 @@ Class EqDec `(S : Setoid A) := take precedence of [==] defined in the type scope, hence we can have both at the same time. *) -Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70). +Notation " x == y " := (equiv_dec x y) (no associativity, at level 70). Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index b2bdd8099a..717e3191ea 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -33,8 +33,6 @@ Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scop (** Coerces objects to their support before comparing them. *) -Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope. - Require Import Coq.Bool.Sumbool. (** Construct a dependent disjunction from a boolean. *) diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index d8eb005ab2..72e6e757d3 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -297,7 +297,6 @@ Require Import ssreflect ssrfun. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Set Warnings "-projection-no-head-constant". Notation reflect := Bool.reflect. Notation ReflectT := Bool.ReflectT. @@ -1227,7 +1226,9 @@ Definition clone_pred T U := Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ id) : form_scope. Canonical predPredType T := PredType (@id (pred T)). +Set Warnings "-redundant-canonical-projection". Canonical boolfunPredType T := PredType (@id (T -> bool)). +Set Warnings "redundant-canonical-projection". (** The type of abstract collective predicates. While {pred T} is contertible to pred T, it presents the pred_sort coercion diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4faecd2e62..0265c0063c 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -242,12 +242,12 @@ let set_prompt prompt = (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot tok st = match Stream.next st with + let rec dot st = match LStream.next st with | Tok.KEYWORD ("."|"...") -> () | Tok.EOI -> () - | _ -> dot tok st + | _ -> dot st in - Pcoq.Entry.of_parser "Coqtoplevel.dot" dot + Pcoq.Entry.(of_parser "Coqtoplevel.dot" { parser_fun = dot }) (* If an error occurred while parsing, we try to read the input until a dot token is encountered. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92e664d56b..917acfad51 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -88,7 +88,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in let in_pa = - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file)) + Pcoq.Parsable.make ~source:(Loc.InFile file) (Stream.of_channel in_chan) in let open State in diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v index 624097728e..b201574808 100644 --- a/user-contrib/Ltac2/Bool.v +++ b/user-contrib/Ltac2/Bool.v @@ -48,7 +48,7 @@ Ltac2 xor x y := end end. -Ltac2 eq x y := +Ltac2 equal x y := match x with | true => match y with @@ -61,3 +61,6 @@ Ltac2 eq x y := | false => true end end. + +#[deprecated(note="Use Bool.equal", since="8.14")] +Ltac2 eq := equal. diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 7af530ab0f..7d17bd3d33 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -631,7 +631,7 @@ let parse_scope = ParseToken.parse_scope type synext = { synext_tok : sexpr list; synext_exp : raw_tacexpr; - synext_lev : int option; + synext_lev : int; synext_loc : bool; synext_depr : Deprecation.t option; } @@ -660,6 +660,14 @@ let deprecated_ltac2_notation = ~warning_name:"deprecated-ltac2-notation" (fun (toks : sexpr list) -> pr_sequence ParseToken.print_token toks) +(* This is a hack to preserve the level 4 entry which is initially empty. The + grammar engine has the great idea to silently delete empty levels on rule + removal, so we have to work around this using the Pcoq API. + FIXME: we should really keep those levels around instead. *) +let get_reinit = function +| 4 -> Some (Gramlib.Gramext.LeftA, Gramlib.Gramext.After "5") +| _ -> None + let perform_notation syn st = let tok = List.rev_map ParseToken.parse_token syn.synext_tok in let KRule (rule, act) = get_rule tok in @@ -675,12 +683,13 @@ let perform_notation syn st = CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp) in let rule = Pcoq.Production.make rule (act mk) in - let lev = match syn.synext_lev with - | None -> None - | Some lev -> Some (string_of_int lev) - in - let rule = (lev, None, [rule]) in - ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; data=[rule]})], st) + let pos = Some (Gramlib.Gramext.Level (string_of_int syn.synext_lev)) in + let rule = {Pcoq.pos; data = [(None, None, [rule])] } in + match get_reinit syn.synext_lev with + | None -> + ([Pcoq.ExtendRule (Pltac.ltac2_expr, rule)], st) + | Some reinit -> + ([Pcoq.ExtendRuleReinit (Pltac.ltac2_expr, reinit, rule)], st) let ltac2_notation = Pcoq.create_grammar_command "ltac2-notation" perform_notation @@ -754,7 +763,15 @@ let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, le let ids = List.fold_left fold Id.Set.empty entries in (* Globalize so that names are absolute *) let body = Tac2intern.globalize ids body in - let lev = match lev with Some _ -> lev | None -> Some 5 in + let lev = match lev with + | Some n -> + let () = + if n < 0 || n > 6 then + user_err (str "Notation levels must range between 0 and 6") + in + n + | None -> 5 + in let ext = { synext_tok = tkn; synext_exp = body; diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index 206f4df19d..0171ddfcf8 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -468,7 +468,7 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme = let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" (fun (env, t) -> - strbrk "The following expression should have type unit but has type " ++ + strbrk "This expression should have type unit but has type " ++ pr_glbtype env t ++ str ".") let warn_redundant_clause = diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index f8a28332b1..2343ffc7e7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -52,7 +52,6 @@ let of_type = Entry.create "of_type" let section_subset_expr = Entry.create "section_subset_expr" let scope_delimiter = Entry.create "scope_delimiter" let syntax_modifiers = Entry.create "syntax_modifiers" -let only_parsing = Entry.create "only_parsing" let make_bullet s = let open Proof_bullet in @@ -1160,7 +1159,7 @@ GRAMMAR EXTEND Gram (* Grammar extensions *) GRAMMAR EXTEND Gram - GLOBAL: syntax only_parsing syntax_modifiers; + GLOBAL: syntax syntax_modifiers; syntax: [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> @@ -1181,10 +1180,9 @@ GRAMMAR EXTEND Gram modl = syntax_modifiers; sc = OPT [ ":"; sc = IDENT -> { sc } ] -> { VernacInfix ((op,modl),p,sc) } - | IDENT "Notation"; id = identref; - idl = LIST0 ident; ":="; c = constr; b = only_parsing -> - { VernacSyntacticDefinition - (id,(idl,c),{ onlyparsing = b }) } + | IDENT "Notation"; id = identref; idl = LIST0 ident; + ":="; c = constr; modl = syntax_modifiers -> + { VernacSyntacticDefinition (id,(idl,c), modl) } | IDENT "Notation"; s = lstring; ":="; c = constr; modl = syntax_modifiers; @@ -1207,10 +1205,6 @@ GRAMMAR EXTEND Gram to factorize with other "Print"-based or "Declare"-based vernac entries *) ] ] ; - only_parsing: - [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true } - | -> { false } ] ] - ; level: [ [ IDENT "level"; n = natural -> { NumLevel n } | IDENT "next"; IDENT "level" -> { NextLevel } ] ] @@ -1230,10 +1224,12 @@ GRAMMAR EXTEND Gram { begin match s1, s2 with | { CAst.v = k }, Some s -> SetFormat(k,s) | s, None -> SetFormat ("text",s) end } - | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at"; - lev = level -> { SetItemLevel (x::l,None,lev) } + | x = IDENT; ","; l = LIST1 IDENT SEP ","; v = + [ "at"; lev = level -> { fun x l -> SetItemLevel (x::l,None,lev) } + | "in"; IDENT "scope"; k = IDENT -> { fun x l -> SetItemScope(x::l,k) } ] -> { v x l } | x = IDENT; "at"; lev = level; b = OPT binder_interp -> { SetItemLevel ([x],b,lev) } + | x = IDENT; "in"; IDENT "scope"; k = IDENT -> { SetItemScope([x],k) } | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) } | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) } ] ] diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f9f65a8c30..c5bfba900c 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -862,6 +862,41 @@ let inSyntaxExtension : syntax_extension_obj -> obj = (* Interpreting user-provided modifiers *) (* XXX: We could move this to the parser itself *) + +module SyndefMods = struct + +type t = { + only_parsing : bool; + scopes : (Id.t * scope_name) list; +} + +let default = { + only_parsing = false; + scopes = []; +} + +end + +let interp_syndef_modifiers modl = let open SyndefMods in + let rec interp skipped acc = function + | [] -> List.rev skipped, acc + | SetOnlyParsing :: l -> + interp skipped { acc with only_parsing = true; } l + | SetItemScope([],_) :: l -> + interp skipped acc l + | SetItemScope(s::ids,k) :: l -> + let scopes = acc.scopes in + let id = Id.of_string s in + if List.mem_assoc id scopes then + user_err (str "Notation scope for argument " ++ str s ++ + str " can be specified only once."); + interp skipped { acc with scopes = (id,k) :: scopes } + (SetItemScope(ids,s) :: l) + | x :: l -> + interp (x :: skipped) acc l + in + interp [] default modl + module NotationMods = struct type notation_modifier = { @@ -872,7 +907,6 @@ type notation_modifier = { subtyps : (Id.t * production_level) list; (* common to syn_data below *) - only_parsing : bool; only_printing : bool; format : lstring option; extra : (string * string) list; @@ -884,7 +918,6 @@ let default = { custom = InConstrEntry; etyps = []; subtyps = []; - only_parsing = false; only_printing = false; format = None; extra = []; @@ -945,8 +978,6 @@ let interp_modifiers modl = let open NotationMods in | SetAssoc a :: l -> if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); interp subtyps { acc with assoc = Some a; } l - | SetOnlyParsing :: l -> - interp subtyps { acc with only_parsing = true; } l | SetOnlyPrinting :: l -> interp subtyps { acc with only_printing = true; } l | SetFormat ("text",s) :: l -> @@ -954,8 +985,10 @@ let interp_modifiers modl = let open NotationMods in interp subtyps { acc with format = Some s; } l | SetFormat (k,s) :: l -> interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l + | (SetOnlyParsing | SetItemScope _) :: _ -> assert false in - let subtyps,mods = interp [] default modl in + let modl, syndef_mods = interp_syndef_modifiers modl in + let subtyps, mods = interp [] default modl in (* interpret item levels wrt to main entry *) let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in (* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *) @@ -965,10 +998,10 @@ let interp_modifiers modl = let open NotationMods in if mods.custom = InConstrEntry then (warn_deprecated_ident_entry (); (id,ETName true)) else (id,ETIdent) | x -> x) mods.etyps } in - { mods with etyps = extra_etyps@mods.etyps } + syndef_mods, { mods with etyps = extra_etyps@mods.etyps } let check_infix_modifiers modifiers = - let mods = interp_modifiers modifiers in + let _, mods = interp_modifiers modifiers in let t = mods.NotationMods.etyps in let u = mods.NotationMods.subtyps in if not (List.is_empty t) || not (List.is_empty u) then @@ -1036,7 +1069,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder | ETConstr _ | ETBigint | ETGlobal - | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny + | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny None let set_internalization_type typs = List.map (fun (_, e) -> internalization_type_of_entry_type e) typs @@ -1292,23 +1325,25 @@ let check_locality_compatibility local custom i_typs = let compute_syntax_data ~local deprecation df modifiers = let open SynData in + let open SyndefMods in let open NotationMods in - let mods = interp_modifiers modifiers in - let onlyprint = mods.only_printing in - let onlyparse = mods.only_parsing in - if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); + let syndef_mods, mods = interp_modifiers modifiers in + let only_printing = mods.only_printing in + let only_parsing = syndef_mods.only_parsing in + if only_printing && only_parsing then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); + if syndef_mods.scopes <> [] then user_err (str "General notations don't support 'in scope'."); let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in - let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in + let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint:only_printing df in let _ = check_useless_entry_types recvars mainvars mods.etyps in (* Notations for interp and grammar *) - let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in + let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols only_printing in let ntn_for_interp = make_notation_key mods.custom symbols in let symbols_for_grammar = if mods.custom = InConstrEntry then remove_curly_brackets symbols else symbols in let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in let ntn_for_grammar = if need_squash then make_notation_key mods.custom symbols_for_grammar else ntn_for_interp in - if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar; + if mods.custom = InConstrEntry && not only_printing then check_rule_productivity symbols_for_grammar; (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = @@ -1329,8 +1364,8 @@ let compute_syntax_data ~local deprecation df modifiers = (* Return relevant data for interpretation and for parsing/printing *) { info = i_data; - only_parsing = mods.only_parsing; - only_printing = mods.only_printing; + only_parsing; + only_printing; deprecation; format = mods.format; extra = mods.extra; @@ -1793,11 +1828,18 @@ let remove_delimiters local scope = let add_class_scope local scope cl = Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) -let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } = +let add_syntactic_definition ~local deprecation env ident (vars,c) modl = + let open SyndefMods in + let skipped, { only_parsing; scopes } = interp_syndef_modifiers modl in + if skipped <> [] then + user_err (str "Simple notations don't support " ++ Ppvernac.pr_syntax_modifier (List.hd skipped)); + let vars = List.map (fun v -> v, List.assoc_opt v scopes) vars in let acvars,pat,reversibility = - try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible - with Not_found -> - let fold accu id = Id.Map.add id NtnInternTypeAny accu in + match vars, intern_name_alias c with + | [], Some(r,u) -> + Id.Map.empty, NRef(r, u), APrioriReversible + | _ -> + let fold accu (id,scope) = Id.Map.add id (NtnInternTypeAny scope) accu in let i_vars = List.fold_left fold Id.Map.empty vars in let nenv = { ninterp_var_type = i_vars; @@ -1805,11 +1847,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } in interp_notation_constr env nenv c in - let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in + let in_pat (id,_) = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in let interp = make_interpretation_vars ~default_if_binding:AsNameOrPattern [] 0 acvars (List.map in_pat vars) in - let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in + let vars = List.map (fun (x,_) -> (x, Id.Map.find x interp)) vars in let also_in_cases_pattern = has_no_binders_type vars in - let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in + let onlyparsing = only_parsing || fst (printability None [] false reversibility pat) in Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index dd71817083..3ece04f5f9 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -52,7 +52,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : local:bool -> Deprecation.t option -> env -> - Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit + Id.t -> Id.t list * constr_expr -> syntax_modifier list -> unit (** Print the Camlp5 state of a grammar *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8e5942440b..be34c563c8 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -468,6 +468,8 @@ let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++ pr_opt pr_constr_as_binder_kind bko + | SetItemScope (l,s) -> + prlist_with_sep sep_v2 str l ++ spc () ++ str"in scope" ++ str s | SetLevel n -> pr_at_level (NumLevel n) | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n)) | SetAssoc LeftA -> keyword "left associativity" @@ -484,9 +486,6 @@ let pr_syntax_modifiers = function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") -let pr_only_parsing_clause onlyparsing = - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []) - let pr_decl_notation prc decl_ntn = let open Vernacexpr in let @@ -1098,12 +1097,12 @@ let pr_vernac_expr v = ) | VernacHints (dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) -> + | VernacSyntacticDefinition (id,(ids,c),l) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ - pr_only_parsing_clause onlyparsing) + pr_syntax_modifiers l) ) | VernacArguments (q, args, more_implicits, mods) -> return ( diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index 9339803948..d36e61864d 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -13,6 +13,8 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t +val pr_syntax_modifier : Vernacexpr.syntax_modifier -> Pp.t + (** Prints a fixpoint body *) val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index a7de34dd09..bf0874c8e5 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -66,8 +66,8 @@ module Vernac_ = | Some ename -> find_proof_mode ename let command_entry = - Pcoq.Entry.of_parser "command_entry" - (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) + Pcoq.Entry.(of_parser "command_entry" + { parser_fun = (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) }) end diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 46acaf7264..9757783d09 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -114,10 +114,6 @@ type import_filter_expr = | ImportAll | ImportNames of one_import_filter_name list -type onlyparsing_flag = { onlyparsing : bool } - (* Some v = Parse only; None = Print also. - If v<>Current, it contains the name of the coq version - which this notation is trying to be compatible with *) type locality_flag = bool (* true = Local *) type option_setting = @@ -135,6 +131,7 @@ type definition_expr = type syntax_modifier = | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level + | SetItemScope of string list * scope_name | SetLevel of int | SetCustomEntry of string * int option | SetAssoc of Gramlib.Gramext.g_assoc @@ -411,8 +408,7 @@ type nonrec vernac_expr = | VernacRemoveHints of string list * qualid list | VernacHints of string list * hints_expr | VernacSyntacticDefinition of - lident * (Id.t list * constr_expr) * - onlyparsing_flag + lident * (Id.t list * constr_expr) * syntax_modifier list | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 4098401bf0..84f4421c2e 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -186,7 +186,7 @@ and vernac_load ~verbosely fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = Util.open_utf8_file_in longfname in - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in + Pcoq.Parsable.make ~source:(Loc.InFile longfname) (Stream.of_channel in_chan) in (* Parsing loop *) let v_mod = if verbosely then Flags.verbosely else Flags.silently in let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing |