Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

4 files changed, 9 insertions, 4 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 24d161d00a..8493119ee5 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -73,6 +73,7 @@ let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+let mkInt i = of_kind (Int i)
 
 let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstRef c -> mkConstU (c,u)
@@ -81,6 +82,7 @@ let mkRef (gr,u) = let open GlobRef in match gr with
   | VarRef x -> mkVar x
 
 let applist (f, arg) = mkApp (f, Array.of_list arg)
+let applistc f arg = mkApp (f, Array.of_list arg)
 
 let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
 let isVar sigma c = match kind sigma c with Var _ -> true | _ -> false
@@ -328,7 +330,7 @@ let iter_with_full_binders sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
+    | Construct _ | Int _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 49cbc4d7e5..2f4cf7d5d0 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -124,10 +124,12 @@ val mkCase : case_info * t * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> t -> t
+val mkInt : Uint63.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
 val applist : t * t list -> t
+val applistc : t -> t list -> t
 
 val mkProd_or_LetIn : rel_declaration -> t -> t
 val mkLambda_or_LetIn : rel_declaration -> t -> t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 018eca1ba2..294b61fd3d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	Some (match lna.(i) with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
   in
   hdrec c
 
@@ -163,6 +163,7 @@ let hdchar env sigma c =
 	lowercase_first_char id
     | Evar _ (* We could do better... *)
     | Meta _ | Case (_, _, _, _) -> "y"
+    | Int _ -> "i"
   in
   hdrec 0 c
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 137770d8f0..13c7fcc216 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -600,7 +600,7 @@ let map_constr_with_binders_left_to_right sigma g f l c =
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
+    | Construct _ | Int _) -> c
   | Cast (b,k,t) -> 
     let b' = f l b in 
     let t' = f l t in
@@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> cstr
+    | Construct _ | Int _) -> cstr
   | Cast (c,k, t) ->
       let c' = f l c in
       let t' = f l t in