HW 9  Classes and type structures

HW 9 
COSC 4780
1 An implementation of classes and type structures
In this assignment you will complete the interpreter (code provided) to support classes and records. You can study the code for details of the implementation. We point out some significant features in the discussion here.
1.1 Representing the type structures in ML
Recall the following types used in the specification of classes and types
structures.
θ ::= τ | τexp | comm | δ | δclass | πdec
δ ::= intloc | π
π ::= {i : θi}i∈I where I ⊆ Identif ier I finite
τ ::= int | bool
This is implemented in ML using a mutually recursive type as follows:
type types =
Int
| Bool
| Intexp
| Boolexp
| Command
| Type of delta
| Class of delta
| Dec of type assignment
and delta =
Intloc
| Pi of type assignment
and type assignment =
TA of ((string * types) list)
;;
1.2 Environments
Recall the semantics of the various types:
1
name
syntax
classes type of the meaning
integers θ, τ, [[int]] : Z
Booleans θ, τ [[bool]] : B
int expressions θ, τexp [[intexp]] : Store → Z
bool expressions θ, τexp, [[boolexp]] : Store → B
commands θ [[comm]] : Store → Store⊥
locations θ, δ [[intloc]] : Location
type assignments θ, δ, π [[{i : θi}i∈I ]] = {i : [[θi
]]}i∈I
class θ [[δclass]] : Store → ([[δ]] × Store)
Environments are used to bind identifiers to the meanings of the syntactic phrases they are bound to. Since different types have different meanings
associated with them we use an ML record to keep track of all of the environments. Environments are represented as ML functions of the correct
type.
type env = { int : string -> int;
bool : string -> bool;
intexp : string -> store -> int;
boolexp: string -> store -> bool;
command: string -> store -> store;
intloc : string -> loc;
pi : string -> env;
intloc class : string -> store -> (loc * store);
pi class : string -> store -> (env * store)
};;
For each of function in the environment we need a separate function to
update that part of the environment. Here’s one of them:
let update boolexp env (i, v) e =
{int = e.int;
bool = e.bool;
intexp = e.intexp;
boolexp = update (i,v) e.boolexp;
command = e.command;
intloc = e.intloc;
2
pi = e.pi;
intloc class = e.intloc class;
pi class = e.pi class
}
;;
1.3 Identifiers and their meanings
We add the following ML type to represent the syntactic class of identifierexpressions.
type identifier = Id of string | XId of identifier * string ;;
A useful operation on an identifier is to get the last part.
let lastId id =
match id with
Id i -> i
| XId (id,i) -> i
;;
Recall the semantics of the identifier-expressions:
[[π ` I : θ]] e = v where {I : v} ∈ e
[[π ` X.I : θ]] e = v
where {I : v} ∈ r and r = [[π ` X : π1 class]] e
We implement this in ML by first finding the environment to use. If the
identifier is of the form Id x then we use the current environment. If the
identifier is complex (of the form XId(id,i)) then we recursively find the
environment for id and use that to look up i. The following function finds
the correct environment to use.
let rec get lookup env id pi env err =
match id with
Id i -> env
| XId (id,i) ->
(match (type of identifier id pi) with
3
Type (Pi pi’) ->
(get lookup env
id (bar union ta pi’ pi) env err).pi (lastId id)
| -> raise (Failure
("meaning of " ^ err ^
": (-> get lookup env) - bad record id.")))
;;
If the identifier is complex, XId(id,i) then we compute the type of the
identifier using the current type assignment pi. The pi-environment is used
to hold the environments that map record fields to their meanings; thus, the
only possible type a for a well-typed record identifier id is Type(Pi pi’)
where pi’ is the type assignment for the record. From there we recursively
get the lookup environment for id using an updated type assignment π
0∪−π.
Since this function is used to compute the meanings for all types of identifiers, we pass a string err so that a useful error message can be printed if a
lookup fails.
Now, for each kind of environment we implement a meaning function for
identifiers of that type which uses get lookup env to find the environment
to lookup in. Here a a few of those functions; there is one for each instance
of the rule (where θ is replaced by a specific type.).
Here’s the rule for when θ is the type int.
[[π ` I : int]] e = k where {I : k} ∈ e
[[π ` X.I : int]] e = k
where {I : k} ∈ r and r = [[π ` X : π1 class]] e
And here is the corresponding ML code.
let meaning of int id id pi env =
let env’ = get lookup env id pi env "int id" in
env’.int (lastId id)
;;
The code is uniform – all the implementations are essentially identical;
though they differ in part of the environment they invoke and hence the
type of functions they return. Here are two more.
let meaning of pi id id pi env =
let env’ = get lookup env id pi env "pi id" in
4
env’.pi (lastId id)
;;
let meaning of intloc class id id pi env =
let env’ = get lookup env id pi env "intloc class id" in
env’.intloc class (lastId id)
;;
1.4 Type Structures and Declarations
Recall that the syntax for declarations and type structures defined mutually
recursively: var and class declarations are defined in terms of type structures
and the record type structure is defined using a declaration.
D ::= D1, D2 | D1; D2 | fun I=E | const I=N | proc I = C
| var I: T | class I=T
T ::= newint | record D end | X
Here is an ML implementation of this syntax class:
type declaration =
Var of string * type structure
| TClass of string * type structure
| Const of string * expression
| Fun of string * expression
| Proc of string * command
| Comma of declaration * declaration
| Semi of declaration * declaration
and type structure =
Newint
| Record of declaration
| X of identifier
;;
It is almost always the case that when a type is defined mutually recursively, the functions the operate on those types are also mutually recursive.
Following the semantic equations that define the meaning of a declarations
and those defining the meaning of type structures we implement the meaning functions mutually recursively. Since the meaning of a type structure
5
is has type ([[δ]] × Store) and [[δ]] = {intloc, π}, we will make two meaning
functions for type structures: meaning of newint for the intloc case and
meaning of record for the π case.
let rec meaning of declaration d pi env s =
match d with
Var (id, ts) ->
if is intloc class ts pi then
[ your code here]
else if is pi class ts pi then
[ your code here]
else
raise (Failure "meaning of declaration: bad class.")
| TClass(name,ts) ->
if is intloc class ts pi then
[ your code here]
else if is pi class ts pi then
[ your code here]
else
raise (Failure "meaning of declaration: bad class.")
| Const (id, e) -> ...
| Fun (id, e) -> ...
| Proc (id, c) -> ...
| Semi (d1,d2) -> ...
| Comma (d1,d2) -> ...
and meaning of newint t pi env s =
match t with
Newint -> allocate s
| Record -> raise (Failure "meaning of newint: records not intloc class.")
| X id -> meaning of intloc class id id pi env s
and meaning of record t pi env s =
match t with
Newint -> raise (Failure "meaning of record: newint not record class.")
| Record d -> meaning of declaration d pi env s
| X id -> meaning of pi class id id pi env s
;;
You need to implement the following semantic rules for the var and class
6
declarations. I have named the environment to add the binding to in the
left column.
intloc env [[π ` var I: T : {I : intloc} dec]] e s = h{I : l}, s0
i
where hl, s0
i = [[π ` T : intloc class]] e s
pi env [[π ` var I: T : {I : π1} dec]] e s = h{I : e}, s0
i
where he, s0
i = [[π ` T : π1 class]] e s
intloc class env [[π ` class I=T : {I : intloc class}dec]] e s = h{I : f}, si
where f t = [[π ` T : intloc class]] e t
pi class env [[π ` class I=T : {I : π1 class}dec]] e s = h{I : f}, si
where f t = [[π ` T : π1 class]] e t
Note that the type structures for intloc or intloc class environments are
newint or identifier expressions. Note that the type structures for π or
π class environments are records or identifier expressions.
7