From a17626eb716b8a7b0ae5c1387f485223ba1c2de5 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 10 May 2019 16:48:40 +0200
Subject: [ltac2] Add primitive integers

---
 user-contrib/Ltac2/Constr.v    |  1 +
 user-contrib/Ltac2/Init.v      |  1 +
 user-contrib/Ltac2/tac2core.ml |  7 +++++--
 user-contrib/Ltac2/tac2ffi.ml  | 23 ++++++++++++++++++-----
 user-contrib/Ltac2/tac2ffi.mli |  6 ++++++
 5 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index d8d222730e..1701bf4365 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -38,6 +38,7 @@ Ltac2 Type kind := [
 | Fix (int array, int, ident option array, constr array, constr array)
 | CoFix (int, ident option array, constr array, constr array)
 | Proj (projection, constr)
+| Uint63 (uint63)
 ].
 
 Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 16e7d7a6f9..dc1690bdfb 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -14,6 +14,7 @@ Ltac2 Type int.
 Ltac2 Type string.
 Ltac2 Type char.
 Ltac2 Type ident.
+Ltac2 Type uint63.
 
 (** Constr-specific built-in types *)
 Ltac2 Type meta.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index d7e7b91ee6..da8600109e 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -424,8 +424,8 @@ let () = define1 "constr_kind" constr begin fun c ->
       Value.of_ext Value.val_projection p;
       Value.of_constr c;
     |]
-  | Int _ ->
-    assert false
+  | Int n ->
+    v_blk 17 [|Value.of_uint63 n|]
   end
 end
 
@@ -503,6 +503,9 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     let p = Value.to_ext Value.val_projection p in
     let c = Value.to_constr c in
     EConstr.mkProj (p, c)
+  | (17, [|n|]) ->
+    let n = Value.to_uint63 n in
+    EConstr.mkInt n
   | _ -> assert false
   in
   return (Value.of_constr c)
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index e3127ab9df..1043d25a75 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -30,6 +30,8 @@ type valexpr =
   (** Open constructors *)
 | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
   (** Arbitrary data *)
+| ValUint63 of Uint63.t
+  (** Primitive integers *)
 
 and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure
 
@@ -47,21 +49,21 @@ type t = valexpr
 
 let is_int = function
 | ValInt _ -> true
-| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false
+| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> false
 
 let tag v = match v with
 | ValBlk (n, _) -> n
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
 let field v n = match v with
 | ValBlk (_, v) -> v.(n)
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
 let set_field v n w = match v with
 | ValBlk (_, v) -> v.(n) <- w
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
 let make_block tag v = ValBlk (tag, v)
@@ -192,7 +194,7 @@ let of_closure cls = ValCls cls
 
 let to_closure = function
 | ValCls cls -> cls
-| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false
+| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ -> assert false
 
 let closure = {
   r_of = of_closure;
@@ -318,6 +320,17 @@ let open_ = {
   r_id = false;
 }
 
+let of_uint63 n = ValUint63 n
+let to_uint63 = function
+| ValUint63 n -> n
+| _ -> assert false
+
+let uint63 = {
+  r_of = of_uint63;
+  r_to = to_uint63;
+  r_id = false;
+}
+
 let of_constant c = of_ext val_constant c
 let to_constant c = to_ext val_constant c
 let constant = repr_ext val_constant
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index bfc93d99e6..f8581061a0 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -28,6 +28,8 @@ type valexpr =
   (** Open constructors *)
 | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
   (** Arbitrary data *)
+| ValUint63 of Uint63.t
+  (** Primitive integers *)
 
 type 'a arity
 
@@ -143,6 +145,10 @@ val of_open : KerName.t * valexpr array -> valexpr
 val to_open : valexpr -> KerName.t * valexpr array
 val open_ : (KerName.t * valexpr array) repr
 
+val of_uint63 : Uint63.t -> valexpr
+val to_uint63 : valexpr -> Uint63.t
+val uint63 : Uint63.t repr
+
 type ('a, 'b) fun1
 
 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
-- 
cgit v1.2.3