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

------------------------------------------------------------------------------
-- | Author : Michael Hanus
--   Version: October 2023
--
-- 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`.
------------------------------------------------------------------------------

module Control.Search.AllValues
  ( getAllValues, getOneValue, getAllFailures )
 where

import Control.Search.Unsafe

------------------------------------------------------------------------------

-- | 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.
getAllValues :: a -> IO [a]
getAllValues e = return (allValues e)

-- | 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.
getOneValue :: a -> IO (Maybe a)
getOneValue x = return (oneValue x)

-- | Returns a list of values that do not satisfy a given constraint.
-- As a simple example, the expression
--
--     getAllFailures ([] ? [1] ? [2]) (\xs -> head xs =:= 1)
--
-- evaluates to `[[], [2]]`.
getAllFailures :: a           -- ^ an expression ´e´ (e.g., a generator
                              --   evaluable to various values)
               -> (a -> Bool) -- ^ a constraint ´c´ that should not be satisfied
               -> IO [a]      -- ^ list of all values of `e`
                              --   such that `(c e)` is not provable
getAllFailures generator test = do
  xs <- getAllValues generator
  failures <- mapM (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 = getOneValue (c x) >>= return . maybe [x] (const [])

------------------------------------------------------------------------------