***********************************************************************
* A CONTINUATION Semantics for Reynolds' SIL,                         *
* from Section 5.8 of the text.                                       *
* Also includes the "repeat" (Ex. 5.2), "catchin" (Ex. 5.3), and      *
* "catch" (Ex. 5.4) commands.                                         *
***********************************************************************

Written by Paul Hudak
October 24, 2007

Exercise 5.2 in Reynolds:
-------------------------

[[ Repeat c b ]] kt kf
  = [[ c ]] (\s -> if [[ b ]] s then kt s 
                   else [[ Repeat c b ]] kt kf s) kf
  = (\k -> [[ c ]] (\s -> if [[ b ]] s then kt s 
                                       else k  s) kf) 
    ([[ Repeat c b ]] kt kf)
  = Y f where
    f k = [[ c ]] (\s -> if [[ b ]] s then kt s 
                                      else k  s) kf

Exercise 5.3 in Reynolds:
-------------------------

[[ Fail ]]          kt kf = kf
[[ CatchIn c0 c1 ]] kt kf = [[ c0 ]] kt ([[ c1 ]] kt kf)

Note: to implement Ex 5.4 below, the failure continuation is extended
to a take a string (label) argument.  So to get both forms of failures
to work, we need to pass a string argument to kf above, and then test
for it in the CatchIn.  In other words:

[[ Fail ]]          kt kf = kf ""
[[ CatchIn c0 c1 ]] kt kf = [[ c0 ]] kt (\l-> if l="" then [[ c1 ]] kt kf
                                                      else kf l)

Exercise 5.4 in Reynolds:
-------------------------

For the direct semantics:

[[ FailWith l ]] s = <l,s>

[[ Catch l c0 c1 ]] s = 
   s',          if [[ c0 ]] s = s'
   <l',s'>,     if [[ c0 ]] s = <l',s'> and l /= l'
   [[ c1 ]] s', if [[ c0 ]] s = <l',s'> and l == l'

and furthermore the "lifting" functions need to be changed to
appropriately propagate the failure labels.  See the file
"SILDirect.lhs" for the details.

For the continuation semantics:

[[ FailWith l ]] kt kf = kf l

[[ Catch l c0 c1 ]] kt kf = [[ c0 ]] kt kf'
where kf' l' = [[ c1 ]] kt kf,  if l==l'
               kf l',           if l/=l'

> module SILCont where

SYNTAX
======

Syntax of integer expressions:

> data IntExp = 
>     EInt Integer		-- constants
>   | EVar Var			-- variables
>   | Neg IntExp		-- negation
>   | IntExp :+: IntExp		-- addition
>   | IntExp :-: IntExp		-- subtraction
>   | IntExp :*: IntExp		-- multiplication
>   | IntExp :/: IntExp		-- division
>   | IntExp `Rem` IntExp	-- remainder
>   deriving (Eq, Show)

Syntax of boolean expressions:

> data BoolExp =
>     TrueB | FalseB		-- constants
>   | IntExp :=:  IntExp	-- equality
>   | IntExp :/=: IntExp	-- inequality
>   | IntExp :<:  IntExp	-- less than
>   | IntExp :<=: IntExp	-- less than or equal
>   | IntExp :>:  IntExp	-- greater than
>   | IntExp :>=: IntExp	-- greater than or equal
>   | Not BoolExp		-- negation
>   | BoolExp :/\:  BoolExp	-- conjunction (and)
>   | BoolExp :\/:  BoolExp	-- disjunction (or)
>   | BoolExp :=>:  BoolExp	-- implication
>   | BoolExp :<=>: BoolExp	-- if and only if
>   deriving (Eq, Show)

Variables are just strings:

> type Var = String

Syntax of commands:

> data Command =
>     Skip
>   | Var := IntExp
>   | Command ::: Command
>   | If BoolExp Command Command
>   | While BoolExp Command
>   | Newvar Var IntExp Command
>   | For Var IntExp IntExp Command
>   | Output IntExp
>   | Input Var
>   | Repeat Command BoolExp
>   | Fail
>   | CatchIn Command Command
>   | FailWith Label
>   | Catch Label Command Command
>   deriving (Eq, Show)

Labels are just strings:

> type Label = String

Operator fixities (i.e. associativity and precedence):

> infixl 9 :*:, :/:, `Rem`
> infixl 8 :-:, :+:
> infix  7 :=:, :/=:, :<:, :>:, :<=:, :>=:
> infixl 6 :/\:
> infixl 5 :\/:
> infixr 4 :=>:
> infixr 3 :<=>:
> infix  2 :=
> infixl 1 :::

The above is just as defined in Reynolds, except that:
(a) The prefix operators (Neg and Not) are not included because they
    are just functions in Haskell, and thus always have higher precedence
    than any infix operator.
(b) Reynolds says that each infix operator should be left associative, 
    but I don't like that, so I made the following changes:
    (i)  I did not give the relational operators (:=:, :<:, etc.) ANY
         associativity, since it doesn't make sense to write, for 
         example, x :>: y :>: z.  Similarly, assignment should have no
         associativity since it doesn't make sense to write x := y := z.
    (ii) I think that implication should be RIGHT asssociative; i.e.
         a => b => c should be parsed as a => (b => c).

States
======

States map variables to integers:

> type Sigma = Var -> Integer

We can extend states using function variation:

> extend :: Sigma -> Var -> Integer -> Sigma
> extend s v i v' = if v == v' then i else s v'

So "extend s v i" is equivalent to "s [v:i]" in Reynolds.

Resumptions and Continuations
=============================

Resumptions mimick the recursive domain equation for Omega in the text:

> data Omega = Term  Sigma
>            | Abort Label Sigma
>            | Out Integer Omega
>            | In (Integer -> Omega)

Alternatively:

data SigmaHat = Term Sigma
              | Abort Sigma

data OmegaHat = T SigmaHat
              | Out Integer Omega
              | In (Integer -> Omega)

Continuations are defined as type synonyms:

> type ContT =          Sigma -> Omega
> type ContF = Label -> Sigma -> Omega

SEMANTICS
=========

Semantic function for integer expressions:

> intExp :: IntExp -> Sigma -> Integer
>
> intExp (EInt i)      s = i
> intExp (EVar v)      s = s v
> intExp (Neg e)       s = - intExp e s
> intExp (e1 :+: e2)   s = intExp e1 s + intExp e2 s
> intExp (e1 :-: e2)   s = intExp e1 s - intExp e2 s
> intExp (e1 :*: e2)   s = intExp e1 s * intExp e2 s
> intExp (e1 :/: e2)   s = intExp e1 s `div` intExp e2 s
> intExp (e1 `Rem` e2) s = intExp e1 s `rem` intExp e2 s

Semantic function for boolean expressions:

> boolExp :: BoolExp -> Sigma -> Bool
>
> boolExp TrueB  s = True
> boolExp FalseB s = False
> boolExp (e1 :=:  e2)  s = intExp e1 s == intExp e2 s
> boolExp (e1 :/=: e2)  s = intExp e1 s /= intExp e2 s
> boolExp (e1 :<:  e2)  s = intExp e1 s <  intExp e2 s
> boolExp (e1 :<=: e2)  s = intExp e1 s <= intExp e2 s
> boolExp (e1 :>:  e2)  s = intExp e1 s >  intExp e2 s
> boolExp (e1 :>=: e2)  s = intExp e1 s >= intExp e2 s
> boolExp (Not p)       s = not (boolExp p s)
> boolExp (p1 :/\:  p2) s = boolExp p1 s && boolExp p2 s
> boolExp (p1 :\/:  p2) s = boolExp p1 s || boolExp p2 s
> boolExp (p1 :=>:  p2) s = if boolExp p1 s then boolExp p2 s else True
> boolExp (p1 :<=>: p2) s = if boolExp p1 s then boolExp p2 s
>                           else not (boolExp p2 s)

Semantic function for commands:

> command :: Command -> ContT -> ContF -> ContT
> 
> command Skip            kt kf = kt
> command (v := e)        kt kf = \s -> kt (extend s v (intExp e s))
> command (c1 ::: c2)     kt kf = command c1 (command c2 kt kf) kf
> command (If b c1 c2)    kt kf = \s -> if boolExp b s 
>                                       then command c1 kt kf s
>                                       else command c2 kt kf s
> command (While b c)     kt kf = y f
>         where f kt' s = if boolExp b s then command c kt' kf s 
>                                        else kt s

Alternatively:
          where f kt' = cond b (command c kt' kf) kt
                cond b c a = \s -> if boolexp b s then c s else a s

> command (Newvar v e c)  kt kf = \s ->
>         command c (\s'   -> kt (extend s' v (s v))) 
>                   (\l s' -> kf l (extend s' v (s v)))
>                   (extend s v (intExp e s))
> command (For v e0 e1 c) kt kf =
>         command (Newvar v e0 
>                    (While (EVar v :<=: e1) 
>                           (c ::: v := EVar v :+: EInt 1))) kt kf
> command (Output i)      kt kf = \s -> Out (intExp i s) (kt s)
> command (Input v)       kt kf = \s -> In (\i -> kt (extend s v i))
> command (Repeat c b)    kt kf = y f
>         where f k = command c (\s -> if boolExp b s then kt s 
>                                                     else k  s) kf
> command (Fail)          kt kf = kf ""
> command (CatchIn c0 c1) kt kf = command c0 kt (\l-> 
>                                   if l=="" then command c1 kt kf 
>                                            else kf l)
> command (FailWith l)    kt kf = kf l
> command (Catch l c0 c1) kt kf = command c0 kt (\l'->
>				    if l==l' then command c1 kt kf
>                                            else kf l')

The fixpoint operator:

> y :: (a -> a) -> a
> y f = f (y f)

Test Harness
============

Initial state that maps all variables to zero:

> s0 :: Sigma
> s0 v = 0

A way to "print" resumption results.  The arguments to printRs are a
resumption, a list of program inputs, and a list of variables to be
displayed upon program termination.

> printRs :: Omega -> [Integer] -> [Var] -> String
>
> printRs (Term s)    is  vs = "Proper termination with bindings: " ++ 
>                              concat (zipWith (\v x-> v++":"++x++" ")
>                                              vs (map (show.s) vs))
> printRs (Abort l s) is  vs = "Uncaught exception with label: " ++ l
> printRs (Out i r)   is  vs = show i ++ " " ++ printRs r is vs
> printRs (In f)   (i:is) vs = printRs (f i) is vs
> printRs (In f)      []  vs = error "you screwed up"

A program testing function:

> test c vs = let r = command c Term Abort s0
>          in putStrLn (printRs r [10,9,8,0] vs)

Note that Term :: ContT and Abort :: ContF are the appropriate initial
success and failure continuations, respectively.

Sample Resumptions:

> r0 = Term s0
> r1 = Abort "TOP" s0
> r2 = Out 42 (Out 420 r0)
> r3 = Out 420 (In (\i-> Out i r0))

Some test SIL programs:

> fac :: Integer -> Command
> fac n = "v" := EInt n   :::
>         "r" := EInt 1   :::
>         While (EVar "v" :>: EInt 0)
>               ( "r" := EVar "r" :*: EVar "v" :::
>                 "v" := EVar "v" :-: EInt 1      ) :::
>         Output (EVar "r")

Diverging program:

> p0 :: Command
> p0 = While TrueB Skip

Input, output, and uncaught exception:

> p1 :: Command
> p1 = "x" := EInt 0 :::
>      Input "n"     :::
>      For "i" (EInt 1) (EVar "n") 
>          ( "x" := EVar "x" :+: EVar "i" :::
>            If (EVar "x" :=: EInt 36) Fail Skip :::
>            Output (EVar "x")
>          )

Repeat example:

> p2 :: Command
> p2 = Repeat
>        ( Input "n"     :::
>          Output (EVar "n") )
>        (EVar "n" :=: EInt 0)

CatchIn exception example:

> p3 :: Command
> p3 = CatchIn
>        ( "x" := EInt 42 :::
>          Fail           :::
>          "y" := EInt 42
>        )
>        ( "z" := EInt 42
>        ) :::
>      Output (EVar "x") :::
>      Output (EVar "y") :::
>      Output (EVar "z")

Catch exception example:

> p4,p4' :: Command
> p4  = Catch "cold" (Catch "cold" ("x" := EInt 42 ::: FailWith "cold")
>                                  ("y" := EInt 42))
>                    ("z" := EInt 42)
> p4' = Catch "cold" (Catch "flu"  ("x" := EInt 42 ::: FailWith "cold")
>                                  ("y" := EInt 42))
>                    ("z" := EInt 42)