home *** CD-ROM | disk | FTP | other *** search
/ PSION CD 2 / PsionCDVol2.iso / Programs / 876 / hugs.sis / PureEngine.hs < prev    next >
Encoding:
Text File  |  2000-09-21  |  1.5 KB  |  45 lines
  1. -- The Pure Prolog inference engine (using explicit prooftrees)
  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 PureEngine( version, prove ) where
  9.  
  10. import Prolog
  11. import Subst
  12.  
  13. version = "tree based" 
  14.  
  15. --- Calculation of solutions:
  16.  
  17. -- Each node in a prooftree corresponds to:
  18. -- either: a solution to the current goal, represented by Done s, where s
  19. --         is the required substitution
  20. -- or:     a choice between a number of subtrees ts, each corresponding to a
  21. --         proof of a subgoal of the current goal, represented by Choice ts.
  22. --         The proof tree corresponding to an unsolvable goal is Choice [] 
  23.  
  24. data Prooftree = Done Subst  |  Choice [Prooftree]
  25.  
  26. -- prooftree uses the rules of Prolog to construct a suitable proof tree for
  27. --           a specified goal
  28. prooftree   :: Database -> Int -> Subst -> [Term] -> Prooftree
  29. prooftree db = pt
  30.  where pt           :: Int -> Subst -> [Term] -> Prooftree
  31.        pt n s []     = Done s
  32.        pt n s (g:gs) = Choice [ pt (n+1) (u@@s) (map (app u) (tp++gs))
  33.                               | (tm:-tp)<-renClauses db n g, u<-unify g tm ]
  34.  
  35. -- search performs a depth-first search of a proof tree, producing the list
  36. --        of solution substitutions as they are encountered.
  37. search              :: Prooftree -> [Subst]
  38. search (Done s)      = [s]
  39. search (Choice pts)  = [ s | pt <- pts, s <- search pt ]
  40.  
  41. prove    :: Database -> [Term] -> [Subst]
  42. prove db  = search . prooftree db 1 nullSubst
  43.  
  44. --- End of PureEngine.hs
  45.