From 9c46109dcf1649080bb13bab4bf02f6d3a34045c Mon Sep 17 00:00:00 2001
From: bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 27 Oct 2006 13:29:22 +0000
Subject: 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
---
 kernel/byterun/coq_interp.c | 29 ++++++++++++++++++++++++++---
 kernel/byterun/coq_values.h |  1 +
 2 files changed, 27 insertions(+), 3 deletions(-)

(limited to 'kernel/byterun')

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_ */
 
 
-- 
cgit v1.2.3