aboutsummaryrefslogtreecommitdiff
path: root/kernel/cPrimitives.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cPrimitives.ml')
-rw-r--r--kernel/cPrimitives.ml118
1 files changed, 90 insertions, 28 deletions
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 5cd91b4e74..9e0f574fa3 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -8,6 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(* Note: don't forget to update v_primitive in checker/values.ml if the *)
+(* number of primitives is changed. *)
+
open Univ
type t =
@@ -18,8 +21,11 @@ type t =
| Int63mul
| Int63div
| Int63mod
+ | Int63divs
+ | Int63mods
| Int63lsr
| Int63lsl
+ | Int63asr
| Int63land
| Int63lor
| Int63lxor
@@ -34,7 +40,10 @@ type t =
| Int63eq
| Int63lt
| Int63le
+ | Int63lts
+ | Int63les
| Int63compare
+ | Int63compares
| Float64opp
| Float64abs
| Float64eq
@@ -68,8 +77,11 @@ let parse = function
| "int63_mul" -> Int63mul
| "int63_div" -> Int63div
| "int63_mod" -> Int63mod
+ | "int63_divs" -> Int63divs
+ | "int63_mods" -> Int63mods
| "int63_lsr" -> Int63lsr
| "int63_lsl" -> Int63lsl
+ | "int63_asr" -> Int63asr
| "int63_land" -> Int63land
| "int63_lor" -> Int63lor
| "int63_lxor" -> Int63lxor
@@ -84,7 +96,10 @@ let parse = function
| "int63_eq" -> Int63eq
| "int63_lt" -> Int63lt
| "int63_le" -> Int63le
+ | "int63_lts" -> Int63lts
+ | "int63_les" -> Int63les
| "int63_compare" -> Int63compare
+ | "int63_compares" -> Int63compares
| "float64_opp" -> Float64opp
| "float64_abs" -> Float64abs
| "float64_eq" -> Float64eq
@@ -163,6 +178,12 @@ let hash = function
| Arrayset -> 46
| Arraycopy -> 47
| Arraylength -> 48
+ | Int63lts -> 49
+ | Int63les -> 50
+ | Int63divs -> 51
+ | Int63mods -> 52
+ | Int63asr -> 53
+ | Int63compares -> 54
(* Should match names in nativevalues.ml *)
let to_string = function
@@ -173,8 +194,11 @@ let to_string = function
| Int63mul -> "mul"
| Int63div -> "div"
| Int63mod -> "rem"
+ | Int63divs -> "divs"
+ | Int63mods -> "rems"
| Int63lsr -> "l_sr"
| Int63lsl -> "l_sl"
+ | Int63asr -> "a_sr"
| Int63land -> "l_and"
| Int63lor -> "l_or"
| Int63lxor -> "l_xor"
@@ -189,7 +213,10 @@ let to_string = function
| Int63eq -> "eq"
| Int63lt -> "lt"
| Int63le -> "le"
+ | Int63lts -> "lts"
+ | Int63les -> "les"
| Int63compare -> "compare"
+ | Int63compares -> "compares"
| Float64opp -> "fopp"
| Float64abs -> "fabs"
| Float64eq -> "feq"
@@ -268,37 +295,57 @@ let types =
PITT_param 1))
in
function
- | Int63head0 | Int63tail0 -> [int_ty; int_ty]
+ | Int63head0 | Int63tail0 ->
+ [int_ty], int_ty
| Int63add | Int63sub | Int63mul
| Int63div | Int63mod
- | Int63lsr | Int63lsl
- | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+ | Int63divs | Int63mods
+ | Int63lsr | Int63lsl | Int63asr
+ | Int63land | Int63lor | Int63lxor ->
+ [int_ty; int_ty], int_ty
| Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
- [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)]
+ [int_ty; int_ty], PITT_ind (PIT_carry, int_ty)
| Int63mulc | Int63diveucl ->
- [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
- | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
- | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+ [int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty))
+ | Int63eq | Int63lt | Int63le | Int63lts | Int63les ->
+ [int_ty; int_ty], PITT_ind (PIT_bool, ())
+ | Int63compare | Int63compares ->
+ [int_ty; int_ty], PITT_ind (PIT_cmp, ())
| Int63div21 ->
- [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
- | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
+ [int_ty; int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty))
+ | Int63addMulDiv ->
+ [int_ty; int_ty; int_ty], int_ty
| Float64opp | Float64abs | Float64sqrt
- | Float64next_up | Float64next_down -> [float_ty; float_ty]
- | Float64ofInt63 -> [int_ty; float_ty]
- | Float64normfr_mantissa -> [float_ty; int_ty]
- | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))]
- | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
- | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
- | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
- | Float64add | Float64sub | Float64mul
- | Float64div -> [float_ty; float_ty; float_ty]
- | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
- | Arraymake -> [int_ty; PITT_param 1; array_ty]
- | Arrayget -> [array_ty; int_ty; PITT_param 1]
- | Arraydefault -> [array_ty; PITT_param 1]
- | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty]
- | Arraycopy -> [array_ty; array_ty]
- | Arraylength -> [array_ty; int_ty]
+ | Float64next_up | Float64next_down ->
+ [float_ty], float_ty
+ | Float64ofInt63 ->
+ [int_ty], float_ty
+ | Float64normfr_mantissa ->
+ [float_ty], int_ty
+ | Float64frshiftexp ->
+ [float_ty], PITT_ind (PIT_pair, (float_ty, int_ty))
+ | Float64eq | Float64lt | Float64le ->
+ [float_ty; float_ty], PITT_ind (PIT_bool, ())
+ | Float64compare ->
+ [float_ty; float_ty], PITT_ind (PIT_f_cmp, ())
+ | Float64classify ->
+ [float_ty], PITT_ind (PIT_f_class, ())
+ | Float64add | Float64sub | Float64mul | Float64div ->
+ [float_ty; float_ty], float_ty
+ | Float64ldshiftexp ->
+ [float_ty; int_ty], float_ty
+ | Arraymake ->
+ [int_ty; PITT_param 1], array_ty
+ | Arrayget ->
+ [array_ty; int_ty], PITT_param 1
+ | Arraydefault ->
+ [array_ty], PITT_param 1
+ | Arrayset ->
+ [array_ty; int_ty; PITT_param 1], array_ty
+ | Arraycopy ->
+ [array_ty], array_ty
+ | Arraylength ->
+ [array_ty], int_ty
let one_param =
(* currently if there's a parameter it's always this *)
@@ -314,8 +361,11 @@ let params = function
| Int63mul
| Int63div
| Int63mod
+ | Int63divs
+ | Int63mods
| Int63lsr
| Int63lsl
+ | Int63asr
| Int63land
| Int63lor
| Int63lxor
@@ -330,7 +380,10 @@ let params = function
| Int63eq
| Int63lt
| Int63le
+ | Int63lts
+ | Int63les
| Int63compare
+ | Int63compares
| Float64opp
| Float64abs
| Float64eq
@@ -367,8 +420,11 @@ let univs = function
| Int63mul
| Int63div
| Int63mod
+ | Int63divs
+ | Int63mods
| Int63lsr
| Int63lsl
+ | Int63asr
| Int63land
| Int63lor
| Int63lxor
@@ -383,7 +439,10 @@ let univs = function
| Int63eq
| Int63lt
| Int63le
+ | Int63lts
+ | Int63les
| Int63compare
+ | Int63compares
| Float64opp
| Float64abs
| Float64eq
@@ -420,14 +479,17 @@ type args_red = arg_kind list
(* Invariant only argument of type int63, float or an inductive can
have kind Kwhnf *)
-let arity t = let sign = types t in nparams t + List.length sign - 1
+let arity t =
+ nparams t + List.length (fst (types t))
let kind t =
let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in
let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in
- params (nparams t) @ List.map args (CList.drop_last (types t))
+ params (nparams t) @ List.map args (fst (types t))
-let types t = params t, types t
+let types t =
+ let args_ty, ret_ty = types t in
+ params t, args_ty, ret_ty
(** Special Entries for Register **)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:33:05 +0000