Initial commit

7 files changed, 369 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1fc2545
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,11 @@
+# Executables
+*.exe
+*.out
+test
+
+# Directory used to store object files, abc files and assembly files
+Clean System Files/
+
+# iTasks environment extra data
+*-data/
+sapl/
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..932c31a
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2016 Camil Staps
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..b9162d8
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,18 @@
+CLM=clm
+CLMFLAGS=-b -nt
+TEST=test
+DEPS=While.dcl While.icl
+
+all: $(TEST)
+
+$(TEST): %: %.icl $(DEPS)
+	$(CLM) $(CLMFLAGS) $@ -o $@
+
+run_test: $(TEST)
+	./$^
+
+clean:
+	rm -fvr $(TEST) Clean\ System\ Files
+
+.PHONY: all clean run_test
+
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..dc4c5e5
--- /dev/null
+++ b/README.md
@@ -0,0 +1,72 @@
+# CleanWhile
+Clean While tools
+
+This module provides types and tools to work with [While][while] in
+[Clean][clean].
+
+Typically you will need `:: Stm`, `:: State` and `eval`. A `Stm` is a statement
+in the While language. Only `;` couldn't be implemented as-is, because it is
+reserved in Clean. The statement composition operator is now `:.`.
+
+For example, the 
+[following program](http://www.cs.ru.nl/~hubbers/courses/sc/leertaak/04.html)
+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):
+
+    sqrt :: Stm
+    sqrt = 'z' := 0 :.
+           'o' := 1 :.
+           's' := 1 :.
+           While ('s' <= 'x')
+             ( 'z' := 'z' + 1 :.
+               'o' := 'o' + 2 :.
+               's' := 's' + 'o' )
+
+We can now execute this code on a `State`, which maps `Var` (`Char`) to `Int`:
+
+    Start :: Int
+    Start = eval NS sqrt st 'z'
+    where
+        st :: Var -> Int
+        st 'x' = 36
+
+`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
+[documentation of While][while] suggests, a `State` can be a partial function
+here. There is no efficient way of enforcing total functions in Clean.
+
+The `NS` argument tells the module to use Natural Semantics (as opposed to
+`SOS`, Structural Operational Semantics). The result should be the same (though
+this has not been heavily tested, it has been proven for the derivation rules
+that define NS and SOS, and the functions in this module are directly derived
+from those rules). These two semantics are defined for While by Nielson and
+Nielson in [Semantics with Applications: A Formal Introduction][wiley].
+
+Besides evaluating statements, we can also construct derivation trees and
+sequences. The following two Start rules generate a derivation tree for Natural
+Semantics and a derivation sequence for Structural Operational Semantics. Both
+types can be `toString`ed:
+
+    Start = tree sqrt st
+    Start = seq sqrt st
+
+## Warning
+
+This breaks `StdEnv` completely. Only import what you need, as always, and use
+qualified imports where needed.
+
+## Todo
+
+ - Gast testing
+ - More boolean operators for testing integers besides `=` and `<=`
+ - Prettyprint for `DerivTree`
+ - Parser
+
+## Copyright &amp; license
+Copyright &copy; 2016 Camil Staps. Licensed under MIT, see LICENSE.
+
+[while]: http://profs.sci.univr.it/~merro/files/WhileExtra_l.pdf
+[clean]: http://clean.cs.ru.nl/Clean
+[wiley]: http://cs.ioc.ee/~tarmo/pls06/wiley.ps.gz
+
diff --git a/While.dcl b/While.dcl
new file mode 100644
index 0000000..1ab5ce9
--- /dev/null
+++ b/While.dcl
@@ -0,0 +1,73 @@
+definition module While
+
+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
+
+instance eval Stm State
+instance eval Int Int
+instance eval Var Int
+instance eval ArithExpr Int
+instance eval Bool Bool
+instance eval BoolExpr Bool
+
+instance toString ArithExpr
+instance toString BoolExpr
+instance toString Stm
+instance toString DerivTree
+instance toString DerivSeq
+
+// Syntax
+
+:: Stm = Skip                                   // Skip
+       | (:.) infixr 1 Stm Stm                  // Composition
+       | E.a: (:=) infix 2 Var a                // Assignment
+         & eval a Int & toString a
+       | E.a: If a Stm Stm                      // If
+         & eval a Bool & toString a
+       | E.a: While a Stm                       // While
+         & eval a Bool & toString a
+
+:: Var :== Char                                 // Variable
+
+:: ArithExpr = E.a b: (+) infixl 6 a b          // Addition
+               & eval a Int & toString a & eval b Int & toString b
+             | E.a b: (-) infixl 6 a b          // Subtraction
+               & eval a Int & eval b Int & toString a & toString b
+             | E.a b: (*) infixl 7 a b          // Multiplication
+               & eval a Int & toString a & eval b Int & toString b
+
+:: BoolExpr = E.a b: (==) infix 4 a b           // Equality on ArithExpr
+               & 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: ~ a                          // Negation
+               & eval a Bool & toString a
+            | E.a b: (/\) infixr 3 a b          // Conjunction
+               & eval a Bool & toString a & eval b Bool & toString b
+
+:: State :== Var -> Int
+
+// Natural Semantics
+
+:: DerivTree = { stm :: Stm
+               , state :: State
+               , children :: [DerivTree]
+               , result :: State
+               }
+
+tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2
+
+// Structural Operational Semantics
+
+:: DerivSeqNode = Done State
+                | NDone Stm State
+
+:: DerivSeq :== [DerivSeqNode]
+
+seq :: Stm State -> DerivSeq // The derivation seq. for @arg1 in state @arg2
+
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
+}
+
diff --git a/test.icl b/test.icl
new file mode 100644
index 0000000..95f1276
--- /dev/null
+++ b/test.icl
@@ -0,0 +1,28 @@
+module test
+
+import While
+
+from StdMisc import abort
+from StdOverloaded import class +++(..), class toString(..)
+from StdString import instance +++ {#Char},
+        instance toString Char, instance toString Int
+import _SystemArray
+
+// From http://www.cs.ru.nl/~hubbers/courses/sc/leertaak/04.html
+// 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' )
+
+Start = toString (tree sqrt st)
+where
+    st :: Var -> Int
+    st 'x' = 16
+
+