From 021f94d7dfef5630e48e79c9238db3a24b2aa221 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 23 Dec 2016 09:28:47 +0100
Subject: Handle application of a primitive projection to a not yet evaluated
 cofixpoint (bug #5286).

---
 kernel/byterun/coq_interp.c | 63 ++++++++++++++++++++++++++++++++++-----------
 1 file changed, 48 insertions(+), 15 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 5dec3b785c..af89712d5e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -891,25 +891,58 @@ value coq_interprete
 
 
       Instruct(PROJ){
+        do_proj:
 	print_instr("PROJ");
 	if (Is_accu (accu)) {
-          value block;
-	  /* Skip over the index of projected field */
-	  pc++;
-	  /* Create atom */
-	  Alloc_small(block, 2, ATOM_PROJ_TAG);
-	  Field(block, 0) = Field(coq_global_data, *pc);
-	  Field(block, 1) = accu;
-          accu = block;
-          /* Create accumulator */
-          Alloc_small(block, 2, Accu_tag);
-          Code_val(block) = accumulate;
-          Field(block, 1) = accu;
-          accu = block;
+          *--sp = accu; // Save matched block on stack
+          accu = Field(accu, 1); // Save atom to accu register
+          switch (Tag_val(accu)) {
+          case ATOM_COFIX_TAG: // We are forcing a cofix
+            {
+              mlsize_t i, nargs;
+              sp -= 2;
+              // Push the current instruction as the return address
+              sp[0] = (value)(pc - 1);
+              sp[1] = coq_env;
+              coq_env = Field(accu, 0); // Pointer to suspension
+              accu = sp[2]; // Save accumulator to accu register
+              sp[2] = Val_long(coq_extra_args); // Push number of args for return
+              nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+              // Push arguments to stack
+              CHECK_STACK(nargs + 1);
+              sp -= nargs;
+              for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+              *--sp = accu; // Last argument is the pointer to the suspension
+              coq_extra_args = nargs;
+              pc = Code_val(coq_env); // Trigger evaluation
+              goto check_stack;
+            }
+          case ATOM_COFIXEVALUATED_TAG:
+            {
+              accu = Field(accu, 1);
+              ++sp;
+              goto do_proj;
+            }
+          default:
+            {
+              value block;
+              /* Skip over the index of projected field */
+              ++pc;
+              /* Create atom */
+              Alloc_small(accu, 2, ATOM_PROJ_TAG);
+              Field(accu, 0) = Field(coq_global_data, *pc++);
+              Field(accu, 1) = *sp++;
+              /* Create accumulator */
+              Alloc_small(block, 2, Accu_tag);
+              Code_val(block) = accumulate;
+              Field(block, 1) = accu;
+              accu = block;
+            }
+          }
 	} else {
-	    accu = Field(accu, *pc++);
+          accu = Field(accu, *pc);
+          pc += 2;
 	}
-	pc++;
 	Next;
       }
 
-- 
cgit v1.2.3


From 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Jan 2017 11:23:48 +0100
Subject: Mapping named_context_val preserves sharing when possible.

This was deactivated by 27c9346 and made an optimization moot in eauto. This
optimization was physically checking for equality, but as lists where rebuilt
by the mapping, this was never true. Some contribs were thus quite slower,
including persistent-union-find which was twice slower.

This 2-line patch fixes it by trying to preserve sharing as much as possible.
Note that we should still do something about eauto, because it does redo
useless work a lot whenever the environment only changes a bit, while we could
cache this computation.
---
 kernel/pre_env.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 7be8606ef4..f211583e06 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -156,7 +156,8 @@ let map_named_val f ctxt =
     (accu, d')
   in
   let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
-  { env_named_ctx = ctx; env_named_map = map }
+  if map == ctxt.env_named_map then ctxt
+  else { env_named_ctx = ctx; env_named_map = map }
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
-- 
cgit v1.2.3