Skip to content

Modernize assignment with PPX rewriters #2

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.

Sign up for GitHub

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

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Modernize assignment with PPX rewriters #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 7 additions & 3 deletions ocaml/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))))

162 changes: 119 additions & 43 deletions ocaml/hw02.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -72,70 +90,128 @@ 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"

(**********************************************************************)
(** {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" = <boolean>`*)
(* 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
Loading