{-# LANGUAGE Safe, TypeFamilies, ExistentialQuantification, MultiParamTypeClasses,
     FunctionalDependencies, FlexibleInstances, Rank2Types, FlexibleContexts, UndecidableInstances #-}
 {-# LANGUAGE StandaloneDeriving, QuantifiedConstraints, PolyKinds #-}
 module Math.Tools.FixedPoint where
 import Math.Tools.Visitor
 import Math.Tools.Universe

 type Coalgebra f a = a -> f a

 -- | These are standard definitions of final coalgebra and initial
 --  algebra from category theory.
 class (Functor f) => FinalCoalgebra f a | a -> f where
       unDestroy :: f a -> a
       unfold_gen :: (b -> f b) -> b -> a -- a.k.a. "count_iterations"
       unfold_gen b -> f b
psi = f a -> a
forall (f :: * -> *) a. FinalCoalgebra f a => f a -> a
unDestroy (f a -> a) -> (b -> f a) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a) -> f b -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> f b) -> b -> a
forall b. (b -> f b) -> b -> a
forall (f :: * -> *) a b.
FinalCoalgebra f a =>
(b -> f b) -> b -> a
unfold_gen b -> f b
psi) (f b -> f a) -> (b -> f b) -> b -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> f b
psi

 type Algebra f a = f a -> a

 class (Functor f) => InitialAlgebra f a | a -> f where
       unCreate :: a -> f a
       fold_gen :: (f b -> b) -> a -> b
       fold_gen f b -> b
phi = f b -> b
phi (f b -> b) -> (a -> f b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f b -> b) -> a -> b
forall b. (f b -> b) -> a -> b
forall (f :: * -> *) a b.
InitialAlgebra f a =>
(f b -> b) -> a -> b
fold_gen f b -> b
phi) (f a -> f b) -> (a -> f a) -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
forall (f :: * -> *) a. InitialAlgebra f a => a -> f a
unCreate


 -- | PRIMITIVES FOR RECURSIVE DATA STRUCTURES
 data Rec f = In (f (Rec f))     -- recursion (least fixed point)
 data CoRec f = CoIn (f (CoRec f)) -- corecursion (greatest fixed point)

 unIn :: Rec f -> f (Rec f)
 unIn :: forall (f :: * -> *). Rec f -> f (Rec f)
unIn ~(In f (Rec f)
x) = f (Rec f)
x

 unStrictIn :: CoRec f -> f (CoRec f)
 unStrictIn :: forall (f :: * -> *). CoRec f -> f (CoRec f)
unStrictIn (CoIn f (CoRec f)
x) = f (CoRec f)
x

 -- | fold over arbitrary functor, using standard definition.
 fold :: (Functor f) => (f a -> a) -> Rec f -> a
 fold :: forall (f :: * -> *) a. Functor f => (f a -> a) -> Rec f -> a
fold f a -> a
phi = f a -> a
phi (f a -> a) -> (Rec f -> f a) -> Rec f -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec f -> a) -> f (Rec f) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> a) -> Rec f -> a
forall (f :: * -> *) a. Functor f => (f a -> a) -> Rec f -> a
fold f a -> a
phi) (f (Rec f) -> f a) -> (Rec f -> f (Rec f)) -> Rec f -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec f -> f (Rec f)
forall (f :: * -> *). Rec f -> f (Rec f)
unIn

 -- | unfold over arbitrary functor, using standard definition.
 unfold :: (Functor f) => (a -> f a) -> a -> Rec f -- a.k.a. "count_iterations"
 unfold :: forall (f :: * -> *) a. Functor f => (a -> f a) -> a -> Rec f
unfold a -> f a
psi = f (Rec f) -> Rec f
forall (f :: * -> *). f (Rec f) -> Rec f
In (f (Rec f) -> Rec f) -> (a -> f (Rec f)) -> a -> Rec f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Rec f) -> f a -> f (Rec f)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> f a) -> a -> Rec f
forall (f :: * -> *) a. Functor f => (a -> f a) -> a -> Rec f
unfold a -> f a
psi) (f a -> f (Rec f)) -> (a -> f a) -> a -> f (Rec f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
psi

 transform :: Functor f => (b -> f b) -> (f a -> a) -> b -> a
 transform :: forall (f :: * -> *) b a.
Functor f =>
(b -> f b) -> (f a -> a) -> b -> a
transform b -> f b
divide f a -> a
combine = (f a -> a) -> Rec f -> a
forall (f :: * -> *) a. Functor f => (f a -> a) -> Rec f -> a
fold f a -> a
combine (Rec f -> a) -> (b -> Rec f) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> f b) -> b -> Rec f
forall (f :: * -> *) a. Functor f => (a -> f a) -> a -> Rec f
unfold b -> f b
divide


 -- | Note the builder and visitor for Rec f allows every level of the
 -- recursion to be done by different function. This allows distinctions
 -- by level to be implemented easily as nested RecFold data structures.
 -- Otherwise this distinction would have to be included in the function
 -- itself (using fmap).
 instance (Functor f) => Visitor (Rec f) where
    data Fold (Rec f) a = forall b.RecFold (f b -> a) (Fold (Rec f) b)
    visit :: forall a. Fold (Rec f) a -> Rec f -> a
visit (RecFold f b -> a
f Fold (Rec f) b
z) (In f (Rec f)
x) = f b -> a
f ((Rec f -> b) -> f (Rec f) -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Fold (Rec f) b -> Rec f -> b
forall v a. Visitor v => Fold v a -> v -> a
forall a. Fold (Rec f) a -> Rec f -> a
visit Fold (Rec f) b
z) f (Rec f)
x)

 instance (Functor f) => ComposableVisitor (Rec f) where
    embed :: forall b. (Rec f -> b) -> Fold (Rec f) b
embed Rec f -> b
f = (f (Rec f) -> b) -> Fold (Rec f) (Rec f) -> Fold (Rec f) b
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold (Rec f -> b
f (Rec f -> b) -> (f (Rec f) -> Rec f) -> f (Rec f) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Rec f) -> Rec f
forall (f :: * -> *). f (Rec f) -> Rec f
In) ((Rec f -> Rec f) -> Fold (Rec f) (Rec f)
forall v b. ComposableVisitor v => (v -> b) -> Fold v b
forall b. (Rec f -> b) -> Fold (Rec f) b
embed Rec f -> Rec f
forall a. a -> a
id)

 instance (Functor f) => Builder (Rec f) where
    data Unfold (Rec f) a = RecUnfold (a -> f a)
    build :: forall a. Unfold (Rec f) a -> a -> Rec f
build z :: Unfold (Rec f) a
z@(RecUnfold a -> f a
f) a
x = f (Rec f) -> Rec f
forall (f :: * -> *). f (Rec f) -> Rec f
In (f (Rec f) -> Rec f) -> f (Rec f) -> Rec f
forall a b. (a -> b) -> a -> b
$ (a -> Rec f) -> f a -> f (Rec f)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Unfold (Rec f) a -> a -> Rec f
forall v a. Builder v => Unfold v a -> a -> v
forall a. Unfold (Rec f) a -> a -> Rec f
build Unfold (Rec f) a
z) (f a -> f (Rec f)) -> f a -> f (Rec f)
forall a b. (a -> b) -> a -> b
$ a -> f a
f a
x

 instance (Universe (f (Rec f))) => Universe (Rec f) where
    allElements :: [Rec f]
allElements = (f (Rec f) -> Rec f) -> [f (Rec f)] -> [Rec f]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Rec f) -> Rec f
forall (f :: * -> *). f (Rec f) -> Rec f
In [f (Rec f)]
forall a. Universe a => [a]
allElements


 fold_level :: Fold (Rec f) a -> Fold (Rec f) (f a)
 fold_level :: forall (f :: * -> *) a. Fold (Rec f) a -> Fold (Rec f) (f a)
fold_level = (f a -> f a) -> Fold (Rec f) a -> Fold (Rec f) (f a)
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold f a -> f a
forall a. a -> a
id

 recfold_twice :: (f b -> a) -> (f c -> b) -> Fold (Rec f) c -> Fold (Rec f) a
 recfold_twice :: forall (f :: * -> *) b a c.
(f b -> a) -> (f c -> b) -> Fold (Rec f) c -> Fold (Rec f) a
recfold_twice f b -> a
f f c -> b
g = (f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold f b -> a
f (Fold (Rec f) b -> Fold (Rec f) a)
-> (Fold (Rec f) c -> Fold (Rec f) b)
-> Fold (Rec f) c
-> Fold (Rec f) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f c -> b) -> Fold (Rec f) c -> Fold (Rec f) b
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold f c -> b
g

 recfold :: (f a -> a) -> Fold (Rec f) a
 recfold :: forall (f :: * -> *) a. (f a -> a) -> Fold (Rec f) a
recfold f a -> a
f = let x :: Fold (Rec f) a
x = (f a -> a) -> Fold (Rec f) a -> Fold (Rec f) a
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold f a -> a
f Fold (Rec f) a
x in Fold (Rec f) a
x

 recfold2 :: (f b -> a) -> (f a -> b) -> Fold (Rec f) a
 recfold2 :: forall (f :: * -> *) b a.
(f b -> a) -> (f a -> b) -> Fold (Rec f) a
recfold2 f b -> a
f f a -> b
g = let x :: Fold (Rec f) a
x = (f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold f b -> a
f ((f a -> b) -> Fold (Rec f) a -> Fold (Rec f) b
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold f a -> b
g Fold (Rec f) a
x) in Fold (Rec f) a
x

 recfold_lst :: [f a -> a] -> Fold (Rec f) a
 recfold_lst :: forall (f :: * -> *) a. [f a -> a] -> Fold (Rec f) a
recfold_lst [f a -> a]
lst = let x :: Fold (Rec f) a
x = ((f a -> a) -> Fold (Rec f) a -> Fold (Rec f) a)
-> Fold (Rec f) a -> [f a -> a] -> Fold (Rec f) a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (f a -> a) -> Fold (Rec f) a -> Fold (Rec f) a
forall (f :: * -> *) a b.
(f b -> a) -> Fold (Rec f) b -> Fold (Rec f) a
RecFold Fold (Rec f) a
x [f a -> a]
lst in Fold (Rec f) a
x

 fold_coerce :: (forall a. f a -> g a) -> Fold (Rec f) (Rec g)
 fold_coerce :: forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> Fold (Rec f) (Rec g)
fold_coerce forall a. f a -> g a
alfa = (f (Rec g) -> Rec g) -> Fold (Rec f) (Rec g)
forall (f :: * -> *) a. (f a -> a) -> Fold (Rec f) a
recfold (g (Rec g) -> Rec g
forall (f :: * -> *). f (Rec f) -> Rec f
In (g (Rec g) -> Rec g)
-> (f (Rec g) -> g (Rec g)) -> f (Rec g) -> Rec g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Rec g) -> g (Rec g)
forall a. f a -> g a
alfa)


 -- | strict foldl
 foldl' :: (a -> b -> a) -> a -> [b] -> a
 foldl' :: forall a b. (a -> b -> a) -> a -> [b] -> a
foldl' a -> b -> a
_ a
a [] = a
a
 foldl' a -> b -> a
f a
a (b
x:[b]
xs) = ((a -> b -> a) -> a -> [b] -> a
forall a b. (a -> b -> a) -> a -> [b] -> a
foldl' a -> b -> a
f (a -> [b] -> a) -> a -> [b] -> a
forall a b. (a -> b) -> a -> b
$! a -> b -> a
f a
a b
x) [b]
xs

 instance (Functor f) => InitialAlgebra f (Rec f) where
 	  unCreate :: Rec f -> f (Rec f)
unCreate = Rec f -> f (Rec f)
forall (f :: * -> *). Rec f -> f (Rec f)
unIn

 instance (Functor f) => InitialAlgebra f (CoRec f) where
 	  unCreate :: CoRec f -> f (CoRec f)
unCreate = CoRec f -> f (CoRec f)
forall (f :: * -> *). CoRec f -> f (CoRec f)
unStrictIn

 instance (Functor f) => FinalCoalgebra f (Rec f) where
 	  unDestroy :: f (Rec f) -> Rec f
unDestroy = f (Rec f) -> Rec f
forall (f :: * -> *). f (Rec f) -> Rec f
In

 while :: (a -> a) -> (a -> Bool) -> a -> [a]
 a -> a
f while :: forall a. (a -> a) -> (a -> Bool) -> a -> [a]
`while` a -> Bool
p = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile a -> Bool
p ([a] -> [a]) -> (a -> [a]) -> a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate a -> a
f

 whileM :: (Monad m) => (a -> m a) -> (a -> Bool) -> a -> m [a]
 (a -> m a
f whileM :: forall (m :: * -> *) a.
Monad m =>
(a -> m a) -> (a -> Bool) -> a -> m [a]
`whileM` a -> Bool
p) a
x | a -> Bool
p a
x = do { a
v <- a -> m a
f a
x ; [a]
w <- (a -> m a
f (a -> m a) -> (a -> Bool) -> a -> m [a]
forall (m :: * -> *) a.
Monad m =>
(a -> m a) -> (a -> Bool) -> a -> m [a]
`whileM` a -> Bool
p) a
v ; [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
w) }
                  | Bool
otherwise = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []

 instance Show (Rec Maybe) where
   show :: Rec Maybe -> String
show Rec Maybe
x = String
"Natural[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rec Maybe -> Integer
count_just Rec Maybe
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

 count_just :: Rec Maybe -> Integer
 count_just :: Rec Maybe -> Integer
count_just = Fold (Rec Maybe) Integer -> Rec Maybe -> Integer
forall v a. Visitor v => Fold v a -> v -> a
forall a. Fold (Rec Maybe) a -> Rec Maybe -> a
visit (Fold (Rec Maybe) Integer -> Rec Maybe -> Integer)
-> Fold (Rec Maybe) Integer -> Rec Maybe -> Integer
forall a b. (a -> b) -> a -> b
$ (Maybe Integer -> Integer) -> Fold (Rec Maybe) Integer
forall (f :: * -> *) a. (f a -> a) -> Fold (Rec f) a
recfold (Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
0 Integer -> Integer
forall a. Enum a => a -> a
succ)