open import Agda.Builtin.Bool renaming (true to tt; false to ff)
open import Agda.Builtin.Nat renaming (suc to su; zero to ze)

module MutualRec (Name : Set) (_≟_ : Name → Name → Bool) where

if_then_else_ : ∀ {A : Set} → Bool → A → A → A
if tt then u else v = u
if ff then u else v = v

mutual
  data Expr : Set where
    _:+:_ : Expr → Expr → Expr
    Var : Name → Expr
    Lit : Nat → Expr
    Let_In : Assgt → Expr → Expr
  data Assgt : Set where
    _↦_ : Name → Expr → Assgt

record Model : Set₁ where field
  Exprᴹ   : Set
  Assgtᴹ  : Set
  _:+:ᴹ_  : Exprᴹ → Exprᴹ → Exprᴹ
  Varᴹ    : Name → Exprᴹ
  Litᴹ    : Nat → Exprᴹ
  Letᴹ_In : Assgtᴹ → Exprᴹ → Exprᴹ
  _↦ᴹ_    : Name → Exprᴹ → Assgtᴹ

module _ (𝕄 : Model) where
  open Model 𝕄
  recExpr  : Expr → Exprᴹ
  recAssgt : Assgt → Assgtᴹ

  recExpr (e₁ :+: e₂)  = recExpr e₁ :+:ᴹ recExpr e₂
  recExpr (Var n)      = Varᴹ n
  recExpr (Lit n)      = Litᴹ n
  recExpr (Let a In e) = Letᴹ recAssgt a In (recExpr e)

  recAssgt (x ↦ e) = x ↦ᴹ recExpr e

Env : Set
Env = Name → Nat

open Model

ev𝕄 : Model
ev𝕄 .Exprᴹ  = Env → Nat
ev𝕄 .Assgtᴹ = Env → Env
ev𝕄 ._:+:ᴹ_ e₁ᴹ e₂ᴹ ρ = e₁ᴹ ρ + e₁ᴹ ρ
ev𝕄 .Varᴹ x ρ = ρ x
ev𝕄 .Litᴹ n ρ = n
ev𝕄 .Letᴹ_In aᴹ eᴹ ρ = eᴹ (aᴹ ρ)
ev𝕄 ._↦ᴹ_ x eᴹ ρ y = if x ≟ y then eᴹ ρ else ρ y

evE : Env → Expr → Nat
evA : Env → Assgt → Env

evE ρ e = recExpr  ev𝕄 e ρ
evA ρ a = recAssgt ev𝕄 a ρ

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat

_&&_ : Bool → Bool → Bool
true && true = true
_ && _ = false

data Tree : Set where
  leaf : Nat → Tree
  branch : Tree → Tree → Tree
  subst : (Nat → Tree) → Tree → Tree

all : (Nat → Bool) → Tree → Bool
all p (leaf x) = p x
all p (branch t1 t2) = all p t1 && all p t2
all p (subst f t) = all (λ b → all p (f b)) t

ASTENV : EoA → Set
ASTENV = λ{A → Env → Env ; E → Env → ℕ}

module foo where
  data ASTF (r : EoA → Set) : EoA → Set where
    _:+:_ : r E → r E → ASTF r E
    Var : String → ASTF r E
    Lit : ℕ → ASTF r E
    Let_In : r A {- ev env assgt -} → r E {- ev env expr ↯ -} → ASTF r E
    _↦_ : String → r E → ASTF r A

  -- translation of Nathaniel's soln
  evAlg : {i : EoA} → ASTF ASTENV i → ASTENV i
  evAlg (x :+: x₁) env = x env + x₁ env
  evAlg (Var x) env = env x
  evAlg (Lit n) env = n
  evAlg (Let envt In expr) env = expr (envt env) 
  evAlg (x ↦ x₁) env = λ y → case x ≈? y of
    λ{ (yes  _) → x₁ env
     ; (no   _) → env y }