module Chapter6.IDesc.Examples.Expr where

open import Level hiding (zero ; suc)

open import Data.Empty
open import Data.Unit hiding (_≤?_ ; _≟_)
open import Data.Sum
open import Data.Product
open import Data.Bool hiding (_≟_ ; T)
open import Data.Nat hiding (fold ;  _≟_ ; _*_)
open import Data.Fin hiding (_+_ ; _<_ ; fold ; lift)
open import Data.Vec hiding (lookup ; _>>=_)

open import Relation.Nullary
open import Relation.Binary hiding (_⇒_)
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Tagged
open import Chapter5.IDesc.Fixpoint

open import Chapter5.IDesc.Examples.Expr

open import Chapter5.IDesc.InitialAlgebra
open import Chapter6.IDesc.FreeMonad
open import Chapter6.IDesc.FreeMonad.IMonad
open import Chapter6.IDesc.FreeMonad.Monad


evalStep : ⟦ toDesc ExprD ⟧func Val ⇒ Val
evalStep (lift zero , v , lift tt) = v
evalStep (lift (suc zero) , true , ift , iff , lift tt) = ift
evalStep (lift (suc zero) , false , ift , iff , lift tt) = iff
evalStep {`nat} (lift (suc (suc zero)) , m , n , lift tt) = m + n
evalStep {`nat} (lift (suc (suc (suc ()))) , _)
evalStep {`bool} (lift (suc (suc zero)) , m , n , lift tt) = ⌊ m ≤? n ⌋
evalStep {`bool} (lift (suc (suc (suc ()))) , _)


eval : Expr ⇒ Val
eval e = fold (toDesc ExprD) (λ {ty} → evalStep {ty}) e


data Context : Set where
  [] : Context
  _∷_ : (Γ : Context)(ty : Ty) → Context

Env : Context → Set
Env [] = ⊤
Env (Γ ∷ ty) = Env Γ × Val ty

Var : Context → Ty → Set
Var [] ty = ⊥
Var (Γ ∷ S) T = Var Γ T ⊎ S ≡ T -- Want: True (S ≟ T)

lookup : ∀{Γ T} → Env Γ → Var Γ T → Val T
lookup {[]} γ ()
lookup {Γ ∷ ty} (γ , _) (inj₁ x) = lookup γ x
lookup {Γ ∷ ty} (_ , t) (inj₂ refl) = t

Term : Context → Ty → Set
Term Γ = ExprD * (Var Γ)

Expr' : Ty → Set
Expr' = ExprD * (λ _ → ⊥)

toExpr : Expr' ⇒ Expr
toExpr = fold ExprD' (λ {T} → help {T})
  where ExprD' : func _ Ty Ty
        ExprD' = toDesc (ExprD *D (λ _ → ⊥))
        help : ⟦ ExprD' ⟧func Expr ⇒ Expr
        help (lift zero , () , _)
        help (lift (suc zero) , v , lift tt) = val v
        help (lift (suc (suc zero)) , b , ift , iff , lift tt) = cond b ift iff
        help {`nat} (lift (suc (suc (suc zero))) , m , n , lift tt) = plus m n
        help {`nat} (lift (suc (suc (suc (suc ())))) , _)
        help {`bool} (lift (suc (suc (suc zero))) , m , n , lift tt) = le m n
        help {`bool} (lift (suc (suc (suc (suc ())))) , _)

discharge : ∀{Γ T} → Env Γ → Var Γ T → Expr' T
discharge γ v = ⟨ lift (suc zero) , lookup γ v , lift tt  ⟩

substExpr : ∀{Γ} → Env Γ → Term Γ ⇒ Expr' 
substExpr γ tm = tm >>= discharge γ
  where open RawIMonad (monad ExprD)

evalTerm : ∀{Γ T} → Env Γ → Term Γ T →  Val T
evalTerm γ tm = eval (toExpr (substExpr γ tm))