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