Assignment 4 type-checker for the language REC

CS 496: Homework Assignment 4

2 Assignment
In this assignment you are asked to extend the type-checker for the language REC with
references, pairs, lists and trees. The interpreter is provided for you. This assignment is
organized in four parts:
1. Part 1. Add type-checking for references.
2. Part 2. Add type-checking for pairs.
3. Part 3. Add type-checking for lists.
4. Part 4. Add type-checking for trees.
The new language including all these constructs will be called CHECKED PLUS.
3 Type-Checking References
One new grammar production, which is added to the parser for CHECKED PLUS, is needed
for the concrete syntax of expressions.
<Expression ::= ()
The concrete syntax of types must be extended so as to allow the typing rules described
below to be implemented. Two new productions are added, the one for unit and for ref:
1
<Type ::= int
<Type ::= bool
<Type ::= unit
<Type ::= ref(<Type)
<Type ::= (<Type - <Type)
The typing rules are:
Γ ` e :: t
Γ ` newref(e) :: ref(t)
Γ ` e :: ref(t)
Γ ` deref(e) :: t
Γ ` e1 :: ref(t) Γ ` e2 :: t
Γ ` setref(e1,e2) :: unit
Γ ` () :: unit
Note the use of the type unit, to indicate that the return result of the assignment operation
is not important.
3.1 Task
You have to update the code for the type checker by adapting the file checker.ml of the
CHECKED language to EXPLICIT-REFS so that type_of_expr can handle :
let rec type_of_expr : expr - texpr tea_result = function
2 ...
| Unit - return UnitType
4 ...
| NewRef (e) - error " Implement me!"
6 | DeRef (e) - error " Implement me!"
| SetRef (e1 , e2 ) - error " Implement me!"
Here are some examples:
1 # chk " let x = newref (0) in deref (x)";;
- : texpr Checked . ReM . result = Ok IntType
3 # chk " let x = newref (0) in x";;
- : texpr Checked . ReM . result = Ok ( RefType IntType )
5 # chk " let x = newref (0) in setref (x ,4)";;
- : texpr Checked . ReM . result = Ok UnitType
7 # chk " newref ( newref ( zero ?(0))) ";;
- : texpr Checked . ReM . result = Ok ( RefType ( RefType BoolType ))
9 # chk " let x = 0 in setref (x ,4) ";;
- : texpr Checked . ReM . result = Error " setref : Expected a reference type "
4 Pairs
4.1 Concrete syntax
Two new productions are added to the grammar of CHECKED PLUS:
2
<Expression ::= pair(<Expression,<Expression)
<Expression ::= unpair (<Identifier,<Identifier)=<Expression in <Expression
Some examples of programs using pairs follow:
pair (3 ,4)
2
pair ( pair (3 ,4) ,5)
4
pair ( zero ?(0) ,3)
6
pair ( proc (x: int ) { x - 1 }, 4)
8
proc (z:< int * int ) { unpair (x ,y )= z in x }
10
proc (z:< int * bool ) { unpair (x ,y )= z in pair (y ,x) }
12
let f = proc ( z:< int * bool ) { unpair (x ,y )= z in pair (y ,x) }
14 in (f pair (1 , zero ?(0)))
Note that the concrete syntax of the types is also extended with a new production:
<Type ::= int
<Type ::= bool
<Type ::= unit
<Type ::= ref(<Type)
<Type ::= (<Type - <Type)
<Type ::= <<Type * <Type
Regarding the behavior of these expressions they are clear. For example, the expression
(proc (z:<int*int) unpair (x,y)=z in x pair(2, 3)) is a function that given a pair of integers,
projects the first component of the pair.
4.2 Task
Add two new cases to the definition of the function type_of_expr in the file checker.ml:
let rec type_of_expr : expr - texpr tea_result = function
2 ...
| Pair (e1 , e2 ) - error " Implement me!"
4 | Unpair ( id1 , id2 ,e1 , e2 ) - error " Implement me!"
You first need to devise the appropriate typing rules!
Here are some examples:
# chk " pair (2 , 3)";;
2 - : texpr Checked . ReM . result = Ok ( PairType ( IntType , IntType ))
# chk "( proc (z:< int *int ) { unpair (x,y)=z in x} pair (2 , 3)) ";;
4 - : texpr Checked . ReM . result = Ok IntType
# chk "( proc (z:int ) { unpair (x,y)=z in x} pair (2 , 3)) ";;
6 - : texpr Checked . ReM . result = Error " unpair : Expected a pair type "
3
5 Lists
5.1 Concrete syntax
The concrete syntax for expressions should be extended with the following productions:
<Expression ::= emptylist <Type
<Expression ::= cons (<Expression, <Expression)
<Expression ::= null? (<Expression)
<Expression ::= hd (<Expression)
<Expression ::= tl (<Expression)
The concrete syntax for types includes one new production (the last one listed below):
<Type ::= int
<Type ::= bool
<Type ::= unit
<Type ::= ref(<Type)
<Type ::= (<Type - <Type)
<Type ::= <<Type * <Type
<Type ::= list(<Type)
The new type constructor is for typing lists. For example,
1. list(int) is the type of lists of integers
2. (int - list(int)) is the type of functions that given an integer produce a list of
integers.
Here are some sample expressions in the extended language. They are supplied in order to
help you understand how each constructor works.
# chk " emptylist int ";;
2 - : texpr Checked . ReM . result = Ok ( ListType IntType )
4 # chk " cons (1 , emptylist int )";;
- : texpr Checked . ReM . result = Ok ( ListType IntType )
6
# chk "hd( cons (1 , emptylist int ))";;
8 - : texpr Checked . ReM . result = Ok IntType
10 # chk "tl( cons (1 , emptylist int ))";;
- : texpr Checked . ReM . result = Ok ( ListType IntType )
12
# chk " cons ( null ?( emptylist int ), emptylist int )";;
14 - : texpr Checked . ReM . result =
Error " cons : type of head and tail do not match "
16
# chk " proc (x: int ) { proc (l: list (int )) { cons (x,l) } }";;
18 - : texpr Checked . ReM . result =
Ok ( FuncType ( IntType , FuncType ( ListType IntType , ListType IntType )))
Here are the typing rules:
4
5.2 Typing rules
Γ ` emptylist t :: list(t)
Γ ` e1 :: t Γ ` e2 :: list(t)
Γ ` cons(e1,e2) :: list(t)
Γ ` e :: list(t)
Γ ` tl(e) :: list(t)
Γ ` e :: list(t)
Γ ` hd(e) :: t
Γ ` e :: list(t)
Γ ` null?(e) :: bool
5.3 Task
Extend the type-checker to del with the new constructs:
1 let rec type_of_expr : expr - texpr tea_result = function
...
3 | EmptyList (t) - error " Implement me!"
| Cons (he , te ) - error " Implement me!"
5 | Null (e) - error " Implement me!"
| Hd (e ) - error " Implement me!"
7 | Tl (e ) - error " Implement me!"
6 Trees
6.1 Concrete syntax
The concrete syntax for expressions should be extended with the following productions:
<Expression ::= emptytree <Type
<Expression ::= node (<Expression, <Expression, <Expression)
<Expression ::= nullT? (<Expression)
<Expression ::= getData (<Expression)
<Expression ::= getLST (<Expression)
<Expression ::= getRST (<Expression)
The concrete syntax for types includes one new production (the last one listed below):
<Type ::= int
<Type ::= bool
<Type ::= unit
<Type ::= ref(<Type)
<Type ::= (<Type - <Type)
<Type ::= <<Type * <Type
<Type ::= list(<Type)
<Type ::= tree (<Type)
Here is a sample program that assumes you have implemented the append operation on
lists. Note that you will not be able to run this program unless you have extended the
5
interpreter to deal with lists and trees. This assignment only asks you to write the typechecker, not the interpreter. You are, of course, encouraged to write the interpreter too!
Here is another example. It should type-check with result Ok (ListType IntType) and
evaluate to Ok (ListVal [NumVal 1; NumVal 2; NumVal 3]):
letrec append ( xs : list ( int )): list ( int ) - list ( int ) =
2 proc ( ys : list ( int )) {
if null ?( xs )
4 then ys
else cons ( hd ( xs ) ,(( append tl ( xs )) ys ))
6 }
in
8 letrec inorder ( x: tree ( int )): list ( int ) =
if nullT ?( x)
10 then emptylist int
else (( append ( inorder getLST (x ))) cons ( getData ( x),
12 ( inorder getRST ( x ))))
in
14 ( inorder node (2 ,
node (1 , emptytree int , emptytree int ),
16 node (3 , emptytree int , emptytree int )))
6.2 Typing rules
Γ ` emptytree t :: tree(t)
Γ ` e1 :: t Γ ` e2 :: tree(t) Γ ` e3 :: tree(t)
Γ ` node(e1,e2,e3) :: tree(t)
Γ ` e :: tree(t)
Γ ` getData(e) :: t
Γ ` e :: tree(t)
Γ ` nullT?(e) :: bool
Γ ` e :: tree(t)
Γ ` getLST(e) :: tree(t)
Γ ` e :: tree(t)
Γ ` getRST(e) :: tree(t)
6.3 Task
Extend the type-checker to del with the new constructs:
let rec type_of_expr : expr - texpr tea_result = function
2 ...
| EmptyTree (t) - error " Implement me!"
4 | Node (de , le , re ) - error " Implement me!"
| NullT (t) - error " Implement me!"
6 | GetData (t ) - error " Implement me!"
| GetLST (t) - error " Implement me!"
8 | GetRST (t) - error " Implement me!"
Here are some sample expressions in the extended language. They are supplied in order
you to help you understand how each construct works.
# chk " emptytree int ";;
2 - : texpr Checked . ReM . result = Ok ( TreeType IntType )
4 # chk " nullT ?( node (1 , node (2 , emptytree int , emptytree int ), emptytree int ))";;
- : texpr Checked . ReM . result = Ok BoolType
6
6
# chk " getData ( node (1 , node (2 , emptytree int , emptytree int ), emptytree int ))";;
8 - : texpr Checked . ReM . result = Ok IntType
10 # chk " getLST ( node (1 , node (2 , emptytree int , emptytree int ), emptytree int ))";;
- : texpr Checked . ReM . result = Ok ( TreeType IntType )
7 Submission instructions
Submit a file named HW3 <SURNAME.zip through Canvas which includes all the source files
required to run the interpreter and type-checker. Your grade will be determined as follows,
for a total of 100 points:
Section Grade
Unit 5
Reference 15
Pair 20
List 30
Tree 30
7