```------------------------------------------------------------------------
--                                                                    --
--  Agda code accompanying the article                                --
--                                                                    --
--    Programming metamorphic algorithms:                             --
--    An experiment in type-driven algorithm design                   --
--                                                                    --
--    https://doi.org/10.22152/programming-journal.org/2021/5/7       --
--                                                                    --
--  by Hsiang-Shang ‘Josh’ Ko                                         --
--    (Institute of Information Science, Academia Sinica, Taiwan)     --
--                                                                    --
--  Checked with Agda version 2.6.1 and Standard Library version 1.3  --
--                                                                    --
------------------------------------------------------------------------

open import Function
open import Data.Product
open import Data.Sum
open import Data.Maybe
open import Relation.Binary.PropositionalEquality

data List (A : Set) : Set where
[]  : List A
_∷_ : A → List A → List A

foldr : {A S : Set} → (A → S → S) → S → List A → S
foldr _◁_ e []       = e
foldr _◁_ e (a ∷ as) = a ◁ foldr _◁_ e as

foldl : {A S : Set} → (S → A → S) → S → List A → S
foldl _▷_ e []       = e
foldl _▷_ e (a ∷ as) = foldl _▷_ (e ▷ a) as

mutual

record CoList (B : Set) : Set where
coinductive
field
decon : CoListF B

data CoListF (B : Set) : Set where
[]  : CoListF B
_∷_ : B → CoList B → CoListF B

unfoldr : {B S : Set} → (S → Maybe (B × S)) → S → CoList B
CoList.decon (unfoldr g s) with g s
CoList.decon (unfoldr g s) | nothing       = []
CoList.decon (unfoldr g s) | just (b , s') = b ∷ unfoldr g s'

data AlgList (A {S} : Set) (_◁_ : A → S → S) (e : S) : S → Set where
[]  : AlgList A _◁_ e e
_∷_ : (a : A) → {s : S} → AlgList A _◁_ e s → AlgList A _◁_ e (a ◁ s)

mutual

record CoalgList (B {S} : Set) (g : S → Maybe (B × S)) (s : S) : Set where
coinductive
field
decon : CoalgListF B g s

data CoalgListF (B {S} : Set) (g : S → Maybe (B × S)) : S → Set where
⟨_⟩    : {s : S} → g s ≡ nothing → CoalgListF B g s
_∷⟨_⟩_ : (b : B) → {s s' : S} → g s ≡ just (b , s') → CoalgList B g s' → CoalgListF B g s

open CoalgList

from-left-alg : {A S : Set} → (S → A → S) → A → (S → S) → (S → S)
from-left-alg _▷_ a t = t ∘ flip _▷_ a

foldl-as-foldr : {A S : Set} {_▷_ : S → A → S} {e : S}
(as : List A) → foldl _▷_ e as ≡ foldr (from-left-alg _▷_) id as e
foldl-as-foldr []       = refl
foldl-as-foldr (a ∷ as) = foldl-as-foldr as

module _ {A B S : Set} where

module ConsumingBeforeProducing
(_▷_ : S → A → S) (g : S → Maybe (B × S))
where

cbp : (s : S) → {h : S → S} → AlgList A (from-left-alg _▷_) id h → CoalgList B g (h s)
decon (cbp s []) with g s        | inspect g s
decon (cbp s []) | nothing       | [ eq ] = ⟨ eq ⟩
decon (cbp s []) | just (b , s') | [ eq ] = b ∷⟨ eq ⟩ cbp s' []
cbp s (a ∷ as) = cbp (s ▷ a) as

module Streaming
(_▷_ : S → A → S) (g : S → Maybe (B × S))
(streaming-condition :
{a : A} {b : B} {s s' : S} → g s ≡ just (b , s') → g (s ▷ a) ≡ just (b , s' ▷ a))
where

streaming-lemma : {b : B} {s s' : S} {h : S → S} →
AlgList A (from-left-alg _▷_) id h → g s ≡ just (b , s') → g (h s) ≡ just (b , h s')
streaming-lemma []       eq = eq
streaming-lemma (a ∷ as) eq = streaming-lemma as (streaming-condition eq)

stream : (s : S) → {h : S → S} → AlgList A (from-left-alg _▷_) id h → CoalgList B g (h s)
decon (stream s as      ) with g s        | inspect g s
decon (stream s []      ) | nothing       | [ eq ] = ⟨ eq ⟩
decon (stream s (a ∷ as)) | nothing       | [ eq ] = decon (stream (s ▷ a) as)
decon (stream s as      ) | just (b , s') | [ eq ] = b ∷⟨ streaming-lemma as eq ⟩ stream s' as

cong-from-just : {X : Set} {x x' : X} → (Maybe X ∋ just x) ≡ just x' → x ≡ x'
cong-from-just refl = refl

module Jigsaw-Infinite
(_◁_ : A → S → S) (e : S) (g∞ : S → B × S)
(piece : A × B → B × A)
(jigsaw-conditionᵢ : {a : A} {b : B} {s s' : S} →
g∞ s ≡ (b , s') → let (b' , a') = piece (a , b) in g∞ (a ◁ s) ≡ (b' , a' ◁ s'))
(straight : B) (straight-production : g∞ e ≡ (straight , e))
where

fillᵢₕ : {s : S} → AlgList A _◁_ e s → Σ[ b ∈ B ] Σ[ t ∈ S ] AlgList A _◁_ e t × (g∞ s ≡ (b , t))
fillᵢₕ []       = straight , _ , [] , straight-production
fillᵢₕ (a ∷ as) with fillᵢₕ as
fillᵢₕ (a ∷ as) | b , _ , as' , eq = let (b' , a') = piece (a , b)
in  b' , _ , a' ∷ as' , jigsaw-conditionᵢ eq

jigsawᵢₕ : {s : S} → AlgList A _◁_ e s → CoalgList B (just ∘ g∞) s
decon (jigsawᵢₕ as) with fillᵢₕ as
decon (jigsawᵢₕ as) | b , _ , as' , eq = b ∷⟨ cong just eq ⟩ jigsawᵢₕ as'

fillᵢᵥ : {s : S} (a : A) → CoalgList B (just ∘ g∞) s → CoalgList B (just ∘ g∞) (a ◁ s)
decon (fillᵢᵥ a bs) with decon bs
decon (fillᵢᵥ a bs) | ⟨ () ⟩
decon (fillᵢᵥ a bs) | b ∷⟨ eq ⟩ bs' =
let (b' , a') = piece (a , b)
in  b' ∷⟨ cong just (jigsaw-conditionᵢ (cong-from-just eq)) ⟩ fillᵢᵥ a' bs'

jigsawᵢᵥ : {s : S} → AlgList A _◁_ e s → CoalgList B (just ∘ g∞) s
decon (jigsawᵢᵥ []) = straight ∷⟨ cong just straight-production ⟩ jigsawᵢᵥ []
jigsawᵢᵥ (a ∷ as) = fillᵢᵥ a (jigsawᵢᵥ as)

module Jigsaw-General
(_◁_ : A → S → S) (e : S) (g : S → Maybe (B × S))
(nothing-from-e : g e ≡ nothing)
(piece : A × B → B × A)
(flat? : (a : A) → ({s : S} → g s ≡ nothing → g (a ◁ s) ≡ nothing) ⊎
({s : S} → g (a ◁ s) ≢ nothing))
(straight : B)
(jigsaw-condition :
{a : A} {b : B} {s s' : S} →
g s ≡ just (b , s') ⊎ (g s ≡ nothing × g (a ◁ s) ≢ nothing × b ≡ straight × s' ≡ s) →
let (b' , a') = piece (a , b) in g (a ◁ s) ≡ just (b' , a' ◁ s'))
where

fill : {s : S} (a : A) → CoalgList B g s → CoalgList B g (a ◁ s)
decon (fill a bs) with decon bs
decon (fill a bs) | ⟨ eq ⟩ with flat? a
decon (fill a bs) | ⟨ eq ⟩ | inj₁ flat     = ⟨ flat eq ⟩
decon (fill a bs) | ⟨ eq ⟩ | inj₂ not-flat =
let (b' , a') = piece (a , straight)
in  b' ∷⟨ jigsaw-condition (inj₂ (eq , not-flat , refl , refl)) ⟩ fill a' bs
decon (fill a bs) | b ∷⟨ eq ⟩ bs' =
let (b' , a') = piece (a , b)
in  b' ∷⟨ jigsaw-condition (inj₁ eq) ⟩ fill a' bs'

jigsaw : {s : S} → AlgList A _◁_ e s → CoalgList B g s
decon (jigsaw []) = ⟨ nothing-from-e ⟩
jigsaw (a ∷ as) = fill a (jigsaw as)

module Jigsaw-Left-Infinite
(_▷_ : S → A → S) (g : S → B × S)
(piece : B × A → A × B)
(jigsaw-condition : {a : A} {b : B} {s s' : S} →
g s ≡ (b , s') → let (a' , b') = piece (b , a) in  g (s ▷ a) ≡ (b' , s' ▷ a'))
where

fillₗᵢ : {s : S} → CoalgList B (just ∘ g) s → (a : A) → CoalgList B (just ∘ g) (s ▷ a)
decon (fillₗᵢ bs a) with decon bs
decon (fillₗᵢ bs a) | ⟨ () ⟩
decon (fillₗᵢ bs a) | b ∷⟨ eq ⟩ bs' =
let (a' , b') = piece (b , a)
in  b' ∷⟨ cong just (jigsaw-condition (cong-from-just eq)) ⟩ fillₗᵢ bs' a'

jigsawₗᵢ : {s : S} → CoalgList B (just ∘ g) s →
{h : S → S} → AlgList A (from-left-alg _▷_) id h → CoalgList B (just ∘ g) (h s)
jigsawₗᵢ bs []       = bs
jigsawₗᵢ bs (a ∷ as) = jigsawₗᵢ (fillₗᵢ bs a) as
```