-- $Id: WhileNProgs.hs,v 1.5 1998/02/22 18:11:21 leavens Exp $

-- Gary T. Leavens

-- Test programs for the core language of Chapter 2 of
-- David A. Schmidt's "The Structure of Typed Programming Languages"
-- (MIT Press, 1994).  Many of these are taken from various examples
-- and exercises in the book.

module WhileNProgs where
import WhileNParser (Identifier)
import qualified Stores
import WhileNDomains

prog :: Int -> String
prog n = progs !! n

progs :: [String]
progs = map fst progs_with_results


progs_with_results :: [(String, DStore -> DStore)]
progs_with_results =
 let dv2int :: DenotableValue -> DInt
     dv2int (DVInt i) = i
     dv2int _ = error "type error"
     dv2loc :: DenotableValue -> DLocation
     dv2loc (DVLoc l) = l
     dv2loc _ = error "type error"
     dv2proc :: DenotableValue -> DStore -> DStore
     dv2proc (DVProc p) = p
     dv2proc _ = error "type error"
     dv2fun :: DenotableValue -> DStore -> ExpressibleValue
     dv2fun (DVFun f) = f
     dv2fun _ = error "type error"
     dv2class :: DenotableValue -> DStore -> (DenotableValue, DStore)
     dv2class (DVClass c) = c
     dv2class _ = error "type error"
 in
 [
   -- The first several tests below use the location syntax
   -- from the early part of the chapter.

   ("fun a = 1, fun b = @loc 1 = 0 in while b do loc 1 := a + 2 od"
    , \s -> let a s' = InInt 1
                b s' = InBool (lookupStore(1,s') == 0)
                w s' = let (InBool bval) = b s'
                       in if bval then let (InInt aval) = a s'
                                       in w(updateStore(1, aval + 2, s'))
                                  else s'
            in w s
   )
   ,
   ("fun a = @loc 1; fun b = a + 1 in while not(b = 2) do loc 1 := 1 od"
    , \s -> let a s' = InInt (lookupStore(1,s'))
                b s' = let (InInt aval) = a s'
		       in InInt (aval + 1)
                w s' = let (InInt bval) = b s'
                       in if not (bval == 2)
                            then updateStore(1, 1, s')
                            else s'
            in w s
   )
   ,
   ("fun f = @loc 1 + 1 in loc 1 := 0; loc 1 := f; loc 2 := 2 + f"
    , \s -> let f s' = InInt (lookupStore(1,s') + 1)
                s1 = updateStore(1, 0, s)
                s2 = let (InInt fval) = f s1
                     in updateStore(1, fval, s1)
                s3 = let (InInt fval) = f s2
                     in updateStore(2, 2 + fval, s2)
            in s3
   )
   ,
   ("alias x = loc 1 in x := 3"
   , \s -> let x = 1
               s1 = updateStore(x,3,s)
           in s1
   )
   ,
   ("alias x = loc 1 in loc 2 := @x"
   , \s -> let x = 1
               s1 = updateStore(2,lookupStore(x,s),s)
           in s1
   )
   ,
   ("(const a = 1, alias x = loc 1); fun f = @x + a; proc p = x := f \
     \in call p; x := a; call p"
   , \s -> let a = 1
               x = 1
               f s' = InInt (lookupStore(x,s') + a)
               p s'= let (InInt fval) = f s'
                     in updateStore(x,fval,s')
               s1 = p s
               s2 = updateStore(x, a, s1)
               s3 = p s2
           in s3
   )
   ,

   -- The following don't use the location syntax.

   ("var i:newint in i := @i"
   , \s -> let (i,s1) = allocateStore s
           in s1
   )
   ,
   ("var i:newint in i := 99"
   , \s -> let (i,s1) = allocateStore s
           in updateStore(i,99,s1)
   )
   ,
   ("var i:newint in i := (1 + 2 + 3)"
   , \s -> let (i,s1) = allocateStore s
           in updateStore(i,6,s1)
   )
   ,
   ("var k:newint \
          \in \
          \k := 3; \
          \while not (@k = 5) \
          \do k := @k + 1 \
          \ od"
    , \s -> let (k,s1) = allocateStore s
                w s' = if not(lookupStore(k,s') == 5)
		        then w(updateStore(k, lookupStore(k,s') + 1, s'))
		        else s'
	        in w s1
   )
   ,
   ("var i:newint; fun a = 1 in i := a"
    , \s -> let (i,s1) = allocateStore s
                a s' = InInt 1
            in let (InInt aval) = a s1
               in updateStore(i,aval,s1)
   )
   ,
   ("var i:newint; fun b = @i = 0 in i := 3; if b then skip else skip fi"
    , \s -> let (i,s1) = allocateStore s
                b s' = InBool (lookupStore(i,s') == 0)
                s2 = updateStore(i,3,s1)
                in let (InBool bval) = b s2
		   in if bval then s2 else s2
   )
   , 
   ("var i:newint; fun a = 1, fun b = @i = 0 in i := 0; while b do i := a od"
    , \s -> let (i,s1) = allocateStore s
                a s' = InInt 1
                b s' = InBool (lookupStore(i,s') == 0)
                s2 = updateStore(i,0,s1)
                w s' = let (InBool bval) = b s'
		       in if bval then let (InInt aval) = a s'
		                      in w(updateStore(i,aval,s'))
		                 else s'
            in w(s2)
   )
   ,
   ("var i:newint; var j:newint, fun f = @i + 1 \
    \in i := 0; i := f; j := 2 + f"
    , \s -> let (i,s1) = allocateStore s
                (j,s2) = allocateStore s1
                f s' = InInt (lookupStore(i,s') + 1)
                s3 = updateStore(i, 0, s2)
                s4 = let (InInt fval) = f s3
		     in updateStore(i, fval, s3)
                s5 = let (InInt fval) = f s4
		     in updateStore(j, 2 + fval, s4)
            in s5
   )
   ,
   ("var i:newint; proc p = if @i = 6 then skip else i := @i + 1; skip fi \
    \in i := 0; call p"
    , \s -> let (i,s1) = allocateStore s
                p s' = if lookupStore(i,s') == 6
                        then s'
                        else updateStore(i, lookupStore(i,s') + 1, s')
                s2 = updateStore(i, 0, s1)
            in p s2
   )
   ,
   ("var x:newint; var y:newint; proc p = y := @x+1 in x := 0; call p"
    , \s -> let (x,s1) = allocateStore s
                (y,s2) = allocateStore s1
                p s' = updateStore(y, lookupStore(x,s') + 1, s')
                s3 = updateStore(x, 0, s2)
            in p s3
   )
   ,
   
   ("var x:newint; var y:newint in x := 0; y := @x+ 1"
    , \s -> let (x,s1) = allocateStore s
                (y,s2) = allocateStore s1
                s3 = updateStore(x, 0, s2)
            in updateStore(y, lookupStore(x,s3) + 1, s3)
   )
   ,
   ("var a:newint; var b:newint; var c:newint in a := 0; b := @a + @c"
    , \s -> let (a,s1) = allocateStore s
                (b,s2) = allocateStore s1
                (c,s3) = allocateStore s2
                s4 = updateStore(a, 0, s3)
            in updateStore(b, lookupStore(a,s4) + lookupStore(c,s4), s4)
   )
   ,
   ("class m = newint; var a:m; var b:m; var c:newint in a := 0; b := @a + @c"
    , \s -> let m s' = let (l, s'') = allocateStore s'
                       in (DVLoc l, s'')
                (DVLoc a, s1) = m s
                (DVLoc b, s2) = m s1
                (c,s3) = allocateStore s2
                s4 = updateStore(a, 0, s3)
            in updateStore(b, lookupStore(a,s4) + lookupStore(c,s4), s4)
   )
   ,
   ("class r = record var x:newint, var y: newint end; \
    \var a:r; var b:r \
    \in a.x := 3; a.y := 4; b.x := @a.x + 1; b.y := @a.x + @b.x"
    , \s -> let r s' = let (x,s1r) = allocateStore s'
                           (y,s2r) = allocateStore s1r
		       in (DVModule [("x", DVLoc x), ("y", DVLoc y)], s2r)
                (DVModule a, s1) = r s
                (DVModule b, s2) = r s1
                s3 = updateStore(dv2loc(a `dot` "x"), 3, s2)
                s4 = updateStore(dv2loc(a `dot` "y"), 4, s3)
                s5 = updateStore(dv2loc(b `dot` "x"),
		                 lookupStore(dv2loc(a `dot` "x"), s4) + 1,
                                 s4)
                s6 = updateStore(dv2loc(b `dot` "y"),
		                 lookupStore(dv2loc(a `dot` "x"), s5) +
		                 lookupStore(dv2loc(b `dot` "x"), s5),
                                 s5)
            in s6
   )
   ,
   ("var a: newint; \
    \class r = record var c:newint; proc p = (c := @a+1) end; \
    \var f:r, var g:r \
    \in a := 6; call f.p; call g.p; f.c := @g.c + 2"
    , \s -> let (a,s1) = allocateStore s
                r s' = let (c,s1r) = allocateStore s'
                           p s'' = updateStore(c, lookupStore(a,s'') + 1, s'')
		       in (DVModule [("c", DVLoc c), ("p", DVProc p)], s1r)
                (DVModule f, s2) = r s1
                (DVModule g, s3) = r s2
                s4 = updateStore(a, 6, s3)
                s5 = dv2proc(f `dot` "p") s4
                s6 = dv2proc(g `dot` "p") s5
                s7 = updateStore(dv2loc(f `dot` "c"),
		                 lookupStore(dv2loc(g `dot` "c"), s6) + 2,
                                 s6)
            in s7
   )
   ,
   ("module m = {class k = newint; var a:k; proc p = a := 5}; \
    \var b:newint; \
    \import m \
    \in call p; b := @a"
    , \s -> let ([("m", DVModule m)], s1) =
                          let k s' = let (l,news) = allocateStore s'
                                     in (DVLoc l, news)
                              (DVLoc a, s1m) = k s
                              p s'' = updateStore(a, 5, s'')
		          in ([("m",
			        DVModule [("k", DVClass k), ("a", DVLoc a),
		                          ("p", DVProc p)])],
			      s1m)
                (b,s2) = allocateStore s1
                (DVClass k) = m `dot` "k"
                (DVLoc a) = m `dot` "a"
                (DVProc p) = m `dot` "p"
                s3 = p s2
                s4 = updateStore(b, lookupStore(a,s3), s3)
            in s4
   )
   ,
   ("module m = {class k = newint; var a:k; proc p = a := 5}; \
    \var b:newint \
    \in call m.p; b := @m.a"
    , \s -> let ([("m", DVModule m)], s1) =
                          let k s' = let (l,news) = allocateStore s'
                                     in (DVLoc l, news)
                              (DVLoc a, s1m) = k s
                              p s'' = updateStore(a, 5, s'')
		          in ([("m",
			        DVModule [("k", DVClass k), ("a", DVLoc a),
		                          ("p", DVProc p)])],
			      s1m)
                (b,s2) = allocateStore s1
		s3 = dv2proc(m `dot` "p") s2
                s4 = updateStore(b, lookupStore(dv2loc(m `dot` "a"), s3), s3)
            in s4
   )
   ,
   ("class k = newint; \
    \module s = {var a:k; fun f = @a+1}; \
    \module m = {import s; proc init = a := 0}; \
    \module n = {import s; proc succ = a := f} \
    \in call m.init; call n.succ"
    , \s0 -> let k s' = let (l,news) = allocateStore s'
                        in (DVLoc l, news)
	         ([("s", DVModule s)], s1) = 
		        let (DVLoc a, s2s) = k s0
                            f s' = InInt (lookupStore(a, s') + 1)
			in ([("s", DVModule [("a", DVLoc a), ("f", DVFun f)])],
                            s2s)
	         ([("m", DVModule m)], s2) = 
		        let (DVLoc a) = s `dot` "a"
                            (DVFun f) = s `dot` "f"
                            init s' = updateStore(a, 0, s')
			in ([("m", DVModule [("a", DVLoc a), ("f", DVFun f),
			                     ("init", DVProc init)])],
                            s1)
	         ([("n", DVModule n)], s3) = 
		        let (DVLoc a) = s `dot` "a"
                            (DVFun f) = s `dot` "f"
                            succ s' = let (InInt i) = f s'
			              in updateStore(a, i, s')
			in ([("n", DVModule [("a", DVLoc a), ("f", DVFun f),
			                     ("succ", DVProc succ)])],
                            s2)
                 s4 = dv2proc(m `dot` "init") s3
                 s5 = dv2proc(n `dot` "succ") s4
             in s5

   )
   ,
   ("class k = newint; var b: k; proc p = b := 0; \
    \var c: record var b:k; var k: newint; fun f = @k end \
    \in call p"
    , \s -> let k s' = let (l, s'') = allocateStore s'
                       in (DVLoc l, s'')
                (DVLoc b, s1) = k s
                p s' = updateStore(b, 0, s')
                (DVModule c, s2) = let (DVLoc b, s1c) = k s1
                                   in let (k, s2c) = allocateStore s1c
                                          f s' = InInt (lookupStore(k,s'))
                                      in (DVModule [("b", DVLoc b),
				                    ("k", DVLoc k),
                                                    ("f", DVFun f)],
                                          s2c)
                s3 = p s2
            in s3
   )
 ]

type_error_progs =
 [
   "var i:newint in i := true",
   "var i:newint in if not 2 then i := not(2 = 1) else skip fi",
   "var i:newint; fun B = i = 0 in i := 0; if B then skip else skip fi",
   "var i:newint, var i:newint in i := 1",
   "var i:newint; var i:newint in i := 1",
   "var i:newint in j := 0"
 ]

looping_progs =
 [
   "var i:newint n while 1 = 1 do i := 1 od"
 ]