Portability  unknown 

Stability  unstable 
Maintainer  ecaustin@ittc.ku.edu 
Safe Haskell  None 
 Function Combinators
 Basic Operations on Pairs
 Basic Operations on Lists
 Basic Operations on Association Lists
 Methods for Error Handling
 Methods for Function Repetition
 Methods for List Iteration
 Methods for Sorting and Merging Lists
 Methods for Splitting and Stripping Binary Terms
 Methods for Searching and Manipulating Lists
 Set Operations on Lists
 Set Operations Parameterized by Predicate
 Operations on "Num" Types
 Classes for Common "Language" Operations
 Miscellaneous Reexported Libraries
This module defines or reexports common utility functions, type classes,
and auxilliary data types used in HaskHOL. The following conventions hold
true:
* Where possible, we favor reexporting common functions rather than
redefining them.
* We favor reexporting 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.
 iComb :: a > a
 kComb :: a > b > a
 cComb :: (a > b > c) > b > a > c
 wComb :: (a > a > b) > a > b
 ffComb :: (a > c) > (b > d) > (a, b) > (c, d)
 ffCombM :: Monad m => (a > m c) > (b > m d) > (a, b) > m (c, d)
 liftM1 :: Monad m => (a > b > m c) > m a > b > m c
 swap :: (a, b) > (b, a)
 pairMap :: (a > b) > (a, a) > (b, b)
 pairMapM :: Monad m => (a > m b) > (a, a) > m (b, b)
 first :: (a > c) > (a, b) > (c, b)
 firstM :: Monad m => (a > m c) > (a, b) > m (c, b)
 second :: (b > c) > (a, b) > (a, c)
 secondM :: Monad m => (b > m c) > (a, b) > m (a, c)
 tryHead :: [a] > Maybe a
 tryTail :: [a] > Maybe [a]
 tryInit :: [a] > Maybe [a]
 butLast :: [a] > Maybe [a]
 tryLast :: [a] > Maybe a
 tryIndex :: [a] > Int > Maybe a
 el :: Int > [a] > Maybe a
 rev :: [a] > [a]
 assoc :: Eq a => a > [(a, b)] > Maybe b
 revLookup :: Eq a => a > [(b, a)] > Maybe b
 revAssoc :: Eq a => a > [(b, a)] > Maybe b
 assocd :: Eq a => a > [(a, b)] > b > b
 lookupd :: Eq a => a > [(a, b)] > b > b
 revLookupd :: Eq a => a > [(b, a)] > b > b
 revAssocd :: Eq a => a > [(b, a)] > b > b
 can :: (Alternative m, Monad m) => (a > m b) > a > m Bool
 canNot :: (Alternative m, Monad m) => (a > m b) > a > m Bool
 check :: (a > Bool) > a > Maybe a
 note :: a > Maybe b > Either a b
 hush :: Either a b > Maybe b
 fromRight :: Either err a > a
 fromRightM :: MonadPlus m => Either err a > m a
 fromJustM :: MonadPlus m => Maybe a > m a
 class Monad m => LiftOption l m where
 class (Alternative m, Monad m) => Note m where
 funpow :: Int > (a > a) > a > a
 funpowM :: Monad m => Int > (a > m a) > a > m a
 repeatM :: (Alternative m, Monad m) => (a > m a) > a > m a
 map2 :: (a > b > c) > [a] > [b] > Maybe [c]
 map2M :: (Monad m, MonadPlus m) => (a > b > m c) > [a] > [b] > m [c]
 doList :: Monad m => (a > m b) > [a] > m ()
 allpairs :: (a > b > c) > [a] > [b] > [c]
 itlist :: (a > b > b) > [a] > b > b
 itlistM :: (Foldable t, Monad m) => (a > b > m b) > t a > b > m b
 foldrM :: (Foldable t, Monad m) => (a > b > m b) > b > t a > m b
 revItlist :: (a > b > b) > [a] > b > b
 foldlM :: (Foldable t, Monad m) => (a > b > m a) > a > t b > m a
 tryFoldr1 :: (a > a > a) > [a] > Maybe a
 endItlist :: (a > a > a) > [a] > Maybe a
 foldr1M :: (Monad m, MonadPlus m) => (a > a > m a) > [a] > m a
 foldr2 :: (a > b > c > c) > c > [a] > [b] > Maybe c
 itlist2 :: (a > b > c > c) > [a] > [b] > c > Maybe c
 foldr2M :: (Monad m, MonadPlus m) => (a > b > c > m c) > c > [a] > [b] > m c
 foldl2 :: (c > a > b > c) > c > [a] > [b] > Maybe c
 revItlist2 :: (a > b > c > c) > [a] > [b] > c > Maybe c
 foldl2M :: (Monad m, MonadPlus m) => (c > a > b > m c) > c > [a] > [b] > m c
 sort :: Eq a => (a > a > Bool) > [a] > [a]
 sortBy :: (a > a > Ordering) > [a] > [a]
 merge :: (a > a > Bool) > [a] > [a] > [a]
 mergesort :: forall a. (a > a > Bool) > [a] > [a]
 splitList :: (b > Maybe (a, b)) > b > ([a], b)
 splitListM :: (Alternative m, Monad m) => (b > m (a, b)) > b > m ([a], b)
 revSplitList :: forall a. (a > Maybe (a, a)) > a > (a, [a])
 revSplitListM :: forall m b. (Alternative m, Monad m) => (b > m (b, b)) > b > m (b, [b])
 nsplit :: (a > Maybe (a, a)) > [b] > a > Maybe ([a], a)
 nsplitM :: Monad m => (b > m (b, b)) > [c] > b > m ([b], b)
 stripList :: forall a. (a > Maybe (a, a)) > a > [a]
 stripListM :: forall m a. (Alternative m, Monad m) => (a > m (a, a)) > a > m [a]
 forall :: (a > Bool) > [a] > Bool
 forall2 :: (a > b > Bool) > [a] > [b] > Maybe Bool
 exists :: (a > Bool) > [a] > Bool
 partition :: (a > Bool) > [a] > ([a], [a])
 mapFilter :: (a > Maybe b) > [a] > [b]
 mapFilterM :: (Alternative m, Monad m) => (a > m b) > [a] > m [b]
 find :: (a > Bool) > [a] > Maybe a
 findM :: (Monad m, MonadPlus m) => (a > m Bool) > [a] > m a
 tryFind :: (Monad m, MonadPlus m) => (a > m b) > [a] > m b
 flat :: [[a]] > [a]
 dropWhileEnd :: (a > Bool) > [a] > [a]
 remove :: (a > Bool) > [a] > Maybe (a, [a])
 trySplitAt :: Int > [a] > Maybe ([a], [a])
 chopList :: Int > [a] > Maybe ([a], [a])
 elemIndex :: Eq a => a > [a] > Maybe Int
 index :: Eq a => a > [a] > Maybe Int
 stripPrefix :: Eq a => [a] > [a] > Maybe [a]
 uniq :: Eq a => [a] > [a]
 shareOut :: [[a]] > [b] > Maybe [[b]]
 mem :: Eq a => a > [a] > Bool
 insert :: Eq a => a > [a] > [a]
 insertMap :: Eq a => a > b > [(a, b)] > [(a, b)]
 union :: Eq a => [a] > [a] > [a]
 unions :: Eq a => [[a]] > [a]
 intersect :: Eq a => [a] > [a] > [a]
 delete :: Eq a => a > [a] > [a]
 (\\) :: Eq a => [a] > [a] > [a]
 subset :: Eq a => [a] > [a] > Bool
 setEq :: Eq a => [a] > [a] > Bool
 setify :: Eq a => [a] > [a]
 nub :: Eq a => [a] > [a]
 mem' :: (a > a > Bool) > a > [a] > Bool
 insert' :: (a > a > Bool) > a > [a] > [a]
 union' :: (a > a > Bool) > [a] > [a] > [a]
 unions' :: (a > a > Bool) > [[a]] > [a]
 subtract' :: (a > a > Bool) > [a] > [a] > [a]
 group' :: (a > a > Bool) > [a] > [[a]]
 uniq' :: Eq a => (a > a > Bool) > [a] > [a]
 setify' :: Eq a => (a > a > Bool) > (a > a > Bool) > [a] > [a]
 num0 :: Integer
 num1 :: Integer
 num2 :: Integer
 num10 :: Integer
 pow2 :: Integer > Integer
 pow10 :: Integer > Integer
 numdom :: Real a => a > Rational
 numerator :: Rational > Integer
 denominator :: Rational > Integer
 gcdNum :: Integer > Integer > Integer
 lcmNum :: Integer > Integer > Integer
 numOfString :: forall a. (Eq a, Num a) => String > Maybe a
 class Lang a where
 class LangSeq a where
 module HaskHOL.Core.Lib.Lift
 module Control.Applicative
 module Control.DeepSeq
 module Control.Monad
 module Data.Maybe
 module Data.Either
 module Data.Typeable
 module Text.ParserCombinators.Parsec.Expr
Function Combinators
wComb :: (a > a > b) > a > bSource
The W combinator. Takes a function of arity 2 and applies a single argument to it twice.
ffComb :: (a > c) > (b > d) > (a, b) > (c, d)Source
The FF combinator. An alias for the arrow combinator ***
.
liftM1 :: Monad m => (a > b > m c) > m a > b > m cSource
Promotes a function to a monad, but only for its first argument, i.e.
liftM1 f a b === flip f b =<< a
Basic Operations on Pairs
pairMap :: (a > b) > (a, a) > (b, b)Source
Applies a function to both elements of a pair using the ***
operator.
first :: (a > c) > (a, b) > (c, b)Source
Applies a function only to the first element of a pair. A reexport of
first
.
second :: (b > c) > (a, b) > (a, c)Source
Applies a function only to the second element of a pair. A reexport of
second
.
Basic Operations on Lists
el :: Int > [a] > Maybe aSource
An alias to tryIndex
for HOL users more familiar with this name. Note that
the order of the arguments is flipped.
Basic Operations on Association Lists
assoc :: Eq a => a > [(a, b)] > Maybe bSource
An alias to lookup
for HOL users more familiar with this name.
revAssoc :: Eq a => a > [(b, a)] > Maybe bSource
An alias to revLookup
for HOL users who are more familiar with this name.
assocd :: Eq a => a > [(a, b)] > b > bSource
An alias to lookupd
for HOL users who are more familiar with this name.
lookupd :: Eq a => a > [(a, b)] > b > bSource
A version of lookup
that defaults to a provided value rather than fail.
revLookupd :: Eq a => a > [(b, a)] > b > bSource
A version of revLookup
that defaults to a provided value rather than fail.
revAssocd :: Eq a => a > [(b, a)] > b > bSource
An alias to revLookupd
for HOL users who are more familiar with this name.
Methods for Error Handling
can :: (Alternative m, Monad m) => (a > m b) > a > m BoolSource
Returns a boolean value indicating whether a monadic computation succeeds or
fails. The <>
operator is used for branching.
canNot :: (Alternative m, Monad m) => (a > m b) > a > m BoolSource
The opposite of can
. Functionally equivalent to
\ f > liftM not . can f
check :: (a > Bool) > a > Maybe aSource
Checks if a predicate succeeds for a provided value, returning that value
guarded by a Maybe
type if so.
fromRightM :: MonadPlus m => Either err a > m aSource
class Monad m => LiftOption l m whereSource
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.
Used to lift an option value, i.e. Maybe
or Either
, so that it can be
passed as an argument to a monadic computation.
(#<<) :: (a > m b) > l a > m bSource
MonadPlus m => LiftOption Maybe m  
MonadPlus m => LiftOption (Either a) m 
class (Alternative m, Monad m) => Note m whereSource
The Note
class provides an ad hoc way of tagging an error case with a
string.
Methods for Function Repetition
funpow :: Int > (a > a) > a > aSource
Repeatedly applies a function to an argument n
times. Rather than fail,
the original argument is returned when n<=0
.
repeatM :: (Alternative m, Monad m) => (a > m a) > a > m aSource
Repeatedly applies a monadic computation to an argument until there is a
failure. The <>
operator is used for branching.
map2 :: (a > b > c) > [a] > [b] > Maybe [c]Source
A safe version of a list map for functions of arity 2. Fails with Nothing
if the two lists are of different lengths.
doList :: Monad m => (a > m b) > [a] > m ()Source
Map a monadic function over a list, ignoring the results. A reexport of
mapM_
.
allpairs :: (a > b > c) > [a] > [b] > [c]Source
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.
Methods for List Iteration
itlist :: (a > b > b) > [a] > b > bSource
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.
itlistM :: (Foldable t, Monad m) => (a > b > m b) > t a > b > m bSource
The monadic version of itlist
.
revItlist :: (a > b > b) > [a] > b > bSource
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.
endItlist :: (a > a > a) > [a] > Maybe aSource
An alias to tryFoldr1
for HOL users more familiar with this name.
foldr2 :: (a > b > c > c) > c > [a] > [b] > Maybe cSource
A safe version of a right, list fold for functions of arity 2. Fails with
Nothing
if the two lists are of different lengths.
itlist2 :: (a > b > c > c) > [a] > [b] > c > Maybe cSource
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.
foldl2 :: (c > a > b > c) > c > [a] > [b] > Maybe cSource
A safe version of a left, list fold for functions of arity 2. Fails with
Nothing
if the two lists are of different lengths.
revItlist2 :: (a > b > c > c) > [a] > [b] > c > Maybe cSource
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.
Methods for Sorting and Merging Lists
sort :: Eq a => (a > a > Bool) > [a] > [a]Source
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.
merge :: (a > a > Bool) > [a] > [a] > [a]Source
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.
Methods for Splitting and Stripping Binary Terms
splitList :: (b > Maybe (a, b)) > b > ([a], b)Source
Repeatedly applies a binary destructor function to a term until failure.
Application is forward, or leftassociative, 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)
.
splitListM :: (Alternative m, Monad m) => (b > m (a, b)) > b > m ([a], b)Source
The monadic version of splitList
.
revSplitList :: forall a. (a > Maybe (a, a)) > a > (a, [a])Source
Repeatedly applies a binary destructor function to a term until failure.
Application is reverse, or rightassociative, 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])
.
revSplitListM :: forall m b. (Alternative m, Monad m) => (b > m (b, b)) > b > m (b, [b])Source
The monadic version of revSplitList
.
nsplit :: (a > Maybe (a, a)) > [b] > a > Maybe ([a], a)Source
Repeatedly applies a binary destructor function to a term for every element in a provided list.
Application is reverse, or rightassociative, 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
.
stripList :: forall a. (a > Maybe (a, a)) > a > [a]Source
Repeatedly applies a binary destructor function to a term until failure.
Application is forward, or leftassociative, 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]
.
stripListM :: forall m a. (Alternative m, Monad m) => (a > m (a, a)) > a > m [a]Source
The monadic version of stripList
.
Methods for Searching and Manipulating Lists
forall :: (a > Bool) > [a] > BoolSource
An alias to all
for HOL users who are more familiar with this name.
exists :: (a > Bool) > [a] > BoolSource
An alias to any
for HOL users who are more familiar with this name.
partition :: (a > Bool) > [a] > ([a], [a])Source
Separates a list of elements using a predicate. A reexport of partition
.
mapFilter :: (a > Maybe b) > [a] > [b]Source
An alias to mapMaybe
for HOL users more familiar with this name.
mapFilterM :: (Alternative m, Monad m) => (a > m b) > [a] > m [b]Source
tryFind :: (Monad m, MonadPlus m) => (a > m b) > [a] > m bSource
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.
dropWhileEnd :: (a > Bool) > [a] > [a]Source
Drops elements from the end of a list while a predicate is true. A reexport
of dropWhileEnd
.
remove :: (a > Bool) > [a] > Maybe (a, [a])Source
Separates the first element of a list that satisfies a predicate. Fails with
Nothing
if no such element is found.
trySplitAt :: Int > [a] > Maybe ([a], [a])Source
chopList :: Int > [a] > Maybe ([a], [a])Source
An alias to trySplitAt
for HOL users more familiar with this name
index :: Eq a => a > [a] > Maybe IntSource
An alias to elemIndex
for HOL users more familiar with this name.
stripPrefix :: Eq a => [a] > [a] > Maybe [a]Source
Drops the given prefix from a list. Fails with Nothing
if there is no such
prefix. A reexport of stripPrefix
.
shareOut :: [[a]] > [b] > Maybe [[b]]Source
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"]
Set Operations on Lists
mem :: Eq a => a > [a] > BoolSource
An alias to elem
for HOL users who are more familiar with this name.
insertMap :: Eq a => a > b > [(a, b)] > [(a, b)]Source
Inserts, or updates, a key value pair in an association list.
Note that this insert is unordered, but uniqueness preserving.
intersect :: Eq a => [a] > [a] > [a]Source
Finds the intersection of two lists. A reexport of intersect
.
Set Operations Parameterized by Predicate
mem' :: (a > a > Bool) > a > [a] > BoolSource
A version of mem
where the membership test is an explicit predicate, rather
than a strict equality test.
insert' :: (a > a > Bool) > a > [a] > [a]Source
A version of insert
where the uniqueness test is an explicit predicate,
rather than a strict equality test.
union' :: (a > a > Bool) > [a] > [a] > [a]Source
A version of union
where the uniqueness test is an explicit predicate,
rather than a strict equality test.
unions' :: (a > a > Bool) > [[a]] > [a]Source
A version of unions
where the uniqueness test is an explicit predicate,
rather than a strict equality test.
subtract' :: (a > a > Bool) > [a] > [a] > [a]Source
A version of subtract
where the uniqueness test is an explicit predicate,
rather than a strict equality test.
group' :: (a > a > Bool) > [a] > [[a]]Source
Groups neighbors in a list together based on a predicate. A reexport of
groupBy
.
uniq' :: Eq a => (a > a > Bool) > [a] > [a]Source
A version of uniq
that eliminates elements based on a provided predicate.
setify' :: Eq a => (a > a > Bool) > (a > a > Bool) > [a] > [a]Source
A version of setify
that eliminates elements based on a provided predicate.
Operations on "Num" Types
The following are aliases to frequently used values and functions for
arbitraryprecision integers. Typically, they are used when converting to and
from numbers in the implementation language and the logic language. The
aliases clarify the intended use and saves us from having lots of explicit
type annotations to force Integer
values.
numdom :: Real a => a > RationalSource
Converts a real number to a rational representation.
An alias to toRational
for HOL users more familiar with this name.
numerator :: Rational > IntegerSource
Returns the numerator of a rational number. A reexport of numerator
.
denominator :: Rational > IntegerSource
Returns the denominator of a rational number. A reexport of denominator
.
gcdNum :: Integer > Integer > IntegerSource
Finds the least common denominator between two numbers. An alias to gcd
for
HOL users more familiar with this name.
lcmNum :: Integer > Integer > IntegerSource
Finds the least common multiplier between two numbers. An alias to lcm
for
HOL users more familiar with this name.
numOfString :: forall a. (Eq a, Num a) => String > Maybe aSource
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
Classes for Common "Language" Operations
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.
A primitive language operation that always fails. Typically this is
written using throw
.
An instance of _FAIL
with a fixed failure string.
A primitive language operation that always succeeds.
A language combinator for branching based on failure. The language
equivalent of the <>
operator.
A language combinator that performs the first operation in a list.
A language combinator that fails if the wrapped operation doesn't invoke some change, i.e. a tactic fails to change the goal state.
A language combinator that prevents the wrapped operation from having an
effect if it fails. The language equivalent of the backtracking try
operator.
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.
Miscellaneous Reexported Libraries
module HaskHOL.Core.Lib.Lift
Reexports deriveLift
, deriveLiftMany
, and Lift
to be used with
our extensible state mechanisms.
module Control.Applicative
Reexports Applicative
, Alternative
, and the utility functions for
use with the HOL
monad.
module Control.DeepSeq
Reexports the entirety of the library, but currently only NFData
is
used. Necessary for using the Criterion benchmarking library.
module Control.Monad
Reexports the entirety of the library for use with the HOL
monad.
module Data.Maybe
Reexports the entirety of the library. Used primarily to make interacting with primitive rules easier at later points in the system.
module Data.Either
Reexports the entirety of the library. Used primarily to make interacting with primitive rules easier at later points in the system.
module Data.Typeable
Reexports the Typeable
class name for use in deriving clauses.
Reexports the entirety of the library. Used primarily for its Assoc
data type, but also contains a number of primitives used by the parser.