-- $Id: CoreLangProgs.hs,v 1.4 1998/03/19 07:18:13 leavens Exp $

-- Gary T. Leavens

-- Test programs for the core language of Chapter 1 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 CoreLangProgs where
import Domains

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

progs :: [String]
progs = map fst progs_with_results

progs_with_results :: [(String, DStore -> DStore)]
progs_with_results =
 [
   ("loc 2 := @loc 1"
    , \ s -> updateStore(2,lookupStore(1,s),s)
   )
   ,
   ("loc 3 := 99"
    , \ s -> updateStore(3,99,s)
   )
   ,
   ("loc 2 := (1 + 2 + 3)"
    , \ s -> updateStore(2,6,s)
   )
   ,
   ("loc 3 := 3; \
    \while not (@loc 3 = 5)\
    \do loc 3 := @loc 3 + 1 \
    \od"
    , \s -> updateStore(3,5,s)
   )
   ,
   ("if @loc 3 = 5 then loc 1 := 99 else loc 2 := 999 fi; skip"
    , \s -> if lookupStore(3,s) == 5
            then updateStore(1,99,s)
            else updateStore(2,999,s)
   )
   ,
   ("if not (@loc 3 = @loc 3 + 2) then loc 1 := 99 else loc 2 := 999 fi; skip"
    , \s -> updateStore(1,99,s)
   )
   ,
   ("loc 3 := @loc 1 + 1; if @loc 3 = 0 then 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'
   )
   ,
   ("loc 2 := 1; if @loc 2 = 0 then skip else loc 1 := @loc 2 + 4 fi"
    , \s -> updateStore(1,5,updateStore(2,1,s))
   )
   ,
   ("loc 1 := 2; loc 2 := @loc 1 + 1; skip"
    , \s -> updateStore(2,3,updateStore(1,2,s))
   )
   ,
   ("while @loc 1 = 0 do loc 1 := 1 od"
    , \s -> updateStore(1,1,s)
   )
   ,
   ("if @loc 1 < @loc 2 and @loc 2 > @loc 1 then loc 3 := 4 else loc 3 := 5 fi"
    , \s -> let v1 = lookupStore(1,s)
                v2 = lookupStore(2,s)
            in if v1 < v2 && v2 > v1 then updateStore(3,4,s)
                                      else updateStore(3,5,s)
   )
   ,
   ("if @loc 1 <= @loc 2 or @loc 2 >= @loc 1 then loc 3 := 4 else loc 3 := 5 fi"
    , \s -> let v1 = lookupStore(1,s)
                v2 = lookupStore(2,s)
            in if v1 <= v2 || v2 >= v1 then updateStore(3,4,s)
                                       else updateStore(3,5,s)
   )
 ]

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

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