module N3Engine where import "Utils" import "TripleData" import "XML" import "N3Parser" import "Array" import "LoadTree" import "N3Unify" import "Observe" import "GenerateDB" import "Transform" import "ToN3" import "Subgraphs" import "AltsOut" import "AltsIn" import "Time" import "SubAnons" -- format of trace (in notation 3): -- [:call tripleSet]. -- try to match a tripleset -- [:exit [tripleSet]]. -- show the found alternatives -- only when flag extended -- [:failed tripleSet]. -- unification failed -- {:solution = {{:var1 = :term1 :var2 = :term2. ....}}. -- the goallist was empty -- The output of the trace is controlled by the flag verbose. verbose = False extended = True maxCounter = 15000 :: Int testGrounded = True counterFlag = True oneSol = False testEngine2 = n3Engine ["authen.axiom.n3", "authen.lemma.n3"] testEngine1 = show (proof [tauDB] [tauQ] []) testEngine = n3Solution ["authen.axiom.n3", "authen.lemma.n3"] -- This generates a database and a query . Input is a list of filenames; -- output is a solution to a query and a trace. n3Solution :: [String] -> IO() n3Solution filenames = do listF <- sequence (map readFile filenames) putStr ("Starting the parse ...\n") TOD sec1 m1 <- getClockTime let (s, t1, t2) = getDBQuery1 listF putStr (s ++ "\n") TOD sec2 m2 <- t1 TOD sec3 m3 <- t2 putStr "Working time:\n" putStr (" seconds " ++ show (sec2 - sec1) ++ " micros " ++ show (m2-m1) ++ "\n") changeAnons1 :: DB -> DB changeAnons1 [] = [] changeAnons1 (x:xs) = map changeTriple x: changeAnons1 xs where changeTriple (Triple(Var (EVar s), p, o)) |containsString "T$$$" s = Triple (URI s, p, o) |otherwise = Triple (Var (EVar s), p, o) changeTriple t = t getDBQuery1 :: [String] -> (String, IO ClockTime, IO ClockTime) getDBQuery1 [] = ("Empty input for proof search", getClockTime, getClockTime) getDBQuery1 inputs = ((testVerbose "" ("Substitutions:\n\n" ++ substListListToN3 sll)) ++ "\nN3Trace:\n\n" ++ trace ++ solutions, t1, t2) where ((dbOut, queryOut), t1) = (getDBQuery inputs, getClockTime) dbOut1 = changeAnons1 dbOut (sll, trace) = (proof dbOut1 queryOut ((intToString 0) ++ " ")) (solutions, t2) = ("\nQuery:\n\n" ++ dbToN3 queryOut ++ getSolutions sll queryOut, getClockTime) getSolutions :: [SubstitutionList] -> [TripleSet] -> String getSolutions [] _ = "" getSolutions (x:xs) queryOut = sol2 ++ getSolutions xs queryOut where sol1 = applySubstitutionListToDB x queryOut sol2 = "\nSolution:\n\n" ++ dbToN3 sol1 -- This generates a database and a query . Input is a list of filenames; -- output is a solution to a query and a trace. n3Engine :: [String] -> IO() n3Engine filenames = do listF <- sequence (map readFile filenames) putStr (show (getDBQuerya listF)) getDBQuerya :: [String] -> ([SubstitutionList], N3Trace) getDBQuerya [] = ([],"Empty input for proof search") getDBQuerya inputs = ([substList], trace) where (dbOut, queryOut) = getDBQuery inputs ([substList], trace) = proof dbOut queryOut ((intToString 0) ++ " ") testGetAlts = show (getAlts [tauDB] tauQ 1) -- type Alternatives = [(TripleSet, SubstitutionList)] -- Bool = True -> A rule was handled;Bool = False -> no rule. -- The int is the rule number -- type UnifRes = [(Bool, TripleSet, SubstitutionList, Int)] -- True returned means a rule has been handled -- False means no rule. -- API: altsOut and altsIn . getAlts :: DB -> TripleSet -> Int -> UnifRes getAlts [] _ _ = [] getAlts db [] _ = [] getAlts db@(x:xs) goal int | bool && bv1 = res1 ++ getAlts xs goal int | bool && bv2 = res2 ++ getAlts xs goal int | bool = res ++ getAlts xs goal int | otherwise = getAlts xs goal int where (bool, alts) = unifyTripleSets goal1 (renameTripleSet x1 int) [(ts, sl)] = alts -- call api outgoing alternatives -- unifRes2 = altsOut (res1, goal, x) -- unifRes3 = altsOut (res, goal, x) res = [(False, ts1, sl1, -1)|(ts1,sl1) <- alts] res1 = [(True, ts1, sl1, nr1)|(ts1,sl1) <- alts] res2 = [(False, ts1, sl1, nr2)|(ts1,sl1) <- alts] (y:ys) = x1 bv1 = testRule y bv2 = testRule (head goal1) Rule (_, _, nr1) = y Rule (_, _, nr2) = (head goal1) -- call api incoming goal and tripleset to match with (goal1, x1) = altsIn (goal, x) testRule (Rule r) = True testRule t = False testRenameTripleSet = show (renameTripleSet tauDB 2) -- rename the variables in a tripleset renameTripleSet :: TripleSet -> Int -> TripleSet renameTripleSet [] level = [] renameTripleSet t@(x:xs) level = renameTriple x level:renameTripleSet xs level where renameTriple t@(Triple(s, p, o)) l = Triple(s1, p1, o1) where s1 = renameAtom s l p1 = renameAtom p l o1 = renameAtom o l renameAtom (Var v) l = Var (renameVar v l) renameAtom (TripleSet t) l = TripleSet (renameTripleSet t l) renameAtom any l = any renameVar (UVar s) l = (UVar ((intToString l) ++ "$_$" ++ s)) renameVar (EVar s) l = (EVar ((intToString l) ++ "$_$" ++ s)) renameVar (GVar s) l = (GVar ((intToString l) ++ "$_$" ++ s)) renameVar (GEVar s) l = (GEVar ((intToString l) ++ "$_$" ++ s)) renameTriple r@(Rule (ants, conseq, i)) l = Rule (renameTripleSet ants l, renameTripleSet conseq l, i) type N3Trace = String -- The first UnfiRes are the goals, the second the alternatives; -- Goals is the old goals list; the Int is the resolution level. type Stack = [(SubstitutionList, UnifRes, UnifRes, Int)] -- type Alternatives = [(TripleSet, SubstitutionList)] alts = [] stack = [([],[],alts, 0:: Int)] -- type UnifRes = [(Bool, TripleSet, SubstitutionList, Int)] -- the oldgoals list; the first Int is the rule number; -- the second Int is the level number. type Goals = [(TripleSet, Int, Int)] testGQuery ((_,[Triple(URI "query", URI "query", URI "query")], _,_):query) = query testGQuery q = checkGroundedU q checkGroundedU [] = [] checkGroundedU (q:qs) | bv1 = checkGroundedU qs | otherwise = q:(checkGroundedU qs) where (_, ts, _, _) = q g = checkTripleSet ts bv1 = g == [] proof :: DB -> Query -> N3Trace -> ([SubstitutionList], N3Trace) proof db query trace = solve [] query1 stack db 1 trace [] where query1 = (False,[Triple(URI "query",URI "query", URI "query")], [], -1): expandQuery query expandQuery [] = [] expandQuery (x:xs) = (False, x, [], -1): expandQuery xs -- solve executes the unification process with alternatives as a result solve :: SubstitutionList -> UnifRes -> Stack -> DB -> Int -> N3Trace -> Goals -> ([SubstitutionList], N3Trace) solve substitutionList [] stack db level trace oldGoals |oneSol = ([substitutionList], traceOut1) |otherwise = (substitutionList:substitutionList1, traceOut) where (substitutionList1, traceOut) = backtrack stack db level trace oldGoals traceOut1 = testVerbose trace ("[:stopped :one_solution].\n\n") solve substitutionList goals stack db level trace oldGoals | bv1 = ([substitutionList], traceOut3) | goalList == [] && oneSol = ([substitutionList], traceOut5) | goalList == [] = solve substitutionList [] stack db1 level traceOut1 oldGoals | (alts1 == []) = choose substitutionList [] [] stack db level1 traceOut2 oldGoals1 -- | bv3 = solve substitutionList gs1 stack db level trace oldGoals | otherwise = choose substitutionList gs1 alts1 stack db level1 traceOut oldGoals1 where goalList = (testGQuery goals) gl@(g1:gs1) = eliminateDoublesSpecial goalList (_, g3,_, nrG) = g1 addToGoals goal oldGoals bool |bool && bv1 = goal:oldGoals |otherwise = oldGoals where (g, _, _) = goal bv1 = (checkTripleSet g == []) oldGoals1 = addToGoals (g2,(-2), level + 1) oldGoals (alts1 /= []) -- test if this goal has already been found -- if yes get the next goal bv3 = testFound g2 oldGoals testFound g [] = False testFound g oldGoals | not ((checkTripleSet g) == []) = False | otherwise = checkGoals1 oldGoals (g, (-2), level) [] g2 = applySubstitutionListToTripleSet substitutionList g3 -- if bv2 = true, then this goal has already happened level1 = level + 1 res = (getAlts db g2 level1) alts1 = eliminateDoubles res getTripleSets urs = [ts|(_, ts, _, _) <- urs] getSubstitutionList urs = [sl|(_, _, sl, _) <- urs] (trace2, i) = testCounterFlag trace bv1 = i > maxCounter trace1 = testVerbose "" (testExtended "" ( -- "oldGoals " ++ show oldGoals ++ "\n" ++ -- ":goalList = {" ++ showGoals goals ++ "}\n" ":alternatives = {" ++ dbToN3 (applySubstitutionListToDB substitutionList (getTripleSets alts1)) ++ "}\n" ++ ":subtitutions = {" ++ substListListToN3 ( (substitutionList: getSubstitutionList alts1)) ++ "}\n") ) showGoals goals = dbToN3 [gg|(_,gg,_, _) <- goals] traceOut = testVerbose trace2 ("[:call " ++ tripleSetToN3 g2 ++ "].\n" ++ trace1 ) traceOut1 = testVerbose trace2 ("{:solution = " ++ substListToN3 substitutionList ++ "}.\n\n") -- add the solution to the db db1 = addToDB db (applySubstitutionListToDB substitutionList query) addToDB :: [TripleSet] -> [TripleSet] -> [TripleSet] addToDB [] ts = ts addToDB db [] = db addToDB db db1 = subgraphDB (db ++ db1) (-1) traceOut2 = testVerbose trace2 ("[:failed " ++ tripleSetToN3 g2 ++ "].\n\n") traceOut4 = testVerbose trace2 ("[:looping " ++ tripleSetToN3 g2 ++ "].\n\n") traceOut3 = testVerbose trace2 ("[:failed :limitCounter].\n\n") traceOut5 = testVerbose trace2 ("[:stopped :one_solution].\n\n") -- when looping alts are sometimes returning identical -- intercepting here is efficient choose :: SubstitutionList -> UnifRes -> UnifRes -> Stack -> DB -> Int -> N3Trace -> Goals -> ([SubstitutionList], N3Trace) choose substList goals [] stack db level trace oldGoals = backtrack stack db level traceOut oldGoals where traceOut = testVerbose trace "" choose substList goals alts@(a:as) stack db level trace oldGoals -- alts were rejected by anti-looping; use next alts |bool && bv4 = choose substList goals a2s stack db level traceOut1 oldGoals -- bool indicates that the alts were generated by a rule |bool && not bv2 && bv3 = solve substitutionList2a goals2a stack2a db level traceOut oldGoals |bool && not bv2 = solve substitutionList1a goals1a stack2 db level traceOut oldGoals1 |otherwise = solve substitutionList1 goals1 stack1 db level traceOut oldGoals2 where (bool, tripleset, substitutionList, nrIn) = a a1 = (tripleset, substitutionList) stack1 = (substList, goals, as, level):stack traceOut = testVerbose trace "" traceOut1 = testVerbose trace ("[:looping " ++ tripleSetToN3 ts2a ++ "]:\n") -- ++ (show oldGoals) ++ "\n") -- add the antecedents bv2 = tripleset == [] alts1 = [a1] (substitutionList1, goals1) = addAltsToGoal (a1, substList, goals) addAltsToGoal (([TripleNil],_), substList, goals) = (substList, goals) addAltsToGoal (alt, substList, goals) = ((substList ++ sl),goals ++ [(bool, ts, substList ++ sl, nrIn)]) where (ts, sl) = alt -- add match of tripleset with rule to goallist bv3 = as == [] (substitutionList2a, goals2a) = addRuleToGoal (a1, substList, goals) stack2a = stack -- (substList, goals,as):stack -- add alts from match with tripleset (tsg, slg) = a1 oldGoals2 = (ts2b, -1, level):oldGoals ts2b = applySubstitutionListToTripleSet (substList ++ slg) tsg (a2:a2s) = as (substitutionList1a, goals1a) = addAltsToGoal (a1, substitutionList2, goals2) (_, ts2, sl2,_) = a2 a2a = (ts2, sl2) stack2 = (substList, goals, a2s, level):stack oldGoals1 = (ts2a, nrIn, level):oldGoals ts2a = applySubstitutionListToTripleSet (substList ++ sl2) ts2 bv4 = checkGoals oldGoals (ts2a, nrIn, level) [] (substitutionList2, goals2) = addRuleToGoal (a2a, substList, goals) addRuleToGoal (([], sl), substList, goals) = ((substList ++ sl), goals) addRuleToGoal (alt, substList, goals) = ((substList ++ sl), goals ++ ts1) where -- ts2 = subgraphDB [ts] (-1) ts2 = subgraphTripleSet ts ts1 = [(bool,t, substList ++ sl, nrIn)| t <- ts2] (ts, sl) = alt backtrack :: Stack -> DB -> Int -> N3Trace -> Goals -> ([SubstitutionList], N3Trace) backtrack [] _ _ trace oldGoals = ([], trace) backtrack stack db level trace oldGoals = choose substList goals alts sts db level traceOut oldGoals1 where st@((substList, goals, alts, level):sts) = stack traceOut = testVerbose trace "" oldGoals1 = tillLevel oldGoals tillLevel [] = [] tillLevel ((goal, nr, lev):og) |lev > level = tillLevel og |otherwise = (goal, nr, lev):og -- False means the goal is good. checkGoals [] goal sl = False checkGoals (([], nr, _):xs) goalI sl = checkGoals xs goalI sl checkGoals ((ts, nr, _):xs) goalI@(goal,nrIn, _) sl |nr == -2 = checkGoals xs goalI sl |bv1 && (nrIn == -1) = True |bv1 && (nr == nrIn) = True -- goal already met |otherwise = checkGoals xs goalI sl where bv1 = (compareTsG ts goal) comapareTsG _ [] = False compareTsG [] g = False compareTsG t g = compareTreesVars t g -- False means the goal is good. checkGoals1 [] goal sl = False checkGoals1 (([], nr, _):xs) goalI sl = checkGoals1 xs goalI sl checkGoals1 ((ts, nr, _):xs) goalI@(goal,nrIn, _) sl |bv1 && (nr == (-2)) && (nrIn == (-2)) = True |otherwise = checkGoals1 xs goalI sl where bv1 = (compareTsG ts goal) comapareTsG _ [] = False compareTsG [] g = False compareTsG t g = compareTreesVars t g -- type UnifRes = [(Bool, TripleSet, SubstitutionList, Int)] eliminateDoublesSpecial :: UnifRes -> UnifRes eliminateDoublesSpecial [] = [] eliminateDoublesSpecial (x:xs) = x1:eliminateDoublesSpecial xs where x1 = elimDoubleSpecial x elimDoubleSpecial (bv1, ts1, s1, nr1) = (bv1, elimDoubles ts1, s1, nr1) where elimDoubles [] = [] elimDoubles (x:xs) | elimDoubleX x xs = elimDoubles xs | otherwise = x:elimDoubles xs where elimDoubleX x [] = False elimDoubleX x (y:ys) | bv1 = True | otherwise = elimDoubleX x ys where bv1 = compareTriplesVars x y testVerbose trace s |verbose = trace ++ s |otherwise = trace testExtended trace s |extended = trace ++ s |otherwise = trace testCounterFlag trace |counterFlag = (trace1, i) |otherwise = ("", 0) where (bool, s, r) = parseUntil ' ' trace i = stringToInt s trace1 = (intToString (i+1)) ++ " " ++ r -- test data from N3Unify.hs -- example authen.axiom.n3 and authen.lemma.n3 -- tau1 = Triple(URI "", -- URI ":member", URI "") -- tau2 = Triple(URI "", URI ":w3cmember", -- URI "") -- tau3 = Triple(URI "", URI ":subscribed", -- URI "") -- tau4 = Triple(Var (UVar ":person"), URI ":member", Var (UVar ":institution")) -- tau5 = Triple(Var (UVar ":institution"), URI ":w3cmember", -- URI "") -- tau6 = Triple(Var (UVar ":institution"), URI ":subscribed", -- Var (UVar ":mailinglist")) -- tau7 = Triple (Var (UVar ":person"), URI ":authenticated", -- Var (UVar ":mailinglist")) -- ants = [tau4, tau5, tau6] -- cons = tau7 -- rule = Rule (ants, cons, 1) -- tau8 = Triple(Var (EVar "_:who"), URI ":authenticated", -- URI "") -- tauQ = [tau8] -- tauDB = [tau1, tau2, tau3, rule] -- sub1 = (UVar ":person", URI "") -- sub2 = (UVar ":mailinglist", URI "") -- sub3 = (UVar ":institution", URI "") -- subList = [sub1, sub2, sub3] menu = let print s = putStr (s ++ "\n") in do print "Type the command = first word." print "Between [] are the used files." print "" print "en1 [animal.n3, animal-simple.n3]" print "en2 [authen.axiom.n3,authen.lemma.n3]" print "en3 [danb.n3, danb-query.n3]" print "en5 [gedcom-facts.n3, gedcom-relations.n3, gedcom-query.n3]" print "en19 [vogel.l.n3, vogel.q.n3]" print "en22 [Owls.n3, owls.query.n3]" print "en25 [ontology.axiom.n3, ontology.query.n3]" print "en26 [ontology1.axiom.n3, ontology1.query.n3]" print "en27 [gedcom-simple.n3, gedcom-relSimple.n3, gedcom-qsimple.n3]" print "en32 [path.axiom.n3, path.query.n3]" print "en35 [booleW.a.n3, booleW.q.n3]" en1 = n3Solution ["animal.n3", "animal-simple.n3"] en2 = n3Solution ["authen.axiom.n3","authen.lemma.n3"] -- ok en3 = n3Solution ["danb.n3", "danb-query.n3"] -- ok en3a = n3Solution ["danb.n3", "danb-query1.n3"] en4 = n3Solution ["danc.n3", "danc-query.n3"] en5 = n3Solution ["gedcom-facts.n3", "gedcom-relations.n3", "gedcom-query.n3"] en6 = n3Solution ["graph.axiom.n3", "graph.lemma.n3"] en6a = n3Solution ["graph.axiom1.n3", "graph.lemma1.n3"] en7 = n3Solution ["lists.n3", "lists-query.n3"] en8 = n3Solution ["rdf-facts.n3", "rdf-rules.n3", "rdf-query.n3"] en9 = n3Solution ["rdfc25May-test.n3", "rdfc25May.n3"] en10 = n3Solution ["rdfs-rules.n3", "rdfs-query.n3"] en11 = n3Solution ["russell.axiom.n3", "russell.lemma.n3"] en12 = n3Solution ["subclass.n3", "subclass-query.n3"] en13 = n3Solution ["subprop.n3", "subprop-query.n3"] en14 = n3Solution ["test-test.n3", "test.n3"] en15 = n3Solution ["tpoint-all.n3", "tpoint-facts.n3", "tpoint.n3", "tpoint-query.n3"] en16 = n3Solution ["varprop.n3", "varprop-query.n3"] en17 = n3Solution ["ziv.n3", "ziv-query.n3"] en18 = n3Solution ["wol-facts.n3", "wol-rules.n3", "wol-query.n3"] en19 = n3Solution ["vogel.l.n3", "vogel.q.n3"] -- ok en21 = n3Solution ["induction.axiom.n3", "induction.query.n3"] -- ok en22 = n3Solution ["Owls.n3", "owls.query.n3"] -- ok en23 = n3Solution ["logic.a.n3", "logic.q.n3"] -- some ok en24 = n3Solution ["unif.n3","unif.q.n3"] -- ok en25 = n3Solution ["ontology.axiom.n3", "ontology.query.n3"] -- ok en26 = n3Solution ["ontology1.axiom.n3", "ontology1.query.n3"] -- ok en27 = n3Solution ["gedcom-simple.n3", "gedcom-relSimple.n3", "gedcom-qsimple.n3"] -- ok en28 = n3Solution ["owns.n3", "owns.q.n3"] -- ok en29 = n3Solution ["ontology2.axiom.n3", "ontology.query.n3"] en29a = n3Solution ["ontology3.axiom.n3", "ontology1.query.n3"] en29b = n3Solution ["ontologyM.axiom.n3", "ontology.query.n3"] en30 = n3Solution ["eq.a.n3", "eq.q.n3"] en31 = n3Solution ["subprop.a.n3", "subprop.q.n3"] en32 = n3Solution ["path.axiom.n3", "path.query.n3"] en33 = n3Solution ["mult.a.n3", "mult.q.n3"] en34 = n3Solution ["boole.axiom.n3", "boole.lemma.n3"] en35 = n3Solution ["booleW.a.n3", "booleW.q.n3"]