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