Module Control.Search.AllValues

Library with operations to encapsulate search, i.e., non-deterministic computations, as I/O operations in order to make the results dependend on the external world, e.g., the schedule for non-determinism.

To encapsulate search in non-I/O computations, one can use set functions (see module Control.Search.SetFunctions.

Author: Michael Hanus

Version: October 2023

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.
getAllFailures :: a -> (a -> Bool) -> IO [a]  Deterministic 
Returns a list of values that do not satisfy a given constraint.

Exported operations:

getAllValues :: a -> IO [a]  Deterministic 

Gets all values of an expression (similarly to Prolog's findall). 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.

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.

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