Make it more obvious when the calling convention of APPLY changes.

Despite their names, APPLY1 to APPLY4 are completely different from
APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return
address was already pushed on the stack, before the arguments were. On the
other hand, APPLY1 to APPLY4 insert the return address in the middle of
the already pushed arguments.

4 files changed, 9 insertions, 3 deletions

diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index c2b087f061..1783560694 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
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 3dc268ccdf..9500b88e60 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 ::
@@ -765,7 +765,7 @@ let rec compile_lam env cenv lam sz cont =
     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 = [Kgetglobal kn; Kshort_apply (arity + Univ.Instance.length u); jump] 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)
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)