diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-27 13:29:22 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-27 13:29:22 +0000 |
| commit | 9c46109dcf1649080bb13bab4bf02f6d3a34045c (patch) | |
| tree | cd9b13611c479a3067638a871c2179422a9c055a /kernel/byterun | |
| parent | 7465eba1019dc082f94b85aab5b7c28ae61c77ef (diff) | |
changement des _sym par _comm dans setoid_ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 29 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 1 |
2 files changed, 27 insertions, 3 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 81880464b..0f91a7e3f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -55,7 +55,7 @@ sp is a local copy of the global variable extern_sp. */ # define Next break #endif -/*#define _COQ_DEBUG_ */ +/* #define _COQ_DEBUG_ */ #ifdef _COQ_DEBUG_ # define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) @@ -821,11 +821,34 @@ value coq_interprete } Instruct(SETFIELD1){ + int i, j, size, size_aux; print_instr("SETFIELD1"); CAML_MODIFY(&Field(accu, 1),*sp); - sp++; - Next; + 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"); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 48fba64bf..a5176f3f5 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,7 @@ /* 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_ */ |