From 4302a75d82b9ac983cd89dd01c742c36777d921b Mon Sep 17 00:00:00 2001
From: Ana
Date: Tue, 1 Dec 2020 08:52:12 +0000
Subject: 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.
---
 interp/constrextern.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

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)
-- 
cgit v1.2.3