1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 |
------------------------------------------------------------------------------ --- This module contains a collection of functions for --- obtaining lists of solutions to constraints. --- These operations are useful to encapsulate --- non-deterministic operations between I/O actions in --- order to connects the worlds of logic and functional programming --- and to avoid non-determinism failures on the I/O level. --- --- In contrast the "old" concept of encapsulated search --- (which could be applied to any subexpression in a computation), --- the operations to encapsulate search in this module --- are I/O actions in order to avoid some anomalities --- in the old concept. --- --- @category general ------------------------------------------------------------------------------ module AllSolutions(getAllSolutions,getAllValues, getOneSolution,getOneValue, getAllFailures, getSearchTree,SearchTree(..)) where import Findall --- Gets all solutions to a constraint (currently, via an incomplete --- depth-first left-to-right strategy). Conceptually, all solutions --- are computed on a copy of the constraint, i.e., the evaluation --- of the constraint does not share any results. Moreover, this --- evaluation suspends if the constraints contain unbound variables. --- Similar to Prolog's findall. getAllSolutions :: (a->Bool) -> IO [a] getAllSolutions c = return (findall c) {- -- In principle, getAllSolutions can be defined by getSearchTree as follows: getAllSolutions c = do (Solutions sols) <- getSearchTree [] c return sols -- However, our above definition is slightly more efficient. -} --- Gets all values of an expression. Since this is based on --- <code>getAllSolutions</code>, it inherits the same restrictions. getAllValues :: a -> IO [a] getAllValues e = return (findall (=:=e)) --- Gets one solution to a constraint (currently, via an incomplete --- left-to-right strategy). Returns Nothing if the search space --- is finitely failed. getOneSolution :: (a->Bool) -> IO (Maybe a) getOneSolution c = do sols <- getAllSolutions c return (if null sols then Nothing else Just (head sols)) --- Gets one value of an expression (currently, via an incomplete --- left-to-right strategy). Returns Nothing if the search space --- is finitely failed. getOneValue :: a -> IO (Maybe a) getOneValue x = getOneSolution (x=:=) --- Returns a list of values that do not satisfy a given constraint. --- @param x - an expression (a generator evaluable to various values) --- @param c - a constraint that should not be satisfied --- @return A list of all values of e such that (c e) is not provable getAllFailures :: a -> (a->Bool) -> IO [a] getAllFailures generator test = do xs <- getAllSolutions (=:=generator) failures <- mapIO (naf test) xs return $ concat failures where -- (naf c x) returns [x] if (c x) fails, and [] otherwise. naf :: (a->Bool) -> a -> IO [a] naf c x = getOneSolution (\_->c x) >>= \mbl-> return (maybe [x] (const []) mbl) --- A search tree for representing search structures. data SearchTree a b = SearchBranch [(b,SearchTree a b)] | Solutions [a] --- Computes a tree of solutions where the first argument determines --- the branching level of the tree. --- For each element in the list of the first argument, --- the search tree contains a branch node with a child tree --- for each value of this element. Moreover, evaluations of --- elements in the branch list are shared within corresponding subtrees. getSearchTree :: [a] -> (b -> Bool) -> IO (SearchTree b a) getSearchTree cs goal = return (getSearchTreeUnsafe cs goal) getSearchTreeUnsafe :: [a] -> (b -> Bool) -> (SearchTree b a) getSearchTreeUnsafe [] goal = Solutions (findall goal) getSearchTreeUnsafe (c:cs) goal = SearchBranch (findall (=:=(solve c cs goal))) solve :: a -> [a] -> (b -> Bool) -> (a,SearchTree b a) solve c cs goal | c=:=y = (y, getSearchTreeUnsafe cs goal) where y free |