diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/vmbytecodes.ml | 2 | ||||
| -rw-r--r-- | kernel/vmbytecodes.mli | 1 | ||||
| -rw-r--r-- | kernel/vmbytegen.ml | 4 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 5 |
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) |