Module Findall

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

Summary of exported operations:

getAllValues :: a -> IO [a]   
Gets all values of an expression (currently, via an incomplete depth-first strategy).
getSomeValue :: a -> IO a   
Gets a value of an expression (currently, via an incomplete depth-first strategy).
allValues :: a -> [a]   
Returns all values of an expression (currently, via an incomplete depth-first strategy).
someValue :: a -> a   
Returns some value for an expression (currently, via an incomplete depth-first strategy).
allSolutions :: (a -> Bool) -> [a]   
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).
someSolution :: (a -> Bool) -> a   
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).
try :: (a -> Bool) -> [a -> Bool]   
Basic search control operator.
inject :: (a -> Bool) -> (a -> Bool) -> a -> Bool   
Inject operator which adds the application of the unary procedure p to the search variable to the search goal taken from Oz.
solveAll :: (a -> Bool) -> [a -> Bool]   
Computes all solutions via a a depth-first strategy.
once :: (a -> Bool) -> a -> Bool   
Gets the first solution via a depth-first strategy.
best :: (a -> Bool) -> (a -> a -> Bool) -> [a -> Bool]   
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.
findall :: (a -> Bool) -> [a]   
Gets all solutions via a depth-first strategy and unpack the values from the lambda-abstractions.
findfirst :: (a -> Bool) -> a   
Gets the first solution via a depth-first strategy and unpack the values from the search goals.
browse :: (a -> Bool) -> IO ()   
Shows the solution of a solved constraint.
browseList :: [a -> Bool] -> IO ()   
Unpacks solutions from a list of lambda abstractions and write them to the screen.
unpack :: (a -> Bool) -> a   
Unpacks a solution's value from a (solved) search goal.
rewriteAll :: a -> [a]   
Gets all values computable by term rewriting.
rewriteSome :: a -> Maybe a   
Similarly to rewriteAll but returns only some value computable by term rewriting.

Exported operations:

getAllValues :: a -> IO [a]   

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.

getSomeValue :: a -> IO a   

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.

allValues :: a -> [a]   

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.

someValue :: a -> a   

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.

allSolutions :: (a -> Bool) -> [a]   

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.

someSolution :: (a -> Bool) -> a   

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.

try :: (a -> Bool) -> [a -> Bool]   

Basic search control operator.

Further infos:
  • externally defined

inject :: (a -> Bool) -> (a -> Bool) -> a -> Bool   

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.

solveAll :: (a -> Bool) -> [a -> Bool]   

Computes all solutions via a a depth-first strategy.

once :: (a -> Bool) -> a -> Bool   

Gets the first solution via a depth-first strategy.

best :: (a -> Bool) -> (a -> a -> Bool) -> [a -> Bool]   

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!

findall :: (a -> Bool) -> [a]   

Gets all solutions via a depth-first strategy and unpack the values from the lambda-abstractions. Similar to Prolog's findall.

findfirst :: (a -> Bool) -> a   

Gets the first solution via a depth-first strategy and unpack the values from the search goals.

browse :: (a -> Bool) -> IO ()   

Shows the solution of a solved constraint.

browseList :: [a -> Bool] -> IO ()   

Unpacks solutions from a list of lambda abstractions and write them to the screen.

unpack :: (a -> Bool) -> a   

Unpacks a solution's value from a (solved) search goal.

rewriteAll :: a -> [a]   

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.

Further infos:
  • externally defined

rewriteSome :: a -> Maybe a   

Similarly to rewriteAll but returns only some value computable by term rewriting. Returns Nothing if there is no such value.

Further infos:
  • externally defined