From 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Oct 2018 13:16:25 +0200 Subject: Replace type sign = bool with SPlus | SMinus --- vernac/egramcoq.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index f1a08cc9b3..b913bccfa3 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -403,8 +403,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,v))) end | TTReference -> begin match forpat with -- cgit v1.2.3 From a95aacce6cc32726b494d4cc694da49eae86cf96 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 11:19:28 +0200 Subject: Rename the INT token to NUMERAL In anticipation of future uses of this token for non integer numerals. --- vernac/g_vernac.mlg | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 589b15fd41..d80f29cf1b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -294,7 +294,7 @@ GRAMMAR EXTEND Gram | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ] ; inline: - [ [ IDENT "Inline"; "("; i = INT; ")" -> { InlineAt (int_of_string i) } + [ [ IDENT "Inline"; "("; i = NUMERAL; ")" -> { InlineAt (int_of_string i) } | IDENT "Inline" -> { DefaultInline } | -> { NoInline } ] ] ; @@ -607,7 +607,7 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; functor_app_annot: - [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = NUMERAL; "]" -> { InlineAt (int_of_string i) } | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline } | -> { DefaultInline } @@ -847,8 +847,8 @@ GRAMMAR EXTEND Gram strategy_level: [ [ IDENT "expand" -> { Conv_oracle.Expand } | IDENT "opaque" -> { Conv_oracle.Opaque } - | n=INT -> { Conv_oracle.Level (int_of_string n) } - | "-"; n=INT -> { Conv_oracle.Level (- int_of_string n) } + | n=NUMERAL -> { Conv_oracle.Level (int_of_string n) } + | "-"; n=NUMERAL -> { Conv_oracle.Level (- int_of_string n) } | IDENT "transparent" -> { Conv_oracle.transparent } ] ] ; instance_name: -- cgit v1.2.3 From 4dc3d04d0812005f221e88744c587de8ef0f38ee Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 15:10:54 +0200 Subject: Rename raw_natural_number to raw_numeral In anticipation of an extension from natural numbers to other numeral constants. --- vernac/egramcoq.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac') diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index b913bccfa3..01e59bbed6 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -245,7 +245,7 @@ type prod_info = production_level * production_position type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry -| TTBigint : ('self, Constrexpr.raw_natural_number) entry +| TTBigint : ('self, Constrexpr.raw_numeral) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry -- cgit v1.2.3 From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 14:40:23 +0200 Subject: Add parsing of decimal constants (e.g., 1.02e+01) Rather than integers '[0-9]+', numeral constant can now be parsed according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'. This can be used in one of the two following ways: - using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin - using `Numeral Notation` with the type `decimal` added to `Decimal.v` See examples of each use case in the next two commits. --- vernac/egramcoq.ml | 6 +++--- vernac/g_vernac.mlg | 9 ++++----- vernac/metasyntax.ml | 2 +- 3 files changed, 8 insertions(+), 9 deletions(-) (limited to 'vernac') diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 01e59bbed6..568e5b9997 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -245,7 +245,7 @@ type prod_info = production_level * production_position type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry -| TTBigint : ('self, Constrexpr.raw_numeral) entry +| TTBigint : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry @@ -403,8 +403,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,v))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,v))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) end | TTReference -> begin match forpat with diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d80f29cf1b..1e6a928c7c 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -294,7 +294,7 @@ GRAMMAR EXTEND Gram | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ] ; inline: - [ [ IDENT "Inline"; "("; i = NUMERAL; ")" -> { InlineAt (int_of_string i) } + [ [ IDENT "Inline"; "("; i = natural; ")" -> { InlineAt i } | IDENT "Inline" -> { DefaultInline } | -> { NoInline } ] ] ; @@ -607,8 +607,8 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; functor_app_annot: - [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = NUMERAL; "]" -> - { InlineAt (int_of_string i) } + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = natural; "]" -> + { InlineAt i } | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline } | -> { DefaultInline } ] ] @@ -847,8 +847,7 @@ GRAMMAR EXTEND Gram strategy_level: [ [ IDENT "expand" -> { Conv_oracle.Expand } | IDENT "opaque" -> { Conv_oracle.Opaque } - | n=NUMERAL -> { Conv_oracle.Level (int_of_string n) } - | "-"; n=NUMERAL -> { Conv_oracle.Level (- int_of_string n) } + | n=integer -> { Conv_oracle.Level n } | IDENT "transparent" -> { Conv_oracle.transparent } ] ] ; instance_name: diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index b5e9e1b0d5..843296d24e 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -250,7 +250,7 @@ let quote_notation_token x = let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> - (try let _ = Bigint.of_string x in true with Failure _ -> false) + NumTok.of_string x <> None | _ -> false -- cgit v1.2.3