Module 11: IMP

In this module we are going to model a simple imperative language called IMP.

This module is due Tuesday, October 30.

The IMP language

The syntax of the language is as follows:

<prog> ::= <stmt> [ ';' <stmt> ]*

<stmt> ::=
  | <type> <var>
  | <var> ':=' <expr>
  | '{' <prog> '}'
  | 'if' <expr> 'then' <stmt> 'else' <stmt>
  | 'repeat' <expr> <stmt>
  | 'while' <expr> <stmt>
  | 'input' <var>
  | 'output' <expr>

<type> ::= 'int' | 'bool'

<expr> ::=
  | <int>
  | 'False' | 'True'
  | <var>
  | <uop> <expr>
  | <expr> <bop> <expr>

<uop> ::= '-' | '!'

<bop> ::= '+' | '-' | '*' | '/' | '&&' | '||' | '<' | '=='

Notice that the syntax is separated into expressions and statements. The difference is that

Most imperative languages have this distinction between expressions and statements (though some blur the line quite a bit).

Note that a <prog> consists of a sequence of statements, separated by (not ended by) semicolons. A compound statement can be created by surrounding a <prog> with curly braces.

Here is an example of a simple IMP program, which reads an integer from the user and then counts from 1 up to the integer, printing the values to the screen:

int max; int i;
input max;
i := 0;
while i < max {
  i := i + 1;
  output i
}

In order to focus on the parts that are interesting and different, this week I have provided you with some starter code. First, some imports we will need.

We now define algebraic data types for the abstract syntax of IMP. Note that we have two separate types, one for statements and one for expressions.

Parser

Now, a parser for IMP. You are welcome to skim through it, but there’s nothing really surprising going on.

lexer :: TokenParser u
lexer = makeTokenParser $
  emptyDef
  { reservedNames   = [ "True", "False", "if", "then", "else", "begin", "end"
                        , "repeat", "while", "input", "output", "int", "bool" ]
  , reservedOpNames = [ ":=", "==", "<", "+", "-", "*", "!", "&&", "||"  ]
  }

parens :: Parser a -> Parser a
parens = getParens lexer

reserved, reservedOp :: String -> Parser ()
reserved   = getReserved lexer
reservedOp = getReservedOp lexer

symbol :: String -> Parser String
symbol = getSymbol lexer

ident :: Parser String
ident = getIdentifier lexer

integer :: Parser Integer
integer = getInteger lexer

whiteSpace :: Parser ()
whiteSpace = getWhiteSpace lexer

parseAtom :: Parser Expr
parseAtom
  =   EInt        <$> integer
  <|> EBool True  <$  reserved "True"
  <|> EBool False <$  reserved "False"
  <|> EVar        <$> ident
  <|> parens parseExpr

parseExpr :: Parser Expr
parseExpr = buildExpressionParser table parseAtom
  where
    table = [ [ unary  "!"  (EUn Not) ]
            , [ unary  "-"  (EUn Neg) ]
            , [ binary "*"  (EBin Mul)    AssocLeft
              , binary "/"  (EBin Div)    AssocLeft ]
            , [ binary "+"  (EBin Add)    AssocLeft
              , binary "-"  (EBin Sub)    AssocLeft
              ]
            , [ binary "==" (EBin Equals) AssocNone
              , binary "<"  (EBin Less)   AssocNone
              ]
            , [ binary "&&" (EBin And)    AssocRight ]
            , [ binary "||" (EBin Or)     AssocRight ]
            ]
    unary  name fun       = Prefix (fun <$ reservedOp name)
    binary name fun assoc = Infix  (fun <$ reservedOp name) assoc

parseProg :: Parser Prog
parseProg = parseStmt `sepBy` (reservedOp ";")

parseStmt :: Parser Stmt
parseStmt =
      parseBlock
  <|> If      <$> (reserved "if" *> parseExpr)
              <*> (reserved "then" *> parseStmt)
              <*> (reserved "else" *> parseStmt)
  <|> Repeat  <$> (reserved "repeat" *> parseExpr) <*> parseBlock
  <|> While   <$> (reserved "while" *> parseExpr)  <*> parseBlock
  <|> Input   <$> (reserved "input" *> ident)
  <|> Output  <$> (reserved "output" *> parseExpr)
  <|> Assign  <$> ident <*> (reservedOp ":=" *> parseExpr)
  <|> Decl    <$> parseType <*> ident

parseType :: Parser Type
parseType = (TyInt <$ reserved "int") <|> (TyBool <$ reserved "bool")

parseBlock :: Parser Stmt
parseBlock = Block  <$> (symbol "{" *> parseProg <* symbol "}")

impParser :: Parser Prog
impParser = whiteSpace *> parseProg <* eof

Type checking expressions

Next, a static type checker. First, some errors:

Now let’s infer the type of expressions.

The binTy function gives the expected input types and the output type of each binary operator.

To infer the type of a binary operator application, e1 op e2, we ask for the type of the operator, check that e1 and e2 have the right types, then return the operator’s output type.

Inferring the type of a unary operator application is similar.

Finally, to check the type of an expression, we just infer its type and make sure it’s the type we wanted.

Type checking statements

Now it’s finally your turn to write some code! For checking programs, we just go through and check each statement. The interesting difference is that because statements can create variables, which are in scope for the rest of the program, both checkProg and checkStmt not only take a context as an argument but also return a new context as output.

And now for checkStmt, which checks an individual statement. Fill in all the undefined places below!

Now we come to checking blocks of the form { <prog> }. In one sense, this is easy, since we can just call checkProg. However, there is one subtle thing to think about. Here are two possible different implementations of this case, call them A and B:

(A) checkStmt ctx (Block ss)   = checkProg ctx ss >>= \ctx' -> Right ctx'

(B) checkStmt ctx (Block ss)   = checkProg ctx ss *> Right ctx

Checking if, repeat, and while is straightforward. Note that we take a similar approach to contexts as we did for blocks above. Take a look at the implementations of if and repeat, then fill in the implementation for while.

Checking input and output statements is straightforward: we can only input and output variables with type int.

You can use the below function to test your typechecking code. I have provided you with a few IMP programs for testing. all.imp should typecheck successfully; err1.imp through err5.imp should each generate an error. Be sure to test before moving on to the next section!

An IMPterpreter

Let’s define a Value to just be an Integer. As usual, if everything has type checked successfully, we can use Integer to represent both integers and booleans, without worrying about nonsensical operations.

A “memory” is a mapping from variable names to values. In the past we have called this an “environment”, but we use the name “memory” now to emphasize the fact that it keeps track of the values of mutable variables, which can be changed by assignment statements.

We interpret expressions as usual. There’s nothing very interesting to see here.

OK, now we have dealt with expressions. But how do we interpret statements?

Remember that an interpreter turns syntax into semantics, that is, it takes an abstract syntax tree and produces its meaning. So the question to ask ourselves is: what is the meaning of a statement?

The meaning of a statement is an effect: a statement changes the “state of the world” in some way. We can model this as a function which takes the current state of the world and produces a new state. That is, an interpreter for statements will have the type Stmt -> (World -> World) for some appropriate type World.

Programming in IMP

At this point, you should be able to compile this module (ghc --make 15-IMP.lhs) and then run it on input files containing IMP programs.

You should feel free to write other example IMP programs to test your implementation as well.

Extending IMP

Feedback

Some extra definitions (feel free to ignore)