Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.

Reviewed-by: ppedrot

8 files changed, 81 insertions, 54 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
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index c2b087f061..b5604d0593 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -35,6 +35,7 @@ type instruction =
   | Kpush
   | Kpop of int
   | Kpush_retaddr of Label.t
+  | Kshort_apply of int
   | Kapply of int
   | Kappterm of int * int
   | Kreturn of int
@@ -93,6 +94,7 @@ let rec pp_instr i =
   | Kpush -> str "push"
   | Kpop n -> str "pop " ++ int n
   | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+  | Kshort_apply n -> str "short_apply " ++ int n
   | Kapply n -> str "apply " ++ int n
   | Kappterm(n, m) ->
       str "appterm " ++ int n ++ str ", " ++ int m
@@ -146,8 +148,8 @@ let rec pp_instr i =
         (Constant.print (fst id))
 
   | Kcamlprim (op, lbl) ->
-    str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
-    pp_lbl lbl
+    str "camlcall " ++ str (CPrimitives.to_string op) ++ str ", branch " ++
+    pp_lbl lbl ++ str " on accu"
 
 and pp_bytecodes c =
   match c with
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index eeca0d2ad1..d9e2d91177 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -30,6 +30,7 @@ type instruction =
   | Kpush                               (** sp = accu :: sp *)
   | Kpop of int                         (** sp = skipn n sp *)
   | Kpush_retaddr of Label.t            (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
+  | Kshort_apply of int                 (** number of arguments (arguments on top of stack) *)
   | Kapply of int                       (** number of arguments (arguments on top of stack) *)
   | Kappterm of int * int               (** number of arguments, slot size *)
   | Kreturn of int                      (** slot size *)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 7d3b3469b0..b4d97228bf 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -461,7 +461,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont =
   | None ->
       if nargs <= 4 then
         comp_args comp_arg cenv args sz
-          (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont)))
+          (Kpush :: (comp_fun cenv f (sz+nargs) (Kshort_apply nargs :: cont)))
       else
         let lbl,cont1 = label_code cont in
         Kpush_retaddr lbl ::
@@ -757,26 +757,25 @@ let rec compile_lam env cenv lam sz cont =
     let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
     comp_args (compile_lam env) cenv args sz cont
 
-  | Lprim ((kn,u), op, args) when is_caml_prim op ->
+  | Lprim (kn, op, args) when is_caml_prim op ->
     let arity = CPrimitives.arity op in
     let nparams = CPrimitives.nparams op in
     let nargs = arity - nparams in
-    assert (arity = Array.length args && arity <= 4);
+    assert (arity = Array.length args && arity <= 4 && nargs >= 1);
     let (jump, cont) = make_branch cont in
     let lbl_default = Label.create () in
     let default =
-      let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in
+      let cont = [Kshort_apply arity; jump] in
+      let cont = Kpush :: compile_get_global cenv kn (sz + arity) cont in
       let cont =
-        if Univ.Instance.is_empty u then cont
-        else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont)
-      in
-      Klabel lbl_default ::
-      Kpush ::
-      if Int.equal nparams 0 then cont
-      else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont)
-    in
+        if Int.equal nparams 0 then cont
+        else
+          let params = Array.sub args 0 nparams in
+          Kpush :: comp_args (compile_lam env) cenv params (sz + nargs) cont in
+      Klabel lbl_default :: cont in
     fun_code := Ksequence default :: !fun_code;
-    comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont)
+    let cont = Kcamlprim (op, lbl_default) :: cont in
+    comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz cont
 
   | Lprim (kn, op, args) ->
     comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont)
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index caa263432e..44e933ef26 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -300,8 +300,11 @@ let emit_instr env = function
       out env opPOP; out_int env n
   | Kpush_retaddr lbl ->
       out env opPUSH_RETADDR; out_label env lbl
+  | Kshort_apply n ->
+      assert (1 <= n && n <= 4);
+      out env(opAPPLY1 + n - 1)
   | Kapply n ->
-      if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n)
+      out env opAPPLY; out_int env n
   | Kappterm(n, sz) ->
       if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz)
                else (out env opAPPTERM; out_int env n; out_int env sz)