definition module While

from StdOverloaded import class toString

:: Semantics = NS                           // Natural Semantics
             | SOS                          // Structural Operational Semantics

// evaluate @2 in state @3 according to @1
class eval a b :: Semantics a st -> b | toState st
instance eval Stm State
instance eval Int Int
instance eval Var Int
instance eval ArithExpr Int
instance eval Bool Bool
instance eval BoolExpr Bool

class toState a :: a -> State
instance toState State
instance toState CharState

instance toString ArithExpr
instance toString Bool
instance toString BoolExpr
instance toString Stm
instance toString Var
instance toString DerivTree
instance toString DerivSeq

// Syntax

:: Stm = Skip                                   // Skip
       | (:.) infixr 1 Stm Stm                  // Composition
       | E.a: (:=) infix 2 Var a                // Assignment
         & eval a Int & toString a
       | E.a: If a Stm Stm                      // If
         & eval a Bool & toString a
       | E.a: While a Stm                       // While
         & eval a Bool & toString a

:: Var = Var Char                               // Variable

:: ArithExpr = E.a b: (+) infixl 6 a b          // Addition
               & eval a Int & toString a & eval b Int & toString b
             | E.a b: (-) infixl 6 a b          // Subtraction
               & eval a Int & eval b Int & toString a & toString b
             | E.a b: (*) infixl 7 a b          // Multiplication
               & eval a Int & toString a & eval b Int & toString b

:: BoolExpr = E.a b: (==) infix 4 a b           // Equality on ArithExpr
               & eval a Int & toString a & eval b Int & toString b
            | E.a b: (<=) infix 4 a b           // Ord
               & eval a Int & toString a & eval b Int & toString b
            | E.a b: (>=) infix 4 a b
               & eval a Int & toString a & eval b Int & toString b
            | E.a b: (<) infix 4 a b
               & eval a Int & toString a & eval b Int & toString b
            | E.a b: (>) infix 4 a b
               & eval a Int & toString a & eval b Int & toString b
            | E.a: ~ a                          // Negation
               & eval a Bool & toString a
            | E.a b: (\/) infixr 4 a b          // Disjunction
               & eval a Bool & toString a & eval b Bool & toString b
            | E.a b: (/\) infixr 3 a b          // Conjunction
               & eval a Bool & toString a & eval b Bool & toString b

:: State :== Var -> Int
:: CharState :== Char -> Int

// Natural Semantics

:: DerivTree = { stm :: Stm
               , state :: State
               , children :: [DerivTree]
               , result :: State
               }

tree :: Stm st -> DerivTree | toState st // The deriv. tree for @1 in state @2

// Structural Operational Semantics

:: DerivSeqNode = Done State
                | NDone Stm State

:: DerivSeq :== [DerivSeqNode]

seq :: Stm st -> DerivSeq | toState st // The deriv. seq. for @1 in state @2