{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module Data.Propagator
( Prop, up, down, lift, over, lift2, unary, binary
, (.&&), all', allWithIndex', and'
, (.||), any', anyWithIndex', or'
, false, not', true, exactly, choose
, (.==), (./=), distinct
, (.>), (.>=), (.<), (.<=)
, (.+), (.-), negate'
, (.*.), (./.), (.%.)
, (.*), (./), recip'
, abs'
, (.$)
, zipWith'
, (.>>=)
) where
import Control.Monad.Cell.Class (MonadCell (..))
import qualified Control.Monad.Cell.Class as Cell
import Data.JoinSemilattice.Class.Abs (AbsR (..))
import Data.JoinSemilattice.Class.Boolean (BooleanR (..))
import Data.JoinSemilattice.Class.Eq (EqR (..), neR)
import Data.JoinSemilattice.Class.FlatMapping (FlatMapping (..))
import Data.JoinSemilattice.Class.Fractional (FractionalR (..), divideR, multiplyR, recipR)
import Data.JoinSemilattice.Class.Integral (IntegralR (..), divR, modR, timesR)
import Data.JoinSemilattice.Class.Lifting (Lifting (..))
import Data.JoinSemilattice.Class.Mapping (Mapping (..))
import Data.JoinSemilattice.Class.Merge (Merge)
import Data.JoinSemilattice.Class.Ord (OrdR (..), gtR, gteR, ltR)
import Data.JoinSemilattice.Class.Sum (SumR (..), negateR, subR)
import Data.JoinSemilattice.Class.Zipping (Zipping (..))
import Data.Kind (Type)
data Prop (m :: Type -> Type) (content :: Type) where
Nullary
:: m (Cell m x)
-> Prop m x
Unary
:: Merge x
=> (forall f. MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x
-> Prop m y
Binary
:: ( Merge x
, Merge y
)
=> (forall f. MonadCell f => Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x
-> Prop m y
-> Prop m z
instance (AbsR x, SumR x, Num x, MonadCell m)
=> Num (Prop m x) where
+ :: Prop m x -> Prop m x -> Prop m x
(+) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. SumR x => (x, x, x) -> (x, x, x)
addR)
(-) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. SumR x => (x, x, x) -> (x, x, x)
subR)
abs :: Prop m x -> Prop m x
abs = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, x) -> (x, x)) -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, x) -> (x, x)
forall x. AbsR x => (x, x) -> (x, x)
absR)
negate :: Prop m x -> Prop m x
negate = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, x) -> (x, x)) -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, x) -> (x, x)
forall x. (Num x, SumR x) => (x, x) -> (x, x)
negateR)
* :: Prop m x -> Prop m x -> Prop m x
(*) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary \Cell f x
these Cell f x
those Cell f x
total ->
Cell f x -> (x -> f ()) -> f ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
Cell.watch Cell f x
these \x
this -> Cell f x -> (x -> f ()) -> f ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
Cell.with Cell f x
those \x
that ->
Cell f x -> x -> f ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell f x
total (x
this x -> x -> x
forall a. Num a => a -> a -> a
* x
that)
fromInteger :: Integer -> Prop m x
fromInteger = m (Cell m x) -> Prop m x
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (m (Cell m x) -> Prop m x)
-> (Integer -> m (Cell m x)) -> Integer -> Prop m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> m (Cell m x)
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
Cell.fill (x -> m (Cell m x)) -> (Integer -> x) -> Integer -> m (Cell m x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> x
forall a. Num a => Integer -> a
Prelude.fromInteger
signum :: Prop m x -> Prop m x
signum = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary \Cell f x
these Cell f x
those -> Cell f x -> (x -> f ()) -> f ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
Cell.watch Cell f x
these (Cell f x -> x -> f ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell f x
those (x -> f ()) -> (x -> x) -> x -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> x
forall a. Num a => a -> a
signum)
instance (AbsR x, Fractional x, FractionalR x, Num x, MonadCell m)
=> Fractional (Prop m x) where
/ :: Prop m x -> Prop m x -> Prop m x
(/) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. FractionalR x => (x, x, x) -> (x, x, x)
divideR)
fromRational :: Rational -> Prop m x
fromRational = m (Cell m x) -> Prop m x
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (m (Cell m x) -> Prop m x)
-> (Rational -> m (Cell m x)) -> Rational -> Prop m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> m (Cell m x)
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
Cell.fill (x -> m (Cell m x)) -> (Rational -> x) -> Rational -> m (Cell m x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> x
forall a. Fractional a => Rational -> a
Prelude.fromRational
recip :: Prop m x -> Prop m x
recip = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, x) -> (x, x)) -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, x) -> (x, x)
forall x. (FractionalR x, Num x) => (x, x) -> (x, x)
recipR)
up :: Applicative m => Cell m x -> Prop m x
up :: Cell m x -> Prop m x
up = m (Cell m x) -> Prop m x
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (m (Cell m x) -> Prop m x)
-> (Cell m x -> m (Cell m x)) -> Cell m x -> Prop m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell m x -> m (Cell m x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
down :: (MonadCell m, Monoid x) => Prop m x -> m (Cell m x)
down :: Prop m x -> m (Cell m x)
down = \case
Nullary m (Cell m x)
x -> m (Cell m x)
x
Unary forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ()
f Prop m x
a -> do
Cell m x
x <- Prop m x -> m (Cell m x)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
down Prop m x
a
Cell m x
y <- m (Cell m x)
forall (m :: * -> *) x. (MonadCell m, Monoid x) => m (Cell m x)
Cell.make
Cell m x -> Cell m x -> m ()
forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ()
f Cell m x
x Cell m x
y
Cell m x -> m (Cell m x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cell m x
y
Binary forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f x -> f ()
f Prop m x
a Prop m y
b -> do
Cell m x
x <- Prop m x -> m (Cell m x)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
down Prop m x
a
Cell m y
y <- Prop m y -> m (Cell m y)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
down Prop m y
b
Cell m x
z <- m (Cell m x)
forall (m :: * -> *) x. (MonadCell m, Monoid x) => m (Cell m x)
Cell.make
Cell m x -> Cell m y -> Cell m x -> m ()
forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f x -> f ()
f Cell m x
x Cell m y
y Cell m x
z
Cell m x -> m (Cell m x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cell m x
z
lift :: forall f m c x. (MonadCell m, c x) => Lifting f c => x -> Prop m (f x)
lift :: x -> Prop m (f x)
lift = m (Cell m (f x)) -> Prop m (f x)
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (m (Cell m (f x)) -> Prop m (f x))
-> (x -> m (Cell m (f x))) -> x -> Prop m (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> m (Cell m (f x))
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
fill (f x -> m (Cell m (f x))) -> (x -> f x) -> x -> m (Cell m (f x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> f x
forall (f :: * -> *) (c :: * -> Constraint) x.
(Lifting f c, c x) =>
x -> f x
lift'
over :: (Merge x, Merge y) => (x -> y) -> Prop m x -> Prop m y
over :: (x -> y) -> Prop m x -> Prop m y
over x -> y
f = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary \Cell f x
x Cell f y
y -> Cell f x -> (x -> f ()) -> f ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
Cell.watch Cell f x
x (Cell f y -> y -> f ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell f y
y (y -> f ()) -> (x -> y) -> x -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> y
f)
unary :: (Merge x, Merge y) => ((x, y) -> (x, y)) -> Prop m x -> Prop m y
unary :: ((x, y) -> (x, y)) -> Prop m x -> Prop m y
unary (x, y) -> (x, y)
f = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, y) -> (x, y)) -> Cell f x -> Cell f y -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, y) -> (x, y)
f)
binary :: (Merge x, Merge y, Merge z) => ((x, y, z) -> (x, y, z)) -> Prop m x -> Prop m y -> Prop m z
binary :: ((x, y, z) -> (x, y, z)) -> Prop m x -> Prop m y -> Prop m z
binary (x, y, z) -> (x, y, z)
f = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, y, z) -> (x, y, z))
-> Cell f x -> Cell f y -> Cell f z -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, y, z) -> (x, y, z)
f)
lift2 :: (Merge x, Merge y, Merge z) => (x -> y -> z) -> Prop m x -> Prop m y -> Prop m z
lift2 :: (x -> y -> z) -> Prop m x -> Prop m y -> Prop m z
lift2 x -> y -> z
f = ((x, y, z) -> (x, y, z)) -> Prop m x -> Prop m y -> Prop m z
forall x y z (m :: * -> *).
(Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z)) -> Prop m x -> Prop m y -> Prop m z
binary \(x
x, y
y, z
_) -> (x
forall a. Monoid a => a
mempty, y
forall a. Monoid a => a
mempty, x -> y -> z
f x
x y
y)
(.&&) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
.&& :: Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
(.&&) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f Bool) -> Cell f (f Bool) -> Cell f (f Bool) -> f ())
-> Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool))
-> Cell f (f Bool) -> Cell f (f Bool) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool)
forall (f :: * -> *).
BooleanR f =>
(f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool)
andR)
infixr 3 .&&
all' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
all' :: (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
all' x -> Prop m (f Bool)
f = [Prop m (f Bool)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
[Prop m (f Bool)] -> Prop m (f Bool)
and' ([Prop m (f Bool)] -> Prop m (f Bool))
-> ([x] -> [Prop m (f Bool)]) -> [x] -> Prop m (f Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> Prop m (f Bool)) -> [x] -> [Prop m (f Bool)]
forall a b. (a -> b) -> [a] -> [b]
map x -> Prop m (f Bool)
f
allWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
allWithIndex' :: (Int -> x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
allWithIndex' Int -> x -> Prop m (f Bool)
f = ((Int, x) -> Prop m (f Bool)) -> [(Int, x)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *) x.
(BooleanR f, MonadCell m) =>
(x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
all' ((Int -> x -> Prop m (f Bool)) -> (Int, x) -> Prop m (f Bool)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> x -> Prop m (f Bool)
f) ([(Int, x)] -> Prop m (f Bool))
-> ([x] -> [(Int, x)]) -> [x] -> Prop m (f Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [x] -> [(Int, x)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..]
and' :: (BooleanR f, MonadCell m) => [ Prop m (f Bool) ] -> Prop m (f Bool)
and' :: [Prop m (f Bool)] -> Prop m (f Bool)
and' = (Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool))
-> Prop m (f Bool) -> [Prop m (f Bool)] -> Prop m (f Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
BooleanR f =>
Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
(.&&) Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
Prop m (f Bool)
true
any' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
any' :: (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
any' x -> Prop m (f Bool)
f = [Prop m (f Bool)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
[Prop m (f Bool)] -> Prop m (f Bool)
or' ([Prop m (f Bool)] -> Prop m (f Bool))
-> ([x] -> [Prop m (f Bool)]) -> [x] -> Prop m (f Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> Prop m (f Bool)) -> [x] -> [Prop m (f Bool)]
forall a b. (a -> b) -> [a] -> [b]
map x -> Prop m (f Bool)
f
anyWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [ x ] -> Prop m (f Bool)
anyWithIndex' :: (Int -> x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
anyWithIndex' Int -> x -> Prop m (f Bool)
f = ((Int, x) -> Prop m (f Bool)) -> [(Int, x)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *) x.
(BooleanR f, MonadCell m) =>
(x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
any' ((Int -> x -> Prop m (f Bool)) -> (Int, x) -> Prop m (f Bool)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> x -> Prop m (f Bool)
f) ([(Int, x)] -> Prop m (f Bool))
-> ([x] -> [(Int, x)]) -> [x] -> Prop m (f Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [x] -> [(Int, x)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..]
exactly :: (BooleanR f, MonadCell m) => Int -> (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
exactly :: Int -> (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
exactly Int
n x -> Prop m (f Bool)
f [x]
xs =
let l :: Int
l = [x] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [x]
xs
choices :: [[Bool]]
choices = Int -> Int -> [[Bool]]
choose Int
l Int
n
applyChoice :: [Bool] -> [Prop m (f Bool)]
applyChoice [Bool]
picks = (Bool -> x -> Prop m (f Bool))
-> [Bool] -> [x] -> [Prop m (f Bool)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Bool
pick x
x -> if Bool
pick then x -> Prop m (f Bool)
f x
x else Prop m (f Bool) -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
Prop m (f Bool) -> Prop m (f Bool)
not' (x -> Prop m (f Bool)
f x
x)) [Bool]
picks [x]
xs
in [Prop m (f Bool)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
[Prop m (f Bool)] -> Prop m (f Bool)
or' (([Bool] -> Prop m (f Bool)) -> [[Bool]] -> [Prop m (f Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ([Prop m (f Bool)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
[Prop m (f Bool)] -> Prop m (f Bool)
and'([Prop m (f Bool)] -> Prop m (f Bool))
-> ([Bool] -> [Prop m (f Bool)]) -> [Bool] -> Prop m (f Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Bool] -> [Prop m (f Bool)]
applyChoice) [[Bool]]
choices)
choose :: Int -> Int -> [[Bool]]
choose :: Int -> Int -> [[Bool]]
choose Int
n Int
k =
if Int
kInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
0 Bool -> Bool -> Bool
|| Int
kInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
n
then []
else
if Int
nInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0
then [[]]
else
([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
FalseBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) (Int -> Int -> [[Bool]]
choose (Int -> Int
forall a. Enum a => a -> a
pred Int
n) Int
k) [[Bool]] -> [[Bool]] -> [[Bool]]
forall a. [a] -> [a] -> [a]
++
([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
TrueBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) (Int -> Int -> [[Bool]]
choose (Int -> Int
forall a. Enum a => a -> a
pred Int
n) (Int -> Int
forall a. Enum a => a -> a
pred Int
k))
false :: (BooleanR f, MonadCell m) => Prop m (f Bool)
false :: Prop m (f Bool)
false = m (Cell m (f Bool)) -> Prop m (f Bool)
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (f Bool -> m (Cell m (f Bool))
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
Cell.fill f Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR)
not' :: (BooleanR f, MonadCell m) => Prop m (f Bool) -> Prop m (f Bool)
not' :: Prop m (f Bool) -> Prop m (f Bool)
not' = (forall (f :: * -> *).
MonadCell f =>
Cell f (f Bool) -> Cell f (f Bool) -> f ())
-> Prop m (f Bool) -> Prop m (f Bool)
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((f Bool, f Bool) -> (f Bool, f Bool))
-> Cell f (f Bool) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (f Bool, f Bool) -> (f Bool, f Bool)
forall (f :: * -> *).
BooleanR f =>
(f Bool, f Bool) -> (f Bool, f Bool)
notR)
or' :: (BooleanR f, MonadCell m) => [ Prop m (f Bool) ] -> Prop m (f Bool)
or' :: [Prop m (f Bool)] -> Prop m (f Bool)
or' = (Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool))
-> Prop m (f Bool) -> [Prop m (f Bool)] -> Prop m (f Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
BooleanR f =>
Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
(.||) Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
(BooleanR f, MonadCell m) =>
Prop m (f Bool)
false
true :: (BooleanR f, MonadCell m) => Prop m (f Bool)
true :: Prop m (f Bool)
true = m (Cell m (f Bool)) -> Prop m (f Bool)
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (f Bool -> m (Cell m (f Bool))
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
Cell.fill f Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR)
(.||) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
.|| :: Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
(.||) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f Bool) -> Cell f (f Bool) -> Cell f (f Bool) -> f ())
-> Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool))
-> Cell f (f Bool) -> Cell f (f Bool) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool)
forall (f :: * -> *).
BooleanR f =>
(f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool)
orR)
infixr 2 .||
(.==) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
.== :: Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
(.==) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ())
-> Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f x, f Bool) -> (f x, f x, f Bool))
-> Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(EqR f, EqC' f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
eqR)
infix 4 .==
(./=) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
./= :: Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
(./=) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ())
-> Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f x, f Bool) -> (f x, f x, f Bool))
-> Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(EqR f, EqC' f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
neR)
infix 4 ./=
distinct :: (EqR f, EqC f x, MonadCell m) => [ Prop m (f x) ] -> Prop m (f Bool)
distinct :: [Prop m (f x)] -> Prop m (f Bool)
distinct = \case
Prop m (f x)
x : [Prop m (f x)]
xs -> (Prop m (f x) -> Prop m (f Bool))
-> [Prop m (f x)] -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *) x.
(BooleanR f, MonadCell m) =>
(x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
all' (Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall (f :: * -> *) x (m :: * -> *).
(EqR f, EqC f x, MonadCell m) =>
Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
./= Prop m (f x)
x) [Prop m (f x)]
xs Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
forall (f :: * -> *) (m :: * -> *).
BooleanR f =>
Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
.&& [Prop m (f x)] -> Prop m (f Bool)
forall (f :: * -> *) x (m :: * -> *).
(EqR f, EqC f x, MonadCell m) =>
[Prop m (f x)] -> Prop m (f Bool)
distinct [Prop m (f x)]
xs
[ ] -> m (Cell m (f Bool)) -> Prop m (f Bool)
forall (m :: * -> *) x. m (Cell m x) -> Prop m x
Nullary (f Bool -> m (Cell m (f Bool))
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
Cell.fill f Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR)
(.>) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
.> :: Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
(.>) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ())
-> Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f x, f Bool) -> (f x, f x, f Bool))
-> Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
gtR)
infix 4 .>
(.>=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
.>= :: Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
(.>=) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ())
-> Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f x, f Bool) -> (f x, f x, f Bool))
-> Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
gteR)
infix 4 .>=
(.<) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
.< :: Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
(.<) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ())
-> Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f x, f Bool) -> (f x, f x, f Bool))
-> Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
ltR)
infix 4 .<
(.<=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
.<= :: Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
(.<=) = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ())
-> Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f x, f Bool) -> (f x, f x, f Bool))
-> Cell f (f x) -> Cell f (f x) -> Cell f (f Bool) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
lteR)
infix 4 .<=
(.+) :: (SumR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
.+ :: Prop m x -> Prop m x -> Prop m x
(.+) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. SumR x => (x, x, x) -> (x, x, x)
addR)
infixl 6 .+
negate' :: (Num x, SumR x, MonadCell m) => Prop m x -> Prop m x
negate' :: Prop m x -> Prop m x
negate' = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, x) -> (x, x)) -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, x) -> (x, x)
forall x. (Num x, SumR x) => (x, x) -> (x, x)
negateR)
(.-) :: (SumR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
.- :: Prop m x -> Prop m x -> Prop m x
(.-) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. SumR x => (x, x, x) -> (x, x, x)
subR)
infixl 6 .-
(.*.) :: (Num x, IntegralR x) => Prop m x -> Prop m x -> Prop m x
.*. :: Prop m x -> Prop m x -> Prop m x
(.*.) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. (IntegralR x, Num x) => (x, x, x) -> (x, x, x)
timesR)
infixl 7 .*.
(./.) :: (IntegralR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
./. :: Prop m x -> Prop m x -> Prop m x
(./.) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. IntegralR x => (x, x, x) -> (x, x, x)
divR)
infixl 7 ./.
(.%.) :: (IntegralR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
.%. :: Prop m x -> Prop m x -> Prop m x
(.%.) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. IntegralR x => (x, x, x) -> (x, x, x)
modR)
infixl 7 .%.
(.*) :: (FractionalR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
.* :: Prop m x -> Prop m x -> Prop m x
(.*) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. FractionalR x => (x, x, x) -> (x, x, x)
multiplyR)
infixl 7 .*
(./) :: (FractionalR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
./ :: Prop m x -> Prop m x -> Prop m x
(./) = (forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x -> Prop m x
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((x, x, x) -> (x, x, x))
-> Cell f x -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary (x, x, x) -> (x, x, x)
forall x. FractionalR x => (x, x, x) -> (x, x, x)
divideR)
infixl 7 ./
recip' :: (Num x, FractionalR x, MonadCell m) => Prop m x -> Prop m x
recip' :: Prop m x -> Prop m x
recip' = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, x) -> (x, x)) -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, x) -> (x, x)
forall x. (FractionalR x, Num x) => (x, x) -> (x, x)
recipR)
abs' :: (AbsR x, MonadCell m) => Prop m x -> Prop m x
abs' :: Prop m x -> Prop m x
abs' = (forall (f :: * -> *). MonadCell f => Cell f x -> Cell f x -> f ())
-> Prop m x -> Prop m x
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((x, x) -> (x, x)) -> Cell f x -> Cell f x -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary (x, x) -> (x, x)
forall x. AbsR x => (x, x) -> (x, x)
absR)
(.$) :: (Mapping f c, c x, c y) => (x -> y) -> Prop m (f x) -> Prop m (f y)
.$ :: (x -> y) -> Prop m (f x) -> Prop m (f y)
(.$) x -> y
f = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f y) -> f ())
-> Prop m (f x) -> Prop m (f y)
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((f x, f y) -> (f x, f y)) -> Cell f (f x) -> Cell f (f y) -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary ((Maybe (x -> y), Maybe (y -> x)) -> (f x, f y) -> (f x, f y)
forall (f :: * -> *) (c :: * -> Constraint) x y.
(Mapping f c, c x, c y) =>
(Maybe (x -> y), Maybe (y -> x)) -> (f x, f y) -> (f x, f y)
mapR ((x -> y) -> Maybe (x -> y)
forall a. a -> Maybe a
Just x -> y
f, Maybe (y -> x)
forall a. Maybe a
Nothing)))
zipWith' :: (Zipping f c, c x, c y, c z) => (x -> y -> z) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
zipWith' :: (x -> y -> z) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
zipWith' x -> y -> z
f = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f y) -> Cell f (f z) -> f ())
-> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
forall x y z (m :: * -> *).
(Merge x, Merge y) =>
(forall (f :: * -> *).
MonadCell f =>
Cell f x -> Cell f y -> Cell f z -> f ())
-> Prop m x -> Prop m y -> Prop m z
Binary (((f x, f y, f z) -> (f x, f y, f z))
-> Cell f (f x) -> Cell f (f y) -> Cell f (f z) -> f ()
forall (m :: * -> *) x y z.
(MonadCell m, Merge x, Merge y, Merge z) =>
((x, y, z) -> (x, y, z))
-> Cell m x -> Cell m y -> Cell m z -> m ()
Cell.binary ((Maybe ((x, y) -> z), Maybe ((x, z) -> y), Maybe ((y, z) -> x))
-> (f x, f y, f z) -> (f x, f y, f z)
forall (f :: * -> *) (c :: * -> Constraint) x y z.
(Zipping f c, c x, c y, c z) =>
(Maybe ((x, y) -> z), Maybe ((x, z) -> y), Maybe ((y, z) -> x))
-> (f x, f y, f z) -> (f x, f y, f z)
zipWithR (((x, y) -> z) -> Maybe ((x, y) -> z)
forall a. a -> Maybe a
Just ((x -> y -> z) -> (x, y) -> z
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry x -> y -> z
f), Maybe ((x, z) -> y)
forall a. Maybe a
Nothing, Maybe ((y, z) -> x)
forall a. Maybe a
Nothing)))
(.>>=) :: (FlatMapping f c, c x, c y) => Prop m (f x) -> (x -> f y) -> Prop m (f y)
.>>= :: Prop m (f x) -> (x -> f y) -> Prop m (f y)
(.>>=) Prop m (f x)
xs x -> f y
f = (forall (f :: * -> *).
MonadCell f =>
Cell f (f x) -> Cell f (f y) -> f ())
-> Prop m (f x) -> Prop m (f y)
forall x y (m :: * -> *).
Merge x =>
(forall (f :: * -> *). MonadCell f => Cell f x -> Cell f y -> f ())
-> Prop m x -> Prop m y
Unary (((f x, f y) -> (f x, f y)) -> Cell f (f x) -> Cell f (f y) -> f ()
forall (m :: * -> *) x y.
(MonadCell m, Merge x, Merge y) =>
((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()
Cell.unary ((Maybe (x -> f y), Maybe (f y -> x)) -> (f x, f y) -> (f x, f y)
forall (f :: * -> *) (c :: * -> Constraint) x y.
(FlatMapping f c, c x, c y) =>
(Maybe (x -> f y), Maybe (f y -> x)) -> (f x, f y) -> (f x, f y)
flatMapR ((x -> f y) -> Maybe (x -> f y)
forall a. a -> Maybe a
Just x -> f y
f, Maybe (f y -> x)
forall a. Maybe a
Nothing))) Prop m (f x)
xs