home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / MacHaskell 2.2 / progs / demo / prolog / Engine.hs next >
Encoding:
Text File  |  1994-09-27  |  2.0 KB  |  62 lines  |  [TEXT/YHS2]
  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
  62.