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

This second version accommodates rules with just one clause on the RHS, such
as the one in the "easy" file that says:
Likes[x, ComputerScience] IF Knows[x, Programming]

We use a simple class called Rule with a head and a premises part.For
this program the premises is just one FOLexp.  Later it will become a list
of subgoals that must be consistently satisfied.

We assume all queries are single facts, and since rules only have one premise
there will only be one goal at a time in this version.

As for the Fdict introduced in version BC1, the keys in 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 = [FOLexp(body)] #make this a list for later

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 ######

def FOLBC(goals, thetalist):
    #goals[0] is the FOLexp we want to prove
    #thetalist will be a list of substitutions
    if goals == []: return thetalist  #setting up for a list of goals later
    aGoal = goals[0]   # simplified for version 2
    if not aGoal.isCompound():  #check that the goal is well formed
        print "Error in goal: " , aGoal
        return
    return FOLBC1(aGoal, thetalist)  #try to prove it and return result
        
def FOLBC1(aGoal, thetalist):
    if Fdict.has_key(aGoal.op):
        for clause in Fdict[aGoal.op]:
            theta = unify(clause, aGoal)
            if theta != False: thetalist.append(theta)
    if Rdict.has_key(aGoal.op):
        for r in Rdict[aGoal.op]:
            theta = unify(r.head, aGoal)
            if theta != False:
                # here is where we do our first chaining
                # must apply theta to the LHS before chaining
                thetalist = FOLBC1(subst(theta, r.body[0]), thetalist)
    return thetalist
   

###################   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])