#!/usr/bin/python
""" $Id: proofcheck.py,v 1.4 2001/01/28 07:13:14 connolly Exp $

This is a translation of McCune's proof checker into python

ftp://info.mcs.anl.gov/pub/Otter/QED/check-4.tar.gz
md5 sum: 57df012a4aab3661f700902e79830ca8  check-4.tar.gz
Apr  3  1995
108326 bytes

http://www-unix.mcs.anl.gov/~mccune/papers/robbins/
http://lists.w3.org/Archives/Public/sw99/2000JanMar/0002.html

For now, I'm using lisp syntax (in particular, for
the tests, KIF syntax). But I intend to try
out Drew McDermott's RDF-ish syntax
cf
A modest proposal for reforming RDF Drew McDermott (Wed, Dec 13 2000) 
http://lists.w3.org/Archives/Public/www-rdf-logic/2000Dec/0044.html

translation notes:
  foo-bar      ==> fooBar
"""

from string import atoi

import KIFSyntax
KS = KIFSyntax

t = intern('t')
f = None
nil = ()
equalSym = intern('=') #McCune: what's going on here? in some parts of the proof checker, it says equal; in others, eq; in the proof object, it's '='.
notSym = intern('not')

inputSym = intern('input')
resolveSym = intern('resolve')
mergeSym = intern('merge')
instantiateSym = intern('instantiate')
paramodSym = intern('paramod')
flipSym = intern('flip')

def toSym(s):
    if s == 't': return t
    elif s == 'f': return f
    elif s == '0': return 0
    elif s == 'nil': return nil
    else:
	try:
	    return atoi(s)
	except ValueError:
	    return intern(s)

#HACK: list end object kept at 0th item in tuple.
def list_(*args):
    return ((),) + tuple(args)
def listp(x):
    return type(x) is type((1,))
def nlistp(c):
    return c is nil or type(c) is not type((1,))
def car(c):
    assert len(c)>=2
    return c[1]

def cdr(c):
    if c[0] is ():
	if len(c)>2: return ((),) + c[2:]
	else: return ()
    else: return c[0]
def cons(x, y):
    if type(y) is type((1,)): return ((), x) + y[1:]
    else: return (y, x)
def cadr(l):
    return l[2]
def caar(l):
    return l[1][1]
def caddr(l):
    return l[3]
def member(i, c):
    return i in c[1:]

def assoc(k, l):
    for i in l[1:]:
	if k == car(i):
	    return i
    return nil

def append(l1, l2):
    assert l1[0] is () and l2[0] is ()
    return ((),) + l1[1:] + l2[1:]

def map_(thunk, l):
    assert l[0] is ()
    return ((),) + tuple(map(thunk, l[1:]))

def toString(e):
    if type(e) is type((1,)):
	ret = '('
	if e is ():
	    pass
	elif e[0] is ():
	    for i in e[1:]:
		ret = ret + toString(i) + ' '
	else:
	    ret = ret + toString(e[1]) + ' . ' + toString(e[0]) + ' '
	ret = ret + ')'
	return ret
    else: return str(e)
    
### McCune's code starts here

def ithMember (c, i):
    #print i, "th member of ", toString(c), "is", toString(c[i])
    return c[i]

def removeIthMember(c, i):
    return c[:i] + c[i+1:]

def subset (x, y):
    for carx in x[1:]:
	if not member(carx, y): return f
    return t

def length (x):
    if x is nil: return 0
    else: return len(x)-1

def testListUtils():
    import KIFSyntax
    K = KIFSyntax
    l = KS.quoterm("(=> (and (?p ?x ?y) (?p ?y ?z)) (?p ?x ?z))",
		  symNamed=toSym)
    l2 = KS.quoterm("(=> (and (?p ?x ?y) (?p ?y ?z)) (?p ?x ?z) abc)",
		   symNamed=toSym)
    print "l :", l
    print "l2:", l2
    print "0th member should be", l[0], ":", ithMember(l, 0)
    print "remove 2nd gives:", removeIthMember(l, 1)
    print "l subset l2?", subset(l, l2)
    print "l2 subset l?", subset(l2, l)
    print "length:", length(l)

    al = KS.quoterm("((bannana yellow) (orange orange) (grape blue))")
    k = KS.quoterm("grape")
    print "assoc test", assoc(k, al)

########
#
# Proof steps have the form (id justification clause).
# ...

def wfSym (s):
    """hmm... shouldn't this exclude not and equal as well?"""
    return (nlistp (s)
	    and s <> t
	    and s <> f
	    and s <> nil
	    and s <> 0
	    )

wfPredSym = wfSym

wfFuncSym = wfSym

wfVarSym = wfSym

def wfTermList(l):
    if nlistp(l): return f
    for cl in l[1:]:
	if nlistp(cl):
	    if not wfVarSym(cl): return f
	else:
	    if not (wfFuncSym(car(cl))
		    and wfTermList(cdr(cl))): return f
    return t

def wfTerm (x):
    return wfTermList (list_(x))

def wfEqAtom (a):
    return (length(a) == 3
	    and car(a) == equalSym
	    and wfTermList(cdr(a))
	    )

def wfAtom (a):
    return (wfEqAtom(a)
	    or (listp(a)
		and wfPredSym (car(a))
		and wfTermList (cdr(a))
		)
	    )

def wfLiteral (lit):
    if not listp(lit): return f
    if car(lit) is notSym:
	return (length(lit) == 2
		and wfAtom(cadr(lit))
		)
    else:
	return wfAtom(lit)

def wfClause (c):
    for carc in c[1:]:
	if not wfLiteral (carc): return f
    return t

def wfSubst (subst):
    for carsubst in subst[1:]:
	if not (listp(carsubst)
		and wfVarSym (car(carsubst))
		and wfTerm (cdr(carsubst)) ): return f
    return t

def wfJustification (just):
    if nlistp(just):
	return f

    carJust = car(just)

    if carJust is inputSym:
	return length(just) == 1
    elif carJust == resolveSym:
	return length(just) == 5
    elif carJust is mergeSym:
	return length(just) == 3
    elif carJust is instantiateSym:
	return (length(just) == 3
		and wfSubst(caddr(just)) ) #BUG! in McCune's code; it says cadr here, but the thing below (defn substitution (step) (caddadr step)) makes it clear it should be caddr
    elif carJust is paramodSym:
	return length(just) == 5
    elif carJust is flipSym:
	return length(just) == 3
    else:
	return f
        
def wfStep (st):
    if length(st) <> 3:
	ret =  f
    else: ret = (nlistp (car(st))
		 and wfClause (caddr(st))
		 and wfJustification (cadr(st)) )
    if not ret: print "@@bad step:", st, nlistp(car(st)), wfClause(caddr(st)), wfJustification(cadr(st))
    return ret

def wfProof (p):
    for carp in p[1:]:
	if not wfStep (carp): return f
    return t

def wfProofVerbose (p):
    return map_(lambda(carp): cons(car(carp), wfStep(carp)), p)


def testWfStuff():
    import KIFSyntax
    K = KIFSyntax

    for case, res in (('(x y z)', 0),
		      ('t', 0),
		      ('f', 0),
		      ('()', 0),
		      ('0', 0),
		      ('a', 1),
		      ('b', 1),
		      ('c31', 1)):
	print "wfSym case", case,
	l = KS.quoterm(case, symNamed=toSym)
	ans = wfSym(l)
	if ans == res:
	    print "OK:", ans
	else: print "FAIL!", ans

    for case, res in (('(x y z)', 1),
		      ('t', 0),
		      ('f', 0),
		      ('()', 0),
		      ('0', 0),
		      ('a', 1),
		      ('(b c (d e ff))', 1),
		      ('c31', 1)):
	print "wfTerm case", case,
	l = KS.quoterm(case, symNamed=toSym)
	print "quoterm", l
	ans = wfTerm(l)
	if ((ans and res) or (not ans and not res)):
	    print "OK: ", ans
	else: print "FAIL! ", ans

    for case, res in (('(x y z)', 1),
		      ('t', 0),
		      ('f', 0),
		      ('()', 0),
		      ('0', 0),
		      ('a', 1),
		      ('(b c (d e ff))', 1),
		      ('c31', 1),
		      ('(equal a b)', 1),
		      ('(equal (ff x) (g x))', 1),
		      ('(equal (equal ff x) (g x))', 0),
		      ('(not (equal (ff x) y))', 1),
		      ):
	print "wfLiteral case", case,
	l = KS.quoterm(case, symNamed=toSym)
	print "quoterm", l
	ans = wfTerm(l)
	if ((ans and res) or (not ans and not res)):
	    print "OK: ", ans
	else: print "FAIL! ", ans

    print "@@more unit tests"

# Here are routines to get stuff out of proof steps.  Note that "rule"
# and "clause" apply to all types of step, but the others don't.

def rule         (step): return step[2][1]
def clause       (step): return step[3]
def par1Id       (step): return step[2][2]
def pos1         (step): return step[2][3]
def par2Id       (step): return step[2][4]
def pos2         (step): return step[2][5]
def substitution (step): return step[2][3]

# Just check that the steps are sound; don't check if there are extra
# literals in the results.
#
# ------------------------------------------------ resolution

def complementary (p, q):
    return ((car(p) is notSym and cadr(p) == q) or
	    ((car(q) == notSym) and (cadr(q) == p)) )

def checkResolve2 (parent1, pos1, parent2, pos2, resolvent):
    return (complementary(ithMember(parent1, car(pos1)),
			  ithMember(parent2, car(pos2)))
	    and subset(removeIthMember(parent1, car(pos1)), resolvent)
	    and subset(removeIthMember(parent2, car(pos2)), resolvent))


def checkResolve (step, checked):
    return checkResolve2(clause(assoc(par1Id(step), checked)), pos1(step),
			 clause(assoc(par2Id(step), checked)), pos2(step),
			 clause(step) )

# ------------------------------------------------ merge
# The position doesn't make it any easier to check.

def checkMerge2 (parent, position, result):
    return subset(parent, result)

def checkMerge (step, checked):
    return checkMerge2(clause(assoc(par1Id(step), checked)), pos1(step),
		       clause(step) )

# ------------------------------------------------ instantiation

def applyList (x, subst):  # x is a list of terms.
    print "@@applyList", toString(x), "subst:", toString(subst)
    def applyElt(carx, subst=subst):
	if nlistp(carx):
	    item = assoc(carx, subst)
	    if item: return cdr(item)
	    else: return carx
	else: return cons(car(carx), applyList(cdr(carx), subst))
    ret = map_(applyElt, x)
    print "@@applyList done:", toString(ret)
    return ret

def checkInstance2 (parent, subst, result):
    res = applyList(parent, subst)
    print "@@checkInstance", res==result, "::", toString(res), "=?=", toString(result)
    print "@@parent was", toString(parent)
    return res == result

def checkInstance (step, checked):
    return checkInstance2(clause(assoc(par1Id(step), checked)), substitution(step),
			  clause(step))


# ------------------------------------------------ paramodulation

def subtermAtPos (x, pos):  # x is a list of terms.
    assert listp(x), toString(x)
    item = ithMember(x, car(pos))
    if nlistp(cdr(pos)):
	return item
    else:
	return subtermAtPos(cdr(item), cdr(pos))

def replaceAtPos (x, pos, replacement):  # x is a list of terms.
    #print "replaceAtPos:", toString(x), "at", toString(pos), "by", toString(replacement)
    assert listp(x), toString(x)
    p = car(pos)
    if nlistp(cdr(pos)):
	return x[:p] + (replacement,) + x[p+1:] # PEEKING!
    else:
	return x[:p] + (cons(car(x[p]), replaceAtPos(cdr(x[p]), cdr(pos), replacement)),) + x[p+1:]

def beta (clause, pos):  # replacement term
    bpos = list_(car(pos), (cadr(pos) == 1 and 2 or 1))
    t = subtermAtPos(clause, bpos)
    return t

def checkParamod2 (fromCl, fromPos, intoCl, intoPos, para):
    print "@@checkParamod2: fromCl:", toString(fromCl), \
	  "fromPos:", toString(fromPos), \
	  "intoCl:", toString(intoCl), \
	  "intoPos:", toString(intoPos), \
	  "para:", toString(para)
    return (wfEqAtom(ithMember(fromCl, car(fromPos)))
	    and (subtermAtPos(intoCl, intoPos) ==
		 subtermAtPos(fromCl, fromPos) )
	    and member(cons(car(ithMember(intoCl, car(intoPos))),
			    replaceAtPos(cdr(ithMember(intoCl, car(intoPos))),
					 cdr(intoPos),
					 beta(fromCl, fromPos) ) ),
		       para)
	    and subset(removeIthMember(fromCl, car(fromPos)), para)
	    and subset(removeIthMember(intoCl, car(intoPos)), para) )

def checkParamod (step, checked):
    return checkParamod2(clause(assoc(par1Id(step), checked)),
			 pos1(step),
			 clause(assoc(par2Id(step), checked)),
			 pos2(step),
			 clause(step) )

untranslatedRest="""
; ------------------------------------------------ flip

(defn check-flip-2 (parent pos eq-lit result)
  (and (if (equal (car eq-lit) 'not)
           (and (wf-eq-atom (cadr eq-lit))
                (member (list 'not (list (caadr eq-lit)
                                         (caddadr eq-lit)
                                         (cadadr eq-lit))) result))
           (and (wf-eq-atom eq-lit)
                (member (list (car eq-lit)
                              (caddr eq-lit)
                              (cadr eq-lit)) result)))
       (subset (remove-ith-member parent (car pos)) result)))
           
(defn check-flip (step checked)
  (check-flip-2 (clause (assoc (par1-id step) checked))
                (pos1 step)
                (ith-member (clause (assoc (par1-id step) checked))
                            (car (pos1 step)))
                (clause step)))
"""
# ------------------------------------------------ 

def checkStep (step, checked):
    if not wfStep(step): return f
    r = rule(step)
    print "@@checking: rule", r, "in", toString(step)
    if   r is inputSym:       return t
    elif r is resolveSym:     return checkResolve(step, checked)
    elif r is mergeSym:       return checkMerge(step, checked)
    elif r is instantiateSym: return checkInstance(step, checked)
    elif r is paramodSym:     return checkParamod(step, checked)
    elif r is flipSym:        return checkFlip(step, checked)
    else: return f

# ------------------------------------------------ 
#
# The proof is partitioned into CHECKED and NOT-CHECKED; the
# CHECKed part happens to get constructed backwards.
#
# This version returns the result for each step.

def checkProofVerbose (notChecked, checked):
    if nlistp(notChecked):
	return nil
    else:
	return cons(cons(caar(notChecked), checkStep(car(notChecked), checked)),
		    checkProofVerbose(cdr(notChecked),
				      cons(car(notChecked), checked) ) )

# This version returns just T or F.

def checkProof (notChecked, checked):
    if nlistp(notChecked):
	return t
    else: return (check-step(car(notChecked), checked)
		  and checkProof(cdr(notChecked),
				 cons(car(notChecked), checked) ) )

# This version returns a list of the bad steps

def checkProofErrors (notChecked):
    i = 0
    res = []
    while i<length(notChecked):
	print "@@cPE:", i, "done; ", length(notChecked) - i, "to go"
	thisStep = notChecked[i+1]
	checked = notChecked[:i+1]
	if checkStep(thisStep, checked): pass # nothing
	else: res.append(car(thisStep))
	i = i + 1
    return ((),) + tuple(res)

# ------------------------------------------------ 
#
# Here are the top-level routines.  Pick one.
#

def check (proof):             # return T or F
    return checkProof(proof, nil)

def checkVerbose (proof):      # return T or F for each step
  checkProofVerbose(proof, nil)

def checkErrors (proof):       # return a list of the bad steps
    return list_(toSym('the-bad-steps-are'),
		 checkProofErrors(proof) )



if __name__ == '__main__':
    import sys

    testListUtils()
    testWfStuff()

    print "reading proof..."
    pf = KS.quoterm(sys.stdin.read(), symNamed=toSym)

    print "checking proof for well-formedness..."
    print wfProofVerbose(pf)

    print "checking proof..."
    print checkErrors(pf)