Skip to content

GitLab

Commit fb183378 authored by Michael Hanus's avatar Michael Hanus
Browse files

Libraries AllSolutions, Combinatorial, Findall, Random, SearchTree*,... 

Libraries AllSolutions, Combinatorial, Findall, Random, SearchTree*, SetFunctions, Traversal ValueSequence removed (available in packages)
parent 2aa68cf1
Expand all Hide whitespace changes
Inline Side-by-side
Combinatorial.curry deleted 100644 → 0
View file @ 2aa68cf1
------------------------------------------------------------------------------
--- 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 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
Findall.curry deleted 100644 → 0
View file @ 2aa68cf1
------------------------------------------------------------------------------
--- Library with some operations for encapsulating search.
--- 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 `SetFunctions`),
--- which should be used.
---
--- In previous versions of PAKCS, some of these operations were part of
--- the standard prelude. We keep them in this separate module
--- in order to support a more portable standard prelude.
---
--- @author Michael Hanus
--- @version September 2018
--- @category general
------------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# OPTIONS_CYMAKE -Wno-incomplete-patterns #-}
module Findall
( getAllValues, getSomeValue
, allValues, someValue, oneValue
, allSolutions, someSolution
, isFail
#ifdef __PAKCS__
, try, inject, solveAll, once, best
, findall, findfirst, browse, browseList, unpack
, rewriteAll, rewriteSome
#endif
) where
#ifdef __PAKCS__
#else
import qualified SearchTree as ST
#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. In PAKCS, the evaluation suspends
--- as long as the expression contains unbound variables.
--- Similar to Prolog's findall.
getAllValues :: a -> IO [a]
getAllValues e = return (allValues e)
--- Gets a value of an expression (currently, via an incomplete
--- depth-first strategy). The expression must have a value, otherwise
--- 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.
getSomeValue :: a -> IO a
getSomeValue e = return (someValue e)
--- Returns 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. In PAKCS, the evaluation suspends as long as the expression
--- contains 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.
allValues :: a -> [a]
#ifdef __PAKCS__
allValues external
#else
allValues e = ST.allValuesDFS (ST.someSearchTree e)
#endif
--- Returns some value for an expression (currently, via an incomplete
--- depth-first strategy). 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.
---
--- 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.
someValue :: a -> a
#ifdef __PAKCS__
someValue external
#else
someValue = ST.someValueWith ST.dfsStrategy
#endif
--- Returns just one value for an expression (currently, via an incomplete
--- depth-first strategy). 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.
---
--- 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
#ifdef __PAKCS__
oneValue external
#else
oneValue x =
let vals = ST.allValuesWith ST.dfsStrategy (ST.someSearchTree x)
in (if null vals then Nothing else Just (head vals))
#endif
--- Returns all values satisfying a predicate, i.e., all arguments such that
--- the predicate applied to the argument can be evaluated to `True`
--- (currently, via an incomplete depth-first strategy).
--- In PAKCS, the evaluation suspends as long as the predicate expression
--- contains 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.
allSolutions :: (a->Bool) -> [a]
#ifdef __PAKCS__
allSolutions p = findall (\x -> p x =:= True)
#else
allSolutions p = allValues (let x free in p x &> x)
#endif
--- Returns some values satisfying a predicate, i.e., some argument such that
--- the predicate applied to the argument can be evaluated to `True`
--- (currently, via an incomplete depth-first strategy).
--- 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.
someSolution :: (a->Bool) -> a
#ifdef __PAKCS__
someSolution p = findfirst (\x -> p x =:= True)
#else
someSolution p = someValue (let x free in p x &> x)
#endif
--- 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.
isFail :: a -> Bool
#ifdef __PAKCS__
isFail external
#else
isFail x = null (allValues (x `seq` ()))
#endif
#ifdef __PAKCS__
------------------------------------------------------------------------------
--- Basic search control operator.
try :: (a -> Bool) -> [a -> Bool]
try external
--- Inject operator which adds the application of the unary
--- procedure p to the search variable to the search goal
--- taken from Oz. p x comes before g x to enable a test+generate
--- form in a sequential implementation.
inject :: (a -> Bool) -> (a -> Bool) -> (a -> Bool)
inject g p = \x -> p x & g x
--- Computes all solutions via a a depth-first strategy.
--
-- Works as the following algorithm:
--
-- solveAll g = evalResult (try g)
-- where
-- evalResult [] = []
-- evalResult [s] = [s]
-- evalResult (a:b:c) = concatMap solveAll (a:b:c)
--
-- The following solveAll algorithm is faster.
-- For comparison we have solveAll2, which implements the above algorithm.
solveAll :: (a -> Bool) -> [a -> Bool]
solveAll g = evalall (try g)
where
evalall [] = []
evalall [a] = [a]
evalall (a:b:c) = evalall3 (try a) (b:c)
evalall2 [] = []
evalall2 (a:b) = evalall3 (try a) b
evalall3 [] b = evalall2 b
evalall3 [l] b = l : evalall2 b
evalall3 (c:d:e) b = evalall3 (try c) (d:e ++b)
solveAll2 :: (a -> Bool) -> [a -> Bool]
solveAll2 g = evalResult (try g)
where
evalResult [] = []
evalResult [s] = [s]
evalResult (a:b:c) = concatMap solveAll2 (a:b:c)
--- Gets the first solution via a depth-first strategy.
once :: (a -> Bool) -> (a -> Bool)
once g = head (solveAll g)
--- Gets the best solution via a depth-first strategy according to
--- a specified operator that can always take a decision which
--- of two solutions is better.
--- In general, the comparison operation should be rigid in its arguments!
best :: (a -> Bool) -> (a -> a -> Bool) -> [a -> Bool]
best g cmp = bestHelp [] (try g) []
where
bestHelp [] [] curbest = curbest
bestHelp [] (y:ys) curbest = evalY (try (constrain y curbest)) ys curbest
bestHelp (x:xs) ys curbest = evalX (try x) xs ys curbest
evalY [] ys curbest = bestHelp [] ys curbest
evalY [newbest] ys _ = bestHelp [] ys [newbest]
evalY (c:d:xs) ys curbest = bestHelp (c:d:xs) ys curbest
evalX [] xs ys curbest = bestHelp xs ys curbest
evalX [newbest] xs ys _ = bestHelp [] (xs++ys) [newbest]
evalX (c:d:e) xs ys curbest = bestHelp ((c:d:e)++xs) ys curbest
constrain y [] = y
constrain y [curbest] =
inject y (\v -> let w free in curbest w & cmp v w =:= True)
--- Gets all solutions via a depth-first strategy and unpack
--- the values from the lambda-abstractions.
--- Similar to Prolog's findall.
findall :: (a -> Bool) -> [a]
findall external
--- Gets the first solution via a depth-first strategy
--- and unpack the values from the search goals.
findfirst :: (a -> Bool) -> a
findfirst external
--- Shows the solution of a solved constraint.
browse :: Show a => (a -> Bool) -> IO ()
browse g = putStr (show (unpack g))
--- Unpacks solutions from a list of lambda abstractions and write
--- them to the screen.
browseList :: Show a => [a -> Bool] -> IO ()
browseList [] = done
browseList (g:gs) = browse g >> putChar '\n' >> browseList gs
--- Unpacks a solution's value from a (solved) search goal.
unpack :: (a -> Bool) -> a
unpack g | g x = x where x free
--- Gets all values computable by term rewriting.
--- In contrast to `findall`, 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.
rewriteAll :: a -> [a]
rewriteAll external
--- Similarly to 'rewriteAll' but returns only some value computable
--- by term rewriting. Returns `Nothing` if there is no such value.
rewriteSome :: a -> Maybe a
rewriteSome external
#endif
Findall.pakcs deleted 100644 → 0
View file @ 2aa68cf1
<?xml version="1.0" standalone="no"?>
<!DOCTYPE primitives SYSTEM "http://www.informatik.uni-kiel.de/~pakcs/primitives.dtd">
<primitives>
<primitive name="allValues" arity="1">
<library>prim_standard</library>
<entry>prim_allValues[raw]</entry>
</primitive>
<primitive name="someValue" arity="1">
<library>prim_standard</library>
<entry>prim_someValue[raw]</entry>
</primitive>
<primitive name="oneValue" arity="1">
<library>prim_standard</library>
<entry>prim_oneValue[raw]</entry>
</primitive>
<primitive name="findall" arity="1">
<library>prim_standard</library>
<entry>prim_findall[raw]</entry>
</primitive>
<primitive name="findfirst" arity="1">
<library>prim_standard</library>
<entry>prim_findfirst[raw]</entry>
</primitive>
<primitive name="isFail" arity="1">
<library>prim_standard</library>
<entry>prim_isFail[raw]</entry>
</primitive>
<primitive name="try" arity="1">
<library>prim_standard</library>
<entry>prim_try[raw]</entry>
</primitive>
<primitive name="rewriteAll" arity="1">
<library>prim_standard</library>
<entry>prim_rewriteAll[raw]</entry>
</primitive>
<primitive name="rewriteSome" arity="1">
<library>prim_standard</library>
<entry>prim_rewriteSome[raw]</entry>
</primitive>
</primitives>
FiniteMap.curry deleted 100644 → 0
View file @ 2aa68cf1
This diff is collapsed.
Random.curry deleted 100644 → 0
View file @ 2aa68cf1
------------------------------------------------------------------------------
--- Library for pseudo-random number generation in Curry.
---
--- This library provides operations for generating pseudo-random
--- number sequences.
--- For any given seed, the sequences generated by the operations
--- in this module should be **identical** to the sequences
--- generated by the `java.util.Random package`.
---
------------------------------------------------------------------------------
--- The KiCS2 implementation is based on an algorithm taken from
--- <http://en.wikipedia.org/wiki/Random_number_generation>.
--- There is an assumption that all operations are implicitly
--- executed mod 2^32 (unsigned 32-bit integers) !!!
--- GHC computes between -2^29 and 2^29-1, thus the sequence
--- is NOT as random as one would like.
---
--- m_w = <choose-initializer>; /* must not be zero */
--- m_z = <choose-initializer>; /* must not be zero */
---
--- uint get_random()
--- {
--- m_z = 36969 * (m_z & 65535) + (m_z >> 16);
--- m_w = 18000 * (m_w & 65535) + (m_w >> 16);
--- return (m_z << 16) + m_w; /* 32-bit result */
--- }
---
------------------------------------------------------------------------------
--- The PAKCS implementation is a linear congruential pseudo-random number
--- generator described in
--- Donald E. Knuth, _The Art of Computer Programming_,
--- Volume 2: _Seminumerical Algorithms_, section 3.2.1.
---
------------------------------------------------------------------------------
--- @author Sergio Antoy (with extensions by Michael Hanus)
--- @version June 2017
--- @category algorithm
------------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
module Random
( nextInt, nextIntRange, nextBoolean, getRandomSeed
, shuffle
) where
import System ( getCPUTime )
import Time
#ifdef __PAKCS__
------------------------------------------------------------------
-- Private Operations
------------------------------------------------------------------
-- a few constants
multiplier :: Int
multiplier = 25214903917
addend :: Int
addend = 11
powermask :: Int
powermask = 48
mask :: Int
mask = 281474976710656 -- 2^powermask
intsize :: Int
intsize = 32
intspan :: Int
intspan = 4294967296 -- 2^intsize
intlimit :: Int
intlimit = 2147483648 -- 2^(intsize-1)
-- the basic sequence of random values
sequence :: Int -> [Int]
sequence seed = next : sequence next
where next = nextseed seed
-- auxiliary private operations
nextseed :: Int -> Int
nextseed seed = (seed * multiplier + addend) `rem` mask
xor :: Int -> Int -> Int
xor x y = if (x==0) && (y==0) then 0 else lastBit + 2 * restBits
where lastBit = if (x `rem` 2) == (y `rem` 2) then 0 else 1
restBits = xor (x `quot` 2) (y `quot` 2)
power :: Int -> Int -> Int
power base exp = binary 1 base exp
where binary x b e
= if (e == 0) then x
else binary (x * if (e `rem` 2 == 1) then b else 1)
(b * b)
(e `quot` 2)
nextIntBits :: Int -> Int -> [Int]
nextIntBits seed bits = map adjust list
where init = (xor seed multiplier) `rem` mask
list = sequence init
shift = power 2 (powermask - bits)
adjust x = if arg > intlimit then arg - intspan
else arg
where arg = (x `quot` shift) `rem` intspan
#else
zfact :: Int
zfact = 36969
wfact :: Int
wfact = 18000
two16 :: Int
two16 = 65536
large :: Int
large = 536870911 -- 2^29 - 1
#endif
------------------------------------------------------------------
-- Public Operations
------------------------------------------------------------------
--- Returns a sequence of pseudorandom, integer values.
---
--- @param seed - The seed of the random sequence.
nextInt :: Int -> [Int]
#ifdef __PAKCS__
nextInt seed = nextIntBits seed intsize
#else
nextInt seed =
let ns = if seed == 0 then 1 else seed
next2 mw mz =
let mza = zfact * (mz `mod` two16) + (mz * two16)
mwa = wfact * (mw `mod` two16) + (mw * two16)
tmp = (mza `div` two16 + mwa)
res = if tmp < 0 then tmp+large else tmp
in res : next2 mwa mza
in next2 ns ns
#endif
--- Returns a pseudorandom sequence of values
--- between 0 (inclusive) and the specified value (exclusive).
---
--- @param seed - The seed of the random sequence.
--- @param n - The bound on the random number to be returned.
--- Must be positive.
nextIntRange :: Int -> Int -> [Int]
#ifdef __PAKCS__
nextIntRange seed n | n>0
= if power_of_2 n then map adjust_a seq
else map adjust_b (filter adjust_c seq)
where seq = nextIntBits seed (intsize - 1)
adjust_a x = (n * x) `quot` intlimit
adjust_b x = x `rem` n
adjust_c x = x - (x `rem` n) + (n - 1) >= 0
power_of_2 k = k == 2 ||
k > 2 && k `rem` 2 == 0 && power_of_2 (k `quot` 2)
#else
nextIntRange seed n | n>0
= map (`mod` n) (nextInt seed)
#endif
--- Returns a pseudorandom sequence of boolean values.
---
--- @param seed - The seed of the random sequence.
nextBoolean :: Int -> [Bool]
#ifdef __PAKCS__
nextBoolean seed = map (/= 0) (nextIntBits seed 1)
#else
nextBoolean seed = map (/= 0) (nextInt seed)
#endif
--- Returns a time-dependent integer number as a seed for really random numbers.
--- Should only be used as a seed for pseudorandom number sequence
--- and not as a random number since the precision is limited to milliseconds
getRandomSeed :: IO Int
getRandomSeed =
getClockTime >>= \time ->
getCPUTime >>= \msecs ->
let (CalendarTime y mo d h m s _) = toUTCTime time
#ifdef __PAKCS__
in return ((y+mo+d+h+(m+1)*(s+1)*(msecs+1)) `rem` mask)
#else
in return ((y+mo+d+h+(m+1)*(s+1)*(msecs+1)) `mod` two16)
#endif
--- Computes a random permutation of the given list.
---
--- @param rnd random seed
--- @param l lists to shuffle
--- @return shuffled list