atp-haskell-1.14: Translation from Ocaml to Haskell of John Harrison's ATP code

Safe HaskellNone
LanguageHaskell98

Data.Logic.ATP.Lib

Contents

Synopsis

Documentation

data Failing a :: * -> * #

An error idiom. Rather like the error monad, but collect all | errors together

Constructors

Success a 
Failure [ErrorMsg] 

Instances

Functor Failing 

Methods

fmap :: (a -> b) -> Failing a -> Failing b #

(<$) :: a -> Failing b -> Failing a #

Applicative Failing 

Methods

pure :: a -> Failing a #

(<*>) :: Failing (a -> b) -> Failing a -> Failing b #

(*>) :: Failing a -> Failing b -> Failing b #

(<*) :: Failing a -> Failing b -> Failing a #

Alternative Failing 

Methods

empty :: Failing a #

(<|>) :: Failing a -> Failing a -> Failing a #

some :: Failing a -> Failing [a] #

many :: Failing a -> Failing [a] #

Show a => Show (Failing a) 

Methods

showsPrec :: Int -> Failing a -> ShowS #

show :: Failing a -> String #

showList :: [Failing a] -> ShowS #

failing :: ([String] -> b) -> (a -> b) -> Failing a -> b Source #

class Foldable c => SetLike c where Source #

A simple class, slightly more powerful than Foldable, so we can write functions that operate on the elements of a set or a list.

Minimal complete definition

slView, slMap, slUnion, slEmpty, slSingleton

Methods

slView :: forall a. c a -> Maybe (a, c a) Source #

slMap :: forall a b. Ord b => (a -> b) -> c a -> c b Source #

slUnion :: Ord a => c a -> c a -> c a Source #

slEmpty :: c a Source #

slSingleton :: a -> c a Source #

Instances

SetLike [] Source # 

Methods

slView :: [a] -> Maybe (a, [a]) Source #

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

slUnion :: Ord a => [a] -> [a] -> [a] Source #

slEmpty :: [a] Source #

slSingleton :: a -> [a] Source #

SetLike Seq Source # 

Methods

slView :: Seq a -> Maybe (a, Seq a) Source #

slMap :: Ord b => (a -> b) -> Seq a -> Seq b Source #

slUnion :: Ord a => Seq a -> Seq a -> Seq a Source #

slEmpty :: Seq a Source #

slSingleton :: a -> Seq a Source #

SetLike Set Source # 

Methods

slView :: Set a -> Maybe (a, Set a) Source #

slMap :: Ord b => (a -> b) -> Set a -> Set b Source #

slUnion :: Ord a => Set a -> Set a -> Set a Source #

slEmpty :: Set a Source #

slSingleton :: a -> Set a Source #

slInsert :: (SetLike set, Ord a) => a -> set a -> set a Source #

setAny :: Foldable t => (a -> Bool) -> t a -> Bool Source #

setAll :: Foldable t => (a -> Bool) -> t a -> Bool Source #

flatten :: Ord a => Set (Set a) -> Set a Source #

tryfind :: Foldable t => (a -> Failing r) -> t a -> Failing r Source #

tryfindM :: Monad m => (t -> m (Failing a)) -> [t] -> m (Failing a) Source #

runRS :: RWS r () s a -> r -> s -> (a, s) Source #

evalRS :: RWS r () s a -> r -> s -> a Source #

settryfind :: (t -> Failing a) -> Set t -> Failing a Source #

(|=>) :: Ord k => k -> a -> Map k a Source #

(|->) :: Ord k => k -> a -> Map k a -> Map k a Source #

fpf :: Ord a => Map a b -> a -> Maybe b Source #

Time and timeout

timeComputation :: IO r -> IO (r, NominalDiffTime) Source #

Perform an IO operation and return the elapsed time along with the result.

timeMessage :: (r -> NominalDiffTime -> String) -> IO r -> IO r Source #

Perform an IO operation and output a message about how long it took.

time :: IO r -> IO r Source #

Output elapsed time

timeout :: String -> DiffTime -> IO r -> IO (Either String r) Source #

Allow a computation to proceed for a given amount of time.

compete :: [IO a] -> IO a Source #

Run several IO operations in parallel, return the result of the first one that completes and kill the others.

Map aliases

defined :: Ord t => Map t a -> t -> Bool Source #

undefine :: forall k a. Ord k => k -> Map k a -> Map k a Source #

Undefinition.

apply :: Ord k => Map k a -> k -> Maybe a Source #

tryApplyD :: Ord k => Map k a -> k -> a -> a Source #

allpairs :: forall a b c set. (SetLike set, Ord c) => (a -> b -> c) -> set a -> set b -> set c Source #

distrib :: Ord a => Set (Set a) -> Set (Set a) -> Set (Set a) Source #

image :: (Ord b, Ord a) => (a -> b) -> Set a -> Set b Source #

optimize :: forall s a b. (SetLike s, Foldable s) => (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a Source #

minimize :: (Ord b, SetLike s, Foldable s) => (a -> b) -> s a -> Maybe a Source #

maximize :: (Ord b, SetLike s, Foldable s) => (a -> b) -> s a -> Maybe a Source #

can :: (t -> Failing a) -> t -> Bool Source #

allsets :: forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b) Source #

allsubsets :: forall a. Ord a => Set a -> Set (Set a) Source #

allnonemptysubsets :: forall a. Ord a => Set a -> Set (Set a) Source #

mapfilter :: (a -> Failing b) -> [a] -> [b] Source #

setmapfilter :: Ord b => (a -> Failing b) -> Set a -> Set b Source #

(∅) :: (Monoid (c a), SetLike c) => c a Source #

deepen :: (Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth) Source #

Try f with higher and higher values of n until it succeeds, or optional maximum depth limit is exceeded.

Orphan instances

Monad Failing Source # 

Methods

(>>=) :: Failing a -> (a -> Failing b) -> Failing b #

(>>) :: Failing a -> Failing b -> Failing b #

return :: a -> Failing a #

fail :: String -> Failing a #

Eq a => Eq (Failing a) Source # 

Methods

(==) :: Failing a -> Failing a -> Bool #

(/=) :: Failing a -> Failing a -> Bool #

Data a => Data (Failing a) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Failing a -> c (Failing a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Failing a) #

toConstr :: Failing a -> Constr #

dataTypeOf :: Failing a -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Failing a)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Failing a)) #

gmapT :: (forall b. Data b => b -> b) -> Failing a -> Failing a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Failing a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Failing a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Failing a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Failing a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Failing a -> m (Failing a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Failing a -> m (Failing a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Failing a -> m (Failing a) #

Ord a => Ord (Failing a) Source # 

Methods

compare :: Failing a -> Failing a -> Ordering #

(<) :: Failing a -> Failing a -> Bool #

(<=) :: Failing a -> Failing a -> Bool #

(>) :: Failing a -> Failing a -> Bool #

(>=) :: Failing a -> Failing a -> Bool #

max :: Failing a -> Failing a -> Failing a #

min :: Failing a -> Failing a -> Failing a #

Read a => Read (Failing a) Source # 
Pretty a => Pretty (Failing a) Source #