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 = True extended = True maxCounter = 25 :: 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 "Parsing time:\n" putStr (" seconds " ++ show (sec2 - sec1) ++ " micros " ++ show (m2-m1) ++ "\n") putStr "Inferencing time: \n" putStr (" seconds " ++ show (sec3 - sec2) ++ " micros " ++ show (m3 - m2) ++ "\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 = (substitutionList:substitutionList1, traceOut) where (substitutionList1, traceOut) = backtrack stack db level trace oldGoals --[] solve substitutionList goals stack db level trace oldGoals | bv1 = ([substitutionList], traceOut3) | goalList == [] && oneSol = ([substitutionList], traceOut5) | goalList == [] = solve substitutionList [] stack db1 level traceOut1 oldGoals | bv2 = choose substitutionList [] [] stack db level1 traceOut4 oldGoals | (alts1 == []) = choose substitutionList [] [] stack db level1 traceOut2 oldGoals | otherwise = choose substitutionList gs1 alts1 stack db level1 traceOut oldGoals where goalList = (testGQuery goals) gl@(g1:gs1) = goalList (_, g3,_, nrG) = g1 -- oldGoals1 = (g2, nrG):oldGoals g2 = applySubstitutionListToTripleSet substitutionList g3 -- if bv2 = true, then this goal has already happened bv2 = False -- (checkGoal oldGoals (g2,nrG) substitutionList) level1 = level + 1 res1 = (getAlts db g2 level1) res = res1 -- altsOut (res1, g2, []) alts1 = eliminateDoubles (eliminateDoublesSpecial 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 ++ "\n\n" ) 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 -- False means the goal is good. checkGoal [] goal sl = False checkGoal (([], nr):xs) goalI sl = checkGoal xs goalI sl checkGoal ((ts, nr):xs) goalI@(goal,nrIn) sl |bv1 && (nr == nrIn) = True -- goal already met |otherwise = checkGoal xs goalI sl where goal2 = goal -- applySubstitutionListToTripleSet goal sl bv1 = (compareTsG ag1 goal2) ag1 = ts -- applySubstitutionListToTripleSet ts sl ag = checkTripleSet ag1 bv2 = ag == [] compareTsG _ [] = False compareTsG [] g = False compareTsG t g = compareTreesVars t g 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 |bool && not bv2 && bv3 = solve substitutionList2a goals2a stack2a db level traceOut oldGoals |bool && not bv3 && bv4 = choose substList goals a2s stack db level traceOut1 oldGoals |bool && not bv2 = solve substitutionList1a goals1a stack2 db level traceOut oldGoals1 |otherwise = solve substitutionList1 goals1 stack1 db level traceOut oldGoals 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),(bool, ts, substList ++ sl, nrIn):goals) 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 (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), ts1 ++ goals) where -- ts2 = subgraphDB [ts] (-1) ts2 = subgraphTripleSet ts ts1 = [(bool,t, substList ++ sl, nrIn)| t <- ts2] (ts, sl) = alt -- 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 |bv1 && (nr == nrIn) = True -- goal already met |bv2 = checkGoals xs goalI sl |otherwise = checkGoals xs goalI sl where goal2 = goal -- applySubstitutionListToTripleSet goal sl bv1 = (compareTsG ag1 goal2) ag1 = ts -- applySubstitutionListToTripleSet ts sl ag = checkTripleSet ag1 bv2 = ag1 == [] comapreTsG _ [] = False compareTsG [] g = False compareTsG t g = compareTreesVars t g 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 -- 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]" 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 ["booleth.axiom.n3", "booleth.lemma.n3"]