{-# LANGUAGE Safe,TypeOperators, MultiParamTypeClasses, FunctionalDependencies, TypeFamilies, ConstraintKinds, PolyKinds #-}
 module Math.Tools.CoFunctor where
 import safe Math.Tools.I
 import safe Math.Tools.Universe
 import Data.Functor.Contravariant

 -- | For exposition of classical logic used here,
 -- see "Lawvere,Rosebrugh: Sets for mathematics".
 -- 
 -- > (x |>> f) |>> g == x |>> (f . g)
 -- > inverse_image g (inverse_image f x) == inverse_image (f . g) x
 -- Notice, CoFunctor is nowadays in base, so
 -- please use Data.Functor.Contravariant.Contravariant
 type CoFunctor p = Contravariant p

 inverseImage :: (CoFunctor p) => (a -> b) -> p b -> p a
 inverseImage :: forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage = (a -> b) -> p b -> p a
forall a' a. (a' -> a) -> p a -> p a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap
  
 (|>>) :: (CoFunctor p) => p b -> (a -> b) -> p a
 |>> :: forall (p :: * -> *) b a. CoFunctor p => p b -> (a -> b) -> p a
(|>>) = ((a -> b) -> p b -> p a) -> p b -> (a -> b) -> p a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> p b -> p a
forall a' a. (a' -> a) -> p a -> p a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap

  -- class (Contravariant p) => CoFunctor p where
  --    inverse_image :: (a -> b) -> p b -> p a
  --    (|>>) :: p b -> (a -> b) -> p a
  --    (|>>) = flip inverse_image
  --    inverse_image = contramap

 class Representable p where
    type Representation p :: * -> *
    represent :: Representation p a -> p a
    (!>) :: p a -> (Representation p a -> p a) -> p a

 class Propositional p where
    runProposition :: p a -> a -> p ()

 class (Propositional p) => BinaryLogic p where
    toBool :: p () -> Bool

 class (CoFunctor p) => Relational p where
    relation   :: (a -> p b) -> p (a,b)
    unrelation :: p (a,b)    -> a -> p b

  -- direct_image(f) -| inverse_image(f) -| universal(f)

 class (CoFunctor p) => Existential p where
    directImage :: (Universe a,Eq b) => (a -> b) -> p a -> p b
    universalImage   :: (Universe a,Eq b) => (a -> b) -> p a -> p b


 class (CoFunctor p) => Difference p minus | p -> minus where
    difference :: (p a -> p b) -> p (b `minus` a)
    undifference :: p (b `minus` a) -> p a -> p b

 class (Eq c, CoFunctor p) => HasEqualizers p c where
    -- minimal complete definition: equalizer
    equalizer :: (a -> c) -> (a -> c) -> p a
    pullback  :: (a -> c) -> (b -> c) -> p (a,b)
    pullback a -> c
f b -> c
g = ((a, b) -> c) -> ((a, b) -> c) -> p (a, b)
forall a. (a -> c) -> (a -> c) -> p a
forall (p :: * -> *) c a.
HasEqualizers p c =>
(a -> c) -> (a -> c) -> p a
equalizer (a -> c
f (a -> c) -> ((a, b) -> a) -> (a, b) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst) (b -> c
g (b -> c) -> ((a, b) -> b) -> (a, b) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> b
forall a b. (a, b) -> b
snd)

 class (Functor p) => Topology p where
    arbitraryUnion  :: [p a] -> p a
    finiteIntersect :: [p a] -> p a

 class HasTerminalObject t where
    terminalArrow :: a -> t

 class (CoFunctor p) => HasVariables p t where
    variable :: String -> p t

 class (CoFunctor p) => PropositionalLogic p where
    (-&-) :: p a -> p a -> p a
    (-|-) :: p a -> p a -> p a
    invert  :: p a -> p a

 -- | <https://en.wikipedia.org/wiki/Modal_logic>

 class (PropositionalLogic p) => ModalLogic p where
    eventually :: p a -> p a
    always     :: p a -> p a
    always     = p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert (p a -> p a) -> (p a -> p a) -> p a -> p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. ModalLogic p => p a -> p a
eventually (p a -> p a) -> (p a -> p a) -> p a -> p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert
    eventually = p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert (p a -> p a) -> (p a -> p a) -> p a -> p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. ModalLogic p => p a -> p a
always     (p a -> p a) -> (p a -> p a) -> p a -> p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert

 class (CoFunctor p) => Continuous p where
    expand :: p (Either a b) -> (p a, p b)

 class (CoFunctor p) => SubtractiveLogic p where
    (-\-) :: p a -> p a -> p a

 class (CoFunctor p) => ImplicativeLogic p where
    (-=>-) :: p a -> p a -> p a

 class (CoFunctor p) => BooleanLogic p where
    true   :: p a

 class (CoFunctor p) => UniversalLogic p where
    singleton   :: (Eq a) => a -> p a
    allMembers :: (Universe a) => p a

 class (CoFunctor p) => Universal p where
    exist :: (Universe b) => p (a,b) -> p a
    univ  :: (Universe b) => p (a,b) -> p a

 member :: (Propositional p) => a -> p a -> p ()
 member :: forall (p :: * -> *) a. Propositional p => a -> p a -> p ()
member a
x p a
p = p a -> a -> p ()
forall a. p a -> a -> p ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
runProposition p a
p a
x

 isIn :: (BinaryLogic p) => a -> p a -> Bool
 isIn :: forall (p :: * -> *) a. BinaryLogic p => a -> p a -> Bool
isIn a
x p a
p = p () -> Bool
forall (p :: * -> *). BinaryLogic p => p () -> Bool
toBool (p () -> Bool) -> p () -> Bool
forall a b. (a -> b) -> a -> b
$ a
x a -> p a -> p ()
forall (p :: * -> *) a. Propositional p => a -> p a -> p ()
`member` p a
p

 isNotIn :: (BinaryLogic p) => a -> p a -> Bool
 isNotIn :: forall (p :: * -> *) a. BinaryLogic p => a -> p a -> Bool
isNotIn a
x p a
p = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
x a -> p a -> Bool
forall (p :: * -> *) a. BinaryLogic p => a -> p a -> Bool
`isIn` p a
p

 terminalPart :: (Propositional p) => p () -> p ()
 terminalPart :: forall (p :: * -> *). Propositional p => p () -> p ()
terminalPart p ()
p = p () -> () -> p ()
forall a. p a -> a -> p ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
runProposition p ()
p ()

 propositionalImplication :: (PropositionalLogic p) => p a -> p a -> p a
 propositionalImplication :: forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
propositionalImplication p a
f p a
g = (p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert p a
f) p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
-|- p a
g

 relativeComplement :: (PropositionalLogic p) => p a -> p a -> p a
 relativeComplement :: forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
relativeComplement p a
f p a
g = p a
f p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
-&- p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert p a
g

 intersectList :: (BooleanLogic p, PropositionalLogic p) => [p a] -> p a
 intersectList :: forall (p :: * -> *) a.
(BooleanLogic p, PropositionalLogic p) =>
[p a] -> p a
intersectList = (p a -> p a -> p a) -> p a -> [p a] -> p a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
(-&-) p a
forall a. p a
forall (p :: * -> *) a. BooleanLogic p => p a
true

 unionList :: (BooleanLogic p, PropositionalLogic p) => [p a] -> p a
 unionList :: forall (p :: * -> *) a.
(BooleanLogic p, PropositionalLogic p) =>
[p a] -> p a
unionList = (p a -> p a -> p a) -> p a -> [p a] -> p a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
(-|-) p a
forall (p :: * -> *) a.
(BooleanLogic p, PropositionalLogic p) =>
p a
falseProp

 characteristic :: (BooleanLogic p) => (a -> p ()) -> p a
 characteristic :: forall (p :: * -> *) a. BooleanLogic p => (a -> p ()) -> p a
characteristic a -> p ()
f = (a -> p ()) -> p (p ()) -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage a -> p ()
f p (p ())
forall a. p a
forall (p :: * -> *) a. BooleanLogic p => p a
true

  -- false :: (BooleanLogic p) => p (p ())
  -- false = characteristic not

 falseProp :: (BooleanLogic p, PropositionalLogic p) => p a
 falseProp :: forall (p :: * -> *) a.
(BooleanLogic p, PropositionalLogic p) =>
p a
falseProp = p a -> p a
forall a. p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a
invert p a
forall a. p a
forall (p :: * -> *) a. BooleanLogic p => p a
true

 (-<=>-) :: (ImplicativeLogic p, PropositionalLogic p) => p a -> p a -> p a
 p a
p -<=>- :: forall (p :: * -> *) a.
(ImplicativeLogic p, PropositionalLogic p) =>
p a -> p a -> p a
-<=>- p a
q = (p a
p p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. ImplicativeLogic p => p a -> p a -> p a
-=>- p a
q) p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
-&- (p a
q p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. ImplicativeLogic p => p a -> p a -> p a
-=>- p a
p)

 symmetricDifference :: (PropositionalLogic p, SubtractiveLogic p) => p a -> p a -> p a
 symmetricDifference :: forall (p :: * -> *) a.
(PropositionalLogic p, SubtractiveLogic p) =>
p a -> p a -> p a
symmetricDifference p a
x p a
y = (p a
x p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. SubtractiveLogic p => p a -> p a -> p a
-\- p a
y) p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
-|- (p a
y p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. SubtractiveLogic p => p a -> p a -> p a
-\- p a
x)

  -- The boundary is not useful in propositional logic, this produces a
  -- proposition that is always false. true -\- p == invert p,
  -- so boundary p == p -&- invert p == false

 boundary :: (PropositionalLogic p, BooleanLogic p, SubtractiveLogic p)
             => p a -> p a
 boundary :: forall (p :: * -> *) a.
(PropositionalLogic p, BooleanLogic p, SubtractiveLogic p) =>
p a -> p a
boundary p a
p = p a
p p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. PropositionalLogic p => p a -> p a -> p a
-&- (p a
forall a. p a
forall (p :: * -> *) a. BooleanLogic p => p a
true p a -> p a -> p a
forall a. p a -> p a -> p a
forall (p :: * -> *) a. SubtractiveLogic p => p a -> p a -> p a
-\- p a
p)

 currySubst :: (CoFunctor p) => ((a,b) -> c) -> p (b -> c) -> p a
 currySubst :: forall (p :: * -> *) a b c.
CoFunctor p =>
((a, b) -> c) -> p (b -> c) -> p a
currySubst = (a -> b -> c) -> p (b -> c) -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage ((a -> b -> c) -> p (b -> c) -> p a)
-> (((a, b) -> c) -> a -> b -> c)
-> ((a, b) -> c)
-> p (b -> c)
-> p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> c) -> a -> b -> c
forall a b c. ((a, b) -> c) -> a -> b -> c
curry

 uncurrySubst :: (CoFunctor p) => (a -> b -> c) -> p c -> p (a,b)
 uncurrySubst :: forall (p :: * -> *) a b c.
CoFunctor p =>
(a -> b -> c) -> p c -> p (a, b)
uncurrySubst = ((a, b) -> c) -> p c -> p (a, b)
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (((a, b) -> c) -> p c -> p (a, b))
-> ((a -> b -> c) -> (a, b) -> c)
-> (a -> b -> c)
-> p c
-> p (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry

 dualize :: (Difference p minus) => (a -> b) -> p (a `minus` b)
 dualize :: forall (p :: * -> *) (minus :: * -> * -> *) a b.
Difference p minus =>
(a -> b) -> p (minus a b)
dualize = (p b -> p a) -> p (minus a b)
forall a b. (p a -> p b) -> p (minus b a)
forall (p :: * -> *) (minus :: * -> * -> *) a b.
Difference p minus =>
(p a -> p b) -> p (minus b a)
difference ((p b -> p a) -> p (minus a b))
-> ((a -> b) -> p b -> p a) -> (a -> b) -> p (minus a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> p b -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage

 coin1 :: (CoFunctor p) => p a -> p (a,b)
 coin1 :: forall (p :: * -> *) a b. CoFunctor p => p a -> p (a, b)
coin1 = ((a, b) -> a) -> p a -> p (a, b)
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (a, b) -> a
forall a b. (a, b) -> a
fst

 coin2 :: (CoFunctor p) => p b -> p (a,b)
 coin2 :: forall (p :: * -> *) b a. CoFunctor p => p b -> p (a, b)
coin2 = ((a, b) -> b) -> p b -> p (a, b)
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (a, b) -> b
forall a b. (a, b) -> b
snd

 cofst :: (CoFunctor p) => p (Either a b) -> p a
 cofst :: forall (p :: * -> *) a b. CoFunctor p => p (Either a b) -> p a
cofst = (a -> Either a b) -> p (Either a b) -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage a -> Either a b
forall a b. a -> Either a b
Left

 cosnd :: (CoFunctor p) => p (Either a b) -> p b
 cosnd :: forall (p :: * -> *) a b. CoFunctor p => p (Either a b) -> p b
cosnd = (b -> Either a b) -> p (Either a b) -> p b
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage b -> Either a b
forall a b. b -> Either a b
Right

 cocase :: (CoFunctor p) => (Either a b -> c) -> p c -> (p a, p b)
 cocase :: forall (p :: * -> *) a b c.
CoFunctor p =>
(Either a b -> c) -> p c -> (p a, p b)
cocase Either a b -> c
f p c
x = ((a -> c) -> p c -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (Either a b -> c
f (Either a b -> c) -> (a -> Either a b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a b
forall a b. a -> Either a b
Left) p c
x, (b -> c) -> p c -> p b
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (Either a b -> c
f (Either a b -> c) -> (b -> Either a b) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either a b
forall a b. b -> Either a b
Right) p c
x)

 copair :: (Propositional p, BooleanLogic p) => p a -> p b -> p (Either a b)
 copair :: forall (p :: * -> *) a b.
(Propositional p, BooleanLogic p) =>
p a -> p b -> p (Either a b)
copair p a
f p b
g = (Either a b -> p ()) -> p (Either a b)
forall (p :: * -> *) a. BooleanLogic p => (a -> p ()) -> p a
characteristic ((Either a b -> p ()) -> p (Either a b))
-> (Either a b -> p ()) -> p (Either a b)
forall a b. (a -> b) -> a -> b
$ (a -> p ()) -> (b -> p ()) -> Either a b -> p ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (p a -> a -> p ()
forall a. p a -> a -> p ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
runProposition p a
f) (p b -> b -> p ()
forall a. p a -> a -> p ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
runProposition p b
g)

 pairSubst :: (CoFunctor p) => (a -> b) -> (a -> c) -> p (b,c) -> p a
 pairSubst :: forall (p :: * -> *) a b c.
CoFunctor p =>
(a -> b) -> (a -> c) -> p (b, c) -> p a
pairSubst a -> b
f a -> c
g = (a -> (b, c)) -> p (b, c) -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (\a
x -> (a -> b
f a
x,a -> c
g a
x))

 graphSubst :: (CoFunctor p) => (a -> b) -> p (a,b) -> p a
 graphSubst :: forall (p :: * -> *) a b.
CoFunctor p =>
(a -> b) -> p (a, b) -> p a
graphSubst a -> b
f = (a -> (a, b)) -> p (a, b) -> p a
forall (p :: * -> *) a b. CoFunctor p => (a -> b) -> p b -> p a
inverseImage (\a
x -> (a
x,a -> b
f a
x))

 instance HasTerminalObject () where
    terminalArrow :: forall a. a -> ()
terminalArrow a
_ = ()

 instance Representable IO where
    type Representation IO = I
    represent :: forall a. Representation IO a -> IO a
represent = a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> IO a) -> (I a -> a) -> I a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I a -> a
forall a. I a -> a
unI
    IO a
m !> :: forall a. IO a -> (Representation IO a -> IO a) -> IO a
!> Representation IO a -> IO a
f = IO a
m IO a -> (a -> IO a) -> IO a
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (I a -> IO a
Representation IO a -> IO a
f (I a -> IO a) -> (a -> I a) -> a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> I a
forall a. a -> I a
I)
 
 instance Representable [] where
    type Representation [] = I
    represent :: forall a. Representation [] a -> [a]
represent = a -> [a]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> [a]) -> (I a -> a) -> I a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I a -> a
forall a. I a -> a
unI
    [a]
m !> :: forall a. [a] -> (Representation [] a -> [a]) -> [a]
!> Representation [] a -> [a]
f = [a]
m [a] -> (a -> [a]) -> [a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (I a -> [a]
Representation [] a -> [a]
f (I a -> [a]) -> (a -> I a) -> a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> I a
forall a. a -> I a
I)

 data Assertion a = PrimAssert { forall a. Assertion a -> a -> Bool
assertedCondition :: a -> Bool }
                  | NotAssert { forall a. Assertion a -> Assertion a
assertedNegations :: Assertion a }
                  | AndAssert { forall a. Assertion a -> [Assertion a]
assertedConjunctions :: [Assertion a] }
                  | OrAssert { forall a. Assertion a -> [Assertion a]
assertedDisjunctions :: [Assertion a] }
  
 instance ImplicativeLogic Assertion where
    Assertion a
f -=>- :: forall a. Assertion a -> Assertion a -> Assertion a
-=>- Assertion a
g = [Assertion a] -> Assertion a
forall a. [Assertion a] -> Assertion a
OrAssert [Assertion a -> Assertion a
forall a. Assertion a -> Assertion a
NotAssert Assertion a
f, Assertion a
g]

 instance Contravariant Assertion where
   contramap :: forall a' a. (a' -> a) -> Assertion a -> Assertion a'
contramap a' -> a
f (PrimAssert a -> Bool
p) = (a' -> Bool) -> Assertion a'
forall a. (a -> Bool) -> Assertion a
PrimAssert (a -> Bool
p (a -> Bool) -> (a' -> a) -> a' -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> a
f)
   contramap a' -> a
f (NotAssert Assertion a
x) = Assertion a' -> Assertion a'
forall a. Assertion a -> Assertion a
NotAssert ((a' -> a) -> Assertion a -> Assertion a'
forall a' a. (a' -> a) -> Assertion a -> Assertion a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap a' -> a
f Assertion a
x)
   contramap a' -> a
f (AndAssert [Assertion a]
lst) = [Assertion a'] -> Assertion a'
forall a. [Assertion a] -> Assertion a
AndAssert ([Assertion a'] -> Assertion a') -> [Assertion a'] -> Assertion a'
forall a b. (a -> b) -> a -> b
$ (Assertion a -> Assertion a') -> [Assertion a] -> [Assertion a']
forall a b. (a -> b) -> [a] -> [b]
map ((a' -> a) -> Assertion a -> Assertion a'
forall a' a. (a' -> a) -> Assertion a -> Assertion a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap a' -> a
f) [Assertion a]
lst
   contramap a' -> a
f (OrAssert [Assertion a]
lst)  = [Assertion a'] -> Assertion a'
forall a. [Assertion a] -> Assertion a
OrAssert ([Assertion a'] -> Assertion a') -> [Assertion a'] -> Assertion a'
forall a b. (a -> b) -> a -> b
$  (Assertion a -> Assertion a') -> [Assertion a] -> [Assertion a']
forall a b. (a -> b) -> [a] -> [b]
map ((a' -> a) -> Assertion a -> Assertion a'
forall a' a. (a' -> a) -> Assertion a -> Assertion a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap a' -> a
f) [Assertion a]
lst

 instance PropositionalLogic Assertion where
   Assertion a
p1 -&- :: forall a. Assertion a -> Assertion a -> Assertion a
-&- Assertion a
p2 = [Assertion a] -> Assertion a
forall a. [Assertion a] -> Assertion a
AndAssert [Assertion a
p1,Assertion a
p2]
   Assertion a
p1 -|- :: forall a. Assertion a -> Assertion a -> Assertion a
-|- Assertion a
p2 = [Assertion a] -> Assertion a
forall a. [Assertion a] -> Assertion a
OrAssert [Assertion a
p1,Assertion a
p2]
   invert :: forall a. Assertion a -> Assertion a
invert = Assertion a -> Assertion a
forall a. Assertion a -> Assertion a
NotAssert

 instance BooleanLogic Assertion where
    true :: forall a. Assertion a
true = (a -> Bool) -> Assertion a
forall a. (a -> Bool) -> Assertion a
PrimAssert ((a -> Bool) -> Assertion a) -> (a -> Bool) -> Assertion a
forall a b. (a -> b) -> a -> b
$ Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True

 instance Propositional Assertion where
   runProposition :: forall a. Assertion a -> a -> Assertion ()
runProposition (PrimAssert a -> Bool
p) a
x = (() -> Bool) -> Assertion ()
forall a. (a -> Bool) -> Assertion a
PrimAssert ((() -> Bool) -> Assertion ()) -> (() -> Bool) -> Assertion ()
forall a b. (a -> b) -> a -> b
$ Bool -> () -> Bool
forall a b. a -> b -> a
const (a -> Bool
p a
x)
   runProposition (NotAssert Assertion a
p) a
x = Assertion () -> Assertion ()
forall a. Assertion a -> Assertion a
NotAssert (Assertion a -> a -> Assertion ()
forall a. Assertion a -> a -> Assertion ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
runProposition Assertion a
p a
x)
   runProposition (AndAssert [Assertion a]
lst) a
x = [Assertion ()] -> Assertion ()
forall a. [Assertion a] -> Assertion a
AndAssert ([Assertion ()] -> Assertion ()) -> [Assertion ()] -> Assertion ()
forall a b. (a -> b) -> a -> b
$ (Assertion a -> Assertion ()) -> [Assertion a] -> [Assertion ()]
forall a b. (a -> b) -> [a] -> [b]
map (Assertion a -> a -> Assertion ()
forall a. Assertion a -> a -> Assertion ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
`runProposition` a
x) [Assertion a]
lst
   runProposition (OrAssert [Assertion a]
lst) a
x = [Assertion ()] -> Assertion ()
forall a. [Assertion a] -> Assertion a
OrAssert ([Assertion ()] -> Assertion ()) -> [Assertion ()] -> Assertion ()
forall a b. (a -> b) -> a -> b
$ (Assertion a -> Assertion ()) -> [Assertion a] -> [Assertion ()]
forall a b. (a -> b) -> [a] -> [b]
map (Assertion a -> a -> Assertion ()
forall a. Assertion a -> a -> Assertion ()
forall (p :: * -> *) a. Propositional p => p a -> a -> p ()
`runProposition` a
x) [Assertion a]
lst

 instance BinaryLogic Assertion where
   toBool :: Assertion () -> Bool
toBool (PrimAssert () -> Bool
p) = () -> Bool
p ()
   toBool (NotAssert Assertion ()
p) = Bool -> Bool
not (Assertion () -> Bool
forall (p :: * -> *). BinaryLogic p => p () -> Bool
toBool Assertion ()
p)
   toBool (AndAssert [Assertion ()]
lst) = (Assertion () -> Bool) -> [Assertion ()] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Assertion () -> Bool
forall (p :: * -> *). BinaryLogic p => p () -> Bool
toBool [Assertion ()]
lst
   toBool (OrAssert [Assertion ()]
lst) = (Assertion () -> Bool) -> [Assertion ()] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Assertion () -> Bool
forall (p :: * -> *). BinaryLogic p => p () -> Bool
toBool [Assertion ()]
lst