Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

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