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, 4 insertions, 3 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 016b63be09..1008492825 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,10 +47,11 @@ type inline = int option
     transparent body, or an opaque one *)
 
 (* Global declarations (i.e. constants) can be either: *)
-type constant_def =
+type 'a constant_def =
   | Undef of inline                       (** a global assumption *)
-  | Def of constr Mod_subst.substituted   (** or a transparent global definition *)
+  | Def of 'a                             (** or a transparent global definition *)
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
+  | Primitive of CPrimitives.t            (** or a primitive operation *)
 
 type constant_universes =
   | Monomorphic_const of Univ.ContextSet.t
@@ -88,7 +89,7 @@ type typing_flags = {
  * the OpaqueDef *)
 type constant_body = {
     const_hyps : Constr.named_context; (** New: younger hyp at top *)
-    const_body : constant_def;
+    const_body : Constr.t Mod_subst.substituted constant_def;
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;