Declare type of primitives in CPrimitives

Rather than in typeops

7 files changed, 77 insertions, 80 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d854cadd15..d433cdc1ba 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -90,58 +90,62 @@ let to_string = function
   | 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 prim_type =
+  | PT_int63
 
-type args_red = arg_kind list
+type 'a prim_ind =
+  | PIT_bool : unit prim_ind
+  | PIT_carry : prim_type prim_ind
+  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_cmp : unit prim_ind
 
-(* Invariant only argument of type int63 or an inductive can
-   have kind Kwhnf *)
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
-let kind = function
-  | Int63head0 | Int63tail0 -> [Kwhnf]
+type ind_or_type =
+  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
+  | PITT_type : prim_type -> ind_or_type
 
+let types =
+  let int_ty = PITT_type PT_int63 in
+  function
+  | Int63head0 | Int63tail0 -> [int_ty; int_ty]
   | Int63add | Int63sub | Int63mul
   | Int63div | Int63mod
   | Int63lsr | Int63lsl
-  | Int63land | Int63lor | Int63lxor
-  | Int63addc | Int63subc
-  | Int63addCarryC | Int63subCarryC  | Int63mulc | Int63diveucl
-  | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf]
+  | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+  | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
+     [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)]
+  | Int63mulc | Int63diveucl ->
+     [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+  | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
+  | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+  | Int63div21 ->
+     [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+  | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
 
-  | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf]
+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] *)
 
-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
+type args_red = arg_kind list
 
-  | Int63div21 | Int63addMulDiv -> 3
+(* Invariant only argument of type int63 or an inductive can
+   have kind Kwhnf *)
 
-(** Special Entries for Register **)
+let arity t = List.length (types t) - 1
 
-type prim_ind =
-  | PIT_bool
-  | PIT_carry
-  | PIT_pair
-  | PIT_cmp
+let kind t =
+  let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in
+  aux (arity t)
 
-type prim_type =
-  | PT_int63
+(** Special Entries for Register **)
 
 type op_or_type =
   | OT_op of t
   | OT_type of prim_type
 
-let prim_ind_to_string = function
+let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_bool -> "bool"
   | PIT_carry -> "carry"
   | PIT_pair -> "pair"
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 6913371caf..3c825a8018 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -53,18 +53,26 @@ val kind : t -> args_red
 
 (** Special Entries for Register **)
 
-type prim_ind =
-  | PIT_bool
-  | PIT_carry
-  | PIT_pair
-  | PIT_cmp
-
 type prim_type =
   | PT_int63
 
+type 'a prim_ind =
+  | PIT_bool : unit prim_ind
+  | PIT_carry : prim_type prim_ind
+  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_cmp : unit prim_ind
+
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
+
 type op_or_type =
   | OT_op of t
   | OT_type of prim_type
 
-val prim_ind_to_string : prim_ind -> string
+val prim_ind_to_string : 'a prim_ind -> string
 val op_or_type_to_string : op_or_type -> string
+
+type ind_or_type =
+  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
+  | PITT_type : prim_type -> ind_or_type
+
+val types : t -> ind_or_type list
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 873c6af93d..48a6ff4c96 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -36,5 +36,5 @@ let empty = {
 }
 
 type action =
-  | Register_ind of CPrimitives.prim_ind * inductive
-  | Register_type of CPrimitives.prim_type * Constant.t
+  | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
+  | Register_type : CPrimitives.prim_type * Constant.t -> action
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 2a7b390951..0eb3eaf940 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -23,5 +23,5 @@ type retroknowledge = {
 val empty : retroknowledge
 
 type action =
-  | Register_ind of CPrimitives.prim_ind * inductive
-  | Register_type of CPrimitives.prim_type * Constant.t
+  | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
+  | Register_type : CPrimitives.prim_type * Constant.t -> action
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e846b17aa0..52bd9a6ada 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1327,7 +1327,7 @@ let register_inline kn senv =
   let cb = {cb with const_inline_code = true} in
   let env = add_constant kn cb env in { senv with env}
 
-let check_register_ind ind r env =
+let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
   let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in
   let check_if b msg =
     if not b then
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b2f6668577..ae6993b0e2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -226,7 +226,7 @@ val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t
 (** {6 Retroknowledge / Native compiler } *)
 
 val register_inline : Constant.t -> safe_transformer0
-val register_inductive : inductive -> CPrimitives.prim_ind -> safe_transformer0
+val register_inductive : inductive -> 'a CPrimitives.prim_ind -> safe_transformer0
 
 val set_strategy :
   Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b87384d228..a967711a83 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -243,39 +243,24 @@ let type_of_prim env t =
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
     | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.")
   in
-  let rec nary_int63_op arity ty =
-    if Int.equal arity 0 then ty
-      else Constr.mkProd(Context.nameR (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty)
-  in
-  let return_ty =
-    let open CPrimitives in
-    match t with
-    | Int63head0
-    | Int63tail0
-    | Int63add
-    | Int63sub
-    | Int63mul
-    | Int63div
-    | Int63mod
-    | Int63lsr
-    | Int63lsl
-    | Int63land
-    | Int63lor
-    | Int63lxor
-    | Int63addMulDiv -> int_ty
-    | Int63eq
-    | Int63lt
-    | Int63le -> bool_ty ()
-    | Int63mulc
-    | Int63div21
-    | Int63diveucl -> pair_ty int_ty int_ty
-    | Int63addc
-    | Int63subc
-    | Int63addCarryC
-    | Int63subCarryC -> carry_ty int_ty
-    | Int63compare -> compare_ty ()
-  in
-  nary_int63_op (CPrimitives.arity t) return_ty
+  let open CPrimitives in
+  let tr_prim_type = function
+    | PT_int63 -> int_ty in
+  let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with
+    | PIT_bool, () -> bool_ty ()
+    | PIT_carry, t -> carry_ty (tr_prim_type t)
+    | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
+    | PIT_cmp, () -> compare_ty () in
+  let tr_type = function
+    | PITT_ind (i, a) -> tr_ind i a
+    | PITT_type t -> tr_prim_type t in
+  let rec nary_op = function
+    | [] -> assert false
+    | [ret_ty] -> tr_type ret_ty
+    | arg_ty :: r ->
+       let arg_ty = tr_type arg_ty in
+       Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in
+  nary_op (types t)
 
 let type_of_prim_or_type env = let open CPrimitives in
   function