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 {#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 = (toState 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 (a1 >= a2) st = eval m (a2 <= a1) st
    eval m (a1 < a2) st  = ltI (eval m a1 st) (eval m a2 st)
    eval m (a1 > a2) st  = eval m (a2 < a1) st
    eval m (~ b) st      = not (eval m b st)
    eval m (b1 /\ b2) st = eval m b1 st && eval m b2 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 (toState st)) in st`
    eval NS stm st  = (tree stm (toState st)).result

// Natural Semantics

tree :: Stm st -> DerivTree | toState st
tree stm stv = tree` stm (toState stv)
where
    tree` :: Stm State -> DerivTree
    tree` stm=:Skip st = dTree stm st [] st
    tree` stm=:(v:=a) st
        = let e = eval NS a st in dTree stm st [] (\w->if (eqV v w) e (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 st -> DerivSeq | toState st
seq stm stv = let st = toState stv in case step stm st of
    (Done st`) = [NDone stm 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 = let e = eval SOS a st in Done (\w->if (eqV v w) e (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

// State utilities

instance toState State where toState st = st
instance toState CharState where toState cst = \(Var v) -> cst v
instance toState (Var -> Int) where toState st = st

// String utilities

(<+) infixr 5 :: a b -> String | toString a & toString b
(<+) a b = toString a +++ toString b

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

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

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

parens :: Stm -> String
parens (s1 :. s2) = "(" <+ s1 <+ "; " <+ s2 <+ ")"
parens stm        = toString stm

instance toString Var where toString (Var v) = {v}

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

        concat :: [a] -> String | toString a
        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" [stm \\ (NDone stm _) <- seq]
    where
        join :: a [b] -> String | toString a & toString b
        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
}

eqV :: !Var !Var -> Bool
eqV (Var a) (Var b) = eqC a b