module IaProver where
import "N3Parser"
import "IO"
import "Utils"
import "XML"
import "Load"
import "Interact"
import "Observe"

-- start the interactive engine
-- triple, tripleset or anonymous set.
-- When finished enter 'q' to stop.
startEngine :: IO ()
startEngine  =  do is <- getContents
                   putStr (loopE 0 is)

type SolveOut = ([Subst], [XMLTree], [Alt], Stack, [XMLTree], [XMLTree])

t = iProof "authen.axiom.n3" "authen.lemma.n3"

iProof :: String -> String -> IO ()
iProof axiom lemma = do s1 <- readFile axiom
                        s2 <- readFile lemma
                        intProof (loadAndGet axiom
                                  (n3Parser  s1) dbAxiom plist1)
                                (loadAndGet lemma
                                  (n3Parser s2) dbLemma plist2)

intProof :: XMLTree -> XMLTree -> IO ()
intProof axiomDB lemmaDB =
    do is <- getContents
       putStr ((loopE1 1 (getIdata axiomDB lemmaDB)) is)

   
testGetIdata = putStr (showAlts alts [])
    where (subs, goals, alts, stack, db, trace) = getIdata testTreeT testQuery

getIdata axiomDB lemmaDB = solveI nullSubst lemma1 [] db1
   where (db1, varList) = generateExtendedDB axiomDB embedded
         (lemma1, varList1) = generateExtendedDB lemmaDB False
-- this reads a line in a loop and call exec

executeIProof axiom lemma = solveI nullSubst lemma1 [] db1
   where (db1, varList) = generateExtendedDB axiom embedded
         (lemma1, varList1) = generateExtendedDB lemma False

proofInT fileName1 fileName2 s1 s2 = 
        executeIProofT
                (loadAndGet fileName1 (n3Parser s1) dbAxiom plist1)
                (loadAndGet fileName2 (n3Parser s2) dbLemma plist2)

executeIProofT axiom lemma = (db1, lemma1)
   where (db1, varList) = generateExtendedDB axiom embedded
         (lemma1, varList1) = generateExtendedDB lemma False

loopE1 :: Int -> SolveOut -> Interact
loopE1 mystate output = readLine "> " (execE1 mystate output)

execE1 :: Int -> SolveOut -> String -> Interact
execE1 mystate solveOut s
   | bv2 = writeStr "Bye bye !!"  end
--   | bv1 && bv3 = writeStr "end of inference" end
   | mystate == 3 =  writeStr -- (showStack stack [])
                        "state3"
                  --       (writeData "state3" goals)
                           (loopE1 3 solveOut1)
   | mystate == 1 = writeStr  (writeData "choose" trace3)
                         (loopE1 3 solveOut1)
   | otherwise  = writeStr (writeData "choose"  trace3)
                         (loopE1 2 solveOut1)
                  where (subs, goals, alts, stack, db, trace3) = solveOut
                        (sub:subts) = subs
                        bv2 = startsWith s "q"
                        (subs1, goals1, alts1, stack1, db1, trace1) =
                              chooseI sub goals (alts, []) stack db
                        solveOut1 = (subs1, goals1, alts1, stack1, db1, [])

writeData s mytrace =  ("\n" ++ s ++ "\n" ++ treeListToXML mytrace ++ "\n")

-- this reads a line in a loop and then executes exec
loopE :: Int -> Interact
loopE state = readLine "> " (execE state)


-- this function interprets the input string
execE ::  Int -> String -> Interact
execE state s
   | state == 3 = writeStr s (loopE 0)
   | (bv1 || bv2) && state == 0 = writeStr helpMessage (loopE 0)
   | bv3 && state == 0 = writeStr proofMessage (loopE 1)
   | bv4 && state == 0 = writeStr "Bye bye !!" end
--   | state == 1 = searchProof s (loopE 0)
--   | state == 1 && bv6 = loopE1 2 solveOut
      -- set state 2
--   | bv6 = writeStr (treeListToXML db1) (loopE1 2 solveOut)
--   | bv7 = writeStr "bv7" readMyFile
  --            writeStr  (fileToXML db3) (loopE 0)
   -- (treeListToXML db2) (loopE1 2 solveOut1)
      -- Entering interactive mode..." (loopE1 2 solveOut)
   | otherwise = writeStr helpMessage (loopE 0)
   where bv1 = startsWith s "?"
         bv2 = startsWith s "help"
         bv3 = startsWith s "proof"
         bv7 = startsWith s "p"
         bv4 = startsWith s "q"
         bv5 = startsWith s "trace"
         bv6 = startsWith s "i "
         s1 = drop 2 s
         (bool, f1, f2) = parseUntil ' ' s1

state :: Int
state = 0
                       
helpMessage = "Semantic web inference engine\n" ++
              "================================\n\n" ++
              "?         = help function\n" ++
              "help      = help function\n" ++
              "proof     = start a proof\n" ++
              "q or quit = quit the program\n" ++
              "trace     = trace mode\n" ++
              "i         = interactive mode type: i axiomfile lemmafile\n" 

proofMessage = "Enter all axiom files followed by the lemma files\n"