Commit 86990b8a authored by Michael Hanus 's avatar Michael Hanus

Synched with lib-trunk

parent 1b7709e3
------------------------------------------------------------------------------
--- 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 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>
------------------------------------------------------------------------------
--- 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
------------------------------------------------------------------------------
--- 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
<?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>
This diff is collapsed.
------------------------------------------------------------------------------
--- The library provides some operations to format values of basic
--- data types with arbitrary flags similarly to the `printf` statement of C.
---
--- These operations are used for the translation of integrated
--- code with the format tag to replace the format specifiers.
---
--- This library follows the C specification for the formatting. This
--- specification may be found at
--- <http://pubs.opengroup.org/onlinepubs/009695399/functions/fprintf.html>
---
--- @author Jasper Sikorra - jsi@informatik.uni-kiel.de
--- @version November 2017
--- @category general
------------------------------------------------------------------------------
module Format(showChar,showInt,showFloat,showString) where
import Char
import Integer
import Float
import List
import ReadNumeric
-- Basic type for show functions
type ShowSpec a = Typ -> Maybe Flag -> Maybe Width -> Maybe Precision
-> a -> String
type Typ = Char
type Flag = String
type Width = Int
type Precision = Int
--- The function showChar formats a character
--- @param type - will be ignored
--- @param flags - a string, everything but the minus char will be ignored
--- @param width - the minimal number of characters to be printed
--- @param precision - will be ignored
--- @param char - The char which should be formatted
--- @return A string containing the formatted character
showChar :: ShowSpec Char
showChar _ mf mw _ c =
let flags = convertFlags mf
width = convertWidth mw
minusFlag = getMinusFlag flags
cToString = [c]
in if minusFlag then fillWithCharsLeftAlign width ' ' cToString
else fillWithCharsRightAlign width ' ' cToString
--- The function showInt formats an Int
--- @param t - A char setting the way of number representation
--- @param mf - A string containing all flags
--- @param mw - The minimal number of characters to be printed
--- @param mp - The minimal number of numbers to be printed
--- @param i - The Int which should be formatted
--- @return A string containing the formatted Int
showInt :: ShowSpec Int
showInt t mf mw mp i =
-- convert to better format