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

-- 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:

-- rule :: "{" triplelist verbimplies triplelist "}" "a" objectTruth ";"
--            verbforall 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>"
-- objectforall :: URI ["," URI]*

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

-- infix definitions for substitutions
--infixr 3 @@
--infix 4 ->-

--- Substitutions:

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

-- substitutions are represented by functions mapping variables  to
-- substituted values.
--
-- app s     extends the substitution s to a function mapping terms to terms
-- nullSubst is the empty substitution which maps every identifier to the
--           same identifier (as a term).
-- v ->- t   is the substitution which maps the variable v to the term t,
--           but otherwise behaves like nullSubst.
-- s1@@ s2  is the composition of substitutions s1 and s2
--                 s @@ nullSubst = s = nullSubst @@ s

app :: Subst -> Substituted -> Substituted
app s (Tag tag@("Var",_, _)) = s (Tag tag)
-- t is a general XML tree; the substitution has to be applied to all
-- variables
app s t = applySubstitution s t

nullSubst :: Subst
nullSubst v = v

(->-)                   :: Var -> Substituted -> Subst
(v ->- t) v1
   | v1 == v       = t
   | otherwise     = v1

(@@)                    :: Subst -> Subst -> Subst
s1 @@ s2                 = app s1 . s2 


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


-- Theoretical data structure 
-------------------------------
--
-- a term is a list of triples or a list of terms
--data Term = TripleList [Triple] |
--            Triple Triple|
--            TermList [Term] |
--            TermNull
--
-- a triple is made with a subject and a propertylist.
--type Triple = (Subject, PropertyList)
--
-- a propertylist is a list of properties
--type PropertyList = [Property]
--
-- a property is made of a verb and an objectlist
--type Property = (Verb, ObjectList)
--
-- a objectlist is a list of Objects
--type ObjectList = [Object]
--
-- an atom is an  uri, a variable or null
--data Atom = URI URI|
--            Var Var|
--            AtomNull
--
--
-- Subject Verb and Object are atoms or terms
--data Subject = SubjectAtom Atom |
--               SubjectTerm Term|
--               SubjectNull
--
--data Verb = VerbAtom Atom |
--            VerbTerm Term |
--            VerbNull
--
--data Object = ObjectAtom Atom |
--              ObjectTerm Term |
--              ObjectNull
--
-- a URI is a tuple with two strings; the first is the short name;
-- the second is the full name
--type URI = (String, String)
--
-- 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
-- 
--type Var = (String, String, Int)
--
-- a clause is a tuple with two terms . If the second term is empty
-- the clause is a fact; otherwise it is a rule.
--type Clause = (Term, Term)
--
-- a rule is a tuple made of two terms.
--type Rule = (Term, Term)
--
-- an alternate list is a list of clauses.
--type Alts = [Clause]
--
-- a stack permits the backtrack to a situation
--type Stack = [([Var],GoalList, [Rule])]
--
-- a query is Term =  a list of triples
--type Query = Term
--
-- a goallist  is a Term = list of triples
--type GoalList  = Term
--
-- a goal is a triple
--type Goal = Triple
--
-- a DB is a list of clauses (facts are rules with empty right sides)
--type DB = [Clause]
--
-- a prefixlist is a list of prefixes
--type PrefixList = [String]
--
----------------------------------------------------------------------

-- data structure

type DB = [XMLTree]

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

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

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 1  -- number variables starting from 1
         db = (markRules (generateDB axiom))
         varList = eliminateEmpties(eliminateDoubles(getAllVariables db))
         queryDB = markAllVariables querydb [] 1  -- number variables starting from 1
         querydb = (generateDB lemma)
         varList1 = eliminateEmpties (getAllVariables1 (queryDB))

executeProof axiom lemma = putStr (showSubstitutionList
                                 (fst(proof dataBase queryDB))
                                 (varList++varList1))
   where dataBase = markAllVariables db varList 1  -- number variables starting from 1
         db = (markRules (generateDB axiom))
         varList = eliminateEmpties(eliminateDoubles(getAllVariables db))
         queryDB = markAllVariables querydb [] 1  -- number variables starting from 1
         querydb = (generateDB lemma)
         varList1 = eliminateEmpties (getAllVariables1 (queryDB))
                    

-- 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)))

-- The database is a list of clauses and is constituted by the children
-- of the XML tree generated by the module load.

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

-- 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)

-- testdata
testTestTreeT = putStr (fileToXML testTreeT)

testTreeT = loadDB pa7

testTestQuery = putStr (fileToXML testQuery)

testQuery = loadDB pa8

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

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 1  -- number variables starting from 1
   where db = (markRules (generateDB testTreeT))
         varList = (getAllVariables 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
testTriple2 = putStr (fileToXML triple2)
triple2 = getChild(getChild(getChild(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")
testObject1 = putStr (fileToXML object1)
object1 = o
   where [o] = eliminateEmpties(getChildrenByName verb1 "Object")
testObject2 = putStr (fileToXML object2)
object2 = o
   where [o] = eliminateEmpties(getChildrenByName verb2 "Object")
   
testTransformVarlist = putStr (treeListToXML testVarlist1)                            

testVarlist = (eliminateEmpties(eliminateDoubles(getAllVariables
                             (markRules (generateDB (testTreeT))))))
testVarlist1 = eliminateEmpties(markAllVariables testVarlist testVarlist 1)

testVarlistQ1 = eliminateEmpties(getAllVariables1 (markAllVariables
               (generateDB testQuery) [] 1))
testAllVarlist = putStr (treeListToXML allVarlist)
allVarlist = testVarlist1 ++ testVarlistQ1

testUnifyTwoTriples = putStr(showSubstitution (sndTriple
                  (unifyTwoTriples triple1 triple2)) testVarlist1)
testUnifyTwoTriples1 = putStr(fileToXML (thdTriple
                  (unifyTwoTriples triple1 triple2)))

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

testUnifyTwoObjects = putStr(showSubstitution (sndTriple
                  (unifyTwoObjects object1 object2 nullSubst)) testVarlist1)
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"

-- displays a substitution on condition that the substituted
-- variable is in the varlist.
showSubstitution :: Subst -> Varlist -> String
showSubstitution subst [] = ""
showSubstitution subst varlist@(v:vs) 
   | subst v == v = showSubstitution subst vs
   | otherwise = "\nVariable:\n" ++ fileToXML v ++ "\nTerm:\n"
                 ++ fileToXML (subst v) ++ (showSubstitution subst vs)


-- display a list of substitutions
showSubstitutionList :: [Subst] -> Varlist -> String
showSubstitutionList [] varlist = ""
showSubstitutionList (s:ss) varlist = showSubstitution s varlist ++
                                      showSubstitutionList ss varlist

-- 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)

type Varlist = [XMLTree]

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

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

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

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

-- mark the variables in a clause
-- The integer parameter is for numbering anonymous variables
markVariables :: XMLTree -> Varlist -> Int -> XMLTree
markVariables tree varlist i =
   walkATree tree f
      where f (Tag tag@("URI", t, p))
               | startsWith s "_:" = addTree (Tag ("Var", 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
               | otherwise = Tag tag
               where Tag tag1 = Tag ("Var", t, p)
                     Content (s, _) =  getChild (Tag tag)
            f t = t

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))))))

-- 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

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 t = []
         varList = getChildrenByName (Tree tagList) "Var"

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

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

-- 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. See the XML Schema for the XML format
-- (to do !!!)
-- 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

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

-- 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> or <Var>.
-- The second triple is returned modified.
unifyTwoTriples :: XMLTree -> XMLTree -> (Bool, Subst, XMLTree)
unifyTwoTriples t1 t2 = (b1, subst1, t3)
   where -- unify the subjects
         (b, subst) = unifyAtoms t1 t2 nullSubst
         v1 = eliminateEmpties (getChildrenByName t1 "Verb")
         v2 = eliminateEmpties (getChildrenByName 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, _, _) = v3

testSpecial = fst (unifyAtoms (getChild verb1) (getChild verb2) nullSubst)

-- unify two atoms (subject, verb or object). Returns a substitution
-- and a boolean.
-- Possibilities: URI with URI; VAR with URI; VAR with VAR.
unifyAtoms :: XMLTree -> XMLTree -> Subst -> (Bool, Subst)
unifyAtoms Empty _ substIn = (False, nullSubst)
unifyAtoms t1 t2 substIn
   -- this test must be first!!!
   | t3 == t4 = (True, substIn)
   | testTag1 && s1 == "Var" = (True, substIn @@ ((Tag c1) ->- t6))
   | testTag2 && s2 == "Var" = (True, substIn @@ ((Tag c2) ->- t5))
   | otherwise = (False, substIn)
   where t3 = applySubstitution substIn t1
         t4 = applySubstitution substIn t2
         Tag c1@(s1, _, _) = t5
         Tag c2@(s2, _, _) = t6
         testTag1 = testTag t5
         testTag2 = testTag t6
         t5 = getChild t3
         t6 = getChild t4
         testTag (Tag c) = True
         testTag t = False

-- 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 (getChild verb) (getChild v)
          subst
         [verb] = v1
         -- get the objectlist
         o1 = eliminateEmpties (getChildrenByName verb "Object")
         o2 = eliminateEmpties (getChildrenByName 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, _, _) = o3

-- unify two "object"trees. 
unifyObjects :: [XMLTree] -> [XMLTree] -> Subst -> (Bool, Subst, XMLTree)
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
         (bool, subst, o3) = unifyTwoObjects object o substIn
         [object] = o1
         -- failure; search further
         (bool1, subst1, o2) = unifyObjects o1 os substIn


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

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

-- 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
   | (markedTags /= []) && (markedTags1 /= [])
                 = (False, nullSubst, t2) -- return unmodified object
   | testTag2 && s2 == "Var" = (True, substIn @@ ((Tag c2) ->- t5),
                               addTree t3 marked)
   | testTag1 && s1 == "Var" = (True, substIn @@ ((Tag c1) ->- t6),
                               addTree t4 marked)
   | t3 == t4 = (True, substIn, addTree t2 marked)
   | otherwise = (False, substIn, t2) -- return unmodified object
   where t3 = applySubstitution substIn t1
         t4 = applySubstitution substIn t2
         t5 = getChild t3
         t6 = getChild t4
         Tag c1@(s1, _, _) = t5
         Tag c2@(s2, _, _) = t6
         testTag1 = testTag t5
         testTag2 = testTag t6
         -- test if already marked
         markedTags =  eliminateEmpties (getChildrenByName t1 "mark")
         markedTags1 = eliminateEmpties (getChildrenByName t2 "mark")
         -- test if this is a tag
         testTag (Tag c) = True
         testTag t = False

marked = Tag ("mark", Empty, Empty)

-- 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 -> Varlist -> String
showStack [] varlist = []
showStack ((s, g, l):xs) varlist = "STACK:\n " ++ "Substitution: " ++
          (showSubstitution s varlist) ++ "\n" ++ "Goals: "
          ++ (treeListToXML g) ++ "\n" ++ "Alts: " ++ (showAlts l varlist)

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

-- show an alternative
showAlt alt@(treeList, subst) varlist =
   treeListToXML treeList ++ showSubstitution subst varlist ++ "\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)

testProof = stringToFile ("Subst: \n" ++ (showSubstitutionList subst varlist)
                    ++ "\nDebug info:\n" ++ string) "testProof.tst"
    where (subst, string) = proof testDB testQueryDB
          varlist = testVarlist1 ++ testVarlistQ1

-- 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 a string that contains information if the verbose flag is set.
-- the query is the initial goallist.
proof :: [XMLTree] -> [XMLTree] -> ([Subst], String)
proof db query = solve str nullSubst query [] 0
   where
      solve :: String -> Subst -> [XMLTree] -> Stack -> Int
                            -> ([Subst], String)
      -- 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 s subs [] stack n =   (subs:sub, s1)
            where (sub, s1) = backtrack s stack (n+1)
      -- search a solution for the goal at the top of the goallist.
      solve s subs goals stack n
         | n > 20 = ([subs], s1)
         | bv1 = solve s subs [] stack n
         | otherwise = choose s1 subs gs1 (getAlts db (app subs g1))
                                      stack (n+1)
             where s1 = s ++ testVerbose ("solve:\n" ++ treeListToXML (g1:gs1)
                                            ++ "\n")
                   goalList = checkGrounded goals
                   bv1 = goalList == []
                   gl@(g1:gs1) = goalList

      -- choose an alternative                 
      choose :: String -> Subst -> [XMLTree] -> ([Alt], String) -> Stack
                         -> Int -> ([Subst], String)
      -- the list of alternatives is empty; backtrack to
      -- the last list of alternatives 
      choose s subs gs ([],_)  stack n = backtrack s1 stack (n+1)
                           where s1 = s ++ ""
      -- 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 s subs gs (altList, altS) stack n
         = solve s1 (sub@@subs) (tree ++ gs) ((subs,gs,alts):stack) (n+1)
         where s1 = s ++ testVerbose ("choose:\n" ++ showAlts
                      altList allVarlist ++ altS ++ "\n")
               al@((tree,sub):alts) = altList

      -- If a goal fails then retrieve the last saved situation from
      -- the stack.
      backtrack :: String -> Stack -> Int -> ([Subst], String)
      -- stack is empty; nothing to backtrack.
      backtrack s [] n = ([],s)
      backtrack s stack n  
         = choose s1 subst goals (alts, "")  sts (n+1)
         where s1 = s ++ "\n\nBacktrack:\n\n" 
               st@((subst, goals, alts):sts) = stack

str = testVerbose "Start of proof:"

checkGrounded :: [XMLTree] -> [XMLTree]
checkGrounded [] = []
checkGrounded (x:xs)
   | t == [] = checkGrounded xs
   | otherwise = x:checkGrounded xs
   where t = getChildrenByName x "Var"

-- if the verbose flag is True then the string that is input is output
-- else an empty string is returned
testVerbose :: String -> String
testVerbose s
   | verbose = s
   | otherwise = []

-- 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 is the rename level. Output is a list of alternatives
-- consisting of pairs that contain a clause and a substitution:
-- type Alt = (XMLTree, Subst).
getAlts :: [XMLTree] -> XMLTree -> ([Alt], String)
getAlts [] t = ([], "")
getAlts (x:xs) t 
   | bv1 && bool = ([(eliminateEmpties goals, subst)] ++ alts, s2 ++ s1)
   | (not bv1) && bool1 = ([([t], subst1)] ++ alts, s2 ++ s1)
   | otherwise = getAlts xs t 
   where Tag (s, _, _) = x
         bv1 = s == "Rule"
         -- unify with a rule
         (bool, subst, t1, goals) = unifyWithRule t x
         -- unify with a triple
         (bool1, subst1, t2) = unifyTwoTriples t x
         (alts, s1) = getAlts xs t
         s2 = "\n alt tag = " ++ s ++ "\n"

testGetAlts =
   stringToFile (showAlts (fst(getAlts testDB x)) varlist) "testGetAlts.tst"
      where (x:xs) = testQueryDB
            varlist = testVarlist1 ++ testVarlistQ1

-- Example data
------------------


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

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

verbose = True

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

impliesURI = swaplog ++ "#implies"

varURI = swaplog ++ "#forAll"