Overloaded state, more boolean ops, unaliased Var

1 files changed, 67 insertions, 40 deletions

diff --git a/While.icl b/While.icl
index 6d1a613..efa1c92 100644
--- a/While.icl
+++ b/While.icl
@@ -4,14 +4,14 @@ 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},
+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 = st v
+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)
@@ -23,28 +23,36 @@ 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)
+                           || 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 st) in st`
-    eval NS stm st  = (tree stm st).result
+    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 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
+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
@@ -52,54 +60,70 @@ 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`) = [NDone stm st, Done st`]
-                                 (NDone stm` st`) = [NDone stm st:seq stm` st`]
+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 = Done (\w->if (eqC v w) (eval SOS a st) (st w))
+    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) = toString a1 +++ "+" +++ toString a2
-    toString (a1 - a2) = toString a1 +++ "-" +++ toString a2
-    toString (a1 * a2) = toString a1 +++ "*" +++ toString a2
+    toString (a1 + a2) = a1 <+ "+" <+ a2
+    toString (a1 - a2) = a1 <+ "-" <+ a2
+    toString (a1 * a2) = a1 <+ "*" <+ 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
+    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) = 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"
+    toString (s1 :. s2) = s1 <+ "; " <+ s2
+    toString (v := a) = v <+ ":=" <+ a
+    toString (If b s1 s2) = "if " <+ b <+ " then " <+ s1 <+ " else " <+ s2
+    toString (While b s) = "while " <+ b <+ " do " <+ s <+ " done"
+
+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 +++ toString stm +++ "\n"
-        toS i {stm,children} = pad i +++ "(" +++ toString stm +++ "\n" +++
-                concat (map (toS (addI i 1)) children) +++ pad i +++ ")\n"
+        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 :: [String] -> String
+        concat :: [a] -> String | toString a
         concat [] = ""
-        concat [s:ss] = s +++ concat ss
+        concat [s:ss] = s <+ concat ss
 
         pad :: Int -> String
         pad 0 = ""
@@ -107,11 +131,11 @@ where
 
 instance toString DerivSeq
 where
-    toString seq = join "\n" (map toString [stm \\ (NDone stm _) <- seq])
+    toString seq = join "\n" [stm \\ (NDone stm _) <- seq]
     where
-        join :: String [String] -> String
+        join :: a [b] -> String | toString a & toString b
         join _ [] = ""
-        join g [s:ss] = s +++ g +++ join g ss
+        join g [s:ss] = s <+ g <+ join g ss
 
 // Low end
 addI :: !Int !Int -> Int
@@ -144,3 +168,6 @@ eqC a b = code inline {
     eqC
 }
 
+eqV :: !Var !Var -> Bool
+eqV (Var a) (Var b) = eqC a b
+