definition module While

from StdOverloaded import class toString

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

// evaluate @arg2 in state @arg3 according to @arg1
class eval a b :: Semantics a State -> b

instance eval Stm State
instance eval Int Int
instance eval Var Int
instance eval ArithExpr Int
instance eval Bool Bool
instance eval BoolExpr Bool

instance toString ArithExpr
instance toString BoolExpr
instance toString Stm
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 :== 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: ~ a                          // Negation
               & eval a Bool & toString a
            | E.a b: (/\) infixr 3 a b          // Conjunction
               & eval a Bool & toString a & eval b Bool & toString b

:: State :== Var -> Int

// Natural Semantics

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

tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2

// Structural Operational Semantics

:: DerivSeqNode = Done State
                | NDone Stm State

:: DerivSeq :== [DerivSeqNode]

seq :: Stm State -> DerivSeq // The derivation seq. for @arg1 in state @arg2