import "N3Parser"
import "IO"
import "Utils"
import "XML"
import "Load"
import "Interact"
import "Observe"

-- The data structure of this program is based on the Euler program
-- by Jos De Roo : http://www.agfa.com/Euler
-- The resolution engine is modelled after the mini-prolog interpreter
-- of Marc P. Jones in the Hugs distribution. 

-- BNF for rules (in N3):

-- rule ::= "{" triplelist verbimplies triplelist "}" "a" objectTruth ";"
--            verbforall|verbforsome objectforall
-- ruleSubject ::= triplelist
-- triplelist ::= "{" triple* "}"
-- triple ::= as usual
-- verbimplies ::= "<http://www.w3.org/2000/10/swap/log#implies>"
-- objectTruth ::= "<http://www.w3.org/2000//10/swap/log#Truth>"
-- verbforall ::= "<http://www.w3.org/2000/10/swap/log#forall>"
-- verbforsome ::= "<http://www.w3.org/2000/10/swap/log#forsome>"
-- objectforall ::= URI ["," URI]*

-- BNF of the database:
--
-- database ::= clause*
-- clause ::= rule | triple
-- ** number is sequence number
-- ** ref1 is the number of the generating N3 statement in the process
-- ** of resolving abbreviations.
-- ** ref2 refers to the generating N3 statement for triples that where
-- ** embedded in another triple but externalised.
-- triple ::= subject verb object [number] [ref1] [ref2]
-- subject ::= triplelist | "<subject>" content "</subject<"
-- content ::= URI | var | vare
-- ** The first string is the abreviated URI; the second is the full URI.
-- ** For a var the tag uri is simply changed into the tag var.
-- ** var is an universal variable; vare is an existential variable
-- URI ::= "<URI>" String String "</URI>"
-- var ::= "<Var>" String String "<Var>"
-- vare ::= "<Vare>" String String "<Vare>"
-- verb ::= "<Verb>" content "</Verb>"
-- object ::= triplelist | "<Object>" content "</Object>"
-- triplelist ::= triple*
-- number ::= "<Number>" n "</Number>"
-- ref1 ::= "<Ref1>" n "</Ref1>"
-- ref2 ::= "<Ref2>" n "</Ref2>"
-- n ::= an integer
-- rule ::= "<Rule> <Subject>" triplelist  "<Verb> <URI>"
--          log:implies <http://www.w3.org/2000/10/swap/log#implies>
--          "</URI> <Object>" triple "</Object> </Verb> </Subject>"
--          "<Verb> <URI>"
--           a http://www.w3.org/1999/02/22-rdf-syntax-ns#type
--          "</URI> <Object> <URI>" 
--          log:Truth http://www.w3.org/2000/10/swap/log#Truth
--          "</URI> </Object> </Verb> <Verb> <URI>"
--           log:forAll http://www.w3.org/2000/10/swap/log#forAll
--          "</URI>" objectlist "</Verb> </Rule>"
-- objectlist ::= ("<Object>"  content "</Object>")*
--
-- Eventually log:forAll can be replaced by log:forSome
--
-- Mechanism of the engine
-----------------------------
-- All abbreviations of N3 have been removed (except for rules) so
-- that only triples consisting of subject, verb and object rest
-- (No more propertylists or objectlists). However every triple refers
-- by a number to the original N3 statement. Embedded triples are
-- (depending on a flag) duplicated als single triples with however also
-- a reference to the original triple and an indication of its embedded
-- origin.
-- Unification is done on triple basis. Firsts subjects are unified,
-- then verbs, then objects. Each time the current substitution is
-- augmented and applied to the next unification.
--
-- Handling of existential variables:
-- They are indicated by a tag <Vare>.
-- Functions to be adpated: markVariables, getVariables, unifyTwoTriples.
-- Embedded triples should be compared. 

-- Definition of the data structures
----------------------------------------

-- infix definitions for substitutions
infixr 3 @@

--- Substitutions:

-- a substitution is a list of tuples
type Subst = [(Var, Substituted)]

-- a variable is a triple containing the short name of the variable,
-- the full name and an integer:
-- the integer serves for variable renaming; two variables are equal if they
-- have the same name and the same value for the integer
-- The format is: <Var>name1 name2 integer</Var>
-- The integer is represented in string format
 
type Var = XMLTree
-- type for universal variable list
type Varlist = [XMLTree]
-- type for existential variable list
type EVarList = [XMLTree]

-- substitutions are represented by lists of tuples mapping variables  to
-- substituted values.
--
-- nullSubst is the empty substitution which maps every identifier to the
--           same identifier (as a term).
-- s1@@ s2  is the composition of substitutions s1 and s2
--                 s @@ nullSubst = s = nullSubst @@ s


nullSubst :: Subst
nullSubst = []

-- merge two substitutions; eliminate duplicates
(@@) :: Subst -> Subst -> Subst
s1 @@ s2 = s1 ++ s2

-- apply a substitution to a tree
applySubstitution :: Subst -> XMLTree -> XMLTree
applySubstitution [] tree = tree
applySubstitution subst tree = walkATree tree f
      where f (Tag tag@("Var", _, _)) =
                   (applySubstitutionToVar subst  (Tag tag))
            f (Tag tag@("EVar", _, _)) =
                   (applySubstitutionToVar subst  (Tag tag))
            f t = t

-- apply a substitution to a variable
applySubstitutionToVar :: Subst -> XMLTree -> XMLTree
applySubstitutionToVar [] v1 = v1 
applySubstitutionToVar (s@(v, t):ss) v1 
      | bv1 && v == v1 = applySubstitutionToVar ss t
      | v == v1 = t
      | otherwise = applySubstitutionToVar ss v1
      where bv1 = testVar t
            testVar (Tag t@("Var",_,_)) = True
            testVar (Tag t@("EVar",_,_)) = True
            testVar t = False

-- apply a substitution to a list
applySubstitutionToList :: Subst -> [XMLTree] -> [XMLTree]
applySubstitutionToList subst [] = []
applySubstitutionToList subst (x:xs) =
   (applySubstitution subst x):(applySubstitutionToList subst xs)

-- apply a substitution list to a list
applySubstitutionListToList :: [Subst] -> [XMLTree] -> [XMLTree]
applySubstitutionListToList [] list = list
applySubstitutionListToList (s:ss) list =
   applySubstitutionListToList ss
           (applySubstitutionToList s list)

-- a variable can be substituted by a variable, an URI, a general Term or
-- Empty. All these are XML trees. 
type Substituted = XMLTree

-- displays a substitution
showSubstitution :: Subst -> String
showSubstitution [] = ""
showSubstitution (s@(v, t):ss)  
    = "\nTerm1:\n" ++ fileToXML v ++ "\nTerm2:\n"
                 ++ fileToXML t ++ (showSubstitution ss)

-- display a list of substitutions
showSubstitutionList :: [Subst] -> String
showSubstitutionList [] = "Last empty list\n"
showSubstitutionList (s:ss) = showSubstitution s ++ "\n------------ next list"
                ++ "------------\n" ++ showSubstitutionList ss

-- check whether this is a circular substitution i.e. contains two times
-- the same variable;  and check for occurs.
checkCircularity :: Subst -> Bool
checkCircularity [] = False
checkCircularity ((v,t):xs)
   | (checkOccurs (v,t) xs) || bv1 = True
   | otherwise = checkCircularity xs
   where bv1 = v == t

-- check whether a variable already occurs within a substitution
checkOccurs :: (Var, Substituted) -> Subst -> Bool
checkOccurs _ [] = False
checkOccurs (v,t) ((v1,t1):xs)
   | v == v1 = True
   | otherwise = checkOccurs (v,t) xs

----------------------------------------------------------------------

-- data structure

type DB = [XMLTree]

-- Functions                     
----------------

t = searchProof "authen.axiom.n3" "authen.lemma.n3"
u = searchProof "danb.n3" "danb-query.n3"
onto = searchProof "ontology.axiom.n3" "ontology.query.n3"
onto1 = searchProof "ontology1.axiom.n3" "ontology1.query.n3"
comp = searchProof "complexTest.axiom.n3" "complexTest.query.n3"
danbg =searchProof "danbg.n3" "danbg-query.n3"
gedcom =searchProof "gedcom-merge.n3" "gedcom-query.n3"
type1 = searchProof "type1.axiom.n3" "type1.query.n3"

showDBs :: XMLTree -> XMLTree -> IO ()
showDBs axiomDB lemmaDB  =  putStr (fileToXML axiomDB)

-- read a parsed axiom-file, read a parsed lemma-file,execute
-- the refutation algorithm and display the result.
searchProof :: String -> String -> IO ()
searchProof fileName1 fileName2 =
    do s1 <- readFile fileName1
       s2 <- readFile fileName2
       executeProof (loadAndGet fileName1 (n3Parser s1) dbAxiom plist1)
                    (loadAndGet fileName2 (n3Parser s2) dbLemma plist2)
                    fileName1 fileName2

testSearchProof fileName1 fileName2 =
    do s1 <- readFile fileName1
       s2 <- readFile fileName2
       testExecuteProof (loadAndGet fileName1 (n3Parser s1) dbAxiom plist1)
                    (loadAndGet fileName2 (n3Parser s2) dbLemma plist2)

-- searches a proof for a query
loadAndGet :: String -> String -> XMLTree -> [String] -> XMLTree
loadAndGet fileName parseString db plist =  (thdTriple
             (loadString (parseString, plist, db))) 

dbAxiom = Tag ("DB", Empty, Empty)
dbLemma = Tag ("DB", Empty, Empty)
plist1 = []
plist2 = []

testExecuteProof axiom lemma = putStr (treeListToXML (queryDB))
   where dataBase = markAllVariables db varList varList2 1  -- number variables starting from 1
         db = (markRules (generateDB axiom))
         varList = eliminateEmpties(eliminateDoubles(getAllVariables db))
         varList2 = eliminateEmpties(eliminateDoubles(getAllVariablesE db))
         queryDB = markAllVariables querydb [] [] 1  -- number variables starting from 1
         querydb = (generateDB lemma)
         varList1 = eliminateEmpties (getAllVariables1 (queryDB))

printDB = False
embedded = False

authen = searchProof "authen.axiom.n3" "authen.lemma.n3"
danb = searchProof "danb.n3" "danb-query.n3"

-- each substitution in the returned substitutionlist is an
-- alternative solution to the query.
-- The method getAllSolutions puts all the solutions in a string
executeProof axiom lemma fileName1 fileName2
   | printDB = stringToFile (" axiom db:\n\n" ++ treeListToXML  db ++
                  "\n\n axiom variables:\n\n" ++ treeListToXML  varList ++
                  "\n\n  lemma db:\n\n" ++ treeListToXML qdb1 ++
                  "\n\n lemma variables:\n\n" ++ treeListToXML  varList1)
                  (fileName1 ++ "_" ++ fileName2 ++ ".db")
   | otherwise =  stringToFile ("trace:\n" ++ fileToXML trace
                     ++ "\nsubstitutions:\n" ++
                    (showSubstitutionList substitution) ++ "\n"
                    ++ "Lemma:\n" ++ treeListToXML qdb1 ++ "\n" ++
                     "Solutions:\n" ++ getAllSolutions substitution qdb1)
                    (fileName1 ++ "_" ++ fileName2 ++ ".eng")
   where (db, varList) = generateExtendedDB axiom embedded
         (qdb, varList1) = generateExtendedDB lemma False
         qdb1 = eliminateLog qdb
         (substitution, trace) = (proof db qdb1)

-- eliminate log: statements from lemma.
eliminateLog :: [XMLTree] -> [XMLTree]
eliminateLog [] = []
eliminateLog (x:xs)
   | (bv1) || (bv2) = eliminateLog xs
   | otherwise = x:eliminateLog xs
   where verb = getChildByName x "Verb"
         children = getAllTags verb
         bv1 = searchContent children "log:forAll"
         bv2 = searchContent children "log:forSome"

-- displays all the solutions in a string
getAllSolutions :: [Subst] -> [XMLTree] -> String
getAllSolutions [] query = "\nThis were all the solutions"
getAllSolutions (s:ss) query =
       "\n-----------Solution--------\n" ++ treeListToXML(applySubstitutionToList s query)
       ++ "\n" ++ getAllSolutions ss query


-- this extends the DB by eliminating abbreviations, adding a number
-- and duplicating embedded triples if the embedded flag is set
-- The passes flag indicates whether embedded triples will be
-- instantiated or not.
generateExtendedDB :: XMLTree -> Bool -> ([XMLTree], Varlist)
generateExtendedDB input embedded
   | embedded = (db5, varList1)
   | otherwise = (db6, varList1)
   where db5 = eliminateDoubles(eliminateEmpties(db4 ++ getEmbedded db4))
         db6 = eliminateDoubles(eliminateEmpties db4)
         db4 = extendDB db3
         -- number variables starting from 1
         db3 = addUpNumbers (eliminateDoubles(
                      db2 )) 1 "Number"
         db2 = markAllVariables db1 varList varList2 1
         db1 = (markRules (generateDB input))
         varList = getAllVariables db1
         varList2 = getAllVariablesE db1
         varList1 = eliminateEmpties(eliminateDoubles(
                 getAllVariables1 db2))


-- read a lemma, load it, generate the DB and print the result
testLemma fileName = readExternN3 fileName (loadLemma fileName)
   where loadLemma fileName parseString = putStr(treeListToXML(queryDB))
            where
               queryDB = markAllVariables querydb [] [] 1
               querydb = generateDB(
                       thdTriple(loadString (parseString, plist2, dbLemma)))

-- read a lemma, load it, generate the DB, extend the subjects
-- and print the result
testLemma1 fileName = readExternN3 fileName (loadLemma fileName)
   where loadLemma fileName parseString = stringToFile
                               (treeListToXML(queryDB1)) (fileName ++ ".ext")
            where
               queryDB1 = extendDB queryDB
               queryDB = markAllVariables queryDB2 [] [] 1
               queryDB2 = markRules querydb
               querydb = generateDB(
                       thdTriple(loadString (parseString, plist2, dbLemma)))

-- read a lemma, load it, solve the abbreviations,
-- generate the embedded triples
-- and print the result
testLemma2 fileName = readExternN3 fileName (loadLemma fileName)
   where loadLemma fileName parseString = stringToFile
                               (treeListToXML(queryDB5)) (fileName ++ ".emb")            where
               queryDB4 = eliminateDoubles(eliminateEmpties(queryDB3 ++
                                (getEmbedded queryDB3 )))
               queryDB5 = getEmbedded queryDB3
               queryDB3 = extendDB queryDB
               queryDB = addUpNumbers (eliminateDoubles(
                      (markAllVariables queryDB2 [] [] 1) )) 1 "Number"
               queryDB2 = markRules querydb
               querydb = generateDB(
                       thdTriple(loadString (parseString, plist2, dbLemma)))

-- get all embedded triples of a database and add a number
-- returns only the embedded triples
-- rules are skipped
-- These triples are marked by a tag "Ref2"
getEmbedded :: [XMLTree] -> [XMLTree]
getEmbedded [] = []
getEmbedded (x:xs)
   | bv1 && s1 == "Rule" = getEmbedded xs 
   | not bv2 && bv3 && not bv4 = numberedChildren ++ getEmbedded xs
   | otherwise = getEmbedded xs
   where children =  getChildrenByName x "Subject"
    -- [addTree (Tree (getChildrenByName x "Subject")) x]
    -- [addTree (Tag ("test",Empty, Empty)) x]
         bv4 = children == []
         children1 = getChildrenByName x "Ref1"
         (t:cs) = children1
         bv3 = testTag t
         bv2 = children1 == []
         c = getContentFromTag t
         Content (s, _) = c
         n = stringToInt s
         numberedChildren = addNumbers children n "Ref2"
         bv1 = testTag x
         Tag (s1, _, _) = x
          
-- add a (same) number to each tree in a list
-- The string is the name of the tag that contains the number
addNumbers :: [XMLTree] -> Int -> String -> [XMLTree]
addNumbers [] n s = []
addNumbers (c:cs) n s = addNumber c n:addNumbers cs n s
   where addNumber c n = addTree c tag1
             where tag = Tag (s, Empty, Empty)
                   c1 = Content (intToString n, Empty)
                   tag1 = addTree tag c1

testAddUpNumbers = stringToFile (treeListToXML(
                    addUpNumbers testDB 1 "Number")) "testAddUpNumbers.tst"

-- add upgoing numbers to each tree in a list
-- The string is the name of the tag that contains the number
addUpNumbers :: [XMLTree] -> Int -> String -> [XMLTree]
addUpNumbers [] n s = []
addUpNumbers (c:cs) n s = addNumber c n:addUpNumbers cs (n+1) s
   where addNumber c n = addTree c tag1 
             where tag = Tag (s, Empty, Empty)
                   c1 = Content (intToString n, Empty)
                   tag1 = addTree tag c1

                                                      
-- The database is a list of clauses and is constituted by the children
-- of the XML tree generated by the module load.
-- generate the database from the XML tree
generateDB :: XMLTree -> [XMLTree]
generateDB db 
   | bv2 = t1
   | bv1 = [Tag tag]
   | otherwise = []
   where t = getChildren db
         bv1 = testTag t 
         bv2 = testTree t
         Tree t1 = t
         Tag tag = t

-- saveVars fileName = readExternN3 fileName (testGetVars fileName)

-- mark the rules in the database
markRules :: DB -> DB
markRules [] = []
markRules db@(x:xs)
   | found = tag:markRules xs
   | otherwise = x:markRules xs
   where tagList = getAllTags x
         found = searchContent tagList "log:implies" 
         Tag (name, tree, parent) = x
         tag = Tag ("Rule", tree, parent)


-- this function marks all variables; the tag <URI> is changed to
-- <Var> .
markAllVariables :: DB -> Varlist -> EVarList -> Int -> DB
markAllVariables [] varlist varlist1 i = []
markAllVariables db@(x:xs) varlist varlist1 i =
    (markVariables x varlist varlist1 i):
          (markAllVariables xs varlist varlist1 (i + 1))

-- mark the variables in a clause
-- The integer parameter is for numbering anonymous variables
markVariables :: XMLTree -> Varlist -> EVarList -> Int -> XMLTree
markVariables tree varlist varlist1 i =
   walkATree tree f
      where f (Tag tag@("URI", t, p))
               | startsWith s "_:" = addTree (Tag ("EVar", Empty, p))
                          (Content ("_" ++ intToString i ++ s, Empty))
               | startsWith s "?:" = addTree (Tag ("Var", Empty, p))
                          (Content ("?" ++ intToString i ++ s, Empty))
               | isIn varlist (Tag tag) = Tag tag1
               | isIn varlist1 (Tag tag) = Tag tag2
               | otherwise = Tag tag
               where Tag tag1 = Tag ("Var", t, p)
                     Tag tag2 = Tag ("EVar", t, p) 
                     Content (s, _) =  getChild (Tag tag)
            f t = t

-- extends the subjects in a DB (eliminate the abbreviations)
extendDB :: [XMLTree] -> [XMLTree]
extendDB [] = []
extendDB [Empty] = []
extendDB (x:xs)
  | bv5 = [x] ++ extendDB xs 
  | (not bv3) && bv2 && bv4 && bv1 = tree1 ++ extendDB xs
  | otherwise = extendSubjects x (-1):extendDB xs
  where -- encapsulate in a tree so the extra generated triples can be added.
        -- get the number of the clause
        children = (getChildrenByName x "Number")
        (t:cs) = children
        bv4 = testTag t
        bv3 = children == []
        bv1 = testContent c
        bv2 = testTag x
        Tag (s1, _, _) = x
        bv5 = s1 == "Rule"
        c = getContentFromTag t
        Content (s, _) = c
        n = stringToInt s
        -- extend the clause
        Tree tree = extendSubjects x n
        tree1 = tree
extendDB t = []

testExtendSubjects = putStr (fileToXML (extendSubjects (getChild testComp) 1))
testExtendSubjects1 = putStr (fileToXML tree)
   where Tag t@(s,t1,p) = getChild testComp
         tree = Tree (addNumbers (extendSubject
              (Tag (s, extendSubjects t1 1, p))) 1 "Ref1")
testExtendSubjects2 = putStr (fileToXML tree)
   where Tag t@(s,t1,p) = getChild testComp
         tree = Tree (extendSubject
              (Tag (s, t1 , p)))
testExtendSubjects3 = putStr (fileToXML tree)
   where Tag t@(s,t1,p) = getChild testComp
         tree = extendSubjects t1 1
testExtendSubjects4 = putStr (fileToXML (extendSubjects (Tree objectComp) 1))
testExtendSubjects5 = putStr (showXML  (extendSubjects oComp 1) " ")
testExtendSubjects6 = putStr (treeListToXML (getAllTags (extendSubjects oComp 1) ))

oComp = Tag ("Object", Tree treeComp, Empty)

-- this extends propertylists into separate triples
extendSubjects :: XMLTree -> Int -> XMLTree
extendSubjects Empty n = Empty
-- rules have a special format and stay as they are
extendSubjects (Tag tag@("Rule", _, _)) n = Tag tag
extendSubjects (Tag tag@(s, t, p)) n
   | (s /= "Subject") = Tag (s, extendSubjects t n, p)
   -- the tag is a subject
   | otherwise = Tree (addNumbers (extendSubject           
       (Tag (s, tree, p))) n "Ref1")
   where tree = extendSubjects t n
extendSubjects (Tree t) n = Tree (extendSubjectsTree t n)
extendSubjects c n = c  -- everything else

testExtendSubjectsTree = putStr ( treeListToXML (
                       extendSubjectsTree treeComp 1))

extendSubjectsTree :: [XMLTree] -> Int -> [XMLTree]
extendSubjectsTree [] n = []
extendSubjectsTree (x:xs) n = (extendSubjects x n):(extendSubjectsTree xs n)
--    | bv1 && bv2 = Tree (addNumbers (extendSubject
--        (Tag (s, extendSubjects t n, p))) n "Ref1"):
--                 (extendSubjectsTree xs n)
--    | otherwise = (extendSubjects x n):(extendSubjectsTree xs n)
--    where bv1 = testTag x                                             
--          Tag (s, t, p) = x
--          bv2 = s == "Subject"


testExtendSubject = putStr (treeListToXML( extendSubject (getChild testComp)))

extendSubject :: XMLTree -> [XMLTree]
extendSubject (Tag s@("Subject", t, p))
   | (i == 0) || (i == 1) = [Tag s]
   | otherwise = createTree verbs
   where Tag s1@(s2, t1, p1) = extendVerbs (Tag s)
         verbs = getDirectChildrenByName (Tag s1) "Verb"
         i = length verbs
         content =  getChild (Tag s1)
         createTree [] = []
         createTree (v:vs) = (Tag ("Subject", Tree (content:[v]), p1)):
                                     createTree vs
extendSubject t = [t]

testExtendVerbs = putStr (fileToXML (extendVerbs testComp))

--         tree = addNumbers (addSubjects subjects) n "Ref1"

-- this extends objectlists into separate triples
extendVerbs :: XMLTree -> XMLTree
extendVerbs Empty = Empty
extendVerbs (Tag tag@("Rule", _, _)) = Tag tag
extendVerbs (Tag tag@("Subject", t, p))
   | (i == 0) = Tag ("Subject", extendVerbs t, p)
   | otherwise = Tag ("Subject",
                     ( Tree (content:tree)), p)
   where verbs = getDirectChildrenByName (Tag tag) "Verb"
         i = length verbs
         addVerbs [] = []
         addVerbs (v:vs) = extendVerb v ++ addVerbs vs
         tree = addVerbs verbs
         content = getChild (Tag tag)
extendVerbs (Tag tag@(s, tree,p)) = Tag (s, extendVerbs tree, p)
extendVerbs (Tree []) = Tree []
extendVerbs (Tree t@(x:xs))
   = merge (Tree [extendVerbs x]) (extendVerbs (Tree xs))
extendVerbs c = c  -- everything else

testExtendVerb = putStr (treeListToXML( extendVerb verb3))

testGetDirectChildrenByName = putStr(treeListToXML(
         getDirectChildrenByName verb3 "Object"))

extendVerb :: XMLTree -> [XMLTree]
extendVerb (Tag v@("Verb", t, p))
   | (i == 0) = [Tag ("Verb", extendVerbs t, p)]
   | (i == 1) = [Tag v]
   | otherwise = createTree objects
   where objects = getDirectChildrenByName (Tag v) "Object"
         i = length objects
         content =  getChild (Tag v) 
         createTree [] = []
         createTree (o:os) = (Tag ("Verb", Tree (content:[o]), p)):
                                     createTree os
extendVerb t = [t] -- [extendVerbs t]


-- get the list of variables
getAllVariables :: DB -> Varlist
getAllVariables [] = []
getAllVariables (x:xs) = (getVariables x) ++ (getAllVariables xs)

-- get the variables from a tag
getVariables :: XMLTree -> [XMLTree]
getVariables t
   | tagList == [] = []
   | otherwise = varList
   where tagList = selectFromTree t f
         f (Tag tag@("Verb", t, _))
            | bool = [Tag tag]
            | otherwise = []
            where list = getAllTags t
                  bool = searchContent list "log:forAll" 
         f t = []
         (y:ys) = getChildrenByName (Tree tagList) "URI"
         varList = ys

-- get the list of existential variables
getAllVariablesE :: DB -> Varlist
getAllVariablesE [] = []
getAllVariablesE (x:xs) = (getVariablesE x) ++ (getAllVariablesE xs)

-- get the variables from a tag
getVariablesE :: XMLTree -> [XMLTree]
getVariablesE t
   | tagList == [] = [] 
   | otherwise = varList
   where tagList = selectFromTree t f
         f (Tag tag@("Verb", t, _))
            | bool = [Tag tag]
            | otherwise = []
            where list = getAllTags t
                  bool = searchContent list "log:forSome"
         f t = []
         (y:ys) = getChildrenByName (Tree tagList) "URI"
         varList = ys

getAllVariables1 :: DB -> Varlist
getAllVariables1 [] = []
getAllVariables1 (x:xs) = (getVariables1 x) ++ (getAllVariables1 xs)

-- get the variables from a tag
getVariables1 :: XMLTree -> [XMLTree]
getVariables1 t
   | tagList == [] = [] 
   | otherwise = varList
   where tagList = selectFromTree t f
         f (Tag tag@("Var", _, _)) = [Tag tag]
         f (Tag tag@("EVar", _, _)) = [Tag tag]
         f t = []
         varList = getChildrenByName (Tree tagList) "Var"
                  ++ getChildrenByName (Tree tagList) "EVar"

-- unify a triple with a rule. The first clause is a 'simple' triple:
-- with one verb and one object. The second is a rule following the bnf
-- for rules given higher.
-- The last returned parameter is the list of newly generated goals. 
unifyWithRule :: XMLTree -> XMLTree -> (Bool, Subst, XMLTree, [XMLTree])
unifyWithRule triple rule
   | bv1 && bool = (True, subst, tree, ts)
   | otherwise = (False, nullSubst, triple, [])
   where triples = selectTriplesFromRule rule
         (bool, subst, tree) = unifyTwoTriples triple t
         (t:ts) = triples
         bv1 = length triples > 1

-- get the premisses and the consequent of a rule.
-- The first element in the returned list is the consequent.
selectTriplesFromRule :: XMLTree -> [XMLTree]
selectTriplesFromRule rule = reverse xs
   where list = selectFromTree rule f
         f (Tag tag@(s, _, _))
           | (s == "Subject") && (bv1 || bv2) = [Tag tag]
           | otherwise = []
           where Tag (s1, _, _) = getChild (Tag tag)
                 bv1 = s1 == "URI"
                 bv2 = s1 == "Var"
         f t = []
         (xs) = eliminateEmpties list

-- 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.
unifyTwoTriples :: XMLTree -> XMLTree -> (Bool, Subst, XMLTree)
unifyTwoTriples t1 t2
   | b == False = (False, nullSubst, t2)
   | b1 == False = (False, nullSubst, t2)
   | otherwise = (True, subst1, t3)
   where -- unify the subjects
         (b, subst) = unifyAtoms t1 t2 nullSubst
         v1 = eliminateEmpties (getDirectChildrenByName t1 "Verb")
         v2 = eliminateEmpties (getDirectChildrenByName t2 "Verb")
         -- unify the verbs
         (b1, subst1, v3) = unifyVerbs v1 v2 subst
         -- unification of the objects must be called from unifyVerbs
         -- reconstitute the second triple
         t3 = replaceChild t2 v3 s
         Tag (s, t, p) = v3

-- unify two atoms (subject, verb or object). Returns a substitution
-- and a boolean.
-- Possibilities: URI with URI; (E)VAR with URI; (E)VAR with (E)VAR.
unifyAtoms :: XMLTree -> XMLTree -> Subst -> (Bool, Subst)
unifyAtoms Empty _ substIn = (False, nullSubst)
unifyAtoms t1 t2 substIn
   -- this test must be first!!!
   | (not bv3) && (not bv4) = (False, substIn)
   | testTag1 && (not testTag2) && (s1 == "Var" || s1 == "EVar") =
                              (True, substIn @@ [(Tag c1, t4)])
   | testTag2 && (not testTag1) && (s2 == "Var" || s2 == "EVar") =
                              (True, substIn @@ [(Tag c1, t3)])
   | testTag1 && (s1 == "Var" || s1 == "EVar") =
                       (True, substIn @@ [(Tag c1, t6)])
   | testTag2 && (s2 == "Var" || s2 == "EVar") =
                       (True, substIn @@ [(t5, Tag c2)])
   | (not bv5) || (not bv6) = (False, substIn)
   | (t5 == t6) || (bv5 && bv6 && bv1 && bv2) = (True, substIn)
   | bv7 && bv8 = unifyTwoTerms t7 t8
   | otherwise = (False, substIn)
   where bv3 = testTag t1
         bv4 = testTag t2
         t3 = applySubstitution substIn t1
         t4 = applySubstitution substIn t2
         Tag c1@(s1, _, _) = t5
         Tag c2@(s2, _, _) = t6
         testTag1 = testTag t5
         testTag2 = testTag t6
         t5 = getSpecialChild t3
         t6 = getSpecialChild t4
         -- an anonymous subject matches only with another anonymous
         -- subject or with whatever subject ????
         Content c3@(s3, _) = content1
         content1 = getContentFromTag t5
         bv5 = testContent content1
         Content c4@(s4, _) = content2
         content2 = getContentFromTag t6
         bv6 = testContent content2
         bv1 = (startsWith s3 "_T$$$")
         bv2 = (startsWith s4 "_T$$$")
         -- test if recusively matching is necessary
         bv7 = s1 == "Subject"
         bv8 = s2 == "Subject"
         -- get a single triple or a triple list
         t7 = getSpecialChild1 t3
         t8 = getSpecialChild1 t4

getSpecialChild :: XMLTree -> XMLTree
getSpecialChild (Tag (s, Tree t@(x:xs), _)) = x
getSpecialChild (Tag (s, t, _)) = t
getSpecialChild t = getChild t

getSpecialChild2 :: XMLTree -> XMLTree
getSpecialChild2 (Tag (s, Tree t, _)) = Tree t
getSpecialChild2 (Tag (s, t, _)) = t
getSpecialChild2 t = getChild t

getSpecialChild1 :: XMLTree -> [XMLTree]
getSpecialChild1 (Tag (s, Tree t, _)) = t
getSpecialChild1 (Tag (s, t, _)) = [t]
getSpecialChild1 t = [getChild t]

-- unify two "verb"trees. For two matching verbs the corresponding objects
-- have to be unified as well.
unifyVerbs :: [XMLTree] -> [XMLTree] -> Subst -> (Bool, Subst, XMLTree)
unifyVerbs [] _ _ = (False, nullSubst, Empty)
unifyVerbs [Empty] _ subst = (False, nullSubst, Empty)
unifyVerbs v1 [] subst = (False, nullSubst, Empty)
unifyVerbs v1 v2@(v:vs) subst
   | bool = (bool1, subst2, addTreeAfter v4 (mergeTreeList vs))
   | otherwise = (bool2, subst4, addTreeAfter v v3)
   where -- unify the verbs
         (bool, subst1) = unifyAtoms verb  v subst
         [verb] = v1
         -- get the objectlist
         o1 = eliminateEmpties (getDirectChildrenByName verb "Object")
         o2 = eliminateEmpties (getDirectChildrenByName v "Object")
         -- unify the objectlists
         (bool1, subst2, o3) = unifyObjects o1 o2 subst1
         -- reconstitute the second verb
         v4 = replaceChild v o3 s
         -- failure; search further
         (bool2, subst4, v3) = unifyVerbs v1 vs subst
         Tag (s, p, t) = o3

-- unify two "object"trees. 
unifyObjects :: [XMLTree] -> [XMLTree] -> Subst -> (Bool, Subst, XMLTree)
unifyObjects [] _ _ = (False, nullSubst, Empty)
unifyObjects [Empty] _ substIn = (False, nullSubst, Empty)
unifyObjects o1 [] substIn = (False, nullSubst, Empty)
unifyObjects o1 o2@(o:os) substIn
   | bool = (bool, subst, addTreeAfter o3 (mergeTreeList os))
   | otherwise = (bool1,  subst1, addTreeAfter o o2)
   where -- unify the objects
         (o4:oss) = o1
         (bool, subst, o3) = unifyTwoObjects o4 o substIn
         -- failure; search further
         (bool1, subst1, o2) = unifyObjects o1 os substIn

-- unify two objects. This is like unifyAtoms; only the subject is
-- marked as being unified. Returns a substitution
-- and a boolean.
-- Possibilities: URI with URI; VAR with URI; VAR with VAR.
unifyTwoObjects :: XMLTree -> XMLTree -> Subst -> (Bool, Subst, XMLTree)
--unifyTwoObjects Empty t substIn = (False, nullSubst, t)
unifyTwoObjects t1 t2 substIn
   | (not bv5) || (not bv6) = (False, substIn, t2)  -- not object tags
   |  bv1 && bv2 && (not bv3) && (not bv4) = (bool, subst, t2)
   | (not bv3) && (not bv4) = (False, substIn, t2)  -- not  tags
   | bv3 && (not bv4) && (s1 == "Var" || s1 == "EVar") =
                              (True, substIn @@ [(Tag c1,t4)], t4)
   | bv4 && (not bv3) && (s2 == "Var" || s2 == "EVar") =
                              (True, substIn @@ [(Tag c1, t3)], t3)
   | (s2 == "Var")||(s2 == "EVar") = (True, substIn @@ [(t5, Tag c2)],
                                t3)
   | (s1 == "Var")||(s1 == "EVar") = (True, substIn @@ [(Tag c1, t6)],
                                t4)
   | t3 == t4 = (True, substIn, t2)
   | otherwise = (False, substIn, t2) -- return unmodified object
   where t3 = applySubstitution substIn t1
         t4 = applySubstitution substIn t2
	 Tag t3'@(s3, _, _) = t3
	 Tag t4'@(s4, _, _) = t4
         bv3 = (testTag t5)
         bv4 = (testTag t6)
	 bv5 = (testTag t1)
	 bv6 = (testTag t2)
         t5 = getSpecialChild2 t3
         t6 = getSpecialChild2 t4
         Tag c1@(s1, _, _) = t5
         Tag c2@(s2, _, _) = t6
         -- test for recursively term matching
         bv1 = (s3 == "Object")
         bv2 = (s4 == "Object")
         -- get a single triple or a triple list
         t7 = getSpecialChild1 t3
         t8 = getSpecialChild1 t4
         (bool, subst) = unifyTwoTerms t7 t8

-- get a child or the first child
getChildO :: XMLTree -> XMLTree
getChildO Empty = Empty
getChildO (Tree []) = Empty
getChildO (Tree (x:xs))
   | bv1 = x
   | bv2 = getChildO x
   | otherwise = Empty
   where bv1 = testTag x
         bv2 = testTree x 
getChildO (Tag ftag@(stag, Empty, _)) = Empty
getChildO (Tag ftag@(stag, Tag t, _)) = Tag t
getChildO (Tag ftag@(stag, Tree (x:xs), _)) = x  -- get first child
getChildO (Tag ftag@(stag, Content c, _)) = Content c
getChildO t = Empty  -- everything else is certainly bad


-- this function unifies two terms
-- each term is a list of triples
unifyTwoTerms :: [XMLTree] -> [XMLTree] -> (Bool, Subst)
unifyTwoTerms [] ys = (True, nullSubst)
unifyTwoTerms (x:xs) ys
   | bool = (True, subst @@ subst1)
   | otherwise = unifyTwoTerms xs ys 
   where (bool, subst, tree) = unifyTripleWithTerm x ys
         xs1 = applySubstitutionToList subst xs
         ys1 = applySubstitutionToList subst ys
         (bool1, subst1) = unifyTwoTerms xs1 ys1


-- unify a triple with a term
-- a term is a list of triples
unifyTripleWithTerm :: XMLTree -> [XMLTree] -> (Bool, Subst, XMLTree)
unifyTripleWithTerm t [] = (True, nullSubst, t)
unifyTripleWithTerm t (x:xs)
   | bool = (bool, subst, tree)
   | otherwise = unifyTripleWithTerm t xs
   where (bool, subst, tree) = unifyTwoTriples t1 x1
         t1 = getChildO t
         x1 = getChildO x

testValidTag (Tag t@(s,Tag t1@(s1,_,_),p)) = bv1
   where bv1 = s == "URI" || s == "Var"
testValidTag (Tag t@(s,Tree t1,p)) = bv1 && bv2
   where t2 = getChild (Tree t1)
         bv1 = testTag t2
         Tag (s2, p2, t3) = t2
         bv2 = s2 == "URI" || s2 == "Var"
testValidTag t = False


-- the stack is a list of triples. The first element is the substitution
-- at the point where the stack entry is made; the second element is
-- the list of outstanding goals and the third element is the list of altenative
-- clauses at the snapshot. 
type Stack = [(Subst, [XMLTree], [Alt])]

-- show the contents of the stack
showStack :: Stack -> String
showStack [] = []
showStack ((s, g, l):xs)  = "STACK:\n " ++ "Substitution: " ++
          (showSubstitution s) ++ "\n" ++ "Goals: "
          ++ (treeListToXML g) ++ "\n" ++ "Alts: " ++ (showAlts l)

-- show an alternative list
showAlts :: [Alt] -> String
showAlts [] = []
showAlts (x:xs) = showAlt x ++ showAlts xs 

-- show an alternative
showAlt alt@(treeList, subst) =
   treeListToXML treeList ++ showSubstitution subst ++ "\nEnd\n"

-- an alternative consists of a goal and a substitution that must
-- be combined with the substitution that was already found at that
-- point. 
type Alt = ([XMLTree], Subst)

-- a proof has as input the database of clauses and a query
-- the output is a list of substitutions (one for each found solution)
-- and an XMLTree that contains information if the verbose flag is set.
-- the query is the initial goallist.
proof :: [XMLTree] -> [XMLTree] -> ([Subst], XMLTree)
proof db query = solve str nullSubst query [] 0 db

solve :: XMLTree -> Subst -> [XMLTree] -> Stack -> Int -> [XMLTree]
                            -> ([Subst], XMLTree)
-- when the goal list is empty and the stack is empty all solutions
-- have been found; if the goallist is empty but not the stack then
-- a backtrack will be done in search of further solutions.
solve t subs [] stack n db =   (subs:sub, t1)
   where (sub, t1) = backtrack t stack (n+1) db
-- search a solution for the goal at the top of the goallist.
solve t subs goals stack n db
   -- testing n permits to limit the number of loops when
   -- the limitFlag is set.
   | n > loopLimit && limitFlag = ([subs], t1)
   | bv2 || bv1 = solve t2 subs [] stack n db
   | otherwise = choose t1 subs (tail goalList) alts stack (n+1) db
    where -- make the trace
          t1 = testVerbose (addTree t solveTag)
          t2 = testVerbose (addTree t (Tag ("solve goallist empty",
                                  Empty, Empty)))
          solveTag = Tag ("solve",
                       Tree [goalsTag,getFailedSubstitution alts], Empty)
          goalsTag = Tag ("goals", Tree goals, Empty)
          bv2 = goals == []
          goalList = (checkGrounded goals)
          bv1 = goalList == []
          -- get the alternatives
          g = head goalList
          alts = (getAlts db (applySubstitution subs g) subs)
          getFailedSubstitution ([], _) = t3
             where t3 = Tag ("failed_substitution", Tree [t4, g], Empty)
                   c = Content(showSubstitution subs, Empty)
                   t4 = Tag ("already_made_substitution", c, Empty)
          getFailedSubstitution al = Empty


-- choose an alternative                 
choose :: XMLTree -> Subst -> [XMLTree] -> ([Alt], [XMLTree]) -> Stack
                         -> Int -> [XMLTree] -> ([Subst], XMLTree)
-- the list of alternatives is empty; backtrack to
-- the last list of alternatives 
choose t subs gs ([],_)  stack n db = backtrack t1 stack (n+1) db
   where t1 = testVerbose (addTree t (Tag ("choose", Empty, Empty)))
-- add the goals of the first alternative to the goallist
-- and combine the substitutions and try to solve; save the
-- previous goallist on the stack with the previous substitution
-- and the previous list of alternatives.
choose t subs gs (altList, altS) stack n db
      = solve t2 (subs@@sub) (tree ++ gs) ((subs,gs,alts):stack) (n+1) db
   where t1 = testVerbose (addTree t (Tag ("choose", Empty, Empty)))
         t2 = testExtended (addTree t1 (Tree altS))
         al@((tree,sub):alts) = altList
         
-- If a goal fails then retrieve the last saved situation from
-- the stack.
backtrack :: XMLTree -> Stack -> Int -> [XMLTree] -> ([Subst], XMLTree)
-- stack is empty; nothing to backtrack.
backtrack t [] n db = ([], t)
backtrack t stack n db 
         = choose t1 subst goals (alts,[])  sts (n+1) db
   where t1 = testVerbose (addTree t (Tag ("backtrack", Empty, Empty))) 
         st@((subst, goals, alts):sts) = stack


str = testVerbose (Tag ("proof", Empty, Empty))

-- checks whether a goal is grounded or not; if it is the goal is
-- eliminated.
checkGrounded :: [XMLTree] -> [XMLTree]
checkGrounded [] = []
checkGrounded (x:xs)
   | ((bv2 && (not bv1)) || (not bv2)) && (n == 0) = checkGrounded xs
   | (bv2 && bv1) || (n > 0) = x:checkGrounded xs 
   | otherwise = x:checkGrounded xs
   where t = (getChildrenByName x "Var")
         t1 = (getChildrenByName x "EVar")
         Tag (s, _, _) = x
         bv1 = (s == "Var")||(s == "EVar")
         bv2 = testTag x
         n = length t + length t1
  
-- if the verbose flag is True then the XMLTree that is input is output
-- else an empty XMLTree is returned
testVerbose :: XMLTree -> XMLTree
testVerbose t
   | verbose = t
   | otherwise = Empty

-- if the extended flag is True then the XMLTree that is input is output
-- else an empty XMLTree is returned
testExtended :: XMLTree -> XMLTree
testExtended t
   | extended = t
   | otherwise = Empty

-- get the list of matches of a triple with the heads in the database
-- unify and rename the variables
-- this is the kernel of the resolution engine
-- The first parameter is the database; the second is the goal to unify;
-- The third parameter is the current substitution.
-- Output is a list of alternatives
-- consisting of pairs that contain a clause and a substitution:
-- type Alt = (XMLTree, Subst), and an XMLTree that contains trace data.
getAlts :: [XMLTree] -> XMLTree -> Subst -> ([Alt], [XMLTree])
getAlts [] t substIn = ([], [out2])
   where out1 = Tag ("Input triple for generation of above goals", Empty, Empty)
         out2 = testExtended (addTree out1 t)
getAlts (x:xs) t substIn
   | bv2 && bv1 && bool && (not bv3) =
             ([(eliminateEmpties goals, subst)] ++ alts, out1:out3:out2)
   | bv2 && (not bv1) && bool1 && (not bv4) =
                    ([([x], subst1)] ++ alts, out1:out2)
   | otherwise = getAlts xs t substIn
   where Tag (s, _, _) = x
         bv2 = testTag x
         bv1 = s == "Rule"
         -- unify with a rule
         (bool, subst, t1, goals) = unifyWithRule t x
         -- check the validity of the substitution
         bv3 = checkCircularity  (subst ++ substIn)
         -- unify with a triple
         (bool1, subst1, t2) = unifyTwoTriples t x
         -- check the validity of the substitution
         bv4 = checkCircularity (subst1 ++ substIn)
         (alts, out2) = getAlts xs t substIn
         out = Tag ("Substitution", Empty, Empty)
         tree1 = [t, x]
         -- only trace output when the verbose flag is set
         out1 = testVerbose (addTree out (Tree tree1))
         out4 = Tag ("Goals", Empty, Empty)
         -- if the extended flag is set the goallist is output too
         out3 = testExtended (addTree out4 (Tree goals))

-- Test functions and data
--------------------------------

-- testdata
testTestTreeT = putStr (fileToXML testTreeT)

saveTestTreeT = stringToFile (fileToXML testTreeT) "testTreeT.tst"

testTreeT = loadDB pa7

testTestQuery = putStr (fileToXML testQuery)

testQuery = loadDB pa8

testTestDB = stringToFile (treeListToXML testDB) "testTestDB.tst"

testTestComp = putStr (fileToXML testComp)
testComp = loadDB pa9
testVerbComp = putStr (treeListToXML verbComp)
verbComp = getChildrenByName testComp "Verb"
testObjectComp = putStr (treeListToXML objectComp)
objectComp = getChildrenByName (Tree verbComp) "Object"
testTreeComp = putStr (treeListToXML treeComp)
treeComp =  getChildrenByName (Tree objectComp) "Subject"

testTestQueryDB = putStr (treeListToXML testQueryDB)

queryTriple = x                                      

   where (x:xs) = testQueryDB

-- build a query for testing.
testQueryDB :: [XMLTree]
testQueryDB = markAllVariables db [] [] 1  -- number variables starting from 1
   where db = (generateDB testQuery)

-- build a database for testing.
testDB :: [XMLTree]
testDB = markAllVariables db varList varList1 1  -- number variables starting from 1
   where db = (markRules (generateDB testTreeT))
         varList = getAllVariables db
         varList1 = getAllVariablesE db

testTestRule = putStr (fileToXML testRule)

testRule = x1
   where (x:x1:xs) = reverse testDB

-- testdata for unification.
testTriple1 = putStr (fileToXML triple1)
triple1 = x
   where (x:xs) = testDB
testTriple11 = putStr (fileToXML triple11)
triple11 = addTree (addTree (Tag ("Top", Empty, Empty))
                 (addTree triple1 verb2)) (addTree triple2 verb1)
testTriple2 = putStr (fileToXML triple2)
triple2 = (getChild(getChild r))
  where rules@(r:rs) = eliminateEmpties (getChildrenByName tree "Rule")
        tree = addTree (Tag ("DB", Empty, Empty)) (mergeTreeList testDB)
testVerb1 = putStr (fileToXML verb1)
verb1 = v
   where [v] = eliminateEmpties(getChildrenByName triple1 "Verb")
testVerb2 = putStr (fileToXML verb2)
verb2 = v
   where [v] = eliminateEmpties(getChildrenByName triple2 "Verb")
verb3 = addTree verb2 object1
testObject1 = putStr (fileToXML object1)
object1 = o
   where [o] = eliminateEmpties(getChildrenByName verb1 "Object")
testObject2 = putStr (fileToXML object2)
object2 = o
   where [o] = eliminateEmpties(getChildrenByName verb2 "Object")
                                                     
testUnifyTwoTriples = putStr(showSubstitution (sndTriple
                  (unifyTwoTriples triple1 triple2)))
testUnifyTwoTriples1 = putStr(fileToXML (thdTriple
                  (unifyTwoTriples triple1 triple2)))

testUnifyVerbs = putStr(showSubstitution (sndTriple
                  (unifyVerbs [verb1] [verb2] nullSubst)))
testUnifyVerbs1 =  (fstTriple
                  (unifyVerbs [verb1] [verb2] nullSubst))
testUnifyVerbs2 =  putStr(fileToXML(thdTriple
                  (unifyVerbs [verb1] [verb2] nullSubst)))

testUnifyTwoObjects = putStr(showSubstitution (sndTriple
                  (unifyTwoObjects object1 object2 nullSubst)))
testUnifyTwoObjects1 =  (fstTriple
                  (unifyTwoObjects object1 object2 nullSubst))
testUnifyTwoObjects2 =  putStr(fileToXML(thdTriple
                  (unifyTwoObjects object1 object2 nullSubst)))

testApplySubstitution = putStr (fileToXML (applySubstitution
                                nullSubst object2))

testMergeTreeList = stringToFile (fileToXML (mergeTreeList testDB))
                 "testMergeTreeList.tst"

testMarkRules = stringToFile (treeListToXML (markRules (generateDB(
                              testTreeT)))) "testMarkRules.tst"

testGetAllTags = stringToFile (showXMLlist (getAllTags testTreeT))
                               "testGetAllTags.tst"

testGenerateDB = stringToFile (treeListToXML (generateDB testTreeT))
                              "testGenerateDB.tst" 

testMarkAllVariables = stringToFile (treeListToXML
              (markAllVariables db1 varlist varList1 1)) "testMarkAllVariables.tst"
   where varlist = (getAllVariables db1)
         varList1 = getAllVariablesE db1
         db1 = markRules (generateDB (testTreeT))

testMarkAllVariablesQ = stringToFile (treeListToXML
              (markAllVariables db1 varlist varList1 1)) "testMarkAllVariablesQ.tst"
   where varlist = (getAllVariables db1)
         varList1 = getAllVariablesE db1
         db1 = markRules (generateDB (testQuery))

testMarkVariables = putStr (fileToXML (markVariables testTreeT varlist varlist 1))
   where varlist = (getAllVariables db1)
         db1 = markRules (generateDB (testTreeT))

testSelectTriplesFromRule = putStr (treeListToXML (t:ts))
     where (t:ts) = (selectTriplesFromRule  testRule)

testAdds = putStr (fileToXML (Tag tag2))
               where Tag tag1 = Tag ("Var", Empty, Empty)
                     Tag tag2 = addTree (Tag tag1) (Tag tag3)
                     Tag tag3 = addTree (Tag ("Id", Empty, Empty))
                                         (Content ("0", Empty))
           
testWalkATree1 = putStr (fileToXML (walkATree testTreeT f))
                 where f t = t

testGetAllVariables = putStr (treeListToXML (eliminateDoubles(getAllVariables
                             (markRules (generateDB (testTreeT))))))

testSearchContent = searchContent (getAllTags testTreeT) "log:implies"

testUnifyWithRule = putStr  ("Subst: " ++ (showSubstitution  subst) ++
   "\nTree: " ++ (fileToXML tree) ++ "\n" ++ (show bool)) 
   where (bool, subst, tree, treeList)  = 
              unifyWithRule queryTriple testRule

testProof = stringToFile ("Subst: \n" ++ (showSubstitutionList subst)
                    ++ "\nDebug info:\n" ++ fileToXML tree) "testProof.tst"
    where (subst, tree) = proof testDB testQueryDB

testGetAlts =
   stringToFile (showAlts (fst(getAlts testDB x nullSubst))) "testGetAlts.tst"
      where (x:xs) = testQueryDB


-- constants
--------------------

-- the unloaded list of variables
varlist :: XMLTree
varlist = Tag ("Variables", Empty, Empty)

verbose = True

extended = True

loopLimit :: Int
loopLimit = 50

limitFlag = False

swaplog = "http://www.w3.org/2000/10/swap/log"

impliesURI = swaplog ++ "#implies"

varURI = swaplog ++ "#forAll"

-- =======================================================
-- interactive part
-- start the interactive engine
-- triple, tripleset or anonymous set.
-- When finished enter 'q' to stop.

startEngine :: IO ()
startEngine  = loopE 0 

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

t1 = iProof "gn1.n3" "gn1-q.n3"
t2 = iProof "ontology.axiom.n3" "ontology.query.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 =
    loopE1 1 (getIdata axiomDB lemmaDB)

   
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

-- interactive loop
-- Johan Jeuring helped me with this. Thank you, Johan.
loopE1 :: Int -> SolveOut -> IO ()
loopE1 mystate output = do putStr "> "
                           s <- getLine
                           execE1 mystate output s

execE1 :: Int -> SolveOut -> String -> IO ()
execE1 mystate solveOut s
   | bv2 = do putStr ("Bye bye !!")  
   | bv1 && bv3 && bv4 = do putStr (writeData "end of inference" trace3) 
   | mystate == 3 =  do putStr (writeData "state3" trace3)
                        (loopE1 3 solveOut1)
   | mystate == 1 = do putStr  (writeData "choose" trace3)
                       (loopE1 3 solveOut1)
   | otherwise  = do putStr (writeData "choose"  trace3)
                     (loopE1 2 solveOut1)
   where (subs, goals, alts, stack, db, trace3) = solveOut
         (sub:subts) = subs
         bv2 = startsWith s "q"
         bv1 = stack == []
         bv3 = goals == []
         bv4 = alts == []
         (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 -> IO ()
loopE state = do putStr "> "
                 s <- getLine
                 execE state s

execW :: String -> IO ()                  
execW s = do searchProof s s
             loopE 0 

-- this function interprets the input string
execE ::  Int -> String -> IO ()
execE state s
   | state == 3 = do putStr s
                     (loopE 0)
   | (bv1 || bv2) && state == 0 = do putStr helpMessage
                                     (loopE 0)
   | bv3 && state == 0 = do putStr proofMessage
                            (loopE 1)
   | bv4 && state == 0 = do putStr "Bye bye !!" 
   | state == 1 =  do putStr ("Starting ...." )
                      (execW s)
   | otherwise = do putStr 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"

-- a proof has as input the database of clauses and a query
-- the output is a list of substitutions (one for each found solution)
-- and an XMLTree that contains information if the verbose flag is set.
-- the query is the initial goallist.
proofI :: [XMLTree] -> [XMLTree] ->
               ([Subst],[XMLTree],[Alt], Stack,[XMLTree], [XMLTree])
proofI db query = solveI nullSubst query [] db

-- the interactive solve gets returned: a substitution, the goallist,
-- the alternatives [Alt], the stack and the DB. The trace XMLTree
-- is not necessary here; neither the limitation integer.
-- With the returned values the procs:
-- bacttrackI stack db   (if the goallist is empty) or
-- choose subs gs1 alts stack db
-- can be called. 
solveI :: Subst -> [XMLTree] -> Stack -> [XMLTree]
                 -> ([Subst], [XMLTree], [Alt], Stack, [XMLTree], [XMLTree])
-- when the goal list is empty and the stack is empty all solutions
-- have been found; if the goallist is empty but not the stack then
-- a backtrack will be done in search of further solutions.
solveI  subs [] stack db = backtrackI stack db
--([subs], [], [], stack, db, [])
-- search a solution for the goal at the top of the goallist.
solveI subs goals stack db
   | bv1 = solveI subs [] stack db
   | otherwise = ([subs], gs1, fst(alts), stack, db, snd(alts))
   where goalList = checkGrounded goals
         alts = getAlts db (applySubstitution subs g1) subs
         bv1 = goalList == []
         gl@(g1:gs1) = goalList

-- choose an alternative
chooseI :: Subst -> [XMLTree] -> ([Alt], [XMLTree]) -> Stack -> [XMLTree]
              -> ([Subst],[XMLTree], [Alt], Stack, [XMLTree], [XMLTree])
-- the list of alternatives is empty; backtrack to
-- the last list of alternatives
chooseI subs gs ([],_)  stack db = backtrackI stack db
-- add the goals of the first alternative to the goallist
-- and combine the substitutions and try to solve; save the
-- previous goallist on the stack with the previous substitution
-- and the previous list of alternatives.
chooseI  subs gs (altList, altS) stack db =
   (subst1, goals, alts1, stack, db, altS1)
   where  al@((tree,sub):alts) = altList
          (subst1, goals, alts1, stack, db, altS1) =
               solveI (sub@@subs) (tree ++ gs) ((subs,gs,alts):stack) db

-- If a goal fails then retrieve the last saved situation from
-- the stack.
backtrackI :: Stack ->  [XMLTree] ->
   ([Subst], [XMLTree], [Alt], Stack, [XMLTree], [XMLTree])
-- stack is empty; nothing to backtrack.
backtrackI [] db = ([], [], [], [(nullSubst, [], [])], [], [])
backtrackI stack db 
   = ([subst], goals, alts, sts, db, [])
   where st@((subst, goals, alts):sts) = stack

-- To do:
--
-- * parameters log:param
-- * test interactive part
-- * make global test-functions
-- * test all use-cases
-- * make a specification of this program in N3
-- * make a spec of propositional and first order logic in N3
-- * problem of pure variable declarations