diff --git a/ocaml/.gitignore b/ocaml/.gitignore new file mode 100644 index 0000000..85ffc0b --- /dev/null +++ b/ocaml/.gitignore @@ -0,0 +1,15 @@ +*.annot +*.cmo +*.cma +*.cmi +*.a +*.o +*.cmx +*.cmxs +*.cmxa + +# dune working directory +_build/ + +# merlin +.merlin diff --git a/ocaml/.ocamlinit b/ocaml/.ocamlinit new file mode 100644 index 0000000..6b39728 --- /dev/null +++ b/ocaml/.ocamlinit @@ -0,0 +1,5 @@ +#use "topfind";; +#require "core";; +#require "oUnit";; +#directory "_build";; +#load "hw02.cma";; diff --git a/ocaml/README.md b/ocaml/README.md new file mode 100644 index 0000000..4f77a6f --- /dev/null +++ b/ocaml/README.md @@ -0,0 +1,36 @@ +# hw02/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. diff --git a/ocaml/dune b/ocaml/dune new file mode 100644 index 0000000..bc9f7c6 --- /dev/null +++ b/ocaml/dune @@ -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)))) diff --git a/ocaml/dune-project b/ocaml/dune-project new file mode 100644 index 0000000..cd8d4e3 --- /dev/null +++ b/ocaml/dune-project @@ -0,0 +1 @@ +(lang dune 2.1) diff --git a/ocaml/hw03.ml b/ocaml/hw03.ml new file mode 100644 index 0000000..ae267f7 --- /dev/null +++ b/ocaml/hw03.ml @@ -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] +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] +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" + diff --git a/ocaml/hw03.sh b/ocaml/hw03.sh new file mode 100755 index 0000000..586ec91 --- /dev/null +++ b/ocaml/hw03.sh @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +dune runtest diff --git a/ocaml/test_hw03.ml b/ocaml/test_hw03.ml new file mode 100644 index 0000000..628f0e1 --- /dev/null +++ b/ocaml/test_hw03.ml @@ -0,0 +1,182 @@ +open OUnit2 + +(**********************************************************************) +(** {1 Utilities} *) + +let assert_invalid_arg: (unit -> 'a) -> unit = fun test -> + try + ignore (test ()); + assert_failure "expected an Invalid_argument exception" + with Invalid_argument _ -> () + | e -> raise e + +(**********************************************************************) +(** {1 Interface for Homework} *) + +module type HW03 = sig + type var = string + val pp_var : var -> string + + type num = int + val pp_num : num -> string + + type str = string + val pp_str : str -> string + + type typ = + | TNum + | TStr + | Nat + | Arr of typ * typ + | Unit + | Prod of typ * typ + | Void + | Sum of typ * typ + val pp_typ : typ -> string + + 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 + val pp_exp : exp -> string + + val is_val : exp -> bool + + type typctx + val pp_typctx : typctx -> string + + val emp : typctx + val lookup : typctx -> var -> typ option + val extend : typctx -> var -> typ -> typctx + + val exp_typ : typctx -> exp -> typ option + val subst : exp -> var -> exp -> exp + val eval : exp -> exp + val step : exp -> exp + val steps_pap : typ -> exp -> exp +end + +(**********************************************************************) +(** {1 Testing} *) + +module Make(HW: HW03) = struct + + (********************************************************************) + (** {2 Utilities} *) + + module F = Format + let pp_option (pp: 'a -> string): 'a option -> string = function + | None -> "None" + | Some a -> F.sprintf "Some @[%a@]" (fun () -> pp) a + + (********************************************************************) + (** {2 Expressions} *) + + open HW + + let num_1 = Num 1 + let num_2 = Num 2 + let plus_1_1 = Plus (num_1, num_1) + + (********************************************************************) + (** {2 Tests} *) + + let test_is_val: test = + "is_val" >::: + List.map + (fun (expected,e) -> + let lbl = F.sprintf "(is_val %s)" (pp_exp e) in + let (===) = assert_equal ~printer:string_of_bool in + lbl >:: (fun _ -> expected === is_val e)) + [ + true, num_1; + false, plus_1_1; + ] + + let test_exp_typ: test = + "exp_typ" >::: + List.map + (fun (expected,(gamma,e)) -> + let lbl = F.sprintf "(exp_typ %s %s)" + (pp_typctx gamma) (pp_exp e) + in + let (===) = assert_equal ~printer:(pp_option pp_typ) in + lbl >:: (fun _ -> expected === exp_typ gamma e)) + [ + Some TNum, (emp, num_1); + Some TNum, (emp, plus_1_1); + ] + + + let test_subst: test = + "subst" >::: [] + + let exp_rewrite_tester + (lblpre: string) + (f: exp -> exp): exp option * exp -> test = (fun (expected,e) -> + let lbl = F.sprintf "(%s %s)" lblpre (pp_exp e) in + let (===) = assert_equal ~printer:pp_exp in + lbl >:: (fun _ -> + match expected with + | None -> assert_invalid_arg (fun () -> f e) + | Some e' -> e' === f e)) + + let test_step: test = + "step" >::: + List.map + (exp_rewrite_tester "step" step) + [ ] + + let eval_tests: (exp option * exp) list = [ + Some num_1, num_1; + Some num_2, plus_1_1; + ] + + let test_eval: test = + "eval" >::: List.map (exp_rewrite_tester "eval" eval) eval_tests + + let test_steps_pap: test = + "steps_pap" >::: + List.fold_right + (fun ((_,e) as test) acc -> + match exp_typ emp e with + | None -> acc + | Some tau -> + let lblpre = "steps_pap " ^ (pp_typ tau) in + (exp_rewrite_tester lblpre (steps_pap tau) test) :: acc) + eval_tests + [] + + let tests = + "Hw03" >::: [ + test_is_val; + test_exp_typ; + test_subst; + test_step; + test_eval; + test_steps_pap; + ] +end + +let () = + let module TestHW = Make(Hw03) in + run_test_tt_main TestHW.tests