Skip to content

Add partially-modernized ocaml hw03 harness #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 25, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions ocaml/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
*.annot
*.cmo
*.cma
*.cmi
*.a
*.o
*.cmx
*.cmxs
*.cmxa

# dune working directory
_build/

# merlin
.merlin
5 changes: 5 additions & 0 deletions ocaml/.ocamlinit
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#use "topfind";;
#require "core";;
#require "oUnit";;
#directory "_build";;
#load "hw02.cma";;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
#load "hw02.cma";;
#load "hw03.cma";;

36 changes: 36 additions & 0 deletions ocaml/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
# hw02/ocaml
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
# hw02/ocaml
# hw03/ocaml


This repository contains some minimal OCaml starter files for Homework Assignment 2.

```
.
├── hw03.ml a template for your submission (if you wish)
├── hw03.sh a minimal script to run tests
└── test_hw03.ml a template for your tests (if you wish)
```

1 directory, 6 files

## Dependencies

First, make sure you have `ocaml` and `opam` installed from your system's package manager. Then, you can install the build and library dependencies as follows:

```
opam install dune base ounit2
```

## Build and Run Tests

You can build and run tests as follows:

```
dune runtest
```

Or, the simple top-level script

```
./hw03.sh
```

simply calls the above.
9 changes: 9 additions & 0 deletions ocaml/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
(test
(name test_hw03)
(libraries base ounit2)
(preprocess (pps ppx_let ppx_sexp_conv ppx_compare))
)

(env
(dev
(flags (:standard -warn-error -A))))
1 change: 1 addition & 0 deletions ocaml/dune-project
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(lang dune 2.1)
157 changes: 157 additions & 0 deletions ocaml/hw03.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,157 @@
(** Homework 3

E(PCF)PS: E (numbers and strings), PCF (primitive recursion), P (products),
and S (sums).
*)

(**********************************************************************)
(** {1 Utilities} *)

let unimp: string -> 'a = fun s -> failwith ("Unimplemented: " ^ s)

(**********************************************************************)
(** {1 Syntax}

The pretty-printing functions

{C [pp_]{i typ}[ : ]{i typ}[ -> string] }

are defined here in terms of the {!Format} module in the standard
library. Using the {!Format} module is optional.
*)

module F = Format
open Base

let pp_of_fmt (f: F.formatter -> 'a -> unit): 'a -> string = fun a ->
f F.str_formatter a; F.flush_str_formatter ()

type var = string [@@deriving sexp_of, compare, equal]
let f_var = F.pp_print_string
let pp_var: var -> string = fun x -> x

type num = int [@@deriving sexp_of, compare, equal]
let f_num = F.pp_print_int
let pp_num = Int.to_string

type str = string [@@deriving sexp_of, compare, equal]
let f_str = F.pp_print_string
let pp_str: str -> string = fun s -> s

type typ =
| TNum
| TStr
| Nat
| Arr of typ * typ
| Unit
| Prod of typ * typ
| Void
| Sum of typ * typ
[@@deriving sexp_of, compare, equal]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This spacing looks a little funny?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
[@@deriving sexp_of, compare, equal]
[@@deriving sexp_of, compare, equal]

let f_typ f = function
| TNum -> F.fprintf f "num"
| _ -> unimp "f_typ"
let pp_typ: typ -> string = pp_of_fmt f_typ

type exp =
| Var of var
| Num of num
| Str of str
| Plus of exp * exp
| Times of exp * exp
| Cat of exp * exp
| Len of exp
| Let of exp * var * exp
| Z
| S of exp
| IfZ of exp * var * exp * exp
| Lam of var * typ * exp
| Ap of exp * exp
| Fix of var * typ * exp
| Triv
| Pair of exp * exp
| PrL of exp
| PrR of exp
| Abort of typ * exp
| InL of typ * typ * exp
| InR of typ * typ * exp
| Case of exp * var * exp * var * exp
[@@deriving sexp_of, compare, equal]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This spacing looks a little funny?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
[@@deriving sexp_of, compare, equal]
[@@deriving sexp_of, compare, equal]

let pp_exp_sexp e = pp_of_fmt Ppx_sexp_conv_lib.Sexp.pp_hum (sexp_of_exp e)
let rec f_exp f =
function
| Var x -> F.fprintf f "%a" f_var x
| Num n -> F.fprintf f "%a" f_num n
| Plus (e1,e2) -> F.fprintf f "(@[%a@ +@ %a@])" f_exp e1 f_exp e2
| _ -> unimp "f_exp"
let pp_exp: exp -> string = pp_of_fmt f_exp

(**********************************************************************)
(** {1 Values} *)

let is_val: exp -> bool = function
| Num _ -> true
| _ -> unimp "is_val"

(**********************************************************************)
(** {1 Typing} *)

type typctx = unit (* TODO: replace *)
let pp_typctx: typctx -> string = fun _ -> "todo"

let emp: typctx = () (* TODO: replace *)
let lookup: typctx -> var -> typ option = fun gamma x -> unimp "lookup"
let extend: typctx -> var -> typ -> typctx = fun gamma x tau -> unimp "extend"

let rec exp_typ: typctx -> exp -> typ option = fun gamma ->
(* Open the Base.Option library for some convenience functions on
options. Comment out the following line to remove the library
dependency on Base. *)
let open Base.Option in
(* Let_syntax enables the syntax shown below in the "Times" case,
which is similar to Haskell do notation. Plus and Times cases
here are functionally identical, so just choose whichever monad
syntax you're more comfortable with.
*)
let open Base.Option.Let_syntax in
function
| Num _ -> Some TNum
| Plus (e1, e2) ->
exp_typ gamma e1 >>= fun tau1 ->
exp_typ gamma e2 >>= fun tau2 ->
some_if (equal_typ tau1 TNum && equal_typ tau2 TNum) TNum
| Times (e1, e2) ->
let%bind tau1 = exp_typ gamma e1 in
let%bind tau2 = exp_typ gamma e2 in
some_if (equal_typ tau1 TNum && equal_typ tau2 TNum) TNum
| _ -> unimp "exp_typ"

(**********************************************************************)
(** {1 Substitution} *)

let subst: exp -> var -> exp -> exp = fun e' x ->
function
(* Be very careful with Var expressions. *)
| Var y when equal_var x y -> unimp "subst"
| Var y -> unimp "subst"
| _ -> unimp "subst"

(**********************************************************************)
(** {1 Evaluation} *)

let rec eval: exp -> exp = fun e ->
match e with
| Num _ -> e
| Plus (e1, e2) ->
begin match eval e1, eval e2 with
| Num n1, Num n2 -> Num (n1 + n2)
| _ -> invalid_arg (pp_exp e)
end
| _ -> unimp "eval"

(**********************************************************************)
(** {1 Reduction} *)

let step: exp -> exp = fun e -> unimp "step"
let steps_pap: typ -> exp -> exp = fun tau e -> unimp "step_pap"

2 changes: 2 additions & 0 deletions ocaml/hw03.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/usr/bin/env sh
dune runtest
Loading