expr/exist/while.icl

   1 implementation module while
   2
   3 import StdEnv
   4
   5 :: Gamma :== String -> Int
   6 instance gamma Gamma
   7 where
   8         put g i v = \i`->if (i == i`) v (g i)
   9         get g v = g v
  10
  11 emptyGamma :: Gamma
  12 emptyGamma = abort "Undefined variable"
  13
  14 instance eval WhileExpr
  15 where
  16         eval (i =. v)         = \g->put g i (evali v g)
  17         eval (If b _ t _ e)   = \g->if (evalb b g) (eval t g) (eval e g)
  18         eval (a :. b)         = eval b o eval a
  19         eval x=:(While b _ e) = \g->if (evalb b g) (eval (e :. x) g) g
  20         eval Skip             = id
  21         eval (WExpr e)        = eval e
  22
  23 instance evali WhileInt
  24 where
  25         evali (Int i)  = const i
  26         evali (Var s)  = flip get s
  27         evali (a +. b) = \g->evali a g + evali b g
  28         evali (WInt e) = evali e
  29
  30 instance evalb WhileBool
  31 where
  32         evalb (Bool b)  = const b
  33         evalb (a ==. b) = \g->evali a g == evali b g
  34         evalb (a &. b)  = \g->evalb a g && evalb b g
  35         evalb (Not a)   = not o evalb a
  36         evalb (WBool e) = evalb e
  37
  38 Start = (eval ("a" =. Int 42 :. While (Bool False) Do ("b" =. Int 4)) emptyGamma) "a"