diff --git a/ocaml/dune b/ocaml/dune index 70af005..8b2bac1 100644 --- a/ocaml/dune +++ b/ocaml/dune @@ -1,7 +1,11 @@ -(test - (name test_hw02) - (libraries base ounit2)) +(library + (name hw02) + (libraries base) + (inline_tests) + (preprocess (pps ppx_let ppx_inline_test ppx_sexp_conv ppx_compare)) +) (env (dev (flags (:standard -warn-error -A)))) + diff --git a/ocaml/hw02.ml b/ocaml/hw02.ml index 6944e8b..8a5f4ed 100644 --- a/ocaml/hw02.ml +++ b/ocaml/hw02.ml @@ -7,9 +7,11 @@ (**********************************************************************) (** {1 Utilities} *) -let unimp: string -> 'a = fun s -> failwith ("Unimplemented: " ^ s) +let unimp s = failwith ("Unimplemented: " ^ s) (**********************************************************************) + +module F = Format (** {1 Syntax} The pretty-printing functions @@ -20,21 +22,33 @@ let unimp: string -> 'a = fun s -> failwith ("Unimplemented: " ^ s) library. Using the {!Format} module is optional. *) -module F = Format -let pp_of_fmt (f: F.formatter -> 'a -> unit): 'a -> string = fun a -> - f F.str_formatter a; F.flush_str_formatter () +open Base + +type 'a fmt = F.formatter -> 'a -> unit + +type 'a pp = 'a -> string + +let pp_of_fmt fmt a = + fmt F.str_formatter a; + F.flush_str_formatter () + +type var = string [@@deriving sexp_of, compare, equal] + +let f_var : var fmt = F.pp_print_string + +let pp_var : var pp = fun x -> x + +type num = int [@@deriving sexp_of, compare, equal] -type var = string -let f_var = F.pp_print_string -let pp_var: var -> string = fun x -> x +let f_num : num fmt = F.pp_print_int -type num = int -let f_num = F.pp_print_int -let pp_num = string_of_int +let pp_num : num pp = Int.to_string -type str = string -let f_str = F.pp_print_string -let pp_str: str -> string = fun s -> s +type str = string [@@deriving sexp_of, compare, equal] + +let f_str : str fmt = F.pp_print_string + +let pp_str : str pp = fun s -> s type typ = | TNum @@ -45,10 +59,14 @@ type typ = | Prod of typ * typ | Void | Sum of typ * typ -let f_typ f = function +[@@deriving sexp_of, compare, equal] + +let rec f_typ f = function | TNum -> F.fprintf f "num" + | Arr (t1, t2) -> F.printf "%a -> %a" f_typ t1 f_typ t2 | _ -> unimp "f_typ" -let pp_typ: typ -> string = pp_of_fmt f_typ + +let pp_typ : typ -> string = pp_of_fmt f_typ type exp = | Var of var @@ -72,18 +90,22 @@ type exp = | InL of typ * typ * exp | InR of typ * typ * exp | Case of exp * var * exp * var * exp -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 +[@@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_var f x + | Num n -> f_num f 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 + +let pp_exp : exp pp = pp_of_fmt f_exp (**********************************************************************) (** {1 Values} *) -let is_val: exp -> bool = function +let is_val : exp -> bool = function | Num _ -> true | _ -> unimp "is_val" @@ -91,51 +113,105 @@ let is_val: exp -> bool = function (** {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 pp_typctx : typctx pp = fun _ -> "todo" + +let emp : typctx = () (* TODO: replace *) + +let lookup (gamma : typctx) (x : var) : typ option = unimp "lookup" -let rec exp_typ: typctx -> exp -> typ option = fun gamma -> +let extend (gamma : typctx) (x : var) (tau : typ) : typctx = unimp "extend" + +let rec exp_typ (gamma : typctx) : exp -> typ option = (* 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 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 (tau1 == TNum && tau2 == TNum) TNum + 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 +let subst (e' : exp) (x : var) : exp -> exp = function (* Be very careful with Var expressions. *) - | Var y when x = y -> unimp "subst" + | Var y when equal_var x y -> unimp "subst" | Var y -> unimp "subst" | _ -> unimp "subst" (**********************************************************************) (** {1 Evaluation} *) -let rec eval: exp -> exp = fun e -> +let rec eval 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 + | Plus (e1, e2) -> ( + match (eval e1, eval e2) with + | Num n1, Num n2 -> Num (n1 + n2) + | _ -> invalid_arg (pp_exp e) ) | _ -> unimp "eval" - + (**********************************************************************) (** {1 Reduction} *) -let step: exp -> exp = fun e -> unimp "step" -let steps_pap: typ -> exp -> exp = fun tau e -> unimp "step_pap" +let step (e : exp) : exp = unimp "step" + +let steps_pap (tau : typ) (e : exp) : exp = unimp "step_pap" + +(**********************************************************************) +(** {1 Tests} *) + +module Test = struct + (********************************************************************) + (** {2 Utilities} *) + + let pp_option (pp : 'a -> string) : 'a option -> string = function + | None -> "None" + | Some a -> F.sprintf "Some @[%a@]" (fun () -> pp) a + + (********************************************************************) + (** {2 Expressions} *) + + let num_1 = Num 1 + + let num_2 = Num 2 + + let plus_1_1 = Plus (num_1, num_1) + + (********************************************************************) + (** {2 Example Tests} *) + (* Write tests as below: `let%test "test name" = `*) + (* Run tests with `dune runtest` *) + + let%test "one is a val" = is_val num_1 + + let%test "plus is not a val" = not @@ is_val plus_1_1 + + let has_type gamma exp tau = + match exp_typ gamma exp with + | None -> false + | Some tau' -> equal_typ tau tau' + + let%test "num_1 : TNum" = has_type emp num_1 TNum + + let%test "plus_1_1 : TNum" = has_type emp plus_1_1 TNum + + let%test "num_1 --> num_1" = equal_exp num_1 (step num_1) + let%test "plus_1_1 -> num_2" = equal_exp num_2 (step plus_1_1) +end diff --git a/ocaml/test_hw02.ml b/ocaml/test_hw02.ml deleted file mode 100644 index d694e33..0000000 --- a/ocaml/test_hw02.ml +++ /dev/null @@ -1,181 +0,0 @@ -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 HW02 = 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 - | Rec of exp * var * var * exp * exp - | Lam of var * typ * exp - | Ap of exp * 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: HW02) = 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 = - "Hw02" >::: [ - test_is_val; - test_exp_typ; - test_subst; - test_step; - test_eval; - test_steps_pap; - ] -end - -let () = - let module TestHW = Make(Hw02) in - run_test_tt_main TestHW.tests