Merge PR#719: Constrexpr.Numeral without bigint

16 files changed, 96 insertions, 44 deletions

diff --git a/API/API.mli b/API/API.mli
index 4b2845443e..69278e7c9f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2055,8 +2055,10 @@ sig
   type explicitation = Constrexpr.explicitation =
                      | ExplByPos of int * Names.Id.t option
                      | ExplByName of Names.Id.t
+  type sign = bool
+  type raw_natural_number = string
   type prim_token = Constrexpr.prim_token =
-                  | Numeral of Bigint.bigint
+                  | Numeral of raw_natural_number * sign
                   | String of string
   type notation = string
   type instance_expr = Misctypes.glob_level list
diff --git a/API/grammar_API.mli b/API/grammar_API.mli
index 4da5b380fe..c643f09086 100644
--- a/API/grammar_API.mli
+++ b/API/grammar_API.mli
@@ -116,7 +116,7 @@ sig
     val pattern_identref : Names.Id.t located Gram.Entry.e
     val base_ident : Names.Id.t Gram.Entry.e
     val natural : int Gram.Entry.e
-    val bigint : Bigint.bigint Gram.Entry.e
+    val bigint : Constrexpr.raw_natural_number Gram.Entry.e
     val integer : int Gram.Entry.e
     val string : string Gram.Entry.e
     val qualid : API.Libnames.qualid located Gram.Entry.e
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
 
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 614c097b5a..593b190a6b 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -31,8 +31,16 @@ type abstraction_kind = AbsLambda | AbsPi
 
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
+(** Representation of integer literals that appear in Coq scripts.
+    We now use raw strings of digits in base 10 (big-endian), and a separate
+    sign flag. Note that this representation is not unique, due to possible
+    multiple leading zeros, and -0 = +0 *)
+
+type sign = bool
+type raw_natural_number = string
+
 type prim_token =
-  | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
+  | Numeral of raw_natural_number * sign
   | String of string
 
 type instance_expr = Misctypes.glob_level list
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 890ce2deca..35ffa20d08 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -227,7 +227,7 @@ type prod_info = production_level * production_position
 type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
-| TTBigint : ('self, Bigint.bigint) entry
+| TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
@@ -337,8 +337,8 @@ match e with
 | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
   begin match forpat with
-  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral v))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral v))
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true)))
   end
 | TTReference ->
   begin match forpat with
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 54bac253d0..de76118026 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -203,7 +203,7 @@ GEXTEND Gram
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c.CAst.v with
-              CPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+            | CPrim (Numeral (n,true)) ->
                 CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
@@ -280,7 +280,7 @@ GEXTEND Gram
   atomic_constr:
     [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i)
       | s=sort   -> CAst.make ~loc:!@loc @@  CSort s
-      | n=INT    -> CAst.make ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n))
+      | n=INT    -> CAst.make ~loc:!@loc @@ CPrim (Numeral (n,true))
       | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s)
       | "_"      -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)
       | "?"; "["; id=ident; "]"  -> CAst.make ~loc:!@loc @@  CHole (None, IntroIdentifier id, None)
@@ -395,18 +395,18 @@ GEXTEND Gram
       | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p.CAst.v with
-            | CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+            | CPatPrim (Numeral (n,true)) ->
                  CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p)
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           let p =
             match p with
-            | { CAst.v = CPatPrim (Numeral z) } when Bigint.is_pos_or_zero z ->
+            | { CAst.v = CPatPrim (Numeral (n,true)) } ->
                  CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
 	  CAst.make ~loc:!@loc @@ CPatCast (p, ty)
-      | n = INT    -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
+      | n = INT    -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (n,true))
       | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ]
   ;
   impl_ident_tail:
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 78f75a73cb..c77d6e204e 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -114,7 +114,7 @@ GEXTEND Gram
   natural:
     [ [ i = INT -> my_int_of_string (!@loc) i ] ]
   ;
-  bigint: (* Negative numbers are dealt with specially *)
-    [ [ i = INT -> (Bigint.of_string i) ] ]
+  bigint: (* Negative numbers are dealt with elsewhere *)
+    [ [ i = INT -> i ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 959e8ddf52..9fb3daabaf 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -199,7 +199,7 @@ module Prim :
     val pattern_identref : Id.t located Gram.entry
     val base_ident : Id.t Gram.entry
     val natural : int Gram.entry
-    val bigint : Bigint.bigint Gram.entry
+    val bigint : Constrexpr.raw_natural_number Gram.entry
     val integer : int Gram.entry
     val string : string Gram.entry
     val lstring : string located Gram.entry
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index a971fc79f6..804f734504 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -139,14 +139,16 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
+let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
       TacCase (with_evar,(clear,cl))
   (* Reinterpret numbers as a notation for terms *)
   | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
       TacCase (with_evar,
-        (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)),
-	 NoBindings)))
+        (clear,(CAst.make @@ CPrim (mkNumeral n),
+         NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 3ea8c24314..09917339a7 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -346,7 +346,8 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype false [] (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral bigi -> int_of_string (Bigint.to_string bigi)
+          | _, Constrexpr.Numeral (s,b) ->
+             let n = int_of_string s in if b then n else -n
           | _ -> raise Not_found
           end
         | None -> raise Not_found
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 626464b96f..49eedb767b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -80,7 +80,7 @@ let tag_var = tag Tag.variable
         | Any -> true
 
   let prec_of_prim_token = function
-    | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+    | Numeral (_,b) -> if b then lposint else lnegint
     | String _ -> latom
 
   open Notation
@@ -231,7 +231,7 @@ let tag_var = tag Tag.variable
     | ArgVar (loc,s) -> pr_lident (loc,s)
 
   let pr_prim_token = function
-    | Numeral n -> str (Bigint.to_string n)
+    | Numeral (n,s) -> str (if s then n else "-"^n)
     | String s -> qs s
 
   let pr_evar pr id l =
diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v
index 451bec9b20..3b57310d6e 100644
--- a/test-suite/bugs/closed/3036.v
+++ b/test-suite/bugs/closed/3036.v
@@ -15,11 +15,11 @@ Definition perm := Qc.
 Locate Qle_bool.
 
 Definition compatibleb (p1 p2 : perm) : bool :=
-let p1pos := Qle_bool 00 p1 in
-  let p2pos := Qle_bool 00 p2 in
+let p1pos := Qle_bool 0 p1 in
+  let p2pos := Qle_bool 0 p2 in
     negb (
          (p1pos && p2pos)
-      || ((p1pos || p2pos) && (negb (Qle_bool 00 ((p1 + p2)%Qc)))))%Qc.
+      || ((p1pos || p2pos) && (negb (Qle_bool 0 ((p1 + p2)%Qc)))))%Qc.
 
 Definition compatible (p1 p2 : perm) := compatibleb p1 p2 = true.