import "N3Parser"
import "IO"
import "Utils"

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

-- 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 (SubstVar v)            = s v
app s (SubstURI u)            = SubstURI u
--app s (Term t)
--    | TripleList x:xs
--    | TermList y:ys

nullSubst               :: Subst
nullSubst v              = SubstVar v

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

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

data Substituted= SubstVar Var|
                  SubstURI URI|
                  SubstTerm Term|
                  SubstNull

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

-- null property
nullP = (VerbNull, [ObjectTerm TermNull])

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

instance Eq Atom  
   where
      URI (s, s1) == URI (s2, s3) = (s == s2) && (s1 == s3)
      Var (s1, s2, n) == Var (s3, s4, n1) = (s1 == s3) && (s2 == s4)
                         && (n == n1)
      AtomNull == AtomNull = True
      _ == _ = False

instance Eq Subject
   where
      (SubjectAtom a1) == (SubjectAtom a2) = a1 == a2
      SubjectNull == SubjectNull = True
      _ == _ = False

instance Eq Verb
   where
      (VerbAtom a1) == (VerbAtom a2) = a1 == a2
      VerbNull == VerbNull = True
      _ == _ = False

instance Eq Object
   where
      (ObjectAtom a1) == (ObjectAtom a2) = a1 == a2
      ObjectNull == ObjectNull = True
      _ == _ = False

-- 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 variablelist of kind 1 is a globals list (see Utils.hs)
type VarList = Globals

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

-- access the data structure
-- The string defines the tag of which a list is wanted
-- access is done on the clause level
accessL :: Clause -> String -> [a]

-- returns a sequence of all tags in a clause
accessS :: Clause -> [a]

-- display functions
---------------------------

-- show an atom
showAtom :: Atom -> String
showAtom (URI (s1, s2)) = " URI: (" ++ s1 ++ ", " ++ s2 ++ ") "
showAtom (Var (s1, s2, n)) = "VAR: (" ++ s1 ++ ", " ++ s2 ++ ", " ++ show n
                              ++") "
showAtom (AtomNull) = ""

-- show a subject
showSubject :: Subject -> String
showSubject (SubjectAtom atom) = "Subject: " ++ showAtom atom
showSubject (SubjectTerm term) = "Subject: " ++ showTerm term
showSubject SubjectNull = "SubjectNull"

-- show a verb
showVerb :: Verb -> String
showVerb (VerbAtom atom) = "Verb: " ++ showAtom atom
showVerb (VerbTerm term) = "Verb: " ++ showTerm term
showVerb VerbNull = "VerbNull"

-- show an object
showObject :: Object -> String
showObject (ObjectAtom atom) = "Object: " ++ showAtom atom
showObject (ObjectTerm term) = "Object: " ++ showTerm term
showObject ObjectNull = "ObjectNull"

-- show an ObjectList
showObjectList :: [Object] -> String
showObjectList [] = " End of ObjectList "
showObjectList (x:xs) = showObject x ++ showObjectList xs

-- show a property
showProperty :: Property -> String
showProperty (v, ol) = " Property:  " ++ showVerb v ++ " ObjectList: " ++
                       showObjectList ol

-- show a propertyList
showPropertyList :: [Property] -> String
showPropertyList [] = " End of PropertyList "
showPropertyList (x:xs) = showProperty x ++ showPropertyList xs

-- show a triple
showTriple :: Triple -> String
showTriple (s, pl) = " Triple: " ++ showSubject s ++ " PropertyList: " ++
                       showPropertyList pl

-- show a triplelist
showTripleList :: [Triple] -> String
showTripleList [] = " End of TripleList "
showTripleList (x:xs) = showTriple x ++ showTripleList xs

-- show a variable
showVariable :: Var -> String
showVariable (s1, s2, n) = "Var(" ++ s1 ++ ", " ++ s2 ++ ", " ++
                            show n ++ ") "

-- show a variablelist
showVariableList :: [Var] -> String
showVariableList [] = " End of variable list "
shiwVariableList (x:xs) = showVariable x ++ showVariableList xs


-- show a term
showTerm :: Term -> String
showTerm (TripleList t) = "Term: " ++ showTripleList t
showTerm (TermList t) = "TermList: " ++ showTermList t
showTerm (Triple t) = "Term: " ++ showTriple t
showTerm TermNull = "TermNull "

-- show a termlist
showTermList :: [Term] -> String
showTermList [] = " End of TermList "
showTermList (x:xs) = showTerm x ++ "\n     " ++ showTermList xs

-- show a clause
showClause :: Clause -> String
showClause (t1, t2) = " Clause: (" ++ showTerm t1 ++ ", " ++
                        showTerm t2 ++ ") "

-- show the contents of the stack
--showStack [] = []
--showStack ((v, g, l):xs) = "STACK " ++ showVariableList v ++ " **** " ++
--          showTripleList g ++ " **** " ++ showDB l
--          ++ "////  " ++ showStack xs

-- show a db
showDB :: [Clause] -> String
showDB [] = " EndOfDB"
showDB (x:xs) = showClause x ++ "\n\n" ++ showDB xs 

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

-- read a parsed file, load it and print the result
saveEngine fileName = readExternN3 fileName (loadAndSave fileName)

--
saveVars fileName = readExternN3 fileName (testGetVars fileName)

-- loadFile loads a file into the data structures
loadAndSave :: String -> String -> IO ()
loadAndSave fileName parseString = stringToFile (showDB (thdTriple
             (loadString (parseString, plist, db)))) (fileName ++ ".ld")

-- loadFile loads a file into the data structures
testGetVars :: String -> String -> IO ()
testGetVars fileName parseString = stringToFile ((showDB (fst(result))) ++
                                   show(snd(result)))
                                  (fileName ++ ".tv")
   where result = genLogic
                  (splitDB(thdTriple
                  (loadString (parseString, plist, db))), varlist)

-- read a parsed file and load it
-- type??
readEngine fileName  = readExternN3 fileName loadFile

-- loadFile loads a file into the data structures
loadFile :: String -> IO ()
loadFile parseString = putStr (showDB (thdTriple (loadString
                         (parseString, plist, db))))
  -- putStr (fstTriple (loadString (parseString, plist, db)))

--  get elements of a quadruple
fstTriple (a, b, c) = a
thdTriple (a, b, c) = c

testLoadString = showDB (thdTriple (loadString (pa1, plist, db)))

-- this function creates the datastrucure
loadString :: (String, PrefixList, DB) ->
              (String, PrefixList, DB)
loadString ([], p, db) = ([], p, db)
loadString (s, p, db)
   | token == "Prefix" = loadString (s2, p ++ [token1], db)
   | token == "Subject" = loadString (s3, p, db ++ [(TripleList [t],TermNull)])
   | token == "Set" = loadString (s4, p, db ++ [(te,TermNull)])
   | token == "AnonSet" = loadString (s4, p, db ++ [(te,TermNull)])
   | otherwise = (s, p, db)
   where
      (token, s1) = getNextToken ("", s)
      (token1, s2) = getNextToken ("", s1)  -- get the prefix
      (s3, t) = loadTriple s
      (s4, te) = loadTerm (s3, merge (TermList []) (TripleList [t]))

testLoadTerm1 =  fst (loadTerm (pa5, TermList[]))
testLoadTerm2 = showTerm(snd(loadTerm (pa5,TermList[])))

-- load a term next token might be Set || AnonSet || Subject || EndOfSet
-- otherwise loadTriple
-- If Set then create a TermList
loadTerm :: (String, Term) -> (String, Term)
loadTerm (s, t)
   | token == "Set" = (s3, t2) 
   | token == "AnonSet" = (s3, t2)
   | token == "Subject" = (s5, t4)
   | token == "EndOfSet" = (s1, t)       -- return on EndOfSet
   | otherwise = (s, t)  -- this is not a term
   where
      (token, s1) = getNextToken ("", s)
      (s3, t2) = loadTerm (s4, merge t (TripleList [t3]))
      (s2, t1) = loadTriple s
      (s5, t4) = loadTerm (s2, merge t (TripleList [t1]))
      (s4, t3) = loadTriple s1

merge (TermList t1) (TermList t2) = TermList (t1 ++ t2)
merge (TermList t1) (TripleList t2) = TermList (t1 ++ [TripleList t2])

testLoadTriple = showTriple (snd (loadTriple pa1))

testLoadAnonSet = showTerm (snd (loadTerm (pa4, TermList [])))

-- load a triple; load the subject and a propertylist.
loadTriple :: String -> (String, Triple)
loadTriple s
   | token == "Subject" = (s3, (sub, p))
   | token == "Set" = (s3, (sub, p))
   | otherwise = (s, (SubjectNull, []))  
   where
      (token, s1) = getNextToken ("", s)
      (s2, sub) = loadSubject s
      (s3, p) = loadPropertyList (s2, [])

testLoadPropertyList = showPropertyList (snd (loadPropertyList (pa3, [])))

-- load a propertylist
loadPropertyList :: (String, PropertyList) -> (String, PropertyList)
loadPropertyList ([], p) = ([], p)
loadPropertyList (s, p) 
      | token == "_subject" =  loadPropertyList (s2, p ++ [p1])
      | otherwise = (s1, p ++ [p1])
      where
         (s1, p1) = loadProperty s
         (token, s2) = getNextToken ("", s1)

-- load a property
-- the next token might be: Verb || _subject
loadProperty :: String -> (String, Property)
loadProperty s
      | token == "Verb" =  (s5, (v1, n))
      | token == "_subject" = (s6, (v2, n1))   -- necessary??
      | otherwise = (s, (VerbNull, []))     
      where
        (token, s1) = getNextToken ("", s)
        (s5, n) = loadObjectList (s3, [])
        (s6, n1) = loadObjectList (s4, [])
        (s3, v1) = loadVerb s
        (s4, v2) = loadVerb s1

testLoadObjectList = map showObject (snd(loadObjectList (pa2, [])))

-- load an objectlist
loadObjectList :: (String, ObjectList) -> (String, ObjectList)
loadObjectList ([], o) = ([], o)
loadObjectList (s, o)
      | token == "_subject" && token1 == "_verb"
                     = loadObjectList (s3, o ++ [o1])
      | otherwise = (s1, o ++ [o1])
      where
         (s1, o1) = loadObject s
         (token, s2) = getNextToken ("", s1)
         (token1, s3) = getNextToken ("", s2)

-- load a subject
-- the next token might be: Subject || Set || AnonSet
loadSubject :: String -> (String, Subject)
loadSubject [] = ([], SubjectNull)
loadSubject s
      | token == "Subject" =  (s3, SubjectAtom (URI (token1, token2)))
      | token == "Set" = (s4, SubjectTerm t1)
      | token == "AnonSet" = (s4, SubjectTerm t1)
      | otherwise = (s, SubjectNull)
      where
        (token, s1) = getNextToken ("", s)
        (token1, s2) = getNextToken ("", s1)
        (token2, s3) = getNextToken ("", s2)
        (s4, t1) = loadTerm (s, TermList [])

-- load a verb
-- the next token might be: Verb || _subject || Set || AnonSet
loadVerb :: String -> (String, Verb)
loadVerb [] = ([], VerbNull) 
loadVerb s
      | token == "Verb" =  (s3, VerbAtom (URI (token1, token2)))
      | token == "_subject" = (s4, VerbAtom (URI (token2, token3)))
      | token == "Set" = (s5, VerbTerm t1)
      | token == "AnonSet" = (s5, VerbTerm t1)
      | otherwise = (s, VerbNull)      
      where
        (token, s1) = getNextToken ("", s)
        (token1, s2) = getNextToken ("", s1)
        (token2, s3) = getNextToken ("", s2)
        (token3, s4) = getNextToken ("", s3)
        (s5, t1) = loadTerm (s, TermList [])

-- load an object
-- the next token might be: Object || _subject
loadObject :: String -> (String, Object)
loadObject [] = ([], ObjectNull)
loadObject s
      | token == "Object" =  (s3, ObjectAtom (URI (token1, token2)))
      | token == "_subject" && token1 == "_verb"
                  = (s5, ObjectAtom (URI (token3, token4)))
      | token == "Set" = (s6, ObjectTerm t1)
      | token == "AnonSet" = (s6, ObjectTerm t1)
      | otherwise = (s, ObjectNull)
      where
        (token, s1) = getNextToken ("", s)
        (token1, s2) = getNextToken ("", s1)
        (token2, s3) = getNextToken ("", s2)
        (token3, s4) = getNextToken ("", s3)
        (token4, s5) = getNextToken ("", s4)
        (s6, t1) = loadTerm (s, TermList [])

-- getNextToken returns the next token and the rest string
-- is normally called with first string empty
getNextToken :: (String, String) -> (String, String)
getNextToken ([], []) = ([], [])
getNextToken (s, []) = (s, [])
getNextToken (s1, s2@(x:xs))
   | startsWith s2 "/@/" = (s1, drop 3 s2)
   | otherwise = getNextToken (s1 ++ [x], xs)

-- split lists of terms in DB into single terms. The second term is
-- still always null. Split TripleList into single Triple.
splitDB :: DB -> DB
splitDB [] = []
splitDB (((TermList (z:zs)),t):xs) =
   splitTripleList(z, t) ++ splitDB (((TermList zs), t):xs)
splitDB (x@((TripleList t), t1):xs) = splitTripleList(x) ++ splitDB xs
splitDB (x:xs) = x : splitDB xs

splitTripleList :: Clause -> [Clause]
splitTripleList (TripleList [],_) = []
splitTripleList (TripleList (x:xs),t) = (Triple x, t):
                      splitTripleList (TripleList xs, t)
splitTripleList (t1, t) = [(t1,t)]

-- generate a list of variables and split the rules into one or
-- more pairs of terms.
-- detect log:implies and log:forAll and log:forSome
-- All triplelists contain only one triple now, but can
-- contain several after the rule split.
genLogic :: (DB, Globals) ->  (DB, Globals)
genLogic ([], varlist) = ([], varlist)
genLogic ((x:xs), varlist) = mergeDB(z, genLogic (xs, varlist2))
    where  z@(c, varlist2) = genLogicClause (x, varlist)  
           mergeDB ((c1, varlist3), (db1, varlist4)) = (c1:db1, varlist4)

testGenLogic = snd(genLogic (dbt, varlist))

-- get the variables in a clause and split the rules
-- In input the clause contains a single triple
genLogicClause :: (Clause, Globals) -> (Clause, Globals)
genLogicClause (c@(Triple t, t2), varlist) = (clause, varlist1)
   where varlist1 = getVariablesFromTripleList ([t], varlist)
         clause = splitRuleInTriple c
genLogicClause (c, varlist) = (c, varlist)

testGenLogicClause = showClause(fst (result)) ++  show(snd(result))
   where result =  genLogicClause (cl2, varlist)

-- here I assume that the verb "log:forAll" is not in a nested structure.
getVariablesFromTripleList ([], varlist) = varlist
getVariablesFromTripleList ((t:ts), varlist) =
   getVariablesFromTripleList (ts, getVariablesFromTriple (t, varlist))
   where      
         getVariablesFromTriple ((s, pl), varlist) =
            getVariablesFromPropertyList (pl, varlist)
         getVariablesFromPropertyList ([], varlist) = varlist
         getVariablesFromPropertyList ((t:ts), varlist) =
            getVariablesFromPropertyList (ts,
                getVariablesFromProperty (t, varlist))
         getVariablesFromProperty (t1@((VerbAtom (URI (u1, u2))), o), varlist)
            | u2 == swaplog ++ "#forAll" =
                        getVariablesFromObjectList (o, varlist)
            | otherwise = varlist
         getVariablesFromProperty (t, varlist) = varlist
         getVariablesFromObjectList ([], varlist) = varlist
         getVariablesFromObjectList ((o:os), varlist) =
             getVariablesFromObjectList (os,
                getVariableFromObject (o, varlist))
         getVariableFromObject (o1@((ObjectAtom (URI (u1, u2)))), varlist) =
            setStringParam varlist u2 u1
         getVariableFromObject (o1, varlist) = varlist

testGetVariablesFromTripleList =
         (getVariablesFromTripleList ([t4], varlist))

-- here I assume that the verb "log:implies" is in a rule structure
-- following the rule bnf given higher.
splitRuleInTriple ::  Clause -> Clause
splitRuleInTriple cl@(Triple t@((SubjectTerm t1), pl), t2)
   | v == VerbNull = cl
   | otherwise = c
   where
        (v, [(ObjectTerm t3)]) = getProperty pl impliesURI
        c = (Triple t, t3)

testSplitRuleInTriple = showClause (splitRuleInTriple (Triple t4, TermNull))

-- get a property from a propertylist with a specified verb
getProperty :: PropertyList -> String -> Property
getProperty [] _ = nullP
getProperty pl@(p:ps) s
    | u2 == s = p
    | otherwise = getProperty ps s
    where (v, ol) = p
          VerbAtom (URI (u1, u2)) = v

testGetProperty = showProperty (getProperty pl2 impliesURI)

-- testdata

t :: Triple
t = (s, [(v, [o])])

te :: Term
te = Triple t

cl :: Clause
cl = (te, TripleList [])
cl1 = (Triple t3, TripleList [])
cl2 = (Triple t4, TripleList [])

dbt = [cl, cl2]

s = SubjectAtom (URI (":c",":c"))
s1 = SubjectAtom (URI (":c1",":c1"))
v = VerbAtom (URI (":a",":a"))
v1 = VerbAtom (URI (":a1",":a1"))
o = ObjectAtom (URI (":b",":b"))
o1 = ObjectAtom (URI (":b1",":b1"))
o2 = ObjectAtom (URI (":b11",":b12"))

ol = [o,o1]
ol1 = [o1, o]
ol2 = [o1, o2]

po = (v, ol)
po1 = (v1, ol1)
pl = [po1, po]
pl1 = [po, po1]
pl2 = [(VerbAtom (URI ("log:implies", impliesURI)),
      [ObjectTerm (Triple t2)])]
pl3 = [(VerbAtom (URI ("log:implies", impliesURI)),
      [ObjectTerm (Triple t2)]),
      (VerbAtom (URI ("log:forAll", varURI)),
      ol2)]

t1 = (s, pl)
t2 = (s1, pl1)
t3 = (SubjectTerm (Triple t1), pl2)
t4 = (SubjectTerm (Triple t1), pl3)

-- test unification takes as input two triples and returns a truth value
--testUnify :: Triple -> Triple -> Bool
--testUnify TripleNull TripleNull = False
--testUnify TripleNull t2 = False
--testUnify t1 TripleNull = False
--testUnify (Triple s1 v1 o1) (Triple s2 v2 o2) =
--   (testUnifyTerm s1 s2)&&(testUnifyTerm v1 v2)&&(testUnifyTerm o1 o2)

-- unification takes as input two triples and produces a most general triple 
--unify :: Triple -> Triple -> Triple
--unify TripleNull TripleNull = TripleNull
--unify TripleNull t2 = t2
--unify t1 TripleNull = t1
--unify (Triple s1 v1 o1) (Triple s2 v2 o2) =
--   Triple (unifyTerm s1 s2) (unifyTerm v1 v2) (unifyTerm o1 o2)
                                                       
-- testUnifyTerm test the unification of two terms
--testUnifyTerm :: Term -> Term -> Bool
--testUnifyTerm (Term (Vari (v,g,l))) t = True
--testUnifyTerm t (Term (Vari (v,g,l))) = True
--testUnifyTerm (Term (Uri u1)) (Term (Uri u2))
--   | u1 == u2 = Tr
--   | otherwise = False

-- unifyTerm unifies two terms and returns a most general term
--unifyTerm :: Term -> Term -> Term
--unifyTerm (Term (Vari (v,g,l))) t = (Term (Vari (v,g,l ++ [t])))
--unifyTerm t (Term (Vari (v,g,l))) = (Term (Vari (v,g,l ++ [t])))
--unifyTerm (Term (Uri u1)) (Term (Uri u2)) = Term NullAtom

-- a proof has as input the database of clauses and a query
-- the output is a list of variables with the substitutions
-- the query is the initial goallist
-- returns the solution, 
-- and a string for verbose information
--proof :: [Rule] -> Query -> ([Var], String)
--proof db query = solve str 1 [] query []
--   where
--      solve :: String -> Int -> [Var] -> [Triple] -> Stack -> ([Var], String)
--      solve s n vars [] stack = (vars ++ x1, x2)
--            where (x1, x2) = backtrack s n stack
--      solve s n vars (g:gs) stack = choose s1 n vars1 gs (getAlts db g n) stack
--            where vars1 = nubVar (getVarsTriple g)
--                  s1 = s ++ "solve "
--                  
--      choose :: String -> Int -> [Var] -> [Triple] -> [Alts] -> Stack -> ([Var], String)
--      choose s n vars gs [] stack = backtrack s1 n stack
--                           where s1 = s ++ ""
--      choose s n vars gs (y:ys) stack =   
--                           solve s1 (n+1) (nubVar ((getVarsTriple x)
--                           ++ (getVarsTripleList xs)))
--                           (gs ++ xs) ((vars,gs,ys):stack)
--                           where (x,xs) = y
--                                 s1 = s ++ "choose "
--
--      backtrack :: String -> Int -> Stack -> ([Var], String)
--      backtrack s n [] = ([],s)
--      backtrack s n ((vars,gs,ys):stack) = choose s1 (n-1) (derefVarList vars n)
--                                              gs ys stack
--                                           where s1 = s ++ showStack stack 
--      str = testVerbose "Start of proof:"

-- 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 = []

--testProof = (showVariableList x1) ++ x2
--            where (x1, x2) = proof db q1

--getVars :: Rule -> [Var]
--getVars (t, l) = getVarsTriple t ++ getVarsTripleList l

-- get the variables in a triple
--getVarsTriple :: Triple -> [Var]
--getVarsTriple (Triple s v o) =  getVarsTerm s ++ getVarsTerm v ++ getVarsTerm o

-- get the variables in a triplelist
--getVarsTripleList :: [Triple] -> [Var]
--getVarsTripleList [] = []
--getVarsTripleList (x:xs) = getVarsTriple x ++ getVarsTripleList xs

-- get the variables in a term
--getVarsTerm :: Term -> [Var]
--getVarsTerm (Term (Vari v)) = [v]
--getVarsTerm t = []

-- get the variables in a term list 
--getVarsTermList :: [Term] -> [Var]
--getVarsTermList [] = []
--getVarsTermList (x:xs) = getVarsTerm x ++ getVarsTermList xs


-- dereferences a variable after a backtrack
--derefVar :: Var -> Int -> Var
--derefVar (s, i, l) n = (s, i, derefTermList l n)

-- deref the variable in a term
--derefTerm :: Term -> Int -> Term
--derefTerm (Term (Vari v)) n = (Term (Vari (derefVar v n)))
--derefTerm t n = t

--derefTermList :: [Term] -> Int -> [Term]
--derefTermList [] n = [] 
--derefTermList (x:xs) n = derefTerm x n : derefTermList xs n

-- dereferences a variable list after a backtrack 
--derefVarList :: [Var] -> Int -> [Var]
--derefVarList [] n = []
--derefVarList ((s, i, l):xs) n
--   | i == n = derefVarList xs n
--   | otherwise = derefVar (s, i, l) n : derefVarList xs n

-- match a goal with the database
-- This returns a GoalList or []
-- where GoalList is a list of goals and [Alts] is a list of alternatives.
-- type Alts = Rule
--matchDB :: DB -> Triple -> Int -> (GoalList, [Alts])
--matchDB (x:xs) t n 
--   | bv1 = (y2, getAlts xs t n+1)
--   | otherwise = matchDB xs t n
--   where bv1 = testUnifyRule x t
--         (y1, y2) = x

-- get the list of matches of a triple with the heads in the database
-- unify , rename and copy the variables
-- this is the kernel of the resolution engine 
--getAlts :: [Rule] -> Triple -> Int -> [Alts]
--getAlts [] t n = []
--getAlts (x:xs) t n
--   | bv1 = [(renameTriple y3 n, ts)] ++ (getAlts xs t n)
--   | otherwise = getAlts xs t n
--   where bv1 = testUnifyRule x t
--         (y1, y2) = x                -- the first rule in the database
--         y3 = unify y1 t             -- unify the triple with the head of the rule
--         ys = renameTripleList y2 n  -- rename this list
--         ts = copyVars y3 ys

--copyVars :: Triple -> [Triple] -> [Triple]
--copyVars t [] = []
--copyVars t (x:xs) = copyTripleVars t x: copyVars t xs

--copyTripleVars :: Triple -> Triple -> Triple
--copyTripleVars t (Triple s v o) = Triple (copyTermVars t s) (copyTermVars t v)
--                                         (copyTermVars t o)

--copyTermVars :: Triple -> Term -> Term
--copyTermVars (Triple s ve o) t =
--    (copyTermTerm s (copyTermTerm ve (copyTermTerm o t)))
--copyTermVars t term = term

--copyTermTerm (Term (Vari (s, n, l))) (Term (Vari (s1, n1, l1)))
--   | s == s1 = (Term (Vari (s, n, l)))
--   | otherwise = (Term (Vari (s1, n1, l1)))
--copyTermTerm t1 t2 = t2

-- checks if a variable is present in this triple
--checkVar :: Triple -> Var -> Bool
--checkVar (Triple s ve o) v = (checkTerm s v)&&(checkTerm ve v)&&(checkTerm o v)

-- checks if a term contains the same variable name as the input variable
--checkTerm :: Term -> Var -> Bool
--checkTerm (Term (Vari (s, n, l))) (s1, n1, l1) = s == s1
--checkTerm t v = False

--testGetAlts =
--   showDB (getAlts db q3 1)

--testUnifyRule :: Rule -> Triple ->  Bool
--testUnifyRule (t,l) t1  = testUnify t t1

-- rename the variables in a triple
--renameTriple :: Triple -> Int -> Triple
--renameTriple (Triple s v o) n = Triple  ((renameTerm s) n) ((renameTerm v) n)
--                                        ((renameTerm o) n)

-- rename the variables in a triple list
--renameTripleList :: [Triple] -> Int -> [Triple]
--renameTripleList [] n = []
--renameTripleList (x:xs) n = renameTriple x n : renameTripleList xs n


-- The integer value of the variables is set to the integer parameter
--renameVars :: Triple -> Int -> Triple
--renameVars (Triple s v o) n  =
--   Triple ((renameTerm s) n) ((renameTerm v) n) ((renameTerm o) n)

-- rename the variables in a term
--renameTerm :: Term -> Int -> Term
--renameTerm (Term (Vari (v,i,l))) n = (Term (Vari (v, n, renameTermList l n)))
--renameTerm t n = t

--renameTermList :: [Term] -> Int -> [Term]
--renameTermList [] n = []
--renameTermList (x:xs) n  = (renameTerm x n):renameTermList xs n

-- remove duplicate variables from list
--nubVar :: [Var] -> [Var]
--nubVar []            = []
--nubVar (x:xs)        = x : nubVar (filter (notEqualVar x) xs)

--notEqualVar :: Var -> Var -> Bool
--notEqualVar (s, n, l) (s1, n1, l1
--   | s == s1 && n == n1 = False
--   | otherwise = True

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

-- unify test
--t1 = Triple x1 (Term (Uri uri1)) x2
--t2 = Triple x3 x4 (Term (Uri uri2))

--x1 = Term (Vari ("X1", 0, []))
--x2 = Term (Vari ("X2", 0, []))
--x3 = Term (Vari ("X3", 0, []))
--x4 = Term (Vari ("X4", 0, []))

--uri1 = "http://test1"
--uri2 = "http://test2"

--t3 = Triple (Term (Uri "lloyd")) (Term (Uri "lecturer"))
--            (Term (Uri "csc3030"))
--t4 = Triple (Term (Uri "csc3030")) (Term (Uri "content"))
--            (Term (Uri "haskell"))
--t5 = Triple (Term (Uri "csc3030")) (Term (Uri "content"))
--            (Term (Uri "prolog"))
      
--r1 =(Triple x1 (Term (Uri "teaches")) x3,
--            [Triple x1 (Term (Uri "lecturer"))
--              x2, Triple x2 (Term (Uri "content")) x3])

--q1 = [Triple (Term (Uri "lloyd")) (Term (Uri "teaches")) x4]

--q2 = Triple (Term (Uri "csc3030")) (Term (Uri "content")) x4

--q3 = Triple x1 (Term (Uri "teaches")) x3

--db = [(t3, []), (t4, []), (t5, []),
--     r1]

pa1 = "Subject/@/<mailto:jos.deroo.jd@belgium.agfa.com>/@/" ++
     "mailto:jos.deroo.jd@belgium.agfa.com/@/Verb/@/:member/@/" ++
     "<http://www/w3.org#member>/@/Object/@/<http://www.agfa.com>" ++
     "/@/http://www.agfa.com/@/"

-- test loadObjectList
pa2 = "Object/@/<http://www.agfa.com>/@/http://www.agfa.com/@/_subject" ++
       "/@/_verb/@/Object/@/<http://gn>/@/http://gn/@/Subject/@/"

-- test loadPropertyList
pa3 = "Verb/@/:member/@/" ++
     "<http://www/w3.org#member>/@/Object/@/<http://www.agfa.com>" ++
     "/@/http://www.agfa.com/@/" ++ "_subject/@/Verb/@/:test/@/hp:test/@/" ++
     "Object/@/:ok/@/ok:ok/@/"

-- test AnonSet
pa4 = "AnonSet/@/Subject/@/_T1/@/_T1/@/Verb/@/a/@/rdf:type/@/Object/@/agg:Company"
      ++ "/@/http://example.com/xmlns/aggregation-demo#Company/@/" 
      ++ "_subject/@/Verb/@/agg:corporateHomepage/@/" ++
      "http://example.com/xmlns/aggregation-demo#corporateHomepage/@/" ++
      "Object/@/<http://megacorp.example.com/>/@/" ++
      "http://megacorp.example.com//@/_subject/@/Verb/@/agg:name/@/" ++
      "http://example.com/xmlns/aggregation-demo#name/@/Object/@/" ++
      "MegaCorp Inc./@/MegaCorp Inc./@/_subject/@/Verb/@/agg:owner/@/" ++
      "http://example.com/xmlns/aggregation-demo#owner/@/Object/@/agg:gn" ++
      "/@/agg:gn/@/EndOfSet/@/"

-- test embedded sets
pa5 = "Set/@/Set/@/Subject/@/:t/@/:t/@/Verb/@/:v/@/:v/@/Object/@/:o/@/:o" ++
      "/@/Subject/@/:t1/@/:t1/@/Verb/@/:v1/@/:v1/@/Object/@/:o1/@/:o1/@/" ++
      "EndOfSet/@/Verb/@/:v2/@/:v2/@/Object/@/:o2/@/:o2/@/EndOfSet/@/"
-- constants
--------------------

-- the unloaded database
db = []

-- the unloaded list of prefixes
plist = []

-- the unloaded list of variables
varlist :: Globals
varlist = []

verbose = True

an = AtomNull

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

impliesURI = swaplog ++ "#implies"

varURI = swaplog ++ "#forAll"