From 178c20a61cca77935631901fd1d0e694aa834112 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Fri, 19 Oct 2018 20:27:35 -0400
Subject: [PATCH] Refactoring code.

---
 src/arachne.c | 107 ++++++++++++++++++++++++++++++++------------------
 1 file changed, 68 insertions(+), 39 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index e36050a..5307267 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -1375,6 +1375,23 @@ bind_goal_new_intruder_run (const Binding b)
   return flag;
 }
 
+//! Debug information?
+void
+debug_send_candidate (const Protocol p, const Role r, const Roledef rd,
+		      const int index)
+{
+#ifdef DEBUG
+  indentPrint ();
+  eprintf ("Checking send candidate with message ");
+  termPrint (rd->message);
+  eprintf (" from ");
+  termPrint (p->nameterm);
+  eprintf (", ");
+  termPrint (r->nameterm);
+  eprintf (", index %i\n", index);
+#endif
+}
+
 //! Dummy helper function for iterator; abort if sub-unification found
 int
 test_sub_unification (Termlist substlist, Termlist keylist)
@@ -1383,6 +1400,50 @@ test_sub_unification (Termlist substlist, Termlist keylist)
   return false;
 }
 
+//! Proof output for first match
+void
+proof_term_match_first (const int found, const Binding b)
+{
+  if (switches.output == PROOF && found == 1)
+    {
+      indentPrint ();
+      eprintf ("The term ", found);
+      termPrint (b->term);
+      eprintf (" matches patterns from the role definitions. Investigate.\n");
+    }
+}
+
+//! Proof output for any match
+void
+proof_term_match (const Protocol p, const Role r, const Roledef rd,
+		  const int index, const int found)
+{
+  if (switches.output == PROOF)
+    {
+      indentPrint ();
+      eprintf ("%i. It matches the pattern ", found);
+      termPrint (rd->message);
+      eprintf (" from ");
+      termPrint (p->nameterm);
+      eprintf (", ");
+      termPrint (r->nameterm);
+      eprintf (", at %i\n", index);
+    }
+}
+
+//! Proof output for no match
+void
+proof_term_match_none (const Binding b, const int found)
+{
+  if (switches.output == PROOF && found == 0)
+    {
+      indentPrint ();
+      eprintf ("The term ");
+      termPrint (b->term);
+      eprintf (" does not match any pattern from the role definitions.\n");
+    }
+}
+
 //! Bind a regular goal
 /**
  * Problem child. Valgrind does not like it.
@@ -1405,19 +1466,8 @@ bind_goal_regular_run (const Binding b)
       }
 
     // Test for interm unification
-#ifdef DEBUG
-    if (DEBUGL (5))
-      {
-	indentPrint ();
-	eprintf ("Checking send candidate with message ");
-	termPrint (rd->message);
-	eprintf (" from ");
-	termPrint (p->nameterm);
-	eprintf (", ");
-	termPrint (r->nameterm);
-	eprintf (", index %i\n", index);
-      }
-#endif
+    debug_send_candidate (p, r, rd, index);
+
     if (!subtermUnify
 	(rd->message, b->term, NULL, NULL, test_sub_unification))
       {
@@ -1425,25 +1475,9 @@ bind_goal_regular_run (const Binding b)
 
 	// A good candidate
 	found++;
-	if (switches.output == PROOF && found == 1)
-	  {
-	    indentPrint ();
-	    eprintf ("The term ", found);
-	    termPrint (b->term);
-	    eprintf
-	      (" matches patterns from the role definitions. Investigate.\n");
-	  }
-	if (switches.output == PROOF)
-	  {
-	    indentPrint ();
-	    eprintf ("%i. It matches the pattern ", found);
-	    termPrint (rd->message);
-	    eprintf (" from ");
-	    termPrint (p->nameterm);
-	    eprintf (", ");
-	    termPrint (r->nameterm);
-	    eprintf (", at %i\n", index);
-	  }
+	proof_term_match_first (found, b);
+	proof_term_match (p, r, rd, index, found);
+
 	indentDepth++;
 
 	// Bind to existing run
@@ -1474,13 +1508,8 @@ bind_goal_regular_run (const Binding b)
   // Bind to all possible sends of regular runs
   found = 0;
   flag = iterate_role_sends (bind_this_role_send);
-  if (switches.output == PROOF && found == 0)
-    {
-      indentPrint ();
-      eprintf ("The term ");
-      termPrint (b->term);
-      eprintf (" does not match any pattern from the role definitions.\n");
-    }
+
+  proof_term_match_none (b, found);
   return flag;
 }