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


{- Part 3 

Conatural numbers. 

Health warning: Don't try this exercise unless you feel very clever.
You will get upto 80/100 without it, anyway. 

I repeat the definition of the conatural numbers from the lecture.
-}

record ℕ∞ : Set where
  coinductive
  field
    prd∞ : Maybe ℕ∞

open ℕ∞

zero∞ : ℕ∞
prd∞ zero∞ = nothing

suc∞ : ℕ∞ → ℕ∞
prd∞ (suc∞ n) = just n

_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
prd∞ (m +∞ n) with prd∞ m
prd∞ (m +∞ n) | just m' = just (m' +∞ n)
prd∞ (m +∞ n) | nothing = prd∞ n

{- Now your task is to define multiplication _*∞_ for conatural numbers.

This is harder then it sounds. Why? Because to check termination of corecursive programs 
agda needs to make sure that if you want to find out a finite amout of information about
the result of the function it only needs a finite amount of information about its inputs. 
Such a function is called productive. And agda isn't very clever in figuring this out, it
has to be obvious from the program (similar as structural recursion has to be obviously 
structural). 

If you need more hints, ask on moodle.
-}

_*∞_ :  ℕ∞ → ℕ∞ → ℕ∞
m *∞ n = {!!}

{- Here are some testing tools -}

ℕ→ℕ∞ : ℕ → ℕ∞
ℕ→ℕ∞ zero = zero∞
ℕ→ℕ∞ (suc n) = suc∞ (ℕ→ℕ∞ n)

{- The first parameter below is a bound. -}
ℕ∞→ℕ : ℕ → ℕ∞ → Maybe ℕ
ℕ∞→ℕ n m with prd∞ m
ℕ∞→ℕ zero m | just x = nothing
ℕ∞→ℕ (suc n) m | just m' with ℕ∞→ℕ n m'
ℕ∞→ℕ (suc n) m | just m' | just k = just (suc k)
ℕ∞→ℕ (suc n) m | just m' | nothing = nothing
ℕ∞→ℕ n m | nothing = just zero

{- My unit-test -}
x3*5 = ℕ∞→ℕ 100 (ℕ→ℕ∞ 3 *∞ ℕ→ℕ∞ 5)
{- just 15 -}