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 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 |
------------------------------------------------------------------------------ --- 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 connect 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. --- ------------------------------------------------------------------------------ {-# LANGUAGE CPP #-} module Control.AllSolutions ( getAllValues, getAllSolutions, getOneValue, getOneSolution , getAllFailures ) where import Control.SearchTree --- Gets all values of an expression (currently, via an incomplete --- depth-first strategy). Conceptually, all values are computed --- on a copy of the expression, i.e., the evaluation of the expression --- does not share any results. Moreover, the evaluation suspends --- as long as the expression contains unbound variables. getAllValues :: a -> IO [a] getAllValues e = getSearchTree e >>= return . allValuesDFS --- 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 = do st <- getSearchTree x let vals = allValuesDFS st return (if null vals then Nothing else Just (head vals)) --- 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 = getAllValues (let x free in (x,c x)) >>= return . map fst --- 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)) --- 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 <- getAllValues generator failures <- mapIO (naf test) xs return $ concat failures -- (naf c x) returns [x] if (c x) fails, and [] otherwise. naf :: (a -> Bool) -> a -> IO [a] naf c x = getOneSolution (lambda c x) >>= returner x lambda :: (a -> Bool) -> a -> () -> Bool lambda c x _ = c x returner :: a -> Maybe b -> IO [a] returner x mbl = return (maybe [x] (const []) mbl) |