diff options
Diffstat (limited to 'While.dcl')
| -rw-r--r-- | While.dcl | 25 |
1 files changed, 19 insertions, 6 deletions
@@ -5,9 +5,8 @@ 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 - +// 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 @@ -15,9 +14,14 @@ 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 BoolExpr instance toString Stm +instance toString Var instance toString DerivTree instance toString DerivSeq @@ -32,7 +36,7 @@ instance toString DerivSeq | E.a: While a Stm // While & eval a Bool & toString a -:: Var :== Char // Variable +:: Var = Var Char // Variable :: ArithExpr = E.a b: (+) infixl 6 a b // Addition & eval a Int & toString a & eval b Int & toString b @@ -45,12 +49,21 @@ instance toString DerivSeq & 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 @@ -60,7 +73,7 @@ instance toString DerivSeq , result :: State } -tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2 +tree :: Stm st -> DerivTree | toState st // The deriv. tree for @1 in state @2 // Structural Operational Semantics @@ -69,5 +82,5 @@ tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2 :: DerivSeq :== [DerivSeqNode] -seq :: Stm State -> DerivSeq // The derivation seq. for @arg1 in state @arg2 +seq :: Stm st -> DerivSeq | toState st // The deriv. seq. for @1 in state @2 |