import UtilsN3, xml, PVa, LoadTree, GenerateDB, UtilsN3, string

class Unify:

   # There are two possibilities for unification: 
   # 1) unification is done on the level of sets of triples.
   # There is the "masterset" and the "slaveset".
   # Each triple of the masterset is matched against
   # each triple of the slaveset till a match is found.
   # No further matches will be tried within the slave tripleset,
   # thus this will not be pushed on the stack.
   # This permits the use of procedures with a case statement:
   # only the first match is executed and thus a sequencing
   # of instructions. 
   # 2) unification is done on a level of triples.
   # Before the unification the module Builtin.py is optionally called.
   # This module will execute actions e.g. :a a owl:list will create a list.
   # A successfull unification without alternatives will then be returned.
   # Math builtins will make a calculation before the unification.
   # The module Types.py will optionally be called when two atoms are unified to 
   # make a type check.

    # a dictionary for fast access to parts of the xml tree
    semDic = {}
    # the semantic tree
    semTree = xml.XmlTree("SemTree")
    # definition of logForAll, logForSome and logImplies
    logForAll = "http://www.w3.org/2000/10/swap/log#forAll"
    logForSome = "http://www.w3.org/2000/10/swap/log#forSome"
    logImplies = "http://www.w3.org/2000/10/swap/log#implies"
    # the database generator
    generate = GenerateDB.GenerateDB()
    # a utils object
    utils = UtilsN3.Utils()

    def __init__(self):
        self.semTree.clearTree()
 
    # definitions for substitutions
    # a substitution is represented by a list of tuples.
    # The null substitution is just an empty list.
    # The first element of the tuple is to be substituted by the second element. 

    # merge two substitutions:
    # this is simply done by adding the  two lists.
    
    # apply a substitution to a tree.
    # Returns a tree.
    def applySubstitution(self, subst, tree):
        if len(subst) == 0:
            return tree
        else:
            applySubst = self.ApplySubstitution()
            applySubst.setSubstitution(subst)
            tree = tree.walkATree(tree, applySubst)
            return tree

    # apply a substitution to a tree.
    # take into account the level of inferencing
    # Returns a tree.
    def applySubstitutionWithLevel(self, subst, tree, level):
        if len(subst) == 0:
            return tree
        else:
            applySubst = self.ApplySubstitutionWithLevel()
            applySubst.setSubstitution(subst)
            applySubst.setLevel(level)
            tree = tree.walkATree(tree, applySubst)
            return tree

    # apply a substitution in reverse to a tree.
    # Returns a tree.
    def applySubstitutionReverse(self, subst, tree):
        if len(subst) == 0:
            return tree
        else:
            applySubst = self.ApplySubstitutionReverse()
            applySubst.setSubstitution(subst)
            tree = tree.walkATree(tree, applySubst)
            return tree
        
    # apply a substitution to a variable.
    def applySubstitutionToVar(self, subst, tree):
        if len(subst) == 0:
            return tree
        else:
            bool = (tree.name == "Var" or tree.name == "EVar" or
                     tree.name == "GVar" or tree.name == "GEVar")
            subst1, subst2 = subst[0]
            if (bool and tree.compareTrees(subst1, tree)):
                return self.applySubstitutionToVar (subst[1:], subst2)
            elif tree.compareTrees(subst1, tree):
                return subst2
            else:
                return self.applySubstitutionToVar (subst[1:], subst2)

    # apply a substitution to a list.
    def applySubstitutionToList(self, subst, treeList):
        if len(treeList) == 0:
            return []
        else:
            return ([self.applySubstitution(subst, treeList[0])] +
                self.applySubstitutionToList(subst, treeList[1:]))

    # apply a substitution list to a tree list.
    def applySubstitutionListToList(self, substList, treeList): 
        if len(substList) == 0:
            return treeList
        else:
            return (self.applySubstitutionListToList(substList[1:]) +
                (self.applySubstitutionToList(substList[0], treeList)))

    # displays a substitution.
    def showSubstitution(self, subst):
        if len(subst) == 0:
            return ""
        else:
            subst1, subst2 = subst[0]
            return ("\nTerm:\n" + subst1.toStringXml("") + "\nTerm:\n" +
                subst2.toStringXml("")
                    + "-----\n" + self.showSubstitution(subst[1:]))

    # display a list of substitutions.
    def showSubstitutionList(self, substList):
        output = "\nSubstitution List\n"
        for subst in substList:
            output = output + (self.showSubstitution(subst) + "==============")
        output = output + "\nEnd of substitution list.\n\n"
        return output                               

    class ApplySubstitution:

        def setSubstitution(self, subst):
            self.subst = subst

        def f (self, tree):
            if len(self.subst) == 0:
                return tree
            if (tree.name == "Var" or tree.name == "EVar" or
                   tree.name == "GVar" or tree.name == "GEVar"
                   or tree.name == "URI"):
                for substitution in self.subst:
                    subst1, subst2 = substitution
                    if subst1.compareTreesFull(subst1, tree):
                        tree = subst2
            return tree            

    class ApplySubstitutionWithLevel:

        import UtilsN3

        utils = UtilsN3.Utils()

        def setSubstitution(self, subst):
            self.subst = subst

        def setLevel(self,level):
            self.level = level

        def f (self, tree):
            if len(self.subst) == 0:
                return tree
            if (tree.name == "Var" or tree.name == "EVar" or
                   tree.name == "GVar" or tree.name == "GEVar"):
                for substitution in self.subst:
                    subst2, subst1 = substitution
                    subst3 = subst1.copy()
                    subst4 = subst2.copy()
                    level1 = self.level - 1
                    if (subst3.name == "Var" or subst3.name == "EVar" or
                        subst3.name == "GVar" or subst3.name == "GEVar"):
                        (bool, s1, rest) = (
                             self.utils.parseUntilString (subst3.content, "$_$"))
                        if bool == "T":
                            level1 = int(s1)
                            subst3.content = rest[3:]
                    level2 = self.level - 1
                    if (subst4.name == "Var" or subst4.name == "EVar" or
                        subst4.name == "GVar" or subst4.name == "GEVar"):
                        (bool1, s2, rest) = (
                            self.utils.parseUntilString(subst4.content, "$_$"))
                        if bool1 == "T":
                            level2 = int(s1) 
                            subst4.content = rest[3:]
                        print "??????????????????????"
                        print `level2`, `level1`, self.level
                    if (level2 == self.level - 1 and level1 == self.level - 1):
                        if subst3.compareTrees(subst3, tree):
                            print "//////////////:"
                            tree = subst4
            if (tree.name == "URI"): 
                for substitution in self.subst:
                    subst2, subst1 = substitution
                    if subst1.compareTreesFull(subst1, tree):
                        tree = subst2
            return tree            

    class ApplySubstitutionReverse:

        def setSubstitution(self, subst):
            self.subst = subst

        def f (self, tree):
            if len(self.subst) == 0:
                return tree
            if (tree.name == "Var" or tree.name == "EVar" or
                   tree.name == "GVar" or tree.name == "GEVar"
                   or tree.name == "URI"):
                for substitution in self.subst:
                    subst2, subst1 = substitution
                    if subst2.compareTrees(subst1, tree):
                        tree = subst2
            return tree            
            
    # eliminate the doubles from a substitution
    def elimDoubleSubstitutions(self, substitution):
        if (len(substitution) == 0 or len(substitution) == 1):
            return substitution
        else:
            subst = substitution[0]
            t1, t2 = subst
            for subst1 in substitution[1:]:
                t3, t4 = subst1
                if ( t1.compareTreesFull(t1,t3) and
                          t1.compareTreesFull(t2, t4)):
                    return self.elimDoubleSubstitutions(substitution[1:])
            return [subst] + self.elimDoubleSubstitutions(substitution[1:])

    # compare two substitutions
    # if equal then 1 is returned else 0
    def compareSubstitutions(self, substitution1, substitution2):
        if (not len(substitution1) == len(substitution2)):
            return 0
        count = 0 
        flag = 1
        for subst1 in substitution1:
            flag = 1
            subst2 = substitution2[count]
            t1, t2 = subst1
            t3, t4 = subst2
            if (not t1.compareTreesFull(t1,t3) or
                  not t1.compareTreesFull(t2, t4)):
                flag = 0
                break
            count = count + 1
        return flag

    # eliminate the doubles from a substitutionLIST
    def eliminateDoublesFromSubstitutionList(self, substitutionList):
        if (len(substitutionList) == 0 or len(substitutionList) == 1):
            return substitutionList
        else:
            substitution1 = substitutionList[0]
            for substitution in substitutionList[1:]:
                if ( self.compareSubstitutions(substitution1,
                            substitution)):
                    return self.eliminateDoublesFromSubstitutionList(substitutionList[1:])
            return ([substitution1] +
                     self.eliminateDoublesFromSubstitutionList(substitutionList[1:]))
               
    # unify a tripleSet with a rule. The first clause is
    # a rule following the bnf for rules given higher. 
    # The second is tripleset.
    # The last returned parameter is the list of newly generated goals. 
    def unifyWithRule(self, tripleSet, rule):
        antecedents, consequents = self.selectTriplesFromRule(rule)
        bool, subst, tree, tree1 = self.unifyTripleSets(tripleSet, consequents)
        if bool:
            return (1, subst, tree, antecedents.children)
        else:
           return (0, [], tripleSet, [])


    # get all variables from a tree
    def getAllVariablesFromTree(self, tree):
        vars = tree.getChildrenByName(tree, "Var", [])
        vars = vars + tree.getChildrenByName(tree, "EVar", [])
        vars = vars + tree.getChildrenByName(tree, "GVar", [])
        vars = vars + tree.getChildrenByName(tree, "GEVar", [])
        return vars

    # get the antecedents and consequents from a rule.
    # These are returned as tripleSets.
    def selectTriplesFromRule(self, rule):
        done = 0
        subject = rule.getChildByName("Subject")
        subject1 = subject
        while not done:
            subject2 = subject1
            subject1 = subject
            subject = subject.getChildByName("Subject")
            if subject.type == "Empty":
                break
        antecedents = xml.XmlTree("TripleSet")
        antecedents.children = subject2.getDirectChildrenByName("Subject")
        verb = subject2.getChildByName("Verb")
        consequents = xml.XmlTree("TripleSet")
        consequents.children = verb.getChildrenByName(verb, "Subject", [])
        return (antecedents, consequents)
            
    # unify two triplesets; the second might be a rule.
    # optimisation possible by marking rules !!!!!
    def unifyTwoTripleSets(self, tripleSet1, tripleSet2):
        verbs = tripleSet2.getChildrenByName(tripleSet2, "Verb", [])
        bool = 0
        for verb in verbs:
            uri = verb.getChildByName("URI")
            content = uri.content
            (bool1, s1, rest) = self.utils.parseUntil(" ", content)
            if rest == self.logImplies:
                bool = 1
                break
        if bool:
            return self.unifyWithRule(tripleSet1, tripleSet2)
        else:
            return self.unifyTripleSets(tripleSet1, tripleSet2)

    # unify two triplesets but none is a rule.
    # returns a boolean, a substitution and a tripleset.
    def unifyTripleSets(self, tripleSet1, tripleSet2):
        subst = []
        tripleSet = xml.XmlTree("TripleSet")
        triples = tripleSet1.getDirectChildrenByName("Subject")
        bool = 0
        for triple in triples:
            bool, subst1, tree = self.unifyTripleWithTripleSet(triple, tripleSet2)
            subst = subst + subst1
            tripleSet.addTreeList(tree)
            if bool == 0:
                break
        if bool == 1:
            return (1, subst, tripleSet, tree)
        else:
            return (0, [], tripleSet1, [])

    # unify a triple with a tripleset.
    # return a boolean, a substitution and a triple 
    def unifyTripleWithTripleSet(self, triple, tripleSet):
        triples = tripleSet.getDirectChildrenByName("Subject")
        for triple1 in triples:
            bool, subst, tree = self.unifyTwoTriples(triple, triple1)
            if bool:
                return (1, subst, tree)
        return (0, [], [triple])            
        
    # unify two triples; returns a substitution. 
    # The first tree has a single verb and a single object;
    # the second tree might have multiple verbs and/or objects.
    # The first node is <Subject>. The children can be: <URI>, <Var>, <EVar>.
    # The second triple is returned modified.
    def unifyTwoTriples(self, triple1, triple2):
        # unify the subjects 
        bool, subst = self.unifyAtoms(triple1, triple2, [])
        if not bool:
            return (0, [], [triple2])
        else:
            verbs1 = triple1.getDirectChildrenByName("Verb")
            verbs2 = triple2.getDirectChildrenByName("Verb")
            # unify the verbs
            bool1, subst1, verb3 = self.unifyVerbs (verbs1, verbs2, subst)
            # unification of the objects must be called from unifyVerbs.
            # reconstitute the second triple.
            triple2.deleteAllChildren("Verb")
            triple2.addTree(verb3)
            if bool1:
                return (1, subst1, [triple2])
            else:
                return (0, [], [triple2])
            
    # unify two atoms (subject, verb or object). Returns a substitution
    # and a boolean.
    # Possibilities: URI with URI;(G)(E)VAR with URI; (G)(E)VAR with (G)(E)VAR.
    def unifyAtoms(self, tree1, tree2, substIn):
        if (tree1.type == "Empty" or tree2.type == "Empty"):
            return (0, substIn)
        else:
                atom1, type1 = self.getAtomFromTree(tree1)
                atom2, type2 = self.getAtomFromTree(tree2)
                if (type1 == "var" and type2 == "var" and
                    self.compareTreesVars(atom1, atom2)):
                    return (0, substIn)
                if tree1.compareTreesFull(atom1, atom2):
                    return (1, substIn)
                if (type1 == "var" and (type2 == "atom" or type2 == "subject")):
                    return (1, substIn + [(atom1, atom2)])
                if ((type1 == "atom" or type1 == "subject") and type2 == "var"):
                    return (1, substIn + [(atom2, atom1)])
                if (type1 == "var" and type2 == "var"):
                    return (1, substIn + [(atom1, atom2)])
                if (type1 == "subject" and type2 == "subject"):
                    treeList1 = tree1.getDirectChildrenByName("Subject")
                    treeList2 = tree2.getDirectChildrenByName("Subject")
                    return self.unifyTwoTerms(treeList1, treeList2)
                return (0, substIn)

    # get an atom from a tree.
    # returns the atom and the type = "var", "atom", "subject" or "empty".
    # If true then an simple atom exists,
    # otherwise the atom is complex. 
    def getAtomFromTree(self, tree):
        uri = tree.getChildByName("URI")
        if not uri.type == "Empty":
            return (uri, "atom")
        uri = tree.getChildByName("Var")
        if not uri.type == "Empty":
            return (uri, "var")
        uri = tree.getChildByName("EVar")
        if not uri.type == "Empty":
            return (uri, "var")
        uri = tree.getChildByName("GVar")
        if not uri.type == "Empty": 
            return (uri, "var")
        uri = tree.getChildByName("GEVar")
        if not uri.type == "Empty":
            return (uri, "var")
        uri = tree.getChildByName("Subject")
        if not uri.type == "Empty":
            return (uri, "subject")
        return (uri, "empty")  # no atom found; return empty tag and type.

    # unify two "verb"trees. For two matching verbs the corresponding objects
    # have to be unified as well.
    # The first list should have only one entry. (This is a little bit weird!!)
    def unifyVerbs(self, verbList1, verbList2, subst): 
        if (len(verbList1) == 0 or len(verbList2) == 0):
            return (0, [], xml.XmlTree("Empty"))
        verb1 = verbList1[0]
        for verb2 in verbList2:
            bool, subst1 = self.unifyAtoms(verb1, verb2, subst)
            if bool:
                objects1 = verb1.getDirectChildrenByName("Object")
                objects2 = verb2.getDirectChildrenByName("Object")
                bool1, subst2, object = self.unifyObjects(objects1, objects2, subst1)
                if bool1:
                   verb2.deleteAllChildren("Object")
                   verb2.addTree(object)
                   return (bool1,  subst2, verb2)
        return (0, [], verb2)
                
            
    # unify two "object"trees.
    # the first list should only contain one object.
    def unifyObjects(self, objectList1, objectList2, substIn):
        if (len(objectList1) == 0 or len(objectList2) == 0):
            return (0, [], xml.XmlTree("Object"))
        else:
            object = objectList1[0]
            object1 = objectList2[0] 
            bool, subst = self.unifyAtoms(object, object1, substIn)
            if bool:
                return (1,  subst, object1)
            else: # failure; search on.
                return self.unifyObjects(objectList1, objectList2[1:], substIn)

    # this function unifies two terms.
    # each term is a list of triples.
    def unifyTwoTerms(self, treeList1, treeList2):
        if (len(treeList1) == 0):
            return (1, [])
        else:
            bool, subst, tree = self.unifyTripleWithTerm(treeList1[0], treeList2)
            if bool:
                treeList3 = treeList1[1:]
                bool1, subst1 = self.unifyTwoTerms(treeList3,  treeList2)
                if bool1:
                    return (1, subst + subst1)
                else:
                    return (0, [])
            else:
                return (0, [])

    # unify a triple with a term.
    # a term is a list of triples.
    def unifyTripleWithTerm(self, triple, treeList):
        if len(treeList) == 0:
            return (1, [], triple)
        else:
            bool, subst, tree = self.unifyTwoTriples(triple, treeList[0])
            if (len(treeList) == 1 or bool):
                return (bool, subst, tree)
            return self.unifyTripleWithTerm(triple, treeList[1:])
                
    # create test data
    def createTestData(self):
        self.generate.createTestDB()
        self.semTree = self.generate.semTree
        self.semDic = self.generate.semDic
        axioms = self.semDic["axioms"]
        tripleSets = axioms.getDirectChildrenByName("TripleSet")
        tripleSet1 = tripleSets[0]
        triple1 = tripleSet1.getChildByName("Subject")
        tripleSet2 = tripleSets[1]
        triple2 = tripleSet2.getChildByName("Subject")
        rule1 = tripleSets[2]
        rule2 = tripleSets[3]
        query = self.semDic["query"]
        queryTriples = query.getDirectChildrenByName("TripleSet")
        qtripleSet1 = queryTriples[0]
        qtriple1 = qtripleSet1.getChildByName("Subject")
        qtripleSet2 = queryTriples[1]
        qtriple2 = qtripleSet2.getChildByName("Subject")
        rule1.printXml("")
        qtripleSet2.printXml("")
        bool, subst, tree, goals = self.unifyWithRule(rule1, qtripleSet2)
        print bool, self.showSubstitution(subst)
        tree.printXml("")
        tree.printTreeList(goals)

    # compare two trees; strip the level indication of the vars
    # this compares name, content and children
    def compareTreesVars (self, tree1, tree2):
       name1 = string.strip(tree1.name)
       name2 = string.strip(tree2.name)
       if (name1 == "Var" or name1 == "EVar" or
              name1 == "GVar" or name1 == "GEVar"):
           (bool1, s1, rest1) = (
                  self.utils.parseUntilString(tree1.content, "$_$"))
           name1 = rest1[3:]
       if (name2 == "Var" or name2 == "EVar" or
              name2 == "GVar" or name2 == "GEVar"):
           (bool2, s2, rest2) = (
                  self.utils.parseUntilString(tree2.content, "$_$"))
           name2 = rest2[3:]
       if (name1 == name2):
             children1 = tree1.children
             children2 = tree2.children
             flag = 0
             for t1 in children1:
                flag = 0
                for t2 in children2:
                   if self.compareTreesVars(t1, t2):
                      flag = 1
                      break
                if flag == 0:
                   return 0
             return 1   
       else:
          return 0
       
#unify = Unify()
#unify.createTestData()