Merge PR#719: Constrexpr.Numeral without bigint

5 files changed, 61 insertions, 22 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 79e0e61646..396dde0465 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -45,8 +45,11 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
+(* Note: redundant Numeral representations such as -0 and +0 (or different
+   numbers of leading zeros) are considered different here. *)
+
 let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral i1, Numeral i2 -> Bigint.equal i1 i2
+| Numeral (n1,s1), Numeral (n2,s2) -> String.equal n1 n2 && s1 == s2
 | String s1, String s2 -> String.equal s1 s2
 | _ -> false
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f0ee1d58a6..8a798bfb00 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -355,23 +355,31 @@ let expand_curly_brackets loc mknot ntn l =
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
+let is_number s =
+  let rec aux i =
+    Int.equal (String.length s) i ||
+    match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
+  in aux 0
+
+let is_zero s =
+  let rec aux i =
+    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+  in aux 0
+
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
   then expand_curly_brackets loc mknot ntn l
   else match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
-    | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
+    | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
         mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
     | _ ->
 	match decompose_notation_key ntn, l with
-	| [Terminal "-"; Terminal x], [] ->
-	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
-	     with Failure _ -> mknot (loc,ntn,[]))
-	| [Terminal x], [] ->
-	    (try mkprim (loc, Numeral (Bigint.of_string x))
-	     with Failure _ -> mknot (loc,ntn,[]))
-	| _ ->
-	    mknot (loc,ntn,l)
+	| [Terminal "-"; Terminal x], [] when is_number x ->
+	   mkprim (loc, Numeral (x,false))
+	| [Terminal x], [] when is_number x ->
+	   mkprim (loc, Numeral (x,true))
+	| _ -> mknot (loc,ntn,l)
 
 let make_notation loc ntn (terms,termlists,binders as subst) =
   if not (List.is_empty termlists) || not (List.is_empty binders) then
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 67fee62028..89827300c4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1219,6 +1219,11 @@ let alias_of als = match als.alias_ids with
 
 *)
 
+let is_zero s =
+  let rec aux i =
+    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+  in aux 0
+
 let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
 let product_of_cases_patterns aliases idspl =
@@ -1331,9 +1336,9 @@ let drop_notations_pattern looked_for genv =
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
-	when Bigint.is_strictly_pos p ->
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[])
+	when not (is_zero p) ->
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
       rcp_of_glob pat
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
@@ -1639,9 +1644,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	CAst.make ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
-	when Bigint.is_strictly_pos p ->
-	intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p)))
+    | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[]))
+         when not (is_zero p) ->
+       intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
     | CNotation ("( _ )",([a],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
diff --git a/interp/notation.ml b/interp/notation.ml
index 23332f7c45..300f6b1dd0 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,16 +318,34 @@ 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
 
 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
-    (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 +457,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 +483,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 =
diff --git a/interp/notation.mli b/interp/notation.mli
index d271a88fe7..c739ec12fd 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,6 +74,11 @@ type 'a prim_token_interpreter =
 type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
 
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+
+val declare_rawnumeral_interpreter : scope_name -> required_module ->
+  rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit
+
 val declare_numeral_interpreter : scope_name -> required_module ->
   bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit