implementation module While

from StdBool import not, &&, ||
from StdList import hd, last, map, take
from StdMisc import abort
from StdOverloaded import class +++(..), class toString(..)
from StdString import instance +++ {#Char},
    instance toString Int, instance toString Bool, instance toString Char
import _SystemArray

// Evaluation utilities

instance eval Int Int where eval _ i _ = i
instance eval Var Int where eval _ v st = st v
instance eval ArithExpr Int
where
    eval m (a1 + a2) st = addI (eval m a1 st) (eval m a2 st)
    eval m (a1 - a2) st = subI (eval m a1 st) (eval m a2 st)
    eval m (a1 * a2) st = mulI (eval m a1 st) (eval m a2 st)

instance eval Bool Bool where eval _ b _ = b
instance eval BoolExpr Bool
where
    eval m (a1 == a2) st = eqI (eval m a1 st) (eval m a2 st)
    eval m (a1 <= a2) st = ltI (eval m a1 st) (eval m a2 st)
                         || eqI (eval m a1 st) (eval m a2 st)
    eval m (~ b) st = not (eval m b st)
    eval m (b1 /\ b2) st = eval m b1 st && eval m b2 st

instance eval Stm State
where
    eval SOS stm st = let (Done st`) = last (seq stm st) in st`
    eval NS stm st  = (tree stm st).result

// Natural Semantics

tree :: Stm State -> DerivTree
tree stm=:Skip st = dTree stm st [] st
tree stm=:(v:=a) st = dTree stm st [] (\w->if (eqC v w) (eval NS a st) (st w))
tree stm=:(s1 :. s2) st = dTree stm st [t1,t2] t2.result
where t1 = tree s1 st; t2 = tree s2 t1.result
tree stm=:(If b s1 s2) st = dTree stm st [t] t.result
where t = tree (if (eval NS b st) s1 s2) st
tree stm=:(While b s) st
| eval NS b st = dTree stm st [t1,t2] t2.result
| otherwise    = dTree stm st [] st
where t1 = tree s st; t2 = tree stm t1.result

// Records are too much typing
dTree :: Stm State [DerivTree] State -> DerivTree
dTree stm st ts r = {stm=stm, state=st, children=ts, result=r}

// Structural Operational Semantics

seq :: Stm State -> DerivSeq
seq stm st = case step stm st of (Done st) = [Done st]
                                 (NDone stm st) = [NDone stm st : seq stm st]
where
    step :: Stm State -> DerivSeqNode
    step Skip st = Done st
    step (v := a) st = Done (\w->if (eqC v w) (eval SOS a st) (st w))
    step (s1 :. s2) st = case step s1 st of 
        seqe=:(NDone s1` st`) = NDone (s1` :. s2) st`
        (Done st`) = NDone s2 st`
    step (If b s1 s2) st = NDone (if (eval SOS b st) s1 s2) st
    step stm=:(While b s) st = NDone (If b (s:.stm) Skip) st

// String utilities

instance toString ArithExpr
where
    toString (a1 + a2) = toString a1 +++ "+" +++ toString a2
    toString (a1 - a2) = toString a1 +++ "-" +++ toString a2
    toString (a1 * a2) = toString a1 +++ "*" +++ toString a2

instance toString BoolExpr
where
    toString (a1 == a2) = toString a1 +++ "=" +++ toString a2
    toString (a1 <= a2) = toString a1 +++ "<=" +++ toString a2
    toString (~ b) = "~" +++ toString b
    toString (b1 /\ b2) = toString b1 +++ "/\\" +++ toString b2

instance toString Stm
where
    toString Skip = "skip"
    toString (s1 :. s2) = toString s1 +++ "; " +++ toString s2
    toString (v := a) = {v} +++ ":=" +++ toString a
    toString (If b s1 s2) = "if " +++ toString b +++ " then " +++ toString s1 +++ " else " +++ toString s2
    toString (While b s) = "while " +++ toString b +++ " do " +++ toString s +++ " done"

instance toString DerivTree
where
    toString t = toS 0 t
    where
        toS :: Int DerivTree -> String
        toS i {stm,children=[]} = pad i +++ toString stm +++ "\n"
        toS i {stm,children} = pad i +++ "(" +++ toString stm +++ "\n" +++
                concat (map (toS (addI i 1)) children) +++ pad i +++ ")\n"

        concat :: [String] -> String
        concat [] = ""
        concat [s:ss] = s +++ concat ss

        pad :: Int -> String
        pad 0 = ""
        pad i = pad (subI i 1) +++ "  "

instance toString DerivSeq
where
    toString seq = join "\n" (map toString [stm \\ (NDone stm _) <- seq])
    where
        join :: String [String] -> String
        join _ [] = ""
        join g [s:ss] = s +++ g +++ join g ss

// Low end
addI :: !Int !Int -> Int
addI a b = code inline {
    addI
}

subI :: !Int !Int -> Int
subI a b = code inline {
    subI
}

mulI :: !Int !Int -> Int
mulI a b = code inline {
    mulI
}

eqI :: !Int !Int -> Bool
eqI a b = code inline {
    eqI
}

ltI :: !Int !Int -> Bool
ltI a b = code inline {
    ltI
}

eqC :: !Char !Char -> Bool
eqC a b = code inline {
    eqC
}