-- $Id: Problem_2_2_a_Progs.hs,v 1.1 1998/02/15 06:27:23 leavens Exp $

-- Gary T. Leavens

-- Test programs for the core language of Chapter 1, for problem 2.2(a) 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 Problem_2_2_a_Progs where
import Domains  -- really should redefine this...

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

progs :: [String]
progs = map fst progs_with_results

progs_with_results :: [(String, DStore -> DStore)]
progs_with_results =
 [
   ("bool loc 1 := true"
    , \s -> error "semantics not ready yet")
   ,
   ("bool loc 1 := 1 = @int loc 2; bool loc 1 := not @bool loc 1"
    , \s -> error "semantics not ready yet")
   ,
   ("bool loc 1 := true; if @bool loc 1 then bool loc 1 := false else skip fi"
    , \s -> error "semantics not ready yet")
   ,
   ("int loc 2 := @int loc 1", \s -> updateStore(2,lookupStore(1,s),s))
   ,
   ("int loc 3 := 99", \s -> updateStore(3,99,s))
   ,
   ("int loc 2 := (1 + 2 + 3)", \s -> updateStore(2,6,s))
   ,
   ("int loc 3 := 3; \
    \while not (@int loc 3 = 5)\
    \do int loc 3 := @int loc 3 + 1 \
    \od",
    \s -> updateStore(3,5,s))
   ,
   ("if @int loc 3 = 5 then int loc 1 := 99 else int loc 2 := 999 fi; skip",
    \s -> if lookupStore(3,s) == 5
          then updateStore(1,99,s)
          else updateStore(2,999,s))
   ,
   ("if not (@int loc 3 = @int loc 3 + 2) then int loc 1 := 99 else int loc 2 := 999 fi; skip",
    \s -> updateStore(1,99,s))
   ,
   ("int loc 3 := @int loc 1 + 1; if @int loc 3 = 0 then int loc 2 := 1 else skip fi",
    \s -> let s' = updateStore(3,lookupStore(1,s)+1,s)
          in if lookupStore(3,s') == 0 then updateStore(2,1,s') else s')
   ,
   ("int loc 2 := 1; if @int loc 2 = 0 then skip else int loc 1 := @int loc 2 + 4 fi",
    \s -> updateStore(1,5,updateStore(2,1,s)))
   ,
   ("int loc 1 := 2; int loc 2 := @int loc 1 + 1; skip",
    \s -> updateStore(2,3,updateStore(1,2,s)))
   ,
   ("while @int loc 1 = 0 do int loc 1 := 1 od",
    \s -> updateStore(1,1,s))
 ]

type_error_progs =
 [
   "if not 2 then int loc 1 := not(2 = 1) else skip fi"
   ,
   "int loc 1 := true"
   ,
   "int loc 3 := true + 4"
   ,
   "if 3 then skip else skip fi; int loc 1 := 2"
   ,
   "int loc 3 := 4; while 0 do skip od; skip"
   ,
   "int loc 1 := @bool loc 2"
   ,
   "bool loc 1 := 3 + 4"
 ]

looping_progs =
 [
   "while 1 = 1 do int loc 1 := 1 od"
 ]