From 35a84b3077c219fb5f11c580a5ec405a889c0a4b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 8 Sep 2020 11:53:42 +0200 Subject: [refman] Replace num by int num stands for natural numbers whereas the text deals with negative values. --- doc/sphinx/proof-engine/tactics.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 99888cbe1d..ed5de95212 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4737,12 +4737,12 @@ Non-logical tactics ------------------------ -.. tacn:: cycle @num +.. tacn:: cycle @int :name: cycle - Reorders the selected goals so that the first :n:`@num` goals appear after the + Reorders the selected goals so that the first :n:`@int` goals appear after the other selected goals. - If :n:`@num` is negative, it puts the last :n:`@num` goals at the + If :n:`@int` is negative, it puts the last :n:`@int` goals at the beginning of the list. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent @@ -4761,11 +4761,11 @@ Non-logical tactics all: cycle 2. all: cycle -3. -.. tacn:: swap @num @num +.. tacn:: swap @int @int :name: swap Exchanges the position of the specified goals. - Negative values for :n:`@num` indicate counting goals + Negative values for :n:`@int` indicate counting goals backward from the end of the list of selected goals. Goals are indexed from 1. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent -- cgit v1.2.3 From b4d11894fd676ec53e4fdf860d32173a778242c5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:02:00 +0200 Subject: [parsing] Rename token NUMERAL to NUMBER --- coqpp/coqpp_main.ml | 4 ++-- doc/tools/docgram/common.edit_mlg | 8 ++++---- doc/tools/docgram/fullGrammar | 10 +++++----- parsing/cLexer.ml | 8 ++++---- parsing/g_constr.mlg | 4 ++-- parsing/g_prim.mlg | 6 +++--- parsing/pcoq.ml | 2 +- parsing/tok.ml | 22 +++++++++++----------- parsing/tok.mli | 4 ++-- plugins/ssr/ssrparser.mlg | 8 ++++---- 10 files changed, 38 insertions(+), 38 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 2735c5b5eb..5e3199e8a6 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -201,8 +201,8 @@ function | "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s | "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s | "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s -| "NUMERAL", None -> fprintf fmt "Tok.PNUMERAL None" -| "NUMERAL", Some s -> fprintf fmt "Tok.PNUMERAL (Some (NumTok.Unsigned.of_string %a))" print_string s +| "NUMBER", None -> fprintf fmt "Tok.PNUMBER None" +| "NUMBER", Some s -> fprintf fmt "Tok.PNUMBER (Some (NumTok.Unsigned.of_string %a))" print_string s | "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s | "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK" | "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 9971a03894..a619089cdd 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -300,7 +300,7 @@ term_let: [ atomic_constr: [ | MOVETO qualid_annotated global univ_instance -| MOVETO primitive_notations NUMERAL +| MOVETO primitive_notations NUMBER | MOVETO primitive_notations string | MOVETO term_evar "_" | REPLACE "?" "[" ident "]" @@ -780,7 +780,7 @@ numeral: [ ] bigint: [ -| DELETE NUMERAL +| DELETE NUMBER | num ] @@ -797,7 +797,7 @@ ident: [ | first_letter LIST0 subsequent_letter ] -NUMERAL: [ +NUMBER: [ | numeral ] @@ -2210,7 +2210,7 @@ SPLICE: [ | IDENT | LEFTQMARK | natural -| NUMERAL +| NUMBER | STRING | hyp | var diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index f628c86cf1..f82f196b36 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -162,7 +162,7 @@ appl_arg: [ atomic_constr: [ | global univ_instance | sort -| NUMERAL +| NUMBER | string | "_" | "?" "[" ident "]" @@ -283,7 +283,7 @@ pattern0: [ | "_" | "(" pattern200 ")" | "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" -| NUMERAL +| NUMBER | string ] @@ -440,12 +440,12 @@ natural: [ ] bigint: [ -| NUMERAL -| test_minus_nat "-" NUMERAL +| NUMBER +| test_minus_nat "-" NUMBER ] bignat: [ -| NUMERAL +| NUMBER ] bar_cbrace: [ diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index 85640cabba..a98cf3b7de 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -710,7 +710,7 @@ let rec next_token ~diff_mode loc s = let n = NumTok.Unsigned.parse s in let ep = Stream.count s in comment_stop bp; - (NUMERAL n, set_loc_pos loc bp ep) + (NUMBER n, set_loc_pos loc bp ep) | Some '\"' -> Stream.junk s; let (loc, len) = @@ -796,8 +796,8 @@ let token_text : type c. c Tok.p -> string = function | PKEYWORD t -> "'" ^ t ^ "'" | PIDENT None -> "identifier" | PIDENT (Some t) -> "'" ^ t ^ "'" - | PNUMERAL None -> "numeral" - | PNUMERAL (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'" + | PNUMBER None -> "numeral" + | PNUMBER (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'" | PSTRING None -> "string" | PSTRING (Some s) -> "STRING \"" ^ s ^ "\"" | PLEFTQMARK -> "LEFTQMARK" @@ -891,5 +891,5 @@ let terminal s = (* Precondition: the input is a numeral (c.f. [NumTok.t]) *) let terminal_numeral s = match NumTok.Unsigned.parse_string s with - | Some n -> PNUMERAL (Some n) + | Some n -> PNUMBER (Some n) | None -> failwith "numeral token expected." diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 61317f3ef2..1ec83c496a 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -258,7 +258,7 @@ GRAMMAR EXTEND Gram atomic_constr: [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) } | s = sort -> { CAst.make ~loc @@ CSort s } - | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } + | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } @@ -370,7 +370,7 @@ GRAMMAR EXTEND Gram | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } - | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) } + | n = NUMBER-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] ; fixannot: diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index cc59b2175b..044758f11a 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -127,11 +127,11 @@ GRAMMAR EXTEND Gram [ [ i = bignat -> { my_int_of_string ~loc i } ] ] ; bigint: - [ [ i = NUMERAL -> { my_to_nat_string true ~loc i } - | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ] + [ [ i = NUMBER -> { my_to_nat_string true ~loc i } + | test_minus_nat; "-"; i = NUMBER -> { "-" ^ my_to_nat_string ~loc false i } ] ] ; bignat: - [ [ i = NUMERAL -> { my_to_nat_string ~loc true i } ] ] + [ [ i = NUMBER -> { my_to_nat_string ~loc true i } ] ] ; bar_cbrace: [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 2cc16f85d5..b9853029a0 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -64,7 +64,7 @@ struct | _ -> None let lk_nat tok n strm = match stream_nth n strm with - | Tok.NUMERAL p when NumTok.Unsigned.is_nat p -> Some (n + 1) + | Tok.NUMBER p when NumTok.Unsigned.is_nat p -> Some (n + 1) | _ -> None let rec lk_list lk_elem n strm = diff --git a/parsing/tok.ml b/parsing/tok.ml index b1ceab8822..1ab7847805 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -17,7 +17,7 @@ type 'c p = | PPATTERNIDENT : string option -> string p | PIDENT : string option -> string p | PFIELD : string option -> string p - | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p + | PNUMBER : NumTok.Unsigned.t option -> NumTok.Unsigned.t p | PSTRING : string option -> string p | PLEFTQMARK : unit p | PBULLET : string option -> string p @@ -30,8 +30,8 @@ let pattern_strings : type c. c p -> string * string option = | PPATTERNIDENT s -> "PATTERNIDENT", s | PIDENT s -> "IDENT", s | PFIELD s -> "FIELD", s - | PNUMERAL None -> "NUMERAL", None - | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.Unsigned.sprint n) + | PNUMBER None -> "NUMBER", None + | PNUMBER (Some n) -> "NUMBER", Some (NumTok.Unsigned.sprint n) | PSTRING s -> "STRING", s | PLEFTQMARK -> "LEFTQMARK", None | PBULLET s -> "BULLET", s @@ -43,7 +43,7 @@ type t = | PATTERNIDENT of string | IDENT of string | FIELD of string - | NUMERAL of NumTok.Unsigned.t + | NUMBER of NumTok.Unsigned.t | STRING of string | LEFTQMARK | BULLET of string @@ -58,8 +58,8 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option = | PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl - | PNUMERAL None, PNUMERAL None -> Some Util.Refl - | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl + | PNUMBER None, PNUMBER None -> Some Util.Refl + | PNUMBER (Some n1), PNUMBER (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl | PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl | PLEFTQMARK, PLEFTQMARK -> Some Util.Refl | PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl @@ -73,7 +73,7 @@ let equal t1 t2 = match t1, t2 with | PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2 | IDENT s1, IDENT s2 -> string_equal s1 s2 | FIELD s1, FIELD s2 -> string_equal s1 s2 -| NUMERAL n1, NUMERAL n2 -> NumTok.Unsigned.equal n1 n2 +| NUMBER n1, NUMBER n2 -> NumTok.Unsigned.equal n1 n2 | STRING s1, STRING s2 -> string_equal s1 s2 | LEFTQMARK, LEFTQMARK -> true | BULLET s1, BULLET s2 -> string_equal s1 s2 @@ -100,7 +100,7 @@ let extract_string diff_mode = function else s | PATTERNIDENT s -> s | FIELD s -> if diff_mode then "." ^ s else s - | NUMERAL n -> NumTok.Unsigned.sprint n + | NUMBER n -> NumTok.Unsigned.sprint n | LEFTQMARK -> "?" | BULLET s -> s | QUOTATION(_,s) -> s @@ -124,15 +124,15 @@ let match_pattern (type c) (p : c p) : t -> c = let err () = raise Stream.Failure in let seq = string_equal in match p with - | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ()) + | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMBER n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ()) | PIDENT None -> (function IDENT s' -> s' | _ -> err ()) | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ()) | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ()) | PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ()) | PFIELD None -> (function FIELD s -> s | _ -> err ()) | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ()) - | PNUMERAL None -> (function NUMERAL s -> s | _ -> err ()) - | PNUMERAL (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMERAL n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ()) + | PNUMBER None -> (function NUMBER s -> s | _ -> err ()) + | PNUMBER (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMBER n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ()) | PSTRING None -> (function STRING s -> s | _ -> err ()) | PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ()) | PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ()) diff --git a/parsing/tok.mli b/parsing/tok.mli index b556194eb3..5bbb7a0013 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -15,7 +15,7 @@ type 'c p = | PPATTERNIDENT : string option -> string p | PIDENT : string option -> string p | PFIELD : string option -> string p - | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p + | PNUMBER : NumTok.Unsigned.t option -> NumTok.Unsigned.t p | PSTRING : string option -> string p | PLEFTQMARK : unit p | PBULLET : string option -> string p @@ -29,7 +29,7 @@ type t = | PATTERNIDENT of string | IDENT of string | FIELD of string - | NUMERAL of NumTok.Unsigned.t + | NUMBER of NumTok.Unsigned.t | STRING of string | LEFTQMARK | BULLET of string diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 60af804c1b..98439e27a1 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "/" -> (match Util.stream_nth 1 strm with - | Tok.NUMERAL _ when b1 -> + | Tok.NUMBER _ when b1 -> (match Util.stream_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 - | Tok.NUMERAL _ -> () + | Tok.NUMBER _ -> () | _ -> raise Stream.Failure end | _ -> raise Stream.Failure) | Tok.KEYWORD "/" when not b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 3 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm = | Tok.KEYWORD "//" when not b1 -> (match Util.stream_nth 1 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) -- cgit v1.2.3 From f61d7d1139bd5f9e0efd34460e8daf68e454e46b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:06:00 +0200 Subject: [parsing] Simplify bigint --- doc/tools/docgram/common.edit_mlg | 5 +++-- doc/tools/docgram/fullGrammar | 4 ++-- parsing/g_prim.mlg | 13 ++++++------- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a619089cdd..549ace5d13 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -780,8 +780,9 @@ numeral: [ ] bigint: [ -| DELETE NUMBER -| num +| DELETE bignat +| REPLACE test_minus_nat "-" bignat +| WITH OPT "-" bignat ] first_letter: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index f82f196b36..73b721702e 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -440,8 +440,8 @@ natural: [ ] bigint: [ -| NUMBER -| test_minus_nat "-" NUMBER +| bignat +| test_minus_nat "-" bignat ] bignat: [ diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 044758f11a..270662b824 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -23,12 +23,11 @@ let my_int_of_string ?loc s = with Failure _ -> CErrors.user_err ?loc (Pp.str "This number is too large.") -let my_to_nat_string ?loc ispos s = +let my_to_nat_string ?loc s = match NumTok.Unsigned.to_nat s with | Some n -> n | None -> - let pos = if ispos then "a natural" else "an integer" in - CErrors.user_err ?loc Pp.(str "This number is not " ++ str pos ++ str " number.") + CErrors.user_err ?loc Pp.(str "This number is not an integer.") let test_pipe_closedcurly = let open Pcoq.Lookahead in @@ -127,12 +126,12 @@ GRAMMAR EXTEND Gram [ [ i = bignat -> { my_int_of_string ~loc i } ] ] ; bigint: - [ [ i = NUMBER -> { my_to_nat_string true ~loc i } - | test_minus_nat; "-"; i = NUMBER -> { "-" ^ my_to_nat_string ~loc false i } ] ] + [ [ i = bignat -> { i } + | test_minus_nat; "-"; i = bignat -> { "-" ^ i } ] ] ; bignat: - [ [ i = NUMBER -> { my_to_nat_string ~loc true i } ] ] - ; + [ [ i = NUMBER -> { my_to_nat_string ~loc i } ] ] + ; bar_cbrace: [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] ; -- cgit v1.2.3 From 46b9480a717d5ca78e354fa843f39eed87cb7b15 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:08:00 +0200 Subject: [refman] Rename num to natural --- doc/sphinx/README.rst | 20 +-- doc/sphinx/README.template.rst | 14 +- doc/sphinx/addendum/extraction.rst | 4 +- doc/sphinx/addendum/nsatz.rst | 2 +- doc/sphinx/addendum/program.rst | 4 +- doc/sphinx/addendum/type-classes.rst | 22 +-- doc/sphinx/language/core/assumptions.rst | 2 +- doc/sphinx/language/core/basic.rst | 16 +- doc/sphinx/language/core/modules.rst | 2 +- doc/sphinx/language/core/records.rst | 2 +- doc/sphinx/language/core/sorts.rst | 2 +- doc/sphinx/language/core/variants.rst | 2 +- doc/sphinx/language/extensions/match.rst | 6 +- doc/sphinx/proof-engine/ltac.rst | 32 ++-- doc/sphinx/proof-engine/ltac2.rst | 10 +- doc/sphinx/proof-engine/proof-handling.rst | 26 ++-- .../proof-engine/ssreflect-proof-language.rst | 48 +++--- doc/sphinx/proof-engine/tactics.rst | 170 ++++++++++----------- doc/sphinx/proof-engine/vernacular-commands.rst | 32 ++-- doc/sphinx/user-extensions/syntax-extensions.rst | 20 +-- doc/sphinx/using/libraries/funind.rst | 8 +- doc/tools/coqrst/coqdomain.py | 6 +- doc/tools/docgram/common.edit_mlg | 27 ++-- doc/tools/docgram/orderedGrammar | 112 +++++++------- 24 files changed, 292 insertions(+), 297 deletions(-) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index d799ecfe83..4461ff9240 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -15,10 +15,10 @@ Coq objects Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: - .. tacv:: simpl @pattern at {+ @num} + .. tacv:: simpl @pattern at {+ @natural} :name: simpl_at - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies ``simpl`` only to the :n:`{+ @natural}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences @@ -46,10 +46,10 @@ Most objects should have a body (i.e. a block of indented text following the sig Notations --------- -The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g `_): +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @natural {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``natural``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g `_): ``@…`` - A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + A placeholder (``@ident``, ``@natural``, ``@tactic``\ …) ``{? …}`` an optional block @@ -80,9 +80,9 @@ As an exercise, what do the following patterns mean? .. code:: - pattern {+, @term {? at {+ @num}}} - generalize {+, @term at {+ @num} as @ident} - fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + pattern {+, @term {? at {+ @natural}}} + generalize {+, @term at {+ @natural} as @ident} + fix @ident @natural with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} Objects ------- @@ -141,7 +141,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica ``.. opt::`` :black_nib: A Coq option (a setting with non-boolean value, e.g. a string or numeric value). Example:: - .. opt:: Hyps Limit @num + .. opt:: Hyps Limit @natural :name Hyps Limit Controls the maximum number of hypotheses displayed in goals after @@ -157,7 +157,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Example:: - .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } } term += let: @pattern := @term in @term | second_production @@ -178,7 +178,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: - .. tacn:: do @num @expr + .. tacn:: do @natural @expr :token:`expr` is evaluated to ``v`` which must be a tactic value. … diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 5762967c36..b4e21aa14a 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -15,10 +15,10 @@ Coq objects Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: - .. tacv:: simpl @pattern at {+ @num} + .. tacv:: simpl @pattern at {+ @natural} :name: simpl_at - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies ``simpl`` only to the :n:`{+ @natural}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences @@ -46,10 +46,10 @@ Most objects should have a body (i.e. a block of indented text following the sig Notations --------- -The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g `_): +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @natural {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``natural``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g `_): ``@…`` - A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + A placeholder (``@ident``, ``@natural``, ``@tactic``\ …) ``{? …}`` an optional block @@ -80,9 +80,9 @@ As an exercise, what do the following patterns mean? .. code:: - pattern {+, @term {? at {+ @num}}} - generalize {+, @term at {+ @num} as @ident} - fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + pattern {+, @term {? at {+ @natural}}} + generalize {+, @term at {+ @natural} as @ident} + fix @ident @natural with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} Objects ------- diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index ce68274036..c2249b8e57 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -429,11 +429,11 @@ Additional settings Provides a comment that is included at the beginning of the output files. -.. opt:: Extraction Flag @num +.. opt:: Extraction Flag @natural :name: Extraction Flag Controls which optimizations are used during extraction, providing a finer-grained - control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. + control than :flag:`Extraction Optimize`. The bits of :token:`natural` are used as a bit mask. Keeping an option off keeps the extracted ML more similar to the Coq term. Values are: diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ed93145622..8a64a7ed4b 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -64,7 +64,7 @@ Buchberger algorithm. This computation is done after a step of *reification*, which is performed using :ref:`typeclasses`. -.. tacv:: nsatz with radicalmax:=@num%N strategy:=@num%Z parameters:=[{*, @ident}] variables:=[{*, @ident}] +.. tacv:: nsatz with radicalmax:=@natural%N strategy:=@natural%Z parameters:=[{*, @ident}] variables:=[{*, @ident}] Most complete syntax for `nsatz`. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 3d36c5c50f..c6a4b4fe1a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -303,9 +303,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation @num {? of @ident} +.. cmd:: Obligation @natural {? of @ident} - Start the proof of obligation :token:`num`. + Start the proof of obligation :token:`natural`. .. cmd:: Next Obligation {? of @ident} diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 903aa266e2..11162ec96b 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -330,7 +330,7 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @num} := { {*; @field_def} } +.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @natural} := { {*; @field_def} } This command is used to declare a typeclass instance named :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and @@ -340,7 +340,7 @@ Summary of the commands An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for - :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number + :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number of non-dependent binders of the instance. This command supports the :attr:`global` attribute that can be @@ -362,7 +362,7 @@ Summary of the commands to fill them. It works exactly as if no body had been given and the :tacn:`refine` tactic has been used first. - .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term + .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @natural } := @term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type :n:`forall {* @binder }, @term__0 @@ -381,11 +381,11 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} {? | @num} +.. cmd:: Existing Instance {+ @ident} {? | @natural} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional - priority :token:`num`. It can be used for redeclaring instances at the end of + priority :token:`natural`. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. @@ -446,10 +446,10 @@ few other commands related to typeclasses. + When considering local hypotheses, we use the union of all the modes declared in the given databases. - .. tacv:: typeclasses eauto @num + .. tacv:: typeclasses eauto @natural .. warning:: - The semantics for the limit :n:`@num` + The semantics for the limit :n:`@natural` is different than for auto. By default, if no limit is given, the search is unbounded. Contrary to :tacn:`auto`, introduction steps are counted, which might result in larger limits being necessary when @@ -581,7 +581,7 @@ Settings Otherwise, the search strategy is depth-first search. The default is off. :cmd:`Typeclasses eauto` is another way to set this flag. -.. opt:: Typeclasses Depth @num +.. opt:: Typeclasses Depth @natural :name: Typeclasses Depth Sets the maximum proof search depth. The default is unbounded. @@ -593,7 +593,7 @@ Settings also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto` is another way to set this flag. -.. opt:: Typeclasses Debug Verbosity @num +.. opt:: Typeclasses Debug Verbosity @natural :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. @@ -604,7 +604,7 @@ Settings Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num +.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @natural :name: Typeclasses eauto This command allows more global customization of the typeclass @@ -618,5 +618,5 @@ Typeclasses eauto `:=` search (the default) or breadth-first search. The search strategy can also be set with :flag:`Typeclasses Iterative Deepening`. - + :token:`num` This sets the depth limit of the search. The depth + + :token:`natural` This sets the depth limit of the search. The depth limit can also be set with :opt:`Typeclasses Depth`. diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 955f48b772..fe10e345cd 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -125,7 +125,7 @@ has type :n:`@type`. .. _Axiom: -.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt } +.. cmd:: @assumption_token {? Inline {? ( @natural ) } } {| {+ ( @assumpt ) } | @assumpt } :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables .. insertprodn assumption_token of_type diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 1f0d696d99..63c4243921 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -115,20 +115,20 @@ Numerals Numerals are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals start with ``0x`` or ``0X``. :n:`@int` is an integer; - a numeral without fractional nor exponent parts. :n:`@num` is a non-negative + a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. .. insertprodn numeral hexdigit .. prodn:: - numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum } - | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum } - int ::= {? - } @num - num ::= {| @decnum | @hexnum } - decnum ::= @digit {* {| @digit | _ } } + numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } + | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } + int ::= {? - } @natural + natural ::= {| @decnat | @hexnat } + decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 - hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } + hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } hexdigit ::= {| 0 .. 9 | a .. f | A .. F } .. todo PR need some code fixes for hex, see PR 11948 @@ -292,7 +292,7 @@ rest of the |Coq| manual: :term:`terms ` and :term:`types .. prodn:: document ::= {* @sentence } sentence ::= {? @attributes } @command . - | {? @attributes } {? @num : } @query_command . + | {? @attributes } {? @natural : } @query_command . | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... } | @control_command diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 29e703c223..866104d5d1 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -67,7 +67,7 @@ together, as well as a means of massive abstraction. module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl ) module_type_inl ::= ! @module_type | @module_type {? @functor_app_annot } - functor_app_annot ::= [ inline at level @num ] + functor_app_annot ::= [ inline at level @natural ] | [ no inline ] module_type ::= @qualid | ( @module_type ) diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index 0080f1d052..cd44d06e67 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -19,7 +19,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. prodn:: record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } - record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @num } {? @decl_notations } + record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 3517d70005..98dd9a5426 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -20,7 +20,7 @@ Sorts | Type @%{ @universe %} universe ::= max ( {+, @universe_expr } ) | @universe_expr - universe_expr ::= @universe_name {? + @num } + universe_expr ::= @universe_name {? + @natural } The types of types are called :gdef:`sorts `. diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 8e2bf32dd6..ec8e93751c 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -22,7 +22,7 @@ Variants :attr:`universes(noncumulative)` and :attr:`private(matching)` attributes. - .. exn:: The @num th argument of @ident must be @ident in @type. + .. exn:: The @natural th argument of @ident must be @ident in @type. :undocumented: Private (matching) inductive types diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 182f599a29..c36b9deef3 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -879,7 +879,7 @@ generated expression and the original. Here is a summary of the error messages corresponding to each situation: -.. exn:: The constructor @ident expects @num arguments. +.. exn:: The constructor @ident expects @natural arguments. The variable ident is bound several times in pattern term Found a constructor of inductive type term while a constructor of term is expected @@ -890,8 +890,8 @@ situation: The pattern matching is not exhaustive. -.. exn:: The elimination predicate term should be of arity @num (for non \ - dependent case) or @num (for dependent case). +.. exn:: The elimination predicate term should be of arity @natural (for non \ + dependent case) or @natural (for dependent case). The elimination predicate provided to match has not the expected arity. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d8b2af092f..2bccfcd615 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -397,7 +397,7 @@ behavior.) `par` Applies :n:`@ltac_expr` to all focused goals in parallel. The number of workers can be controlled via the command line option - :n:`-async-proofs-tac-j @num` to specify the desired number of workers. + :n:`-async-proofs-tac-j @natural` to specify the desired number of workers. Limitations: ``par:`` only works on goals that don't contain existential variables. :n:`@ltac_expr` must either solve the goal completely or do nothing (i.e. it cannot make some progress). @@ -412,8 +412,8 @@ Selectors can also be used nested within a tactic expression with the .. prodn:: selector ::= {+, @range_selector } | [ @ident ] - range_selector ::= @num - @num - | @num + range_selector ::= @natural - @natural + | @natural Applies :token:`ltac_expr3` to the selected goals. @@ -426,10 +426,10 @@ Selectors can also be used nested within a tactic expression with the Limits the application of :token:`ltac_expr3` to the goal previously named :token:`ident` by the user (see :ref:`existential-variables`). - :n:`@num__1 - @num__2` - Selects the goals :n:`@num__1` through :n:`@num__2`, inclusive. + :n:`@natural__1 - @natural__2` + Selects the goals :n:`@natural__1` through :n:`@natural__2`, inclusive. - :n:`@num` + :n:`@natural` Selects a single goal. .. exn:: No such goal. @@ -916,7 +916,7 @@ Failing (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`, :tacn:`repeat`, or branching command is aborted and the level is decremented. In the case of :n:`+`, a nonzero level skips the first backtrack point, even if - the call to :tacn:`fail` :n:`@num` is not enclosed in a :n:`+` construct, + the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct, respecting the algebraic identity. :n:`{* {| @ident | @string | @int } }` @@ -926,7 +926,7 @@ Failing .. exn:: Tactic failure. :undocumented: - .. exn:: Tactic failure (level @num). + .. exn:: Tactic failure (level @natural). :undocumented: .. exn:: No such goal. @@ -976,7 +976,7 @@ amount of time: :name: timeout :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value - ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds + ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds if it is still running. In this case the outcome is a failure. :tacn:`timeout` is an :token:`l3_tactic`. @@ -1675,8 +1675,8 @@ Proving a subgoal as a separate lemma: abstract Does a :tacn:`solve` :n:`[ @ltac_expr2 ]` and saves the subproof as an auxiliary lemma. if :n:`@ident__name` is specified, the lemma is saved with that name; otherwise - the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @num }` where - :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`num` + the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @natural }` where + :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`natural` is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. @@ -1709,7 +1709,7 @@ Proving a subgoal as a separate lemma: abstract .. tacn:: transparent_abstract @ltac_expr3 {? using @ident } Like :tacn:`abstract`, but save the subproof in a transparent lemma with a name in - the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @num }`. + the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @natural }`. .. warning:: @@ -2197,7 +2197,7 @@ Backtraces Tracing execution ~~~~~~~~~~~~~~~~~ -.. cmd:: Info @num @ltac_expr +.. cmd:: Info @natural @ltac_expr Applies :token:`ltac_expr` and prints a trace of the tactics that were successfully applied, discarding branches that failed. @@ -2205,7 +2205,7 @@ Tracing execution This command is valid only in proof mode. It accepts :ref:`goal-selectors`. - The number :n:`@num` is the unfolding level of tactics in the trace. At level + The number :n:`@natural` is the unfolding level of tactics in the trace. At level 0, the trace contains a sequence of tactics in the actual script, at level 1, the trace will be the concatenation of the traces of these tactics, etc… @@ -2237,12 +2237,12 @@ Tracing execution position in the script. In particular, the calls to idtac in branches which failed are not printed. - .. opt:: Info Level @num + .. opt:: Info Level @natural :name: Info Level This option is an alternative to the :cmd:`Info` command. - This will automatically print the same trace as :n:`Info @num` at each + This will automatically print the same trace as :n:`Info @natural` at each tactic call. The unfolding level can be overridden by a call to the :cmd:`Info` command. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b217448711..9b8749f185 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1294,7 +1294,7 @@ workarounds through Ltac1 (described below). Two examples of syntax differences: -- There is no notation defined that's equivalent to :n:`intros until {| @ident | @num }`. There is, +- There is no notation defined that's equivalent to :n:`intros until {| @ident | @natural }`. There is, however, already an ``intros_until`` tactic function defined ``Std.v``, so it may be possible for a user to add the necessary notation. - The built-in `simpl` tactic in Ltac1 supports the use of scope keys in delta flags, e.g. :n:`simpl ["+"%nat]` @@ -1555,7 +1555,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. insertprodn ltac2_destruction_arg ltac2_constr_with_bindings .. prodn:: - ltac2_destruction_arg ::= @num + ltac2_destruction_arg ::= @natural | @lident | @ltac2_constr_with_bindings ltac2_constr_with_bindings ::= @term {? with @ltac2_bindings } @@ -1568,7 +1568,7 @@ Here is the syntax for the :n:`q_*` nonterminals: | {+ @term } ltac2_simple_binding ::= ( @qhyp := @term ) qhyp ::= $ @ident - | @num + | @natural | @lident .. insertprodn ltac2_strategy_flag ltac2_delta_flag @@ -1606,7 +1606,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. prodn:: q_occurrences ::= {? @ltac2_occs } ltac2_occs ::= at @ltac2_occs_nums - ltac2_occs_nums ::= {? - } {+ {| @num | $ @ident } } + ltac2_occs_nums ::= {? - } {+ {| @natural | $ @ident } } ltac2_concl_occ ::= * {? @ltac2_occs } ltac2_hypident_occ ::= @ltac2_hypident {? @ltac2_occs } ltac2_hypident ::= @ident_or_anti @@ -1630,7 +1630,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. prodn:: ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter - ltac2_rewriter ::= {? @num } {? {| ? | ! } } @ltac2_constr_with_bindings + ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings .. insertprodn ltac2_for_each_goal ltac2_goal_tactics diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 55e4f26fe8..f90ebadb3a 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -259,9 +259,9 @@ Name a set of section hypotheses for ``Proof using`` -.. cmd:: Existential @num := @term +.. cmd:: Existential @natural := @term - This command instantiates an existential variable. :token:`num` is an index in + This command instantiates an existential variable. :token:`natural` is an index in the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. This command is intended to be used to instantiate existential @@ -313,9 +313,9 @@ Navigation in the proof tree This command cancels the effect of the last command. Thus, it backtracks one step. -.. cmdv:: Undo @num +.. cmdv:: Undo @natural - Repeats Undo :token:`num` times. + Repeats Undo :token:`natural` times. .. cmdv:: Restart :name: Restart @@ -336,9 +336,9 @@ Navigation in the proof tree Prefer the use of bullets or focusing brackets (see below). -.. cmdv:: Focus @num +.. cmdv:: Focus @natural - This focuses the attention on the :token:`num` th subgoal to prove. + This focuses the attention on the :token:`natural` th subgoal to prove. .. deprecated:: 8.8 @@ -373,9 +373,9 @@ Navigation in the proof tree together with a suggestion about the right bullet or ``}`` to unfocus it or focus the next one. - .. cmdv:: @num: %{ + .. cmdv:: @natural: %{ - This focuses on the :token:`num`\-th subgoal to prove. + This focuses on the :token:`natural`\-th subgoal to prove. .. cmdv:: [@ident]: %{ @@ -439,7 +439,7 @@ Navigation in the proof tree You are trying to use ``}`` but the current subproof has not been fully solved. - .. exn:: No such goal (@num). + .. exn:: No such goal (@natural). :undocumented: .. exn:: No such goal (@ident). @@ -559,9 +559,9 @@ Requesting information .. exn:: No focused proof. :undocumented: - .. cmdv:: Show @num + .. cmdv:: Show @natural - Displays only the :token:`num`\-th subgoal. + Displays only the :token:`natural`\-th subgoal. .. exn:: No such goal. :undocumented: @@ -649,7 +649,7 @@ Requesting information its normalized form at the current stage of the proof, useful for debugging universe inconsistencies. - .. cmdv:: Show Goal @num at @num + .. cmdv:: Show Goal @natural at @natural :name: Show Goal This command is only available in coqtop. Displays a goal at a @@ -838,7 +838,7 @@ Controlling the effect of proof editing commands ------------------------------------------------ -.. opt:: Hyps Limit @num +.. opt:: Hyps Limit @natural :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 5a11b4f474..2d1b622a2d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -617,7 +617,7 @@ Abbreviations selected occurrences of a term. .. prodn:: - occ_switch ::= { {? {| + | - } } {* @num } } + occ_switch ::= { {? {| + | - } } {* @natural } } where: @@ -1580,7 +1580,7 @@ whose general syntax is i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } .. prodn:: - i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } + i_block ::= {| [^ @ident ] | [^~ {| @ident | @natural } ] } The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a @@ -1842,8 +1842,8 @@ Block introduction :n:`[^~ @ident ]` *block destructing* using :token:`ident` as a suffix. -:n:`[^~ @num ]` - *block destructing* using :token:`num` as a suffix. +:n:`[^~ @natural ]` + *block destructing* using :token:`natural` as a suffix. Only a :token:`s_item` is allowed between the elimination tactic and the block destructing. @@ -2236,17 +2236,17 @@ tactics to *permute* the subgoals generated by a tactic. These two equivalent tactics invert the order of the subgoals in focus. - .. tacv:: last @num first + .. tacv:: last @natural first - If :token:`num`\'s value is :math:`k`, + If :token:`natural`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the circular order of subgoals remains unchanged. - .. tacn:: first @num last + .. tacn:: first @natural last :name: first (ssreflect) - If :token:`num`\'s value is :math:`k`, + If :token:`natural`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order of subgoals remains unchanged. @@ -2319,7 +2319,7 @@ tactic should be repeated on the current subgoal. There are four kinds of multipliers: .. prodn:: - mult ::= {| @num ! | ! | @num ? | ? } + mult ::= {| @natural ! | ! | @natural ? | ? } Their meaning is: @@ -4086,7 +4086,7 @@ will generally fail to perform congruence simplification, even on rather simple cases. We therefore provide a more robust alternative in which the function is supplied: -.. tacn:: congr {? @num } @term +.. tacn:: congr {? @natural } @term :name: congr This tactic: @@ -4120,7 +4120,7 @@ which the function is supplied: Lemma test (x y z : nat) : x = y -> x = z. congr (_ = _). - The optional :token:`num` forces the number of arguments for which the + The optional :token:`natural` forces the number of arguments for which the tactic should generate equality proof obligations. This tactic supports equalities between applications with dependent @@ -5392,8 +5392,8 @@ In this context, the identity view can be used when no view has to be applied: Declaring new Hint Views ~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Hint View for move / @ident {? | @num } - Hint View for apply / @ident {? | @num } +.. cmd:: Hint View for move / @ident {? | @natural } + Hint View for apply / @ident {? | @natural } This command can be used to extend the database of hints for the view mechanism. @@ -5410,7 +5410,7 @@ Declaring new Hint Views views. The optional natural number is the number of implicit arguments to be considered for the declared hint view lemma. - .. cmdv:: Hint View for apply//@ident {? | @num } + .. cmdv:: Hint View for apply//@ident {? | @natural } This variant with a double slash ``//``, declares hint views for right hand sides of double views. @@ -5571,7 +5571,7 @@ Module name Natural number -.. prodn:: natural ::= {| @num | @ident } +.. prodn:: nat_or_ident ::= {| @natural | @ident } where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a @@ -5614,19 +5614,19 @@ view :ref:`introduction_ssr` intro block :ref:`introduction_ssr` .. prodn:: - i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } + i_block ::= {| [^ @ident ] | [^~ {| @ident | @natural } ] } intro item see :ref:`introduction_ssr` -.. prodn:: int_mult ::= {? @num } @mult_mark +.. prodn:: int_mult ::= {? @natural } @mult_mark multiplier see :ref:`iteration_ssr` -.. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } +.. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } } occur. switch see :ref:`occurrence_selection_ssr` -.. prodn:: mult ::= {? @num } @mult_mark +.. prodn:: mult ::= {? @natural } @mult_mark multiplier see :ref:`iteration_ssr` @@ -5741,7 +5741,7 @@ respectively. unlock (see :ref:`locking_ssr`) -.. tacn:: congr {? @num } @term +.. tacn:: congr {? @natural } @term congruence (see :ref:`congruence_ssr`) @@ -5765,11 +5765,11 @@ localization see :ref:`localization_ssr` iteration see :ref:`iteration_ssr` -.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] } +.. prodn:: tactic += @tactic ; {| first | last } {? @natural } {| @tactic | [ {+| @tactic } ] } selector see :ref:`selectors_ssr` -.. prodn:: tactic += @tactic ; {| first | last } {? @num } +.. prodn:: tactic += @tactic ; {| first | last } {? @natural } rotation see :ref:`selectors_ssr` @@ -5780,11 +5780,11 @@ closing see :ref:`terminators_ssr` Commands ~~~~~~~~ -.. cmd:: Hint View for {| move | apply } / @ident {? | @num } +.. cmd:: Hint View for {| move | apply } / @ident {? | @natural } view hint declaration (see :ref:`declaring_new_hints_ssr`) -.. cmd:: Hint View for apply // @ident {? @num } +.. cmd:: Hint View for apply // @ident {? @natural } right hand side double , view hint declaration (see :ref:`declaring_new_hints_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ed5de95212..de39edc8e9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -100,12 +100,12 @@ The general form of a term with a bindings list is .. prodn:: ref ::= @ident - | @num + | @natural bindings_list ::= {+ (@ref := @term) } | {+ @term } + In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an - :n:`@ident` or a :n:`@num`. The references are determined according to the type of + :n:`@ident` or a :n:`@natural`. The references are determined according to the type of :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the type of :n:`@term` and the binding provides the tactic with an instance for the parameter of this name. If :n:`@ref` is a number ``n``, it refers to @@ -484,7 +484,7 @@ following syntax: | * |- {? * {? @at_occurrences } } | * at_occurrences ::= at @occurrences - occurrences ::= {? - } {* @num } + occurrences ::= {? - } {* @natural } The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate @@ -921,11 +921,11 @@ Applying theorems This summarizes the different syntactic variants of :n:`apply @term in @ident` and :n:`eapply @term in @ident`. -.. tacn:: constructor @num +.. tacn:: constructor @natural :name: constructor This tactic applies to a goal such that its conclusion is an inductive - type (say :g:`I`). The argument :token:`num` must be less or equal to the + type (say :g:`I`). The argument :token:`natural` must be less or equal to the numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th constructor of :g:`I`, then :g:`constructor i` is equivalent to :n:`intros; apply c__i`. @@ -942,7 +942,7 @@ Applying theorems :g:`constructor n` where ``n`` is the number of constructors of the head of the goal. - .. tacv:: constructor @num with @bindings_list + .. tacv:: constructor @natural with @bindings_list Let ``c`` be the i-th constructor of :g:`I`, then :n:`constructor i with @bindings_list` is equivalent to @@ -1073,9 +1073,9 @@ Managing the local context .. exn:: No such hypothesis in current goal. :undocumented: - .. tacv:: intros until @num + .. tacv:: intros until @natural - This repeats :tacn:`intro` until the :token:`num`\-th non-dependent + This repeats :tacn:`intro` until the :token:`natural`\-th non-dependent product. .. example:: @@ -1091,7 +1091,7 @@ Managing the local context .. exn:: No such hypothesis in current goal. - This happens when :token:`num` is 0 or is greater than the number of + This happens when :token:`natural` is 0 or is greater than the number of non-dependent products of the goal. .. tacv:: intro {? @ident__1 } after @ident__2 @@ -1576,7 +1576,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term; ... ; generalize @term`. Note that the sequence of term :sub:`i` 's are processed from n to 1. -.. tacv:: generalize @term at {+ @num} +.. tacv:: generalize @term at {+ @natural} This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the @@ -1587,7 +1587,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it uses :n:`@ident` to name the generalized hypothesis. -.. tacv:: generalize {+, @term at {+ @num} as @ident} +.. tacv:: generalize {+, @term at {+ @natural} as @ident} This is the most general form of :n:`generalize` that combines the previous behaviors. @@ -1619,16 +1619,16 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. -.. tacv:: instantiate (@num := @term) +.. tacv:: instantiate (@natural := @term) This variant allows to refer to an existential variable which was not named - by the user. The :n:`@num` argument is the position of the existential variable + by the user. The :n:`@natural` argument is the position of the existential variable from right to left in the goal. Because this variant is not robust to slight changes in the goal, its use is strongly discouraged. -.. tacv:: instantiate ( @num := @term ) in @ident - instantiate ( @num := @term ) in ( value of @ident ) - instantiate ( @num := @term ) in ( type of @ident ) +.. tacv:: instantiate ( @natural := @term ) in @ident + instantiate ( @natural := @term ) in ( value of @ident ) + instantiate ( @natural := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. @@ -1728,13 +1728,13 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - .. tacv:: destruct @num + .. tacv:: destruct @natural - :n:`destruct @num` behaves as :n:`intros until @num` + :n:`destruct @natural` behaves as :n:`intros until @natural` followed by destruct applied to the last introduced hypothesis. .. note:: - For destruction of a numeral, use syntax :n:`destruct (@num)` (not + For destruction of a numeral, use syntax :n:`destruct (@natural)` (not very interesting anyway). .. tacv:: destruct @pattern @@ -1827,10 +1827,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident` is a quantified variable of the goal. -.. tacv:: simple destruct @num +.. tacv:: simple destruct @natural - This tactic behaves as :n:`intros until @num; case @ident` where :n:`@ident` - is the name given by :n:`intros until @num` to the :n:`@num` -th + This tactic behaves as :n:`intros until @natural; case @ident` where :n:`@ident` + is the name given by :n:`intros until @natural` to the :n:`@natural` -th non-dependent premise of the goal. .. tacv:: case_eq @term @@ -1861,8 +1861,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) @ident; induction @ident`. If :n:`@ident` is not anymore dependent in the goal after application of :n:`induction`, it is erased (to avoid erasure, use parentheses, as in :n:`induction (@ident)`). - + If :n:`@term` is a :n:`@num`, then :n:`induction @num` behaves as - :n:`intros until @num` followed by :n:`induction` applied to the last + + If :n:`@term` is a :n:`@natural`, then :n:`induction @natural` behaves as + :n:`intros until @natural` followed by :n:`induction` applied to the last introduced hypothesis. .. note:: @@ -2024,10 +2024,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This tactic behaves as :n:`intros until @ident; elim @ident` when :n:`@ident` is a quantified variable of the goal. -.. tacv:: simple induction @num +.. tacv:: simple induction @natural - This tactic behaves as :n:`intros until @num; elim @ident` where :n:`@ident` - is the name given by :n:`intros until @num` to the :n:`@num`-th non-dependent + This tactic behaves as :n:`intros until @natural; elim @ident` where :n:`@ident` + is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent premise of the goal. .. tacn:: double induction @ident @ident @@ -2037,7 +2037,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`induction @ident; induction @ident` (or :n:`induction @ident ; destruct @ident` depending on the exact needs). -.. tacv:: double induction @num__1 @num__2 +.. tacv:: double induction @natural__1 @natural__2 This tactic is deprecated and should be replaced by :n:`induction num1; induction num3` where :n:`num3` is the result @@ -2146,9 +2146,9 @@ and an explanation of the underlying technique. .. exn:: Not a discriminable equality. :undocumented: -.. tacv:: discriminate @num +.. tacv:: discriminate @natural - This does the same thing as :n:`intros until @num` followed by + This does the same thing as :n:`intros until @natural` followed by :n:`discriminate @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. @@ -2157,12 +2157,12 @@ and an explanation of the underlying technique. This does the same thing as :n:`discriminate @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. -.. tacv:: ediscriminate @num +.. tacv:: ediscriminate @natural ediscriminate @term {? with @bindings_list} :name: ediscriminate; _ This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the - type of the hypothesis referred to by :token:`num`, has uninstantiated + type of the hypothesis referred to by :token:`natural`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: discriminate @@ -2235,9 +2235,9 @@ and an explanation of the underlying technique. This error is given when one side of the equality is not a constructor. - .. tacv:: injection @num + .. tacv:: injection @natural - This does the same thing as :n:`intros until @num` followed by + This does the same thing as :n:`intros until @natural` followed by :n:`injection @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. @@ -2246,12 +2246,12 @@ and an explanation of the underlying technique. This does the same as :n:`injection @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. - .. tacv:: einjection @num + .. tacv:: einjection @natural einjection @term {? with @bindings_list} :name: einjection; _ This works the same as :n:`injection` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@num`, has uninstantiated + type of the hypothesis referred to by :n:`@natural`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: injection @@ -2263,10 +2263,10 @@ and an explanation of the underlying technique. :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ @simple_intropattern} + injection @natural as {+ @simple_intropattern} injection as {+ @simple_intropattern} einjection @term {? with @bindings_list} as {+ @simple_intropattern} - einjection @num as {+ @simple_intropattern} + einjection @natural as {+ @simple_intropattern} einjection as {+ @simple_intropattern} These variants apply :n:`intros {+ @simple_intropattern}` after the call to @@ -2278,10 +2278,10 @@ and an explanation of the underlying technique. corresponds to a hypothesis. .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern - injection @num as @injection_intropattern + injection @natural as @injection_intropattern injection as @injection_intropattern einjection @term {? with @bindings_list} as @injection_intropattern - einjection @num as @injection_intropattern + einjection @natural as @injection_intropattern einjection as @injection_intropattern These are equivalent to the previous variants but using instead the @@ -2330,9 +2330,9 @@ and an explanation of the underlying technique. :g:`Prop`). This behavior can be turned off by using the :flag:`Keep Proof Equalities` setting. -.. tacv:: inversion @num +.. tacv:: inversion @natural - This does the same thing as :n:`intros until @num` then :n:`inversion @ident` + This does the same thing as :n:`intros until @natural` then :n:`inversion @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident @@ -2375,9 +2375,9 @@ and an explanation of the underlying technique. Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ]. -.. tacv:: inversion @num as @or_and_intropattern_loc +.. tacv:: inversion @natural as @or_and_intropattern_loc - This allows naming the hypotheses introduced by :n:`inversion @num` in the + This allows naming the hypotheses introduced by :n:`inversion @natural` in the context. .. tacv:: inversion_clear @ident as @or_and_intropattern_loc @@ -2625,7 +2625,7 @@ and an explanation of the underlying technique. .. seealso:: :tacn:`functional inversion` -.. tacn:: fix @ident @num +.. tacn:: fix @ident @natural :name: fix This tactic is a primitive tactic to start a proof by induction. In @@ -2633,11 +2633,11 @@ and an explanation of the underlying technique. as the ones described in :tacn:`induction`. In the syntax of the tactic, the identifier :n:`@ident` is the name given to - the induction hypothesis. The natural number :n:`@num` tells on which + the induction hypothesis. The natural number :n:`@natural` tells on which premise of the current goal the induction acts, starting from 1, counting both dependent and non dependent products, but skipping local definitions. Especially, the current lemma must be composed of at - least :n:`@num` products. + least :n:`@natural` products. Like in a fix expression, the induction hypotheses have to be used on structurally smaller arguments. The verification that inductive proof @@ -2646,7 +2646,7 @@ and an explanation of the underlying technique. is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). -.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} +.. tacv:: fix @ident @natural with {+ (@ident {+ @binder} [{struct @ident}] : @type)} This starts a proof by mutual induction. The statements to be simultaneously proved are respectively :g:`forall binder ... binder, type`. @@ -2756,11 +2756,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many times as possible (perhaps zero time). This form never fails. - + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. + + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. + `!` : works as `?`, except that at least one rewrite should succeed, otherwise the tactic fails. - + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, - leading to failure if these :token:`num` rewrites are not possible. + + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, + leading to failure if these :token:`natural` rewrites are not possible. .. tacv:: erewrite @term :name: erewrite @@ -2937,15 +2937,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. The term :n:`@term` and :n:`@term’` must be convertible. - .. tacv:: change @term at {+ @num} with @term’ + .. tacv:: change @term at {+ @natural} with @term’ - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` + This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. @@ -2990,8 +2990,8 @@ Performing computations | delta {? @delta_flag } ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } - occs_nums ::= {+ {| @num | @ident } } - | - {| @num | @ident } {* @int_or_var } + occs_nums ::= {+ {| @natural | @ident } } + | - {| @natural | @ident } {* @int_or_var } int_or_var ::= @int | @ident unfold_occ ::= @reference {? at @occs_nums } @@ -3228,9 +3228,9 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies :tacn:`simpl` only to the subterms matching :n:`@pattern` in the current goal. -.. tacv:: simpl @pattern at {+ @num} +.. tacv:: simpl @pattern at {+ @natural} - This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3243,10 +3243,10 @@ the conversion in hypotheses :n:`{+ @ident}`. is the unfoldable constant :n:`@qualid` (the constant can be referred to by its notation using :n:`@string` if such a notation exists). -.. tacv:: simpl @qualid at {+ @num} - simpl @string at {+ @num} +.. tacv:: simpl @qualid at {+ @natural} + simpl @string at {+ @natural} - This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM @@ -3374,14 +3374,14 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for instance, when the tactic ``apply`` fails on matching. -.. tacv:: pattern @term at {+ @num} +.. tacv:: pattern @term at {+ @natural} - Only the occurrences :n:`{+ @num}` of :n:`@term` are considered for + Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from left to right. -.. tacv:: pattern @term at - {+ @num} +.. tacv:: pattern @term at - {+ @natural} - All occurrences except the occurrences of indexes :n:`{+ @num }` + All occurrences except the occurrences of indexes :n:`{+ @natural }` of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from left to right. @@ -3394,12 +3394,12 @@ the conversion in hypotheses :n:`{+ @ident}`. If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these occurrences will also be considered and possibly abstracted. -.. tacv:: pattern {+, @term at {+ @num}} +.. tacv:: pattern {+, @term at {+ @natural}} - This behaves as above but processing only the occurrences :n:`{+ @num}` of + This behaves as above but processing only the occurrences :n:`{+ @natural}` of :n:`@term` starting from :n:`@term`. -.. tacv:: pattern {+, @term {? at {? -} {+, @num}}} +.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}} This is the most general syntax that combines the different variants. @@ -3556,9 +3556,9 @@ Automation :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will fail even if applying manually one of the hints would succeed. - .. tacv:: auto @num + .. tacv:: auto @natural - Forces the search depth to be :token:`num`. The maximal search depth + Forces the search depth to be :token:`natural`. The maximal search depth is 5 by default. .. tacv:: auto with {+ @ident} @@ -3609,7 +3609,7 @@ Automation Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} This is the most general form, combining the various options. @@ -3664,7 +3664,7 @@ Automation Note that ``ex_intro`` should be declared as a hint. - .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} The various options for :tacn:`eauto` are the same as for :tacn:`auto`. @@ -3827,12 +3827,12 @@ automatically created. .. deprecated:: 8.10 - .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident :name: Hint Resolve This command adds :n:`simple apply @qualid` to the hint list with the head symbol of the type of :n:`@qualid`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The + subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type of :n:`@qualid` does not start with a product the tactic added in the hint list @@ -3930,7 +3930,7 @@ automatically created. overwriting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident + .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and @@ -4359,7 +4359,7 @@ some incompatibilities. This combines the effects of the different variants of :tacn:`firstorder`. -.. opt:: Firstorder Depth @num +.. opt:: Firstorder Depth @natural :name: Firstorder Depth This option controls the proof-search depth bound. @@ -4396,10 +4396,10 @@ some incompatibilities. congruence. Qed. -.. tacv:: congruence @num +.. tacv:: congruence @natural - Tries to add at most :token:`num` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of :token:`num` does not make + Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`natural` does not make success slower, only failure. You might consider adding some lemmas as hypotheses using assert in order for :tacn:`congruence` to use them. @@ -4598,9 +4598,9 @@ symbol :g:`=`. then :n:`simplify_eq @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. -.. tacv:: simplify_eq @num +.. tacv:: simplify_eq @natural - This does the same thing as :n:`intros until @num` then + This does the same thing as :n:`intros until @natural` then :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last introduced hypothesis. @@ -4609,12 +4609,12 @@ symbol :g:`=`. This does the same as :n:`simplify_eq @term` but using the given bindings to instantiate parameters or hypotheses of :n:`@term`. -.. tacv:: esimplify_eq @num +.. tacv:: esimplify_eq @natural esimplify_eq @term {? with @bindings_list} :name: esimplify_eq; _ This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@num`, has uninstantiated + type of the hypothesis referred to by :n:`@natural`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: simplify_eq @@ -4913,10 +4913,10 @@ Performance-oriented tactic variants .. tacv:: change_no_check @term with @term’ :undocumented: - .. tacv:: change_no_check @term at {+ @num} with @term’ + .. tacv:: change_no_check @term at {+ @natural} with @term’ :undocumented: - .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident + .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident .. example:: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 36ad4af837..e13558b440 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -32,7 +32,7 @@ Displaying .. exn:: @qualid not a defined object. :undocumented: - .. exn:: Universe instance should have length @num. + .. exn:: Universe instance should have length @natural. :undocumented: .. exn:: This object does not support universe names. @@ -44,9 +44,9 @@ Displaying This command displays information about the current state of the environment, including sections and modules. -.. cmd:: Inspect @num +.. cmd:: Inspect @natural - This command displays the :n:`@num` last objects of the + This command displays the :n:`@natural` last objects of the current environment, including sections and modules. .. cmd:: Print Section @qualid @@ -60,7 +60,7 @@ Query commands -------------- Unlike other commands, :production:`query_command`\s may be prefixed with -a goal selector (:n:`@num:`) to specify which goal context it applies to. +a goal selector (:n:`@natural:`) to specify which goal context it applies to. If no selector is provided, the command applies to the current goal. If no proof is open, then the command only applies to accessible objects. (see Section :ref:`invocation-of-tactics`). @@ -757,10 +757,10 @@ interactively, they cannot be part of a vernacular file loaded via of the interactive session. -.. cmd:: Back {? @num } +.. cmd:: Back {? @natural } - Undoes all the effects of the last :n:`@num @sentence`\s. If - :n:`@num` is not specified, the command undoes one sentence. + Undoes all the effects of the last :n:`@natural @sentence`\s. If + :n:`@natural` is not specified, the command undoes one sentence. Sentences read from a `.v` file via a :cmd:`Load` are considered a single sentence. While :cmd:`Back` can undo tactics and commands executed within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all @@ -772,14 +772,14 @@ interactively, they cannot be part of a vernacular file loaded via The user wants to undo more commands than available in the history. -.. cmd:: BackTo @num +.. cmd:: BackTo @natural - This command brings back the system to the state labeled :n:`@num`, + This command brings back the system to the state labeled :n:`@natural`, forgetting the effect of all commands executed after this state. The state label is an integer which grows after each successful command. It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see above), the :cmd:`BackTo` command now handles proof states. For that, it may - have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if + have to undo some extra commands and end on a state :n:`@natural′ ≤ @natural` if necessary. .. _quitting-and-debugging: @@ -834,16 +834,16 @@ Quitting and debugging output to the file ":n:`@string`.out". -.. cmd:: Timeout @num @sentence +.. cmd:: Timeout @natural @sentence Executes :n:`@sentence`. If the operation - has not terminated after :n:`@num` seconds, then it is interrupted and an error message is + has not terminated after :n:`@natural` seconds, then it is interrupted and an error message is displayed. - .. opt:: Default Timeout @num + .. opt:: Default Timeout @natural :name: Default Timeout - If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`, + If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@natural`, except for :cmd:`Timeout` commands themselves. If unset, no timeout is applied. @@ -890,14 +890,14 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. -.. opt:: Printing Width @num +.. opt:: Printing Width @natural :name: Printing Width This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. -.. opt:: Printing Depth @num +.. opt:: Printing Depth @natural :name: Printing Depth This option controls the nesting depth of the formatter used for pretty- diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9e8e5e5fa5..2c10e77868 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -931,7 +931,7 @@ of patterns have. The lower level is 0 and this is the level used by default to put rules delimited with tokens on both ends. The level is left to be inferred by Coq when using :n:`in custom @ident`. The level is otherwise given explicitly by using the syntax -:n:`in custom @ident at level @num`, where :n:`@num` refers to the level. +:n:`in custom @ident at level @natural`, where :n:`@natural` refers to the level. Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this @@ -1053,8 +1053,8 @@ Here are the syntax elements used by the various notation commands. .. insertprodn syntax_modifier level .. prodn:: - syntax_modifier ::= at level @num - | in custom @ident {? at level @num } + syntax_modifier ::= at level @natural + | in custom @ident {? at level @natural } | {+, @ident } at @level | @ident at @level {? @binder_interp } | @ident @explicit_subentry @@ -1068,16 +1068,16 @@ Here are the syntax elements used by the various notation commands. explicit_subentry ::= ident | global | bigint - | strict pattern {? at level @num } + | strict pattern {? at level @natural } | binder | closed binder | constr {? at @level } {? @binder_interp } | custom @ident {? at @level } {? @binder_interp } - | pattern {? at level @num } + | pattern {? at level @natural } binder_interp ::= as ident | as pattern | as strict pattern - level ::= level @num + level ::= level @natural | next level .. note:: No typing of the denoted expression is performed at definition @@ -1530,7 +1530,7 @@ numbers (see :ref:`datatypes`). .. note:: - Negative integers are not at the same level as :n:`@num`, for this + Negative integers are not at the same level as :n:`@natural`, for this would make precedence unnatural. .. _numeral-notations: @@ -1624,7 +1624,7 @@ Numeral notations .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type. - As noted above, the :n:`(abstract after @num)` directive has no + As noted above, the :n:`(abstract after @natural)` directive has no effect when :n:`@qualid__parse` lands in an :g:`option` type. .. exn:: Cannot interpret this number as a value of type @type @@ -1776,7 +1776,7 @@ Tactic notations allow customizing the syntax of tactics. can you run into problems if you shadow another tactic or tactic notation? If so, how to avoid ambiguity? -.. cmd:: Tactic Notation {? ( at level @num ) } {+ @ltac_production_item } := @ltac_expr +.. cmd:: Tactic Notation {? ( at level @natural ) } {+ @ltac_production_item } := @ltac_expr .. insertprodn ltac_production_item ltac_production_item @@ -1789,7 +1789,7 @@ Tactic notations allow customizing the syntax of tactics. This command supports the :attr:`local` attribute, which limits the notation to the current module. - :token:`num` + :token:`natural` The parsing precedence to assign to the notation. This information is particularly relevant for notations for tacticals. Levels can be in the range 0 .. 5 (default is 5). diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst index 3625eac4a5..738d64bfc3 100644 --- a/doc/sphinx/using/libraries/funind.rst +++ b/doc/sphinx/using/libraries/funind.rst @@ -243,16 +243,16 @@ Tactics Function. - .. tacv:: functional inversion @num + .. tacv:: functional inversion @natural - This does the same thing as :n:`intros until @num` followed by + This does the same thing as :n:`intros until @natural` followed by :n:`functional inversion @ident` where :token:`ident` is the identifier for the last introduced hypothesis. .. tacv:: functional inversion @ident @qualid - functional inversion @num @qualid + functional inversion @natural @qualid - If the hypothesis :token:`ident` (or :token:`num`) has a type of the form + If the hypothesis :token:`ident` (or :token:`natural`) has a type of the form :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to functional inversion, this variant allows choosing which :token:`qualid` diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index cffe196b77..3fef3bcbd1 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -351,7 +351,7 @@ class TacticObject(NotationObject): Example:: - .. tacn:: do @num @expr + .. tacn:: do @natural @expr :token:`expr` is evaluated to ``v`` which must be a tactic value. … """ @@ -401,7 +401,7 @@ class OptionObject(NotationObject): Example:: - .. opt:: Hyps Limit @num + .. opt:: Hyps Limit @natural :name Hyps Limit Controls the maximum number of hypotheses displayed in goals after @@ -452,7 +452,7 @@ class ProductionObject(CoqObject): Example:: - .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } } term += let: @pattern := @term in @term | second_production diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 549ace5d13..ff40555696 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -749,7 +749,7 @@ digit: [ | "0" ".." "9" ] -decnum: [ +decnat: [ | digit LIST0 [ digit | "_" ] ] @@ -757,26 +757,22 @@ hexdigit: [ | [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ] ] -hexnum: [ +hexnat: [ | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ] ] -num: [ -| [ decnum | hexnum ] -] - -natural: [ | DELETENT ] natural: [ -| num (* todo: or should it be "nat"? *) +| REPLACE bignat +| WITH [ decnat | hexnat ] ] int: [ -| OPT "-" num +| OPT "-" natural ] numeral: [ -| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum ) -| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum ) +| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) +| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] bigint: [ @@ -1841,7 +1837,7 @@ query_command: [ ] (* re-add as a placeholder *) sentence: [ | OPT attributes command "." -| OPT attributes OPT ( num ":" ) query_command "." +| OPT attributes OPT ( natural ":" ) query_command "." | OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ] | control_command ] @@ -2053,8 +2049,8 @@ tac2rec_fields: [ (* todo: weird productions, ints only after an initial "-"??: occs_nums: [ - | LIST1 [ num | ident ] - | "-" [ num | ident ] LIST0 int_or_var + | LIST1 [ natural | ident ] + | "-" [ natural | ident ] LIST0 int_or_var *) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) @@ -2160,7 +2156,7 @@ RENAME: [ | Prim.string string | Prim.integer int | Prim.qualid qualid -| Prim.natural num +| Prim.natural natural ] gmatch_list: [ @@ -2210,7 +2206,6 @@ SPLICE: [ | match_context_list | IDENT | LEFTQMARK -| natural | NUMBER | STRING | hyp diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 3cd5a85654..6d07f6b0c4 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -130,19 +130,19 @@ type: [ ] numeral: [ -| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum ) -| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum ) +| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) +| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] int: [ -| OPT "-" num +| OPT "-" natural ] -num: [ -| [ decnum | hexnum ] +natural: [ +| [ decnat | hexnat ] ] -decnum: [ +decnat: [ | digit LIST0 [ digit | "_" ] ] @@ -150,7 +150,7 @@ digit: [ | "0" ".." "9" ] -hexnum: [ +hexnat: [ | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ] ] @@ -230,7 +230,7 @@ nonterminal: [ sentence: [ | OPT attributes command "." -| OPT attributes OPT ( num ":" ) query_command "." +| OPT attributes OPT ( natural ":" ) query_command "." | OPT attributes OPT ( toplevel_selector ":" ) ltac_expr [ "." | "..." ] | control_command ] @@ -277,7 +277,7 @@ universe: [ ] universe_expr: [ -| universe_name OPT ( "+" num ) +| universe_name OPT ( "+" natural ) ] universe_name: [ @@ -509,8 +509,8 @@ ref_or_pattern_occ: [ ] occs_nums: [ -| LIST1 [ num | ident ] -| "-" [ num | ident ] LIST0 int_or_var +| LIST1 [ natural | ident ] +| "-" [ natural | ident ] LIST0 int_or_var ] int_or_var: [ @@ -535,7 +535,7 @@ record_definition: [ ] record_field: [ -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations +| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" natural ] OPT decl_notations ] field_body: [ @@ -589,7 +589,7 @@ sort_family: [ ] hint_info: [ -| "|" OPT num OPT one_term +| "|" OPT natural OPT one_term ] module_binder: [ @@ -602,7 +602,7 @@ module_type_inl: [ ] functor_app_annot: [ -| "[" "inline" "at" "level" num "]" +| "[" "inline" "at" "level" natural "]" | "[" "no" "inline" "]" ] @@ -714,7 +714,7 @@ command: [ | "Locate" reference | "Locate" "Term" reference | "Locate" "Module" qualid -| "Info" num ltac_expr +| "Info" natural ltac_expr | "Locate" "Ltac" qualid | "Locate" "Library" qualid | "Locate" "File" string @@ -762,7 +762,7 @@ command: [ | "Print" "Module" "Type" qualid | "Print" "Module" qualid | "Print" "Namespace" dirpath -| "Inspect" num +| "Inspect" natural | "Add" "ML" "Path" string | OPT "Export" "Set" setting_name | "Print" "Table" setting_name @@ -773,7 +773,7 @@ command: [ | "Restore" "State" [ ident | string ] | "Reset" "Initial" | "Reset" ident -| "Back" OPT num +| "Back" OPT natural | "Debug" [ "On" | "Off" ] | "Declare" "Reduction" ident ":=" red_expr | "Declare" "Custom" "Entry" ident @@ -802,17 +802,17 @@ command: [ | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] -| "Existential" num OPT ( ":" term ) ":=" term +| "Existential" natural OPT ( ":" term ) ":=" term | "Admitted" | "Qed" | "Save" ident | "Defined" OPT ident | "Restart" -| "Undo" OPT ( OPT "To" num ) -| "Focus" OPT num +| "Undo" OPT ( OPT "To" natural ) +| "Focus" OPT natural | "Unfocus" | "Unfocused" -| "Show" OPT [ ident | num ] +| "Show" OPT [ ident | natural ] | "Show" "Existentials" | "Show" "Universes" | "Show" "Conjectures" @@ -824,7 +824,7 @@ command: [ | "Create" "HintDb" ident OPT "discriminated" | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident ) | "Hint" hint OPT ( ":" LIST1 ident ) -| "Comments" LIST0 [ one_term | string | num ] +| "Comments" LIST0 [ one_term | string | natural ] | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info | "Declare" "Scope" scope_name | "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) @@ -894,7 +894,7 @@ command: [ | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ] | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ] -| "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr +| "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid | "Ltac" tacdef_body LIST0 ( "with" tacdef_body ) @@ -916,7 +916,7 @@ command: [ | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] -| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] +| assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] | [ "Definition" | "Example" ] ident_decl def_body | "Let" ident_decl def_body | "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) @@ -959,7 +959,7 @@ command: [ | "Context" LIST1 binder | "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ] | "Existing" "Instance" qualid OPT hint_info -| "Existing" "Instances" LIST1 qualid OPT [ "|" num ] +| "Existing" "Instances" LIST1 qualid OPT [ "|" natural ] | "Existing" "Class" qualid | "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ] | "Implicit" [ "Type" | "Types" ] reserv_list @@ -995,12 +995,12 @@ command: [ | "Print" "Ltac2" qualid (* Ltac2 plugin *) | "Time" sentence | "Redirect" string sentence -| "Timeout" num sentence +| "Timeout" natural sentence | "Fail" sentence | "Drop" | "Quit" -| "BackTo" num -| "Show" "Goal" num "at" num +| "BackTo" natural +| "Show" "Goal" natural "at" natural ] section_subset_expr: [ @@ -1067,8 +1067,8 @@ univ_name_list: [ hint: [ | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info -| "Resolve" "->" LIST1 qualid OPT num -| "Resolve" "<-" LIST1 qualid OPT num +| "Resolve" "->" LIST1 qualid OPT natural +| "Resolve" "<-" LIST1 qualid OPT natural | "Immediate" LIST1 [ qualid | one_term ] | "Variables" "Transparent" | "Variables" "Opaque" @@ -1079,7 +1079,7 @@ hint: [ | "Mode" qualid LIST1 [ "+" | "!" | "-" ] | "Unfold" LIST1 qualid | "Constructors" LIST1 qualid -| "Extern" num OPT one_term "=>" ltac_expr +| "Extern" natural OPT one_term "=>" ltac_expr ] tacdef_body: [ @@ -1127,7 +1127,7 @@ lident: [ ] destruction_arg: [ -| num +| natural | constr_with_bindings | constr_with_bindings_arg ] @@ -1221,7 +1221,7 @@ q_destruction_arg: [ ] ltac2_destruction_arg: [ -| num (* Ltac2 plugin *) +| natural (* Ltac2 plugin *) | lident (* Ltac2 plugin *) | ltac2_constr_with_bindings (* Ltac2 plugin *) ] @@ -1249,7 +1249,7 @@ ltac2_simple_binding: [ qhyp: [ | "$" ident (* Ltac2 plugin *) -| num (* Ltac2 plugin *) +| natural (* Ltac2 plugin *) | lident (* Ltac2 plugin *) ] @@ -1318,8 +1318,8 @@ class: [ ] syntax_modifier: [ -| "at" "level" num -| "in" "custom" ident OPT ( "at" "level" num ) +| "at" "level" natural +| "in" "custom" ident OPT ( "at" "level" natural ) | LIST1 ident SEP "," "at" level | ident "at" level OPT binder_interp | ident explicit_subentry @@ -1336,12 +1336,12 @@ explicit_subentry: [ | "ident" | "global" | "bigint" -| "strict" "pattern" OPT ( "at" "level" num ) +| "strict" "pattern" OPT ( "at" "level" natural ) | "binder" | "closed" "binder" | "constr" OPT ( "at" level ) OPT binder_interp | "custom" ident OPT ( "at" level ) OPT binder_interp -| "pattern" OPT ( "at" "level" num ) +| "pattern" OPT ( "at" "level" natural ) ] binder_interp: [ @@ -1351,7 +1351,7 @@ binder_interp: [ ] level: [ -| "level" num +| "level" natural | "next" "level" ] @@ -1388,14 +1388,14 @@ simple_tactic: [ | "esplit" OPT ( "with" bindings ) | "exists" OPT ( LIST1 bindings SEP "," ) | "eexists" OPT ( LIST1 bindings SEP "," ) -| "intros" "until" [ ident | num ] +| "intros" "until" [ ident | natural ] | "intro" OPT ident OPT where | "move" ident OPT where | "rename" LIST1 ( ident "into" ident ) SEP "," | "revert" LIST1 ident -| "simple" "induction" [ ident | num ] -| "simple" "destruct" [ ident | num ] -| "double" "induction" [ ident | num ] [ ident | num ] +| "simple" "induction" [ ident | natural ] +| "simple" "destruct" [ ident | natural ] +| "double" "induction" [ ident | natural ] [ ident | natural ] | "admit" | "clear" LIST0 ident | "clear" "-" LIST1 ident @@ -1551,7 +1551,7 @@ simple_tactic: [ | "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings ) | "case" induction_clause_list | "ecase" induction_clause_list -| "fix" ident num OPT ( "with" LIST1 fixdecl ) +| "fix" ident natural OPT ( "with" LIST1 fixdecl ) | "cofix" ident OPT ( "with" LIST1 cofixdecl ) | "pose" bindings_with_parameters | "pose" one_term OPT as_name @@ -1585,11 +1585,11 @@ simple_tactic: [ | "edestruct" induction_clause_list | "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 ) | "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 ) -| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | num ] OPT as_or_and_ipat OPT [ "with" one_term ] -| "simple" "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) -| "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) -| "inversion_clear" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) -| "inversion" [ ident | num ] "using" one_term OPT ( "in" LIST1 ident ) +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | natural ] OPT as_or_and_ipat OPT [ "with" one_term ] +| "simple" "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) +| "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) +| "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) +| "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident ) | "red" OPT clause_dft_concl | "hnf" OPT clause_dft_concl | "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl @@ -1610,7 +1610,7 @@ simple_tactic: [ | "f_equal" | "firstorder" OPT ltac_expr firstorder_rhs | "gintuition" OPT ltac_expr -| "functional" "inversion" [ ident | num ] OPT qualid (* funind plugin *) +| "functional" "inversion" [ ident | natural ] OPT qualid (* funind plugin *) | "functional" "induction" term OPT fun_ind_using OPT with_names (* funind plugin *) | "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names (* funind plugin *) | "psatz_Z" OPT int_or_var ltac_expr @@ -1698,7 +1698,7 @@ as_name: [ ] rewriter: [ -| OPT num OPT [ "?" | "!" ] constr_with_bindings_arg +| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg ] oriented_rewriter: [ @@ -1758,7 +1758,7 @@ simple_intropattern_closed: [ simple_binding: [ | "(" ident ":=" term ")" -| "(" num ":=" term ")" +| "(" natural ":=" term ")" ] bindings: [ @@ -1807,7 +1807,7 @@ ltac2_occs: [ ] ltac2_occs_nums: [ -| OPT "-" LIST1 [ num (* Ltac2 plugin *) | "$" ident ] (* Ltac2 plugin *) +| OPT "-" LIST1 [ natural (* Ltac2 plugin *) | "$" ident ] (* Ltac2 plugin *) ] ltac2_concl_occ: [ @@ -1858,7 +1858,7 @@ ltac2_oriented_rewriter: [ ] ltac2_rewriter: [ -| OPT num OPT [ "?" | "!" ] ltac2_constr_with_bindings +| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings ] q_dispatch: [ @@ -2328,8 +2328,8 @@ selector: [ ] range_selector: [ -| num "-" num -| num +| natural "-" natural +| natural ] match_key: [ -- cgit v1.2.3 From 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:09:00 +0200 Subject: [refman] Rename numeral to number --- doc/sphinx/language/coq-library.rst | 2 +- doc/sphinx/language/core/basic.rst | 4 +- doc/sphinx/language/core/variants.rst | 2 +- doc/sphinx/user-extensions/syntax-extensions.rst | 56 ++++++++++++------------ doc/tools/docgram/common.edit_mlg | 4 +- doc/tools/docgram/orderedGrammar | 10 ++--- 6 files changed, 39 insertions(+), 39 deletions(-) diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c27eb216e8..765373619f 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,7 +1062,7 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. -.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing] +.. warn:: The constant @number is not a binary64 floating-point value. A closest value @number will be used and unambiguously printed @number. [inexact-float,parsing] Not all decimal constants are floating-point values. This warning is generated when parsing such a constant (for instance ``0.1``). diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 63c4243921..be513833ad 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -119,10 +119,10 @@ Numerals integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. - .. insertprodn numeral hexdigit + .. insertprodn number hexdigit .. prodn:: - numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } + number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } int ::= {? - } @natural natural ::= {| @decnat | @hexnat } diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index ec8e93751c..2904250e41 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -79,7 +79,7 @@ to apply specific treatments accordingly. | %{%| {* @qualid := @pattern } %|%} | _ | ( {+| @pattern } ) - | @numeral + | @number | @string Note that the :n:`@pattern ::= @pattern10 : @term` production diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2c10e77868..8474d0287f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1124,7 +1124,7 @@ refer to different definitions depending on which notation scopes are currently open. For instance, the infix symbol ``+`` can be used to refer to distinct definitions of the addition operator, such as for natural numbers, integers or reals. -Notation scopes can include an interpretation for numerals and +Notation scopes can include an interpretation for numbers and strings with the :cmd:`Numeral Notation` and :cmd:`String Notation` commands. .. insertprodn scope scope_key @@ -1311,31 +1311,31 @@ Scopes` or :cmd:`Print Scope`. ``nat_scope`` This scope includes the standard arithmetical operators and relations on type - nat. Positive integer numerals in this scope are mapped to their canonical + nat. Positive integer numbers in this scope are mapped to their canonical representent built from :g:`O` and :g:`S`. The scope is delimited by the key ``nat``, and bound to the type :g:`nat` (see above). ``N_scope`` This scope includes the standard arithmetical operators and relations on type :g:`N` (binary natural numbers). It is delimited by the key ``N`` and comes - with an interpretation for numerals as closed terms of type :g:`N`. + with an interpretation for numbers as closed terms of type :g:`N`. ``Z_scope`` This scope includes the standard arithmetical operators and relations on type :g:`Z` (binary integer numbers). It is delimited by the key ``Z`` and comes - with an interpretation for numerals as closed terms of type :g:`Z`. + with an interpretation for numbers as closed terms of type :g:`Z`. ``positive_scope`` This scope includes the standard arithmetical operators and relations on type :g:`positive` (binary strictly positive numbers). It is delimited by - key ``positive`` and comes with an interpretation for numerals as closed + key ``positive`` and comes with an interpretation for numbers as closed terms of type :g:`positive`. ``Q_scope`` This scope includes the standard arithmetical operators and relations on type :g:`Q` (rational numbers defined as fractions of an integer and a strictly positive integer modulo the equality of the numerator- - denominator cross-product) and comes with an interpretation for numerals + denominator cross-product) and comes with an interpretation for numbers as closed terms of type :g:`Q`. ``Qc_scope`` @@ -1346,7 +1346,7 @@ Scopes` or :cmd:`Print Scope`. ``R_scope`` This scope includes the standard arithmetical operators and relations on type :g:`R` (axiomatic real numbers). It is delimited by the key ``R`` and comes - with an interpretation for numerals using the :g:`IZR` morphism from binary + with an interpretation for numbers using the :g:`IZR` morphism from binary integer numbers to :g:`R` and :g:`Z.pow_pos` for potential exponent parts. ``bool_scope`` @@ -1514,18 +1514,18 @@ Abbreviations .. extracted from Gallina chapter -Numerals and strings --------------------- +Numbers and strings +------------------- .. insertprodn primitive_notations primitive_notations .. prodn:: - primitive_notations ::= @numeral + primitive_notations ::= @number | @string -Numerals and strings have no predefined semantics in the calculus. They are +Numbers and strings have no predefined semantics in the calculus. They are merely notations that can be bound to objects through the notation mechanism. -Initially, numerals are bound to Peano’s representation of natural +Initially, numbers are bound to Peano’s representation of natural numbers (see :ref:`datatypes`). .. note:: @@ -1544,8 +1544,8 @@ Numeral notations .. insertprodn numeral_modifier numeral_modifier .. prodn:: - numeral_modifier ::= ( warning after @numeral ) - | ( abstract after @numeral ) + numeral_modifier ::= ( warning after @number ) + | ( abstract after @number ) This command allows the user to customize the way numeral literals are parsed and printed. @@ -1591,35 +1591,35 @@ Numeral notations function application, constructors, inductive type families, sorts, and primitive integers) will be considered for printing. - :n:`( warning after @numeral )` + :n:`( warning after @number )` displays a warning message about a possible stack - overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@numeral`. + overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@number`. .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(warning after @numeral)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`numeral`. + with :n:`(warning after @number)`, this warning is emitted when + parsing a number greater than or equal to :token:`number`. - :n:`( abstract after @numeral )` + :n:`( abstract after @number )` returns :n:`(@qualid__parse m)` when parsing a literal - :n:`m` that's greater than :n:`@numeral` rather than reducing it to a normal form. + :n:`m` that's greater than :n:`@number` rather than reducing it to a normal form. Here :g:`m` will be a :g:`Numeral.int` or :g:`Numeral.uint` or :g:`Z`, depending on the type of the parsing function :n:`@qualid__parse`. This allows for a more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a - warning will be emitted when an integer larger than :token:`numeral` - is parsed. Note that :n:`(abstract after @numeral)` has no effect + warning will be emitted when an integer larger than :token:`number` + is parsed. Note that :n:`(abstract after @number)` has no effect when :n:`@qualid__parse` lands in an :g:`option` type. .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @qualid__parse. When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(abstract after @numeral)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`numeral`. + with :n:`(abstract after @number)`, this warning is emitted when + parsing a number greater than or equal to :token:`number`. Typically, this indicates that the fully computed representation - of numerals can be so large that non-tail-recursive OCaml + of numbers can be so large that non-tail-recursive OCaml functions run out of stack space when trying to walk them. .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type. @@ -1630,9 +1630,9 @@ Numeral notations .. exn:: Cannot interpret this number as a value of type @type The numeral notation registered for :token:`type` does not support - the given numeral. This error is given when the interpretation + the given number. This error is given when the interpretation function returns :g:`None`, or if the interpretation is registered - only for integers or non-negative integers, and the given numeral + only for integers or non-negative integers, and the given number has a fractional or exponent part or is negative. @@ -1657,7 +1657,7 @@ Numeral notations Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a - concrete numeral expressed as a (hexa)decimal. They may not return + concrete number expressed as a (hexa)decimal. They may not return opaque constants. String notations diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index ff40555696..fbf83760ad 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -770,7 +770,7 @@ int: [ | OPT "-" natural ] -numeral: [ +number: [ | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] @@ -795,7 +795,7 @@ ident: [ ] NUMBER: [ -| numeral +| number ] (* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 6d07f6b0c4..a021bdbec0 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -93,7 +93,7 @@ term_explicit: [ ] primitive_notations: [ -| numeral +| number | string ] @@ -129,7 +129,7 @@ type: [ | term ] -numeral: [ +number: [ | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] @@ -429,7 +429,7 @@ pattern0: [ | "{|" LIST0 ( qualid ":=" pattern ) "|}" | "_" | "(" LIST1 pattern SEP "|" ")" -| numeral +| number | string ] @@ -1291,8 +1291,8 @@ field_mod: [ ] numeral_modifier: [ -| "(" "warning" "after" numeral ")" -| "(" "abstract" "after" numeral ")" +| "(" "warning" "after" number ")" +| "(" "abstract" "after" number ")" ] hints_path: [ -- cgit v1.2.3 From 724966f56caa66a5ddc9a992cf870ebc2efae004 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 7 Sep 2020 11:53:49 +0200 Subject: [refman] Rename int to integer --- doc/sphinx/language/core/basic.rst | 10 +++--- doc/sphinx/proof-engine/ltac.rst | 16 ++++----- doc/sphinx/proof-engine/ltac2.rst | 20 +++++------ .../proof-engine/ssreflect-proof-language.rst | 2 +- doc/sphinx/proof-engine/tactics.rst | 16 ++++----- doc/sphinx/proof-engine/vernacular-commands.rst | 4 +-- doc/sphinx/user-extensions/syntax-extensions.rst | 2 +- doc/tools/docgram/common.edit_mlg | 42 ++++++++++------------ doc/tools/docgram/fullGrammar | 6 ++-- doc/tools/docgram/orderedGrammar | 38 ++++++++++---------- plugins/ltac/g_class.mlg | 2 +- plugins/ltac/profile_ltac_tactics.mlg | 4 +-- 12 files changed, 79 insertions(+), 83 deletions(-) diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index be513833ad..d248839fa0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -111,11 +111,11 @@ Identifiers symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. -Numerals - Numerals are sequences of digits with an optional fractional part +Numbers + Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals start with ``0x`` or ``0X``. :n:`@int` is an integer; - a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative + a number without fractional nor exponent parts. :n:`@natural` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. @@ -124,7 +124,7 @@ Numerals .. prodn:: number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } - int ::= {? - } @natural + integer ::= {? - } @natural natural ::= {| @decnat | @hexnat } decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 @@ -434,7 +434,7 @@ gray boxes after the labels "Flag", "Option" and "Table". In the pdf, they appear after a boldface label. They are listed in the :ref:`options_index`. -.. cmd:: Set @setting_name {? {| @int | @string } } +.. cmd:: Set @setting_name {? {| @integer | @string } } :name: Set If :n:`@setting_name` is a flag, no value may be provided; the flag diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2bccfcd615..2a102adfcc 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -74,7 +74,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`. ltac_expr0 ::= ( @ltac_expr ) | [> @for_each_goal ] | @tactic_atom - tactic_atom ::= @int + tactic_atom ::= @integer | @qualid | () @@ -188,7 +188,7 @@ examining the part at the end under "Entry tactic:tactic_arg". - * - ``integer`` - - :token:`int` + - :token:`integer` - an integer - @@ -876,7 +876,7 @@ Print/identity tactic: idtac ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: idtac {* {| @ident | @string | @int } } +.. tacn:: idtac {* {| @ident | @string | @integer } } :name: idtac Leaves the proof unchanged and prints the given tokens. Strings and integers are printed @@ -888,7 +888,7 @@ Print/identity tactic: idtac Failing ~~~~~~~ -.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @int } } +.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @integer } } :name: fail; gfail :tacn:`fail` is the always-failing tactic: it does not solve any @@ -919,7 +919,7 @@ Failing the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct, respecting the algebraic identity. - :n:`{* {| @ident | @string | @int } }` + :n:`{* {| @ident | @string | @integer } }` The given tokens are used for printing the failure message. If :token:`ident` is an |Ltac| variable, its contents are printed; if not, it is an error. @@ -2302,11 +2302,11 @@ performance issue. This flag enables and disables the profiler. -.. cmd:: Show Ltac Profile {? {| CutOff @int | @string } } +.. cmd:: Show Ltac Profile {? {| CutOff @integer | @string } } Prints the profile. - :n:`CutOff @int` + :n:`CutOff @integer` By default, tactics that account for less than 2% of the total time are not displayed. `CutOff` lets you specify a different percentage. @@ -2373,7 +2373,7 @@ performance issue. Equivalent to the :cmd:`Reset Ltac Profile` command, which allows resetting the profile from tactic scripts for benchmarking purposes. -.. tacn:: show ltac profile {? {| cutoff @int | @string } } +.. tacn:: show ltac profile {? {| cutoff @integer | @string } } :name: show ltac profile Equivalent to the :cmd:`Show Ltac Profile` command, diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 9b8749f185..b4f32c6cbb 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -283,7 +283,7 @@ There is dedicated syntax for list and array literals. | [ {*; @ltac2_expr5 } ] | %{ {? {+ @tac2rec_fieldexpr } {? ; } } %} | @ltac2_tactic_atom - ltac2_tactic_atom ::= @int + ltac2_tactic_atom ::= @integer | @string | @qualid | @ @ident @@ -1159,7 +1159,7 @@ Match on values Notations --------- -.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @int } := @ltac2_expr +.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @integer } := @ltac2_expr :name: Ltac2 Notation .. todo seems like name maybe should use lident rather than ident, considering: @@ -1177,7 +1177,7 @@ Notations :cmd:`Ltac2 Notation` provides a way to extend the syntax of Ltac2 tactics. The left-hand side (before the `:=`) defines the syntax to recognize and gives formal parameter - names for the syntactic values. :n:`@int` is the level of the notation. + names for the syntactic values. :n:`@integer` is the level of the notation. When the notation is used, the values are substituted into the right-hand side. The right-hand side is typechecked when the notation is used, not when it is defined. In the following example, `x` is the formal parameter name and @@ -1333,7 +1333,7 @@ Syntactic classes are described with a form of S-expression: .. prodn:: ltac2_scope ::= @string - | @int + | @integer | @name | @name ( {+, @ltac2_scope } ) @@ -1384,14 +1384,14 @@ table further down lists the classes that that are handled plainly. :n:`terminal(@string)` Accepts the specified string whether it's a keyword or not, returning a value of `()`. - :n:`tactic {? (@int) }` - Parses an :token:`ltac2_expr`. If :token:`int` is specified, the construct - parses a :n:`ltac2_expr@int`, for example `tactic(5)` parses :token:`ltac2_expr5`. + :n:`tactic {? (@integer) }` + Parses an :token:`ltac2_expr`. If :token:`integer` is specified, the construct + parses a :n:`ltac2_expr@integer`, for example `tactic(5)` parses :token:`ltac2_expr5`. `tactic(6)` parses :token:`ltac2_expr`. - :token:`int` must be in the range `0 .. 6`. + :token:`integer` must be in the range `0 .. 6`. - You can also use `tactic` to accept an :token:`int` or a :token:`string`, but there's - no syntactic class that accepts *only* an :token:`int` or a :token:`string`. + You can also use `tactic` to accept an :token:`integer` or a :token:`string`, but there's + no syntactic class that accepts *only* an :token:`integer` or a :token:`string`. .. todo this doesn't work as expected: "::" is in ltac2_expr1 Ltac2 Notation "ex4" x(tactic(0)) := x. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 2d1b622a2d..ca50a02562 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -5573,7 +5573,7 @@ Natural number .. prodn:: nat_or_ident ::= {| @natural | @ident } -where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral +where :token:`ident` is an Ltac variable denoting a standard |Coq| number (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index de39edc8e9..2f505e7448 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1734,7 +1734,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) followed by destruct applied to the last introduced hypothesis. .. note:: - For destruction of a numeral, use syntax :n:`destruct (@natural)` (not + For destruction of a number, use syntax :n:`destruct (@natural)` (not very interesting anyway). .. tacv:: destruct @pattern @@ -1866,7 +1866,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) introduced hypothesis. .. note:: - For simple induction on a numeral, use syntax induction (num) + For simple induction on a number, use syntax induction (number) (not very interesting anyway). + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident` @@ -2992,7 +2992,7 @@ Performing computations | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } | - {| @natural | @ident } {* @int_or_var } - int_or_var ::= @int + int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } pattern_occ ::= @one_term {? at @occs_nums } @@ -4737,12 +4737,12 @@ Non-logical tactics ------------------------ -.. tacn:: cycle @int +.. tacn:: cycle @integer :name: cycle - Reorders the selected goals so that the first :n:`@int` goals appear after the + Reorders the selected goals so that the first :n:`@integer` goals appear after the other selected goals. - If :n:`@int` is negative, it puts the last :n:`@int` goals at the + If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the beginning of the list. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent @@ -4761,11 +4761,11 @@ Non-logical tactics all: cycle 2. all: cycle -3. -.. tacn:: swap @int @int +.. tacn:: swap @integer @integer :name: swap Exchanges the position of the specified goals. - Negative values for :n:`@int` indicate counting goals + Negative values for :n:`@integer` indicate counting goals backward from the end of the list of selected goals. Goals are indexed from 1. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e13558b440..6c07253bce 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1028,7 +1028,7 @@ described first. .. prodn:: strategy_level ::= opaque - | @int + | @integer | expand | transparent strategy_level_or_var ::= @strategy_level @@ -1052,7 +1052,7 @@ described first. + ``opaque`` : level of opaque constants. They cannot be expanded by tactics (behaves like +∞, see next item). - + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the + + :n:`@integer` : levels indexed by an integer. Level 0 corresponds to the default behavior, which corresponds to transparent constants. This level can also be referred to as ``transparent``. Negative levels correspond to constants to be expanded before normal transparent diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 8474d0287f..d31ec51d52 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1887,7 +1887,7 @@ Tactic notations allow customizing the syntax of tactics. - :tacn:`refine` * - ``integer`` - - :token:`int` + - :token:`integer` - an integer - diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index fbf83760ad..89009764c8 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -736,11 +736,6 @@ export_token: [ ] (* lexer stuff *) -integer: [ | DELETENT ] -RENAME: [ -| integer int (* todo: review uses in .mlg files, some should be "natural" *) -] - LEFTQMARK: [ | "?" ] @@ -766,8 +761,9 @@ natural: [ | WITH [ decnat | hexnat ] ] -int: [ -| OPT "-" natural +integer: [ +| REPLACE bigint +| WITH OPT "-" natural ] number: [ @@ -1091,13 +1087,13 @@ simple_tactic: [ | WITH "subst" OPT ( LIST1 var ) | DELETE "subst" | DELETE "congruence" -| DELETE "congruence" int +| DELETE "congruence" integer | DELETE "congruence" "with" LIST1 constr -| REPLACE "congruence" int "with" LIST1 constr -| WITH "congruence" OPT int OPT ( "with" LIST1 constr ) +| REPLACE "congruence" integer "with" LIST1 constr +| WITH "congruence" OPT integer OPT ( "with" LIST1 constr ) | DELETE "show" "ltac" "profile" -| REPLACE "show" "ltac" "profile" "cutoff" int -| WITH "show" "ltac" "profile" OPT [ "cutoff" int | string ] +| REPLACE "show" "ltac" "profile" "cutoff" integer +| WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] | DELETE "show" "ltac" "profile" string (* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *) | DELETE "transparent_abstract" tactic3 @@ -1205,11 +1201,11 @@ command: [ | REPLACE "Next" "Obligation" "of" ident withtac | WITH "Next" "Obligation" OPT ( "of" ident ) withtac | DELETE "Next" "Obligation" withtac -| REPLACE "Obligation" int "of" ident ":" lglob withtac -| WITH "Obligation" int OPT ( "of" ident ) OPT ( ":" lglob withtac ) -| DELETE "Obligation" int "of" ident withtac -| DELETE "Obligation" int ":" lglob withtac -| DELETE "Obligation" int withtac +| REPLACE "Obligation" integer "of" ident ":" lglob withtac +| WITH "Obligation" integer OPT ( "of" ident ) OPT ( ":" lglob withtac ) +| DELETE "Obligation" integer "of" ident withtac +| DELETE "Obligation" integer ":" lglob withtac +| DELETE "Obligation" integer withtac | REPLACE "Obligations" "of" ident | WITH "Obligations" OPT ( "of" ident ) | DELETE "Obligations" @@ -1229,17 +1225,17 @@ command: [ | DELETE "Show" ident | "Show" OPT [ ident | natural ] | DELETE "Show" "Ltac" "Profile" -| REPLACE "Show" "Ltac" "Profile" "CutOff" int -| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ] +| REPLACE "Show" "Ltac" "Profile" "CutOff" integer +| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ] | DELETE "Show" "Ltac" "Profile" string | DELETE "Show" "Proof" (* combined with Show Proof Diffs in vernac_toplevel *) | REPLACE "Solve" "All" "Obligations" "with" tactic | WITH "Solve" "All" "Obligations" OPT ( "with" tactic ) | DELETE "Solve" "All" "Obligations" -| REPLACE "Solve" "Obligation" int "of" ident "with" tactic -| WITH "Solve" "Obligation" int OPT ( "of" ident ) "with" tactic +| REPLACE "Solve" "Obligation" integer "of" ident "with" tactic +| WITH "Solve" "Obligation" integer OPT ( "of" ident ) "with" tactic | DELETE "Solve" "Obligations" -| DELETE "Solve" "Obligation" int "with" tactic +| DELETE "Solve" "Obligation" integer "with" tactic | REPLACE "Solve" "Obligations" "of" ident "with" tactic | WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic ) | DELETE "Solve" "Obligations" "with" tactic @@ -2154,7 +2150,7 @@ tac2expr5: [ RENAME: [ | Prim.string string -| Prim.integer int +| Prim.integer integer | Prim.qualid qualid | Prim.natural natural ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 73b721702e..994447b12d 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -598,7 +598,7 @@ command: [ | "Hint" "Cut" "[" hints_path "]" opthints | "Typeclasses" "Transparent" LIST0 reference | "Typeclasses" "Opaque" LIST0 reference -| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic @@ -652,7 +652,7 @@ command: [ | "Print" "Rewrite" "HintDb" preident | "Reset" "Ltac" "Profile" | "Show" "Ltac" "Profile" -| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" "CutOff" integer | "Show" "Ltac" "Profile" string | "Show" "Lia" "Profile" (* micromega plugin *) | "Add" "Zify" "InjTyp" constr (* micromega plugin *) @@ -1715,7 +1715,7 @@ simple_tactic: [ | "stop" "ltac" "profiling" | "reset" "ltac" "profile" | "show" "ltac" "profile" -| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" "cutoff" integer | "show" "ltac" "profile" string | "restart_timer" OPT string | "finish_timing" OPT string diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a021bdbec0..105bd4668e 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -134,7 +134,7 @@ number: [ | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] -int: [ +integer: [ | OPT "-" natural ] @@ -514,7 +514,7 @@ occs_nums: [ ] int_or_var: [ -| int +| integer | ident ] @@ -686,7 +686,7 @@ scope_key: [ strategy_level: [ | "opaque" -| int +| integer | "expand" | "transparent" ] @@ -827,9 +827,9 @@ command: [ | "Comments" LIST0 [ one_term | string | natural ] | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info | "Declare" "Scope" scope_name -| "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) +| "Obligation" integer OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr ) -| "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr +| "Solve" "Obligation" integer OPT ( "of" ident ) "with" ltac_expr | "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr ) | "Solve" "All" "Obligations" OPT ( "with" ltac_expr ) | "Admit" "Obligations" OPT ( "of" ident ) @@ -852,7 +852,7 @@ command: [ | "Optimize" "Proof" | "Optimize" "Heap" | "Reset" "Ltac" "Profile" -| "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ] +| "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ] | "Show" "Lia" "Profile" (* micromega plugin *) | "Add" "Zify" "InjTyp" one_term (* micromega plugin *) | "Add" "Zify" "BinOp" one_term (* micromega plugin *) @@ -891,7 +891,7 @@ command: [ | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid -| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int +| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT integer | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ] | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ] | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr @@ -964,7 +964,7 @@ command: [ | "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ] | "Implicit" [ "Type" | "Types" ] reserv_list | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ] -| "Set" setting_name OPT [ int | string ] +| "Set" setting_name OPT [ integer | string ] | "Unset" setting_name | "Open" "Scope" scope | "Close" "Scope" scope @@ -988,7 +988,7 @@ command: [ | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body ) | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def ) | "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string -| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" int ) ":=" ltac2_expr +| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" integer ) ":=" ltac2_expr | "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) @@ -1255,7 +1255,7 @@ qhyp: [ int_or_id: [ | ident -| int (* extraction plugin *) +| integer (* extraction plugin *) ] language: [ @@ -1417,8 +1417,8 @@ simple_tactic: [ | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 | "first" "[" LIST0 ltac_expr SEP "|" "]" | "solve" "[" LIST0 ltac_expr SEP "|" "]" -| "idtac" LIST0 [ ident | string | int ] -| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ] +| "idtac" LIST0 [ ident | string | integer ] +| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | integer ] | "fun" LIST1 name "=>" ltac_expr | "eval" red_expr "in" term | "context" ident "[" term "]" @@ -1462,7 +1462,7 @@ simple_tactic: [ | "evar" "(" ident ":" term ")" | "evar" one_term | "instantiate" "(" ident ":=" term ")" -| "instantiate" "(" int ":=" term ")" OPT hloc +| "instantiate" "(" integer ":=" term ")" OPT hloc | "instantiate" | "stepl" one_term OPT ( "by" ltac_expr ) | "stepr" one_term OPT ( "by" ltac_expr ) @@ -1501,7 +1501,7 @@ simple_tactic: [ | "start" "ltac" "profiling" | "stop" "ltac" "profiling" | "reset" "ltac" "profile" -| "show" "ltac" "profile" OPT [ "cutoff" int | string ] +| "show" "ltac" "profile" OPT [ "cutoff" integer | string ] | "restart_timer" OPT string | "finish_timing" OPT ( "(" string ")" ) OPT string | "eassumption" @@ -1606,7 +1606,7 @@ simple_tactic: [ | "change_no_check" conversion OPT clause_dft_concl | "btauto" | "rtauto" -| "congruence" OPT int OPT ( "with" LIST1 one_term ) +| "congruence" OPT integer OPT ( "with" LIST1 one_term ) | "f_equal" | "firstorder" OPT ltac_expr firstorder_rhs | "gintuition" OPT ltac_expr @@ -2035,7 +2035,7 @@ tac2rec_field: [ ltac2_scope: [ | string (* Ltac2 plugin *) -| int (* Ltac2 plugin *) +| integer (* Ltac2 plugin *) | name (* Ltac2 plugin *) | name "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) ] @@ -2085,7 +2085,7 @@ ltac2_expr0: [ ] ltac2_tactic_atom: [ -| int (* Ltac2 plugin *) +| integer (* Ltac2 plugin *) | string (* Ltac2 plugin *) | qualid (* Ltac2 plugin *) | "@" ident (* Ltac2 plugin *) @@ -2201,7 +2201,7 @@ with_names: [ ] occurrences: [ -| LIST1 int +| LIST1 integer | ident ] @@ -2296,7 +2296,7 @@ ltac_expr0: [ ] tactic_atom: [ -| int +| integer | qualid | "()" ] diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 35c90444b1..8d197e6056 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index eb9d9cbdce..e5309ea441 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -55,7 +55,7 @@ END TACTIC EXTEND show_ltac_profile | [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff } -| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } +| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } | [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s } END @@ -74,7 +74,7 @@ END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY | [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff } -| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) } +| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) } END VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY -- cgit v1.2.3 From 031cc2ba1a19a06766df85b8693c72f16fa62de6 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 7 Sep 2020 12:07:23 +0200 Subject: [refman] Explicit integer and natural As respectively bigint and bignat that fit into an OCaml int. --- doc/sphinx/language/core/basic.rst | 14 +++++++++----- doc/sphinx/user-extensions/syntax-extensions.rst | 24 ++++++++++++------------ doc/tools/docgram/common.edit_mlg | 6 ++---- doc/tools/docgram/orderedGrammar | 12 ++++++++++-- 4 files changed, 33 insertions(+), 23 deletions(-) diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index d248839fa0..9308da6d27 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -114,9 +114,9 @@ Identifiers Numbers Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals - start with ``0x`` or ``0X``. :n:`@int` is an integer; - a number without fractional nor exponent parts. :n:`@natural` is a non-negative - integer. Underscores embedded in the digits are ignored, for example + start with ``0x`` or ``0X``. :n:`@bigint` are integers; + numbers without fractional nor exponent parts. :n:`@bignat` are non-negative + integers. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. .. insertprodn number hexdigit @@ -125,13 +125,17 @@ Numbers number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } integer ::= {? - } @natural - natural ::= {| @decnat | @hexnat } + natural ::= @bignat + bigint ::= {? - } @bignat + bignat ::= {| @decnat | @hexnat } decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } hexdigit ::= {| 0 .. 9 | a .. f | A .. F } - .. todo PR need some code fixes for hex, see PR 11948 + :n:`@integer` and :n:`@natural` are limited to the range that fits + into an OCaml integer (63-bit integers on most architectures). + :n:`@bigint` and :n:`@bignat` have no range limitation. Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d31ec51d52..e8b1add95e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1544,8 +1544,8 @@ Numeral notations .. insertprodn numeral_modifier numeral_modifier .. prodn:: - numeral_modifier ::= ( warning after @number ) - | ( abstract after @number ) + numeral_modifier ::= ( warning after @bignat ) + | ( abstract after @bignat ) This command allows the user to customize the way numeral literals are parsed and printed. @@ -1591,33 +1591,33 @@ Numeral notations function application, constructors, inductive type families, sorts, and primitive integers) will be considered for printing. - :n:`( warning after @number )` + :n:`( warning after @bignat )` displays a warning message about a possible stack - overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@number`. + overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`. .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(warning after @number)`, this warning is emitted when - parsing a number greater than or equal to :token:`number`. + with :n:`(warning after @bignat)`, this warning is emitted when + parsing a number greater than or equal to :token:`bignat`. - :n:`( abstract after @number )` + :n:`( abstract after @bignat )` returns :n:`(@qualid__parse m)` when parsing a literal - :n:`m` that's greater than :n:`@number` rather than reducing it to a normal form. + :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form. Here :g:`m` will be a :g:`Numeral.int` or :g:`Numeral.uint` or :g:`Z`, depending on the type of the parsing function :n:`@qualid__parse`. This allows for a more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a - warning will be emitted when an integer larger than :token:`number` - is parsed. Note that :n:`(abstract after @number)` has no effect + warning will be emitted when an integer larger than :token:`bignat` + is parsed. Note that :n:`(abstract after @bignat)` has no effect when :n:`@qualid__parse` lands in an :g:`option` type. .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @qualid__parse. When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(abstract after @number)`, this warning is emitted when - parsing a number greater than or equal to :token:`number`. + with :n:`(abstract after @bignat)`, this warning is emitted when + parsing a number greater than or equal to :token:`bignat`. Typically, this indicates that the fully computed representation of numbers can be so large that non-tail-recursive OCaml functions run out of stack space when trying to walk them. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 89009764c8..ea60fa22d6 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -756,8 +756,8 @@ hexnat: [ | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ] ] -natural: [ -| REPLACE bignat +bignat: [ +| REPLACE NUMBER | WITH [ decnat | hexnat ] ] @@ -2197,7 +2197,6 @@ ltac2_induction_clause: [ SPLICE: [ | clause | noedit_mode -| bigint | match_list | match_context_list | IDENT @@ -2360,7 +2359,6 @@ SPLICE: [ | search_queries | locatable | scope_delimiter -| bignat | one_import_filter_name | search_where | message_token diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 105bd4668e..8d4e0189e6 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -139,6 +139,14 @@ integer: [ ] natural: [ +| bignat +] + +bigint: [ +| OPT "-" bignat +] + +bignat: [ | [ decnat | hexnat ] ] @@ -1291,8 +1299,8 @@ field_mod: [ ] numeral_modifier: [ -| "(" "warning" "after" number ")" -| "(" "abstract" "after" number ")" +| "(" "warning" "after" bignat ")" +| "(" "abstract" "after" bignat ")" ] hints_path: [ -- cgit v1.2.3 From 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 8 Sep 2020 10:41:03 +0200 Subject: Turn integer into natural in several mlgs Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 . --- doc/sphinx/proof-engine/ltac.rst | 2 +- doc/sphinx/proof-engine/ltac2.rst | 2 +- doc/tools/docgram/common.edit_mlg | 16 ++++++++-------- doc/tools/docgram/fullGrammar | 16 ++++++++-------- doc/tools/docgram/orderedGrammar | 10 +++++----- plugins/ltac/g_ltac.mlg | 2 +- plugins/ltac/g_obligations.mlg | 12 ++++++------ user-contrib/Ltac2/g_ltac2.mlg | 2 +- 8 files changed, 31 insertions(+), 31 deletions(-) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2a102adfcc..f18569c7fd 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -876,7 +876,7 @@ Print/identity tactic: idtac ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: idtac {* {| @ident | @string | @integer } } +.. tacn:: idtac {* {| @ident | @string | @natural } } :name: idtac Leaves the proof unchanged and prints the given tokens. Strings and integers are printed diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b4f32c6cbb..773e393eb6 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1159,7 +1159,7 @@ Match on values Notations --------- -.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @integer } := @ltac2_expr +.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr :name: Ltac2 Notation .. todo seems like name maybe should use lident rather than ident, considering: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index ea60fa22d6..66b6ffac89 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1201,11 +1201,11 @@ command: [ | REPLACE "Next" "Obligation" "of" ident withtac | WITH "Next" "Obligation" OPT ( "of" ident ) withtac | DELETE "Next" "Obligation" withtac -| REPLACE "Obligation" integer "of" ident ":" lglob withtac -| WITH "Obligation" integer OPT ( "of" ident ) OPT ( ":" lglob withtac ) -| DELETE "Obligation" integer "of" ident withtac -| DELETE "Obligation" integer ":" lglob withtac -| DELETE "Obligation" integer withtac +| REPLACE "Obligation" natural "of" ident ":" lglob withtac +| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" lglob withtac ) +| DELETE "Obligation" natural "of" ident withtac +| DELETE "Obligation" natural ":" lglob withtac +| DELETE "Obligation" natural withtac | REPLACE "Obligations" "of" ident | WITH "Obligations" OPT ( "of" ident ) | DELETE "Obligations" @@ -1232,10 +1232,10 @@ command: [ | REPLACE "Solve" "All" "Obligations" "with" tactic | WITH "Solve" "All" "Obligations" OPT ( "with" tactic ) | DELETE "Solve" "All" "Obligations" -| REPLACE "Solve" "Obligation" integer "of" ident "with" tactic -| WITH "Solve" "Obligation" integer OPT ( "of" ident ) "with" tactic +| REPLACE "Solve" "Obligation" natural "of" ident "with" tactic +| WITH "Solve" "Obligation" natural OPT ( "of" ident ) "with" tactic | DELETE "Solve" "Obligations" -| DELETE "Solve" "Obligation" integer "with" tactic +| DELETE "Solve" "Obligation" natural "with" tactic | REPLACE "Solve" "Obligations" "of" ident "with" tactic | WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic ) | DELETE "Solve" "Obligations" "with" tactic diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 994447b12d..9614fc06fe 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -606,14 +606,14 @@ command: [ | "Locate" "Ltac" reference | "Ltac" LIST1 ltac_tacdef_body SEP "with" | "Print" "Ltac" "Signatures" -| "Obligation" integer "of" ident ":" lglob withtac -| "Obligation" integer "of" ident withtac -| "Obligation" integer ":" lglob withtac -| "Obligation" integer withtac +| "Obligation" natural "of" ident ":" lglob withtac +| "Obligation" natural "of" ident withtac +| "Obligation" natural ":" lglob withtac +| "Obligation" natural withtac | "Next" "Obligation" "of" ident withtac | "Next" "Obligation" withtac -| "Solve" "Obligation" integer "of" ident "with" tactic -| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligation" natural "of" ident "with" tactic +| "Solve" "Obligation" natural "with" tactic | "Solve" "Obligations" "of" ident "with" tactic | "Solve" "Obligations" "with" tactic | "Solve" "Obligations" @@ -2099,7 +2099,7 @@ match_list: [ message_token: [ | identref | STRING -| integer +| natural ] ltac_def_kind: [ @@ -2811,7 +2811,7 @@ sexpr: [ syn_level: [ | (* Ltac2 plugin *) -| ":" Prim.integer (* Ltac2 plugin *) +| ":" Prim.natural (* Ltac2 plugin *) ] tac2def_syn: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 8d4e0189e6..bbc4edf199 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -835,9 +835,9 @@ command: [ | "Comments" LIST0 [ one_term | string | natural ] | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info | "Declare" "Scope" scope_name -| "Obligation" integer OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) +| "Obligation" natural OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr ) -| "Solve" "Obligation" integer OPT ( "of" ident ) "with" ltac_expr +| "Solve" "Obligation" natural OPT ( "of" ident ) "with" ltac_expr | "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr ) | "Solve" "All" "Obligations" OPT ( "with" ltac_expr ) | "Admit" "Obligations" OPT ( "of" ident ) @@ -996,7 +996,7 @@ command: [ | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body ) | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def ) | "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string -| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" integer ) ":=" ltac2_expr +| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" natural ) ":=" ltac2_expr | "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) @@ -1425,8 +1425,8 @@ simple_tactic: [ | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 | "first" "[" LIST0 ltac_expr SEP "|" "]" | "solve" "[" LIST0 ltac_expr SEP "|" "]" -| "idtac" LIST0 [ ident | string | integer ] -| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | integer ] +| "idtac" LIST0 [ ident | string | natural ] +| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ] | "fun" LIST1 name "=>" ltac_expr | "eval" red_expr "in" term | "context" ident "[" term "]" diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 114acaa412..78cde2cde8 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram message_token: [ [ id = identref -> { MsgIdent id } | s = STRING -> { MsgString s } - | n = integer -> { MsgInt n } ] ] + | n = natural -> { MsgInt n } ] ] ; ltac_def_kind: diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index fa176482bf..a6673699af 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" natural(num) withtac(tac) ] -> { obligation (num, None, None) tac } | [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } @@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_ END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> +| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] -> { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) } -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> +| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] -> { try_solve_obligation num None (Some (Tacinterp.interp t)) } END diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index bec9632e84..d42a935104 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -371,7 +371,7 @@ GRAMMAR EXTEND Gram ; syn_level: [ [ -> { None } - | ":"; n = Prim.integer -> { Some n } + | ":"; n = Prim.natural -> { Some n } ] ] ; tac2def_syn: -- cgit v1.2.3 From d5eb564a1ae46409e90a2c6bd6af5b77aa37773e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 9 Sep 2020 20:24:46 +0200 Subject: Adding a wit_natural standard argument. --- doc/tools/docgram/common.edit_mlg | 6 +++--- doc/tools/docgram/fullGrammar | 5 +++-- doc/tools/docgram/orderedGrammar | 3 ++- interp/stdarg.ml | 4 ++++ interp/stdarg.mli | 3 +++ parsing/pcoq.ml | 1 + plugins/cc/g_congruence.mlg | 4 ++-- plugins/ltac/tacinterp.ml | 3 +++ 8 files changed, 21 insertions(+), 8 deletions(-) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 66b6ffac89..a22f7ae9f3 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1087,10 +1087,10 @@ simple_tactic: [ | WITH "subst" OPT ( LIST1 var ) | DELETE "subst" | DELETE "congruence" -| DELETE "congruence" integer +| DELETE "congruence" natural | DELETE "congruence" "with" LIST1 constr -| REPLACE "congruence" integer "with" LIST1 constr -| WITH "congruence" OPT integer OPT ( "with" LIST1 constr ) +| REPLACE "congruence" natural "with" LIST1 constr +| WITH "congruence" OPT natural OPT ( "with" LIST1 constr ) | DELETE "show" "ltac" "profile" | REPLACE "show" "ltac" "profile" "cutoff" integer | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 9614fc06fe..2ee8e4347e 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -689,6 +689,7 @@ command: [ | "Print" "Rings" (* setoid_ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) +| "Number" "Notation" reference reference reference ":" ident numnotoption | "Numeral" "Notation" reference reference reference ":" ident numnotoption | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) @@ -1435,9 +1436,9 @@ constr_as_binder_kind: [ simple_tactic: [ | "btauto" | "congruence" -| "congruence" integer +| "congruence" natural | "congruence" "with" LIST1 constr -| "congruence" integer "with" LIST1 constr +| "congruence" natural "with" LIST1 constr | "f_equal" | "firstorder" OPT tactic firstorder_using | "firstorder" OPT tactic "with" LIST1 preident diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index bbc4edf199..aae96fc966 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -896,6 +896,7 @@ command: [ | "Print" "Rings" (* setoid_ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) +| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid @@ -1614,7 +1615,7 @@ simple_tactic: [ | "change_no_check" conversion OPT clause_dft_concl | "btauto" | "rtauto" -| "congruence" OPT integer OPT ( "with" LIST1 one_term ) +| "congruence" OPT natural OPT ( "with" LIST1 one_term ) | "f_equal" | "firstorder" OPT ltac_expr firstorder_rhs | "gintuition" OPT ltac_expr diff --git a/interp/stdarg.ml b/interp/stdarg.ml index d5f104b7f8..343f85be03 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -25,6 +25,9 @@ let wit_bool : bool uniform_genarg_type = let wit_int : int uniform_genarg_type = make0 "int" +let wit_nat : int uniform_genarg_type = + make0 "nat" + let wit_string : string uniform_genarg_type = make0 "string" @@ -59,6 +62,7 @@ let wit_clause_dft_concl = (** Aliases for compatibility *) let wit_integer = wit_int +let wit_natural = wit_nat let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 89bdd78c70..3ae8b7d73f 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -23,6 +23,8 @@ val wit_unit : unit uniform_genarg_type val wit_bool : bool uniform_genarg_type +val wit_nat : int uniform_genarg_type + val wit_int : int uniform_genarg_type val wit_string : string uniform_genarg_type @@ -54,6 +56,7 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, (** Aliases for compatibility *) +val wit_natural : int uniform_genarg_type val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b9853029a0..0d74ad928c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -500,6 +500,7 @@ let with_grammar_rule_protection f x = let () = let open Stdarg in + Grammar.register0 wit_nat (Prim.natural); Grammar.register0 wit_int (Prim.integer); Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg index 3920e3da75..2c91901477 100644 --- a/plugins/cc/g_congruence.mlg +++ b/plugins/cc/g_congruence.mlg @@ -22,9 +22,9 @@ DECLARE PLUGIN "cc_plugin" TACTIC EXTEND cc | [ "congruence" ] -> { congruence_tac 1000 [] } -| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" natural(n) ] -> { congruence_tac n [] } | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } - |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> +| [ "congruence" natural(n) "with" ne_constr_list(l) ] -> { congruence_tac n l } END diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 88480194c8..2258201c22 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2027,6 +2027,9 @@ let () = let () = declare_uniform wit_int +let () = + declare_uniform wit_nat + let () = declare_uniform wit_bool -- cgit v1.2.3 From 6551f14196784e323688e682877229bc7f901659 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 9 Sep 2020 23:33:05 +0200 Subject: Rename Numeral Notation command to Number Notation Keep Numeral Notation wit a deprecation warning. --- doc/changelog/03-notations/12979-doc-numbers.rst | 4 + doc/sphinx/changes.rst | 6 +- doc/sphinx/user-extensions/syntax-extensions.rst | 26 +- plugins/syntax/g_numeral.mlg | 12 +- test-suite/interactive/PrimNotation.v | 12 +- test-suite/output/Notations4.v | 2 +- test-suite/output/NumberNotations.out | 236 +++++++++++ test-suite/output/NumberNotations.v | 489 +++++++++++++++++++++++ test-suite/output/NumeralNotations.out | 236 ----------- test-suite/output/NumeralNotations.v | 489 ----------------------- test-suite/output/ZSyntax.v | 2 +- test-suite/output/bug_12159.v | 4 +- test-suite/output/sint63Notation.v | 4 +- test-suite/success/NumeralNotationsNoLocal.v | 2 +- theories/Init/Decimal.v | 4 +- theories/Init/Hexadecimal.v | 2 +- theories/Init/Numeral.v | 2 +- theories/Init/Prelude.v | 12 +- theories/NArith/BinNat.v | 2 +- theories/NArith/BinNatDef.v | 4 +- theories/Numbers/AltBinNotations.v | 10 +- theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/PArith/BinPos.v | 2 +- theories/PArith/BinPosDef.v | 4 +- theories/QArith/QArith_base.v | 2 +- theories/ZArith/BinInt.v | 2 +- theories/ZArith/BinIntDef.v | 4 +- 27 files changed, 795 insertions(+), 781 deletions(-) create mode 100644 doc/changelog/03-notations/12979-doc-numbers.rst create mode 100644 test-suite/output/NumberNotations.out create mode 100644 test-suite/output/NumberNotations.v delete mode 100644 test-suite/output/NumeralNotations.out delete mode 100644 test-suite/output/NumeralNotations.v diff --git a/doc/changelog/03-notations/12979-doc-numbers.rst b/doc/changelog/03-notations/12979-doc-numbers.rst new file mode 100644 index 0000000000..631bd6ec69 --- /dev/null +++ b/doc/changelog/03-notations/12979-doc-numbers.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + :n:`Numeral Notation`, please use :ref:`Number Notation ` instead. + (`#12979 `_, + by Pierre Roux). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 191eae6430..af66efa95e 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2009,7 +2009,7 @@ reference manual. Here are the most important user-visible changes: inductive types (`#8965 `_, by Jason Gross). - - Experimental: :ref:`Numeral Notations ` now parse decimal + - Experimental: :ref:`Number Notations ` now parse decimal constants such as ``1.02e+01`` or ``10.2``. Parsers added for :g:`Q` and :g:`R`. In the rare case when such numeral notations were used in a development along with :g:`Q` or :g:`R`, they may have to be removed or @@ -2281,7 +2281,7 @@ Other changes in 8.10+beta1 parentheses on abbreviations shortening a strict prefix of an application, by Hugo Herbelin). - - :cmd:`Numeral Notation` now support inductive types in the input to + - :cmd:`Number Notation` now support inductive types in the input to printing functions (e.g., numeral notations can be defined for terms containing things like :g:`@cons nat O O`), and parsing functions now fully normalize terms including parameters of constructors (so that, @@ -2782,7 +2782,7 @@ changes: next version of |Coq|, see the next subsection for a script to ease porting, by Jason Gross and Jean-Christophe Léchenet. - - Added the :cmd:`Numeral Notation` command for registering decimal + - Added the :cmd:`Number Notation` command for registering decimal numeral notations for custom types, by Daniel de Rauglaudre, Pierre Letouzey and Jason Gross. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e8b1add95e..8184e37163 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1125,7 +1125,7 @@ are currently open. For instance, the infix symbol ``+`` can be used to refer to distinct definitions of the addition operator, such as for natural numbers, integers or reals. Notation scopes can include an interpretation for numbers and -strings with the :cmd:`Numeral Notation` and :cmd:`String Notation` commands. +strings with the :cmd:`Number Notation` and :cmd:`String Notation` commands. .. insertprodn scope scope_key @@ -1533,13 +1533,13 @@ numbers (see :ref:`datatypes`). Negative integers are not at the same level as :n:`@natural`, for this would make precedence unnatural. -.. _numeral-notations: +.. _number-notations: -Numeral notations -~~~~~~~~~~~~~~~~~ +Number notations +~~~~~~~~~~~~~~~~ -.. cmd:: Numeral Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } - :name: Numeral Notation +.. cmd:: Number Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } + :name: Number Notation .. insertprodn numeral_modifier numeral_modifier @@ -1597,7 +1597,7 @@ Numeral notations .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). - When a :cmd:`Numeral Notation` is registered in the current scope + When a :cmd:`Number Notation` is registered in the current scope with :n:`(warning after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. @@ -1615,7 +1615,7 @@ Numeral notations .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @qualid__parse. - When a :cmd:`Numeral Notation` is registered in the current scope + When a :cmd:`Number Notation` is registered in the current scope with :n:`(abstract after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. Typically, this indicates that the fully computed representation @@ -1638,12 +1638,12 @@ Numeral notations .. exn:: @qualid__parse should go from Numeral.int to @type or (option @type). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). - The parsing function given to the :cmd:`Numeral Notation` + The parsing function given to the :cmd:`Number Notation` vernacular is not of the right type. .. exn:: @qualid__print should go from @type to Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). - The printing function given to the :cmd:`Numeral Notation` + The printing function given to the :cmd:`Number Notation` vernacular is not of the right type. .. exn:: Unexpected term @term while parsing a numeral notation. @@ -1745,19 +1745,19 @@ The following errors apply to both string and numeral notations: .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`String Notation` or :cmd:`Numeral Notation` must be a single qualified + The type passed to :cmd:`String Notation` or :cmd:`Number Notation` must be a single qualified identifier. .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`String Notation` or :cmd:`Numeral Notation` must be single qualified + Both functions passed to :cmd:`String Notation` or :cmd:`Number Notation` must be single qualified identifiers. .. todo: generally we don't document syntax errors. Is this a good execption? .. exn:: @qualid is bound to a notation that does not denote a reference. - Identifiers passed to :cmd:`String Notation` or :cmd:`Numeral Notation` must be global + Identifiers passed to :cmd:`String Notation` or :cmd:`Number Notation` must be global references, or notations which evaluate to single qualified identifiers. .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703 diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index e66dbe17b2..c030925ea9 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -24,6 +24,11 @@ let pr_numnot_option = function | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + } VERNAC ARGUMENT EXTEND numnotoption @@ -34,8 +39,13 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v index 07986b0df3..55116dc78b 100644 --- a/test-suite/interactive/PrimNotation.v +++ b/test-suite/interactive/PrimNotation.v @@ -21,7 +21,7 @@ Local Set Universe Polymorphism. Delimit Scope punit_scope with punit. Delimit Scope pcunit_scope with pcunit. Delimit Scope int_scope with int. -Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Number Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. Module A. NonCumulative Inductive punit@{u} : Type@{u} := ptt. Cumulative Inductive pcunit@{u} : Type@{u} := pctt. @@ -31,10 +31,10 @@ Module A. := fun v => match v with 0%int => Some pctt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. - Numeral Notation punit to_punit of_punit : punit_scope. + Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. Back 2. - Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Number Notation pcunit to_pcunit of_pcunit : punit_scope. Check let v := 0%punit in v : pcunit. End A. Reset A. @@ -44,7 +44,7 @@ Module A. Definition to_punit : Decimal.int -> option punit := fun v => match v with 0%int => Some ptt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. - Numeral Notation punit to_punit of_punit : punit_scope. + Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. End A. Local Set Universe Polymorphism. @@ -52,7 +52,7 @@ Inductive punit@{u} : Type@{u} := ptt. Definition to_punit : Decimal.int -> option punit := fun v => match v with 0%int => Some ptt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. -Numeral Notation punit to_punit of_punit : punit_scope. +Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. Back 6. (* check backtracking of registering universe polymorphic constants *) Local Unset Universe Polymorphism. @@ -60,5 +60,5 @@ Inductive punit : Set := ptt. Definition to_punit : Decimal.int -> option punit := fun v => match v with 0%int => Some ptt | _ => None end. Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. -Numeral Notation punit to_punit of_punit : punit_scope. +Number Notation punit to_punit of_punit : punit_scope. Check let v := 0%punit in v : punit. diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 73445bad12..6dadd8c7fe 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -131,7 +131,7 @@ Module NumeralNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Numeral Notation myint63 of_int to_int : test17_scope. + Number Notation myint63 of_int to_int : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumeralNotations. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out new file mode 100644 index 0000000000..8065c8d311 --- /dev/null +++ b/test-suite/output/NumberNotations.out @@ -0,0 +1,236 @@ +The command has indeed failed with message: +Unexpected term (nat -> nat) while parsing a numeral notation. +The command has indeed failed with message: +Unexpected non-option term opaque4 while parsing a numeral notation. +The command has indeed failed with message: +Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral +notation. +let v := 0%ppp in v : punit + : punit +let v := 0%ppp in v : punit + : punit +let v := 0%ppp in v : punit + : punit +let v := 0%ppp in v : punit + : punit +let v := 0%uto in v : unit + : unit +The command has indeed failed with message: +Cannot interpret this number as a value of type unit +The command has indeed failed with message: +Cannot interpret this number as a value of type unit +let v := 0%upp in v : unit + : unit +let v := 0%upp in v : unit + : unit +let v := 0%upp in v : unit + : unit +let v := 0%ppps in v : punit + : punit +File "stdin", line 91, characters 2-46: +Warning: To avoid stack overflow, large numbers in punit are interpreted as +applications of pto_punits. [abstract-large-number,numbers] +The command has indeed failed with message: +In environment +v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit +The term "v" has type "punit@{Set}" while it is expected to have type + "punit@{u}". +S + : nat -> nat +S (ack 4 4) + : nat +let v := 0%wnat in v : wnat + : wnat +0%wnat + : wnat +{| unwrap := ack 4 4 |} + : wnat +{| Test6.unwrap := 0 |} + : Test6.wnat +let v := 0%wnat in v : Test6.wnat + : Test6.wnat +let v := 0%wuint in v : wuint + : wuint +let v := 1%wuint in v : wuint + : wuint +let v := 0%wuint8 in v : wuint + : wuint +let v := 0 in v : nat + : nat +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "wuint". + = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} + : wuint +let v := 0%wuint8' in v : wuint + : wuint +let v := 0%wuint9 in v : wuint + : wuint +let v := 0%wuint9' in v : wuint + : wuint +let v := 0 in v : nat + : nat +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "wuint". +File "stdin", line 203, characters 2-71: +Warning: The 'abstract after' directive has no effect when the parsing +function (of_uint) targets an option type. +[abstract-large-number-no-op,numbers] +The command has indeed failed with message: +The 'abstract after' directive has no effect when the parsing function +(of_uint) targets an option type. [abstract-large-number-no-op,numbers] +let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit + : unit +let v := 0%test13 in v : unit + : unit +The command has indeed failed with message: +to_uint' is bound to a notation that does not denote a reference. +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +to_uint'' is bound to a notation that does not denote a reference. +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +let v := 0%test14' in v : unit + : unit +let v := 0%test14' in v : unit + : unit +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +let v := 0%test14' in v : unit + : unit +The command has indeed failed with message: +This command does not support the Global option in sections. +let v := 0%test14'' in v : unit + : unit +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +The command has indeed failed with message: +In environment +v := 0 : nat +The term "v" has type "nat" while it is expected to have type "unit". +let v := 0%test15 in v : unit + : unit +let v := 0%test15 in v : unit + : unit +let v := 0%test15 in v : unit + : unit +let v := foo a.t in v : Foo + : Foo +The command has indeed failed with message: +Cannot interpret in test16_scope because NumberNotations.Test16.F.Foo could not be found in the current environment. +let v := 0%test17 in v : myint63 + : myint63 +let v := 0%Q in v : Q + : Q +let v := 1%Q in v : Q + : Q +let v := 2%Q in v : Q + : Q +let v := 3%Q in v : Q + : Q +let v := 4%Q in v : Q + : Q + = (0, 1) + : nat * nat + = (1, 1) + : nat * nat + = (2, 1) + : nat * nat + = (3, 1) + : nat * nat + = (4, 1) + : nat * nat +let v := (-1)%Zlike in v : Zlike + : Zlike +let v := 0%Zlike in v : Zlike + : Zlike +let v := 1%Zlike in v : Zlike + : Zlike +let v := 2%Zlike in v : Zlike + : Zlike +let v := 3%Zlike in v : Zlike + : Zlike +let v := 4%Zlike in v : Zlike + : Zlike +2%Zlike + : Zlike +0%Zlike + : Zlike +let v := 0%kt in v : ty + : ty +let v := 1%kt in v : ty + : ty +let v := 2%kt in v : ty + : ty +let v := 3%kt in v : ty + : ty +let v := 4%kt in v : ty + : ty +let v := 5%kt in v : ty + : ty +The command has indeed failed with message: +Cannot interpret this number as a value of type ty + = 0%kt + : ty + = 1%kt + : ty + = 2%kt + : ty + = 3%kt + : ty + = 4%kt + : ty + = 5%kt + : ty +let v : ty := Build_ty Empty_set zero in v : ty + : ty +let v : ty := Build_ty unit one in v : ty + : ty +let v : ty := Build_ty bool two in v : ty + : ty +let v : ty := Build_ty Prop prop in v : ty + : ty +let v : ty := Build_ty Set set in v : ty + : ty +let v : ty := Build_ty Type type in v : ty + : ty +1 + : nat +(-1000)%Z + : Z +0 + : Prop ++0 + : bool +-0 + : bool +00 + : nat * nat +1000 + : Prop +1_000 + : list nat diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v new file mode 100644 index 0000000000..e411005da3 --- /dev/null +++ b/test-suite/output/NumberNotations.v @@ -0,0 +1,489 @@ +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +Declare Scope opaque_scope. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Number Notation Numeral.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Numeral.int. + Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. + Number Notation Numeral.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Declare Scope silly_scope. + +Module Test3. + Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). + Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Number Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + +Module Test4. + Declare Scope opaque_scope. + Declare Scope silly_scope. + Declare Scope pto. + Declare Scope ppo. + Declare Scope ptp. + Declare Scope ppp. + Declare Scope uto. + Declare Scope upo. + Declare Scope utp. + Declare Scope upp. + Declare Scope ppps. + Polymorphic NonCumulative Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. + Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Number Notation punit to_punit of_punit : pto. + Number Notation punit pto_punit of_punit : ppo. + Number Notation punit to_punit pof_punit : ptp. + Number Notation punit pto_punit pof_punit : ppp. + Number Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. + Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Number Notation unit pto_unit of_unit : upo. + Number Notation unit to_unit pof_unit : utp. + Number Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Number Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) +End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + Local Set Primitive Projections. + Record > wnat := wrap { unwrap :> nat }. + Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x. + Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. + Module Export Scopes. + Declare Scope wnat_scope. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Number Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Set Printing Coercions. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Numeral.uint }. + Declare Scope wuint_scope. + Delimit Scope wuint_scope with wuint. + Number Notation wuint wrap unwrap : wuint_scope. + Check let v := 0%wuint in v : wuint. + Check let v := 1%wuint in v : wuint. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Numeral.uint }. + Declare Scope wuint8_scope. + Declare Scope wuint8'_scope. + Delimit Scope wuint8_scope with wuint8. + Delimit Scope wuint8'_scope with wuint8'. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Number Notation wuint wrap' unwrap' : wuint8_scope. + Check let v := 0%wuint8 in v : wuint. + End with_var. + Check let v := 0%wuint8 in v : nat. + Fail Check let v := 0%wuint8 in v : wuint. + Compute wrap (Nat.to_num_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Number Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. +End Test8. + +Module Test9. + Declare Scope wuint9_scope. + Declare Scope wuint9'_scope. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. + Section with_let. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Numeral.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Number Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Number Notation wuint wrap'' unwrap'' : wuint9'_scope. + Check let v := 0%wuint9' in v : wuint. + End with_let. + Check let v := 0%wuint9 in v : nat. + Fail Check let v := 0%wuint9 in v : wuint. +End Test9. + +Module Test10. + (* Test that it is only a warning to add abstract after to an optional parsing function *) + Definition to_uint (v : unit) := Nat.to_num_uint 0. + Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Numeral.uint) := tt. + Declare Scope unit_scope. + Declare Scope unit2_scope. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Number Notation unit of_uint to_uint : unit_scope (abstract after 1). + Local Set Warnings Append "+abstract-large-number-no-op". + (* Check that there is actually a warning here *) + Fail Number Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Number Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. + +Module Test12. + (* Test for numeral notations on context variables *) + Declare Scope test12_scope. + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). + + Number Notation unit of_uint to_uint : test12_scope. + Check let v := 1%test12 in v : unit. + End test12. +End Test12. + +Module Test13. + (* Test for numeral notations on notations which do not denote references *) + Declare Scope test13_scope. + Declare Scope test13'_scope. + Declare Scope test13''_scope. + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Number Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Number Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Number Notation unit of_uint to_uint'' : test13''_scope. + Fail Check let v := 0%test13'' in v : unit. +End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test that [Local Number Notation]s do not escape modules + nor sections. *) + Declare Scope test14_scope. + Declare Scope test14'_scope. + Declare Scope test14''_scope. + Declare Scope test14'''_scope. + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Delimit Scope test14''_scope with test14''. + Delimit Scope test14'''_scope with test14'''. + Module Inner. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Local Number Notation unit of_uint to_uint : test14_scope. + Global Number Notation unit of_uint to_uint : test14'_scope. + Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Fail Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + Section InnerSection. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Local Number Notation unit of_uint to_uint : test14''_scope. + Fail Global Number Notation unit of_uint to_uint : test14'''_scope. + Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. + End InnerSection. + Fail Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. +End Test14. + +Module Test15. + (** Test module include *) + Declare Scope test15_scope. + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. + Number Notation unit of_uint to_uint : test15_scope. + Check let v := 0%test15 in v : unit. + End Inner. + Module Inner2. + Include Inner. + Check let v := 0%test15 in v : unit. + End Inner2. + Import Inner Inner2. + Check let v := 0%test15 in v : unit. +End Test15. + +Module Test16. + (** Test functors *) + Declare Scope test16_scope. + Delimit Scope test16_scope with test16. + Module Type A. + Axiom T : Set. + Axiom t : T. + End A. + Module F (a : A). + Inductive Foo := foo (_ : a.T). + Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : Foo := foo a.t. + Global Number Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. + End F. + Module a <: A. + Definition T : Set := unit. + Definition t : T := tt. + End a. + Module Import f := F a. + (** Ideally this should work, but it should definitely not anomaly *) + Fail Check let v := 0%test16 in v : Foo. +End Test16. + +Require Import Coq.Numbers.Cyclic.Int63.Int63. +Module Test17. + (** Test int63 *) + Declare Scope test17_scope. + Declare Scope test17_scope. + Delimit Scope test17_scope with test17. + Local Set Primitive Projections. + Record myint63 := of_int { to_int : int }. + Number Notation myint63 of_int to_int : test17_scope. + Check let v := 0%test17 in v : myint63. +End Test17. + +Module Test18. + (** Test https://github.com/coq/coq/issues/9840 *) + Record Q := { num : nat ; den : nat ; reduced : Nat.gcd num den = 1 }. + Declare Scope Q_scope. + Delimit Scope Q_scope with Q. + + Definition nat_eq_dec (x y : nat) : {x = y} + {x <> y}. + Proof. decide equality. Defined. + + Definition transparentify {A} (D : {A} + {not A}) (H : A) : A := + match D with + | left pf => pf + | right npf => match npf H with end + end. + + Axiom gcd_good : forall x, Nat.gcd x 1 = 1. + + Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. + Definition nat_of_Q (x : Q) : option nat + := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. + Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). + Definition uint_of_Q (x : Q) : option Numeral.uint + := option_map Nat.to_num_uint (nat_of_Q x). + + Number Notation Q Q_of_uint uint_of_Q : Q_scope. + + Check let v := 0%Q in v : Q. + Check let v := 1%Q in v : Q. + Check let v := 2%Q in v : Q. + Check let v := 3%Q in v : Q. + Check let v := 4%Q in v : Q. + Compute let v := 0%Q in (num v, den v). + Compute let v := 1%Q in (num v, den v). + Compute let v := 2%Q in (num v, den v). + Compute let v := 3%Q in (num v, den v). + Compute let v := 4%Q in (num v, den v). +End Test18. + +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Module Test19. + (** Test another thing related to https://github.com/coq/coq/issues/9840 *) + Record Zlike := { summands : list Z }. + Declare Scope Zlike_scope. + Delimit Scope Zlike_scope with Zlike. + + Definition Z_of_Zlike (x : Zlike) := List.fold_right Z.add 0%Z (summands x). + Definition Zlike_of_Z (x : Z) := {| summands := cons x nil |}. + + Number Notation Zlike Zlike_of_Z Z_of_Zlike : Zlike_scope. + + Check let v := (-1)%Zlike in v : Zlike. + Check let v := 0%Zlike in v : Zlike. + Check let v := 1%Zlike in v : Zlike. + Check let v := 2%Zlike in v : Zlike. + Check let v := 3%Zlike in v : Zlike. + Check let v := 4%Zlike in v : Zlike. + Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. + Check {| summands := nil |}. +End Test19. + +Module Test20. + (** Test Sorts *) + Local Set Universe Polymorphism. + Inductive known_type : Type -> Type := + | prop : known_type Prop + | set : known_type Set + | type : known_type Type + | zero : known_type Empty_set + | one : known_type unit + | two : known_type bool. + + Existing Class known_type. + Existing Instances zero one two prop. + Existing Instance set | 2. + Existing Instance type | 4. + + Record > ty := { t : Type ; kt : known_type t }. + + Definition ty_of_uint (x : Numeral.uint) : option ty + := match Nat.of_num_uint x with + | 0 => @Some ty zero + | 1 => @Some ty one + | 2 => @Some ty two + | 3 => @Some ty prop + | 4 => @Some ty set + | 5 => @Some ty type + | _ => None + end. + Definition uint_of_ty (x : ty) : Numeral.uint + := Nat.to_num_uint match kt x with + | prop => 3 + | set => 4 + | type => 5 + | zero => 0 + | one => 1 + | two => 2 + end. + + Declare Scope kt_scope. + Delimit Scope kt_scope with kt. + + Number Notation ty ty_of_uint uint_of_ty : kt_scope. + + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. + Fail Check let v := 6%kt in v : ty. + Eval cbv in (_ : known_type Empty_set) : ty. + Eval cbv in (_ : known_type unit) : ty. + Eval cbv in (_ : known_type bool) : ty. + Eval cbv in (_ : known_type Prop) : ty. + Eval cbv in (_ : known_type Set) : ty. + Eval cbv in (_ : known_type Type) : ty. + Local Set Printing All. + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. +End Test20. + +Module Test21. + + Check 00001. + Check (-1_000)%Z. + +End Test21. + +Module Test22. + +Notation "0" := False. +Notation "+0" := true. +Notation "-0" := false. +Notation "00" := (0%nat, 0%nat). +Check 0. +Check +0. +Check -0. +Check 00. + +Notation "1000" := True. +Notation "1_000" := (cons 1 nil). +Check 1000. +Check 1_000. + +(* To do: preserve parsing of -0: +Require Import ZArith. +Check (-0)%Z. +*) + +End Test22. diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out deleted file mode 100644 index 34c31ff8a6..0000000000 --- a/test-suite/output/NumeralNotations.out +++ /dev/null @@ -1,236 +0,0 @@ -The command has indeed failed with message: -Unexpected term (nat -> nat) while parsing a numeral notation. -The command has indeed failed with message: -Unexpected non-option term opaque4 while parsing a numeral notation. -The command has indeed failed with message: -Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral -notation. -let v := 0%ppp in v : punit - : punit -let v := 0%ppp in v : punit - : punit -let v := 0%ppp in v : punit - : punit -let v := 0%ppp in v : punit - : punit -let v := 0%uto in v : unit - : unit -The command has indeed failed with message: -Cannot interpret this number as a value of type unit -The command has indeed failed with message: -Cannot interpret this number as a value of type unit -let v := 0%upp in v : unit - : unit -let v := 0%upp in v : unit - : unit -let v := 0%upp in v : unit - : unit -let v := 0%ppps in v : punit - : punit -File "stdin", line 91, characters 2-46: -Warning: To avoid stack overflow, large numbers in punit are interpreted as -applications of pto_punits. [abstract-large-number,numbers] -The command has indeed failed with message: -In environment -v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit -The term "v" has type "punit@{Set}" while it is expected to have type - "punit@{u}". -S - : nat -> nat -S (ack 4 4) - : nat -let v := 0%wnat in v : wnat - : wnat -0%wnat - : wnat -{| unwrap := ack 4 4 |} - : wnat -{| Test6.unwrap := 0 |} - : Test6.wnat -let v := 0%wnat in v : Test6.wnat - : Test6.wnat -let v := 0%wuint in v : wuint - : wuint -let v := 1%wuint in v : wuint - : wuint -let v := 0%wuint8 in v : wuint - : wuint -let v := 0 in v : nat - : nat -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "wuint". - = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} - : wuint -let v := 0%wuint8' in v : wuint - : wuint -let v := 0%wuint9 in v : wuint - : wuint -let v := 0%wuint9' in v : wuint - : wuint -let v := 0 in v : nat - : nat -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "wuint". -File "stdin", line 203, characters 2-72: -Warning: The 'abstract after' directive has no effect when the parsing -function (of_uint) targets an option type. -[abstract-large-number-no-op,numbers] -The command has indeed failed with message: -The 'abstract after' directive has no effect when the parsing function -(of_uint) targets an option type. [abstract-large-number-no-op,numbers] -let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit - : unit -let v := 0%test13 in v : unit - : unit -The command has indeed failed with message: -to_uint' is bound to a notation that does not denote a reference. -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -to_uint'' is bound to a notation that does not denote a reference. -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -let v := 0%test14' in v : unit - : unit -let v := 0%test14' in v : unit - : unit -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -let v := 0%test14' in v : unit - : unit -The command has indeed failed with message: -This command does not support the Global option in sections. -let v := 0%test14'' in v : unit - : unit -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -The command has indeed failed with message: -In environment -v := 0 : nat -The term "v" has type "nat" while it is expected to have type "unit". -let v := 0%test15 in v : unit - : unit -let v := 0%test15 in v : unit - : unit -let v := 0%test15 in v : unit - : unit -let v := foo a.t in v : Foo - : Foo -The command has indeed failed with message: -Cannot interpret in test16_scope because NumeralNotations.Test16.F.Foo could not be found in the current environment. -let v := 0%test17 in v : myint63 - : myint63 -let v := 0%Q in v : Q - : Q -let v := 1%Q in v : Q - : Q -let v := 2%Q in v : Q - : Q -let v := 3%Q in v : Q - : Q -let v := 4%Q in v : Q - : Q - = (0, 1) - : nat * nat - = (1, 1) - : nat * nat - = (2, 1) - : nat * nat - = (3, 1) - : nat * nat - = (4, 1) - : nat * nat -let v := (-1)%Zlike in v : Zlike - : Zlike -let v := 0%Zlike in v : Zlike - : Zlike -let v := 1%Zlike in v : Zlike - : Zlike -let v := 2%Zlike in v : Zlike - : Zlike -let v := 3%Zlike in v : Zlike - : Zlike -let v := 4%Zlike in v : Zlike - : Zlike -2%Zlike - : Zlike -0%Zlike - : Zlike -let v := 0%kt in v : ty - : ty -let v := 1%kt in v : ty - : ty -let v := 2%kt in v : ty - : ty -let v := 3%kt in v : ty - : ty -let v := 4%kt in v : ty - : ty -let v := 5%kt in v : ty - : ty -The command has indeed failed with message: -Cannot interpret this number as a value of type ty - = 0%kt - : ty - = 1%kt - : ty - = 2%kt - : ty - = 3%kt - : ty - = 4%kt - : ty - = 5%kt - : ty -let v : ty := Build_ty Empty_set zero in v : ty - : ty -let v : ty := Build_ty unit one in v : ty - : ty -let v : ty := Build_ty bool two in v : ty - : ty -let v : ty := Build_ty Prop prop in v : ty - : ty -let v : ty := Build_ty Set set in v : ty - : ty -let v : ty := Build_ty Type type in v : ty - : ty -1 - : nat -(-1000)%Z - : Z -0 - : Prop -+0 - : bool --0 - : bool -00 - : nat * nat -1000 - : Prop -1_000 - : list nat diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v deleted file mode 100644 index ca8a14cce1..0000000000 --- a/test-suite/output/NumeralNotations.v +++ /dev/null @@ -1,489 +0,0 @@ -(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) - -Declare Scope opaque_scope. - -(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) -Module Test1. - Axiom hold : forall {A B C}, A -> B -> C. - Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). - Numeral Notation Numeral.int opaque3 opaque3 : opaque_scope. - Delimit Scope opaque_scope with opaque. - Fail Check 1%opaque. -End Test1. - -(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) -Module Test2. - Axiom opaque4 : option Numeral.int. - Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. - Numeral Notation Numeral.int opaque6 opaque6 : opaque_scope. - Delimit Scope opaque_scope with opaque. - Open Scope opaque_scope. - Fail Check 1%opaque. -End Test2. - -Declare Scope silly_scope. - -Module Test3. - Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). - Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). - Definition of_silly (v : silly) := match v with SILLY v _ => v end. - Numeral Notation silly to_silly of_silly : silly_scope. - Delimit Scope silly_scope with silly. - Fail Check 1%silly. -End Test3. - -Module Test4. - Declare Scope opaque_scope. - Declare Scope silly_scope. - Declare Scope pto. - Declare Scope ppo. - Declare Scope ptp. - Declare Scope ppp. - Declare Scope uto. - Declare Scope upo. - Declare Scope utp. - Declare Scope upp. - Declare Scope ppps. - Polymorphic NonCumulative Inductive punit := ptt. - Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. - Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. - Numeral Notation punit to_punit of_punit : pto. - Numeral Notation punit pto_punit of_punit : ppo. - Numeral Notation punit to_punit pof_punit : ptp. - Numeral Notation punit pto_punit pof_punit : ppp. - Numeral Notation unit to_unit of_unit : uto. - Delimit Scope pto with pto. - Delimit Scope ppo with ppo. - Delimit Scope ptp with ptp. - Delimit Scope ppp with ppp. - Delimit Scope uto with uto. - Check let v := 0%pto in v : punit. - Check let v := 0%ppo in v : punit. - Check let v := 0%ptp in v : punit. - Check let v := 0%ppp in v : punit. - Check let v := 0%uto in v : unit. - Fail Check 1%uto. - Fail Check (-1)%uto. - Numeral Notation unit pto_unit of_unit : upo. - Numeral Notation unit to_unit pof_unit : utp. - Numeral Notation unit pto_unit pof_unit : upp. - Delimit Scope upo with upo. - Delimit Scope utp with utp. - Delimit Scope upp with upp. - Check let v := 0%upo in v : unit. - Check let v := 0%utp in v : unit. - Check let v := 0%upp in v : unit. - - Polymorphic Definition pto_punits := pto_punit_all@{Set}. - Polymorphic Definition pof_punits := pof_punit@{Set}. - Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). - Delimit Scope ppps with ppps. - Universe u. - Constraint Set < u. - Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) - Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) -End Test4. - -Module Test5. - Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) -End Test5. - -Module Test6. - (* Check that numeral notations on enormous terms don't take forever to print/parse *) - (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) - Fixpoint ack (n m : nat) : nat := - match n with - | O => S m - | S p => let fix ackn (m : nat) := - match m with - | O => ack p 1 - | S q => ack p (ackn q) - end - in ackn m - end. - - Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) - - Local Set Primitive Projections. - Record > wnat := wrap { unwrap :> nat }. - Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x. - Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. - Module Export Scopes. - Declare Scope wnat_scope. - Delimit Scope wnat_scope with wnat. - End Scopes. - Module Export Notations. - Export Scopes. - Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). - End Notations. - Set Printing Coercions. - Check let v := 0%wnat in v : wnat. - Check wrap O. - Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) -End Test6. - -Module Test6_2. - Import Test6.Scopes. - Check Test6.wrap 0. - Import Test6.Notations. - Check let v := 0%wnat in v : Test6.wnat. -End Test6_2. - -Module Test7. - Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. - Declare Scope wuint_scope. - Delimit Scope wuint_scope with wuint. - Numeral Notation wuint wrap unwrap : wuint_scope. - Check let v := 0%wuint in v : wuint. - Check let v := 1%wuint in v : wuint. -End Test7. - -Module Test8. - Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. - Declare Scope wuint8_scope. - Declare Scope wuint8'_scope. - Delimit Scope wuint8_scope with wuint8. - Delimit Scope wuint8'_scope with wuint8'. - Section with_var. - Context (dummy : unit). - Definition wrap' := let __ := dummy in wrap. - Definition unwrap' := let __ := dummy in unwrap. - Numeral Notation wuint wrap' unwrap' : wuint8_scope. - Check let v := 0%wuint8 in v : wuint. - End with_var. - Check let v := 0%wuint8 in v : nat. - Fail Check let v := 0%wuint8 in v : wuint. - Compute wrap (Nat.to_num_uint 0). - - Notation wrap'' := wrap. - Notation unwrap'' := unwrap. - Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. - Check let v := 0%wuint8' in v : wuint. -End Test8. - -Module Test9. - Declare Scope wuint9_scope. - Declare Scope wuint9'_scope. - Delimit Scope wuint9_scope with wuint9. - Delimit Scope wuint9'_scope with wuint9'. - Section with_let. - Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. - Let wrap' := wrap. - Let unwrap' := unwrap. - Local Notation wrap'' := wrap. - Local Notation unwrap'' := unwrap. - Numeral Notation wuint wrap' unwrap' : wuint9_scope. - Check let v := 0%wuint9 in v : wuint. - Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. - Check let v := 0%wuint9' in v : wuint. - End with_let. - Check let v := 0%wuint9 in v : nat. - Fail Check let v := 0%wuint9 in v : wuint. -End Test9. - -Module Test10. - (* Test that it is only a warning to add abstract after to an optional parsing function *) - Definition to_uint (v : unit) := Nat.to_num_uint 0. - Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_any_uint (v : Numeral.uint) := tt. - Declare Scope unit_scope. - Declare Scope unit2_scope. - Delimit Scope unit_scope with unit. - Delimit Scope unit2_scope with unit2. - Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). - Local Set Warnings Append "+abstract-large-number-no-op". - (* Check that there is actually a warning here *) - Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). - (* Check that there is no warning here *) - Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). -End Test10. - -Module Test12. - (* Test for numeral notations on context variables *) - Declare Scope test12_scope. - Delimit Scope test12_scope with test12. - Section test12. - Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). - - Numeral Notation unit of_uint to_uint : test12_scope. - Check let v := 1%test12 in v : unit. - End test12. -End Test12. - -Module Test13. - (* Test for numeral notations on notations which do not denote references *) - Declare Scope test13_scope. - Declare Scope test13'_scope. - Declare Scope test13''_scope. - Delimit Scope test13_scope with test13. - Delimit Scope test13'_scope with test13'. - Delimit Scope test13''_scope with test13''. - Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. - Definition to_uint_good := to_uint tt. - Notation to_uint' := (to_uint tt). - Notation to_uint'' := (to_uint _). - Numeral Notation unit of_uint to_uint_good : test13_scope. - Check let v := 0%test13 in v : unit. - Fail Numeral Notation unit of_uint to_uint' : test13'_scope. - Fail Check let v := 0%test13' in v : unit. - Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. - Fail Check let v := 0%test13'' in v : unit. -End Test13. - -Module Test14. - (* Test that numeral notations follow [Import], not [Require], and - also test that [Local Numeral Notation]s do not escape modules - nor sections. *) - Declare Scope test14_scope. - Declare Scope test14'_scope. - Declare Scope test14''_scope. - Declare Scope test14'''_scope. - Delimit Scope test14_scope with test14. - Delimit Scope test14'_scope with test14'. - Delimit Scope test14''_scope with test14''. - Delimit Scope test14'''_scope with test14'''. - Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. - Local Numeral Notation unit of_uint to_uint : test14_scope. - Global Numeral Notation unit of_uint to_uint : test14'_scope. - Check let v := 0%test14 in v : unit. - Check let v := 0%test14' in v : unit. - End Inner. - Fail Check let v := 0%test14 in v : unit. - Fail Check let v := 0%test14' in v : unit. - Import Inner. - Fail Check let v := 0%test14 in v : unit. - Check let v := 0%test14' in v : unit. - Section InnerSection. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. - Local Numeral Notation unit of_uint to_uint : test14''_scope. - Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. - Check let v := 0%test14'' in v : unit. - Fail Check let v := 0%test14''' in v : unit. - End InnerSection. - Fail Check let v := 0%test14'' in v : unit. - Fail Check let v := 0%test14''' in v : unit. -End Test14. - -Module Test15. - (** Test module include *) - Declare Scope test15_scope. - Delimit Scope test15_scope with test15. - Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. - Numeral Notation unit of_uint to_uint : test15_scope. - Check let v := 0%test15 in v : unit. - End Inner. - Module Inner2. - Include Inner. - Check let v := 0%test15 in v : unit. - End Inner2. - Import Inner Inner2. - Check let v := 0%test15 in v : unit. -End Test15. - -Module Test16. - (** Test functors *) - Declare Scope test16_scope. - Delimit Scope test16_scope with test16. - Module Type A. - Axiom T : Set. - Axiom t : T. - End A. - Module F (a : A). - Inductive Foo := foo (_ : a.T). - Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : Foo := foo a.t. - Global Numeral Notation Foo of_uint to_uint : test16_scope. - Check let v := 0%test16 in v : Foo. - End F. - Module a <: A. - Definition T : Set := unit. - Definition t : T := tt. - End a. - Module Import f := F a. - (** Ideally this should work, but it should definitely not anomaly *) - Fail Check let v := 0%test16 in v : Foo. -End Test16. - -Require Import Coq.Numbers.Cyclic.Int63.Int63. -Module Test17. - (** Test int63 *) - Declare Scope test17_scope. - Declare Scope test17_scope. - Delimit Scope test17_scope with test17. - Local Set Primitive Projections. - Record myint63 := of_int { to_int : int }. - Numeral Notation myint63 of_int to_int : test17_scope. - Check let v := 0%test17 in v : myint63. -End Test17. - -Module Test18. - (** Test https://github.com/coq/coq/issues/9840 *) - Record Q := { num : nat ; den : nat ; reduced : Nat.gcd num den = 1 }. - Declare Scope Q_scope. - Delimit Scope Q_scope with Q. - - Definition nat_eq_dec (x y : nat) : {x = y} + {x <> y}. - Proof. decide equality. Defined. - - Definition transparentify {A} (D : {A} + {not A}) (H : A) : A := - match D with - | left pf => pf - | right npf => match npf H with end - end. - - Axiom gcd_good : forall x, Nat.gcd x 1 = 1. - - Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. - Definition nat_of_Q (x : Q) : option nat - := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. - Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). - Definition uint_of_Q (x : Q) : option Numeral.uint - := option_map Nat.to_num_uint (nat_of_Q x). - - Numeral Notation Q Q_of_uint uint_of_Q : Q_scope. - - Check let v := 0%Q in v : Q. - Check let v := 1%Q in v : Q. - Check let v := 2%Q in v : Q. - Check let v := 3%Q in v : Q. - Check let v := 4%Q in v : Q. - Compute let v := 0%Q in (num v, den v). - Compute let v := 1%Q in (num v, den v). - Compute let v := 2%Q in (num v, den v). - Compute let v := 3%Q in (num v, den v). - Compute let v := 4%Q in (num v, den v). -End Test18. - -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. -Module Test19. - (** Test another thing related to https://github.com/coq/coq/issues/9840 *) - Record Zlike := { summands : list Z }. - Declare Scope Zlike_scope. - Delimit Scope Zlike_scope with Zlike. - - Definition Z_of_Zlike (x : Zlike) := List.fold_right Z.add 0%Z (summands x). - Definition Zlike_of_Z (x : Z) := {| summands := cons x nil |}. - - Numeral Notation Zlike Zlike_of_Z Z_of_Zlike : Zlike_scope. - - Check let v := (-1)%Zlike in v : Zlike. - Check let v := 0%Zlike in v : Zlike. - Check let v := 1%Zlike in v : Zlike. - Check let v := 2%Zlike in v : Zlike. - Check let v := 3%Zlike in v : Zlike. - Check let v := 4%Zlike in v : Zlike. - Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. - Check {| summands := nil |}. -End Test19. - -Module Test20. - (** Test Sorts *) - Local Set Universe Polymorphism. - Inductive known_type : Type -> Type := - | prop : known_type Prop - | set : known_type Set - | type : known_type Type - | zero : known_type Empty_set - | one : known_type unit - | two : known_type bool. - - Existing Class known_type. - Existing Instances zero one two prop. - Existing Instance set | 2. - Existing Instance type | 4. - - Record > ty := { t : Type ; kt : known_type t }. - - Definition ty_of_uint (x : Numeral.uint) : option ty - := match Nat.of_num_uint x with - | 0 => @Some ty zero - | 1 => @Some ty one - | 2 => @Some ty two - | 3 => @Some ty prop - | 4 => @Some ty set - | 5 => @Some ty type - | _ => None - end. - Definition uint_of_ty (x : ty) : Numeral.uint - := Nat.to_num_uint match kt x with - | prop => 3 - | set => 4 - | type => 5 - | zero => 0 - | one => 1 - | two => 2 - end. - - Declare Scope kt_scope. - Delimit Scope kt_scope with kt. - - Numeral Notation ty ty_of_uint uint_of_ty : kt_scope. - - Check let v := 0%kt in v : ty. - Check let v := 1%kt in v : ty. - Check let v := 2%kt in v : ty. - Check let v := 3%kt in v : ty. - Check let v := 4%kt in v : ty. - Check let v := 5%kt in v : ty. - Fail Check let v := 6%kt in v : ty. - Eval cbv in (_ : known_type Empty_set) : ty. - Eval cbv in (_ : known_type unit) : ty. - Eval cbv in (_ : known_type bool) : ty. - Eval cbv in (_ : known_type Prop) : ty. - Eval cbv in (_ : known_type Set) : ty. - Eval cbv in (_ : known_type Type) : ty. - Local Set Printing All. - Check let v := 0%kt in v : ty. - Check let v := 1%kt in v : ty. - Check let v := 2%kt in v : ty. - Check let v := 3%kt in v : ty. - Check let v := 4%kt in v : ty. - Check let v := 5%kt in v : ty. -End Test20. - -Module Test21. - - Check 00001. - Check (-1_000)%Z. - -End Test21. - -Module Test22. - -Notation "0" := False. -Notation "+0" := true. -Notation "-0" := false. -Notation "00" := (0%nat, 0%nat). -Check 0. -Check +0. -Check -0. -Check 00. - -Notation "1000" := True. -Notation "1_000" := (cons 1 nil). -Check 1000. -Check 1_000. - -(* To do: preserve parsing of -0: -Require Import ZArith. -Check (-0)%Z. -*) - -End Test22. diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index be9dc543d6..7b2bb00ce0 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -19,7 +19,7 @@ Check (0 + Z.of_nat 11)%Z. (* Check hexadecimal printing *) Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n). -Numeral Notation Z Z.of_num_int to_num_int : Z_scope. +Number Notation Z Z.of_num_int to_num_int : Z_scope. Check 42%Z. Check (-42)%Z. Check 0%Z. diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v index 6ea90eab29..437b4a68e9 100644 --- a/test-suite/output/bug_12159.v +++ b/test-suite/output/bug_12159.v @@ -6,8 +6,8 @@ Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1. -Numeral Notation unit to_unit of_unit : A. -Numeral Notation unit to_unit of_unit' : B. +Number Notation unit to_unit of_unit : A. +Number Notation unit to_unit of_unit' : B. Definition f x : unit := x. Check f tt. Arguments f x%A. diff --git a/test-suite/output/sint63Notation.v b/test-suite/output/sint63Notation.v index 331d74ed3d..66ffbf2278 100644 --- a/test-suite/output/sint63Notation.v +++ b/test-suite/output/sint63Notation.v @@ -18,8 +18,8 @@ Definition as_signed (bw : Z) (v : Z) := (((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z. Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)). -Numeral Notation uint uof_Z uto_Z : uint_scope. -Numeral Notation sint sof_Z sto_Z : sint_scope. +Number Notation uint uof_Z uto_Z : uint_scope. +Number Notation sint sof_Z sto_Z : sint_scope. Open Scope uint_scope. Compute uof_Z 0. Compute uof_Z 1. diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v index ea3907ef8a..fe97f10ddf 100644 --- a/test-suite/success/NumeralNotationsNoLocal.v +++ b/test-suite/success/NumeralNotationsNoLocal.v @@ -5,7 +5,7 @@ Delimit Scope unit11_scope with unit11. Goal True. evar (to_uint : unit11 -> Decimal.uint). evar (of_uint : Decimal.uint -> unit11). - Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + Fail Number Notation unit11 of_uint to_uint : uint11_scope. exact I. Unshelve. all: solve [ constructor ]. diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 5eae5567d7..025264ab01 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -12,7 +12,7 @@ (** These numbers coded in base 10 will be used for parsing and printing other Coq numeral datatypes in an human-readable way. - See the [Numeral Notation] command. + See the [Number Notation] command. We represent numbers in base 10 as lists of decimal digits, in big-endian order (most significant digit comes first). *) @@ -245,7 +245,7 @@ with succ_double d := End Little. (** Pseudo-conversion functions used when declaring - Numeral Notations on [uint] and [int]. *) + Number Notations on [uint] and [int]. *) Definition uint_of_uint (i:uint) := i. Definition int_of_int (i:int) := i. diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v index a4ddad2875..36f5e5ad1f 100644 --- a/theories/Init/Hexadecimal.v +++ b/theories/Init/Hexadecimal.v @@ -12,7 +12,7 @@ (** These numbers coded in base 16 will be used for parsing and printing other Coq numeral datatypes in an human-readable way. - See the [Numeral Notation] command. + See the [Number Notation] command. We represent numbers in base 16 as lists of hexadecimal digits, in big-endian order (most significant digit comes first). *) diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v index 8a0531e004..179547d0b3 100644 --- a/theories/Init/Numeral.v +++ b/theories/Init/Numeral.v @@ -27,7 +27,7 @@ Register int as num.num_int.type. Register numeral as num.numeral.type. (** Pseudo-conversion functions used when declaring - Numeral Notations on [uint] and [int]. *) + Number Notations on [uint] and [int]. *) Definition uint_of_uint (i:uint) := i. Definition int_of_int (i:int) := i. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 8f862e8cec..0fe3d5491e 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -35,22 +35,22 @@ Declare ML Module "string_notation_plugin". (* Parsing / printing of hexadecimal numbers *) Arguments Nat.of_hex_uint d%hex_uint_scope. Arguments Nat.of_hex_int d%hex_int_scope. -Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint +Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint : hex_uint_scope. -Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int +Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int : hex_int_scope. (* Parsing / printing of decimal numbers *) Arguments Nat.of_uint d%dec_uint_scope. Arguments Nat.of_int d%dec_int_scope. -Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint +Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint : dec_uint_scope. -Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int +Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int : dec_int_scope. (* Parsing / printing of [nat] numbers *) -Numeral Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001). -Numeral Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001). +Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001). +Number Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 1881e387a2..28ba9daed0 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1007,7 +1007,7 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) -Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. +Number Notation N N.of_num_uint N.to_num_uint : N_scope. Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 8a0aee9cf4..222e76c3e7 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -434,9 +434,9 @@ Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). Definition to_num_int n := Numeral.IntDec (to_int n). -Numeral Notation N of_num_uint to_num_uint : N_scope. +Number Notation N of_num_uint to_num_uint : N_scope. End N. (** Re-export the notation for those who just [Import NatIntDef] *) -Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. +Number Notation N N.of_num_uint N.to_num_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 5585f478b3..7c846571a7 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -8,12 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** * Alternative Binary Numeral Notations *) +(** * Alternative Binary Number Notations *) (** Faster but less safe parsers and printers of [positive], [N], [Z]. *) (** By default, literals in types [positive], [N], [Z] are parsed and - printed via the [Numeral Notation] command, by conversion from/to + printed via the [Number Notation] command, by conversion from/to the [Decimal.int] representation. When working with numbers with thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your @@ -43,7 +43,7 @@ Definition pos_of_z z := Definition pos_to_z p := Zpos p. -Numeral Notation positive pos_of_z pos_to_z : positive_scope. +Number Notation positive pos_of_z pos_to_z : positive_scope. (** [N] *) @@ -60,10 +60,10 @@ Definition n_to_z n := | Npos p => Zpos p end. -Numeral Notation N n_of_z n_to_z : N_scope. +Number Notation N n_of_z n_to_z : N_scope. (** [Z] *) Definition z_of_z (z:Z) := z. -Numeral Notation Z z_of_z z_of_z : Z_scope. +Number Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index cd814091a1..d3528ce87c 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -477,4 +477,4 @@ Definition tail031 (i:int31) := end) i On. -Numeral Notation int31 phi_inv_nonneg phi : int31_scope. +Number Notation int31 phi_inv_nonneg phi : int31_scope. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index c8414c241d..e73060af0b 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1886,7 +1886,7 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) -Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. +Number Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index cdb9af542c..b41cd571dc 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -697,9 +697,9 @@ Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p). Definition to_num_int n := Numeral.IntDec (to_int n). -Numeral Notation positive of_num_int to_num_uint : positive_scope. +Number Notation positive of_num_int to_num_uint : positive_scope. End Pos. (** Re-export the notation for those who just [Import BinPosDef] *) -Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. +Number Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 84d70e56de..192dcd885b 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -129,7 +129,7 @@ Definition to_numeral (q:Q) : option Numeral.numeral := | Some q => Some (Numeral.Dec q) end. -Numeral Notation Q of_numeral to_numeral : Q_scope. +Number Notation Q of_numeral to_numeral : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. Arguments inject_Z x%Z. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a566348dd5..9a30e011af 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1297,7 +1297,7 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) -Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. +Number Notation Z Z.of_num_int Z.to_num_int : Z_scope. Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 8464ad1012..69ed101f24 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -668,9 +668,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. -Numeral Notation Z of_num_int to_num_int : Z_scope. +Number Notation Z of_num_int to_num_int : Z_scope. End Z. (** Re-export the notation for those who just [Import BinIntDef] *) -Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. +Number Notation Z Z.of_num_int Z.to_num_int : Z_scope. -- cgit v1.2.3 From ad7140a7127b147caf20d7c3803b918e3c6776f5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:29:00 +0200 Subject: [numeral notation] Improve documentation Following reviews from Jim Fehrle on #12218 and #12979 --- doc/sphinx/language/core/basic.rst | 9 +++++ doc/sphinx/user-extensions/syntax-extensions.rst | 42 +++++++++++++----------- 2 files changed, 32 insertions(+), 19 deletions(-) diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9308da6d27..45bdc019ac 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -137,11 +137,20 @@ Numbers into an OCaml integer (63-bit integers on most architectures). :n:`@bigint` and :n:`@bignat` have no range limitation. + The :ref:`standard library ` provides some + :ref:`interpretations ` for :n:`@number`. The + :cmd:`Number Notation` mechanism offers the user + a way to define custom parsers and printers for :n:`@number`. + Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent a double quote character within a string. In the grammar, strings are identified with :production:`string`. + The :cmd:`String Notation` mechanism offers the + user a way to define custom parsers and printers for + :token:`string`. + Keywords The following character sequences are keywords defined in the main Coq grammar that cannot be used as identifiers (even when starting Coq with the `-noinit` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 8184e37163..838705e100 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1293,6 +1293,8 @@ recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or :g:`A -> B`. +.. _notation-scopes: + Notation scopes used in the standard library of Coq ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1538,7 +1540,7 @@ numbers (see :ref:`datatypes`). Number notations ~~~~~~~~~~~~~~~~ -.. cmd:: Number Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } +.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } :name: Number Notation .. insertprodn numeral_modifier numeral_modifier @@ -1550,32 +1552,32 @@ Number notations This command allows the user to customize the way numeral literals are parsed and printed. - :n:`@qualid` + :n:`@qualid__type` the name of an inductive type, while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the parsing and printing functions, respectively. The parsing function :n:`@qualid__parse` should have one of the following types: - * :n:`Numeral.int -> @qualid` - * :n:`Numeral.int -> option @qualid` - * :n:`Numeral.uint -> @qualid` - * :n:`Numeral.uint -> option @qualid` - * :n:`Z -> @qualid` - * :n:`Z -> option @qualid` - * :n:`Numeral.numeral -> @qualid` - * :n:`Numeral.numeral -> option @qualid` + * :n:`Numeral.int -> @qualid__type` + * :n:`Numeral.int -> option @qualid__type` + * :n:`Numeral.uint -> @qualid__type` + * :n:`Numeral.uint -> option @qualid__type` + * :n:`Z -> @qualid__type` + * :n:`Z -> option @qualid__type` + * :n:`Numeral.numeral -> @qualid__type` + * :n:`Numeral.numeral -> option @qualid__type` And the printing function :n:`@qualid__print` should have one of the following types: - * :n:`@qualid -> Numeral.int` - * :n:`@qualid -> option Numeral.int` - * :n:`@qualid -> Numeral.uint` - * :n:`@qualid -> option Numeral.uint` - * :n:`@qualid -> Z` - * :n:`@qualid -> option Z` - * :n:`@qualid -> Numeral.numeral` - * :n:`@qualid -> option Numeral.numeral` + * :n:`@qualid__type -> Numeral.int` + * :n:`@qualid__type -> option Numeral.int` + * :n:`@qualid__type -> Numeral.uint` + * :n:`@qualid__type -> option Numeral.uint` + * :n:`@qualid__type -> Z` + * :n:`@qualid__type -> option Z` + * :n:`@qualid__type -> Numeral.numeral` + * :n:`@qualid__type -> option Numeral.numeral` .. deprecated:: 8.12 Numeral notations on :g:`Decimal.uint`, :g:`Decimal.int` and @@ -1605,7 +1607,7 @@ Number notations returns :n:`(@qualid__parse m)` when parsing a literal :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form. Here :g:`m` will be a - :g:`Numeral.int` or :g:`Numeral.uint` or :g:`Z`, depending on the + :g:`Numeral.int`, :g:`Numeral.uint`, :g:`Z` or :g:`Numeral.numeral`, depending on the type of the parsing function :n:`@qualid__parse`. This allows for a more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a @@ -1660,6 +1662,8 @@ Number notations concrete number expressed as a (hexa)decimal. They may not return opaque constants. +.. _string-notations: + String notations ~~~~~~~~~~~~~~~~ -- cgit v1.2.3