Changed proof output of initial clauses from "input" to more concrete file/name convention.

Author: schulzs

clauses.py

@@ -274,7 +274,7 @@ def parseClause(lexer):
     lexer.AcceptTok(Token.FullStop)
 
     res = Clause(lits, type, name)
-    res.setDerivation(Derivation("input"))
+    res.setInputDeriv(lexer.getName(), name)
     return res
 
 

derivations.py

@@ -79,8 +79,17 @@ def setName(self, name = None):
             Derivable.derivedIdCounter=Derivable.derivedIdCounter+1
 
     def setDerivation(self, derivation):
+        """
+        Set the derivation that created this derivable.
+        """
         self.derivation = derivation
 
+    def setInputDeriv(self, filename, name):
+        """
+        Special case: It's an input object.
+        """
+        self.derivation = Derivation("file('%s', %s)"%(filename,name))
+
     def getParents(self):
         """
         Return a list of all ancestors of this node in the derivation
@@ -176,8 +185,8 @@ def __repr__(self):
         """
         Return a string for the derivation in TPTP-3 format.
         """
-        if self.operator == "input":
-            return "input"
+        if self.operator.startswith("file("):
+            return self.operator
         elif self.operator == "eq_axiom":
             return "eq_axiom"
         elif self.operator == "reference":
@@ -194,7 +203,7 @@ def getParents(self):
         Return a list of all derived objects that are used in this
         derivation.
         """
-        if self.operator == "input":
+        if self.operator.startswith("file("):
             return []
         elif self.operator == "eq_axiom":
             return []

fofspec.py

@@ -60,15 +60,15 @@ def tptpLexer(source, refdir):
     name = os.path.join(refdir, source)
     try:
         fp = open(name, "r")
-        lex = Lexer(fp.read())
+        lex = Lexer(fp.read(), name)
         fp.close()
         refdir = os.path.dirname(name)
     except IOError:
         tptp = os.getenv("TPTP")
         if tptp:
             name = os.path.join(tptp, source)
             fp = open(name, "r")
-            lex = Lexer(fp.read())
+            lex = Lexer(fp.read()), name
             fp.close()
             refdir = os.path.dirname(name)
         else:

formulas.py

@@ -490,7 +490,7 @@ def parseWFormula(lexer):
     lexer.AcceptTok(Token.FullStop)
 
     res = WFormula(form, type, name)
-    res.setDerivation(Derivation("input"))
+    res.setInputDeriv(lexer.getName(), name)
 
     return res
 

lexer.py

@@ -113,6 +113,7 @@ class Token(object):
     Or             = Ident("|")
     And            = Ident("&")
     Implies        = Ident("=>")
+    AltImplies     = Ident("->")
     BImplies       = Ident("<=")
     Equiv          = Ident("<=>")
     Xor            = Ident("<~>")
@@ -163,6 +164,7 @@ class Lexer(object):
         (re.compile("\|"),                    Token.Or),
         (re.compile("&"),                     Token.And),
         (re.compile("=>"),                    Token.Implies),
+        (re.compile("->"),                    Token.Implies),
         (re.compile("<=>"),                   Token.Equiv),
         (re.compile("<="),                    Token.BImplies),
         (re.compile("<~>"),                   Token.Xor),
@@ -192,6 +194,9 @@ def __init__(self, source, name="user string"):
         self.pos = 0
         self.name = name
 
+    def getName(self):
+        return self.name
+        
     def Push(self, token):
         """
         Return a token to the token stack. This allows basically

unification.py

@@ -212,6 +212,10 @@ def mgu(t1, t2):
     Try to unify t1 and t2, return substitution on success, or None on failure.
     """
     res =  mguTermList([t1], [t2], Substitution())
+    res2 = "False"
+    if res:
+       res2 = "True"
+    # print("# :", term2String(t1), " : ", term2String(t2), " => ", res2);
     return res