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

---
 plugins/ssr/ssrparser.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0ec5f1673a..9931305832 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -360,8 +360,8 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral (s,b) ->
-             let n = int_of_string s in if b then n else -n
+          | _, Constrexpr.Numeral (b,s) ->
+             let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
           | _ -> raise Not_found
           end
         | None -> raise Not_found
-- 
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.
---
 plugins/ssr/ssrparser.mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 9931305832..457b333a16 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -224,20 +224,20 @@ let test_ssrslashnum b1 b2 strm =
   match Util.stream_nth 0 strm with
   | Tok.KEYWORD "/" ->
       (match Util.stream_nth 1 strm with
-      | Tok.INT _ when b1 ->
+      | Tok.NUMERAL _ 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.INT _ -> ()
+               | Tok.NUMERAL _ -> ()
                | _ -> 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.INT _ when b2 ->
+         | Tok.NUMERAL _ when b2 ->
            (match Util.stream_nth 3 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
@@ -248,7 +248,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.INT _ when b2 ->
+         | Tok.NUMERAL _ when b2 ->
            (match Util.stream_nth 2 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
-- 
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.
---
 plugins/ssr/ssrparser.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 457b333a16..7cd62f4ead 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -360,7 +360,7 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral (b,s) ->
+          | _, Constrexpr.Numeral (b,{NumTok.int = s; frac = ""; exp = ""}) ->
              let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
           | _ -> raise Not_found
           end
-- 
cgit v1.2.3