From 1678577ce00716feb8e6baf8d5279f4259f4af01 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Sun, 5 Mar 2006 15:18:39 +0000
Subject: [PATCH] - Improved proof reports. - Minor (epsilon type) efficiency
 improvement.

---
 src/arachne.c | 23 +++++++++++++++++++++--
 src/binding.c | 17 +++++++++++++++--
 src/term.c    | 14 +++++++-------
 3 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 038557b..32b4270 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -87,6 +87,7 @@ arachneInit (const System mysys)
   {
     rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL);
   }
+
   Role add_role (const char *rolenamestring)
   {
     Role r;
@@ -886,7 +887,10 @@ createDecryptionChain (const Binding b, const int run, const int index,
 	    if (switches.output == PROOF)
 	      {
 		indentPrint ();
-		eprintf ("Bound: trying new createDecryptionChain.\n");
+		eprintf ("Bound ");
+		termPrint (b->term);
+		eprintf (" to r%ii%i: trying new createDecryptionChain.\n",
+			 smallrun, 2);
 	      }
 
 	    // Iterate with the new goal
@@ -940,6 +944,19 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
       {
 	if (sl == NULL)
 	  {
+	    if (switches.output == PROOF)
+	      {
+		Roledef rd;
+
+		indentPrint ();
+		eprintf ("Suppose ");
+		termPrint (b->term);
+		eprintf (" originates first at run %i, event %i, as part of ",
+			 run, index);
+		rd = roledef_shift (sys->runs[run].start, index);
+		termPrint (rd->message);
+		eprintf ("\n");
+	      }
 	    // new create key goals, bind etc.
 	    createDecryptionChain (b, run, index, keylist, iterate);
 	  }
@@ -960,12 +977,14 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	      if (!realTermVariable (tsubst))
 		{
 		  // Only for non-variables (i.e. local constants)
-		  int r1, e1, r2, e2;
+		  int r1, e1;
 
 		  r1 = TermRunid (tsubst);
 		  e1 = firstOccurrence (sys, r1, tsubst, SEND);
 		  if (e1 >= 0)
 		    {
+		      int r2, e2;
+
 		      r2 = TermRunid (tvar);
 		      e2 = firstOccurrence (sys, r2, tsubst, READ);
 		      if (e2 >= 0)
diff --git a/src/binding.c b/src/binding.c
index 409515d..96fa42f 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -141,6 +141,12 @@ goal_bind (const Binding b, const int run, const int ev)
       if (dependPushEvent (run, ev, b->run_to, b->ev_to))
 	{
 	  b->done = true;
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      binding_print (b);
+	      eprintf ("\n");
+	    }
 	  return true;
 	}
     }
@@ -350,7 +356,7 @@ labels_ordered (Termmap runs, Termlist labels)
 int
 valid_binding (Binding b)
 {
-  if (b->done && !b->blocked)
+  if (b->done && (!b->blocked))
     return true;
   else
     return false;
@@ -458,7 +464,6 @@ bindings_c_minimal ()
 	if (valid_binding (b))
 	  {
 	    int run;
-	    int node_from;
 
 	    // Find all preceding events
 	    for (run = 0; run < sys->maxruns; run++)
@@ -494,6 +499,14 @@ bindings_c_minimal ()
 			    return false;
 			  }
 		      }
+		    else
+		      {
+			// If this event is not before the target, then the
+			// next in the run certainly is not either (because
+			// that would imply that this one is before it)
+			// Thus, we effectively exit the loop.
+			break;
+		      }
 		  }
 	      }
 	  }
diff --git a/src/term.c b/src/term.c
index 26779fc..ba2c317 100644
--- a/src/term.c
+++ b/src/term.c
@@ -249,25 +249,25 @@ termSubTerm (Term t, Term tsub)
 
   if (isTermEqual (t, tsub))
     {
-      return 1;
+      return true;
     }
   else
     {
       if (t == NULL)
 	{
-	  return 0;
+	  return false;
 	}
       else
 	{
 	  if (tsub == NULL)
 	    {
-	      return 1;
+	      return true;
 	    }
 	  else
 	    {
 	      if (realTermLeaf (t))
 		{
-		  return 0;
+		  return false;
 		}
 	      else
 		{
@@ -296,13 +296,13 @@ termInTerm (Term t, Term tsub)
   tsub = deVar (tsub);
 
   if (isTermEqual (t, tsub))
-    return 1;
+    return true;
   if (realTermLeaf (t))
-    return 0;
+    return false;
   if (realTermTuple (t))
     return (termInTerm (TermOp1 (t), tsub) || termInTerm (TermOp2 (t), tsub));
   else
-    return 0;
+    return false;
 }
 
 //! Print a term to stdout.