""" this is the RDF Finite State Machine
    # it is a resolution based inference engine implemented
    # as a finite state machine
    # all data relevant to inferencing are put in an
    # object InfData.
"""    

# module Proof.py

import Triple, copy, InfData, time
import Utils as utils
import RDFEngine as r
import RDFUnify as un, ITripleX 
import EngineManager, xmlx as x

def proof(infData):
        """ implementation of the finite state machine """
        showf = lambda inf: "step:\n" + "subst:\n" \
                  + un.substListToString(infData.subst, infData) + "\nhistory:\n" +\
		        InfData.showpd (infData.pathdata, infData) + "\n"
        showend = "\n\n**** End of inferencing ****\n===============================\n\n" 
        showbackt = "\nITriple**** Backtrack done. ****\n\n" 
        showlooping = "\n**** Looping detected; path aborted. ****\n\n" 
        showfailure = "\n**** No unification; path aborted. ****\n\n"

        # create an engine manager
        manager = EngineManager.EngineManager()
        mes = infData.mes
        # handle the inferencing parameters 
        handleParamTriples(infData)
        infData.check = 0
        first = 0
        # set start level to 0
        for t in infData.goallist:
            ITripleX.setLevel(t, 0)
        # start the timer    
        time1a = time.clock()
        # finite state loop
        while mes <> "endinf":
            if infData.falseFlag:
                if mes == "failure":
                    mes = "inf"
                else:
                    mes = "failure"
                infData.falseFlag += -1    
            testverbose(infData, "mes ===== " + infData.mes)
            #s = raw_input("begin")
            if mes == "solution":
                # retireve the solution
                getSols(infData)
                # show the solution
                testverbose(infData, showf(infData) + shows(infData))
                # only one solution? Then stop.
                if infData.onesol == 1:
			infData.mes = "endinf"
		else:	
	                r.backtrack(infData)
            elif mes == "backtracked":
                testverbose(infData, showbackt)
                # go and choose new goals
                r.choose(infData)
            elif mes == "looping":
                # looping. Abort current search path.
                testverbose(infData, showlooping)
                r.backtrack(infData)
            elif mes == "failure":
                #s = raw_input("hallo")    
                testverbose(infData, showfailure)
                r.backtrack(infData)
            # main state 
            else:
                act = checkPredicate(infData)
                # check now for builtins
		if act <> "inf" and len(infData.goallist) > 0:
	                gc = un.applySubstitutionListToTriple(infData.subst,\
				copy.deepcopy(infData.goallist[0]))
                if act == "str":
                    # handle string builtins
		    import RDFString
		    gl = infData.goallist
		    (bool1, bool2, list) = RDFString.select(gc, infData)
		    if bool2: # returns True
			    if len(gl) > 1:
				    gl = gl[1:]
			    else:
				    gl = []
			    infData.goallist = gl
    			    infData.pathdata.insert(0, ((gc,gc), infData.level))
#    			    continue
		    elif not bool2:
			    mes = "failure"
			    continue
	            else:
			    pass
		elif act == "Falsehood":
                    # get the triples of the subject
                    g = infData.goallist[0]
                    subg = g[1][1]
                    infData.falseFlag = len(subg)
                    infData.goallist = infData.goallist[1:]
                    infData.goallist = subg + infData.goallist
                    gc = un.applySubstitutionListToTriple(infData.subst, g)
		    infData.pathdata.insert(0, ((gc,gc), infData.level))
		    act = "inf"
		elif act == "list":
                    # handle list builtins
                    import RDFList
		    gl = infData.goallist
		    (bool1, bool2, tr) = RDFList.select(gc, infData)
		    if not bool1 and bool2: # returns True
			    if len(gl) > 1:
				    gl = gl[1:]
			    else:
				    gl = []
			    infData.goallist = gl
    			    infData.pathdata.insert(0, ((gc,gc), infData.level))
#    			    continue
		    elif not bool2:
			    mes = "failure"
			    continue
		    elif bool1 and bool2:
			    if len(gl) > 1:
				    gl = gl[1:]
			    else:
				    gl = []
			    infData.goallist = gl
    			    infData.pathdata.insert(0, ((tr,gc), infData.level))
#    			    continue
	            else:
			    pass
                elif act == "param":
			import RDFParam
                        (bool1, bool2, list) = RDFParam.select(infData.goallist.pop(0))
		elif act == "math":
                    # handle math builtins
                    import RDFMath
		    gl = infData.goallist
		    (bool1, bool2, tr) = RDFMath.select(gc, infData)
		    if bool2: # returns True
			    if len(gl) > 1:
				    gl = gl[1:]
			    else:
				    gl = []
			    infData.goallist = gl
                            tr1 = un.applySubstitutionListToTriple(infData.subst, tr)			    
    			    infData.pathdata.insert(0, ((tr1,tr1), infData.level))
#    			    continue
		    elif not bool2:
			    mes = "failure"
			    continue
	            else:
			    pass
		elif act == "sound":
                    # handle sound builtins
                    import RDFWinsound
		    gl = infData.goallist
		    (bool1, bool2, tr) = RDFWinsound.select(gc, infData)
		    if bool2: # returns True
			    if len(gl) > 1:
				    gl = gl[1:]
			    else:
				    gl = []
			    infData.goallist = gl
    			    infData.pathdata.insert(0, ((gc, gc), infData.level))
#    			    continue
		    elif not bool2:
			    mes = "failure"
			    continue
	            else:
			    pass
		elif act == "rdfe":
                        # handle my extensions
			import RDFRDFE
			(bool1, bool2, list) = RDFRDFE.select(gc, infData)
                        #print "goallist" ,Triple.tsToString(infData.goallist)
			if not bool1 and bool2:
			    if len(infData.goallist) > 1:
				    infData.goallist = infData.goallist[1:]
			    else:
				    infData.goallist = []
			    infData.pathdata.insert(0, ((gc,gc), infData.level))
#			    continue
			else:
				if not bool2:
					mes = "failure"
					continue
                else:
			pass
		#print "goallist", infData.goallist
		# print InfData.graphsToString(infData.graphlist)
		if infData.interactive:
			list = testInput()
			# analyze interactive input
			for it in list:
                                if it[0] == "c":
                                    infData.check = changeFlag(infData.check)
				if it[0] == "n":
					infData.mes = "stop"
					break
				if it[0] == "g":
					infData.interactive = changeFlag(infData.interactive)
				if it[0] == "s":
					infData.verbose = changeFlag(infData.verbose)
				if it[0] == "o":
					if len(it) == 1:
						infData.onesol = changeFlag(infData.onesol)
					else:
						try:
							nr = int(it[1:])
							infData.onesol = nr
						except:
							print "Please, o must be followed by\
								a number!!"
				if it[0] == "a":
                                        print "Andorra is not yet implemented." 
			if first == 0:
		                time1 = time.clock()
		                first = 1
		if infData.mes == "stop":
		    break
		testverbose(infData, showGoals(infData.goallist,\
				     infData) + showf(infData))
		if act == "inf":
      			r.solve(infData)
            if infData.check:			
        	    manager.checkLimits(infData)		
            mes = infData.mes
        if infData.mes[0:6] == "endinf":
            # take the finishing time
            time2 = time.clock() 		
            testnoout(infData, showend)
            sols = getAllSols(infData)
	    if sols == []:
		    print "There were no solutions found."
	    else:
                i = 0
                for sol in sols:
                    t = ITripleX.tsToString(sol, infData)    
                    infData.sols.append(t)
                    print "Solution:\n", t
                    print InfData.showclRes(infData.proofList[i], infData)
                    i += 1
            if first == 1:
                    infData.infTime = time2 - time1
	            print "\nDuration of inferencing: ", time2 -time1, " seconds."
	    else:
                    infData.infTime = time2 - time1a
	            print "\nDuration of inferencing: ", time2 -time1a, " seconds."
            print "Unifications steps: ", infData.unSteps
            print "Unifications: ", infData.unifs
            print "Unifications/sec : ",infData.unifs/infData.infTime                         
            print "Number of solutions: ", len(sols)

# format of a triple = (isR, s, p, o, fr, ruleNr, lev, trNr)
# format of a rule = (isR, s, p, o, fr, ruleNr, lev, trNr)
# resource = tuple(kind, res) where kind is the kind of resource:
# 0 = simple, 1 = list of triples, 2 = list of resources
def handleParamTriple(inf, triple):
    """ handle a triple containing an inference parameter.
    """
    predNr = triple[2][1][0]
    predC = inf.revres[abs(predNr) - 1000].label().content
    if predC[0:9] == "RDFE:init":
        subNr = triple[1][1][0]
        objNr = triple[3][1][0]
        subC = inf.revres[abs(subNr) - 1000].label().content
        objC = int(inf.revres[abs(objNr) - 1000].label().content)
        if subC == ":onesol":
            if objC == 1:
                print "Only one solution will be given.\n" +\
                      "Change with o-flag."
            else:
                print "All solutions will be given.\n" +\
                      "Change with o-flag."
            inf.onesol = objC
        elif subC == ":verbose":
            inf.verbose = objC
        
def handleParamTriples(inf):
    if inf.paramTriple == ():
        return
    ptr = r.getMatching(inf.graphlist, inf.paramTriple, inf)
    for t in ptr:
        handleParamTriple(inf, t)
        
def changeFlag(flag):
	if flag == 1:
		flag = 0
	else:
		flag = 1
	return flag	

def showGoals(goallist, inf):
        return "\nGoallist before solve:\n\n" +\
            ITripleX.tsToString([un.applySubstitutionListToTriple( inf.subst,\
			      t) for t in goallist if not(t == ())], inf)

def getAllSols(inf):
        """ This function applies all found substitutions to the query
            and produces a list of answers
        """
        # print "query    ",ITripleX.tsToString(inf.query, inf), inf.query
        # print "sollist ", [un.substListToString(subst) for subst in inf.solList]
        q1 = [t for t in inf.query]
        return [un.applySubstitutionListToTripleSet(subst, q1)
                for subst in inf.solList]
        
def getSols(inf):
        """ when a solution has been found two things are done:
            the substition is added to self.solList
            A proof is calculated and added to self.proofList
            A general rule is calculated: genRule (this is a triple).
            Results are a tuple of: (solList, proofList, ruleList)
        """
        pathdata = inf.pathdata
        subst1 = [sub for sub in inf.subst]
        inf.solList.append(subst1)
        backs = [ba for (ba, lev) in pathdata]
        inf.proofList.append(convbl(backs,inf.subst))
        if inf.wsactive:
                ts = [t for t in inf.query]
        	sol = un.applySubstitutionListToTripleSet(inf.subst,\
				ts)
		for t in sol:
			nr = t[2][1][0] # get predicate number
			if not inf.workingset.has_key(nr):
				inf.workingset[nr] = [t]
			else:
				inf.workingset[nr] = inf.workingset[nr] + [t]
#               genr = getGenRule inf sol query1

def shows(inf):
	""" show the last solution """
	s = "\nSolution:\n\n"
	s = s + ITripleX.tsToString(un.applySubstitutionListToTripleSet(inf.subst,\
				inf.query), inf)
	s = s + InfData.showcl(inf.proofList[-1], inf)
	return s
	
def convbl(backs, subst):               
        """ convert a list of backsteps to a closure using the substitution sub
            A closure is a list of tuples (triple, triple)
        """
        if backs == []:
            return []
        else:
            return [(un.applySubstitutionListToTriple(subst, t1),\
                     un.applySubstitutionListToTriple(subst, t2))\
                    for (t1, t2) in backs]
                
def testverbose(inf, s):
        if inf.verbose:
            print s
        elif inf.short:
            pass
        elif inf.noout:
            pass
        else:
            pass

def testshort(inf, s):
        if inf.short:
            pass
        elif inf.noout:
            pass
        else:
            print s

def testnoout(inf, s):
        if inf.noout:
            pass
        else:
            print s

def parseInput(s):
	""" parse a comma separated list
	    the list may not be empty
	"""
	list = []
	s = utils.skipBlancs(s)
	while not s == "":
		(bool, psd, rest) = utils.parseUntil(",", s)
		if bool == "F":
			psd = s
			s = ""
		# test the possibilities
		ch = psd[0]
		if ch == "y" or ch == "n" or ch == "s" or ch == "g" or ch == "o"\
		   or ch == "a" or ch == "c":
			list = list + [psd]
		s = utils.skipBlancs(rest)
        return list		

def testInput():
        t = 0
        while t == 0:
            s = raw_input("Continue? (y, n, s, g, o, a, c or ?)")
            if s == "":
                print "Please type y, n, s, g, o, a, c or ?"                    
            elif s[0] == "?":
		print "Abbreviations:\n"
		print "y = yes; next inference step"
		print "n = no; stop inferencing"
		print "s = silent; no more messages"
		print "g = go; no more interactive"
		print "o = onesol; only one solution"
		print "a = andorra; inferencing uses the andorra engine"
		print "c = check; control depth and nr of solutions"
		print "? = help; help function"
		print "presets: s = 0; g = 1; o = 0; a = 0; c = 0"
            else:
		list = parseInput(s)    
		if list == []:
	                print "Please type y, n, s, g, o, a, c or ?"
	        else:
			return list

nilTriple = Triple.getNilTriple()


""" deduce a general rule from a solution
getGenRule inf sol query1
   | not bool = rule
   | otherwise = ""
   where pd =concat [pbs pde|pde <- (pdata inf)]
         -- get the statements of the closure
         clos = cl sol
         -- get the rules from the closure
         rules = getRules [cl|(cl,_) <- clos]
         -- get all URIS from closure
         uris = elim
inateDoubles(concat(map getUrisRule rules))
         -- get the rules from the pathdata
         rulesp = getRules [pds|(pds, _) <- pd]
         -- get all URIS from the pathdata rules
         urisp = eliminateDoubles(concat (map getUrisRule rulesp))
         -- eliminate those uris from the closure list
         uris1 = elimFrom uris urisp
         -- get all uris from the query
         urisq = eliminateDoubles (eliminateEmptyR
                              (concat(map getUrisRule query1)))
         -- eliminate the uris from the query
         uris2 = elimFrom uris1 urisq
         -- get the facts of the closure
         facts1 = getFacts [cl|(cl,_) <- clos]
         facts2 = concat [fcts|(_,fcts,_) <- facts1]
         -- add the query to the facts after substitution
         query1 = query inf
         subst1 = subst inf
         query2 = appsts subst1 query1
         facts = concat(map cons query2) ++ facts2
         -- replace the uris
         repUris facts [] var num = facts 
         repUris facts uris@(u:us) var num
            = repUris (repSet facts u var num) us var (num+1)
         facts3 = repUris facts uris2 "X" 1
         f:fs = facts3
         bool = fact
s3 == []
         rule = sttopro (fs, [f], "")

-- in a set of facts replace a URI by a variable
repSet s uri var num =
   map (repTr uri var num) s

-- in a triple replace a URI by a variable
-- return a triple
repTr uri var num t
   = Triple (repRes (s t) uri var num, repRes (p t) uri var num,
             repRes (o t) uri var num)

-- replace a URI by a variable if it
-- matches with another URI; input is a resource;
-- return a resource
repRes res uri var num
   | res1 == uri = Var (UVar(var ++ (intToString num)))
   | otherwise = res
   where res1 = getUriRes res

-- eliminate the elements from the second set
-- in the first set
elimFrom set1 [] = s
et1
elimFrom set1 (x:xs)
   = elimFrom (elimItem set1 x) xs

-- get the rules of a set
getRules [] = []
getRules (x:xs)
   | trule x = x:getRules xs
   | otherwise = getRules xs

-- get the facts of a set
getFacts [] = []
getFacts (x:xs)
   | tfact x = x:getFacts xs
   | otherwise = getFacts xs

-- get the uris of a rule
getUrisRule r
   = eliminateDoubles(eliminateEmptyR (concat(urisa ++ urisc)))
   where urisa = map
 getUrisTr (ants r)
         urisc = map getUrisTr (cons r)

eliminateEmptyR set = [s|s <- set, s /= ""]

getUrisTr t = set
   where su = getUriRes (s t)
         pu = getUriRes (p t)
         ou = getUriRes (o t)
         set = [su, pu, ou]

-- get the URI from a resource 
getUriRes res
   | turi res = grs res
   | otherwise = ""

"""
def checkPredicate(inf):
	""" check whether the predicate is a builtin,
	    a call to an external server
	    or a predicate
	"""    
	if inf.goallist == []:
		return "inf"
	g = inf.goallist[0]
	pr = g[2]
	(k, r) = pr
	if k > 0:
            return "inf"
        (predi, varn) = r
	pred = inf.revres[abs(predi) - 1000].label().content
	if utils.startsWith(pred, "str:") == "T":
		# these are string functions
                return "str"
        elif utils.startsWith(pred, "liste:") == "T":
		# these are list functions
		return "list"
        elif utils.startsWith(pred, "math:") == "T":
		# these are math functions
		return "math"
        elif utils.startsWith(pred, "sound:") == "T":
		# these are math functions
		return "sound"
	elif utils.startsWith(pred, "a") == "T":
                # check for log:Falsehood
                objNameNr = g[3][1][0]
                try:
                    objName = inf.revres[abs(objNameNr) - 1000].label().content
                    if objName == "log:Falsehood":
                        return "Falsehood"
                except:
                    pass
        elif utils.startsWith(pred, "param:") == "T":
		# these are inferencing parameters
		return "param"
	elif utils.startsWith(pred, "RDFE:") == "T":
		# these are proprietary extensions
		return "rdfe"
	elif utils.startsWith(pred, "/=") == "T":
		return "rdfe"
	elif utils.startsWith(pred, "=") == "T":
                return "rdfe"
        return "inf"

	"""	| goals1 == [] = "inf" -- error ("checkPredicate: empty goals list")
     | g == ([],[],"0") = "inf"
     | otherwise =
       case pred of
           "load"     -> "action"
           "query"    -> "action"
           "end_query"-> "action"
           "print"    -> "action"
           otherwise  -> "inf"
       where t = thead (cons (g)) g
             pred = grs (p t)
             (g:gs) = goals1  -- get the goal
             thead [] g = error ("checkPredicate: " ++ show g)
             thead t
	 g = head t
 

"""