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 `QuickCheck`

.

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.

- Write a version of I with semantics that evaluate the right-arguments of the expressions first, and use
`QuickCheck`

to test that the behaviour is the same. - Complete the
`QuickCheck`

, parsing and printing for*I*.

Site proudly generated by Hakyll

This work is licensed under a Creative Commons Attribution 4.0 International License