+implementation module while
+
+import StdEnv
+
+:: Gamma :== String -> Int
+instance gamma Gamma
+where
+ put g i v = \i`->if (i == i`) v (g i)
+ get g v = g v
+
+emptyGamma :: Gamma
+emptyGamma = abort "Undefined variable"
+
+instance eval WhileExpr
+where
+ eval (i =. v) = \g->put g i (evali v g)
+ eval (If b _ t _ e) = \g->if (evalb b g) (eval t g) (eval e g)
+ eval (a :. b) = eval b o eval a
+ eval x=:(While b _ e) = \g->if (evalb b g) (eval (e :. x) g) g
+ eval Skip = id
+ eval (WExpr e) = eval e
+
+instance evali WhileInt
+where
+ evali (Int i) = const i
+ evali (Var s) = flip get s
+ evali (a +. b) = \g->evali a g + evali b g
+ evali (WInt e) = evali e
+
+instance evalb WhileBool
+where
+ evalb (Bool b) = const b
+ evalb (a ==. b) = \g->evali a g == evali b g
+ evalb (a &. b) = \g->evalb a g && evalb b g
+ evalb (Not a) = not o evalb a
+ evalb (WBool e) = evalb e
+
+Start = (eval ("a" =. Int 42 :. While (Bool False) Do ("b" =. Int 4)) emptyGamma) "a"