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, 8 insertions, 8 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 171d51800e..8d5c2fb687 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -70,6 +70,7 @@ type goal_kind = locality * polymorphic * goal_object_kind
 (** Kinds used in library *)
 
 type logical_kind =
+  | IsPrimitive
   | IsAssumption of assumption_object_kind
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
diff --git a/library/global.ml b/library/global.ml
index 84d2a37170..784a02449c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -175,11 +175,8 @@ let with_global f =
   let (a, ctx) = f (env ()) (current_dirpath ()) in
     push_context_set false ctx; a
 
-(* spiwack: register/unregister functions for retroknowledge *)
-let register field value =
-  globalize0 (Safe_typing.register field value)
-
 let register_inline c = globalize0 (Safe_typing.register_inline c)
+let register_inductive c r = globalize0 (Safe_typing.register_inductive c r)
 
 let set_strategy k l =
   globalize0 (Safe_typing.set_strategy k l)
diff --git a/library/global.mli b/library/global.mli
index 40962e21af..df18625a5f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -142,10 +142,8 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
 
 (** {6 Retroknowledge } *)
 
-val register :
-  Retroknowledge.field -> GlobRef.t -> unit
-
 val register_inline : Constant.t -> unit
+val register_inductive : inductive -> CPrimitives.prim_ind -> unit
 
 (** {6 Oracle } *)
 
diff --git a/library/keys.ml b/library/keys.ml
index 58883ccc88..45b6fae2f0 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -25,13 +25,14 @@ type key =
   | KFix
   | KCoFix
   | KRel
+  | KInt
 
 module KeyOrdered = struct
   type t = key
 
   let hash gr =
     match gr with
-    | KGlob gr -> 8 + GlobRef.Ordered.hash gr
+    | KGlob gr -> 9 + GlobRef.Ordered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -40,6 +41,7 @@ module KeyOrdered = struct
     | KFix -> 5
     | KCoFix -> 6
     | KRel -> 7
+    | KInt -> 8
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -133,6 +135,7 @@ let constr_key kind c =
       | Evar _ -> raise Not_found
       | Sort _ -> KSort 
       | LetIn _ -> KLet
+      | Int _ -> KInt
     in Some (aux c)
   with Not_found -> None
 
@@ -148,6 +151,7 @@ let pr_key pr_global = function
   | KFix -> str"Fix"
   | KCoFix -> str"CoFix"
   | KRel -> str"Rel"
+  | KInt -> str"Int"
 
 let pr_keyset pr_global v = 
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)