[Flolac'10]Operational Semantics Ex1

今天講了一點基本的Operational Semantics的東西。出了一個簡單的Homework。反正不用交出去，OCaml也不熟，所以就用Haskell來玩一下看看。:)

type Number = String
type Variable = String
data AExp = Num Number
          | Var Variable
          | Add AExp AExp
          | Mult AExp AExp
          | Sub AExp AExp
          deriving (Show)

data BExp = T
          | F
          | Eq AExp AExp
          | LeEq AExp AExp
          | Not BExp
          | Conj BExp BExp
          deriving (Show)
          
data Stm = Ass Variable AExp
         | Skip
         | Seq Stm Stm
         | If BExp Stm Stm
         | While BExp Stm
         | Repeat Stm BExp
         deriving (Show)
         
type State = Variable -> Int

n :: Number -> Int
n m = (read m) :: Int

a :: AExp -> State -> Int
a e s  = case e of 
  Num m -> n m
  Var x -> s x
  Add e1 e2 -> (a e1 s) + (a e2 s)
  Mult e1 e2 -> (a e1 s) * (a e2 s)
  Sub e1 e2 -> (a e1 s) - (a e2 s)

b :: BExp -> State -> Bool
b e s  = case e of
  T          -> True
  F          -> False
  Eq e1 e2   -> (a e1 s) == (a e2 s)
  LeEq e1 e2 -> (a e1 s) <= (a e2 s)
  Not bexp   -> not (b bexp s)
  Conj b1 b2 -> (b b1 s) && (b b2 s)

data Configure = Inter Stm State
               | Final State
               

update :: Variable -> AExp -> State -> State
update x e s y = if (x==y) 
  then a e s 
  else s y

ns :: Configure -> Configure
ns c = case c of
  (Inter (Ass v e) s)     -> Final (update v e s)
  (Inter (Skip) s)        -> Final s
  (Inter (Seq st1 st2) s) -> let (Final s') = ns (Inter st1 s) in ns (Inter st2 s')
  (Inter (If bexp st1 st2) s) -> if (b bexp s) 
    then ns (Inter st1 s)
    else ns (Inter st2 s)
  (Inter (While bexp st) s)   -> if (b bexp s) 
    then ns (Inter st s)
    else (Final s)
  (Inter (Repeat st bexp) s)  -> let (Final s') = ns (Inter st s) in
    if (b bexp s') 
      then ns (Inter (Repeat st bexp) s')
      else Final s'

default_state x = error "NotFound"

x1_state = update "x" (Num "1") default_state

test1 = Seq Skip (Ass "x" (Num "5"))

new_state = let (Final sFun) = ns (Inter test1 x1_state) in sFun "x"