denotational semantics

git-svn-id: https://slps.svn.sourceforge.net/svnroot/slps@733 ab42f6e0-554d-0410-b580-99e487e6eeb2

topics/exercises/README.txt

@@ -7,7 +7,8 @@ while3	 - big step semantics for While (+ a DCG parser)
 while4	 - small step semantics for While (+ a DCG parser)
 while5   - typed While in Prolog
 while6   - While evaluation in Haskell (incomplete)
-while7   - While evaluation in Haskell (complete)
+while7   - While evaluation in Haskell (complete, big step operational)
+while8   - While execution in Haskell (complete, denotational)
 
 xml1	 - a DCG parser for XML subset (elements only)
 xml2	 - a DCG parser for XML subset (elements and attributes)

topics/exercises/while8/Eval.hs → topics/exercises/while8/Evaluation.hs

@@ -1,4 +1,4 @@
-module Eval where
+module Evaluation where
 
 import Syntax
 import Prelude hiding (lookup)

topics/exercises/while8/Exec.hs → topics/exercises/while8/Execution.hs

@@ -1,7 +1,7 @@
-module Exec where
+module Execution where
 
 import Syntax
-import Eval
+import Evaluation
 import Prelude hiding (lookup)
 
 update :: State -> Identifier -> Int -> State
@@ -11,6 +11,7 @@ update ((x1,v1):xvs) x2 v2 =
     then ((x1,v2):xvs)
     else ((x1,v1):(update xvs x2 v2))
 
+-- Denotational semantics of While, slides 541–544
 exec :: Statement -> State -> State
 exec (Seq s1 s2) = exec s2 . exec s1
 exec Skip = id
@@ -25,7 +26,3 @@ cond p g1 g2 st | p st      = g1 st
 
 fix :: (t -> t) -> t
 fix f = f (fix f)
-
-main =
-	do
-		print $ exec myWhile []

topics/exercises/while8/Makefile

@@ -1,10 +1,10 @@
 all:
-	ghc while.hs
-	./a.out
+	ghc --make Test.hs
+	./Test
 
 test:
-	ghci while.hs
+	ghci Test.hs
 
 clean:
-	rm -f *~ *.hi *.o a.out
+	rm -f *~ *.hi *.o Test