diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /kernel/byterun | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'kernel/byterun')
-rw-r--r-- | kernel/byterun/coq_fix_code.c | 30 | ||||
-rw-r--r-- | kernel/byterun/coq_instruct.h | 14 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.c | 356 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.c | 7 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.h | 1 | ||||
-rw-r--r-- | kernel/byterun/coq_values.c | 3 | ||||
-rw-r--r-- | kernel/byterun/coq_values.h | 14 |
7 files changed, 281 insertions, 144 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4616580d..70648b44 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -27,31 +27,31 @@ void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= - arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=arity[PUSHACC6]= - arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=arity[ENVACC4]= - arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=arity[PUSHENVACC4]= - arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= + arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= + arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]= + arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]= + arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]= + arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= + arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=arity[MAKEPROD]= 0; + arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= - arity[PUSH_RETADDR]= - arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]= - arity[GRAB]=arity[COGRAB]= - arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]= - arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= - arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]= - arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]= - arity[ACCUMULATECOND]= 1; + arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= + arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= + arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= + arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= + arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= + arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[SWITCH]=0; + arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; } #endif /* THREADED_CODE */ @@ -150,7 +150,7 @@ value coq_tcode_of_code (value code, value size) { block_size = sizes >> 16; sizes = const_size + block_size; for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; }; - } else if (instr == CLOSUREREC) { + } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) { uint32 i, n; COPY32(q,p); p++; /* ndefs */ n = 3 + 2*(*q); /* ndefs, nvars, start, typlbls,lbls*/ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index d3b07526..89616c5f 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -22,18 +22,20 @@ enum instructions { PUSH_RETADDR, APPLY, APPLY1, APPLY2, APPLY3, APPTERM, APPTERM1, APPTERM2, APPTERM3, - RETURN, RESTART, GRAB, GRABREC, COGRAB, - CLOSURE, CLOSUREREC, + RETURN, RESTART, GRAB, GRABREC, + CLOSURE, CLOSUREREC, CLOSURECOFIX, OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE, PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, PUSHOFFSETCLOSURE, GETGLOBAL, PUSHGETGLOBAL, - MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, - MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, - FORCE, SWITCH, PUSHFIELD, + MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4, + SWITCH, PUSHFIELDS, + GETFIELD0, GETFIELD1, GETFIELD, + SETFIELD0, SETFIELD1, SETFIELD, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, ACCUMULATECOND, STOP + ACCUMULATE, ACCUMULATECOND, + MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, STOP }; #endif /* _COQ_INSTRUCT_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8bfe78eb..0f91a7e3 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -65,6 +65,13 @@ sp is a local copy of the global variable extern_sp. */ # define print_int(i) #endif +/* Wrapper pour caml_modify */ +#ifdef OCAML_307 +#define CAML_MODIFY(a,b) modify(a,b) +#else +#define CAML_MODIFY(a,b) caml_modify(a,b) +#endif + /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -164,7 +171,7 @@ value coq_interprete #else opcode_t curr_instr; #endif - print_instr("Enter Interpreter"); + print_instr("Enter Interpreter"); if (coq_pc == NULL) { /* Interpreter is initializing */ print_instr("Interpreter is initializing"); #ifdef THREADED_CODE @@ -383,6 +390,17 @@ value coq_interprete coq_extra_args = 2; goto check_stacks; } + /* Stack checks */ + + check_stacks: + print_instr("check_stacks"); + if (sp < coq_stack_threshold) { + coq_sp = sp; + realloc_coq_stack(Coq_stack_threshold); + sp = coq_sp; + } + Next; + /* Fall through CHECK_SIGNALS */ Instruct(APPTERM) { int nargs = *pc++; @@ -438,6 +456,7 @@ value coq_interprete Instruct(RETURN) { print_instr("RETURN"); + print_int(*pc); sp += *pc++; if (coq_extra_args > 0) { coq_extra_args--; @@ -485,30 +504,6 @@ value coq_interprete Next; } - Instruct(COGRAB){ - int required = *pc++; - print_instr("COGRAB"); - if(forcable == Val_true) { - print_instr("true"); - /* L'instruction précédante est FORCE */ - if (coq_extra_args > 0) coq_extra_args--; - pc++; - forcable = Val_false; - } else { /* L'instruction précédante est APPLY */ - mlsize_t num_args, i; - num_args = 1 + coq_extra_args; /* arg1 + extra args */ - Alloc_small(accu, num_args + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i]; - Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ - sp += num_args; - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } - Next; - } Instruct(GRABREC) { int rec_pos = *pc++; /* commence a zero */ print_instr("GRABREC"); @@ -607,7 +602,59 @@ value coq_interprete accu = accu + 2 * start * sizeof(value); Next; } - + + Instruct(CLOSURECOFIX){ + int nfunc = *pc++; + int nvars = *pc++; + int start = *pc++; + int i, j , size; + value * p; + print_instr("CLOSURECOFIX"); + if (nvars > 0) *--sp = accu; + /* construction du vecteur de type */ + Alloc_small(accu, nfunc, 0); + for(i = 0; i < nfunc; i++) { + Field(accu,i) = (value)(pc+pc[i]); + } + pc += nfunc; + *--sp=accu; + + /* Creation des blocks accumulate */ + for(i=0; i < nfunc; i++) { + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = Val_int(1); + *--sp=accu; + } + /* creation des fonction cofix */ + + p = sp; + size = nfunc + nvars + 2; + for (i=0; i < nfunc; i++) { + + Alloc_small(accu, size, Closure_tag); + Code_val(accu) = pc+pc[i]; + for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j]; + Field(accu, size - 1) = p[nfunc]; + for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j]; + *--sp = accu; + /* creation du block contenant le cofix */ + + Alloc_small(accu,1, ATOM_COFIX_TAG); + Field(accu, 0) = sp[0]; + *sp = accu; + /* mise a jour du block accumulate */ + CAML_MODIFY(&Field(p[i], 1),*sp); + sp++; + } + pc += nfunc; + accu = p[start]; + sp = p + nfunc + 1 + nvars; + print_instr("ici4"); + Next; + } + + Instruct(PUSHOFFSETCLOSURE) { print_instr("PUSHOFFSETCLOSURE"); *--sp = accu; @@ -644,7 +691,7 @@ value coq_interprete /* Access to global variables */ Instruct(PUSHGETGLOBAL) { - print_instr("PUSHGETGLOBAL"); + print_instr("PUSH"); *--sp = accu; } /* Fallthrough */ @@ -703,38 +750,27 @@ value coq_interprete accu = block; Next; } + Instruct(MAKEBLOCK4) { + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK4"); + Alloc_small(block, 4, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + Field(block, 2) = sp[1]; + Field(block, 3) = sp[2]; + sp += 3; + accu = block; + Next; + } /* Access to components of blocks */ - -/* Branches and conditional branches */ - Instruct(FORCE) { - print_instr("FORCE"); - if (Is_block(accu) && Tag_val(accu) == Closure_tag) { - forcable = Val_true; - /* On pousse l'addresse de retour et l'argument */ - sp -= 3; - sp[0] = (value) (pc - 1); - sp[1] = coq_env; - sp[2] = Val_long(coq_extra_args); - /* On evalue le cofix */ - coq_extra_args = 0; - pc = Code_val(accu); - coq_env = accu; - goto check_stacks; - } else { - if (Is_block(accu)) print_int(Tag_val(accu)); - else print_instr("Not a block"); - } - Next; - } - - Instruct(SWITCH) { uint32 sizes = *pc++; print_instr("SWITCH"); - print_int(sizes); + print_int(sizes & 0xFFFF); if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); @@ -748,68 +784,79 @@ value coq_interprete } Next; } - Instruct(PUSHFIELD){ + + Instruct(PUSHFIELDS){ int i; int size = *pc++; - print_instr("PUSHFIELD"); + print_instr("PUSHFIELDS"); sp -= size; for(i=0;i<size;i++)sp[i] = Field(accu,i); Next; } - - Instruct(MAKESWITCHBLOCK) { - mlsize_t sz; - int i, annot; - code_t typlbl,swlbl; - print_instr("MAKESWITCHBLOCK"); - typlbl = (code_t)pc + *pc; - pc++; - swlbl = (code_t)pc + *pc; - pc++; - annot = *pc++; - sz = *pc++; - *--sp = accu; - *--sp=Field(coq_global_data, annot); - /* On sauve la pile */ - if (sz == 0) accu = Atom(0); - else { - Alloc_small(accu, sz, Default_tag); - if (Field(*sp, 2) == Val_true) { - for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; - }else{ - for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; - } - } - *--sp = accu; - /* On cree le zipper switch */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; - /* On cree l'atome */ - Alloc_small(accu, 2, ATOM_SWITCH_TAG); - Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; - sp++;sp[0] = accu; - /* On cree l'accumulateur */ - Alloc_small(accu, 2, Accu_tag); - Code_val(accu) = accumulate; - Field(accu,1) = *sp++; + + Instruct(GETFIELD0){ + print_instr("GETFIELD0"); + accu = Field(accu, 0); Next; } - /* Stack checks */ - - check_stacks: - print_instr("check_stacks"); - if (sp < coq_stack_threshold) { - coq_sp = sp; - realloc_coq_stack(Coq_stack_threshold); - sp = coq_sp; + Instruct(GETFIELD1){ + print_instr("GETFIELD1"); + accu = Field(accu, 1); + Next; } - Next; - /* Fall through CHECK_SIGNALS */ + Instruct(GETFIELD){ + print_instr("GETFIELD"); + accu = Field(accu, *pc); + pc++; + Next; + } + + Instruct(SETFIELD0){ + print_instr("SETFIELD0"); + CAML_MODIFY(&Field(accu, 0),*sp); + sp++; + Next; + } + + Instruct(SETFIELD1){ + int i, j, size, size_aux; + print_instr("SETFIELD1"); + CAML_MODIFY(&Field(accu, 1),*sp); + sp++; + Next; + } + + /* *sp = accu; + * Netoyage des cofix * + size = Wosize_val(accu); + for (i = 2; i < size; i++) { + accu = Field(*sp, i); + if (IS_EVALUATED_COFIX(accu)) { + size_aux = Wosize_val(accu); + *--sp = accu; + Alloc_small(accu, size_aux, Accu_tag); + for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j); + *sp = accu; + Alloc_small(accu, 1, ATOM_COFIX_TAG); + Field(accu, 0) = Field(Field(*sp, 1), 0); + CAML_MODIFY(&Field(*sp, 1), accu); + accu = *sp; sp++; + CAML_MODIFY(&Field(*sp, i), accu); + } + } + sp++; + Next; + } */ + + Instruct(SETFIELD){ + print_instr("SETFIELD"); + CAML_MODIFY(&Field(accu, *pc),*sp); + sp++; pc++; + Next; + } + /* Integer constants */ Instruct(CONST0){ @@ -854,14 +901,7 @@ value coq_interprete Next; } -/* Debugging and machine control */ - - Instruct(STOP){ - print_instr("STOP"); - coq_sp = sp; - return accu; - } - + /* Special operations for reduction of open term */ Instruct(ACCUMULATECOND) { int i, num; print_instr("ACCUMULATECOND"); @@ -869,7 +909,7 @@ value coq_interprete pc++; if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) { /* printf ("false\n"); - printf ("tag = %d", Tag_val(Field(accu,1))); */ + printf ("tag = %d", Tag_val(Field(accu,1))); */ num = Wosize_val(coq_env); for(i = 2; i < num; i++) *--sp = Field(accu,i); coq_extra_args = coq_extra_args + (num - 2); @@ -881,7 +921,7 @@ value coq_interprete }; /* printf ("true\n"); */ } - + Instruct(ACCUMULATE) { mlsize_t i, size; print_instr("ACCUMULATE"); @@ -896,7 +936,86 @@ value coq_interprete sp += 3; Next; } - + Instruct(MAKESWITCHBLOCK) { + print_instr("MAKESWITCHBLOCK"); + *--sp = accu; + accu = Field(accu,1); + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: + { + mlsize_t i, nargs; + print_instr("COFIX_TAG"); + sp-=2; + pc++; + sp[0] = (value) (pc + *pc); + sp[1] = coq_env; + coq_env = Field(accu,0); + accu = sp[2]; + sp[2] = Val_long(coq_extra_args); + nargs = Wosize_val(accu) - 2; + sp -= nargs; + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + *--sp = accu; + print_int(nargs); + coq_extra_args = nargs; + pc = Code_val(coq_env); + goto check_stacks; + } + case ATOM_COFIXEVALUATED_TAG: + { + print_instr("COFIX_EVAL_TAG"); + accu = Field(accu,1); + pc++; + pc = pc + *pc; + sp++; + Next; + } + default: + { + mlsize_t sz; + int i, annot; + code_t typlbl,swlbl; + print_instr("MAKESWITCHBLOCK"); + + typlbl = (code_t)pc + *pc; + pc++; + swlbl = (code_t)pc + *pc; + pc++; + annot = *pc++; + sz = *pc++; + *--sp=Field(coq_global_data, annot); + /* On sauve la pile */ + if (sz == 0) accu = Atom(0); + else { + Alloc_small(accu, sz, Default_tag); + if (Field(*sp, 2) == Val_true) { + for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; + }else{ + for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; + } + } + *--sp = accu; + /* On cree le zipper switch */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; + Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; + Field(accu, 4) = coq_env; + sp++;sp[0] = accu; + /* On cree l'atome */ + Alloc_small(accu, 2, ATOM_SWITCH_TAG); + Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; + sp++;sp[0] = accu; + /* On cree l'accumulateur */ + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = *sp++; + } + } + Next; + } + + + Instruct(MAKEACCU) { int i; print_instr("MAKEACCU"); @@ -921,6 +1040,15 @@ value coq_interprete Next; } +/* Debugging and machine control */ + + Instruct(STOP){ + print_instr("STOP"); + coq_sp = sp; + return accu; + } + + #ifndef THREADED_CODE default: /*fprintf(stderr, "%d\n", *pc);*/ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index db6aacb9..bfcb6812 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -34,7 +34,6 @@ int drawinstr; long coq_saved_sp_offset; value * coq_sp; -value forcable; /* Some predefined pointer code */ code_t accumulate; @@ -135,7 +134,6 @@ value init_coq_vm(value unit) /* ML */ init_coq_atom_tbl(40); /* Initialing the interpreter */ coq_all_transp = 0; - forcable = Val_false; init_coq_interpreter(); /* Some predefined pointer code */ @@ -266,8 +264,9 @@ value coq_set_drawinstr(value unit) return Val_unit; } -value coq_set_forcable (value unit) + +value coq_print_pointer(value p) { - forcable = Val_true; + printf("pointer = %X\n", p); return Val_unit; } diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 7c96e684..0d866dc7 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -43,7 +43,6 @@ extern int drawinstr; /* interp state */ extern value * coq_sp; -extern value forcable; /* Some predefined pointer code */ extern code_t accumulate; diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index baf3ab09..34b885e8 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -27,8 +27,7 @@ value coq_kind_of_closure(value v) { if (Is_instruction(c, GRAB)) return Val_int(0); if (Is_instruction(c, RESTART)) {is_app = 1; c++;} if (Is_instruction(c, GRABREC)) return Val_int(1+is_app); - if (Is_instruction(c, COGRAB)) return Val_int(3+is_app); - if (Is_instruction(c, MAKEACCU)) return Val_int(5); + if (Is_instruction(c, MAKEACCU)) return Val_int(3); return Val_int(0); } diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a186d62a..a5176f3f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -14,15 +14,25 @@ #include "alloc.h" #include "mlvalues.h" +#define Default_tag 0 +#define Accu_tag 0 + + + +#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 Accu_tag 0 -#define Default_tag 0 /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) +#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #endif /* _COQ_VALUES_ */ |