Initial commit

1 files changed, 146 insertions, 0 deletions

diff --git a/While.icl b/While.icl
new file mode 100644
index 0000000..b258d74
--- /dev/null
+++ b/While.icl
@@ -0,0 +1,146 @@
+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
+}
+