import "N3Parser" import "IO" import "Utils" import "XML" import "Load" -- 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 :: "" -- objectTruth :: "" -- verbforall :: "" -- 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: name1 name2 integer -- 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 = app s (Tree list) where list = getChildrenByName t "Var" -- get the list of variables -- apply the substitution to a list of variables app s (Tree (x:xs)) =Tree ([app s (Tree xs)] ++ [app s x]) app s t = Empty nullSubst :: Subst nullSubst v = v --(->-) :: Var -> Substituted -> Substituted (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 -- show the contents of the stack --showStack [] = [] --showStack ((v, g, l):xs) = "STACK " ++ showVariableList v ++ " **** " ++ -- showTripleList g ++ " **** " ++ showDB l -- ++ "//// " ++ showStack xs -- 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 ---------------- -- 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 testTree)) "testGenerateDB" -- generate the database from the XML tree generateDB :: XMLTree -> [XMLTree] generateDB db = t where Tree t = getChildren db --saveVars fileName = readExternN3 fileName (testGetVars fileName) -- testdata testTestTree = putStr (fileToXML (loadDB pa7)) testTree = loadDB pa7 testMarkRules = stringToFile (treeListToXML (markRules (generateDB( testTree)))) "testMarkRules" testGetAllTags = stringToFile (showXMLlist (getAllTags testTree)) "testGetAllTags" -- 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] testGetAllVariables = putStr (treeListToXML (getAllVariables (markRules (generateDB (testTree))))) -- get the list of variables getAllVariables :: DB -> VarList getAllVariables [] = [] getAllVariables (x:xs) = (getVariables x) ++ (getAllVariables xs) -- get the variables from a rule getVariables :: XMLTree -> [XMLTree] getVariables (Tag tag@("Rule", tree, parent)) = varList where tagList = selectFromTree (Tag tag) 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 getVariables t = [] testSearchContent = searchContent (getAllTags testTree) "log:implies" -- 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] -- 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"