From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 26 Apr 2016 17:30:30 +0200
Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of
 BigInt.t)

 This string contains the base-10 representation of the number (big endian)

 Note that some inner parsing stuff still uses bigints, see egramcoq.ml
---
 interp/notation.ml | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 23332f7c45..f74e1d43b7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -10,7 +10,6 @@
 open CErrors
 open Util
 open Pp
-open Bigint
 open Names
 open Term
 open Libnames
@@ -319,7 +318,13 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
         (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
     patl
 
-let mkNumeral n = Numeral n
+let mkNumeral n =
+  if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
+  else Numeral (Bigint.to_string (Bigint.neg n), false)
+
+let ofNumeral n s =
+  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
 let mkString = function
 | None -> None
 | Some s -> if Unicode.is_utf8 s then Some (String s) else None
@@ -327,8 +332,10 @@ let mkString = function
 let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
 
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
+  let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
   declare_prim_token_interpreter sc
-    (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p)
+    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
+                            | p -> cont ?loc p)
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
@@ -440,8 +447,8 @@ let find_notation ntn sc =
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
-  | Numeral n when is_pos_or_zero n -> to_string n
-  | Numeral n -> "- "^(to_string (neg n))
+  | Numeral (n,true) -> n
+  | Numeral (n,false) -> "- "^n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -466,7 +473,8 @@ let interp_prim_token_gen ?loc g p local_scopes =
   with Not_found ->
     user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
-      | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
+      | Numeral _ ->
+         str "No interpretation for numeral " ++ str (notation_of_prim_token p)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token ?loc =
-- 
cgit v1.2.3


From 0b5ef21f936acbb89fa5b272efdcf3cf03de58cc Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 31 May 2017 21:48:26 +0200
Subject: Notation.declare_rawnumeral_interpreter

 This new function is similar to declare_numeral_interpreter,
 but works on a lower level : instead of bigint, numbers are
 represented as string of their decimal digits (plus a boolean sign)
---
 interp/notation.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index f74e1d43b7..300f6b1dd0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -331,6 +331,16 @@ let mkString = function
 
 let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
 
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+
+let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
+  declare_prim_token_interpreter sc
+    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
+                            | p -> cont ?loc p)
+    (patl, (fun r -> match uninterp r with
+                     | None -> None
+                     | Some (n,s) -> Some (Numeral (n,s))), inpat)
+
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
   declare_prim_token_interpreter sc
-- 
cgit v1.2.3