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, 140 insertions, 78 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 5b91a9b572..da5c4fb07b 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -9,85 +9,147 @@
 (************************************************************************)
 
 type t =
-  | Int31head0
-  | Int31tail0
-  | Int31add
-  | Int31sub
-  | Int31mul
-  | Int31div
-  | Int31mod
-(*
-  | Int31lsr
-  | Int31lsl
- *)
-  | Int31land
-  | Int31lor
-  | Int31lxor
-  | Int31addc
-  | Int31subc
-  | Int31addcarryc
-  | Int31subcarryc
-  | Int31mulc
-  | Int31diveucl
-  | Int31div21
-  | Int31addmuldiv
-  | Int31eq
-  | Int31lt
-  | Int31le
-  | Int31compare
+  | Int63head0
+  | Int63tail0
+  | Int63add
+  | Int63sub
+  | Int63mul
+  | Int63div
+  | Int63mod
+  | Int63lsr
+  | Int63lsl
+  | Int63land
+  | Int63lor
+  | Int63lxor
+  | Int63addc
+  | Int63subc
+  | Int63addCarryC
+  | Int63subCarryC
+  | Int63mulc
+  | Int63diveucl
+  | Int63div21
+  | Int63addMulDiv
+  | Int63eq
+  | Int63lt
+  | Int63le
+  | Int63compare
+
+let equal (p1 : t) (p2 : t) =
+  p1 == p2
 
 let hash = function
-  | Int31head0 -> 1
-  | Int31tail0 -> 2
-  | Int31add -> 3
-  | Int31sub -> 4
-  | Int31mul -> 5
-  | Int31div -> 6
-  | Int31mod -> 7
-(*
-  | Int31lsr -> 8
-  | Int31lsl -> 9
- *)
-  | Int31land -> 10
-  | Int31lor -> 11
-  | Int31lxor -> 12
-  | Int31addc -> 13
-  | Int31subc -> 14
-  | Int31addcarryc -> 15
-  | Int31subcarryc -> 16
-  | Int31mulc -> 17
-  | Int31diveucl -> 18
-  | Int31div21 -> 19
-  | Int31addmuldiv -> 20
-  | Int31eq -> 21
-  | Int31lt -> 22
-  | Int31le -> 23
-  | Int31compare -> 24
+  | Int63head0 -> 1
+  | Int63tail0 -> 2
+  | Int63add -> 3
+  | Int63sub -> 4
+  | Int63mul -> 5
+  | Int63div -> 6
+  | Int63mod -> 7
+  | Int63lsr -> 8
+  | Int63lsl -> 9
+  | Int63land -> 10
+  | Int63lor -> 11
+  | Int63lxor -> 12
+  | Int63addc -> 13
+  | Int63subc -> 14
+  | Int63addCarryC -> 15
+  | Int63subCarryC -> 16
+  | Int63mulc -> 17
+  | Int63diveucl -> 18
+  | Int63div21 -> 19
+  | Int63addMulDiv -> 20
+  | Int63eq -> 21
+  | Int63lt -> 22
+  | Int63le -> 23
+  | Int63compare -> 24
 
+(* Should match names in nativevalues.ml *)
 let to_string = function
-  | Int31head0 -> "head0"
-  | Int31tail0 -> "tail0"
-  | Int31add -> "add"
-  | Int31sub -> "sub"
-  | Int31mul -> "mul"
-  | Int31div -> "div"
-  | Int31mod -> "mod"
-(*
-  | Int31lsr -> "l_sr"
-  | Int31lsl -> "l_sl"
- *)
-  | Int31land -> "l_and"
-  | Int31lor -> "l_or"
-  | Int31lxor -> "l_xor"
-  | Int31addc -> "addc"
-  | Int31subc -> "subc"
-  | Int31addcarryc -> "addcarryc"
-  | Int31subcarryc -> "subcarryc"
-  | Int31mulc -> "mulc"
-  | Int31diveucl -> "diveucl"
-  | Int31div21 -> "div21"
-  | Int31addmuldiv -> "addmuldiv"
-  | Int31eq -> "eq"
-  | Int31lt -> "lt"
-  | Int31le -> "le"
-  | Int31compare -> "compare"
+  | Int63head0 -> "head0"
+  | Int63tail0 -> "tail0"
+  | Int63add -> "add"
+  | Int63sub -> "sub"
+  | Int63mul -> "mul"
+  | Int63div -> "div"
+  | Int63mod -> "rem"
+  | Int63lsr -> "l_sr"
+  | Int63lsl -> "l_sl"
+  | Int63land -> "l_and"
+  | Int63lor -> "l_or"
+  | Int63lxor -> "l_xor"
+  | Int63addc -> "addc"
+  | Int63subc -> "subc"
+  | Int63addCarryC -> "addCarryC"
+  | Int63subCarryC -> "subCarryC"
+  | Int63mulc -> "mulc"
+  | Int63diveucl -> "diveucl"
+  | Int63div21 -> "div21"
+  | Int63addMulDiv -> "addMulDiv"
+  | Int63eq -> "eq"
+  | Int63lt -> "lt"
+  | Int63le -> "le"
+  | Int63compare -> "compare"
+
+type arg_kind =
+  | Kparam (* not needed for the evaluation of the primitive when it reduces *)
+  | Kwhnf  (* need to be reduced in whnf before reducing the primitive *)
+  | Karg   (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *)
+
+type args_red = arg_kind list
+
+(* Invariant only argument of type int63 or an inductive can
+   have kind Kwhnf *)
+
+let kind = function
+  | Int63head0 | Int63tail0 -> [Kwhnf]
+
+  | Int63add | Int63sub | Int63mul
+  | Int63div | Int63mod
+  | Int63lsr | Int63lsl
+  | Int63land | Int63lor | Int63lxor
+  | Int63addc | Int63subc
+  | Int63addCarryC | Int63subCarryC  | Int63mulc | Int63diveucl
+  | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf]
+
+  | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf]
+
+let arity = function
+  | Int63head0 | Int63tail0 -> 1
+  | Int63add | Int63sub | Int63mul
+  | Int63div | Int63mod
+  | Int63lsr | Int63lsl
+  | Int63land | Int63lor | Int63lxor
+  | Int63addc | Int63subc
+  | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl
+  | Int63eq | Int63lt | Int63le
+  | Int63compare -> 2
+
+  | Int63div21 | Int63addMulDiv -> 3
+
+(** Special Entries for Register **)
+
+type prim_ind =
+  | PIT_bool
+  | PIT_carry
+  | PIT_pair
+  | PIT_cmp
+
+type prim_type =
+  | PT_int63
+
+type op_or_type =
+  | OT_op of t
+  | OT_type of prim_type
+
+let prim_ind_to_string = function
+  | PIT_bool -> "bool"
+  | PIT_carry -> "carry"
+  | PIT_pair -> "pair"
+  | PIT_cmp -> "cmp"
+
+let prim_type_to_string = function
+  | PT_int63 -> "int63"
+
+let op_or_type_to_string = function
+  | OT_op op -> to_string op
+  | OT_type t -> prim_type_to_string t