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, 16 insertions, 31 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 77820a301e..02f38e7214 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -119,7 +119,7 @@ let empty_env = {
     env_universes = UGraph.initial_universes;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
-  retroknowledge = Retroknowledge.initial_retroknowledge;
+  retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab }
 
 
@@ -450,7 +450,10 @@ let constant_type env (kn,u) =
   let csts = Univ.AUContext.instantiate u uctx in
   (subst_instance_constr u cb.const_type, csts)
 
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result =
+  | NoBody
+  | Opaque
+  | IsPrimitive of CPrimitives.t
 
 exception NotEvaluableConst of const_evaluation_result
 
@@ -461,14 +464,14 @@ let constant_value_and_type env (kn, u) =
   let b' = match cb.const_body with
     | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
     | OpaqueDef _ -> None
-    | Undef _ -> None
+    | Undef _ | Primitive _ -> None
   in
   b', subst_instance_constr u cb.const_type, cst
 
 let body_of_constant_body env cb =
   let otab = opaque_tables env in
   match cb.const_body with
-  | Undef _ ->
+  | Undef _ | Primitive _ ->
      None
   | Def c ->
      Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
@@ -492,6 +495,7 @@ let constant_value_in env (kn,u) =
 	subst_instance_constr u b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
+    | Primitive p -> raise (NotEvaluableConst (IsPrimitive p))
 
 let constant_opt_value_in env cst =
   try Some (constant_value_in env cst)
@@ -503,7 +507,13 @@ let evaluable_constant kn env =
     match cb.const_body with
     | Def _ -> true
     | OpaqueDef _ -> false
-    | Undef _ -> false
+    | Undef _ | Primitive _ -> false
+
+let is_primitive env c =
+  let cb = lookup_constant c env in
+  match cb.Declarations.const_body with
+  | Declarations.Primitive _ -> true
+  | _ -> false
 
 let polymorphic_constant cst env =
   Declareops.constant_is_polymorphic (lookup_constant cst env)
@@ -743,29 +753,4 @@ let is_type_in_type env r =
   | IndRef ind -> type_in_type_ind ind env
   | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env
 
-(*spiwack: the following functions assemble the pieces of the retroknowledge
-   note that the "consistent" register function is available in the module
-   Safetyping, Environ only synchronizes the proactive and the reactive parts*)
-
-open Retroknowledge
-
-(* lifting of the "get" functions works also for "mem"*)
-let retroknowledge f env =
-  f env.retroknowledge
-
-let registered env field =
-    retroknowledge mem env field
-
-let register_one env field entry =
-  { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry }
-
-(* [register env field entry] may register several fields when needed *)
-let register env field gr =
-  match field with
-  | KInt31 Int31Type ->
-    let i31c = match gr with
-      | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1)
-      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
-    in
-    register_one (register_one env (KInt31 Int31Constructor) i31c) field gr
-  | field -> register_one env field gr
+let set_retroknowledge env r = { env with retroknowledge = r }