open import Data.Nat
open import Data.Bool
open import Data.List
open import Data.Maybe
open import Data.Product

mutual
  {-  coℕ∞   unfolds to coℕ -}
  record coℕ∞ : Set where
    coinductive
    field
      ♭ : coℕ

  {- coℕ are the shapes of coℕ∞ -}

  data coℕ : Set where
    zero : coℕ
    suc  : coℕ∞  → coℕ

open coℕ∞


mutual
  {- the following could be automatically defined since
     it just has moves the unfolding to the argument -}
  _+∞'_ : coℕ∞ → coℕ → coℕ∞
  ♭ (m +∞' n) = ♭ m +∞ n

  _+∞_ : coℕ → coℕ → coℕ
  zero  +∞ n  = n
  suc m  +∞ n  = suc (m +∞' n)




{- The following definition is not defined by guarded recursion
   since a function is applied to the corecursive call
   Using sized types one can make it temination check

-}

{-# TERMINATING #-}
mutual
  _*∞'_ : coℕ∞ → coℕ → coℕ∞
  ♭ (m *∞' n) = ♭ m *∞ n

  _*∞_ : coℕ → coℕ → coℕ
  zero  *∞ n  = zero
  suc m  *∞ n  = n +∞  ♭ (m *∞' n)


{- by unfolding the definition of + one can make it termination check -}
mutual
  _*∞₁'_ : coℕ∞ → coℕ → coℕ∞
  ♭ (m *∞₁' n) = ♭ m *∞ n

  _*∞₁_ : coℕ → coℕ → coℕ
  zero  *∞₁ n  = zero
  suc m  *∞₁ n  = plustimes n m n

  plustimes' : coℕ∞ → coℕ∞ → coℕ → coℕ∞
  ♭ (plustimes'  n m k) = plustimes (♭ n) m k

  plustimes : coℕ → coℕ∞ → coℕ → coℕ
  plustimes zero m k = ♭ (m *∞' k)
  plustimes (suc n) m k = suc (plustimes' n m k)