haskhol-core-1.1.0: src/HaskHOL/Core/Lib.hs
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables #-}
{-|
Module: HaskHOL.Core.Lib
Copyright: (c) The University of Kansas 2013
LICENSE: BSD3
Maintainer: ecaustin@ittc.ku.edu
Stability: unstable
Portability: unknown
This module defines or re-exports common utility functions, type classes,
and auxilliary data types used in HaskHOL. The following conventions hold
true:
* Where possible, we favor re-exporting common functions rather than
redefining them.
* We favor re-exporting individual functions rather entire modules to reduce
the number of items in our utility library.
* We default to the names of functions commonly used by Haskell libraries,
however, if there's a different name for a function in HOL systems we
include an alias for it. For example, 'iComb' and 'id'.
Note that none of the functions in this module depend on data types
introduced by HaskHOL. Utility functions that do have such a dependence are
found in the "HaskHOL.Core.Basics" module.
-}
module HaskHOL.Core.Lib
( -- * Function Combinators
iComb
, kComb
, cComb
, wComb
, ffComb
, ffCombM
, liftM1
, on
-- * Basic Operations on Pairs
, swap
, pairMap
, pairMapM
, first
, firstM
, second
, secondM
-- * Basic Operations on Lists
, tryHead
, tryTail
, tryInit
, butLast
, tryLast
, tryIndex
, el
, rev
-- * Basic Operations on Association Lists
, assoc
, revLookup
, revAssoc
, assocd
, lookupd
, revLookupd
, revAssocd
-- * Methods for Error Handling
, can
, canNot
, check
, note
, hush
, fromRight
, fromRightM
, fromJustM
, LiftOption(..)
, Note(..)
, (#<<)
, (<#<)
, (<#>)
, (<#?>)
-- * Methods for Function Repetition
, funpow
, funpowM
, repeatM
, map2
, map2M
, doList
, allpairs
-- * Methods for List Iteration
, itlist
, itlistM
, foldrM
, revItlist
, foldlM
, tryFoldr1
, endItlist
, foldr1M
, foldr2
, itlist2
, foldr2M
, foldl2
, revItlist2
, foldl2M
-- * Methods for Sorting and Merging Lists
, sort
, sortBy
, merge
, mergesort
-- * Methods for Splitting and Stripping Binary Terms
, splitList
, splitListM
, revSplitList
, revSplitListM
, nsplit
, nsplitM
, stripList
, stripListM
-- * Methods for Searching and Manipulating Lists
, forall
, forall2
, exists
, partition
, mapFilter
, mapFilterM
, find
, findM
, tryFind
, flat
, dropWhileEnd
, remove
, trySplitAt
, chopList
, elemIndex
, index
, stripPrefix
, uniq
, shareOut
-- * Set Operations on Lists
, mem
, insert
, insertMap
, union
, unions
, intersect
, delete
, (\\)
, subset
, setEq
, setify
, nub
-- * Set Operations Parameterized by Predicate
, mem'
, insert'
, union'
, unions'
, subtract'
, group'
, uniq'
, setify'
-- * Operations on \"Num\" Types
, (%)
, numdom
, numerator
, denominator
, numOfString
-- * Polymorphic, Finite, Partial Functions Via Patricia Trees
, Func
, funcEmpty
, isEmpty
, funcMap
, funcFoldl
, funcFoldr
, graph
, dom
, ran
, applyd
, apply
, tryApplyd
, defined
, undefine
, (|->)
, combine
, (|=>)
, choose
-- * Re-exported 'Map' primitives
, Map
, mapEmpty
, mapInsert
, mapUnion
, mapDelete
, mapLookup
, mapElems
, mapFromList
, mapToList
, mapMap
, mapFoldrWithKey
, mapRemove
, mapToAscList
-- * Re-exported 'Text' primitives
, Text
, append
, cons
, snoc
, pack
, unpack
, textHead
, textTail
, textNull
, textEmpty
, textStrip
, textShow
-- * Re-exported 'AcidState' primitives
, Update
, Query
, get
, put
, ask
, makeAcidic
-- * Classes for Common \"Language\" Operations
-- $LangClasses
, Lang(..)
, LangSeq(..)
-- * Miscellaneous Re-exported Libraries
, module HaskHOL.Core.Lib.Families {-|
Re-exports a few type families used for basic, type-level boolean
computation.
-}
, module Control.Applicative {-|
Re-exports 'Applicative', 'Alternative', and the utility functions for
use with the 'HOL' monad.
-}
, module Control.DeepSeq {-|
Re-exports the entirety of the library, but currently only 'NFData' is
used. Necessary for using the "Criterion" benchmarking library.
-}
, module Control.Monad {-|
Re-exports the entirety of the library for use with the 'HOL' monad.
-}
, module Data.Maybe {-|
Re-exports the entirety of the library. Used primarily to make
interacting with primitive rules easier at later points in the system.
-}
, module Data.Either {-|
Re-exports the entirety of the library. Used primarily to make
interacting with primitive rules easier at later points in the system.
-}
, module Data.Data {-|
Re-exports the 'Data' and 'Typeable' class names for use in deriving
clauses.
-}
, module Data.SafeCopy {-|
Re-exports the entirety of the library for use with the 'HOL' monad's
acid state primitives.
-}
) where
import HaskHOL.Core.Lib.Families
-- Libraries re-exported in their entirety, except for applicative
import Control.Applicative hiding (Const, WrappedMonad, WrappedArrow, ZipList)
import Control.DeepSeq
import Control.Monad
import Data.Maybe
import Data.Either
import Data.Data (Data, Typeable)
import Data.SafeCopy
-- Libraries containing Re-exports
import qualified Control.Arrow as A
import qualified Data.Foldable as F
import qualified Data.Function as DF (on)
import qualified Data.List as L
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Ratio as R
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Text.Show.Text as Text (Show, show)
import qualified Data.Tuple as T
-- Acid State imports
import qualified Control.Monad.State as State (MonadState, get, put)
import qualified Control.Monad.Reader as Reader (MonadReader, ask)
import Data.Acid (Update, Query)
import qualified Data.Acid as Acid
import Language.Haskell.TH
-- Libraries containing utility functions used, but not exported directly
import Numeric (readInt, readHex, readDec)
import Data.Char (digitToInt)
import Data.Bits
import Data.Hashable
-- combinators
-- | The I combinator. An alias for 'id'.
iComb :: a -> a
iComb = id
-- | The K combinator. An alias for 'const'.
kComb :: a -> b -> a
kComb = const
-- | The C combinator. An alias for 'flip'.
cComb :: (a -> b -> c) -> b -> a -> c
cComb = flip
{-|
The W combinator. Takes a function of arity 2 and applies a single argument
to it twice.
-}
wComb :: (a -> a -> b) -> a -> b
wComb f x = f x x
-- | The FF combinator. An alias for the arrow combinator 'A.***'.
ffComb :: (a -> c) -> (b -> d) -> (a, b) -> (c, d)
ffComb = (A.***)
{-|
The monadic version of the FF combinator. An alias for the arrow combinator
'A.***' lifted for 'A.Kleisli' arrows.
-}
ffCombM :: Monad m => (a -> m c) -> (b -> m d) -> (a, b) -> m (c, d)
ffCombM f g = A.runKleisli $ A.Kleisli f A.*** A.Kleisli g
{-|
Promotes a function to a monad, but only for its first argument, i.e.
> liftM1 f a b === flip f b =<< a
-}
liftM1 :: Monad m => (a -> b -> m c) -> m a -> b -> m c
liftM1 f a b = flip f b =<< a
{-|
Re-export of the 'DF.on' combination from @Data.Function@.
-}
on :: (b -> b -> c) -> (a -> b) -> a -> a -> c
on = DF.on
-- pair basics
-- | Swaps the order of a pair. A re-export of 'T.swap'.
swap :: (a, b) -> (b, a)
swap = T.swap
-- | Applies a function to both elements of a pair using the 'A.***' operator.
pairMap :: (a -> b) -> (a, a) -> (b, b)
pairMap f = f A.*** f
-- | The monadic version of 'pairMap'.
pairMapM :: Monad m => (a -> m b) -> (a, a) -> m (b, b)
pairMapM f = f `ffCombM` f
{-|
Applies a function only to the first element of a pair. A re-export of
'A.first'.
-}
first :: (a -> c) -> (a, b) -> (c, b)
first = A.first
-- | A monadic version of 'first' lifted for 'A.Kleisli' arrows.
firstM :: Monad m => (a -> m c) -> (a, b) -> m (c, b)
firstM = A.runKleisli . A.first . A.Kleisli
{-|
Applies a function only to the second element of a pair. A re-export of
'A.second'.
-}
second :: (b -> c) -> (a, b) -> (a, c)
second = A.second
-- | A monadic version of 'second' lifted for 'A.Kleisli' arrows.
secondM :: Monad m => (b -> m c) -> (a, b) -> m (a, c)
secondM = A.runKleisli . A.second . A.Kleisli
-- list basics
{-|
A safe version of 'head'. Fails with 'Nothing' when trying to take the head
of an empty list.
-}
tryHead :: [a] -> Maybe a
tryHead (x:_) = Just x
tryHead _ = Nothing
{-|
A safe version of 'tail'. Fails with 'Nothing' when trying to take the tail
of an empty list.
-}
tryTail :: [a] -> Maybe [a]
tryTail (_:t) = Just t
tryTail _ = Nothing
{-|
A safe version of 'init'. Fails with 'Nothing' when trying to drop the last
element of an empty list.
-}
tryInit :: [a] -> Maybe [a]
tryInit [_] = Just []
tryInit (x:xs) = do xs' <- tryInit xs
return (x:xs')
tryInit _ = Nothing
-- | An alias to 'tryInit' for HOL users more familiar with this name.
butLast :: [a] -> Maybe [a]
butLast = tryInit
{-|
A safe version of 'last'. Fails with 'Nothing' when trying to take the last
element of an empty list.
-}
tryLast :: [a] -> Maybe a
tryLast [x] = Just x
tryLast (_:xs) = tryLast xs
tryLast _ = Nothing
{-|
A safe version of 'index'. Fails with 'Nothing' if the selected index does
not exist.
-}
tryIndex :: [a] -> Int -> Maybe a
tryIndex xs n
| n >= 0 = tryHead $ drop n xs
| otherwise = Nothing
{-|
An alias to 'tryIndex' for HOL users more familiar with this name. Note that
the order of the arguments is flipped.
-}
el :: Int -> [a] -> Maybe a
el = flip tryIndex
-- | An alias to 'reverse' for HOL users more familiar with this name.
rev :: [a] -> [a]
rev = reverse
-- association lists
-- | An alias to 'lookup' for HOL users more familiar with this name.
assoc :: Eq a => a -> [(a, b)] -> Maybe b
assoc = lookup
{-|
A version of 'lookup' where the search is performed against the second element
of the pair instead of the first. Still fails with 'Nothing' if the desired
value is not found.
-}
revLookup :: Eq a => a -> [(b, a)] -> Maybe b
revLookup _ [] = Nothing
revLookup x ((f, s):as)
| x == s = Just f
| otherwise = revLookup x as
-- | An alias to 'revLookup' for HOL users who are more familiar with this name.
revAssoc :: Eq a => a -> [(b, a)] -> Maybe b
revAssoc = revLookup
-- | A version of 'lookup' that defaults to a provided value rather than fail.
lookupd :: Eq a => a -> [(a, b)] -> b -> b
lookupd x xs b = fromMaybe b $ lookup x xs
-- | An alias to 'lookupd' for HOL users who are more familiar with this name.
assocd :: Eq a => a -> [(a, b)] -> b -> b
assocd = lookupd
{-|
A version of 'revLookup' that defaults to a provided value rather than fail.
-}
revLookupd :: Eq a => a -> [(b, a)] -> b -> b
revLookupd x xs b = fromMaybe b $ revLookup x xs
{-|
An alias to 'revLookupd' for HOL users who are more familiar with this name.
-}
revAssocd :: Eq a => a -> [(b, a)] -> b -> b
revAssocd = revLookupd
-- error handling and checking
{-|
Returns a boolean value indicating whether a monadic computation succeeds or
fails. The '<|>' operator is used for branching.
-}
can :: (Alternative m, Monad m) => (a -> m b) -> a -> m Bool
can f x = (f x >> return True) <|> return False
{-|
The opposite of 'can'. Functionally equivalent to
> \ f -> liftM not . can f
-}
canNot :: (Alternative m, Monad m) => (a -> m b) -> a -> m Bool
canNot f x = (f x >> return False) <|> return True
{-|
Checks if a predicate succeeds for a provided value, returning that value
guarded by a 'Maybe' type if so.
-}
check :: (a -> Bool) -> a -> Maybe a
check p x
| p x = Just x
| otherwise = Nothing
-- | Takes a default error value to convert a 'Maybe' type to an 'Either' type.
note :: a -> Maybe b -> Either a b
note l Nothing = Left l
note _ (Just r) = Right r
{-|
Suppresses the error value of an 'Either' type to convert it to a 'Maybe'
type.
-}
hush :: Either a b -> Maybe b
hush (Left _) = Nothing
hush (Right r) = Just r
{-|
An analogue of 'fromJust' for the 'Either' type. Fails with 'error' when
provided a 'Left' value, so take care only to use it in cases where you know
you are working with a 'Right' value or are catching exceptions.
-}
fromRight :: Either err a -> a
fromRight (Right res) = res
fromRight _ = error "fromRight"
{-|
A version of 'fromRight' that maps 'Left' values to 'mzero' rather than
failing.
-}
fromRightM :: (Monad m, Show err) => Either err a -> m a
fromRightM (Right res) = return res
fromRightM (Left err) = fail $ show err
{-|
A version of 'fromJust' that maps 'Nothing' values to 'mzero' rather than
failing.
-}
fromJustM :: Monad m => Maybe a -> m a
fromJustM (Just res) = return res
fromJustM _ = fail "fromJust"
{-|
The 'LiftOption' class provides an infix operator to more cleanly apply the
'fromJustM' and 'fromRightM' methods to a value that will be passed to a
monadic computation.
-}
class Monad m => LiftOption l m where
{-|
Used to lift an option value, i.e. 'Maybe' or 'Either', so that it can be
passed as an argument to a monadic computation.
-}
liftO :: l a -> m a
instance Monad m => LiftOption Maybe m where
liftO = fromJustM
instance (Show a, Monad m) => LiftOption (Either a) m where
liftO = fromRightM
infixr 1 #<<
-- | A version of '=<<' composed with 'liftO' for the right argument.
(#<<) :: LiftOption l m => (a -> m b) -> l a -> m b
l #<< r = l =<< liftO r
infixr 1 <#<
-- | A version of '<=<' composed with 'liftO' for the right argument.
(<#<) :: LiftOption l m => (b -> m c) -> (a -> l b) -> a -> m c
(<#<) l r x = l =<< liftO (r x)
infixl 4 <#>
-- | A version of 'liftM1' composed with 'liftO' for the right argument.
(<#>) :: LiftOption l m => (a -> b -> m c) -> l a -> b -> m c
l <#> r = liftM1 l $ liftO r
infix 0 <#?>
-- | A version of '<?>' composed with 'liftO' for the job argument.
(<#?>) :: (LiftOption l m, Note m) => l a -> String -> m a
job <#?> err = liftO job <?> err
infix 0 <?>
{-|
The 'Note' class provides an ad hoc way of tagging an error case with a
string.
-}
class (Alternative m, Monad m) => Note m where
{-|
Used to annotate more precise error messages. Replaces the '<|>' operator
in cases such as
> ... <|> fail "..."
-}
(<?>) :: m a -> String -> m a
{-|
Replaces the common pattern
> m >>= \ cond -> if cond then fail "..."
The default case is defined in terms of 'empty' and '<?>'.
-}
failWhen :: m Bool -> String -> m ()
failWhen m str =
do cond <- m
when cond empty <?> str
instance Note (Either String) where
job <?> str = job <|> Left str
-- repetition of a functions
{-|
Repeatedly applies a function to an argument @n@ times. Rather than fail,
the original argument is returned when @n<=0@.
-}
funpow :: Int -> (a -> a) -> a -> a
funpow n f x
| n <= 0 = x
| otherwise = funpow (n - 1) f (f x)
-- | The monadic version of 'funpow'.
funpowM :: Monad m => Int -> (a -> m a) -> a -> m a
funpowM n f x
| n <= 0 = return x
| otherwise = funpowM (n - 1) f =<< f x
{-|
Repeatedly applies a monadic computation to an argument until there is a
failure. The '<|>' operator is used for branching.
-}
repeatM :: (Alternative m, Monad m) => (a -> m a) -> a -> m a
repeatM f x = (repeatM f =<< f x) <|> return x
{-|
A safe version of a list map for functions of arity 2. Fails with 'Nothing'
if the two lists are of different lengths.
-}
map2 :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]
map2 _ [] [] = Just []
map2 f (x:xs) (y:ys) =
do zs <- map2 f xs ys
return $! f x y : zs
map2 _ _ _ = Nothing
{-|
The monadic version of 'map2'. Fails with 'mzero' if the two lists are of
different lengths.
-}
map2M :: (Monad m, MonadPlus m) => (a -> b -> m c) -> [a] -> [b] -> m [c]
map2M _ [] [] = return []
map2M f (x:xs) (y:ys) =
do h <- f x y
t <- map2M f xs ys
return (h : t)
map2M _ _ _ = mzero
{-|
Map a monadic function over a list, ignoring the results. A re-export of
'mapM_'.
-}
doList :: Monad m => (a -> m b) -> [a] -> m ()
doList = mapM_
-- all pairs arrising from applying a function over two lists
{-|
Produces a list containing the results of applying a function to all possible
combinations of arguments from two lists. Rather than failing if the lists
are of different lengths, iteration is shortcutted to end when the left most
list is null.
-}
allpairs :: (a -> b -> c) -> [a] -> [b] -> [c]
allpairs _ [] _ = []
allpairs f (h:t) l2 = foldr (\ x a -> f h x : a) (allpairs f t l2) l2
-- list iteration
{-|
An alias to 'foldr' for HOL users more familiar with this name. Note that the
order of the list and base case arguments is flipped.
-}
itlist :: (a -> b -> b) -> [a] -> b -> b
itlist f = flip (foldr f)
-- | The monadic version of 'itlist'.
itlistM :: (F.Foldable t, Monad m) => (a -> b -> m b) -> t a -> b -> m b
itlistM f = flip (F.foldrM f)
-- | The monadic version of 'foldr'. A re-export of 'F.foldrM'.
foldrM :: (F.Foldable t, Monad m) => (a -> b -> m b) -> b -> t a -> m b
foldrM = F.foldrM
{-|
An alias to 'foldl' for HOL users more familiar with this name. Note that the
order of the list and base case arguments is flipped, as is the order of the
arguments to the function.
-}
revItlist :: (a -> b -> b) -> [a] -> b -> b
revItlist f = flip (foldl $ flip f)
-- | The monadic version of 'foldl'. A re-export of 'F.foldlM'.
foldlM :: (F.Foldable t, Monad m) => (a -> b -> m a) -> a -> t b -> m a
foldlM = F.foldlM
{-|
A safe version of 'foldr1'. Fails with 'Nothing' if an empty list is provided
as an argument.
-}
tryFoldr1 :: (a -> a -> a) -> [a] -> Maybe a
tryFoldr1 _ [] = Nothing
tryFoldr1 _ [x] = Just x
tryFoldr1 f (x:xs) = liftM (f x) $ tryFoldr1 f xs
-- | An alias to 'tryFoldr1' for HOL users more familiar with this name.
endItlist :: (a -> a -> a) -> [a] -> Maybe a
endItlist = tryFoldr1
{-|
The monadic version of 'foldr1'. Fails with 'mzero' if an empty list is
provided as an argument.
-}
foldr1M :: (Monad m, MonadPlus m) => (a -> a -> m a) -> [a] -> m a
foldr1M _ [] = mzero
foldr1M _ [x] = return x
foldr1M f (h:t) = f h =<< foldr1M f t
{-|
A safe version of a right, list fold for functions of arity 2. Fails with
'Nothing' if the two lists are of different lengths.
-}
foldr2 :: (a -> b -> c -> c) -> c -> [a] -> [b] -> Maybe c
foldr2 _ b [] [] = Just b
foldr2 f b (x:xs) (y:ys) =
do b' <- foldr2 f b xs ys
return $! f x y b'
foldr2 _ _ _ _ = Nothing
{-|
An alias to 'foldr2' for HOL users more familiar with this name. Note that
the order of the two list arguments and the base case argument is flipped.
-}
{-# INLINE itlist2 #-}
itlist2 :: (a -> b -> c -> c) -> [a] -> [b] -> c -> Maybe c
itlist2 f xs ys b = foldr2 f b xs ys
{-|
The monadic version of 'foldr2'. Fails with 'mzero' if the two lists are
of different lengths.
-}
foldr2M :: (Monad m, MonadPlus m) =>
(a -> b -> c -> m c) -> c -> [a] -> [b] -> m c
foldr2M _ b [] [] = return b
foldr2M f b (h1:t1) (h2:t2) = f h1 h2 =<< foldr2M f b t1 t2
foldr2M _ _ _ _ = mzero
{-|
A safe version of a left, list fold for functions of arity 2. Fails with
'Nothing' if the two lists are of different lengths.
-}
foldl2 :: (c -> a -> b -> c) -> c -> [a] -> [b] -> Maybe c
foldl2 _ b [] [] = Just b
foldl2 f b (x:xs) (y:ys) =
foldl2 f (f b x y) xs ys
foldl2 _ _ _ _ = Nothing
{-|
An alias to 'foldl2' for HOL users more familiar with this name. Note that
the order of the two list arguments and base case argument is flipped, as is
the order of the arguments to the provided function.
-}
revItlist2 :: (a -> b -> c -> c) -> [a] -> [b] -> c -> Maybe c
revItlist2 f xs ys b = foldl2 (\ z x y -> f x y z) b xs ys
{-|
The monadic version of 'foldl2'. Fails with 'mzero' if the two lists are
of different lengths.
-}
foldl2M :: (Monad m, MonadPlus m) =>
(c -> a -> b -> m c) -> c -> [a] -> [b] -> m c
foldl2M _ b [] [] = return b
foldl2M f b (h1:t1) (h2:t2) =
do b' <- f b h1 h2
foldl2M f b' t1 t2
foldl2M _ _ _ _ = mzero
-- sorting and merging of lists
{-|
Sorts a list using a partitioning predicate to build an implied ordering.
If @p@ is the predicate and @x \`p\` y@ and @not (y \`p\` x)@ are true then
@x@ will be in front of @y@ in the sorted list.
-}
sort :: Eq a => (a -> a -> Bool) -> [a] -> [a]
sort _ [] = []
sort f (piv:rest) =
let (r, l) = partition (f piv) rest in
sort f l ++ (piv : sort f r)
{-|
A more traditional sort using an 'Ordering' relationship between elements. A
re-export of 'L.sortBy'.
-}
sortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortBy = L.sortBy
{-|
Merges two lists using a partitioning predicate to build an implied ordering.
See 'sort' for more information on how the predicate affects the order of the
resultant list.
-}
merge :: (a -> a -> Bool) -> [a] -> [a] -> [a]
merge _ [] l2 = l2
merge _ l1 [] = l1
merge ord l1@(x:xs) l2@(y:ys)
| ord x y = x : merge ord xs l2
| otherwise = y : merge ord l1 ys
{-|
Sorts a list using a partitioning predicate to build an implied ordering;
uses 'merge' internally. See 'sort' for more information on how the predicate
affects the order of the resultant list.
-}
mergesort :: forall a. (a -> a -> Bool) -> [a] -> [a]
mergesort _ [] = []
mergesort ord l = mergepairs [] $ map (: []) l
where mergepairs :: [[a]] -> [[a]] -> [a]
mergepairs [x] [] = x
mergepairs xs [] = mergepairs [] xs
mergepairs xs [y] = mergepairs (y:xs) []
mergepairs xs (y1:y2:ys) = mergepairs (merge ord y1 y2 : xs) ys
-- iterative term splitting and stripping via destructor
{-|
Repeatedly applies a binary destructor function to a term until failure.
Application is forward, or left-associative, such that for a term of the form
@x1 \`f\` x2 \`f\` b@ calling this function with a destructor for @f@ will
produce the result @([x1, x2], b)@.
-}
splitList :: (b -> Maybe (a, b)) -> b -> ([a], b)
splitList f x =
case f x of
Just (l, r) ->
let (ls, res) = splitList f r in
(l:ls, res)
Nothing -> ([], x)
-- | The monadic version of 'splitList'.
splitListM :: (Alternative m, Monad m) => (b -> m (a, b)) -> b -> m ([a], b)
splitListM f x =
(do (l, r) <- f x
(ls, res) <- splitListM f r
return (l:ls, res))
<|> return ([], x)
{-|
Repeatedly applies a binary destructor function to a term until failure.
Application is reverse, or right-associative, such that for a term of the form
@x1 \`f\` x2 \`f\` b@ calling this function with a destructor for @f@ will
produce the result @(f, [x1, x2 \`f\` b])@.
-}
revSplitList :: forall a b. (a -> Maybe (a, b)) -> a -> (a, [b])
revSplitList f = recSplit []
where recSplit :: [b] -> a -> (a, [b])
recSplit ls y =
case f y of
Just (l, r) -> recSplit (r:ls) l
Nothing -> (y, ls)
-- | The monadic version of 'revSplitList'.
revSplitListM :: forall m a b. (Alternative m, Monad m) =>
(a -> m (a, b)) -> a -> m (a, [b])
revSplitListM f = rsplist []
where rsplist :: [b] -> a -> m (a, [b])
rsplist ls y =
(do (l, r) <- f y
rsplist (r:ls) l)
<|> return (y, ls)
{-|
Repeatedly applies a binary destructor function to a term for every element
in a provided list.
Application is reverse, or right-associative, such that for a term of the form
@f x1 (f x2 ...(f xn b))@ calling this function with a destructor for @f@ and
a list @l@ will produce the result @([x1 .. xk], f x(k+1) ...(f xn b))@ where
@k@ is the length of list @l@.
-}
nsplit :: (a -> Maybe (a, a)) -> [b] -> a -> Maybe ([a], a)
nsplit _ [] x = return ([], x)
nsplit dest (_:cs) x =
do (l, r) <- dest x
(ll, y) <- nsplit dest cs r
return (l:ll, y)
-- | The monadic version of 'nsplit'.
nsplitM :: Monad m => (b -> m (b, b)) -> [c] -> b -> m ([b], b)
nsplitM _ [] x = return ([], x)
nsplitM dest (_:n) x =
do (l, r) <- dest x
(ll, y) <- nsplitM dest n r
return (l:ll, y)
{-|
Repeatedly applies a binary destructor function to a term until failure.
Application is forward, or left-associative, such that for a term of the form
@x1 \`f\` x2 \`f\` x3@ calling this function with a destructor for @f@ will
produce the result @[x1, x2, x3]@.
-}
stripList :: forall a. (a -> Maybe (a, a)) -> a -> [a]
stripList dest x = strip x []
where strip :: a -> [a] -> [a]
strip x' acc =
case dest x' of
Just (l, r) -> strip l $ strip r acc
Nothing -> x' : acc
-- | The monadic version of 'stripList'.
stripListM :: forall m a. (Alternative m, Monad m) =>
(a -> m (a, a)) -> a -> m [a]
stripListM dest x = strip x []
where strip :: a -> [a] -> m [a]
strip x' acc =
(do (l, r) <- dest x'
strip l =<< strip r acc)
<|> return (x' : acc)
-- miscellaneous list methods
-- | An alias to 'all' for HOL users who are more familiar with this name.
forall :: (a -> Bool) -> [a] -> Bool
forall = all
{-|
A version of 'all' for predicates of arity 2. Iterates down two lists
simultaneously with 'map2', using 'and' to combine the results.
-}
forall2 :: (a -> b -> Bool) -> [a] -> [b] -> Maybe Bool
forall2 f xs = liftM and . map2 f xs
-- | An alias to 'any' for HOL users who are more familiar with this name.
exists :: (a -> Bool) -> [a] -> Bool
exists = any
{-|
Separates a list of elements using a predicate. A re-export of 'L.partition'.
-}
partition :: (a -> Bool) -> [a] -> ([a], [a])
partition = L.partition
-- | An alias to 'mapMaybe' for HOL users more familiar with this name.
mapFilter :: (a -> Maybe b) -> [a] -> [b]
mapFilter = mapMaybe
{-|
The monadic version of 'mapFilter'. The '(<|>)' operator is used for
branching.
-}
mapFilterM :: (Alternative m, Monad m) => (a -> m b) -> [a] -> m [b]
mapFilterM _ [] = return []
mapFilterM f (x:xs) =
do xs' <- mapFilterM f xs
(do x' <- f x
return (x':xs'))
<|> return xs'
-- | A re-export of 'L.find'.
find :: (a -> Bool) -> [a] -> Maybe a
find = L.find
{-|
The monadic version of 'find'. Fails if the monadic predicate does. Also
fails with 'mzero' if an empty list is provided.
-}
findM :: (Monad m, MonadPlus m) => (a -> m Bool) -> [a] -> m a
findM _ [] = mzero
findM f (x:xs) =
do b <- f x
if b
then return x
else findM f xs
{-|
An alternative monadic version of 'find' where the predicate is a monadic
computation not necessarily of a boolean return type. Returns the result of
the first successful application of the predicate to an element of the list.
Fails with 'mzero' if called on an empty list.
Note that 'mplus' is used for branching instead of '<|>' to minimize the
constraint type; for the vast majority of monads these two functions should be
identical anyway.
-}
tryFind :: (Monad m, MonadPlus m) => (a -> m b) -> [a] -> m b
tryFind _ [] = mzero
tryFind f (x:xs) = f x `mplus` tryFind f xs
-- | An alias to 'concat' for HOL users who are more familiar with this name.
flat :: [[a]] -> [a]
flat = concat
{-|
Drops elements from the end of a list while a predicate is true. A re-export
of 'L.dropWhileEnd'.
-}
dropWhileEnd :: (a -> Bool) -> [a] -> [a]
dropWhileEnd = L.dropWhileEnd
{-|
Separates the first element of a list that satisfies a predicate. Fails with
'Nothing' if no such element is found.
-}
remove :: (a -> Bool) -> [a] -> Maybe (a, [a])
remove _ [] = Nothing
remove p (h:t)
| p h = Just (h, t)
| otherwise =
do (y, n) <- remove p t
return (y, h:n)
{-|
A safe version of 'splitAt'. Fails with 'Nothing' if a split is attempted
at an index that doesn't exist.
-}
trySplitAt :: Int -> [a] -> Maybe ([a], [a])
trySplitAt n l
| n < 0 = Nothing
| n == 0 = Just ([], l)
| otherwise =
case l of
[] -> Nothing
(x:xs) -> do (m, l') <- trySplitAt (n - 1) xs
return (x:m, l')
-- | An alias to 'trySplitAt' for HOL users more familiar with this name
chopList :: Int -> [a] -> Maybe ([a], [a])
chopList = trySplitAt
{-|
Returns the first index where an element appears in list. Fails with
'Nothing' if no such element is found. A re-export of 'L.elemIndex'.
-}
elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex = L.elemIndex
-- | An alias to 'elemIndex' for HOL users more familiar with this name.
index :: Eq a => a -> [a] -> Maybe Int
index = elemIndex
{-|
Drops the given prefix from a list. Fails with 'Nothing' if there is no such
prefix. A re-export of 'L.stripPrefix'.
-}
stripPrefix :: Eq a => [a] -> [a] -> Maybe [a]
stripPrefix = L.stripPrefix
-- | Removes adjacent, equal elements from a list.
uniq :: Eq a => [a] -> [a]
uniq (x:y:t) =
let t' = uniq t in
if x == y then t' else x : t'
uniq l = l
{-|
Partitions a list into a list of lists matching the structure of the first
argument. For example:
@shareOut [[1, 2], [3], [4, 5]] \"abcde\" === [\"ab\", \"c\", \"de\"]@
-}
shareOut :: [[a]] -> [b] -> Maybe [[b]]
shareOut [] _ = Just []
shareOut (p:ps) bs =
do (l, r) <- chopList (length p) bs
ls <- shareOut ps r
return (l : ls)
-- set operations on lists
-- | An alias to 'elem' for HOL users who are more familiar with this name.
mem :: Eq a => a -> [a] -> Bool
mem = elem
{-|
Inserts an item into a list if it would be a unique element.
Important note: This insert is unordered, unlike the 'L.insert' in the
"Data.List" module.
-}
insert :: Eq a => a -> [a] -> [a]
insert x l
| x `elem` l = l
| otherwise = x : l
{-|
Inserts, or updates, a key value pair in an association list.
Note that this insert is unordered, but uniqueness preserving.
-}
insertMap :: Eq a => a -> b -> [(a, b)] -> [(a, b)]
insertMap key v [] = [(key, v)]
insertMap key v (x@(key', _):xs)
| key == key' = (key, v) : xs
| otherwise = x : insertMap key v xs
{-|
Unions two list maintaining uniqueness of elements.
Important note: This union is unordered, unlike the 'L.union' in the
"Data.List" module.
-}
union :: Eq a => [a] -> [a] -> [a]
union l1 l2 = foldr insert l2 l1
-- | Unions a list of lists using 'union'.
unions :: Eq a => [[a]] -> [a]
unions = foldr union []
-- | Finds the intersection of two lists. A re-export of 'L.intersect'.
intersect :: Eq a => [a] -> [a] -> [a]
intersect = L.intersect
-- | Removes an item from a list. A re-export of 'L.delete'.
delete :: Eq a => a -> [a] -> [a]
delete = L.delete
-- | Subtracts one list from the other. A re-export of 'L.\\'.
(\\) :: Eq a => [a] -> [a] -> [a]
(\\) = (L.\\)
-- | Tests if the first list is a subset of the second.
subset :: Eq a => [a] -> [a] -> Bool
subset xs ys = all (`elem` ys) xs
-- | A test for set equality using 'subset'.
setEq :: Eq a => [a] -> [a] -> Bool
setEq l1 l2 = subset l1 l2 && subset l2 l1
-- | Converts a list to a set by removing duplicates. A re-export of 'L.nub'.
nub :: Eq a => [a] -> [a]
nub = L.nub
-- | A version of 'nub' where the resultant list is sorted.
setify :: Ord a => [a] -> [a]
setify = L.sort . nub
-- set operations parameterized by equality
{-|
A version of 'mem' where the membership test is an explicit predicate, rather
than a strict equality test.
-}
mem' :: (a -> a -> Bool) -> a -> [a] -> Bool
mem' _ _ [] = False
mem' eq a (x:xs) = eq a x || mem' eq a xs
{-|
A version of 'insert' where the uniqueness test is an explicit predicate,
rather than a strict equality test.
-}
insert' :: (a -> a -> Bool) -> a -> [a] -> [a]
insert' eq x xs
| mem' eq x xs = xs
| otherwise = x : xs
{-|
A version of 'union' where the uniqueness test is an explicit predicate,
rather than a strict equality test.
-}
union' :: (a -> a -> Bool) -> [a] -> [a] -> [a]
union' eq xs ys = foldr (insert' eq) ys xs
{-|
A version of 'unions' where the uniqueness test is an explicit predicate,
rather than a strict equality test.
-}
unions' :: (a -> a -> Bool) -> [[a]] -> [a]
unions' eq = foldr (union' eq) []
{-|
A version of 'subtract' where the uniqueness test is an explicit predicate,
rather than a strict equality test.
-}
subtract' :: (a -> a -> Bool) -> [a] -> [a] -> [a]
subtract' eq xs ys = filter (\ x -> not $ mem' eq x ys) xs
{-|
Groups neighbors in a list together based on a predicate. A re-export of
'L.groupBy'.
-}
group' :: (a -> a -> Bool) -> [a] -> [[a]]
group' = L.groupBy
-- | A version of 'uniq' that eliminates elements based on a provided predicate.
uniq' :: Eq a => (a -> a -> Bool) -> [a] -> [a]
uniq' eq l@(x:t@(y:_)) =
let t' = uniq' eq t in
if x `eq` y then t'
else if t' == t then l else x:t'
uniq' _ l = l
{-|
A version of 'setify' that eliminates elements based on a provided predicate.
-}
setify' :: Eq a => (a -> a -> Bool) -> (a -> a -> Bool) -> [a] -> [a]
setify' le eq xs = uniq' eq $ sort le xs
-- | Constructs a 'Rational' from two 'Integer's. A re-export of (R.%).
(%) :: Integer -> Integer -> Rational
(%) = (R.%)
{-|
Converts a real number to a rational representation.
An alias to 'toRational' for HOL users more familiar with this name.
-}
numdom :: Rational -> (Integer, Integer)
numdom r =
(R.numerator r, R.denominator r)
-- | Returns the numerator of a rational number. A re-export of 'R.numerator'.
numerator :: Rational -> Integer
numerator = R.numerator
{-|
Returns the denominator of a rational number. A re-export of 'R.denominator'.
-}
denominator :: Rational -> Integer
denominator = R.denominator
{-|
Converts a 'String' representation of a number to an appropriate instance of
the 'Num' class. Fails with 'Nothing' if the conversion cannot be performed.
Note: The following prefixes are valid:
* @0x@ - number read as a hexidecimal value
* @0b@ - number read as a binary value
* Any other prefix causes the number to be read as a decimal value
-}
numOfString :: forall a. (Eq a, Num a) => String -> Maybe a
numOfString s =
case res of
[(x, "")] -> Just x
_ -> Nothing
where res :: [(a, String)]
res = case s of
('0':'x':s') -> readHex s'
('0':'b':s') -> readInt 2 (`elem` "01") digitToInt s'
_ -> readDec s
-- Polymorphic, finite, partial functions via Patricia trees
{-| 'Func' is a Patricia Tree representation of polymorphic, finite, partial
functions.
-}
data Func a b
= Empty
| Leaf !Int ![(a, b)]
| Branch !Int !Int !(Func a b) !(Func a b) deriving Eq
-- | An empty 'Func' tree.
funcEmpty :: Func a b
funcEmpty = Empty
-- | The predicate for empty 'Func' trees.
isEmpty :: Func a b -> Bool
isEmpty Empty = True
isEmpty _ = False
-- | A version of 'map' for 'Func' trees.
funcMap :: (b -> c) -> Func a b -> Func a c
funcMap _ Empty = Empty
funcMap f (Leaf h l) = Leaf h $ map (A.second f) l
funcMap f (Branch p b l r) = Branch p b (funcMap f l) $ funcMap f r
-- | A version of 'foldl' for 'Func' trees.
funcFoldl :: (c -> a -> b -> c) -> c -> Func a b -> c
funcFoldl _ a Empty = a
funcFoldl f a (Leaf _ l) =
let (xs, ys) = unzip l in
fromJust $ foldl2 f a xs ys
funcFoldl f a (Branch _ _ l r) = funcFoldl f (funcFoldl f a l) r
-- | A version of 'foldr' for 'Func' trees.
funcFoldr :: (a -> b -> c -> c) -> c -> Func a b -> c
funcFoldr _ a Empty = a
funcFoldr f a (Leaf _ l) =
let (xs, ys) = unzip l in
fromJust $ foldr2 f a xs ys
funcFoldr f a (Branch _ _ l r) = funcFoldr f (funcFoldr f a r) l
-- | Converts a 'Func' tree to a sorted association list.
graph :: (Ord a, Ord b) => Func a b -> [(a, b)]
graph f = setify $ funcFoldl (\ a x y -> ((x, y):a)) [] f
-- | Converts a 'Func' tree to a sorted list of domain elements.
dom :: Ord a => Func a b -> [a]
dom f = setify $ funcFoldl (\ a x _ -> x:a) [] f
-- | Converts a 'Func' tree to a sorted list of range elements.
ran :: Ord b => Func a b -> [b]
ran f = setify $ funcFoldl (\ a _ y -> y:a) [] f
-- | Application for 'Func' trees.
applyd :: forall a b. (Hashable a, Ord a) => Func a b -> (a -> Maybe b) -> a
-> Maybe b
applyd Empty d x = d x
applyd (Branch p b l r) d x
| (k `xor` p) .&. (b - 1) == 0 =
applyd (if k .&. b == 0 then l else r) d x
| otherwise = d x
where k = hash x
applyd (Leaf h l) d x
| h == hash x = applydRec l
| otherwise = d x
where applydRec :: Ord a => [(a, b)] -> Maybe b
applydRec [] = d x
applydRec ((a, b):t)
| x == a = Just b
| x > a = applydRec t
| otherwise = d x
-- | Application for 'Func' trees with using constant 'Nothing'.
apply :: (Hashable a, Ord a) => Func a b -> a -> Maybe b
apply f = applyd f $ const Nothing
-- | Application for 'Func' trees with a default value.
tryApplyd :: (Hashable a, Ord a) => Func a b -> a -> b -> b
tryApplyd f a d = fromJust $ applyd f (\ _ -> Just d) a
-- | Predicate for testing if a value is defined in a 'Func' tree.
defined ::(Hashable a, Ord a) => Func a b -> a -> Bool
defined f x = isJust $ apply f x
-- | Undefine a value in a 'Func' tree.
undefine :: forall a b. (Hashable a, Ord a, Eq b) => a -> Func a b -> Func a b
undefine _ Empty = Empty
undefine x t@(Branch p b l r)
| hash x .&. b == 0 =
let l' = undefine x l in
if l' == l then t
else case l' of
Empty -> r
_ -> Branch p b l' r
| otherwise =
let r' = undefine x r in
if r' == r then t
else case r' of
Empty -> l
_ -> Branch p b l r'
undefine x t@(Leaf h l)
| h == hash x =
let l' = undefineRec l in
if l' == l then t
else if null l' then Empty
else Leaf h l'
| otherwise = t
where undefineRec :: [(a, b)] -> [(a, b)]
undefineRec [] = []
undefineRec l'@(ab@(a, _):xs)
| x == a = xs
| x < a = l'
| otherwise =
let xs' = undefineRec xs in
if xs' == xs then l' else ab:xs'
newBranch :: Int -> Func a b -> Int -> Func a b -> Func a b
newBranch p1 t1 p2 t2 =
let zp = p1 `xor` p2
b = zp .&. (-zp)
p = p1 .&. (b - 1) in
if p1 .&. b == 0 then Branch p b t1 t2
else Branch p b t2 t1
-- | Insert or update an element in a 'Func' tree.
(|->) :: forall a b. (Hashable a, Ord a) => a -> b -> Func a b -> Func a b
(x |-> y) Empty = Leaf (hash x) [(x, y)]
(x |-> y) t@(Branch p b l r)
| k .&. (b - 1) /= p =
newBranch p t k $ Leaf k [(x, y)]
| k .&. b == 0 = Branch p b ((x |-> y) l) r
| otherwise = Branch p b l $ (x |-> y) r
where k = hash x
(x |-> y) t@(Leaf h l)
| h == k = Leaf h $ defineRec l
| otherwise =
newBranch h t k $ Leaf k [(x, y)]
where k = hash x
defineRec :: [(a, b)] -> [(a, b)]
defineRec [] = [(x, y)]
defineRec l'@(ab@(a, _):xs)
| x == a = (x, y):xs
| x < a = (x, y):l'
| otherwise = ab:defineRec xs
-- | Combines two 'Func' trees.
combine :: forall a b. Ord a => (b -> b -> b) -> (b -> Bool) -> Func a b
-> Func a b -> Func a b
combine _ _ Empty t2 = t2
combine _ _ t1 Empty = t1
combine op z lf@(Leaf k _) br@(Branch p b l r)
| k .&. (b - 1) == p =
if k .&. b == 0
then case combine op z lf l of
Empty -> r
l' -> Branch p b l' r
else case combine op z lf r of
Empty -> l
r' -> Branch p b l r'
| otherwise = newBranch k lf p br
combine op z br@(Branch p b l r) lf@(Leaf k _)
| k .&. (b - 1) == p =
if k .&. b == 0
then case combine op z l lf of
Empty -> r
l' -> Branch p b l' r
else case combine op z r lf of
Empty -> l
r' -> Branch p b l r'
| otherwise = newBranch p br k lf
combine op z t1@(Branch p1 b1 l1 r1) t2@(Branch p2 b2 l2 r2)
| b1 < b2 =
if p2 .&. (b1 - 1) /= p1 then newBranch p1 t1 p2 t2
else if p2 .&. b1 == 0
then case combine op z l1 t2 of
Empty -> r1
l -> Branch p1 b1 l r1
else case combine op z r1 t2 of
Empty -> l1
r -> Branch p1 b1 l1 r
| b2 < b1 =
if p1 .&. (b2 - 1) /= p2 then newBranch p1 t1 p2 t2
else if p1 .&. b2 == 0
then case combine op z t1 l2 of
Empty -> r2
l -> Branch p2 b2 l r2
else case combine op z t1 r2 of
Empty -> l2
r -> Branch p2 b2 l2 r
| p1 == p2 =
case (combine op z l1 l2, combine op z r1 r2) of
(Empty, r) -> r
(l, Empty) -> l
(l, r) -> Branch p1 b1 l r
| otherwise = newBranch p1 t1 p2 t2
combine op z t1@(Leaf h1 l1) t2@(Leaf h2 l2)
| h1 == h2 =
let l = combineRec l1 l2 in
if null l then Empty else Leaf h1 l
| otherwise = newBranch h1 t1 h2 t2
where combineRec :: [(a, b)] -> [(a, b)] -> [(a, b)]
combineRec [] ys = ys
combineRec xs [] = xs
combineRec xs@(xy1@(x1, y1):xs') ys@(xy2@(x2, y2):ys')
| x1 < x2 = xy1:combineRec xs' ys
| x1 > x2 = xy2:combineRec xs ys'
| otherwise =
let y = op y1 y2
l = combineRec xs' ys' in
if z y then l else (x1, y):l
-- | Special case of '(|->)' applied to 'funcEmpty'.
(|=>) :: (Hashable a, Ord a) => a -> b -> Func a b
x |=> y = (x |-> y) funcEmpty
-- | Selects an arbitrary element from a 'Func' tree.
choose :: Func a b -> Maybe (a, b)
choose Empty = Nothing
choose (Leaf _ l) = tryHead l
choose (Branch _ _ t1 _) = choose t1
-- Maps
-- | A re-export of 'Map.empty'.
mapEmpty :: Map a b
mapEmpty = Map.empty
-- | A re-export of 'Map.insert'.
mapInsert :: Ord a => a -> b -> Map a b -> Map a b
mapInsert = Map.insert
-- | A re-export of 'Map.union'.
mapUnion :: Ord k => Map k a -> Map k a -> Map k a
mapUnion = Map.union
-- | A re-export of 'Map.delete'.
mapDelete :: Ord k => k -> Map k a -> Map k a
mapDelete = Map.delete
-- | A re-export of 'Map.lookup'.
mapLookup :: Ord a => a -> Map a b -> Maybe b
mapLookup = Map.lookup
-- | A re-export of 'Map.elems'.
mapElems :: Map k a -> [a]
mapElems = Map.elems
-- | A re-export of 'Map.fromList'.
mapFromList :: Ord a => [(a, b)] -> Map a b
mapFromList = Map.fromList
-- | A re-export of 'Map.toList'.
mapToList :: Ord a => Map a b -> [(a, b)]
mapToList = Map.toList
-- | A re-export of 'Map.map'.
mapMap :: (a -> b) -> Map k a -> Map k b
mapMap = Map.map
-- | A re-export of 'Map.foldrWithKey'.
mapFoldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
mapFoldrWithKey = Map.foldrWithKey
-- | A version of 'remove' for 'Map's based on 'Map.updateLookupWithKey'.
mapRemove :: Ord k => k -> Map k a -> Maybe (a, Map k a)
mapRemove x m =
let (child, map') = Map.updateLookupWithKey (\ _ _ -> Nothing) x m in
case child of
Nothing -> Nothing
Just x' -> Just (x', map')
-- | A re-export of 'Map.toAscList'.
mapToAscList :: Map k a -> [(k, a)]
mapToAscList = Map.toAscList
-- | A re-export of 'Text.append'.
append :: Text -> Text -> Text
append = Text.append
-- | A re-export of 'Text.cons'.
cons :: Char -> Text -> Text
cons = Text.cons
-- | A re-export of 'Text.snoc'.
snoc :: Text -> Char -> Text
snoc = Text.snoc
-- | A re-export of 'Text.pack'.
pack :: String -> Text
pack = Text.pack
-- | A re-export of 'Text.unpack'.
unpack :: Text -> String
unpack = Text.unpack
-- | A re-export of 'Text.head'.
textHead :: Text -> Char
textHead = Text.head
-- | A re-export of 'Text.tail'.
textTail :: Text -> Text
textTail = Text.tail
-- | A re-export of 'Text.null'.
textNull :: Text -> Bool
textNull = Text.null
-- | A re-export of 'Text.empty'.
textEmpty :: Text
textEmpty = Text.empty
-- | A re-export of 'Text.strip'.
textStrip :: Text -> Text
textStrip = Text.strip
-- | A re-export of 'Text.show'.
textShow :: Text.Show a => a -> Text
textShow = Text.show
-- Acid State re-exports
-- | A re-export of 'State.get' from @Control.Monad.State@.
get :: State.MonadState s m => m s
get = State.get
-- | A re-export of 'State.put' from @Control.Monad.State@.
put :: State.MonadState s m => s -> m ()
put = State.put
-- | A re-export of 'Reader.ask' from @Control.Monad.Reader@.
ask :: Reader.MonadReader r m => m r
ask = Reader.ask
-- | A re-export of 'Acid.makeAcidic' from @Data.Acid@.
makeAcidic :: Name -> [Name] -> Q [Dec]
makeAcidic = Acid.makeAcidic
-- language type classes
{-$LangClasses
The following two classes are used as an ad hoc mechanism for sharing
\"language\" operations between different types. For example, both tactics
and conversions share a number of the same operations. Rather than having
multiple functions, such as @thenTac@ and @thenConv@, we've found it easier to
have a single, polymorphic function to use, '_THEN'.
The sequencing operations are seperated in their own class, 'LangSeq', because
their tactic instances have a reliance on the boolean logic theory. Rather
than unecessarily propogate this prerequisite for all members of the 'Lang'
class, we elected to separate them.
-}
{-|
The 'Lang' class defines common language operations and combinators not based
on sequencing.
-}
class Lang a where
{-|
A primitive language operation that always fails. Typically this is
written using 'throw'.
-}
_FAIL :: String -> a
-- | An instance of '_FAIL' with a fixed failure string.
_NO :: a
-- | A primitive language operation that always succeeds.
_ALL :: a
{-|
A language combinator for branching based on failure. The language
equivalent of the '<|>' operator.
-}
_ORELSE :: a -> a -> a
-- | A language combinator that performs the first operation in a list.
_FIRST :: [a] -> a
{-|
A language combinator that fails if the wrapped operation doesn't invoke
some change, i.e. a tactic fails to change the goal state.
-}
_CHANGED :: a -> a
{-|
A language combinator that prevents the wrapped operation from having an
effect if it fails. The language equivalent of the backtracking 'try'
operator.
-}
_TRY :: a -> a
{-|
A language combinator that annotates the wrapped operation with a provided
'String'. The language equivalent of 'note''.
-}
_NOTE :: String -> a -> a
{-|
The 'LangSeq' class defines common language operations and combinators based
on sequencing. See the note at the top of this section for more details as
to why these are separated on their own.
-}
class LangSeq a where
-- | A language combinator that sequences operations.
_THEN :: a -> a -> a
{-|
A language combinator that repeatedly applies a language operation until
failure.
-}
_REPEAT :: a -> a
{-|
A language combinator that performs every operation in a list
sequentially.
-}
_EVERY :: [a] -> a