module FunOrn.Functions.Examples.Plus where


open import Data.Unit
open import Data.Fin hiding (_+_ ; lift)
open import Data.Product

open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.Induction
open import IDesc.Examples.Nat hiding (ze ; su)

open import FunOrn.Functions

-- Paper: Example 5.4

type+ : Type
type+ = μ NatD [ tt ]→ μ NatD [ tt ]→ μ NatD [ tt  `⊤

infix 40 _+_ 

pattern ze = ⟨ zero , tt ⟩
pattern su n = ⟨ suc zero , n ⟩ 

_+'_ :  type+ ⟧Type
m +' ze = m , tt
m +' su n = su (proj₁ (m +' n)) , tt 
m +'  suc (suc ()) , _ 


α : Nat  DAlg NatD  _  Nat × )
α m {tt} {zero , tt} tt = m , tt
α m {tt} {suc zero , n } (m+n , tt) = su m+n , tt
α m {tt} {suc (suc ()) , _} _

_+_ :  type+ ⟧Type
m + n = induction NatD  _  Nat × )  {i}{xs}  α m {i}{xs}) n

private
  module Test where

    open import Relation.Binary.PropositionalEquality

    test-0+0 : ze + ze  ze +' ze
    test-0+0 = refl
  
    test-m+0 : ∀{m}  m + ze  (m , tt)
    test-m+0 = refl

    test-m+1 : ∀{m}  m + (su ze)  m +' (su ze)
    test-m+1 = refl

    test-m+2 : ∀{m}  m + (su (su ze))  m +' (su (su ze))
    test-m+2 = refl