Signed primitive integers

Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed <=), lts (signed <), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.

4 files changed, 43 insertions, 12 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8138b4c6d9..4fb7861ca6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -969,7 +969,13 @@ let rec extern inctx ?impargs scopes vars r =
      with No_match -> extern inctx scopes vars r')
   | None ->
 
-  try extern_notations inctx scopes vars None r
+  let r' = match DAst.get r with
+    | GInt i when Coqlib.has_ref "num.int63.wrap_int" ->
+       let wrap = Coqlib.lib_ref "num.int63.wrap_int" in
+       DAst.make (GApp (DAst.make (GRef (wrap, None)), [r]))
+    | _ -> r in
+
+  try extern_notations inctx scopes vars None r'
   with No_match ->
 
   let loc = r.CAst.loc in
@@ -1123,7 +1129,7 @@ let rec extern inctx ?impargs scopes vars r =
 
   | GInt i ->
      extern_prim_token_delimiter_if_required
-       (Number (NumTok.Signed.of_int_string (Uint63.to_string i)))
+       (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i))))
        "int63" "int63_scope" (snd scopes)
 
   | GFloat f -> extern_float f (snd scopes)
diff --git a/interp/notation.ml b/interp/notation.ml
index d6002d71b5..ed605c994d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -548,11 +548,14 @@ type number_ty =
     hexadecimal : Names.inductive;
     number : Names.inductive }
 
+type pos_neg_int63_ty =
+  { pos_neg_int63_ty : Names.inductive }
+
 type target_kind =
   | Int of int_ty (* Coq.Init.Number.int + uint *)
   | UInt of int_ty (* Coq.Init.Number.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
-  | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+  | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
   | Number of number_ty (* Coq.Init.Number.number + uint + int *)
   | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
   | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
@@ -1038,12 +1041,22 @@ let error_negative ?loc =
 let error_overflow ?loc n =
   CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n))
 
-let interp_int63 ?loc n =
+let error_underflow ?loc n =
+  CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "underflow in int63 literal: " ++ str (Z.to_string n))
+
+let coqpos_neg_int63_of_bigint ?loc ind (sign,n) =
+  let uint = int63_of_pos_bigint ?loc n in
+  let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
+  mkApp (mkConstruct (ind, pos_neg), [|uint|])
+
+let interp_int63 ?loc ind n =
+  let sign = if Z.(compare n zero >= 0) then SPlus else SMinus in
+  let n = Z.abs n in
   if Z.(leq zero n)
   then
     if Z.(lt n (pow z_two 63))
-    then int63_of_pos_bigint ?loc n
-    else error_overflow ?loc n
+    then coqpos_neg_int63_of_bigint ?loc ind (sign,n)
+    else match sign with SPlus -> error_overflow ?loc n | SMinus -> error_underflow ?loc n
   else error_negative ?loc
 
 let bigint_of_int63 c =
@@ -1051,6 +1064,15 @@ let bigint_of_int63 c =
   | Int i -> Z.of_int64 (Uint63.to_int64 i)
   | _ -> raise NotAValidPrimToken
 
+let bigint_of_coqpos_neg_int63 c =
+  match Constr.kind c with
+  | App (c,[|c'|]) ->
+     (match Constr.kind c with
+      | Construct ((_,1), _) (* Pos *) -> bigint_of_int63 c'
+      | Construct ((_,2), _) (* Neg *) -> Z.neg (bigint_of_int63 c')
+      | _ -> raise NotAValidPrimToken)
+  | _ -> raise NotAValidPrimToken
+
 let interp o ?loc n =
   begin match o.warning, n with
   | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold ->
@@ -1070,9 +1092,9 @@ let interp o ?loc n =
         with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
     | Z z_pos_ty, Some n ->
        z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
-    | Int63, Some n ->
-       interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
-    | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
+    | Int63 pos_neg_int63_ty, Some n ->
+       interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n)
+    | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63 _), _ ->
        no_such_prim_token "number" ?loc o.ty_name
     | Number number_ty, _ -> coqnumber_of_rawnum number_ty n
     | Decimal number_ty, _ ->
@@ -1100,7 +1122,7 @@ let uninterp o n =
       | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c)
       | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
       | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
-      | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c)
+      | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c)
       | (Number _, c) -> rawnum_of_coqnumber c
       | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
       | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
diff --git a/interp/notation.mli b/interp/notation.mli
index 97955bf92e..77f245ae77 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -137,11 +137,14 @@ type number_ty =
     hexadecimal : Names.inductive;
     number : Names.inductive }
 
+type pos_neg_int63_ty =
+  { pos_neg_int63_ty : Names.inductive }
+
 type target_kind =
   | Int of int_ty (* Coq.Init.Number.int + uint *)
   | UInt of int_ty (* Coq.Init.Number.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
-  | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+  | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
   | Number of number_ty (* Coq.Init.Number.number + uint + int *)
   | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
   | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
diff --git a/interp/numTok.ml b/interp/numTok.ml
index 124a6cd249..12ef33717a 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -85,7 +85,7 @@ struct
   let string_of_nonneg_bigint c n =
     match c with
     | CDec -> Z.format "%d" n
-    | CHex -> Z.format "0x%x" n
+    | CHex -> Z.format "%#x" n
   let of_bigint c n =
     let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in
     (sign, string_of_nonneg_bigint c n)