Commit 5cbfd658 authored by Kai-Oliver Prott's avatar Kai-Oliver Prott
Browse files

Remove Modules that should not be in base package

parent 0bc804f5
------------------------------------------------------------------------------
--- 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.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)
-- defined in terms of the monad instance for StateT
instance (Functor m, Monad m) => Applicative (StateT s m) where
pure = return
f <*> v = f >>= (\f' -> v >>= (\x -> return (f' x)))
instance (Monad m) => Monad (StateT s m) where
m >>= k = StateT (\ s -> do ~(a, s') <- runStateT m s
runStateT (k a) s')
return a = StateT (\ s -> return (a, s))
fail str = StateT (\ _ -> fail str)
instance MonadTrans (StateT s) where
lift m = StateT (\ s -> do a <- m
return (a, s))
state :: Monad m => (s -> (a, s)) -> StateT s m a
state f = StateT (return . f)
get :: Monad m => StateT s m s
get = state (\ s -> (s, s))
put :: Monad m => s -> StateT s m ()
put s = state (\ _ -> ((), s))
modify :: Monad m => (s -> s) -> StateT s m ()
modify f = state (\ s -> ((), f s))
type State s = StateT s Identity
runState :: State s a -> s -> (a, s)
runState m = runIdentity . runStateT m
evalState :: State s a -> s -> a
evalState m s = fst (runState m s)
execState :: State s a -> s -> s
execState m s = snd (runState m s)
evalStateT :: (Monad m) => StateT s m a -> s -> m a
evalStateT m s = do
~(a, _) <- runStateT m s
return a
execStateT :: (Monad m) => StateT s m a -> s -> m s
execStateT m s = do
~(_, s') <- runStateT m s
return s'
--- ----------------------------------------------------------------------------
--- This module provides some utility functions for inverting functions.
---
--- @author Michael Hanus
--- @version February 2015
--- @category general
--- ----------------------------------------------------------------------------
module Data.Function.Inversion where
--- Inverts a unary function.
invf1 :: (a -> b) -> (b -> a)
invf1 f y | f x =:<= y = x where x free
--- Inverts a binary function.
invf2 :: (a -> b -> c) -> (c -> (a,b))
invf2 f y | f x1 x2 =:<= y = (x1,x2) where x1,x2 free
--- Inverts a ternary function.
invf3 :: (a -> b -> c -> d) -> (d -> (a,b,c))
invf3 f y | f x1 x2 x3 =:<= y = (x1,x2,x3) where x1,x2,x3 free
--- Inverts a function of arity 4.
invf4 :: (a -> b -> c -> d -> e) -> (e -> (a,b,c,d))
invf4 f y | f x1 x2 x3 x4 =:<= y = (x1,x2,x3,x4) where x1,x2,x3,x4 free
--- Inverts a function of arity 5.
invf5 :: (a -> b -> c -> d -> e -> f) -> (f -> (a,b,c,d,e))
invf5 f y | f x1 x2 x3 x4 x5 =:<= y = (x1,x2,x3,x4,x5) where x1,x2,x3,x4,x5 free
------------------------------------------------------------------------------
--- Library for handling global entities.
--- A global entity has a name declared in the program.
--- Its value can be accessed and modified by IO actions.
--- Furthermore, global entities can be declared as persistent so that
--- their values are stored across different program executions.
---
--- Currently, it is still experimental so that its interface might
--- be slightly changed in the future.
---
--- A global entity `g` with an initial value `v`
--- of type `t` must be declared by:
---
--- g :: Global t