module Chapter8.AlgebraicOrnament.Examples.Expr where

open import Level hiding (zero ; suc)

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

open import Relation.Binary.PropositionalEquality

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.InitialAlgebra
open import Chapter5.IDesc.Induction

import  Chapter8.AlgebraicOrnament

ExprD : func _ ⊤ ⊤
ExprD = func.mk λ _ → 
        `σ  (λ { zero → `Σ ℕ λ _ → `1 
                ; (suc zero) → `var tt `× `var tt `× `1 
                ; (suc (suc ())) })

Expr : Set
Expr = μ ExprD tt

const : ℕ → Expr
const n = ⟨ zero , n , lift tt ⟩

add : Expr → Expr → Expr
add m n = ⟨ suc zero , m , n , lift tt ⟩

α : Alg ExprD (λ _ → ℕ)
α {tt} (zero , n , lift tt) = n
α {tt} (suc zero , el , er , lift tt) = el + er
α {tt} (suc (suc ()) , _)

open Chapter8.AlgebraicOrnament.Func ExprD α

ExprSem : ℕ → Set
ExprSem n = μ algOrnD (tt , n)

constS : (n : ℕ) → ExprSem n
constS n = ⟨ (zero , n , lift tt) , refl , lift tt ⟩

addS : ∀{m n} → ExprSem m → ExprSem n → ExprSem (m + n)
addS {m}{n} e₁ e₂ = ⟨ (suc zero , m , n , lift tt) , refl , e₁ , e₂ , lift tt ⟩

private
  record ⟨optimise-0+_⟩ {n : ℕ}(e : ExprSem n) : Set where
    constructor return
    field
      call : ExprSem n
  open ⟨optimise-0+_⟩ public

  β : DAlg algOrnD (λ e → ⟨optimise-0+ e ⟩) 
  β {tt , .n} {(zero , n , lift tt) , refl , lift tt} (lift tt) = return (constS n)
  β {tt , .n} {(suc zero , zero , n , lift tt) , refl , ⟨ (zero , . , lift tt) , refl , lift tt ⟩ , e₂ , lift tt} (optL , optR , lift tt) = return (call optR)
  β {tt , .(m + n)} {(suc zero , m , n , lift tt) , refl , e₁ , e₂ , lift tt} (optL , optR , lift tt) = return (addS e₁ e₂)
  β {_} {(suc (suc ()) , _) , _ , _} _

  optimise : ∀{n} → (e : ExprSem n) → ⟨optimise-0+ e ⟩
  optimise = induction algOrnD (λ e → ⟨optimise-0+ e ⟩) β

optimise-0+ : ∀{n} → (e : ExprSem n) → ExprSem n
optimise-0+ e = call (optimise e)

module Test where

  test-0+ : ∀{k n} → optimise-0+ (addS {}{k} (constS ) n) ≡ optimise-0+ n
  test-0+ = refl