module HomeworkThree 
%default total

data Value = N Nat | B Bool

namespace A
  data Term = Num Nat | Plus Term Term | Equal Term Term | Cond Term Term Term
  
  error : Value
  error = N 999
  
  sem : Term -> Value
  sem (Num n) = N n
  sem (Plus t1 t2) with (sem t1, sem t2)
    | (N n1, N n2) = N $ n1 + n2
    | _ = error
  sem (Equal t1 t2) with (sem t1, sem t2)
    | (N n1, N n2) = B $ n1 == n2
    | (B b1, B b2) = B $ b1 == b2
    | _ = error
  sem (Cond t1 t2 t3) with (sem t1)
    | B True = sem t2
    | B False = sem t3
    | _ = error

namespace B
  data Ty = Nat | Bool
  data Term : Ty -> Type where
    Num   : Nat -> Term Nat
    Plus  : Term Nat -> Term Nat -> Term Nat
    Equal : Term t -> Term t -> Term Bool
    Cond  : Term Bool -> Term t -> Term t -> Term t

  sem : Term ty -> Value
  sem (Num n) = N n
  sem (Plus t1 t2) with (sem t1, sem t2)
    | (N n1, N n2) = N $ n1 + n2
    | _ = error
  sem (Equal t1 t2) with (sem t1, sem t2)
    | (N n1, N n2) = B $ n1 == n2
    | (B b1, B b2) = B $ b1 == b2
    | _ = error
  sem (Cond t1 t2 t3) with (sem t1)
    | B True = sem t2
    | B False = sem t3
    | _ = error

namespace C
  data Value : Ty -> Type where
    N : Nat  -> Value Nat
    B : Bool -> Value Bool

  sem : Term ty -> Value ty
  sem (Num n) = N n
  sem (Plus t1 t2) with (C.sem t1, C.sem t2)
    | (N n1, N n2) = N $ n1 + n2
  sem (Equal t1 t2) with (C.sem t1, C.sem t2)
    | (N n1, N n2) = B $ n1 == n2
    | (B b1, B b2) = B $ b1 == b2
  sem (Cond t1 t2 t3) with (C.sem t1)
    | B True = C.sem t2
    | B False = C.sem t3