'''
BC3.py -- Third of several incremental implementation of backward
chaining to illustrate incremental development of AI software
in CS4100, Artificial Intelligence.

This third version accommodates rules with more than one clause on the RHS, such
as the one in the "average" file that says:
Teenager[p] IF Younger[p, Twenty] AND Older[p, Twelve]

We use a simple class called Rule with a head and a premises part. Now
the body part of the rules, which is a list of subgoals that must be
consistently satisfied, may have more than one member.

Although top level queries are still just one clause, we now have to deal
with lists of subgoals in recursive calls to backward chaining.  This is
one of main complications of the algorithm.

As before, the keys in the Fdict and the Rdict represent
the operator (i.e., the main predicate) of the "head" (the RHS or conclusion)

'''

from unify import *

Fdict = {}  #Here we will store the knowledge base facts
Rdict = {}  # Here we will store the KB rules
AllThetas = [] #Here we will put all the solutions

class Rule:
    def __init__(self, head, body):
        # head and body are each a FOLexp
        # replaceVars method returns a copy of self
        # with variables replaced
        self.head = FOLexp(head)
        self.body = []
        # PREVIOUSLY self.body = [FOLexp(body)]
        for premise in body.split("AND"): 
            self.body.append(FOLexp(premise) #this could be more elegant
        
def standarize(rule):
    # returns a copy of the rule with variables consistently replaced
    return False #stub
          
def acquireKB(KBname):
    kbfile = open(KBname)
    for aline in kbfile.readlines():
        if aline.strip() == '': continue  #skip any blank lines
        if aline.find("IF") > 0:
            r = aline.split("IF")
            addRuleToRDict(Rule(r[0],r[1]))
        else:
            addClauseToFDict(FOLexp(aline))

def addClauseToFDict(clause):
    #Adds a FOL sentence represented as a FOLexp to the KB dictionary
    if Fdict.has_key(clause.op):
        Fdict[clause.op] += [clause]   #append it to entry
    else:
        Fdict[clause.op] = [clause]    # make a new entry

def addRuleToRDict(rule):
    if Rdict.has_key(rule.head.op):
        Rdict[rule.head.op] += [rule]   #append rule to entry
    else:
        Rdict[rule.head.op] = [rule]    # make a new entry

def FOLBCtest(QFname):
    global queryVars ## necessary in Python so other functions can see it
    global AllThetas
    queryfile = open(QFname)
    for aline in queryfile.readlines():
        print 'Query: ' , aline[:-1]
        query = FOLexp(aline)
        queryVars = getVarsInExp(query, [])
        AllThetas = FOLBC([query], [])
        if len(queryVars) == 0: showTFResults(AllThetas)
        else: showMatchResults(AllThetas)
        
def getVarsInExp(fexp, result):
    if fexp.isVar():
        if fexp.name not in result: result.append(fexp.name)
    elif fexp.isCompound():
        for fe in fexp.args:
            result = getVarsInExp(fe, result)
    return result          

################## End of framework. Here begins the true BC ALGORITHM ######
'''
We need a new version for multi-premise rules
def FOLBC(goals, thetalist):
    #goals is the list of FOLexp we want to prove
    #thetalist will be a list of substitutions
    if goals == []: return thetalist
    for aGoal in goals:  #must prove them all consistently using subst !!!
        if not aGoal.isCompound():  #check that the goal is well formed
            print "Error in goal: " , aGoal
            return
        for theta in thetalist:  #we have to try extending each prior match
            theta = FOLBC1(subst(theta, aGoal))
            if theta == False: return False
        
'''
###################   UTILITY/HELPER FUNCTIONS ###################            

def showTFResults(thetalist):
    if len(thetalist) > 0:
        print ">>> ANSWER: True!!"
    else:
        print ">>> ANSWER: False!!"

def showMatchResults(thetalist):
    if len(thetalist) > 1:
        # Display the number of answers and each one
        print ">>> " , len(thetalist) , " answers found."
        i = 1
        for theta in thetalist:
            print ">>> ANSWER " , i
            printTheta(theta)
            i += 1
    else:
        print ">>> ANSWER: "
        printTheta(thetalist[0])