module Control.Isomorphism.Partial.Derived 
  ( foldl
  ) where

import Prelude ()
import Control.Category (Category (id, (.)))
import Control.Isomorphism.Partial.Prim (Iso, inverse, unit, associate, iterate, (***))
import Control.Isomorphism.Partial.Constructors (cons, nil)

foldl :: Iso (alpha, beta) alpha -> Iso (alpha, [beta]) alpha
foldl :: forall alpha beta.
Iso (alpha, beta) alpha -> Iso (alpha, [beta]) alpha
foldl Iso (alpha, beta) alpha
i = Iso alpha (alpha, ()) -> Iso (alpha, ()) alpha
forall alpha beta. Iso alpha beta -> Iso beta alpha
inverse Iso alpha (alpha, ())
forall alpha. Iso alpha (alpha, ())
unit
        Iso (alpha, ()) alpha
-> Iso (alpha, [beta]) (alpha, ()) -> Iso (alpha, [beta]) alpha
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Iso alpha alpha
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id Iso alpha alpha -> Iso [beta] () -> Iso (alpha, [beta]) (alpha, ())
forall alpha beta gamma delta.
Iso alpha beta
-> Iso gamma delta -> Iso (alpha, gamma) (beta, delta)
*** Iso () [beta] -> Iso [beta] ()
forall alpha beta. Iso alpha beta -> Iso beta alpha
inverse Iso () [beta]
forall alpha. Iso () [alpha]
nil)
        Iso (alpha, [beta]) (alpha, ())
-> Iso (alpha, [beta]) (alpha, [beta])
-> Iso (alpha, [beta]) (alpha, ())
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Iso (alpha, [beta]) (alpha, [beta])
-> Iso (alpha, [beta]) (alpha, [beta])
forall alpha. Iso alpha alpha -> Iso alpha alpha
iterate (Iso (alpha, beta) alpha -> Iso (alpha, [beta]) (alpha, [beta])
forall {alpha} {beta} {beta}.
Iso (alpha, beta) beta -> Iso (alpha, [beta]) (beta, [beta])
step Iso (alpha, beta) alpha
i) where

  step :: Iso (alpha, beta) beta -> Iso (alpha, [beta]) (beta, [beta])
step Iso (alpha, beta) beta
i' = (Iso (alpha, beta) beta
i' Iso (alpha, beta) beta
-> Iso [beta] [beta] -> Iso ((alpha, beta), [beta]) (beta, [beta])
forall alpha beta gamma delta.
Iso alpha beta
-> Iso gamma delta -> Iso (alpha, gamma) (beta, delta)
*** Iso [beta] [beta]
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
         Iso ((alpha, beta), [beta]) (beta, [beta])
-> Iso (alpha, [beta]) ((alpha, beta), [beta])
-> Iso (alpha, [beta]) (beta, [beta])
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Iso (alpha, (beta, [beta])) ((alpha, beta), [beta])
forall alpha beta gamma.
Iso (alpha, (beta, gamma)) ((alpha, beta), gamma)
associate
         Iso (alpha, (beta, [beta])) ((alpha, beta), [beta])
-> Iso (alpha, [beta]) (alpha, (beta, [beta]))
-> Iso (alpha, [beta]) ((alpha, beta), [beta])
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Iso alpha alpha
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id Iso alpha alpha
-> Iso [beta] (beta, [beta])
-> Iso (alpha, [beta]) (alpha, (beta, [beta]))
forall alpha beta gamma delta.
Iso alpha beta
-> Iso gamma delta -> Iso (alpha, gamma) (beta, delta)
*** Iso (beta, [beta]) [beta] -> Iso [beta] (beta, [beta])
forall alpha beta. Iso alpha beta -> Iso beta alpha
inverse Iso (beta, [beta]) [beta]
forall alpha. Iso (alpha, [alpha]) [alpha]
cons)