import N3ParserX, ITripleX
import InfData, time, PVa, copy, RDFFSM
import RDFEngine as r
import RDFUnify as un
import Utils as utils
import Prelude as pre
import sys
#import psyco

#psyco.full()

class Proof:
 
    """ An RDFDB object contains:
    # a tripleset, a predicate dictionary, a variable predicate list,
    # an origin (of the triples), a type (query or db)
    # (Variables are treated differently in a query compared to a db)
 
    # Structures in InfData:
    # goallist = list of triples
    # templist = contains temporary triples for embedded rules
    # stack
    # pathdata
    # graphlist = list of RDFDB objects
    # mes = string
    # wset = 'proven' triples"""

    # definition of log constants
    logImplies = "http://www.w3.org/2000/10/swap/log#implies"
    logForAll = "http://www.w3.org/2000/10/swap/log#forAll"
    logForSome = "http://www.w3.org/2000/10/swap/log#forSome"

    # get the file prefix
    pers = PVa.PersistentString("pathPrefix.txt")
    filePrefix = pers.get()
    # get the proxy
    # proxy with authentication: put the proxy address and port in
    # "proxy.txt" and the userid and password (userid:password) in
    # the file "userPass.txt"
    # for proxy without authentication  put "noAuth"
    # in the file "proxy.txt" and put the address and port number of
    # the proxy in the environment variable "http-proxy".
    # both files should exist.
    # if no proxy is required, leave the files empty.
    pr = PVa.PersistentString("proxy.txt")
    proxy = pr.get()
    # get the proxy userid and password
    pr1 = PVa.PersistentString("userPass.txt")
    userPass = pr1.get()
    # proxy flag 0 = proxy with authentication; 1 = no proxy;
    # 2 = proxy without authentication
    authProxy = 0

    # the list of testcases
    testCases = ["animal.n3 animal-simple.n3",  #  ok
                 "project.a1.n3 project.qa.n3", #  ok
                 "authen.axiom.n3 authen.lemma.n3", # ok
                 "danb.n3 danb-query.n3", # ok
                 #"danc.n3 danc-query.n3", 
                 "gedcom-facts.n3 gedcom-relations.n3 gedcom-query.n3", # ok
                 "gedcom-simple.n3 gedcom-relations.n3 gedcom-qsimple.n3", # ok
                 #"graph.axiom.n3 graph.lemma.n3", 
                 "lists.n3 lists-query.n3", # ok
                 "rdf-facts.n3 rdf-rules.n3 rdf-query.n3", # ok
                 "rdfc25May-test.n3 rdfc25May.n3", # ok
                 # "rdfs-rules.n3 rdfs-query.n3", 
                 "russell.axiom.n3 russell.lemma.n3", # ok
                 #"subclass.n3 subclass-query.n3", 
                 "subprop.n3 subprop-query.n3",  # ok
                 #"tpoint-all.n3 tpoint-facts.n3 tpoint.n3 tpoint-query.n3", 
                 "varprop.n3 varprop-query.n3", # 
                 "ziv.n3 ziv-query.n3", # ok
                 #"wol-facts.n3 wol-rules.n3 wol-query.n3", 
                 "vogel.l.n3 vogel.q.n3", # ok
                 "boole.axiom.n3 boole.lemma.n3", # ok
                 "induction.axiom.n3 induction.query.n3", # ok
                 "Owls.n3 owls.query.n3", # ok
                 "ontology.axiom.n3 ontology.query.n3",    # ok
                 "ontology1.axiom.n3 ontology1.query.n3",  # ok
                 "altT.l.n3 altT.q.n3", # ok
                 "notTest.n3 notTest.q.n3", # ok
                 "logic.a.n3 logic.q.n3", # ok
                 "booleW.a.n3 booleW.q.n3",
                 "equal.a.n3 equal.q.n3", # ok
                 "builtins.n3 builtins.q.n3",
                 "ooo.a.n3 ooo.q.n3",
                 "test.n3 test.q.n3",
                 "song.n3 song.a.n3"]

    def __init__(self):
        # flag indicating a parse error
        self.parseError = "F"
        # flags
        self.interactive = 1
        self.verbose = 1
        # save results to disk??
        self.saveOnDisk = 0

        # the input files
        self.inputFiles = []

        # an InfData object
        # contains all data necessary for inferencing
        self.infData = InfData.InfData()

    # function for entering a number
    # the input string is displayed as prompt
    def enterNumber(self, s):
      done = 0
      while (not done):
         try:
            i = input(s)
            done = 1
         except:
            print("Please enter a number.\n")
      return i

    def getFileName(self):
        self.fileName = askopenfilename(filetypes=[("Param files", "*.par")])

    # interactive part
    def interact(self):
      self.printMenu()
      i = -1
      while (not i == 0):
        try: 
         i = self.enterNumber("")
         if i == 0:
            print ("\nThe program is stopped.")
            return
         elif i == 1:
            print "The testcases must be in a directory named \"testCases\"."
            print "The path prefix for this directory must be in the file:"
            print "\"pathPrefix.txt\" (with trailing slash)."
         elif i == 2:
            done = 0
            while not done:
                print "Please enter the name of a file to be loaded:"
                print "For access to the web please enter a complete url."
                print "For a file just give the absolute or relative path."
                print "To stop just push \"enter\""
                fileName = raw_input("")
                if len(fileName) == 0:
                    done = 1
                else: 
                    self.inputFiles = self.inputFiles + [fileName]
            print "\nInput files are: "
            print self.inputFiles
            self.proofTestCase()
         elif i == 3:
            print "Do you want to save the output to disk?"
            print "The filename will be: input_filename + .db"
            print "Answer Y or N."
            s = raw_input("")
            done = 0
            while (not done ):
               if s == "Y":
                  self.saveOnDisk = 1
                  print ("!!!!  Output will be to disk.  !!!!!")
                  done = 1
               elif s == "N":
                  self.saveOnDisk = 0
                  done = 1
                  print ("!!!!  Output will be to the screen.  !!!!!")
               else:
                  s = raw_input("Please enter Y or N.\n")
         elif i == 4:
            self.infData = InfData.InfData()
            self.infData.verbose = self.verbose
            self.infData.interactive = self.interactive
            self.choiceTestCases()
            i = self.enterNumber("")
            li = self.testFiles(i)
         elif i == 5:
            print "Proxy with authentication: put the proxy address and port in"
            print " \"proxy.txt\" and the userid and password (userid:password) in"
            print " the file \"userPass.txt\"."
            print " For a proxy without authentication  put \"noAuth\""
            print " in the file \"proxy.txt\" and put the address and port"
            print " number of the proxy in the environmnet variable:"
            print " \"http-proxy\"."
            print " If no proxy is required leave the files empty."
            print " Both files should exist."
         elif i == 6:
             print "Create the parameter files (see items 1 and 5 of the menu)."
             print " 1) create the file  \"pathPrefix.txt\""
             print " 2) create the file \"proxy.txt\""
             print " 3) create the file \"userPass.txt\""
             print " 4) stop"
             print "Please enter a number."
             i = self.enterNumber("")
             print "Please enter the content of the file:"
             while i < 4: 
                if i == 1:
                   print "pathPrefix.txt"
                   fileName = "pathPrefix.txt"
                elif i == 2:
                   print "proxy.txt"
                   fileName = "proxy.txt"
                elif i == 3:
                   print "userPass.txt"
                   fileName = "userPass.txt"
                s = raw_input("")
                if s == "":
                   s = " "
                file = PVa.PersistentString(fileName)
                file.modify(s)
         elif i == 7:
             n3Parser = N3ParserX.N3ParserX()
             n3Parser.interact()
         elif i == 8:
             if self.interactive:
                 str = "on."
             else:
                 str = "off."
             print "The interactive switch is now " + str
             print "Do you want to change it? (y/n)"
             done = 0
             while not done:
                 s = raw_input("")
                 if s == "y":
                     if self.interactive:
                         self.interactive = 0
                     else:
                         self.interactive = 1
                     break 
                 elif s == "n":
                     break
                 print "Please enter y or n." 
         elif i == 9:
             if self.verbose:
                 str = "on."
             else:
                 str = "off."
             print "The verbose switch is now " + str
             print "Do you want to change it? (y/n)"
             done = 0
             while not done:
                 s = raw_input("")
                 if s == "y":
                     if self.verbose:
                         self.verbose = 0
                     else:
                         self.verbose = 1
                     break 
                 elif s == "n":
                     break
                 print "Please enter y or n." 
         self.printMenu() 
        except IOError, (errno, strerror):
         print "I/O error(%s): %s" % (errno, strerror)
         print("Please retry.")
         self.printMenu()

    # print the menu
    def printMenu(self):
      print "\nRDF Inferencing --- Menu \n\n"
      print "0) stop"
      print "1) file prefix for the testCases"
      print "2) enter filenames and create db"
      print "3) output to disk\n       Name is filename + .db"
      print "4) select test case and execute"
      print "5) proxy parameters"
      print "6) create parameter files"
      print "7) call parser"
      print "8) toggle interactive flag (default is on)"
      print "9) toggle verbose flag (default is on)"
      print "Enter your choice: "

    # handling of the test cases
    def testFiles(self, i):
         web = 0
         n = 0
         n1 = len(self.testCases)
         done = 0
         self.inputFiles = []
         while not done and n<n1:
            n = n +1
            if n == i:
               fileNames = self.testCases[i-1:i].pop()
               # parse into self.inputFiles
               done1 = 0
               while not done1:
                   bool, s1, s2 = utils.parseUntilDelim(" ", fileNames)
                   self.inputFiles = (self.inputFiles +
                       [self.filePrefix + "testCases/" + s1])
                   s2 = utils.skipBlancs(s2)
                   if len(s2) == 0:
                       break
                   fileNames = s2
               done = 1
         print "\nInput files are: " 
         print self.inputFiles
         print ""
         self.proofTestCase()

    def testProofTestCase(self):
        self.infData = InfData.InfData()
        """ test of the function proofTestCase """
        self.inputFiles = ["authen.axiom.n3", "authen.lemma.n3"]
        self.proofTestCase()
        print "\n\nGoallist:\n\n" + Triple.tsToString(self.infData.goallist)
        print "\n\n query:\n" + self.infData.graphlist[-1].toString()
        print "\n\nGraphlist:\n" ,self.infData.graphlist

    def proofTestCase(self):
         fileName = self.inputFiles[0] + ".db"
         if 0: #os.path.isfile(fileName): # does not work well !!!!!!!
             inFile = open(fileName, "r")
             self.semTree = cPickle.load(inFile)
             self.semDic = cPickle.load(inFile)
             inFile.close()
         else:
         # function getRDFDB from N3Parser returns a full RDFDB object  
             print "start parsing..."
             time1 = time.clock()
             # for each file put an RDFDB object in the graphlist
             for file in self.inputFiles[0:-1]:
                 self.parseDB(self.infData, file)
             self.parseQuery(self.infData, self.inputFiles[-1])
             self.infData.query = self.getQuery(self.infData.graphlist, self.infData) 
             self.infData.goallist = self.scanQuery(self.infData.query, self.infData)
             print "end of parsing."
             time2 = time.clock()
             print "Duration of parsing: ", time2 - time1, " seconds."
             self.infData.parseTime = time2 - time1
             print "Graphs:\n\n", InfData.graphsToString(self.infData.graphlist,\
                                                         self.infData)
             self.infData.mes = "main"
             RDFFSM.proof(self.infData)
             if self.saveOnDisk:
                 outFile = open(self.inputFiles[0] + ".db", "w")
                 s = InfData.graphsToString(self.infData.graphlist, self.infData)
                 s = s + "Duration of parsing: "+ str(time2 - time1) +\
                       " seconds.\n"
                 if self.infData.sols == []:
                                     s = s + "There were no solutions found.\n"
                 i = 0
                 for sol in self.infData.sols:
                        s = s + "Solution:\n" + sol + "\n"
                        s = s + InfData.showclRes(self.infData.proofList[i], self.infData) + "\n"
                        i += 1
                 s = s + "Duration of inferencing: " + str(\
                      self.infData.infTime) + "\n" 
                 s = s + "Unifications steps : " + str(self.infData.unSteps) + "\n"
                 s = s + "Unifications : " + str(self.infData.unifs) + "\n"
                 s = s + "Unifications/sec : " + str(self.infData.unifs/\
                            self.infData.infTime) 
                 outFile.write(s)
                 outFile.close()
 
    def parseDB(self, inf, file):
        """ parse a data file and put the results in infData """
        n3Parser = N3ParserX.N3ParserX()
        n3Parser.queryFlag = "F"
        iTriple = ITripleX.ITripleX()
        (ts, inf) = iTriple.getRDFDB(n3Parser, file, inf)
        if n3Parser.errorflag == "T":
            print "\n\n!!!ERROR PARSING FILE: ", file, "\n\n"
            self.parseError = "T"
            exit
        inf.graphlist.append(ts)

    def parseQuery(self, inf, file):
        """ parse a query; this is different from parsing a DB """
        n3Parser = N3ParserX.N3ParserX()
        # set the queryflag in the parser
        n3Parser.queryFlag = "T"
        iTriple = ITripleX.ITripleX()
        (ts, inf) = iTriple.getRDFDB(n3Parser, file, inf)
        if n3Parser.errorflag == "T":
            print "\n\n!!!ERROR PARSING FILE: ", self.inputFiles[-1], "\n\n"
            self.parseError = "T"
            exit
        inf.graphlist.append(ts)

    def getQuery(self, graphlist, inf):
        query = []
        vals = graphlist[-1][0].values()
        for triplel in vals:
            for triple in triplel:
                query.append(triple)
        return query

    def scanQuery(self, query, inf):
        l = []
        for t in query:
            pred = t[2]
            if pred[0] == 0:
                 (nr, varn) = pred[1]
                 name = inf.revres[nr - 1000].fullname().content
                 if name <> "prefix:abbrev":
                     l.append(t)
            else:
                l.append(t)
        return l 

    def choiceTestCases(self):
      print "Possible test cases \n\n"
      n = 1
      for testCase in self.testCases:
         print `n` + ") " + testCase
         n = n + 1
      print "Enter your choice: "
 
"""
getInf [] server = error ("Wrong query: non-existent server: " ++ server ++ "\n")
getInf ((name,inf):ss) server
  | server == name = inf
  | otherwise = getInf ss server

-- get the query for the secondary server
addGoalsQ inf1 inf = inf1{goals=gls}
        where (g:gs) = goals inf
              gls = getTillEnd gs

getTillEnd [] = []
getTillEnd (g:gs)
        | gmpred g == "end_query" = [g]
        | otherwise = g:getTillEnd gs

-- type Closure = [(Statement,Statement)]
-- if st1 == st2 check if st1 is in graph of inf
-- if st1 is a rule 
check if all antecedents are in closure
-- before the rule as st1 
-- verifyClosure closure inf

-- verifySolution

-- adds the results after verifying
-- from the first solution the substitution must be added to the current
-- substitution; the pathdata must be extracted and added to the current
-- pathdata; the data from the other solutions must be tranformed into
-- a matchlist structure
addresults [] inf = inf{goals=elimTillEnd goals1}
        where goals1 = goals inf
addresults (s:ss) inf
        | goals2 == [] = inf2 
        | otherwise = inf1
        where goals1 = goals inf
              Sol su cl = s
              inf1 = inf{goals=(elimTillEnd goals1),
                         ml=(transformToMl ss),
                         pdata = PDE cl (lev inf):(pdata inf),
                         subst= su ++ subst inf}
              goals2 = goals inf1
              (sols1, genr) = getsols inf1 ""
              inf2 = inf1{sols=sols1}

transformToMl sols =
     [Match s [] cl|(Sol s cl) <- sols]

elimTillEnd [] = []
elimTillEnd (g:gs)
        | pred == "end_query" = gs 
        | otherwise = elimTillEnd gs
        where t = head(cons g)
              pred = grs(p t)

action1 g servers inf info 
       | pred == "end_query" = 
                  let -- add the results to inf and eliminate the
                      -- proven goals
                      (sols2, genr) = getsols inf "solution"
                      sols1 = sols2 ++ sols inf
                      infa = addresults sols1 info
                  in 
                  do putStr ("here %%%%%%%%\n" ++ (sgoals (goals infa)))
                     rpro servers infa
                     return ""
       | otherwise = do putStr "undefined action"
                        rpro servers info
                        return ""
       where t = ahead (cons g) g
             pred = grs (p t)
             ahead [] g = error ("action: " ++ show g ++ "\n")
             ahead t g = head t


action g servers inf = do case pred of
                    -- for query get the server indicated from the servers
                    -- list; the context must be switched to this
                    -- server
                    -- change InfData and call RPro; restore old
                    -- infdata and add results 
                    "query"  -> let subst1 = subst inf
                                    g1 = apps subst1 g
                                    server = grs(o (head(cons g1)))
                                    inf1 = getInf servers server
                                    inf2 = addGoalsQ inf1 inf
                                in
                                do astep servers inf2 inf
                    "load"   -> do list <- readFile obj
                                   let graph1 = makeRDFGraph list 3
                                       graphs1 = (graphs inf1)//[(3,graph1)]
                                       inf2 = inf1{graphs=graphs1}
                                   -- putStr (cgraph graph1)
                                   rpro servers inf2
                                   return ""
                    "print"  -> do putStr (obj ++ "\n")
                                   rpro servers inf1
                                   return ""
                    "end_query" -> do putStr "end of query"
                                      rpro servers inf1
                                      return "" 
        where t = ahead (cons g) g
              pred = grs (p t)
              obj = grs(o t)
              graph = (graphs inf)!3
              (gl:gls) = goals inf
              inf1 = inf{goals=gls}   -- take the goal away
              ahead [] g = error ("action: " ++ show g ++ "\n")
              ahead t g = head t

errmsg servers inf is = do putStr ("You entered: " ++ is ++ "\nPlease, try again.\n")
                           rpro servers inf
                           return ""

--- Main program read-solve-print loop:

signOn           :: String
signOn            = "RDFProlog version 2.0\n\n"

separate [] = []
separate filest
        | bool = fi:separate se
        | otherwise = [filest]
        where (bool,fi,se) = parseUntil ' ' filest

-- the integer indicates the provenance = server????
readGraphs             :: InfData -> String -> Int -> IO InfData
readGraphs inf filest nr = do let files = separate filest
                              putStr signOn
                              putStr ("Reading files ...\nEnter command"
                                       ++ " (? for help):\n")
                              listF@(f:fs) <- (sequence (map readFile files))
                              let graphs1 = graphs inf
                                  query1 = transF f
                                  (_,_,graphs2) = enterGraphs (fs,nr,graphs1)
                                  enterGraphs :: ([String],Int,Array Int RDFGraph)
                                         -> ([String],Int,Array Int RDFGraph)
                                  enterGraphs ([],n,graphs1) = ([],n,graphs1)
                                  enterGraphs (f:fs,n,graphs1)
                                    = enterGraphs (fs,n+1,graphs2)
                                    where graph = makeRDFGraph f n
                                          graphs2 = graphs1//[(n,graph)]
                              return (Inf graphs2 query1 query1 [] 1 [] [] [] [] "")


transF f = ts
    where (ts, _, _) = transTS (clauses, 1, 1, 10)
          parse = map clause (lines f)
          clauses = [ r | ((r,""):_) <- parse ]


    """
if __name__ == "__main__":
    fsm = Proof()
    if len(sys.argv) == 1:
        fsm.interact()
    else:
        for f in sys.argv[1:]:
           fsm.inputFiles.append(f)
        fsm.proofTestCase()