Permalink
Browse files

assignment 9 reference solution

git-svn-id: https://slps.svn.sourceforge.net/svnroot/slps@762 ab42f6e0-554d-0410-b580-99e487e6eeb2
  • Loading branch information...
grammarware committed Jan 25, 2010
1 parent 42ce58a commit 548507734c81e9b6d3e466e274d5be57e433a243
@@ -11,6 +11,7 @@ while6 - While evaluation in Haskell (incomplete)
while7 - While evaluation in Haskell (complete, big step operational)
while8 - While execution in Haskell (complete, denotational)
ewhile - Extended While execution in Haskell (complete, denotational)
while_sign - sign detection in While (uses Nielson07 topic)
xml1 - a DCG parser for XML subset (elements only)
xml2 - a DCG parser for XML subset (elements and attributes)
@@ -0,0 +1,114 @@
module Solution9.Main (
module SemanticsLib.Boolean
, module SemanticsLib.Number
, module SemanticsLib.State
, module SemanticsLib.Domain
, module SemanticsLib.TT
, module SemanticsLib.Map
, module Solution9.Sign
) where
import qualified Prelude
import Prelude hiding (id, seq, (<=))
import qualified SemanticsLib.Map as Map
import While.AbstractSyntax
import While.Fold
import While.DenotationalSemantics.DirectStyle
import SemanticsLib.Boolean
import SemanticsLib.Number
import SemanticsLib.State
import SemanticsLib.Domain
import SemanticsLib.TT
import SemanticsLib.Map hiding (lookup, update)
import Solution9.Sign
import Data.Maybe
-- Semantic domains for analysis
type N = Sign
type B = TT
type S = Map Var N
type MA = S -> N
type MB = S -> B
type MS = S -> S
-- Algebra for state transformers
strafos :: STrafoAlg MS MB
strafos = STrafoAlg {
id = Prelude.id
, seq = flip (.)
, cond = \mb ms1 ms2 s ->
case mb s of
TT -> ms1 s
FF -> ms2 s
TopTT -> ms1 (leastState TT mb s)
`lub` ms2 (leastState FF mb s)
BottomTT -> bottom
, fix = (\s -> fromMaybe (error "Divergence detected!") . fixEq s)
}
-- Least feasible state for then/else branch
leastState :: B -> MB -> S -> S
leastState b f s
= lubs [ s' |
s' <- maps (keys s)
, s' <= s
, b <= f s'
, atomic (keys s) s'
]
-- Assembly of the semantics
whileAlg :: WhileAlg MA MB MS
whileAlg = ds ttBooleans
signNumbers
statesAsPOrdMaps
strafos
-- Assignment 9 solution
fixEq :: (Bottom x, Eq x, POrd x)
=> ((x -> x) -> x -> x) -> x -> Maybe x
fixEq f x = iterate (const bottom)
where
iterate r = let r' = f r in
if r x == r' x
then Just (r x)
else if r x <= r' x
then iterate r'
else Nothing
testOne
= Seq
(Assign "x" (Num 1))
(Seq
(Assign "y-1" (Sub (Var "x") (Num 1)))
(Seq
(Assign "x+1" (Add (Var "x") (Num 1)))
(Assign "(x+1)-1" (Sub (Var "x+1") (Num 1)))
)
)
testIf
= Seq
(Assign "x" (Num 5))
(Seq
(Assign "y" (Num 10))
(If
(Eq (Var "x") (Var "y"))
(Assign "z" (Num 1))
(Assign "z" (Num 0)))
)
main =
do
let xpos = Map.update "x" Zero bottom
print xpos
print $ foldStm whileAlg factorial xpos
print $ foldStm whileAlg testOne xpos
print $ foldStm whileAlg testIf xpos
@@ -0,0 +1,4 @@
[("x",Zero)]
[("x",Zero),("y",One)]
[("x",One),("y-1",Zero),("x+1",Pos),("(x+1)-1",ZeroPos)]
[("x",Pos),("y",Pos),("z",ZeroPos)]
@@ -0,0 +1,17 @@
i = -i:.:../../NielsonN07/Haskell:../../NielsonN07/Haskell/src
test:
make Main.test
cat Main.ref
%.test:
@echo Testing $*.hs
@ghci -v0 ${i} $*.hs < ../../NielsonN07/Haskell/include/Main.in > $*.out
@diff -b $*.out $*.ref
@rm $*.out
%.ghci:
ghci ${i} $*.hs
clean:
rm -rf *.out
@@ -0,0 +1,4 @@
If make fails, the most probable reason is that GCHi can’t find the Nielson07 sources. By default it is assumed that the whole SLPS is checked out – if that is not the case, modify Makefile to provide the correct path values.
If you have no Nielson07 sources at all, they can be obtained here:
svn co https://slps.svn.sourceforge.net/svnroot/slps/topics/NielsonN07
Oops, something went wrong.

0 comments on commit 5485077

Please sign in to comment.