tamarin-prover-utils-0.8.5.1: Utility library for the tamarin prover.

MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellSafe-Inferred

Extension.Prelude

Description

Functions that could/should have made it into the Prelude or one of the base libraries

Synopsis

Documentation

implies :: Bool -> Bool -> BoolSource

singleton :: a -> [a]Source

unique :: Eq a => [a] -> BoolSource

check whether the given list contains no duplicates

sortednub :: Ord a => [a] -> [a]Source

Sort list and remove duplicates. O(n*log n)

sortednubBy :: (a -> a -> Ordering) -> [a] -> [a]Source

Sort a list according to a user-defined comparison function and remove duplicates.

sortednubOn :: Ord b => (a -> b) -> [a] -> [a]Source

O(n*log n). Sort list and remove duplicates with respect to a projection.

nubOn :: Eq b => (a -> b) -> [a] -> [a]Source

Keep only the first element of elements having the same projected value

groupOn :: Eq b => (a -> b) -> [a] -> [[a]]Source

O(n). Group on a projection of the data to group

sortOn :: Ord b => (a -> b) -> [a] -> [a]Source

sort on a projection of the data to sort

sortOnMemo :: Ord b => (a -> b) -> [a] -> [a]Source

sort on a projection of the data to sort, memorizing the results of the projection in order to avoid recomputation.

groupSortOn :: Ord b => (a -> b) -> [a] -> [[a]]Source

sort and group on a projection

eqClasses :: (Eq b, Ord b) => (a -> b) -> [a] -> [[a]]Source

partition the given set into equality classes with respect to the representative given by the projection function

eqClassesBy :: (b -> b -> Ordering) -> (a -> b) -> [a] -> [[a]]Source

splitBy :: (a -> Bool) -> [a] -> [[a]]Source

split a list into sublists whenever the predicate identifies an element as a separator. Note that the separator is not retained and a separator at the very end is ignored.

choose :: Int -> [a] -> [[a]]Source

the list of all permutations of a given list permutations :: [a] -> [[a]] permutations [] = [[]] permutations zs = aux zs [] where aux [] _ = [] aux (x:xs) ys = [x:p | p <- permutations (xs++ys)] ++ aux xs (x:ys)

the list of all combinations of n elements of a list. E.g. choose 2 [1,2,3] = [[1,2],[1,3],[2,3]]

leaveOneOut :: [a] -> [[a]]Source

build the list of lists each leaving another element out. (From left to right)

keepFirst :: (a -> a -> Bool) -> [a] -> [a]Source

An element masks another element if the predicate is true. This function keeps only the elements not masked by a previous element in the list.

swap :: (a, b) -> (b, a)Source

These functions were inspired by the ML library accompanying the Isabelle theorem prover (http://isabelle.in.tum.de/)

swap the elements of a pair

sortPair :: Ord a => (a, a) -> (a, a)Source

sort the elements of a pair

isRight :: Either a b -> BoolSource

isLeft :: Either a b -> BoolSource

type Named a = (String, a)Source

Name values of a given type

flushRightBy :: [a] -> Int -> [a] -> [a]Source

Extend a list with the given separators to be flushed right.

flushRight :: Int -> String -> StringSource

Extend a string with spaces to be flushed right.

flushLeftBy :: [a] -> Int -> [a] -> [a]Source

Extend a list with the given separators to be flushed left.

flushLeft :: Int -> String -> StringSource

Extend a string with spaces to be flushed left.

warning :: String -> StringSource

marks a string as being a warning

putErr :: String -> IO ()Source

abbreviation to print to stderr

putErrLn :: String -> IO ()Source

abbreviation to println to stderr

oneOfList :: Alternative f => [a] -> f aSource

Inject the elements of a list as alternatives.

oneOfSet :: Alternative f => Set a -> f aSource

Inject the elements of a set as alternatives.

oneOfMap :: Alternative f => Map k v -> f (k, v)Source

Inject the elements of a map as alternatives.

ifM :: Monad m => m Bool -> m a -> m a -> m aSource

A monadic if statement

errorFree :: MonadPlus m => [m a] -> m [a]Source

Gather all error free computations.

errorFree1 :: MonadPlus m => [m a] -> m [a]Source

Gather all error free computations and ensure that at least one was error free.

unreachable :: String -> aSource

Mark a part of the code as unreachable.