From 2107d76532abbf325179bd2d6efbcdbd1060a246 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Tue, 18 Sep 2007 15:36:11 +0200
Subject: [PATCH] Proof output improved for occurrences of the Athena problem.

---
 src/arachne.c | 12 +++++++++++-
 src/arachne.h |  2 +-
 src/mgu.c     | 12 ++++++------
 3 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index ee155cf..944eea0 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -2703,7 +2703,17 @@ isTriviallyKnownAfterArachne (const System sys, const Term t, const int run,
  * Currently used in mgusubterm in mgu.c
  */
 void
-markNoFullProof ()
+markNoFullProof (const Term tbig, const Term tsmall)
 {
+  // Comment in proof
+  if (switches.output == PROOF)
+    {
+      indentPrint ();
+      eprintf ("Note: the pattern set will be incomplete, because ");
+      termPrint (tbig);
+      eprintf (" allows for infinitely many ways to subtermUnify ");
+      termPrint (tsmall);
+      eprintf (".\n");
+    }
   sys->current_claim->complete = false;
 }
diff --git a/src/arachne.h b/src/arachne.h
index 95b1abb..e0959ea 100644
--- a/src/arachne.h
+++ b/src/arachne.h
@@ -35,6 +35,6 @@ void arachneOutputAttack ();
 void printSemiState ();
 int countIntruderActions ();
 void role_name_print (const int run);
-void markNoFullProof ();
+void markNoFullProof (const Term tbig, const Term tsmall);
 
 #endif
diff --git a/src/mgu.c b/src/mgu.c
index ef4a907..bd506c7 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -328,12 +328,12 @@ subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
       if (isOpenVariable (tbig))
 	{
 	  // This one needs to be pursued by further constraint adding
-		    /**
-		     * Currently, this is not implemented yet. TODO.
-		     * This is actually the main Athena problem that we haven't solved yet.
-		     */
-	  // Mark that we don't have a full proof.
-	  markNoFullProof ();
+	  /**
+	   * Currently, this is not implemented yet. TODO.
+	   * This is actually the main Athena problem that we haven't solved yet.
+	   */
+	  // Mark that we don't have a full proof, and possibly remark in proof output.
+	  markNoFullProof (tbig, tsmall);
 	}
     }