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, 21 insertions, 28 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 97ac3cdebb..1dc8eec0da 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -197,9 +197,18 @@ let rec subst_structure sub do_delta sign =
   in
   List.Smart.map subst_body sign
 
+and subst_retro : type a. Mod_subst.substitution -> a module_retroknowledge -> a module_retroknowledge =
+  fun subst retro ->
+    match retro with
+    | ModTypeRK as r -> r
+    | ModBodyRK l as r ->
+      let l' = List.Smart.map (subst_retro_action subst) l in
+      if l == l' then r else ModBodyRK l
+
 and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
   fun is_mod sub subst_impl do_delta mb ->
-  let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in
+    let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty;
+          mod_retroknowledge=retro; _ } = mb in
   let mp' = subst_mp sub mp in
   let sub =
     if ModPath.equal mp mp' then sub
@@ -209,8 +218,10 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body ->
   let ty' = subst_signature sub do_delta ty in
   let me' = subst_impl sub me in
   let aty' = Option.Smart.map (subst_expression sub id_delta) aty in
+  let retro' = subst_retro sub retro in
   let delta' = do_delta mb.mod_delta sub in
-  if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
+  if mp==mp' && me==me' && ty==ty' && aty==aty'
+     && retro==retro' && delta'==mb.mod_delta
   then mb
   else
     { mb with
@@ -218,7 +229,9 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body ->
       mod_expr = me';
       mod_type = ty';
       mod_type_alg = aty';
-      mod_delta = delta' }
+      mod_retroknowledge = retro';
+      mod_delta = delta';
+    }
 
 and subst_module sub do_delta mb =
   subst_body true sub subst_impl do_delta mb
@@ -259,32 +272,12 @@ let do_delta_dom_codom reso sub = subst_dom_codom_delta_resolver sub reso
 let subst_signature subst = subst_signature subst do_delta_codom
 let subst_structure subst = subst_structure subst do_delta_codom
 
-(** {6 Retroknowledge } *)
-
-(* spiwack: here comes the function which takes care of importing
-   the retroknowledge declared in the library *)
-(* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
-let add_retroknowledge =
-  let perform rkaction env = match rkaction with
-    | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) ->
-      Environ.register env f e
-    | _ ->
-      CErrors.anomaly ~label:"Modops.add_retroknowledge"
-        (Pp.str "had to import an unsupported kind of term.")
-  in
-  fun (ModBodyRK lclrk) env ->
-  (* The order of the declaration matters, for instance (and it's at the
-     time this comment is being written, the only relevent instance) the
-     int31 type registration absolutely needs int31 bits to be registered.
-     Since the local_retroknowledge is stored in reverse order (each new
-     registration is added at the top of the list) we need a fold_right
-     for things to go right (the pun is not intented). So we lose
-     tail recursivity, but the world will have exploded before any module
-     imports 10 000 retroknowledge registration.*)
-  List.fold_right perform lclrk env
-
 (** {6 Adding a module in the environment } *)
 
+let add_retroknowledge r env =
+  match r with
+  | ModBodyRK l -> List.fold_left Primred.add_retroknowledge env l
+
 let rec add_structure mp sign resolver linkinfo env =
   let add_one env (l,elem) = match elem with
     |SFBconst cb ->
@@ -399,7 +392,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	  let constant = lookup_constant con env in
 	  let l = make_inline delta r in
 	  match constant.const_body with
-	    | Undef _ | OpaqueDef _ -> l
+            | Undef _ | OpaqueDef _ | Primitive _ -> l
 	    | Def body ->
 	      let constr = Mod_subst.force_constr body in
               let ctx = Declareops.constant_polymorphic_context constant in