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