{-# OPTIONS --sized-types #-}
module nat-cp where

open import Data.Nat hiding (_+_)
open import Codata.Sized.Conat hiding (_+_)
open import Codata.Sized.Thunk
open import Size
open import Data.Sum renaming (_⊎_ to _+_)
open import Data.Unit
open import Function using (_∘_ ; id)


inℕ : ⊤ + ℕ → ℕ
inℕ = [ (λ _ → zero) , suc ]

outℕ : ℕ → ⊤ + ℕ
outℕ zero = inj₁ tt
outℕ (suc n) = inj₂ n

recℕ : (ℕ → ℕ) → ⊤ + ℕ → ⊤ + ℕ
recℕ f = [ inj₁ ∘ id , inj₂ ∘ f ]

{-
this typechecks, but Agda cannot ensure termination:
cataℕ : (⊤ + ℕ → ℕ) → ℕ → ℕ 
cataℕ g = g ∘ recℕ (cataℕ g) ∘ outℕ
-}

cataℕ : (⊤ + ℕ → ℕ) → ℕ → ℕ
cataℕ g zero = g (inj₁ tt)
cataℕ g (suc n) = g (inj₂ (cataℕ g n))

-- For the anamorphism, we have to switch to the final coalgebra of ⊤ + X
anaℕ : {i : Size} → (Conat i → ⊤ + Conat i) → Conat i → Conat i
anaℕ h = [ (λ _ → zero) , (λ x → suc λ where .force → x) ] ∘ h

plus : ℕ → ℕ → ℕ
plus a = cataℕ [ (λ _ → a) , suc ]

mult : ℕ → ℕ → ℕ
mult a = cataℕ [ (λ _ → zero) , plus a ]

exp : ℕ → ℕ → ℕ
exp a = cataℕ [ (λ _ → 1) , mult a ]