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, 13 insertions, 150 deletions

diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0a2ef5300e..1554fe88da 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -9,157 +9,20 @@
 (************************************************************************)
 
 open Names
-open Constr
-
-type retroknowledge
-
-(** the following types correspond to the different "things"
-   the kernel can learn about.*)
-type int31_field =
-  | Int31Bits
-  | Int31Type
-  | Int31Constructor
-  | Int31Twice
-  | Int31TwicePlusOne
-  | Int31Phi
-  | Int31PhiInv
-  | Int31Plus
-  | Int31PlusC
-  | Int31PlusCarryC
-  | Int31Minus
-  | Int31MinusC
-  | Int31MinusCarryC
-  | Int31Times
-  | Int31TimesC
-  | Int31Div21
-  | Int31Div
-  | Int31Diveucl
-  | Int31AddMulDiv
-  | Int31Compare
-  | Int31Head0
-  | Int31Tail0
-  | Int31Lor
-  | Int31Land
-  | Int31Lxor
-
-type field =
-  | KInt31 of int31_field
-
-val int31_field_of_string : string -> int31_field
-
-val int31_path : DirPath.t
-
-(** This type represent an atomic action of the retroknowledge. It
-   is stored in the compiled libraries 
-   As per now, there is only the possibility of registering things
-   the possibility of unregistering or changing the flag is under study *)
-type action =
-    | RKRegister of field * GlobRef.t
-
-
-(** initial value for retroknowledge *)
-val initial_retroknowledge : retroknowledge
-
-
-(** Given an identifier id (usually Const _)
-   and the continuation cont of the bytecode compilation
-   returns the compilation of id in cont if it has a specific treatment
-   or raises Not_found if id should be compiled as usual *)
-val get_vm_compiling_info  : retroknowledge -> GlobRef.t ->
-                             Cinstr.lambda array -> Cinstr.lambda
-(*Given an identifier id (usually Construct _)
-   and its argument array, returns a function that tries an ad-hoc optimisated
-   compilation (in the case of the 31-bit integers it means compiling them
-   directly into an integer)
-   raises Not_found if id should be compiled as usual, and expectingly
-   CBytecodes.NotClosed if the term is not a closed constructor pattern
-   (a constant for the compiler) *)
-val get_vm_constant_static_info : retroknowledge -> GlobRef.t ->
-                                   constr array -> Cinstr.lambda
-
-(*Given an identifier id (usually Construct _ )
-   its argument array and a continuation, returns the compiled version
-   of id+args+cont when id has a specific treatment (in the case of
-   31-bit integers, that would be the dynamic compilation into integers)
-   or raises Not_found if id should be compiled as usual *)
-val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t ->
-                                   Cinstr.lambda array -> Cinstr.lambda
-
-(** Given a type identifier, this function is used before compiling a match
-   over this type. In the case of 31-bit integers for instance, it is used
-   to add the instruction sequence which would perform a dynamic decompilation
-   in case the argument of the match is not in coq representation *)
-val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda
-                                                       -> Cinstr.lambda
-
-(** Given a type identifier, this function is used by pretyping/vnorm.ml to
-   recover the elements of that type from their compiled form if it's non
-   standard (it is used (and can be used) only when the compiled form
-   is not a block *)
-val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr
-
-
-val get_native_compiling_info  : retroknowledge -> GlobRef.t -> Nativeinstr.prefix ->
-				 Nativeinstr.lambda array -> Nativeinstr.lambda
-
-val get_native_constant_static_info : retroknowledge -> GlobRef.t ->
-                                      constr array -> Nativeinstr.lambda
-
-val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t ->
-                                       Nativeinstr.prefix -> constructor ->
-				       Nativeinstr.lambda array ->
-				       Nativeinstr.lambda
-
-val get_native_before_match_info : retroknowledge -> GlobRef.t ->
-				   Nativeinstr.prefix -> constructor ->
-				   Nativeinstr.lambda -> Nativeinstr.lambda
-
-
-(** the following functions are solely used in Environ and Safe_typing to implement
-   the functions  register and unregister (and mem) of Environ *)
-val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge
-val mem : retroknowledge -> field -> bool
-(* val remove : retroknowledge -> field -> retroknowledge *)
-val find : retroknowledge -> field -> GlobRef.t
-
-
-(** Dispatching type for the above [get_*] functions. *)
-type reactive_info = {(*information required by the compiler of the VM *)
-  vm_compiling :
-      (*fastcomputation flag -> continuation -> result *)
-      (bool -> Cinstr.lambda array -> Cinstr.lambda)
-      option;
-  vm_constant_static :
-      (*fastcomputation flag -> constructor -> args -> result*)
-      (bool -> constr array -> Cinstr.lambda)
-      option;
-  vm_constant_dynamic :
-      (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
-      (bool -> Cinstr.lambda array -> Cinstr.lambda)
-      option;
-  (* fastcomputation flag -> cont -> result *)
-  vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option;
-  (* tag (= compiled int for instance) -> result *)
-  vm_decompile_const : (int -> constr) option;
-
-  native_compiling :
-      (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->
-       Nativeinstr.lambda) option;
-
-  native_constant_static :
-      (bool -> constr array -> Nativeinstr.lambda) option;
-
-  native_constant_dynamic :
-      (bool -> Nativeinstr.prefix -> constructor ->
-       Nativeinstr.lambda array -> Nativeinstr.lambda) option;
-
-  native_before_match : (bool -> Nativeinstr.prefix -> constructor ->
-			 Nativeinstr.lambda -> Nativeinstr.lambda) option
 
+type retroknowledge = {
+    retro_int63 : Constant.t option;
+    retro_bool : (constructor * constructor) option; (* true, false *)
+    retro_carry : (constructor * constructor) option; (* C0, C1 *)
+    retro_pair : constructor option;
+    retro_cmp : (constructor * constructor * constructor) option;
+                    (* Eq, Lt, Gt *)
+    retro_refl : constructor option;
 }
 
-val empty_reactive_info : reactive_info
+val empty : retroknowledge
 
-(** Hook to be set after the compiler are installed to dispatch fields
-    into the above [get_*] functions. *)
-val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t
+type action =
+  | Register_ind of CPrimitives.prim_ind * inductive
+  | Register_type of CPrimitives.prim_type * Constant.t
+  | Register_inline of Constant.t