Module Control.AllValues

Library with operations to encapsulate search, i.e., non-deterministic computations. 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 encapsulate search, in particular, set functions (see module Control.SetFunctions in package setfunctions), which should be used.

Author: Michael Hanus

Version: November 2022

Summary of exported operations:

getAllValues :: a -> IO [a]  Deterministic 
Gets all values of an expression (similarly to Prolog's findall).
getOneValue :: a -> IO (Maybe a)  Deterministic 
Gets one value of an expression.
getAllSolutions :: Data a => (a -> Bool) -> IO [a]  Deterministic 
Gets all solutions to a constraint.
getOneSolution :: Data a => (a -> Bool) -> IO (Maybe a)  Deterministic 
Gets one solution to a constraint.
getAllFailures :: a -> (a -> Bool) -> IO [a]  Deterministic 
Returns a list of values that do not satisfy a given constraint.
allValues :: a -> [a]  Deterministic 
Returns all values of an expression.
someValue :: a -> a  Deterministic 
Returns some value for an expression.
oneValue :: a -> Maybe a  Deterministic 
Returns just one value for an expression.
allSolutions :: Data a => (a -> Bool) -> [a]  Deterministic 
Returns all values satisfying a predicate, i.e., all arguments such that the predicate applied to the argument can be evaluated to True.
someSolution :: Data a => (a -> Bool) -> a  Deterministic 
Returns some value satisfying a predicate, i.e., some argument such that the predicate applied to the argument can be evaluated to True.
oneSolution :: Data a => (a -> Bool) -> Maybe a  Deterministic 
Returns just one value satisfying a predicate.
isFail :: a -> Bool  Deterministic 
Does the computation of the argument to a head-normal form fail? Conceptually, the argument is evaluated on a copy, i.e., even if the computation does not fail, it has not been evaluated.
rewriteAll :: a -> [a]  Deterministic 
Gets all values computable by term rewriting.
rewriteSome :: a -> Maybe a  Deterministic 
Similarly to rewriteAll but returns only some value computable by term rewriting.

Exported operations:

getAllValues :: a -> IO [a]  Deterministic 

Gets all values of an expression (similarly to Prolog's findall). Conceptually, all values are computed on a copy of the expression, i.e., the evaluation of the expression does not share any results. In PAKCS, the evaluation suspends as long as the expression contains unbound variables or the computed values contain unbound variables.

getOneValue :: a -> IO (Maybe a)  Deterministic 

Gets one value of an expression. Returns Nothing if the search space is finitely failed. Conceptually, the value is computed on a copy of the expression, i.e., the evaluation of the expression does not share any results. In PAKCS, the evaluation suspends as long as the expression contains unbound variables or the computed value contains unbound variables.

getAllSolutions :: Data a => (a -> Bool) -> IO [a]  Deterministic 

Gets all solutions to a constraint. 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.

getOneSolution :: Data a => (a -> Bool) -> IO (Maybe a)  Deterministic 

Gets one solution to a constraint. Returns Nothing if the search space is finitely failed.

getAllFailures :: a -> (a -> Bool) -> IO [a]  Deterministic 

Returns a list of values that do not satisfy a given constraint.

Example call:
(getAllFailures x c)
Parameters:
  • x : an expression (a generator evaluable to various values)
  • c : a constraint that should not be satisfied
Returns:
A list of all values of e such that (c e) is not provable

allValues :: a -> [a]  Deterministic 

Returns all values of an expression. Conceptually, all values are computed on a copy of the expression, i.e., the evaluation of the expression does not share any results. In PAKCS, the evaluation suspends as long as the expression contains unbound variables or the computed values contain 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  Deterministic 

Returns some value for an expression. 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. In PAKCS, the evaluation suspends as long as the expression contains unbound variables or the computed value 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.

oneValue :: a -> Maybe a  Deterministic 

Returns just one value for an expression. If the expression has no value, Nothing is returned. Conceptually, the value is computed on a copy of the expression, i.e., the evaluation of the expression does not share any results. In PAKCS, the evaluation suspends as long as the expression contains unbound variables or the computed value 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 :: Data a => (a -> Bool) -> [a]  Deterministic 

Returns all values satisfying a predicate, i.e., all arguments such that the predicate applied to the argument can be evaluated to True. In PAKCS, the evaluation suspends as long as the predicate expression contains unbound variables or the computed values contain 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 :: Data a => (a -> Bool) -> a  Deterministic 

Returns some value satisfying a predicate, i.e., some argument such that the predicate applied to the argument can be evaluated to True. 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.

oneSolution :: Data a => (a -> Bool) -> Maybe a  Deterministic 

Returns just one value satisfying a predicate. If there is no such value, Nothing is returned

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.

isFail :: a -> Bool  Deterministic 

Does the computation of the argument to a head-normal form fail? Conceptually, the argument is evaluated on a copy, i.e., even if the computation does not fail, it has not been evaluated.

rewriteAll :: a -> [a]  Deterministic 

Gets all values computable by term rewriting. In contrast to allValues, 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.

rewriteSome :: a -> Maybe a  Deterministic 

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