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.
---
 interp/numTok.ml | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 interp/numTok.ml

(limited to 'interp/numTok.ml')

diff --git a/interp/numTok.ml b/interp/numTok.ml
new file mode 100644
index 0000000000..cdc6ddb62b
--- /dev/null
+++ b/interp/numTok.ml
@@ -0,0 +1,52 @@
+type t = {
+  int : string;
+  frac : string;
+  exp : string
+}
+
+let equal n1 n2 =
+  String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
+
+let int s = { int = s; frac = ""; exp = "" }
+
+let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
+
+let parse =
+  let buff = ref (Bytes.create 80) in
+  let store len x =
+    let open Bytes in
+    if len >= length !buff then
+      buff := cat !buff (create (length !buff));
+    set !buff len x;
+    succ len in
+  let get_buff len = Bytes.sub_string !buff 0 len in
+  (* reads [0-9]* *)
+  let rec number len s = match Stream.peek s with
+    | Some (('0'..'9') as c) -> Stream.junk s; number (store len c) s
+    | _ -> len in
+  fun s ->
+  let i = get_buff (number 0 s) in
+  let f =
+    match Stream.npeek 2 s with
+    | '.' :: (('0'..'9') as c) :: _ ->
+       Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
+    | _ -> "" in
+  let e =
+    match (Stream.npeek 2 s) with
+    | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
+       Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
+    | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
+       begin match Stream.npeek 3 s with
+       | _ :: _ :: ('0'..'9' as c) :: _ ->
+          Stream.junk s; Stream.junk s; Stream.junk s;
+          get_buff (number (store (store (store 0 e) sign) c) s)
+       | _ -> ""
+       end
+    | _ -> "" in
+  { int = i; frac = f; exp = e }
+
+let of_string s =
+  if s = "" || s.[0] < '0' || s.[0] > '9' then None else
+    let strm = Stream.of_string (s ^ "  ") in
+    let n = parse strm in
+    if Stream.count strm >= String.length s then Some n else None
-- 
cgit v1.2.3


From ab2597acf4245cff82f31fae105a8103a4b46268 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sun, 3 Feb 2019 21:19:56 +0100
Subject: Allow underscores as comments in numeral constants.

The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
---
 interp/numTok.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/numTok.ml')

diff --git a/interp/numTok.ml b/interp/numTok.ml
index cdc6ddb62b..8f2004b889 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -20,15 +20,15 @@ let parse =
     set !buff len x;
     succ len in
   let get_buff len = Bytes.sub_string !buff 0 len in
-  (* reads [0-9]* *)
+  (* reads [0-9_]* *)
   let rec number len s = match Stream.peek s with
-    | Some (('0'..'9') as c) -> Stream.junk s; number (store len c) s
+    | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s
     | _ -> len in
   fun s ->
   let i = get_buff (number 0 s) in
   let f =
     match Stream.npeek 2 s with
-    | '.' :: (('0'..'9') as c) :: _ ->
+    | '.' :: (('0'..'9' | '_') as c) :: _ ->
        Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
     | _ -> "" in
   let e =
-- 
cgit v1.2.3