Project 1: OCaml Warmup

CMSC 430, Fall 2016

Due Wed, Sep 14, 2016 @ 11:59:59pm

This project will help refresh your memory on programming in OCaml by asking you to write two small modules and then develop test cases for them. You may find it helpful to review the OCaml slides from CMSC 330.

Here is the code skeleton for the project.

In this part of the project, you will develop some functions for working with boolean expressions and vectors of boolean expressions. We will use the following data type to represent boolean expressions:

type expr =
    EFalse
  | ETrue
  | EVar of string
  | EAnd of expr * expr
  | EOr of expr * expr
  | ENot of expr
  | EForall of string * expr
  | EExists of string * expr
Here EFalse and ETrue represent the obvious values. EVar s represents the boolean variable with name s. The constructors EAnd, EOr, and ENot represent boolean conjunction, disjunction, and negation, respectively. For example, the expression (a or b) and c could be represented as And(Or(Var "a", Var "b"), Var "c"). (We'll explain Forall and Exists in a moment.)

We will use associative lists, which are just lists of pairs, to assign truth values to variables:

type asst = (string * bool) list
Here if an asst contains the pair (s, b), then that assignment gives the variable represented by the string s the value b. When working with the type asst, you will find the functions List.assoc, List.mem_assoc, and related functions helpful. See the OCaml library documentation for more details.

You may assume for purposes of this project that whenever you work with an asst, variables on the left override variables on the right. E.g., the assignment ["a", true; "a", false] assigns true to Var "a".

The last two expressions, EForall and EExists, represent the similarly named quantifiers. The expression EForall(x,e) is true if e is true when x is true and when x is false. Similarly, EExists(x,e) is true if e is true either when x is true or when x is false.

However complex a boolean expression, it represents a single bit. We can put those bits together to represent integers using the following type:

type bvec = expr list (* low order bit at head of list *)
A bvec is a list of boolean expressions representing bits, with the low order bit at the head of the list. For example, we could represent the number 13 as [ETrue; EFalse; ETrue; ETrue]. Zero could be represented as [] or [EFalse] or [EFalse; EFalse], etc. An unknown 4-bit integer could be represented as [EVar "a"; EVar "b"; EVar "c"; EVar "d"].

You can find the definitions of the above types in boolean.mli, along with type signatures for several functions you must implement in boolean.ml:

If you've gotten this far, you've now built a (likely very slow) solver for part of bitvector arithmetic! Suppose we have:

let x = [EVar "a"; EVar "b"]
let y = [EVar "c"; EVar "d"]
let z = [EFalse; EFalse; ETrue]  (* 4 *)
Then we can use our solver to answer questions like:
sat (eq (add x y) z)  (* are there two, two-bit numbers that sum to 4? *)
sat (eq (add x x) z)  (* is there a two-bit number that, doubled, is 4? *)
etc. Cool!

Your next task is to implement a few functions related to Lambda calculus, which you learned about in CMSC 330. Below is an interface file lambda.mli. You must implement the last six of the listed functions in lambda.ml. (We've already implemented unparse for you.)

    type expr =
    | Var of string
    | Lam of string * expr
    | App of expr * expr

    val unparse : expr -> string

    val free_vars : expr -> string list
    val subst : string -> expr -> expr -> expr
    val beta : expr -> expr option
    val normal_form : expr -> expr
    val expr_of_int : int -> expr
    val add : expr -> expr -> expr
These functions should do the following:

Your last task is to write unit tests for parts 1 and 2 above, using OUnit. Put your test cases in the file test.ml, and be sure to add your test cases to the suites suite_boolean and suite_lambda, as appropriate. We will grade this part of the project by running your test cases against various correct and incorrect implementations. A test case will only be counted as correct if it passes a correct implementation and fails at least one incorrect implementation.

Put all your code in the code skeleton we have supplied, and upload your solution to the submit server. You can either upload your solution via the web interface, or you can run java -jar submit.jar in the project directory. Your code can use any OCaml standard library functions that you like.

Important note: On GRACE you should use the version of OCaml installed at

/afs/glue.umd.edu/class/fall2016/cmsc/430/0101/public/bin

Please post any questions you have about this on Piazza. You are welcome to install OCaml on your own machine, though we can't provide much support for that. We do recommend using opam to manage the installation process if you choose to do that. You can use opam to install both OCaml and OUnit

The Campus Senate has adopted a policy asking students to include the following statement on each assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this assignment." Consequently your program is requested to contain this pledge in a comment near the top.

Please carefully read the academic honesty section of the course syllabus. Any evidence of impermissible cooperation on projects, use of disallowed materials or resources, or unauthorized use of computer accounts, will be submitted to the Student Honor Council, which could result in an XF for the course, or suspension or expulsion from the University. Be sure you understand what you are and what you are not permitted to do in regards to academic integrity when it comes to project assignments. These policies apply to all students, and the Student Honor Council does not consider lack of knowledge of the policies to be a defense for violating them. Full information is found in the course syllabus---please review it at this time.

Web Accessibility