Solve HW3.

HomeworkThree.idr

@@ -0,0 +1,62 @@
+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