Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Lib

Contents

Time and timeout
Map aliases
Orphan instances

Synopsis

data Failing a
- = Success a
- | Failure [ErrorMsg]
failing :: ([String] -> b) -> (a -> b) -> Failing a -> b
class Foldable c => SetLike c where
- slView :: forall a. c a -> Maybe (a, c a)
- slMap :: forall a b. Ord b => (a -> b) -> c a -> c b
- slUnion :: Ord a => c a -> c a -> c a
- slEmpty :: c a
- slSingleton :: a -> c a
slInsert :: (SetLike set, Ord a) => a -> set a -> set a
prettyFoldable :: (Foldable t, Pretty a) => t a -> Doc
setAny :: Foldable t => (a -> Bool) -> t a -> Bool
setAll :: Foldable t => (a -> Bool) -> t a -> Bool
flatten :: Ord a => Set (Set a) -> Set a
tryfind :: Foldable t => (a -> Failing r) -> t a -> Failing r
tryfindM :: Monad m => (t -> m (Failing a)) -> [t] -> m (Failing a)
runRS :: RWS r () s a -> r -> s -> (a, s)
evalRS :: RWS r () s a -> r -> s -> a
settryfind :: (t -> Failing a) -> Set t -> Failing a
(|=>) :: Ord k => k -> a -> Map k a
(|->) :: Ord k => k -> a -> Map k a -> Map k a
fpf :: Ord a => Map a b -> a -> Maybe b
timeComputation :: IO r -> IO (r, NominalDiffTime)
timeMessage :: (r -> NominalDiffTime -> String) -> IO r -> IO r
time :: IO r -> IO r
timeout :: String -> DiffTime -> IO r -> IO (Either String r)
compete :: [IO a] -> IO a
defined :: Ord t => Map t a -> t -> Bool
undefine :: forall k a. Ord k => k -> Map k a -> Map k a
apply :: Ord k => Map k a -> k -> Maybe a
tryApplyD :: Ord k => Map k a -> k -> a -> a
allpairs :: forall a b c set. (SetLike set, Ord c) => (a -> b -> c) -> set a -> set b -> set c
distrib :: Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
image :: (Ord b, Ord a) => (a -> b) -> Set a -> Set b
optimize :: forall s a b. (SetLike s, Foldable s) => (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
minimize :: (Ord b, SetLike s, Foldable s) => (a -> b) -> s a -> Maybe a
maximize :: (Ord b, SetLike s, Foldable s) => (a -> b) -> s a -> Maybe a
can :: (t -> Failing a) -> t -> Bool
allsets :: forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsubsets :: forall a. Ord a => Set a -> Set (Set a)
allnonemptysubsets :: forall a. Ord a => Set a -> Set (Set a)
mapfilter :: (a -> Failing b) -> [a] -> [b]
setmapfilter :: Ord b => (a -> Failing b) -> Set a -> Set b
(∅) :: (Monoid (c a), SetLike c) => c a
deepen :: (Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
newtype Depth = Depth Int
testLib :: Test

Documentation

data Failing a #

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

Constructors

Success a
Failure [ErrorMsg]

Instances

Instances details

MonadFail Failing Source #
Instance details Defined in Data.Logic.ATP.Lib Methods fail :: String -> Failing a #
Alternative Failing
Instance details Defined in Control.Applicative.Error Methods empty :: Failing a # (<\|>) :: Failing a -> Failing a -> Failing a # some :: Failing a -> Failing [a] # many :: Failing a -> Failing [a] #
Applicative Failing
Instance details Defined in Control.Applicative.Error Methods pure :: a -> Failing a # (<>) :: Failing (a -> b) -> Failing a -> Failing b # liftA2 :: (a -> b -> c) -> Failing a -> Failing b -> Failing c # (>) :: Failing a -> Failing b -> Failing b # (<*) :: Failing a -> Failing b -> Failing a #
Functor Failing
Instance details Defined in Control.Applicative.Error Methods fmap :: (a -> b) -> Failing a -> Failing b # (<$) :: a -> Failing b -> Failing a #
Monad Failing Source #
Instance details Defined in Data.Logic.ATP.Lib Methods (>>=) :: Failing a -> (a -> Failing b) -> Failing b # (>>) :: Failing a -> Failing b -> Failing b # return :: a -> Failing a #
Data a => Data (Failing a) Source #
Instance details Defined in Data.Logic.ATP.Lib 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 :: forall r r'. (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) #
Read a => Read (Failing a) Source #
Instance details Defined in Data.Logic.ATP.Lib Methods readsPrec :: Int -> ReadS (Failing a) # readList :: ReadS [Failing a] # readPrec :: ReadPrec (Failing a) # readListPrec :: ReadPrec [Failing a] #
Show a => Show (Failing a)
Instance details Defined in Control.Applicative.Error Methods showsPrec :: Int -> Failing a -> ShowS # show :: Failing a -> String # showList :: [Failing a] -> ShowS #
Eq a => Eq (Failing a) Source #
Instance details Defined in Data.Logic.ATP.Lib Methods (==) :: Failing a -> Failing a -> Bool # (/=) :: Failing a -> Failing a -> Bool #
Ord a => Ord (Failing a) Source #
Instance details Defined in Data.Logic.ATP.Lib 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 #
Pretty a => Pretty (Failing a) Source #
Instance details Defined in Data.Logic.ATP.Lib Methods pPrintPrec :: PrettyLevel -> Rational -> Failing a -> Doc # pPrint :: Failing a -> Doc # pPrintList :: PrettyLevel -> [Failing a] -> Doc #

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.

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

Instances details

SetLike Seq Source #
Instance details Defined in Data.Logic.ATP.Lib Methods slView :: Seq a -> Maybe (a, Seq a) Source # slMap :: forall a b. 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 #
Instance details Defined in Data.Logic.ATP.Lib Methods slView :: Set a -> Maybe (a, Set a) Source # slMap :: forall a b. 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 #
SetLike List Source #
Instance details Defined in Data.Logic.ATP.Lib Methods slView :: [a] -> Maybe (a, [a]) Source # slMap :: forall a b. Ord b => (a -> b) -> [a] -> [b] Source # slUnion :: Ord a => [a] -> [a] -> [a] Source # slEmpty :: [a] Source # slSingleton :: a -> [a] Source #

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

prettyFoldable :: (Foldable t, Pretty a) => t a -> Doc 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.

newtype Depth Source #

Constructors

Depth Int

Instances

Instances details

Enum Depth Source #
Instance details Defined in Data.Logic.ATP.Lib Methods succ :: Depth -> Depth # pred :: Depth -> Depth # toEnum :: Int -> Depth # fromEnum :: Depth -> Int # enumFrom :: Depth -> [Depth] # enumFromThen :: Depth -> Depth -> [Depth] # enumFromTo :: Depth -> Depth -> [Depth] # enumFromThenTo :: Depth -> Depth -> Depth -> [Depth] #
Show Depth Source #
Instance details Defined in Data.Logic.ATP.Lib Methods showsPrec :: Int -> Depth -> ShowS # show :: Depth -> String # showList :: [Depth] -> ShowS #
Eq Depth Source #
Instance details Defined in Data.Logic.ATP.Lib Methods (==) :: Depth -> Depth -> Bool # (/=) :: Depth -> Depth -> Bool #
Ord Depth Source #
Instance details Defined in Data.Logic.ATP.Lib Methods compare :: Depth -> Depth -> Ordering # (<) :: Depth -> Depth -> Bool # (<=) :: Depth -> Depth -> Bool # (>) :: Depth -> Depth -> Bool # (>=) :: Depth -> Depth -> Bool # max :: Depth -> Depth -> Depth # min :: Depth -> Depth -> Depth #
Pretty Depth Source #
Instance details Defined in Data.Logic.ATP.Lib Methods pPrintPrec :: PrettyLevel -> Rational -> Depth -> Doc # pPrint :: Depth -> Doc # pPrintList :: PrettyLevel -> [Depth] -> Doc #

testLib :: Test Source #

Orphan instances

MonadFail Failing Source #
Instance details Methods fail :: String -> Failing a #
Monad Failing Source #
Instance details Methods (>>=) :: Failing a -> (a -> Failing b) -> Failing b # (>>) :: Failing a -> Failing b -> Failing b # return :: a -> Failing a #
Data a => Data (Failing a) Source #
Instance details 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 :: forall r r'. (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) #
Read a => Read (Failing a) Source #
Instance details Methods readsPrec :: Int -> ReadS (Failing a) # readList :: ReadS [Failing a] # readPrec :: ReadPrec (Failing a) # readListPrec :: ReadPrec [Failing a] #
Eq a => Eq (Failing a) Source #
Instance details Methods (==) :: Failing a -> Failing a -> Bool # (/=) :: Failing a -> Failing a -> Bool #
Ord a => Ord (Failing a) Source #
Instance details 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 #
Pretty a => Pretty (Failing a) Source #
Instance details Methods pPrintPrec :: PrettyLevel -> Rational -> Failing a -> Doc # pPrint :: Failing a -> Doc # pPrintList :: PrettyLevel -> [Failing a] -> Doc #