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>

1 files changed, 5 insertions, 3 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 707c46048b..5686c4071d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -56,8 +56,9 @@ let constant_is_polymorphic cb =
   | Monomorphic_const _ -> false
   | Polymorphic_const _ -> true
 
+
 let constant_has_body cb = match cb.const_body with
-  | Undef _ -> false
+  | Undef _ | Primitive _ -> false
   | Def _ | OpaqueDef _ -> true
 
 let constant_polymorphic_context cb =
@@ -67,7 +68,7 @@ let constant_polymorphic_context cb =
 
 let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
-  | Undef _ | Def _ -> false
+  | Undef _ | Def _ | Primitive _ -> false
 
 (** {7 Constant substitutions } *)
 
@@ -83,7 +84,7 @@ let subst_const_type sub arity =
 (** No need here to check for physical equality after substitution,
     at least for Def due to the delayed substitution [subst_constr_subst]. *)
 let subst_const_def sub def = match def with
-  | Undef _ -> def
+  | Undef _ | Primitive _ -> def
   | Def c -> Def (subst_constr sub c)
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
@@ -119,6 +120,7 @@ let hcons_rel_context l = List.Smart.map hcons_rel_decl l
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
+  | Primitive p -> Primitive p
   | Def l_constr ->
     let constr = force_constr l_constr in
     Def (from_val (Constr.hcons constr))