63 lines
1.5 KiB
Idris
63 lines
1.5 KiB
Idris
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
|