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 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 |
------------------------------------------------------------------------------ --- Library with some operations for encapsulating search. --- Note that some of these operations are not fully declarative, --- i.e., the results depend on the order of evaluation and program rules. --- There are newer and better approaches the encpasulate search, --- in particular, set functions (see module `SetFunctions`), --- which should be used. --- --- In previous versions of PAKCS, some of these operations were part of --- the standard prelude. We keep them in this separate module --- in order to support a more portable standard prelude. --- --- @author Michael Hanus --- @version July 2015 --- @category general ------------------------------------------------------------------------------ {-# OPTIONS_CYMAKE -Wno-incomplete-patterns #-} module Findall ( getAllValues, getSomeValue , allValues, someValue , allSolutions, someSolution , try, inject, solveAll, once, best , findall, findfirst, browse, browseList, unpack , rewriteAll, rewriteSome ) where --- 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. --- Similar to Prolog's findall. getAllValues :: a -> IO [a] getAllValues e = return (allValues e) --- Gets a value of an expression (currently, via an incomplete --- depth-first strategy). The expression must have a value, otherwise --- the computation fails. Conceptually, the value is 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. getSomeValue :: a -> IO a getSomeValue e = return (someValue e) --- Returns 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. --- --- Note that this operation is not purely declarative since the ordering --- of the computed values depends on the ordering of the program rules. allValues :: a -> [a] allValues e = findall (\x -> x=:=e) --- Returns some value for an expression (currently, via an incomplete --- depth-first strategy). If the expression has no value, the --- computation fails. Conceptually, the value is 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. --- --- Note that this operation is not purely declarative since --- the computed value depends on the ordering of the program rules. --- Thus, this operation should be used only if the expression --- has a single value. someValue :: a -> a someValue e = findfirst (=:=e) --- Returns all values satisfying a predicate, i.e., all arguments such that --- the predicate applied to the argument can be evaluated to `True` --- (currently, via an incomplete depth-first strategy). --- The evaluation suspends as long as the predicate expression --- contains unbound variables. --- --- Note that this operation is not purely declarative since the ordering --- of the computed values depends on the ordering of the program rules. allSolutions :: (a->Bool) -> [a] allSolutions p = findall (\x -> p x =:= True) --- Returns some values satisfying a predicate, i.e., some argument such that --- the predicate applied to the argument can be evaluated to `True` --- (currently, via an incomplete depth-first strategy). --- If there is no value satisfying the predicate, the computation fails. --- --- Note that this operation is not purely declarative since the ordering --- of the computed values depends on the ordering of the program rules. --- Thus, this operation should be used only if the --- predicate has a single solution. someSolution :: (a->Bool) -> a someSolution p = findfirst (\x -> p x =:= True) ------------------------------------------------------------------------------ --- Basic search control operator. try :: (a -> Bool) -> [a -> Bool] try external --- Inject operator which adds the application of the unary --- procedure p to the search variable to the search goal --- taken from Oz. p x comes before g x to enable a test+generate --- form in a sequential implementation. inject :: (a -> Bool) -> (a -> Bool) -> (a -> Bool) inject g p = \x -> p x & g x --- Computes all solutions via a a depth-first strategy. -- -- Works as the following algorithm: -- -- solveAll g = evalResult (try g) -- where -- evalResult [] = [] -- evalResult [s] = [s] -- evalResult (a:b:c) = concatMap solveAll (a:b:c) -- -- The following solveAll algorithm is faster. -- For comparison we have solveAll2, which implements the above algorithm. solveAll :: (a -> Bool) -> [a -> Bool] solveAll g = evalall (try g) where evalall [] = [] evalall [a] = [a] evalall (a:b:c) = evalall3 (try a) (b:c) evalall2 [] = [] evalall2 (a:b) = evalall3 (try a) b evalall3 [] b = evalall2 b evalall3 [l] b = l : evalall2 b evalall3 (c:d:e) b = evalall3 (try c) (d:e ++b) solveAll2 :: (a -> Bool) -> [a -> Bool] solveAll2 g = evalResult (try g) where evalResult [] = [] evalResult [s] = [s] evalResult (a:b:c) = concatMap solveAll2 (a:b:c) --- Gets the first solution via a depth-first strategy. once :: (a -> Bool) -> (a -> Bool) once g = head (solveAll g) --- Gets the best solution via a depth-first strategy according to --- a specified operator that can always take a decision which --- of two solutions is better. --- In general, the comparison operation should be rigid in its arguments! best :: (a -> Bool) -> (a -> a -> Bool) -> [a -> Bool] best g cmp = bestHelp [] (try g) [] where bestHelp [] [] curbest = curbest bestHelp [] (y:ys) curbest = evalY (try (constrain y curbest)) ys curbest bestHelp (x:xs) ys curbest = evalX (try x) xs ys curbest evalY [] ys curbest = bestHelp [] ys curbest evalY [newbest] ys _ = bestHelp [] ys [newbest] evalY (c:d:xs) ys curbest = bestHelp (c:d:xs) ys curbest evalX [] xs ys curbest = bestHelp xs ys curbest evalX [newbest] xs ys _ = bestHelp [] (xs++ys) [newbest] evalX (c:d:e) xs ys curbest = bestHelp ((c:d:e)++xs) ys curbest constrain y [] = y constrain y [curbest] = inject y (\v -> let w free in curbest w & cmp v w =:= True) --- Gets all solutions via a depth-first strategy and unpack --- the values from the lambda-abstractions. --- Similar to Prolog's findall. findall :: (a -> Bool) -> [a] findall g = map unpack (solveAll g) --- Gets the first solution via a depth-first strategy --- and unpack the values from the search goals. findfirst :: (a -> Bool) -> a findfirst g = head (findall g) --- Shows the solution of a solved constraint. browse :: (_ -> Bool) -> IO () browse g = putStr (show (unpack g)) --- Unpacks solutions from a list of lambda abstractions and write --- them to the screen. browseList :: [_ -> Bool] -> IO () browseList [] = done browseList (g:gs) = browse g >> putChar '\n' >> browseList gs --- Unpacks a solution's value from a (solved) search goal. unpack :: (a -> Bool) -> a unpack g | g x = x where x free --- Gets all values computable by term rewriting. --- In contrast to `findall`, this operation does not wait --- until all "outside" variables are bound to values, --- but it returns all values computable by term rewriting --- and ignores all computations that requires bindings for outside variables. rewriteAll :: a -> [a] rewriteAll external --- Similarly to 'rewriteAll' but returns only some value computable --- by term rewriting. Returns `Nothing` if there is no such value. rewriteSome :: a -> Maybe a rewriteSome external |