diff options
Diffstat (limited to 'kernel/cPrimitives.ml')
| -rw-r--r-- | kernel/cPrimitives.ml | 218 |
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 |