HaskHOL.Core.Lib

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.

Function Combinators

iComb :: a -> a

The I combinator. An alias for id.

kComb :: a -> b -> a

The K combinator. An alias for const.

cComb :: (a -> b -> c) -> b -> a -> c

The C combinator. An alias for flip.

wComb :: (a -> a -> b) -> a -> b

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)

The FF combinator. An alias for the arrow combinator ***.

ffCombM :: Monad m => (a -> m c) -> (b -> m d) -> (a, b) -> m (c, d)

The monadic version of the FF combinator. An alias for the arrow combinator *** lifted for Kleisli arrows.

liftM1 :: Monad m => (a -> b -> m c) -> m a -> b -> m c

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

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

Swaps the order of a pair. A re-export of swap.

pairMap :: (a -> b) -> (a, a) -> (b, b)

Applies a function to both elements of a pair using the *** operator.

pairMapM :: Monad m => (a -> m b) -> (a, a) -> m (b, b)

The monadic version of pairMap.

first :: (a -> c) -> (a, b) -> (c, b)

Applies a function only to the first element of a pair. A re-export of first.

firstM :: Monad m => (a -> m c) -> (a, b) -> m (c, b)

A monadic version of first lifted for Kleisli arrows.

second :: (b -> c) -> (a, b) -> (a, c)

Applies a function only to the second element of a pair. A re-export of second.

secondM :: Monad m => (b -> m c) -> (a, b) -> m (a, c)

A monadic version of second lifted for Kleisli arrows.

Basic Operations on Lists

tryHead :: [a] -> Maybe a

A safe version of head. Fails with Nothing when trying to take the head of an empty list.

tryTail :: [a] -> Maybe [a]

A safe version of tail. Fails with Nothing when trying to take the tail of an empty list.

tryInit :: [a] -> Maybe [a]

A safe version of init. Fails with Nothing when trying to drop the last element of an empty list.

butLast :: [a] -> Maybe [a]

An alias to tryInit for HOL users more familiar with this name.

tryLast :: [a] -> Maybe a

A safe version of last. Fails with Nothing when trying to take the last element of an empty list.

tryIndex :: [a] -> Int -> Maybe a

A safe version of index. Fails with Nothing if the selected index does not exist.

el :: Int -> [a] -> Maybe a

An alias to tryIndex for HOL users more familiar with this name. Note that the order of the arguments is flipped.

rev :: [a] -> [a]

An alias to reverse for HOL users more familiar with this name.

Basic Operations on Association Lists

assoc :: Eq a => a -> [(a, b)] -> Maybe b

An alias to lookup for HOL users more familiar with this name.

revLookup :: Eq a => a -> [(b, a)] -> Maybe b

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.

revAssoc :: Eq a => a -> [(b, a)] -> Maybe b

An alias to revLookup for HOL users who are more familiar with this name.

assocd :: Eq a => a -> [(a, b)] -> b -> b

An alias to lookupd for HOL users who are more familiar with this name.

lookupd :: Eq a => a -> [(a, b)] -> b -> b

A version of lookup that defaults to a provided value rather than fail.

revLookupd :: Eq a => a -> [(b, a)] -> b -> b

A version of revLookup that defaults to a provided value rather than fail.

revAssocd :: Eq a => a -> [(b, a)] -> b -> b

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 Bool

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 Bool

The opposite of can. Functionally equivalent to

 \ f -> liftM not . can f

check :: (a -> Bool) -> a -> Maybe a

Checks if a predicate succeeds for a provided value, returning that value guarded by a Maybe type if so.

note :: a -> Maybe b -> Either a b

Takes a default error value to convert a Maybe type to an Either type.

hush :: Either a b -> Maybe b

Suppresses the error value of an Either type to convert it to a Maybe type.

fromRight :: Either err a -> a

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.

fromRightM :: MonadPlus m => Either err a -> m a

A version of fromRight that maps Left values to mzero rather than failing.

fromJustM :: MonadPlus m => Maybe a -> m a

A version of fromJust that maps Nothing values to mzero rather than failing.

class Monad m => LiftOption l m where

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.

Methods

liftO :: l a -> m a

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 b

A version of =<< composed with liftO for the right argument.

(<#<) :: (b -> m c) -> (a -> l b) -> a -> m c

A version of <=< composed with liftO for the right argument.

(<#>) :: (a -> b -> m c) -> l a -> b -> m c

A version of liftM1 composed with liftO for the right argument.

Instances

MonadPlus m => LiftOption Maybe m

MonadPlus m => LiftOption (Either a) m

class (Alternative m, Monad m) => Note m where

The Note class provides an ad hoc way of tagging an error case with a string.

Methods

(<?>) :: m a -> String -> m a

Used to annotate more precise error messages. Replaces the <|> operator in cases such as

 ... <|> fail "..."

failWhen :: m Bool -> String -> m ()

Replaces the common pattern

 m >>= \ cond -> if cond then fail "..."

The default case is defined in terms of empty and <?>.

Instances

Note (Either String)

Note (HOL cls thry)

Methods for Function Repetition

funpow :: Int -> (a -> a) -> a -> a

Repeatedly applies a function to an argument n times. Rather than fail, the original argument is returned when n<=0.

funpowM :: Monad m => Int -> (a -> m a) -> a -> m a

The monadic version of funpow.

repeatM :: (Alternative m, Monad m) => (a -> m a) -> a -> m a

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]

A safe version of a list map for functions of arity 2. Fails with Nothing if the two lists are of different lengths.

map2M :: (Monad m, MonadPlus m) => (a -> b -> m c) -> [a] -> [b] -> m [c]

The monadic version of map2. Fails with mzero if the two lists are of different lengths.

doList :: Monad m => (a -> m b) -> [a] -> m ()

Map a monadic function over a list, ignoring the results. A re-export of mapM_.

allpairs :: (a -> b -> c) -> [a] -> [b] -> [c]

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 -> b

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 b

The monadic version of itlist.

foldrM :: (Foldable t, Monad m) => (a -> b -> m b) -> b -> t a -> m b

The monadic version of foldr. A re-export of foldrM.

revItlist :: (a -> b -> b) -> [a] -> b -> b

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.

foldlM :: (Foldable t, Monad m) => (a -> b -> m a) -> a -> t b -> m a

The monadic version of foldl. A re-export of foldlM.

tryFoldr1 :: (a -> a -> a) -> [a] -> Maybe a

A safe version of foldr1. Fails with Nothing if an empty list is provided as an argument.

endItlist :: (a -> a -> a) -> [a] -> Maybe a

An alias to tryFoldr1 for HOL users more familiar with this name.

foldr1M :: (Monad m, MonadPlus m) => (a -> a -> m a) -> [a] -> m a

The monadic version of foldr1. Fails with mzero if an empty list is provided as an argument.

foldr2 :: (a -> b -> c -> c) -> c -> [a] -> [b] -> Maybe c

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 c

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.

foldr2M :: (Monad m, MonadPlus m) => (a -> b -> c -> m c) -> c -> [a] -> [b] -> m c

The monadic version of foldr2. Fails with mzero if the two lists are of different lengths.

foldl2 :: (c -> a -> b -> c) -> c -> [a] -> [b] -> Maybe c

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 c

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.

foldl2M :: (Monad m, MonadPlus m) => (c -> a -> b -> m c) -> c -> [a] -> [b] -> m c

The monadic version of foldl2. Fails with mzero if the two lists are of different lengths.

Methods for Sorting and Merging Lists

sort :: Eq a => (a -> a -> Bool) -> [a] -> [a]

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.

sortBy :: (a -> a -> Ordering) -> [a] -> [a]

A more traditional sort using an Ordering relationship between elements. A re-export of sortBy.

merge :: (a -> a -> Bool) -> [a] -> [a] -> [a]

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.

mergesort :: forall a. (a -> a -> Bool) -> [a] -> [a]

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.

Methods for Splitting and Stripping Binary Terms

splitList :: (b -> Maybe (a, b)) -> b -> ([a], b)

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).

splitListM :: (Alternative m, Monad m) => (b -> m (a, b)) -> b -> m ([a], b)

The monadic version of splitList.

revSplitList :: forall a. (a -> Maybe (a, a)) -> a -> (a, [a])

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]).

revSplitListM :: forall m b. (Alternative m, Monad m) => (b -> m (b, b)) -> b -> m (b, [b])

The monadic version of revSplitList.

nsplit :: (a -> Maybe (a, a)) -> [b] -> a -> Maybe ([a], a)

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.

nsplitM :: Monad m => (b -> m (b, b)) -> [c] -> b -> m ([b], b)

The monadic version of nsplit.

stripList :: forall a. (a -> Maybe (a, a)) -> a -> [a]

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].

stripListM :: forall m a. (Alternative m, Monad m) => (a -> m (a, a)) -> a -> m [a]

The monadic version of stripList.

Methods for Searching and Manipulating Lists

forall :: (a -> Bool) -> [a] -> Bool

An alias to all for HOL users who are more familiar with this name.

forall2 :: (a -> b -> Bool) -> [a] -> [b] -> Maybe Bool

A version of all for predicates of arity 2. Iterates down two lists simultaneously with map2, using and to combine the results.

exists :: (a -> Bool) -> [a] -> Bool

An alias to any for HOL users who are more familiar with this name.

partition :: (a -> Bool) -> [a] -> ([a], [a])

Separates a list of elements using a predicate. A re-export of partition.

mapFilter :: (a -> Maybe b) -> [a] -> [b]

An alias to mapMaybe for HOL users more familiar with this name.

mapFilterM :: (Alternative m, Monad m) => (a -> m b) -> [a] -> m [b]

The monadic version of mapFilter. The '(|)' operator is used for branching.

find :: (a -> Bool) -> [a] -> Maybe a

A re-export of find.

findM :: (Monad m, MonadPlus m) => (a -> m Bool) -> [a] -> m a

The monadic version of find. Fails if the monadic predicate does. Also fails with mzero if an empty list is provided.

tryFind :: (Monad m, MonadPlus m) => (a -> m b) -> [a] -> m b

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.

flat :: [[a]] -> [a]

An alias to concat for HOL users who are more familiar with this name.

dropWhileEnd :: (a -> Bool) -> [a] -> [a]

Drops elements from the end of a list while a predicate is true. A re-export of dropWhileEnd.

remove :: (a -> Bool) -> [a] -> Maybe (a, [a])

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])

A safe version of splitAt. Fails with Nothing if a split is attempted at an index that doesn't exist.

chopList :: Int -> [a] -> Maybe ([a], [a])

An alias to trySplitAt for HOL users more familiar with this name

elemIndex :: Eq a => a -> [a] -> Maybe Int

Returns the first index where an element appears in list. Fails with Nothing if no such element is found. A re-export of elemIndex.

index :: Eq a => a -> [a] -> Maybe Int

An alias to elemIndex for HOL users more familiar with this name.

stripPrefix :: Eq a => [a] -> [a] -> Maybe [a]

Drops the given prefix from a list. Fails with Nothing if there is no such prefix. A re-export of stripPrefix.

uniq :: Eq a => [a] -> [a]

Removes adjacent, equal elements from a list.

shareOut :: [[a]] -> [b] -> Maybe [[b]]

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] -> Bool

An alias to elem for HOL users who are more familiar with this name.

insert :: Eq a => a -> [a] -> [a]

Inserts an item into a list if it would be a unique element.

Important note: This insert is unordered, unlike the insert in the Data.List module.

insertMap :: Eq a => a -> b -> [(a, b)] -> [(a, b)]

Inserts, or updates, a key value pair in an association list.

Note that this insert is unordered, but uniqueness preserving.

union :: Eq a => [a] -> [a] -> [a]

Unions two list maintaining uniqueness of elements.

Important note: This union is unordered, unlike the union in the Data.List module.

unions :: Eq a => [[a]] -> [a]

Unions a list of lists using union.

intersect :: Eq a => [a] -> [a] -> [a]

Finds the intersection of two lists. A re-export of intersect.

delete :: Eq a => a -> [a] -> [a]

Removes an item from a list. A re-export of delete.

(\\) :: Eq a => [a] -> [a] -> [a]

Subtracts one list from the other. A re-export of \\.

subset :: Eq a => [a] -> [a] -> Bool

Tests if the first list is a subset of the second.

setEq :: Eq a => [a] -> [a] -> Bool

A test for set equality using subset.

setify :: Eq a => [a] -> [a]

An alias to nub for HOL users more familiar with this name.

nub :: Eq a => [a] -> [a]

Converts a list to a set by removing duplicates. A re-export of nub.

Set Operations Parameterized by Predicate

mem' :: (a -> a -> Bool) -> a -> [a] -> Bool

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]

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]

A version of union where the uniqueness test is an explicit predicate, rather than a strict equality test.

unions' :: (a -> a -> Bool) -> [[a]] -> [a]

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]

A version of subtract where the uniqueness test is an explicit predicate, rather than a strict equality test.

group' :: (a -> a -> Bool) -> [a] -> [[a]]

Groups neighbors in a list together based on a predicate. A re-export of groupBy.

uniq' :: Eq a => (a -> a -> Bool) -> [a] -> [a]

A version of uniq that eliminates elements based on a provided predicate.

setify' :: Eq a => (a -> a -> Bool) -> (a -> a -> Bool) -> [a] -> [a]

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 arbitrary-precision 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.

num0 :: Integer

 0 :: Integer

num1 :: Integer

 1 :: Integer

num2 :: Integer

 2 :: Integer

num10 :: Integer

 10 :: Integer

pow2 :: Integer -> Integer

 x ^ (2 :: Integer)

pow10 :: Integer -> Integer

 x ^ (10 :: Integer)

numdom :: Real a => a -> Rational

Converts a real number to a rational representation. An alias to toRational for HOL users more familiar with this name.

numerator :: Rational -> Integer

Returns the numerator of a rational number. A re-export of numerator.

denominator :: Rational -> Integer

Returns the denominator of a rational number. A re-export of denominator.

gcdNum :: Integer -> Integer -> Integer

Finds the least common denominator between two numbers. An alias to gcd for HOL users more familiar with this name.

lcmNum :: Integer -> Integer -> Integer

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 a

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.

class Lang a where

The Lang class defines common language operations and combinators not based on sequencing.

Methods

_FAIL :: String -> a

A primitive language operation that always fails. Typically this is written using throw.

_NO :: a

An instance of _FAIL with a fixed failure string.

_ALL :: a

A primitive language operation that always succeeds.

_ORELSE :: a -> a -> a

A language combinator for branching based on failure. The language equivalent of the <|> operator.

_FIRST :: [a] -> a

A language combinator that performs the first operation in a list.

_CHANGED :: 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.

_TRY :: 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.

class LangSeq a where

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.

Methods

_THEN :: a -> a -> a

A language combinator that sequences operations.

_REPEAT :: a -> a

A language combinator that repeatedly applies a language operation until failure.

_EVERY :: [a] -> a

A language combinator that performs every operation in a list sequentially.

Miscellaneous Re-exported Libraries

module HaskHOL.Core.Lib.Lift

Re-exports deriveLift, deriveLiftMany, and Lift to be used with our extensible state mechanisms.

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.Typeable

Re-exports the Typeable class name for use in deriving clauses.

module Text.ParserCombinators.Parsec.Expr

Re-exports the entirety of the library. Used primarily for its Assoc data type, but also contains a number of primitives used by the parser.