diff options
| author | Maxime Dénès | 2015-07-06 17:04:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-07-06 17:04:10 +0200 |
| commit | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (patch) | |
| tree | a650355330521a776719279328e82a47527d15a5 /kernel/byterun | |
| parent | 7ad2fe2bd30a07eb2495ea8cf902a24ef13a3627 (diff) | |
| parent | 2face8d77628ded64f7d0a824f4b377694b9d7fd (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 28 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 9 |
4 files changed, 33 insertions, 7 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1be3e65113..29e33d349b 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -60,7 +60,7 @@ void init_arity () { arity[BRANCH]=arity[ISCONST]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[ARECONST]=2; + arity[ARECONST]=arity[PROJ]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 9cbf4077e2..8c5ab0ecbd 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -36,6 +36,7 @@ enum instructions { SWITCH, PUSHFIELDS, GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, + PROJ, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, ACCUMULATE, diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index ddbde9d385..0a121dc32e 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -878,8 +878,32 @@ value coq_interprete caml_modify(&Field(accu, *pc),*sp); sp++; pc++; Next; - } - + } + + + Instruct(PROJ){ + print_instr("PROJ"); + if (Is_accu (accu)) { + /* Skip over the index of projected field */ + pc++; + /* Save the argument on the stack */ + *--sp = accu; + /* Create atom */ + Alloc_small(accu, 2, ATOM_PROJ_TAG); + Field(accu, 0) = Field(coq_global_data, *pc); + Field(accu, 1) = sp[0]; + sp[0] = accu; + /* Create accumulator */ + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = *sp++; + } else { + accu = Field(accu, *pc++); + } + pc++; + Next; + } + /* Integer constants */ Instruct(CONST0){ diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 1bf493e2c0..1590a2141d 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -22,10 +22,11 @@ #define ATOM_ID_TAG 0 #define ATOM_IDDEF_TAG 1 #define ATOM_INDUCTIVE_TAG 2 -#define ATOM_FIX_TAG 3 -#define ATOM_SWITCH_TAG 4 -#define ATOM_COFIX_TAG 5 -#define ATOM_COFIXEVALUATED_TAG 6 +#define ATOM_PROJ_TAG 3 +#define ATOM_FIX_TAG 4 +#define ATOM_SWITCH_TAG 5 +#define ATOM_COFIX_TAG 6 +#define ATOM_COFIXEVALUATED_TAG 7 |