Overloaded state, more boolean ops, unaliased Var

7 files changed, 128 insertions, 71 deletions

diff --git a/Makefile b/Makefile
index b9162d8..891d3f9 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 CLM=clm
-CLMFLAGS=-b -nt
+CLMFLAGS=-nt
 TEST=test
-DEPS=While.dcl While.icl
+DEPS=While.dcl While.icl WhileVars.dcl WhileVars.icl
 
 all: $(TEST)
 
diff --git a/README.md b/README.md
index 0619e88..a69c119 100644
--- a/README.md
+++ b/README.md
@@ -17,23 +17,26 @@ For example, the [following program][sqrt] is a rounded down square root
 function (if `x=n` at the start and `n` is a natural number, then `z` is the
 square root of `n`, rounded down, after execution):
 
+    import While
+    from WhileVars import o, s, x, z // o :== Var 'o'; etc.
+
     sqrt :: Stm
-    sqrt = 'z' := 0 :.
-           'o' := 1 :.
-           's' := 1 :.
-           While ('s' <= 'x')
-             ( 'z' := 'z' + 1 :.
-               'o' := 'o' + 2 :.
-               's' := 's' + 'o' )
+    sqrt = z := 0 :.
+           o := 1 :.
+           s := 1 :.
+           While (s <= x)
+             ( z := z + 1 :.
+               o := o + 2 :.
+               s := s + o )
 
 ### Evaluation
-We can now execute this code on a `State`, which maps `Var` (`Char`) to `Int`:
+We can now execute this code on a `State`, which maps `Var` to `Int`:
 
     Start :: Int
-    Start = eval NS sqrt st 'z'
+    Start = eval NS sqrt st z
     where
-        st :: Var -> Int
-        st 'x' = 36
+        st :: Char -> Int  // Or: st :: Var -> Int  // st :: CharState
+        st 'x' = 9         //     st (Var 'x') = 9  // st = \'x' -> 9
 
 `eval NS sqrt st` is a `State` itself (the state that results from execution of
 `sqrt` in `st`), so we apply that to `z` to get the result. Other than the
@@ -135,8 +138,6 @@ qualified imports where needed.
 ## Todo
 
  - Gast testing
- - More boolean operators for testing integers besides `==` and `<=`
- - Can boolean operators be made functions rather than type constructors?
  - Prettyprint for `DerivTree`
  - Parser
  - Add the state to the `toString` of `DerivTree` and `DerivSeq`
diff --git a/While.dcl b/While.dcl
index 1ab5ce9..aeb685d 100644
--- a/While.dcl
+++ b/While.dcl
@@ -5,9 +5,8 @@ from StdOverloaded import class toString
 :: Semantics = NS                           // Natural Semantics
              | SOS                          // Structural Operational Semantics
 
-// evaluate @arg2 in state @arg3 according to @arg1
-class eval a b :: Semantics a State -> b
-
+// evaluate @2 in state @3 according to @1
+class eval a b :: Semantics a st -> b | toState st
 instance eval Stm State
 instance eval Int Int
 instance eval Var Int
@@ -15,9 +14,14 @@ instance eval ArithExpr Int
 instance eval Bool Bool
 instance eval BoolExpr Bool
 
+class toState a :: a -> State
+instance toState State
+instance toState CharState
+
 instance toString ArithExpr
 instance toString BoolExpr
 instance toString Stm
+instance toString Var
 instance toString DerivTree
 instance toString DerivSeq
 
@@ -32,7 +36,7 @@ instance toString DerivSeq
        | E.a: While a Stm                       // While
          & eval a Bool & toString a
 
-:: Var :== Char                                 // Variable
+:: Var = Var Char                               // Variable
 
 :: ArithExpr = E.a b: (+) infixl 6 a b          // Addition
                & eval a Int & toString a & eval b Int & toString b
@@ -45,12 +49,21 @@ instance toString DerivSeq
                & eval a Int & toString a & eval b Int & toString b
             | E.a b: (<=) infix 4 a b           // Ord
                & eval a Int & toString a & eval b Int & toString b
+            | E.a b: (>=) infix 4 a b
+               & eval a Int & toString a & eval b Int & toString b
+            | E.a b: (<) infix 4 a b
+               & eval a Int & toString a & eval b Int & toString b
+            | E.a b: (>) infix 4 a b
+               & eval a Int & toString a & eval b Int & toString b
             | E.a: ~ a                          // Negation
                & eval a Bool & toString a
+            | E.a b: (\/) infixr 4 a b          // Disjunction
+               & eval a Bool & toString a & eval b Bool & toString b
             | E.a b: (/\) infixr 3 a b          // Conjunction
                & eval a Bool & toString a & eval b Bool & toString b
 
 :: State :== Var -> Int
+:: CharState :== Char -> Int
 
 // Natural Semantics
 
@@ -60,7 +73,7 @@ instance toString DerivSeq
                , result :: State
                }
 
-tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2
+tree :: Stm st -> DerivTree | toState st // The deriv. tree for @1 in state @2
 
 // Structural Operational Semantics
 
@@ -69,5 +82,5 @@ tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2
 
 :: DerivSeq :== [DerivSeqNode]
 
-seq :: Stm State -> DerivSeq // The derivation seq. for @arg1 in state @arg2
+seq :: Stm st -> DerivSeq | toState st // The deriv. seq. for @1 in state @2
 
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
+
diff --git a/WhileVars.dcl b/WhileVars.dcl
new file mode 100644
index 0000000..4db8197
--- /dev/null
+++ b/WhileVars.dcl
@@ -0,0 +1,11 @@
+definition module WhileVars
+
+from While import ::Var(..)
+
+a :== Var 'a'; b :== Var 'b'; c :== Var 'c'; d :== Var 'd'; e :== Var 'e'
+f :== Var 'f'; g :== Var 'g'; h :== Var 'h'; i :== Var 'i'; j :== Var 'j'
+k :== Var 'k'; l :== Var 'l'; m :== Var 'm'; n :== Var 'n'; o :== Var 'o'
+p :== Var 'p'; q :== Var 'q'; r :== Var 'r'; s :== Var 's'; t :== Var 't'
+u :== Var 'u'; v :== Var 'v'; w :== Var 'w'; x :== Var 'x'; y :== Var 'y'
+z :== Var 'z'
+
diff --git a/WhileVars.icl b/WhileVars.icl
new file mode 100644
index 0000000..1540a10
--- /dev/null
+++ b/WhileVars.icl
@@ -0,0 +1,2 @@
+implementation module WhileVars
+
diff --git a/test.icl b/test.icl
index 54668f2..fe689fc 100644
--- a/test.icl
+++ b/test.icl
@@ -1,6 +1,7 @@
 module test
 
 import While
+from WhileVars import o, s, x, z
 
 from StdMisc import abort
 from StdOverloaded import class +++(..), class toString(..)
@@ -12,18 +13,20 @@ import _SystemArray
 // The rounded down square root function:
 //  { x=n /\ n >= 0 } sqrt { z^2 <= n /\ (z+1)^2 > n }
 sqrt :: Stm
-sqrt = 'z' := 0 :.
-       'o' := 1 :.
-       's' := 1 :.
-       While ('s' <= 'x')
-         ( 'z' := 'z' + 1 :.
-           'o' := 'o' + 2 :.
-           's' := 's' + 'o' )
+sqrt = z := 0 :.
+       o := 1 :.
+       s := 1 :.
+       While (s <= x)
+         ( z := z + 1 :.
+           o := o + 2 :.
+           s := s + o )
 
-//Start = toString (seq sqrt st)
-Start = toString (tree sqrt st)
+Start :: Int                      // Value of z after execution of sqrt in st
+Start = eval NS sqrt st z
+//Start = toString (seq sqrt st)    // Derivation sequence of sqrt in st
+//Start = toString (tree sqrt st)   // Derivation tree of sqrt in st
 where
-    st :: Var -> Int
+    st :: Char -> Int
     st 'x' = 9