Commit 3f07450a authored by Kai-Oliver Prott's avatar Kai-Oliver Prott

Add recent version3 changes

parent 54d9592d
------------------------------------------------------------------------------
--- This module contains a collection of functions for
--- obtaining lists of solutions to constraints.
--- These operations are useful to encapsulate
--- non-deterministic operations between I/O actions in
--- order to connect the worlds of logic and functional programming
--- and to avoid non-determinism failures on the I/O level.
---
--- In contrast the "old" concept of encapsulated search
--- (which could be applied to any subexpression in a computation),
--- the operations to encapsulate search in this module
--- are I/O actions in order to avoid some anomalities
--- in the old concept.
---
--- @category general
------------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
module AllSolutions
( getAllValues, getAllSolutions, getOneValue, getOneSolution
, getAllFailures
#ifdef __PAKCS__
, getSearchTree, SearchTree(..)
#endif
) where
#ifdef __PAKCS__
import Findall
#else
import Algorithm.SearchTree
#endif
--- 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.
getAllValues :: a -> IO [a]
#ifdef __PAKCS__
getAllValues e = return (findall (=:=e))
#else
getAllValues e = getSearchTree e >>= return . allValuesDFS
#endif
--- Gets one value of an expression (currently, via an incomplete
--- left-to-right strategy). Returns Nothing if the search space
--- is finitely failed.
getOneValue :: a -> IO (Maybe a)
#ifdef __PAKCS__
getOneValue x = getOneSolution (x=:=)
#else
getOneValue x = do
st <- getSearchTree x
let vals = allValuesDFS st
return (if null vals then Nothing else Just (head vals))
#endif
--- Gets all solutions to a constraint (currently, via an incomplete
--- depth-first left-to-right strategy). 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.
getAllSolutions :: (a->Bool) -> IO [a]
#ifdef __PAKCS__
getAllSolutions c = return (findall c)
#else
getAllSolutions c = getAllValues (let x free in (x,c x)) >>= return . map fst
#endif
--- Gets one solution to a constraint (currently, via an incomplete
--- left-to-right strategy). Returns Nothing if the search space
--- is finitely failed.
getOneSolution :: (a->Bool) -> IO (Maybe a)
getOneSolution c = do
sols <- getAllSolutions c
return (if null sols then Nothing else Just (head sols))
--- Returns a list of values that do not satisfy a given constraint.
--- @param x - an expression (a generator evaluable to various values)
--- @param c - a constraint that should not be satisfied
--- @return A list of all values of e such that (c e) is not provable
getAllFailures :: a -> (a -> Bool) -> IO [a]
getAllFailures generator test = do
xs <- getAllValues generator
failures <- mapIO (naf test) xs
return $ concat failures
-- (naf c x) returns [x] if (c x) fails, and [] otherwise.
naf :: (a -> Bool) -> a -> IO [a]
#ifdef __PAKCS__
naf c x = do
mbl <- getOneSolution (\_->c x)
return (maybe [x] (const []) mbl)
#else
naf c x = getOneSolution (lambda c x) >>= returner x
lambda :: (a -> Bool) -> a -> () -> Bool
lambda c x _ = c x
returner :: a -> Maybe b -> IO [a]
returner x mbl = return (maybe [x] (const []) mbl)
#endif
#ifdef __PAKCS__
--- A search tree for representing search structures.
data SearchTree a b = SearchBranch [(b,SearchTree a b)] | Solutions [a]
deriving (Eq,Show)
--- Computes a tree of solutions where the first argument determines
--- the branching level of the tree.
--- For each element in the list of the first argument,
--- the search tree contains a branch node with a child tree
--- for each value of this element. Moreover, evaluations of
--- elements in the branch list are shared within corresponding subtrees.
getSearchTree :: [a] -> (b -> Bool) -> IO (SearchTree b a)
getSearchTree cs goal = return (getSearchTreeUnsafe cs goal)
getSearchTreeUnsafe :: [a] -> (b -> Bool) -> (SearchTree b a)
getSearchTreeUnsafe [] goal = Solutions (findall goal)
getSearchTreeUnsafe (c:cs) goal =
SearchBranch (findall (=:=(solve c cs goal)))
solve :: a -> [a] -> (b -> Bool) -> (a,SearchTree b a)
solve c cs goal | c=:=y = (y, getSearchTreeUnsafe cs goal) where y free
#endif
<?xml version="1.0" standalone="no"?>
<!DOCTYPE primitives SYSTEM "http://www.informatik.uni-kiel.de/~pakcs/primitives.dtd">
<primitives>
<primitive name="getOneSolution" arity="1">
<library>prim_standard</library>
<entry>prim_getOneSolution[raw]</entry>
</primitive>
</primitives>
--- Implementation of Arrays with Braun Trees. Conceptually, Braun trees
--- are always infinite. Consequently, there is no test on emptiness.
---
--- @authors {bbr, fhu}@informatik.uni-kiel.de
--- @category algorithm
module Array
(Array,
emptyErrorArray, emptyDefaultArray,
listToDefaultArray,listToErrorArray,
(//), update, applyAt,
(!),
combine, combineSimilar)
where
infixl 9 !, //
data Array b = Array (Int -> b) (Entry b)
data Entry b = Entry b (Entry b) (Entry b) | Empty
--- Creates an empty array which generates errors for non-initialized
--- indexes.
emptyErrorArray :: Array b
emptyErrorArray = emptyDefaultArray errorArray
errorArray :: Int -> _
errorArray idx = error ("Array index "++show idx++" not initialized")
--- Creates an empty array, call given function for non-initialized
--- indexes.
--- @param default - function to call for each non-initialized index
emptyDefaultArray :: (Int -> b) -> Array b
emptyDefaultArray dflt = Array dflt Empty
--- Inserts a list of entries into an array.
--- @param array - array to modify
--- @param modifications - list of new (indexes,entries)
--- If an index in the list was already initialized, the old value
--- will be overwritten. Likewise the last entry with a given index
--- will be contained in the result array.
(//) :: Array b -> [(Int,b)] -> Array b
(//) (Array dflt array) modifications =
Array dflt
(foldr (\ (n,v) a -> at (dflt n) a n (const v)) array modifications)
--- Inserts a new entry into an array.
--- @param array - array to modify
--- @param idx - index of update
--- @param val - value to update at index idx
--- Entries already initialized will be overwritten.
update :: Array b -> Int -> b -> Array b
update (Array dflt a) i v =
Array dflt (at (dflt i) a i (const v))
--- Applies a function to an element.
--- @param array - array to modify
--- @param idx - index of update
--- @param fun - function to apply on element at index idx
applyAt :: Array b -> Int -> (b->b) -> Array b
applyAt (Array dflt a) n f = Array dflt (at (dflt n) a n f)
at :: b -> Entry b -> Int -> (b -> b) -> Entry b
at dflt Empty n f
| n==0 = Entry (f dflt) Empty Empty
| odd n = Entry dflt (at dflt Empty (n `div` 2) f) Empty
| otherwise = Entry dflt Empty (at dflt Empty (n `div` 2 - 1) f)
at dflt (Entry v al ar) n f
| n==0 = Entry (f v) al ar
| odd n = Entry v (at dflt al (n `div` 2) f) ar
| otherwise = Entry v al (at dflt ar (n `div` 2 - 1) f)
--- Yields the value at a given position.
--- @param a - array to look up in
--- @param n - index, where to look
(!) :: Array b -> Int -> b
(Array dflt array) ! i = from (dflt i) array i
from :: a -> Entry a -> Int -> a
from dflt Empty _ = dflt
from dflt (Entry v al ar) n
| n==0 = v
| odd n = from dflt al (n `div` 2)
| otherwise = from dflt ar (n `div` 2 - 1)
split :: [a] -> ([a],[a])
split [] = ([],[])
split [x] = ([x],[])
split (x:y:xys) = let (xs,ys) = split xys in
(x:xs,y:ys)
--- Creates a default array from a list of entries.
--- @param def - default funtion for non-initialized indexes
--- @param xs - list of entries
listToDefaultArray :: (Int -> b) -> [b] -> Array b
listToDefaultArray def = Array def . listToArray
--- Creates an error array from a list of entries.
--- @param xs - list of entries
listToErrorArray :: [b] -> Array b
listToErrorArray = listToDefaultArray errorArray
listToArray :: [b] -> Entry b
listToArray [] = Empty
listToArray (x:xs) = let (ys,zs) = split xs in
Entry x (listToArray ys)
(listToArray zs)
--- combine two arbitrary arrays
combine :: (a -> b -> c) -> Array a -> Array b -> Array c
combine f (Array def1 a1) (Array def2 a2) =
Array (\i -> f (def1 i) (def2 i)) (comb f def1 def2 a1 a2 0 1)
comb :: (a -> b -> c) -> (Int -> a) -> (Int -> b)
-> Entry a -> Entry b -> Int -> Int -> Entry c
comb _ _ _ Empty Empty _ _ = Empty
comb f def1 def2 (Entry x xl xr) Empty b o =
Entry (f x (def2 (b+o-1)))
(comb f def1 def2 xl Empty (2*b) o)
(comb f def1 def2 xr Empty (2*b) (o+b))
comb f def1 def2 Empty (Entry y yl yr) b o =
Entry (f (def1 (b+o-1)) y)
(comb f def1 def2 Empty yl (2*b) o)
(comb f def1 def2 Empty yr (2*b) (o+b))
comb f def1 def2 (Entry x xl xr) (Entry y yl yr) b o =
Entry (f x y)
(comb f def1 def2 xl yl (2*b) o)
(comb f def1 def2 xr yr (2*b) (o+b))
--- the combination of two arrays with identical default function
--- and a combinator which is neutral in the default
--- can be implemented much more efficient
combineSimilar :: (a -> a -> a) -> Array a -> Array a -> Array a
combineSimilar f (Array def a1) (Array _ a2) = Array def (combSim f a1 a2)
combSim :: (a -> a -> a) -> Entry a -> Entry a -> Entry a
combSim _ Empty a2 = a2
combSim _ (Entry x y z) Empty = Entry x y z
combSim f (Entry x xl xr) (Entry y yl yr) =
Entry (f x y) (combSim f xl yl) (combSim f xr yr)
------------------------------------------------------------------------------
--- A collection of common non-deterministic and/or combinatorial operations.
--- Many operations are intended to operate on sets.
--- The representation of these sets is not hidden; rather
--- sets are represented as lists.
--- Ideally these lists contains no duplicate elements and
--- the order of their elements cannot be observed.
--- In practice, these conditions are not enforced.
---
--- @author Sergio Antoy (with extensions by Michael Hanus)
--- @version April 2016
--- @category general
------------------------------------------------------------------------------
module Combinatorial(permute, subset, allSubsets, splitSet,
sizedSubset, partition) where
import Data.List(sum)
import SetFunctions
import Test.Prop
------------------------------------------------------------------------------
-- Public Operations
------------------------------------------------------------------------------
--- Compute any permutation of a list.
---
--- @param xs - The list.
--- @return A permutation of the argument.
permute :: [a] -> [a]
permute [] = []
permute (x:xs) = ndinsert (permute xs)
where ndinsert [] = [x]
ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
-- Properties:
permute1234 = permute [1,2,3,4] ~> [1,3,4,2]
-- The length of a permutation is identical to the length of the argument:
permLength xs = length (permute xs) <~> length xs -- lengths are equal
-- The permutation contains the same elements as the argument:
permElems xs = anyOf (permute xs) <~> anyOf xs
------------------------------------------------------------------------------
--- Compute any sublist of a list.
--- The sublist contains some of the elements of the list in the same order.
---
--- @param xs - The list.
--- @return A sublist of the argument.
subset :: [a] -> [a]
subset [] = []
subset (x:xs) = x:subset xs
subset (_:xs) = subset xs
-- Properties:
subset1234 = subset [1,2,3,4] ~> [1,3]
subset123 = subset [1,2,3] <~> ([1,2,3]?[1,2]?[1,3]?[1]?[2,3]?[2]?[3]?[])
subsetElems xs = anyOf (subset xs) <~ anyOf xs
------------------------------------------------------------------------------
--- Compute all the sublists of a list.
---
--- @param xs - The list.
--- @return All the sublists of the argument.
allSubsets :: Ord a => [a] -> [[a]]
allSubsets xs = sortValues (set1 subset xs)
-- Properties:
allSubsets123 =
allSubsets [1,2,3] -=- [[],[1],[1,2],[1,2,3],[1,3],[2],[2,3],[3]]
------------------------------------------------------------------------------
--- Split a list into any two sublists.
---
--- @param xs - The list.
--- @return A pair consisting of two complementary sublists of the argument.
splitSet :: [a] -> ([a],[a])
splitSet [] = ([],[])
splitSet (x:xs) = let (u,v) = splitSet xs in (x:u,v) ? (u,x:v)
-- Properties:
splitSet1234 = splitSet [1,2,3,4] ~> ([1,3,4],[2])
-- The sum of the length of the two sublists is the length of the argument list:
splitSetLengths xs =
(\ (xs,ys) -> length xs + length ys) (splitSet xs) <~> length xs
-- The two sublists and the argument list have the same elements:
splitSetElems xs =
(\ (xs,ys) -> anyOf xs ? anyOf ys) (splitSet xs) <~> anyOf xs
------------------------------------------------------------------------------
--- Compute any sublist of fixed length of a list.
--- Similar to 'subset', but the length of the result is fixed.
---
--- @param c - The length of the output sublist.
--- @param xs - The input list.
--- @return A sublist of `xs` of length `c`.
sizedSubset :: Int -> [a] -> [a]
sizedSubset c l = if c == 0 then [] else aux l
where aux (x:xs) = x:sizedSubset (c-1) xs ? sizedSubset c xs
-- Precondition:
sizedSubset'pre c _ = c>=0
-- Properties:
sizedSubsetLength c xs =
(c>=0 && length xs >= c) ==> length (sizedSubset c xs) <~> c
-- No result if the given output length is larger than the length of the input:
sizedSubsetLengthTooSmall c xs =
(c>=0 && length xs < c) ==> failing (sizedSubset c xs)
------------------------------------------------------------------------------
--- Compute any partition of a list.
--- The output is a list of non-empty lists such that their concatenation
--- is a permutation of the input list.
--- No guarantee is made on the order of the arguments in the output.
---
--- @param xs - The input list.
--- @return A partition of `xs` represented as a list of lists.
partition :: [a] -> [[a]]
partition [] = []
partition (x:xs) = insert x (partition xs)
where insert e [] = [[e]]
insert e (y:ys) = ((e:y):ys) ? (y:insert e ys)
-- Properties:
partition1234 = partition [1,2,3,4] ~> [[4],[2,3],[1]]
partition123 =
partition [1,2,3]
<~>
([[1,2,3]] ? [[2,3],[1]] ? [[1,3],[2]] ? [[3],[1,2]] ? [[3],[2],[1]])
-- The sum of the length of the sublists is the length of the argument list:
partitionLengths xs = sum (map length (partition xs)) <~> length xs
-- The sublists of the partition and the argument list have the same elements:
partitionElems xs = anyOf (map anyOf (partition xs)) <~> anyOf xs
-- end module Combinatorial
module Control.Applicative where
infixl 4 <*>, <*, *>
--- Typeclass for Applicative-Functors
class Functor f => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
(*>) :: f a -> f b -> f b
m *> n = (id <$ m) <*> n
(<*) :: f a -> f b -> f a
(<*) = liftA2 const
liftA2 :: (a -> b -> c) -> f a -> f b -> f c
liftA2 f x = (<*>) (fmap f x)
instance Applicative Maybe where
pure = Just
Just f <*> Just a = Just (f a)
Nothing <*> Just _ = Nothing
Just _ <*> Nothing = Nothing
Nothing <*> Nothing = Nothing
module Control.Applicative
( Applicative(..), liftA, liftA3, when
, sequenceA, sequenceA_
) where
--- Lift a function to actions.
--- This function may be used as a value for `fmap` in a `Functor` instance.
......@@ -33,3 +11,20 @@ liftA f a = pure f <*> a
--- Lift a ternary function to actions.
liftA3 :: Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 f a b c = liftA2 f a b <*> c
-- | Conditional execution of 'Applicative' expressions.
when :: (Applicative f) => Bool -> f () -> f ()
when p s = if p then s else pure ()
--- Evaluate each action in the list from left to right, and
--- collect the results. For a version that ignores the results
--- see 'sequenceA_'.
sequenceA :: (Applicative f) => [f a] -> f [a]
sequenceA [] = pure []
sequenceA (x:xs) = (:) <$> x <*> sequenceA xs
--- Evaluate each action in the structure from left to right, and
--- ignore the results. For a version that doesn't ignore the results
--- see 'sequenceA'.
sequenceA_ :: (Applicative f) => [f a] -> f ()
sequenceA_ = foldr (*>) (pure ())
module Control.Monad
( Functor(..), Applicative(..), Monad(..)
, filterM, (>=>), (<=<), forever, mapAndUnzipM, zipWithM
, zipWithM_, foldM, foldM_, replicateM, replicateM_
, when, unless
) where
import Control.Applicative
--- This generalizes the list-based 'filter' function.
filterM :: (Applicative m) => (a -> m Bool) -> [a] -> m [a]
filterM p = foldr (\ x -> liftA2 (\ flg -> if flg
then (x:)
else id)
(p x))
(pure [])
infixr 1 <=<, >=>
--- Left-to-right composition of Kleisli arrows.
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x -> f x >>= g
--- Right-to-left composition of Kleisli arrows. @('>=>')@, with the arguments
--- flipped.
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = flip (>=>)
--- Repeat an action indefinitely.
forever :: (Applicative f) => f a -> f b
forever a = let a' = a *> a' in a'
-- -----------------------------------------------------------------------------
-- Other monad functions
--- The 'mapAndUnzipM' function maps its first argument over a list, returning
--- the result as a pair of lists. This function is mainly used with complicated
--- data structures or a state-transforming monad.
mapAndUnzipM :: (Applicative m) => (a -> m (b,c)) -> [a] -> m ([b], [c])
mapAndUnzipM f xs = unzip <$> sequenceA (map f xs)
--- The 'zipWithM' function generalizes 'zipWith' to
--- arbitrary applicative functors.
zipWithM :: (Applicative m) => (a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM f xs ys = sequenceA (zipWith f xs ys)
--- 'zipWithM_' is the extension of 'zipWithM' which ignores the final result.
zipWithM_ :: (Applicative m) => (a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ f xs ys = sequenceA_ (zipWith f xs ys)
--- The 'foldM' function is analogous to 'foldl', except that its result is
--- encapsulated in a monad.
foldM :: (Monad m) => (b -> a -> m b) -> b -> [a] -> m b
foldM f z0 xs = foldr f' return xs z0
where f' x k z = f z x >>= k
--- Like 'foldM', but discards the result.
foldM_ :: (Monad m) => (b -> a -> m b) -> b -> [a] -> m ()
foldM_ f a xs = foldM f a xs >> return ()
--- @'replicateM' n act@ performs the action @n@ times,
--- gathering the results.
replicateM :: (Applicative m) => Int -> m a -> m [a]
replicateM cnt0 f =
loop cnt0
where
loop cnt
| cnt <= 0 = pure []
| otherwise = liftA2 (:) f (loop (cnt - 1))
--- Like 'replicateM', but discards the result.
replicateM_ :: (Applicative m) => Int -> m a -> m ()
replicateM_ cnt0 f =
loop cnt0
where
loop cnt
| cnt <= 0 = pure ()
| otherwise = f *> loop (cnt - 1)
--- The reverse of 'when'.
unless :: (Applicative f) => Bool -> f () -> f ()
unless p s = if p then pure () else s
module Control.Monad.Extra where
--- Same as `concatMap`, but for a monadic function.
concatMapM :: (Functor m, Monad m) => (a -> m [b]) -> [a] -> m [b]
concatMapM f xs = concat <$> mapM f xs
--- Same as `mapM` but with an additional accumulator threaded through.
mapAccumM :: Monad m => (a -> b -> m (a, c))
-> a -> [b] -> m (a, [c])
mapAccumM _ s [] = return (s, [])
mapAccumM f s (x : xs) = f s x >>= (\(s', x') -> (mapAccumM f s' xs) >>=
(\(s'', xs') -> return (s'', x' : xs')))
module Control.Monad.Trans.Class where
class MonadTrans t where
lift :: (Monad m) => m a -> t m a
--- ---------------------------------------------------------------------------
--- This monad transformer adds the ability to fail
--- or throw exceptions to a monad.
---
--- @author Bjoern Peemoeller
--- @version September 2014
--- @category general
--- ----------------------------------------------------------------------------
module Control.Monad.Trans.Error (
module Control.Monad.Trans.Error,
module Control.Monad.Trans.Class
) where
import Data.Either
import Data.Functor.Identity
import Control.Monad.Trans.Class
import Control.Applicative
--- Error monad.
newtype ErrorT e m a = ErrorT { runErrorT :: m (Either e a) }
class Error a where
noMsg :: a
noMsg = strMsg ""
strMsg :: String -> a
strMsg _ = noMsg
class ErrorList a where
listMsg :: String -> [a]
instance ErrorList Char where
listMsg = id
instance ErrorList a => Error [a] where
strMsg = listMsg
instance (Functor m) => Functor (ErrorT e m) where
fmap f = ErrorT . fmap (fmap f) . runErrorT
-- defined in terms of the monad instance for ErrorT
instance (Functor m, Monad m, Error e) => Applicative (ErrorT e m) where
pure = return
f <*> v = f >>= (\f' -> v >>= (\x -> return (f' x)))
instance (Monad m, Error e) => Monad (ErrorT e m) where
return a = ErrorT $ return (Right a)
m >>= k = ErrorT (do a <- runErrorT m
case a of
Left l -> return (Left l)
Right r -> runErrorT (k r))
fail msg = ErrorT $ return (Left (strMsg msg))
instance MonadTrans (ErrorT e) where
lift m = ErrorT (do a <- m
return (Right a))
-- Signal an error value e.
throwError :: (Monad m) => e -> ErrorT e m a
throwError l = ErrorT $ return (Left l)
-- Handle an error.
catchError :: (Monad m) => ErrorT e m a -> (e -> ErrorT e m a) -> ErrorT e m a
catchError m h = ErrorT (do a <- runErrorT m
case a of
Left l -> runErrorT (h l)
Right r -> return (Right r))
runError :: ErrorT e Identity a -> Either e a
runError = runIdentity . runErrorT
------------------------------------------------------------------------------
--- This library provides an implementation of the state monad.
---
--- @author Jan-Hendrik Matthes, Bjoern Peemoeller, Fabian Skrlac
--- @version August 2016
--- @category general
------------------------------------------------------------------------------
module Control.Monad.Trans.State
( State, StateT(runStateT)
, evalStateT, execStateT
, get, put, modify, runState, evalState, execState
, module Control.Monad.Trans.Class
) where
import Control.Monad.Trans.Class
import Data.Functor.Identity
import Control.Applicative
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
instance (Functor m) => Functor (StateT s m) where
fmap f m = StateT (\ s ->
fmap (\ ~(a, s') -> (f a, s')) $ runStateT m s)
<