aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cPrimitives.ml76
-rw-r--r--kernel/cPrimitives.mli4
-rw-r--r--kernel/nativecode.ml5
-rw-r--r--kernel/typeops.ml13
4 files changed, 60 insertions, 38 deletions
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 6ef0e9fa15..9e0f574fa3 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -295,38 +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
| Int63divs | Int63mods
| Int63lsr | Int63lsl | Int63asr
- | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+ | 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 | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
- | Int63compare | Int63compares -> [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 *)
@@ -460,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 **)
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index de90179726..6661851d53 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -140,8 +140,8 @@ val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
val univs : t -> Univ.AUContext.t
-val types : t -> Constr.rel_context * ind_or_type list
-(** Parameters * Reduction relevant arguments and output type
+val types : t -> Constr.rel_context * ind_or_type list * ind_or_type
+(** Parameters * Reduction relevant arguments * output type
XXX we could reify universes in ind_or_type (currently polymorphic types
like array are assumed to use universe 0). *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9ce388929c..22bbcb8a65 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -994,9 +994,8 @@ let extract_prim ml_of l =
let decl = ref [] in
let cond = ref [] in
let type_args p =
- let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in
- let params, sign = CPrimitives.types p in
- List.length params, Array.of_list (aux sign) in
+ let params, args_ty, _ = CPrimitives.types p in
+ List.length params, Array.of_list args_ty in
let rec aux l =
match l with
| Lprim(prefix,kn,p,args) ->
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 741491c917..1b1aa84e6b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -785,15 +785,16 @@ let type_of_prim env u t =
| PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t
| PITT_param i -> Constr.mkRel (n+i)
in
- let rec nary_op n = function
- | [] -> assert false
- | [ret_ty] -> tr_type n ret_ty
+ let rec nary_op n ret_ty = function
+ | [] -> tr_type n ret_ty
| arg_ty :: r ->
- Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r)
+ Constr.mkProd (Context.nameR (Id.of_string "x"),
+ tr_type n arg_ty, nary_op (n + 1) ret_ty r)
in
- let params, sign = types t in
+ let params, args_ty, ret_ty = types t in
assert (AUContext.size (univs t) = Instance.length u);
- Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params)
+ Vars.subst_instance_constr u
+ (Term.it_mkProd_or_LetIn (nary_op 0 ret_ty args_ty) params)
let type_of_prim_or_type env u = let open CPrimitives in
function
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:25:13 +0000