1 -- 2 -- Stack based Prolog inference engine 3 -- Mark P. Jones November 1990 4 -- 5 -- uses Haskell B. version 0.99.3 6 -- 7 module Engine(prove) where 8 9 import PrologData 10 import Subst 11 12 --- Calculation of solutions: 13 14 -- the stack based engine maintains a stack of triples (s,goal,alts) 15 -- corresponding to backtrack points, where s is the substitution at that 16 -- point, goal is the outstanding goal and alts is a list of possible ways 17 -- of extending the current proof to find a solution. Each member of alts 18 -- is a pair (tp,u) where tp is a new subgoal that must be proved and u is 19 -- a unifying substitution that must be combined with the substitution s. 20 -- 21 -- the list of relevant clauses at each step in the execution is produced 22 -- by attempting to unify the head of the current goal with a suitably 23 -- renamed clause from the database. 24 25 type Stack = [ (Subst, [Term], [Alt]) ] 26 type Alt = ([Term], Subst) 27 28 alts :: Database -> Int -> Term -> [Alt] 29 alts db n g = [ (tp,u) | (tm:==tp) <- renClauses db n g, u <- unify g tm ] 30 31 -- The use of a stack enables backtracking to be described explicitly, 32 -- in the following `state-based' definition of prove: 33 34 prove :: Database -> [Term] -> [Subst] 35 prove db gl = solve 1 nullSubst gl [] 36 where 37 solve :: Int -> Subst -> [Term] -> Stack -> [Subst] 38 solve n s [] ow = s : backtrack n ow 39 solve n s (g:gs) ow 40 | g==theCut = solve n s gs (cut ow) 41 | otherwise = choose n s gs (alts db n (apply s g)) ow 42 43 choose :: Int -> Subst -> [Term] -> [Alt] -> Stack -> [Subst] 44 choose n s gs [] ow = backtrack n ow 45 choose n s gs ((tp,u):rs) ow = solve (n+1) (u@@s) (tp++gs) ((s,gs,rs):ow) 46 47 backtrack :: Int -> Stack -> [Subst] 48 backtrack n [] = [] 49 backtrack n ((s,gs,rs):ow) = choose (n-1) s gs rs ow 50 51 52 --- Special definitions for the cut predicate: 53 54 theCut :: Term 55 theCut = Struct "!" [] 56 57 cut :: Stack -> Stack 58 cut (top:(s,gl,_):ss) = top:(s,gl,[]):ss 59 cut ss = ss 60 61 --- End of Engine.hs