Version: 6
Last Modified: Mon Mar 4 11:55:23 CST 2013
Changes:
compare function to the signature for problem 1.4fold_left without using the rec
keyword. Do not use library functions other that those included by
default in Pervasives.ml; keywords should be sufficient.
Karma will be awarded for solutions that do not use
loops.(6 points)
merge_sort : ('a -> 'a -> int) ->'a list -> 'a list
with and without
refs. (merge_sort f xs uses the comparison
function f to sort the elements of xs
in ascending order.)
Ask yourself, which solution is more efficient?
Which is more parallelizable? (8 points)
For this problem, you will implement an interpreter for a simplified version of the OCaml language. Evaluation follows the environment model presented in class very closely.
We have provided a lexical analyzer and parser that can take a string
input, parse it as an OCaml program, and output an
abstract
syntax tree (AST) representing the code. The input program is
converted to a tree of type Ast.expr, defined in the
Ast module.
Your job will be to write functions for typechecking and evaluating the AST that is returned from the parser.
There is also a sixth type VUndef that is used internally
for creating recursive definitions and is not available to the
programmer. Take care to ensure that your interpreter never evaluates
an expression to VUndef (raise an exception instead). The following code, taken from ast.ml, declares
the type value. When an expression is evaluated successfully,
the resulting value is an entity of this type.
type value = | VUndef | VBool of bool | VInt of int | VNil | VCons of value * value | VClosure of ((value ref) IdMap.t) * id * expr
id, you could enter this into
the read-eval-print loop:
? let id = fun x -> xIf you wanted to make a recursive function, you could do something like this:
? let rec fact = fun n -> if n = 0 then 1 else n * fact (n - 1)Also notable: no unary arithmetic negation, no strings, and no tuples. Expressions have the following type: (from ast.ml)
(* expressions *) type expr = | Constant of constant | Cons of expr * expr | IfThenElse of expr * expr * expr | Let of id * expr * expr | LetRec of id * expr * expr | Plus of expr * expr | Minus of expr * expr | Mult of expr * expr | Divide of expr * expr | Mod of expr * expr | Gt of expr * expr | Lt of expr * expr | Ltq of expr * expr | Gtq of expr * expr | Neq of expr * expr | Eq of expr * expr | Not of expr | And of expr * expr | Or of expr * expr | Fun of id * expr | App of expr * expr | Var of id | Match of expr * ((pattern * expr) list)Overview of binary operators:
| Op | AST Name | Meaning |
|---|---|---|
| + | Ast.Plus | Integer addition |
| - | Ast.Minus | Integer subtraction |
| * | Ast.Mult | Integer multiplication |
| / | Ast.Divide | Integer division |
| mod | Ast.Mod | Integer modulus |
| = | Ast.Eq | Comparison (equality) |
| <> | Ast.Neq | Comparison (inequality) |
| < | Ast.Lt | Comparison (less than) |
| <= | Ast.Ltq | Comparison (less than or equal to) |
| > | Ast.Gt | Comparison (greater than) |
| >= | Ast.Gtq | Comparison (greater than or equal to) |
| && | Ast.And | Logical AND |
| || | Ast.Or | Logical OR |
| :: | Ast.Cons | Attach an item to front of list |
| Op | AST Name | Meaning |
|---|---|---|
| not | Ast.Not | Logical complement |
type pattern = | PConstant of constant | PVar of id | PCons of pattern * patternThis will allow us to deconstruct lists. If there is the possibility that a value does not match any of the patterns in a match expression, the pattern-matching is said to be inexhaustive. You do not need to perform any exhaustiveness checking or output examples of values which will not pattern match. You will still need to throw an exception if a value if found to not match any pattern.
(* type expressions *) type typ = | TBool | TInt | TList of typ | TVar of id | Arrow of typ * typAs you know, OCaml can infer the type of expressions. This is done through unification, which basically satisfies constraints on types through substitutions. (This problem set was based on the code at the bottom of that link, see acknowledgements). The first thing you need to do is implement the function
collect to collect the
constraints to be unified. Type inference works as follows:
| OCaml | Constraints |
|---|---|
| e1 :: e2 | type(e2) = type(e1) list |
| if e1 then e2 else e3 | type(e1) = bool, type(e2) = type(e3) |
| let [rec] x = e1 in e2 | type(x) = type(e1) |
| e1 [+|-|/|*|mod] e2 | type(e1) = type(e2) = int |
| e1 [<|<=|=|=>|>|<>] e2 | type(e1) = type(e2) |
| not e | type(e) = bool |
| e1 [&&|(||)] e2 | type(e1) = type(e2) = bool |
| e1 e2 | type(e1) = type(e2) -> type(e1 e2) |
| match e with p_i -> e_i | type(e) = type(p_i), type(e_i) = type(match e with p_i -> e_i) (There may be multiple p_i/e_i pairs of course) |
| p1 :: p2 | type(p2) = type(p1) list (where p1 and p2 are patterns) |
type substitution = (id * typ) listEach
id * typ pair represents a substitution
of an id for a typ.
Composing multiple substitutions has been implemented
already; you only need to complete the function unify_one.
Handling type variables is the interesting part of this function. If
neither of the types to be unified is a type variable then either
they are equal or they aren't: if they're equal then carry on merrily,
otherwise the program does not type check so throw an appropriate
exception. One subtlety: be sure to perform an occurs check
for comparing a type variable and a type that may contain that type
variable. For instance a constraint like 'a = 'a -> 'b would not pass the occurs check and you should raise an appropriate
exception. We have provided a function occurs which
may be useful here.
eval which takes
an expression and an environment and evaluates it to a value.
Refer to the lecture notes
here on the
environment model for more information on how this function
should work. One tricky part of writing this function
is evaluating let rec f = e1 in e2. This is where
VUndef comes in. You need a temporary value to
add to the environment f while evaluating e1. Once
you have evaluated e1, you have the desired value for f,
so update f to the right value and evaluate e2.
This trick is sometimes called Landin's knot. If e1 evaluates
to VUndef, throw an appropriate exception (Try
and find an expression that causes this to happen to test it!)
eval.
collect.
unify_one.
$ makeor
$ ./build.shor (Windows)
> build.batTo clean:
$ make cleanor
$ ./clean.shor (Windows)
> clean.bat
$ ./interpreter.exeor (Windows)
> interpreter.exeHowever, we recommend using either of the following (for linux, supports history)
$ rlwrap ./interpreter.exeor
$ ledit ./interpreter.exeTo load a file of definitions: (We recommend using rlwrap or ledit when loading a file as well.)
$ ./interpreter.exe <file>or (Windows)
> interpreter.exe <file>Exiting the interpreter:
? #quit
debug is provided in ast.ml. Set it to true
to get interesting feedback about what is going on during type inference. You
are free to add additional debugging print statements, but please
structure your code such that if this flag is set to false, only what we
have provided in repl.ml prints anything. Use debug_print
or write something similar. We have provided a library of functions for you to play with in lib.ml.
$ ./submit.shFor windows, run clean.bat and then zip up what's left. Make sure your code compiles.
Many thanks to Nate Foster and Andrew Myers for providing starter code for type inference. That code may be found here, and you may refer to it while implementing your type inference.