Skip to content

Commit

Permalink
Add a PUSHENVACCMANY opcode.
Browse files Browse the repository at this point in the history
When closures are nested inside closures, it might happen that several
consecutive values from the environment of the outer closure are pushed
onto the stack in order to create the inner closure. This opcode replaces
a repeated sequence of opcodes "PUSH; ENVACC" of decreasing indices.
  • Loading branch information
silene committed May 3, 2024
1 parent d9c5107 commit 61ee389
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 4 deletions.
14 changes: 14 additions & 0 deletions kernel/byterun/coq_interp.c
Original file line number Diff line number Diff line change
Expand Up @@ -480,6 +480,20 @@ value coq_interprete
accu = Field(coq_env, 2 + *pc++);
Next;
}

Instruct(PUSHENVACCMANY) {
int first = *pc++;
int size = *pc++;
int i;
print_instr("PUSHENVACCMANY");
first += 2;
sp -= size;
for (i = 1; i < size; ++i) sp[i - 1] = Field(coq_env, first + i);
sp[size - 1] = accu;
accu = Field(coq_env, first);
Next;
}

/* Function application */

Instruct(PUSH_RETADDR) {
Expand Down
1 change: 1 addition & 0 deletions kernel/genOpcodeFiles.ml
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ let opcodes =
"PUSHENVACC2", 0;
"PUSHENVACC3", 0;
"PUSHENVACC", 1;
"PUSHENVACCMANY", 2;
"PUSH_RETADDR", 1;
"APPLY", 1;
"APPLY1", 0;
Expand Down
18 changes: 14 additions & 4 deletions kernel/vmemitcodes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -433,10 +433,20 @@ let rec emit env insns remaining = match insns with
else (out env opPUSHACC; out_int env n);
emit env c remaining
| Kpush :: Kenvacc n :: c ->
if n >= 0 && n <= 3
then out env(opPUSHENVACC0 + n)
else (out env opPUSHENVACC; out_int env n);
emit env c remaining
let rec aux n c nb =
match c with
| Kpush :: Kenvacc j :: c when j = n - nb -> aux n c (nb + 1)
| _ -> (nb, c) in
let (nb, c') = aux n c 1 in
if nb >= 3 || (nb >= 2 && n > 3)
then (
out env opPUSHENVACCMANY; out_int env (n - nb + 1); out_int env nb;
emit env c' remaining)
else (
if n >= 0 && n <= 3
then out env (opPUSHENVACC0 + n)
else (out env opPUSHENVACC; out_int env n);
emit env c remaining)
| Kpush :: Koffsetclosure ofs :: c ->
if Int.equal ofs 0 || Int.equal ofs 1
then out env(opPUSHOFFSETCLOSURE0 + ofs)
Expand Down

0 comments on commit 61ee389

Please sign in to comment.