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