$Id: CoreLittleStep.lhs,v 1.9 1998/03/19 07:18:13 leavens Exp $

AUTHOR: Gary T. Leavens

A little-step operational semantics for the core language of
David A. Schmidt's "The Structure of Typed Programming Languages"
(MIT Press, 1994).

This is similar to, but not exactly the same as the semantics proposed
in exercise 8.4 in chapter 1 of Schmidt's book.
The use of the type attributes is not necessary, but makes this more similar
to the CoreSemantics module.

> module CoreLittleStep where
> import CoreLangParser  -- needs true and false as Expressions
> import CoreTyping
> import Domains


	CODING THE ONE-STEP RELATION

The little step semantic functions are stepE, stepC.
Numbers, Booleans, and Locations are values, that is, there is no way
to take further steps from an ATree Integer or an ATree Location.
Hence, we don't need stepN and stepL functions.
We use the meaning functions from the regular denotational semantics
as a way to getting and locations from the annotated syntax trees,
but we don't even need that for numbers or booleans.

> meaningL :: ATree Location -> DLocation
> meaningL (( (Loc i) ::: Node (Aloc Aint) _ )) = i


        STEPS FOR EXPRESSIONS

Note that expressions here can't have side effects.

> terminalE :: Expression -> Bool

> terminalE (Num n) = True
> terminalE (BoolLit b) = True
> terminalE _ = False

> stepE :: (ATree Expression, DStore) -> (ATree Expression, DStore)

> stepE (Deref l ::: Node (Aexp Aint) [atr], s) =
>   (Num (lookupStore (meaningL((l ::: atr)), s))
>      ::: Node (Aexp Aint) [Node Aint []], s)

> stepE (((Num i1) `Plus` (Num i2)) ::: Node (Aexp Aint) [at1, at2], s) =
>   (Num (plus(i1,i2)) ::: Node (Aexp Aint) [Node Aint []], s)
> stepE ((e1 `Plus` e2) ::: Node (Aexp Aint) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 =
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Plus` e2') ::: Node (Aexp Aint) [at1, at2'], s')
>   | otherwise =
>        let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>        in  ((e1' `Plus` e2) ::: (Node (Aexp Aint) [at1', at2]), s')

> stepE (Not (BoolLit b) ::: Node (Aexp Abool) [atr], s) =
>   (BoolLit (not b) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE (Not e ::: Node (Aexp Abool) [atr], s)
>   | terminalE e = error "type error"
>   | otherwise =
>        let (e' ::: atr', s') = stepE (e ::: atr, s)
>        in (Not e' ::: Node (Aexp Abool) [atr'], s')

> stepE (((Num i1) `Equals` (Num i2)) ::: Node (Aexp Abool) [at1, at2], s) =
>   (BoolLit (equalint(i1,i2)) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE (((BoolLit b1) `Equals` (BoolLit b2)) ::: Node (Aexp Abool) [at1, at2],
>        s) =
>   (BoolLit (equalbool(b1,b2)) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `Equals` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Equals` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `Equals` e2) ::: (Node (Aexp Abool) [at1', at2]), s')

> stepE (((Num n1) `Lt` (Num n2)) ::: Node (Aexp Abool) [at1, at2], s) =
>   (BoolLit (n1 < n2) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `Lt` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Lt` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `Lt` e2) ::: (Node (Aexp Abool) [at1', at2]), s')

> stepE (((Num n1) `Gt` (Num n2)) ::: Node (Aexp Abool) [at1, at2], s) =
>   (BoolLit (n1 > n2) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `Gt` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Gt` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `Gt` e2) ::: (Node (Aexp Abool) [at1', at2]), s')

> stepE (((Num n1) `Le` (Num n2)) ::: Node (Aexp Abool) [at1, at2], s) =
>   (BoolLit (n1 <= n2) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `Le` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Le` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `Le` e2) ::: (Node (Aexp Abool) [at1', at2]), s')

> stepE (((Num n1) `Ge` (Num n2)) ::: Node (Aexp Abool) [at1, at2], s) =
>   (BoolLit (n1 >= n2) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `Ge` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Ge` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `Ge` e2) ::: (Node (Aexp Abool) [at1', at2]), s')

> stepE (((BoolLit b1) `And` (BoolLit b2)) ::: Node (Aexp Abool) [at1, at2],
>        s) =
>   (BoolLit (b1 && b2) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `And` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `And` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `And` e2) ::: (Node (Aexp Abool) [at1', at2]), s')

> stepE (((BoolLit b1) `Or` (BoolLit b2)) ::: Node (Aexp Abool) [at1, at2],
>        s) =
>   (BoolLit (b1 || b2) ::: Node (Aexp Abool) [Node Abool []], s)
> stepE ((e1 `Or` e2) ::: Node (Aexp Abool) [at1, at2], s)
>   | terminalE e1 && terminalE e2 = error "type error"
>   | terminalE e1 = 
>        let (e2' ::: at2', s') = stepE (e2 ::: at2, s)
>        in  ((e1 `Or` e2') ::: Node (Aexp Abool) [at1, at2'], s')
>   | otherwise =
>       let (e1' ::: at1', s') = stepE (e1 ::: at1, s)
>       in  ((e1' `Or` e2) ::: (Node (Aexp Abool) [at1', at2]), s')


          STEPS FOR COMMANDS

The step of a command is a transformation from one store to another.

> terminalC :: Command -> Bool

> terminalC Skip = True
> terminalC _ = False

> stepC :: (ATree Command, DStore) -> (ATree Command, DStore)

> stepC ((l `Assign` (Num i)) ::: Node Acomm [atl, ate], s) =
>    (Skip ::: Node Acomm [], 
>     updateStore(meaningL((l ::: atl)), i, s))
> stepC ((l `Assign` e) ::: Node Acomm [atl, ate], s)
>    | terminalE e = error "type error"
>    | otherwise =
>        let (e' ::: ate', s') = stepE(e:::ate, s)
>        in  ((l `Assign` e') ::: Node Acomm [atl, ate'], s')

> stepC ((Skip `Semi` c2) ::: Node Acomm [at1, at2], s) =
>    (c2 ::: at2, s)
> stepC ((c1 `Semi` c2) ::: Node Acomm [at1, at2], s) =
>    let (c1' ::: at1', s') = stepC(c1:::at1, s)
>    in  ((c1' `Semi` c2) ::: Node Acomm [at1', at2], s')

> stepC ((If (BoolLit b) c1 c2) ::: Node Acomm [ate, at1, at2], s) =
>      if b then (c1 ::: at1, s)
>           else (c2 ::: at2, s)
> stepC ((If e c1 c2) ::: Node Acomm [ate, at1, at2], s)
>    | terminalE e = error "type error"
>    | otherwise =
>        let (e' ::: ate', s') = stepE(e:::ate, s)
>        in  ((If e' c1 c2) ::: Node Acomm [ate', at1, at2], s')

> stepC ((While e c) ::: t@(Node Acomm [ate, atc]), s) =
>       ((If e (c `Semi` (While e c)) Skip)
>         ::: Node Acomm [ate, Node Acomm [atc, t], Node Acomm []],
>        s)