We previously looked at the language N. Now we’re going to have a look at I, a language built around integer expressions.
The code for I is available here.
This will show how small-step semantics can be used to specify evaluation order, but will also give us some experience with more interesting parsers and pretty printers.
We will have terms for integer literals, as well as addition, subtraction, multiplication and exponentiation:
We’ll represent these terms in Haskell with:
data IntTerm tm = TmInt Int | TmAdd tm tm | TmSub tm tm | TmMul tm tm | TmExp tm tm
There is only one kind of values in I, the integer literals:
valueTmInt :: Term -> Maybe Term valueTmInt (TmInt i) = Just (TmInt i) valueTmInt _ = Nothing
Most of the steps have one reduction rule which does the required arithmetic:
eAddIntInt :: Term -> Maybe Term eAddIntInt (TmAdd (TmInt i1) (TmInt i2)) = Just (TmInt (i1 + i2)) eAddIntInt _ = Nothing
and two congruence rules that control the evaluation order.
The first of the congruence rules causes the left-most argument to take a step:
eAdd1 :: (Term -> Maybe Term) -> Term -> Maybe Term eAdd1 step (TmAdd tm1 tm2) = TmAdd <$> step tm1 <*> pure tm2 eAdd1 _ _ = Nothing
and the second rule causes the right-most argument to take a step whenever the left-most argument is a value:
We’re using the variables names to represent values as a convenient shorthand, however we could have written the rule as:
which better matches the Haskell version we have:
eAdd2 :: (Term -> Maybe Term) -> Term -> Maybe Term eAdd2 step (TmAdd tm1 tm2) = TmAdd <$> value tm1 <*> step tm2 eAdd2 _ _ = Nothing
The semantics for subtraction:
and for multiplication:
are defined similarly.
Exponentiation is a little different. The congruence rules follow the familiar pattern, but we have two reduction rules.
We can’t work with negative exponents of integers and continue to get integer results, so we define different rules for the cases of negative and non-negative exponents:
To be honest, I wrote the first version of I very late at night, and the semantics and associated code was written mostly by muscle memory. This is just one of the things that
QuickCheck caught while I was trading sleep for talk preparation.
At this point we can turn the handle to write the code we need to test this with
The parsing and printing code will be a bit more challenging. Fortunately there are some great libraries for this, which is where we’re going next.
QuickCheckto test that the behaviour is the same.
QuickCheck, parsing and printing for I.