-- |
-- A vague analog of free monads for invariant monoidals.
-- This can provide a simple basis for things like invertible parsers.
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs, RankNTypes, TupleSections, TypeOperators, QuasiQuotes #-}
#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
{-# LANGUAGE Safe #-}
#endif
module Control.Invertible.Monoidal.Free
  ( Free(..)
  , showsFree
  , mapFree
  , foldFree
  , produceFree
  , runFree
  , parseFree
  , reverseFree
  , freeTNF
  , freeTDNF
  , sortFreeTDNF
  ) where

import Control.Applicative (Alternative(..))
import Control.Arrow ((***), first, second, (+++), left, right)
import Control.Monad (MonadPlus(..))
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State (StateT(..))
import Data.Functor.Classes (Show1, showsPrec1)
import Data.Monoid ((<>), Alt(..))
import Data.Void (Void, absurd)

import Control.Invertible.Monoidal
import qualified Data.Invertible as I

-- |Produce a 'MonoidalAlt' out of any type constructor, simply by converting each monoidal operation into a constructor.
-- Although a version more analogous to a free monad could be defined for instances of 'I.Functor' and restricted to 'Monoidal', including the Yoneda transform makes this the more general case.
data Free f a where
  Void :: Free f Void
  Empty :: Free f ()
  Free :: !(f a) -> Free f a
  Join :: Free f a -> Free f b -> Free f (a, b)
  Choose :: Free f a -> Free f b -> Free f (Either a b)
  Transform :: (a I.<-> b) -> Free f a -> Free f b

instance I.Functor (Free f) where
  fmap :: forall a b. (a <-> b) -> Free f a -> Free f b
fmap a <-> b
f (Transform a <-> a
g Free f a
p) = (a <-> b) -> Free f a -> Free f b
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform (a <-> b
f (a <-> b) -> (a <-> a) -> a <-> b
forall b c a. (b <-> c) -> (a <-> b) -> a <-> c
I.. a <-> a
g) Free f a
p
  fmap a <-> b
f Free f a
p = (a <-> b) -> Free f a -> Free f b
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform a <-> b
f Free f a
p

instance Monoidal (Free f) where
  unit :: Free f ()
unit = Free f ()
forall (f :: * -> *). Free f ()
Empty
  >*< :: forall a b. Free f a -> Free f b -> Free f (a, b)
(>*<) = Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join

instance MonoidalAlt (Free f) where
  zero :: Free f Void
zero = Free f Void
forall (f :: * -> *). Free f Void
Void
  >|< :: forall a b. Free f a -> Free f b -> Free f (Either a b)
(>|<) = Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
Choose

-- |Construct a string representation of a 'Free' structure, given a way to show any @f a@.
showsPrecFree :: (forall a' . f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree :: forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree forall a'. f a' -> ShowS
_ Int
_ Free f a
Void = String -> ShowS
showString String
"Void"
showsPrecFree forall a'. f a' -> ShowS
_ Int
_ Free f a
Empty = String -> ShowS
showString String
"Empty"
showsPrecFree forall a'. f a' -> ShowS
fs Int
d (Free f a
f) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
  (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Free "
  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> ShowS
forall a'. f a' -> ShowS
fs f a
f
showsPrecFree forall a'. f a' -> ShowS
fs Int
d (Join Free f a
p Free f b
q) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
  (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Join "
  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree f a' -> ShowS
forall a'. f a' -> ShowS
fs Int
11 Free f a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> ShowS) -> Int -> Free f b -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree f a' -> ShowS
forall a'. f a' -> ShowS
fs Int
11 Free f b
q
showsPrecFree forall a'. f a' -> ShowS
fs Int
d (Choose Free f a
p Free f b
q) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
  (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Choose "
  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree f a' -> ShowS
forall a'. f a' -> ShowS
fs Int
11 Free f a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> ShowS) -> Int -> Free f b -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree f a' -> ShowS
forall a'. f a' -> ShowS
fs Int
11 Free f b
q
showsPrecFree forall a'. f a' -> ShowS
fs Int
d (Transform a <-> a
_ Free f a
p) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
  (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Transform <bijection> "
  ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree f a' -> ShowS
forall a'. f a' -> ShowS
fs Int
11 Free f a
p

-- |Construct a string representation of a 'Free' structure, given a way to show any @f a@.
showsFree :: (forall a' . f a' -> ShowS) -> Free f a -> ShowS
showsFree :: forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Free f a -> ShowS
showsFree forall a'. f a' -> ShowS
fs = (forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree f a' -> ShowS
forall a'. f a' -> ShowS
fs Int
0

data Underscore = Underscore
instance Show Underscore where
  show :: Underscore -> String
show Underscore
Underscore = String
"_"

instance (Functor f, Show1 f) => Show (Free f a) where
  showsPrec :: Int -> Free f a -> ShowS
showsPrec = (forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
forall (f :: * -> *) a.
(forall a'. f a' -> ShowS) -> Int -> Free f a -> ShowS
showsPrecFree (Int -> f Underscore -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1 Int
11 (f Underscore -> ShowS) -> (f a' -> f Underscore) -> f a' -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Underscore
Underscore Underscore -> f a' -> f Underscore
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$))

-- |Transform the type constructor within a 'Free'.
mapFree :: (forall a' . f a' -> m a') -> Free f a -> Free m a
mapFree :: forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree forall a'. f a' -> m a'
_ Free f a
Void = Free m a
Free m Void
forall (f :: * -> *). Free f Void
Void
mapFree forall a'. f a' -> m a'
_ Free f a
Empty = Free m a
Free m ()
forall (f :: * -> *). Free f ()
Empty
mapFree forall a'. f a' -> m a'
t (Transform a <-> a
f Free f a
p) = (a <-> a) -> Free m a -> Free m a
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform a <-> a
f (Free m a -> Free m a) -> Free m a -> Free m a
forall a b. (a -> b) -> a -> b
$ (forall a'. f a' -> m a') -> Free f a -> Free m a
forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree f a' -> m a'
forall a'. f a' -> m a'
t Free f a
p
mapFree forall a'. f a' -> m a'
t (Join Free f a
p Free f b
q) = Free m a -> Free m b -> Free m (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join ((forall a'. f a' -> m a') -> Free f a -> Free m a
forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree f a' -> m a'
forall a'. f a' -> m a'
t Free f a
p) ((forall a'. f a' -> m a') -> Free f b -> Free m b
forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree f a' -> m a'
forall a'. f a' -> m a'
t Free f b
q)
mapFree forall a'. f a' -> m a'
t (Choose Free f a
p Free f b
q) = Free m a -> Free m b -> Free m (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
Choose ((forall a'. f a' -> m a') -> Free f a -> Free m a
forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree f a' -> m a'
forall a'. f a' -> m a'
t Free f a
p) ((forall a'. f a' -> m a') -> Free f b -> Free m b
forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree f a' -> m a'
forall a'. f a' -> m a'
t Free f b
q)
mapFree forall a'. f a' -> m a'
t (Free f a
x) = m a -> Free m a
forall (f :: * -> *) a. f a -> Free f a
Free (f a -> m a
forall a'. f a' -> m a'
t f a
x)

-- |Given a way to extract a @b@ from any @f a@, use a 'Free' applied to a value to produce a @b@ by converting '>*<' to '<>'.
foldFree :: Monoid b => (forall a' . f a' -> a' -> b) -> Free f a -> a -> b
foldFree :: forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree forall a'. f a' -> a' -> b
_ Free f a
Void a
a = Void -> b
forall a. Void -> a
absurd a
Void
a
foldFree forall a'. f a' -> a' -> b
_ Free f a
Empty () = b
forall a. Monoid a => a
mempty
foldFree forall a'. f a' -> a' -> b
t (Transform a <-> a
f Free f a
p) a
a = (forall a'. f a' -> a' -> b) -> Free f a -> a -> b
forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree f a' -> a' -> b
forall a'. f a' -> a' -> b
t Free f a
p (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ (a <-> a) -> a -> a
forall (a :: * -> * -> *) b c. Bijection a b c -> a c b
I.biFrom a <-> a
f a
a
foldFree forall a'. f a' -> a' -> b
t (Join Free f a
p Free f b
q) (a
a, b
b) = (forall a'. f a' -> a' -> b) -> Free f a -> a -> b
forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree f a' -> a' -> b
forall a'. f a' -> a' -> b
t Free f a
p a
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall a'. f a' -> a' -> b) -> Free f b -> b -> b
forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree f a' -> a' -> b
forall a'. f a' -> a' -> b
t Free f b
q b
b
foldFree forall a'. f a' -> a' -> b
t (Choose Free f a
p Free f b
_) (Left a
a) = (forall a'. f a' -> a' -> b) -> Free f a -> a -> b
forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree f a' -> a' -> b
forall a'. f a' -> a' -> b
t Free f a
p a
a
foldFree forall a'. f a' -> a' -> b
t (Choose Free f a
_ Free f b
p) (Right b
a) = (forall a'. f a' -> a' -> b) -> Free f b -> b -> b
forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree f a' -> a' -> b
forall a'. f a' -> a' -> b
t Free f b
p b
a
foldFree forall a'. f a' -> a' -> b
t (Free f a
x) a
a = f a -> a -> b
forall a'. f a' -> a' -> b
t f a
x a
a

-- |'foldFree' over Alternative rather than Monoid.
produceFree :: Alternative m => (forall a' . f a' -> a' -> b) -> Free f a -> a -> m b
produceFree :: forall (m :: * -> *) (f :: * -> *) b a.
Alternative m =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> m b
produceFree forall a'. f a' -> a' -> b
t Free f a
f = Alt m b -> m b
forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Alt m b -> m b) -> (a -> Alt m b) -> a -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> a' -> Alt m b) -> Free f a -> a -> Alt m b
forall b (f :: * -> *) a.
Monoid b =>
(forall a'. f a' -> a' -> b) -> Free f a -> a -> b
foldFree (\f a'
x a'
a -> m b -> Alt m b
forall {k} (f :: k -> *) (a :: k). f a -> Alt f a
Alt (m b -> Alt m b) -> m b -> Alt m b
forall a b. (a -> b) -> a -> b
$ b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> m b) -> b -> m b
forall a b. (a -> b) -> a -> b
$ f a' -> a' -> b
forall a'. f a' -> a' -> b
t f a'
x a'
a) Free f a
f

-- |Evaluate a 'Free' into an underlying 'Alternative', by evaluating '>|<' with '<|>'.
runFree :: Alternative f => Free f a -> f a
runFree :: forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree Free f a
Void = f a
forall a. f a
forall (f :: * -> *) a. Alternative f => f a
empty
runFree Free f a
Empty = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
runFree (Transform a <-> a
f Free f a
p) = (a <-> a) -> a -> a
forall (a :: * -> * -> *) b c. Bijection a b c -> a b c
I.biTo a <-> a
f (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Free f a -> f a
forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree Free f a
p
runFree (Join Free f a
p Free f b
q) = (,) (a -> b -> a) -> f a -> f (b -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Free f a -> f a
forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree Free f a
p f (b -> a) -> f b -> f a
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Free f b -> f b
forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree Free f b
q
runFree (Choose Free f a
p Free f b
q) = a -> a
a -> Either a b
forall a b. a -> Either a b
Left (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Free f a -> f a
forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree Free f a
p f a -> f a -> f a
forall a. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> b -> a
b -> Either a b
forall a b. b -> Either a b
Right (b -> a) -> f b -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Free f b -> f b
forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree Free f b
q
runFree (Free f a
x) = f a
x

-- |Uncons the current state, returning the head and keeping the tail, or fail if empty.
-- (Parsec's 'Text.Parsec.Prim.Stream' class provides similar but more general functionality.)
unconsState :: Alternative m => StateT [a] m a
unconsState :: forall (m :: * -> *) a. Alternative m => StateT [a] m a
unconsState = ([a] -> m (a, [a])) -> StateT [a] m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT [a] -> m (a, [a])
forall {f :: * -> *} {a}. Alternative f => [a] -> f (a, [a])
ucs where
  ucs :: [a] -> f (a, [a])
ucs (a
a:[a]
l) = (a, [a]) -> f (a, [a])
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, [a]
l)
  ucs [] = f (a, [a])
forall a. f a
forall (f :: * -> *) a. Alternative f => f a
empty

-- |Given a way to convert @b@ elements into any @f a@, use a 'Free' to parse a list of @b@ elements into a value.
-- This just uses 'unconsState' with 'runFree', and is the inverse of 'produceFree', provided the given conversions are themselves inverses.
parseFree :: MonadPlus m => (forall a' . f a' -> b -> m a') -> Free f a -> [b] -> m (a, [b])
parseFree :: forall (m :: * -> *) (f :: * -> *) b a.
MonadPlus m =>
(forall a'. f a' -> b -> m a') -> Free f a -> [b] -> m (a, [b])
parseFree forall a'. f a' -> b -> m a'
t = StateT [b] m a -> [b] -> m (a, [b])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateT [b] m a -> [b] -> m (a, [b]))
-> (Free f a -> StateT [b] m a) -> Free f a -> [b] -> m (a, [b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free (StateT [b] m) a -> StateT [b] m a
forall (f :: * -> *) a. Alternative f => Free f a -> f a
runFree (Free (StateT [b] m) a -> StateT [b] m a)
-> (Free f a -> Free (StateT [b] m) a)
-> Free f a
-> StateT [b] m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a'. f a' -> StateT [b] m a')
-> Free f a -> Free (StateT [b] m) a
forall (f :: * -> *) (m :: * -> *) a.
(forall a'. f a' -> m a') -> Free f a -> Free m a
mapFree (\f a'
x -> m a' -> StateT [b] m a'
forall (m :: * -> *) a. Monad m => m a -> StateT [b] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a' -> StateT [b] m a') -> (b -> m a') -> b -> StateT [b] m a'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a' -> b -> m a'
forall a'. f a' -> b -> m a'
t f a'
x (b -> StateT [b] m a') -> StateT [b] m b -> StateT [b] m a'
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StateT [b] m b
forall (m :: * -> *) a. Alternative m => StateT [a] m a
unconsState)

-- |Flip the effective order of each '>*<' operation in a 'Free', so that processing is done in the reverse order.
-- It probably goes without saying, but applying this to an infinite structure, such as those produced by 'manyI', will not terminate.
reverseFree :: Free f a -> Free f a
reverseFree :: forall (f :: * -> *) a. Free f a -> Free f a
reverseFree (Transform a <-> a
f (Join Free f a
p Free f b
q)) = ((b, a) <-> a) -> Free f (b, a) -> Free f a
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform (a <-> a
f (a <-> a) -> ((b, a) <-> a) -> (b, a) <-> a
forall b c a. (b <-> c) -> (a <-> b) -> a <-> c
I.. (b, a) <-> a
(b, a) <-> (a, b)
forall a b. (a, b) <-> (b, a)
I.swap) (Free f (b, a) -> Free f a) -> Free f (b, a) -> Free f a
forall a b. (a -> b) -> a -> b
$ Free f b -> Free f a -> Free f (b, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f b
q) (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f a
p)
reverseFree (Transform a <-> a
f Free f a
p) = (a <-> a) -> Free f a -> Free f a
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform a <-> a
f (Free f a -> Free f a) -> Free f a -> Free f a
forall a b. (a -> b) -> a -> b
$ Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f a
p
reverseFree (Join Free f a
p Free f b
q) = ((b, a) <-> a) -> Free f (b, a) -> Free f a
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform (b, a) <-> a
(b, a) <-> (a, b)
forall a b. (a, b) <-> (b, a)
I.swap (Free f (b, a) -> Free f a) -> Free f (b, a) -> Free f a
forall a b. (a -> b) -> a -> b
$ Free f b -> Free f a -> Free f (b, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f b
q) (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f a
p)
reverseFree (Choose Free f a
p Free f b
q) = Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
Choose (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f a
p) (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
reverseFree Free f b
q)
reverseFree Free f a
p = Free f a
p

chooseTNF :: Free f a -> Free f b -> Free f (Either a b)
chooseTNF :: forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF (Transform a <-> a
f Free f a
p) (Transform a <-> b
g Free f a
q) = (a <-> a
f (a <-> a) -> (a <-> b) -> Bijection (->) (Either a a) (Either a b)
forall b c b' c'.
Bijection (->) b c
-> Bijection (->) b' c'
-> Bijection (->) (Either b b') (Either c c')
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ a <-> b
g) Bijection (->) (Either a a) (Either a b)
-> Free f (Either a a) -> Free f (Either a b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a -> Free f (Either a a)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF Free f a
p Free f a
q
chooseTNF (Transform a <-> a
f Free f a
p) Free f b
q = (a <-> a) -> Bijection (->) (Either a b) (Either a b)
forall b c d.
Bijection (->) b c -> Bijection (->) (Either b d) (Either c d)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left a <-> a
f Bijection (->) (Either a b) (Either a b)
-> Free f (Either a b) -> Free f (Either a b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF Free f a
p Free f b
q
chooseTNF Free f a
p (Transform a <-> b
g Free f a
q) = (a <-> b) -> Bijection (->) (Either a a) (Either a b)
forall b c d.
Bijection (->) b c -> Bijection (->) (Either d b) (Either d c)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right a <-> b
g Bijection (->) (Either a a) (Either a b)
-> Free f (Either a a) -> Free f (Either a b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a -> Free f (Either a a)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF Free f a
p Free f a
q
chooseTNF Free f a
p Free f b
q = Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
Choose Free f a
p Free f b
q

joinTNF :: Free f a -> Free f b -> Free f (a, b)
joinTNF :: forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTNF (Transform a <-> a
f Free f a
p) (Transform a <-> b
g Free f a
q) = (a <-> a
f (a <-> a) -> (a <-> b) -> Bijection (->) (a, a) (a, b)
forall b c b' c'.
Bijection (->) b c
-> Bijection (->) b' c' -> Bijection (->) (b, b') (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a <-> b
g) Bijection (->) (a, a) (a, b) -> Free f (a, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTNF Free f a
p Free f a
q
joinTNF (Transform a <-> a
f Free f a
p) Free f b
q = (a <-> a) -> Bijection (->) (a, b) (a, b)
forall b c d. Bijection (->) b c -> Bijection (->) (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a <-> a
f Bijection (->) (a, b) (a, b) -> Free f (a, b) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTNF Free f a
p Free f b
q
joinTNF Free f a
p (Transform a <-> b
g Free f a
q) = (a <-> b) -> Bijection (->) (a, a) (a, b)
forall b c d. Bijection (->) b c -> Bijection (->) (d, b) (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second a <-> b
g Bijection (->) (a, a) (a, b) -> Free f (a, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTNF Free f a
p Free f a
q
joinTNF Free f a
p Free f b
q = Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join Free f a
p Free f b
q

-- |Convert a 'Free' to Transform Normal Form: extract and merge all the 'Transform', if any, to a single 'Transform' at the top.
freeTNF :: Free f a -> Free f a
freeTNF :: forall (f :: * -> *) a. Free f a -> Free f a
freeTNF (Transform a <-> a
f Free f a
p) = a <-> a
f (a <-> a) -> Free f a -> Free f a
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
freeTNF Free f a
p
freeTNF (Join Free f a
p Free f b
q) = Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTNF (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
freeTNF Free f a
p) (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
freeTNF Free f b
q)
freeTNF (Choose Free f a
p Free f b
q) = Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
freeTNF Free f a
p) (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
freeTNF Free f b
q)
freeTNF Free f a
p = Free f a
p

joinTDNF :: Free f a -> Free f b -> Free f (a, b)
joinTDNF :: forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF (Transform a <-> a
f Free f a
p) (Transform a <-> b
g Free f a
q) = (a <-> a
f (a <-> a) -> (a <-> b) -> Bijection (->) (a, a) (a, b)
forall b c b' c'.
Bijection (->) b c
-> Bijection (->) b' c' -> Bijection (->) (b, b') (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a <-> b
g) Bijection (->) (a, a) (a, b) -> Free f (a, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
p Free f a
q
joinTDNF (Transform a <-> a
f Free f a
p) Free f b
q = (a <-> a) -> Bijection (->) (a, b) (a, b)
forall b c d. Bijection (->) b c -> Bijection (->) (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a <-> a
f Bijection (->) (a, b) (a, b) -> Free f (a, b) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
p Free f b
q
joinTDNF Free f a
p (Transform a <-> b
g Free f a
q) = (a <-> b) -> Bijection (->) (a, a) (a, b)
forall b c d. Bijection (->) b c -> Bijection (->) (d, b) (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second a <-> b
g Bijection (->) (a, a) (a, b) -> Free f (a, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
p Free f a
q
joinTDNF (Choose Free f a
pp Free f b
pq) Free f b
q = Bijection (->) (Either (a, b) (b, b)) (a, b)
Either (a, b) (b, b) <-> (Either a b, b)
forall a c b. Either (a, c) (b, c) <-> (Either a b, c)
I.eitherFirst Bijection (->) (Either (a, b) (b, b)) (a, b)
-> Free f (Either (a, b) (b, b)) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f (a, b) -> Free f (b, b) -> Free f (Either (a, b) (b, b))
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF (Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
pp Free f b
q) (Free f b -> Free f b -> Free f (b, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f b
pq Free f b
q)
joinTDNF Free f a
p (Choose Free f a
qp Free f b
qq) = Bijection (->) (Either (a, a) (a, b)) (a, b)
Either (a, a) (a, b) <-> (a, Either a b)
forall a b c. Either (a, b) (a, c) <-> (a, Either b c)
I.eitherSecond Bijection (->) (Either (a, a) (a, b)) (a, b)
-> Free f (Either (a, a) (a, b)) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f (a, a) -> Free f (a, b) -> Free f (Either (a, a) (a, b))
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF (Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
p Free f a
qp) (Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
p Free f b
qq)
joinTDNF Free f a
p Free f b
Empty = (a <-> (a, b)) -> Free f a -> Free f (a, b)
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform (Bijection (->) (a, b) a -> a <-> (a, b)
forall b c. Bijection (->) b c -> Bijection (->) c b
forall (a :: * -> * -> *) b c. BiArrow a => a b c -> a c b
I.invert Bijection (->) (a, b) a
(a, ()) <-> a
forall a. (a, ()) <-> a
I.fst) (Free f a -> Free f (a, b)) -> Free f a -> Free f (a, b)
forall a b. (a -> b) -> a -> b
$ Free f a
p
joinTDNF Free f a
Empty Free f b
q = (b <-> (a, b)) -> Free f b -> Free f (a, b)
forall a b (f :: * -> *). (a <-> b) -> Free f a -> Free f b
Transform (Bijection (->) (a, b) b -> b <-> (a, b)
forall b c. Bijection (->) b c -> Bijection (->) c b
forall (a :: * -> * -> *) b c. BiArrow a => a b c -> a c b
I.invert Bijection (->) (a, b) b
((), b) <-> b
forall a. ((), a) <-> a
I.snd) (Free f b -> Free f (a, b)) -> Free f b -> Free f (a, b)
forall a b. (a -> b) -> a -> b
$ Free f b
q
joinTDNF Free f a
p Free f b
q = Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join Free f a
p Free f b
q

-- |Convert a 'Free' to Transform Disjunctive Normal Form: reorder the terms so thet at most one 'Transform' is on the outside, followed by 'Choose' terms, which are above all 'Join' terms', with 'Empty' and 'Free' as leaves.
-- Since each 'Join' above a 'Choose' creates a duplicate 'Join' term, the complexity and result size can be exponential (just as with boolean logic DNF).
freeTDNF :: Free f a -> Free f a
freeTDNF :: forall (f :: * -> *) a. Free f a -> Free f a
freeTDNF (Transform a <-> a
f Free f a
p) = a <-> a
f (a <-> a) -> Free f a -> Free f a
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
freeTDNF Free f a
p
freeTDNF (Join Free f a
p Free f b
q) = Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
freeTDNF Free f a
p) (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
freeTDNF Free f b
q)
freeTDNF (Choose Free f a
p Free f b
q) = Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF (Free f a -> Free f a
forall (f :: * -> *) a. Free f a -> Free f a
freeTDNF Free f a
p) (Free f b -> Free f b
forall (f :: * -> *) a. Free f a -> Free f a
freeTDNF Free f b
q)
freeTDNF Free f a
p = Free f a
p

pivot :: (a,(b,c)) I.<-> ((a,b),c)
pivot :: forall a b c. (a, (b, c)) <-> ((a, b), c)
pivot = [I.biCase|(a,(b,c)) <-> ((a,b),c)|]

swap12 :: (a,(b,c)) I.<-> (b,(a,c))
swap12 :: forall a b c. (a, (b, c)) <-> (b, (a, c))
swap12 = [I.biCase|(a,(b,c)) <-> (b,(a,c))|]

sortJoinTDNF :: (forall a' b' . f a' -> f b' -> Ordering) -> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF :: forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Transform a <-> a
f Free f a
p) (Transform a <-> b
g Free f a
q) = (a <-> a
f (a <-> a) -> (a <-> b) -> Bijection (->) (a, a) (a, b)
forall b c b' c'.
Bijection (->) b c
-> Bijection (->) b' c' -> Bijection (->) (b, b') (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a <-> b
g) Bijection (->) (a, a) (a, b) -> Free f (a, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f a
q
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Transform a <-> a
f Free f a
p) Free f b
q = (a <-> a) -> Bijection (->) (a, b) (a, b)
forall b c d. Bijection (->) b c -> Bijection (->) (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a <-> a
f Bijection (->) (a, b) (a, b) -> Free f (a, b) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f b
q
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p (Transform a <-> b
f Free f a
q) = (a <-> b) -> Bijection (->) (a, a) (a, b)
forall b c d. Bijection (->) b c -> Bijection (->) (d, b) (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second a <-> b
f Bijection (->) (a, a) (a, b) -> Free f (a, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f a
q
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Choose Free f a
pp Free f b
pq) Free f b
q = Bijection (->) (Either (a, b) (b, b)) (a, b)
Either (a, b) (b, b) <-> (Either a b, b)
forall a c b. Either (a, c) (b, c) <-> (Either a b, c)
I.eitherFirst Bijection (->) (Either (a, b) (b, b)) (a, b)
-> Free f (Either (a, b) (b, b)) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f (a, b) -> Free f (b, b) -> Free f (Either (a, b) (b, b))
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF ((forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
pp Free f b
q) ((forall a' b'. f a' -> f b' -> Ordering)
-> Free f b -> Free f b -> Free f (b, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f b
pq Free f b
q)
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p (Choose Free f a
qp Free f b
qq) = Bijection (->) (Either (a, a) (a, b)) (a, b)
Either (a, a) (a, b) <-> (a, Either a b)
forall a b c. Either (a, b) (a, c) <-> (a, Either b c)
I.eitherSecond Bijection (->) (Either (a, a) (a, b)) (a, b)
-> Free f (Either (a, a) (a, b)) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f (a, a) -> Free f (a, b) -> Free f (Either (a, a) (a, b))
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF ((forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f a -> Free f (a, a)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f a
qp) ((forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f b
qq)
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Join Free f a
p Free f b
q) Free f b
r = Bijection (->) (a, (b, b)) (a, b)
(a, (b, b)) <-> ((a, b), b)
forall a b c. (a, (b, c)) <-> ((a, b), c)
pivot Bijection (->) (a, (b, b)) (a, b)
-> Free f (a, (b, b)) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f (b, b) -> Free f (a, (b, b))
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p ((forall a' b'. f a' -> f b' -> Ordering)
-> Free f b -> Free f b -> Free f (b, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f b
q Free f b
r)
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp p :: Free f a
p@(Free f a
x) q :: Free f b
q@(Free f b
y) | f a -> f b -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp f a
x f b
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT = (b, a) <-> (a, b)
forall a b. (a, b) <-> (b, a)
I.swap ((b, a) <-> (a, b)) -> Free f (b, a) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f b -> Free f a -> Free f (b, a)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join Free f b
q Free f a
p
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp p :: Free f a
p@(Free f a
x) (Join q :: Free f a
q@(Free f a
y) Free f b
r) | f a -> f a -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp f a
x f a
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT = Bijection (->) (a, (a, b)) (a, b)
(a, (a, b)) <-> (a, (a, b))
forall a b c. (a, (b, c)) <-> (b, (a, c))
swap12 Bijection (->) (a, (a, b)) (a, b)
-> Free f (a, (a, b)) -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< Free f a -> Free f (a, b) -> Free f (a, (a, b))
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
joinTDNF Free f a
q ((forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f b
r)
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
Empty Free f b
p = Bijection (->) (a, b) b -> Bijection (->) b (a, b)
forall b c. Bijection (->) b c -> Bijection (->) c b
forall (a :: * -> * -> *) b c. BiArrow a => a b c -> a c b
I.invert Bijection (->) (a, b) b
((), b) <-> b
forall a. ((), a) <-> a
I.snd Bijection (->) b (a, b) -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering) -> Free f b -> Free f b
forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f b
p
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p Free f b
Empty = Bijection (->) (a, b) a -> Bijection (->) a (a, b)
forall b c. Bijection (->) b c -> Bijection (->) c b
forall (a :: * -> * -> *) b c. BiArrow a => a b c -> a c b
I.invert Bijection (->) (a, b) a
(a, ()) <-> a
forall a. (a, ()) <-> a
I.fst Bijection (->) a (a, b) -> Free f a -> Free f (a, b)
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p
sortJoinTDNF forall a' b'. f a' -> f b' -> Ordering
_ Free f a
p Free f b
q = Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b. Free f a -> Free f b -> Free f (a, b)
Join Free f a
p Free f b
q

-- |Equivalent to 'freeTDNF', but also sorts the terms within each 'Join' clause to conform to the given ordering.
-- The resulting 'Join' trees will be right-linearized (@Join x (Join y (Join z ...))@ such that @x <= y@, @y <= z@, etc.
-- THis performs a /O(n^2)/ bubble sort on the already exponential TDNF.
sortFreeTDNF :: (forall a' b' . f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF :: forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Transform a <-> a
f Free f a
p) = a <-> a
f (a <-> a) -> Free f a -> Free f a
forall (f :: * -> *) a b. Functor f => (a <-> b) -> f a -> f b
>$< (forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p
sortFreeTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Choose Free f a
p Free f b
q) = Free f a -> Free f b -> Free f (Either a b)
forall (f :: * -> *) a b.
Free f a -> Free f b -> Free f (Either a b)
chooseTNF ((forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p) ((forall a' b'. f a' -> f b' -> Ordering) -> Free f b -> Free f b
forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f b
q)
sortFreeTDNF forall a' b'. f a' -> f b' -> Ordering
cmp (Join Free f a
p Free f b
q) = (forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
forall (f :: * -> *) a b.
(forall a' b'. f a' -> f b' -> Ordering)
-> Free f a -> Free f b -> Free f (a, b)
sortJoinTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f a
p ((forall a' b'. f a' -> f b' -> Ordering) -> Free f b -> Free f b
forall (f :: * -> *) a.
(forall a' b'. f a' -> f b' -> Ordering) -> Free f a -> Free f a
sortFreeTDNF f a' -> f b' -> Ordering
forall a' b'. f a' -> f b' -> Ordering
cmp Free f b
q)
sortFreeTDNF forall a' b'. f a' -> f b' -> Ordering
_ Free f a
p = Free f a
p