|
| 1 | +(** Homework 3 |
| 2 | +
|
| 3 | + E(PCF)PS: E (numbers and strings), PCF (primitive recursion), P (products), |
| 4 | + and S (sums). |
| 5 | +*) |
| 6 | + |
| 7 | +(**********************************************************************) |
| 8 | +(** {1 Utilities} *) |
| 9 | + |
| 10 | +let unimp: string -> 'a = fun s -> failwith ("Unimplemented: " ^ s) |
| 11 | + |
| 12 | +(**********************************************************************) |
| 13 | +(** {1 Syntax} |
| 14 | +
|
| 15 | + The pretty-printing functions |
| 16 | +
|
| 17 | + {C [pp_]{i typ}[ : ]{i typ}[ -> string] } |
| 18 | +
|
| 19 | + are defined here in terms of the {!Format} module in the standard |
| 20 | + library. Using the {!Format} module is optional. |
| 21 | +*) |
| 22 | + |
| 23 | +module F = Format |
| 24 | +open Base |
| 25 | + |
| 26 | +let pp_of_fmt (f: F.formatter -> 'a -> unit): 'a -> string = fun a -> |
| 27 | + f F.str_formatter a; F.flush_str_formatter () |
| 28 | + |
| 29 | +type var = string [@@deriving sexp_of, compare, equal] |
| 30 | +let f_var = F.pp_print_string |
| 31 | +let pp_var: var -> string = fun x -> x |
| 32 | + |
| 33 | +type num = int [@@deriving sexp_of, compare, equal] |
| 34 | +let f_num = F.pp_print_int |
| 35 | +let pp_num = Int.to_string |
| 36 | + |
| 37 | +type str = string [@@deriving sexp_of, compare, equal] |
| 38 | +let f_str = F.pp_print_string |
| 39 | +let pp_str: str -> string = fun s -> s |
| 40 | + |
| 41 | +type typ = |
| 42 | + | TNum |
| 43 | + | TStr |
| 44 | + | Nat |
| 45 | + | Arr of typ * typ |
| 46 | + | Unit |
| 47 | + | Prod of typ * typ |
| 48 | + | Void |
| 49 | + | Sum of typ * typ |
| 50 | + [@@deriving sexp_of, compare, equal] |
| 51 | +let f_typ f = function |
| 52 | + | TNum -> F.fprintf f "num" |
| 53 | + | _ -> unimp "f_typ" |
| 54 | +let pp_typ: typ -> string = pp_of_fmt f_typ |
| 55 | + |
| 56 | +type exp = |
| 57 | + | Var of var |
| 58 | + | Num of num |
| 59 | + | Str of str |
| 60 | + | Plus of exp * exp |
| 61 | + | Times of exp * exp |
| 62 | + | Cat of exp * exp |
| 63 | + | Len of exp |
| 64 | + | Let of exp * var * exp |
| 65 | + | Z |
| 66 | + | S of exp |
| 67 | + | IfZ of exp * var * exp * exp |
| 68 | + | Lam of var * typ * exp |
| 69 | + | Ap of exp * exp |
| 70 | + | Fix of var * typ * exp |
| 71 | + | Triv |
| 72 | + | Pair of exp * exp |
| 73 | + | PrL of exp |
| 74 | + | PrR of exp |
| 75 | + | Abort of typ * exp |
| 76 | + | InL of typ * typ * exp |
| 77 | + | InR of typ * typ * exp |
| 78 | + | Case of exp * var * exp * var * exp |
| 79 | + [@@deriving sexp_of, compare, equal] |
| 80 | +let pp_exp_sexp e = pp_of_fmt Ppx_sexp_conv_lib.Sexp.pp_hum (sexp_of_exp e) |
| 81 | +let rec f_exp f = |
| 82 | + function |
| 83 | + | Var x -> F.fprintf f "%a" f_var x |
| 84 | + | Num n -> F.fprintf f "%a" f_num n |
| 85 | + | Plus (e1,e2) -> F.fprintf f "(@[%a@ +@ %a@])" f_exp e1 f_exp e2 |
| 86 | + | _ -> unimp "f_exp" |
| 87 | +let pp_exp: exp -> string = pp_of_fmt f_exp |
| 88 | + |
| 89 | +(**********************************************************************) |
| 90 | +(** {1 Values} *) |
| 91 | + |
| 92 | +let is_val: exp -> bool = function |
| 93 | + | Num _ -> true |
| 94 | + | _ -> unimp "is_val" |
| 95 | + |
| 96 | +(**********************************************************************) |
| 97 | +(** {1 Typing} *) |
| 98 | + |
| 99 | +type typctx = unit (* TODO: replace *) |
| 100 | +let pp_typctx: typctx -> string = fun _ -> "todo" |
| 101 | + |
| 102 | +let emp: typctx = () (* TODO: replace *) |
| 103 | +let lookup: typctx -> var -> typ option = fun gamma x -> unimp "lookup" |
| 104 | +let extend: typctx -> var -> typ -> typctx = fun gamma x tau -> unimp "extend" |
| 105 | + |
| 106 | +let rec exp_typ: typctx -> exp -> typ option = fun gamma -> |
| 107 | + (* Open the Base.Option library for some convenience functions on |
| 108 | + options. Comment out the following line to remove the library |
| 109 | + dependency on Base. *) |
| 110 | + let open Base.Option in |
| 111 | + (* Let_syntax enables the syntax shown below in the "Times" case, |
| 112 | + which is similar to Haskell do notation. Plus and Times cases |
| 113 | + here are functionally identical, so just choose whichever monad |
| 114 | + syntax you're more comfortable with. |
| 115 | + *) |
| 116 | + let open Base.Option.Let_syntax in |
| 117 | + function |
| 118 | + | Num _ -> Some TNum |
| 119 | + | Plus (e1, e2) -> |
| 120 | + exp_typ gamma e1 >>= fun tau1 -> |
| 121 | + exp_typ gamma e2 >>= fun tau2 -> |
| 122 | + some_if (equal_typ tau1 TNum && equal_typ tau2 TNum) TNum |
| 123 | + | Times (e1, e2) -> |
| 124 | + let%bind tau1 = exp_typ gamma e1 in |
| 125 | + let%bind tau2 = exp_typ gamma e2 in |
| 126 | + some_if (equal_typ tau1 TNum && equal_typ tau2 TNum) TNum |
| 127 | + | _ -> unimp "exp_typ" |
| 128 | + |
| 129 | +(**********************************************************************) |
| 130 | +(** {1 Substitution} *) |
| 131 | + |
| 132 | +let subst: exp -> var -> exp -> exp = fun e' x -> |
| 133 | + function |
| 134 | + (* Be very careful with Var expressions. *) |
| 135 | + | Var y when equal_var x y -> unimp "subst" |
| 136 | + | Var y -> unimp "subst" |
| 137 | + | _ -> unimp "subst" |
| 138 | + |
| 139 | +(**********************************************************************) |
| 140 | +(** {1 Evaluation} *) |
| 141 | + |
| 142 | +let rec eval: exp -> exp = fun e -> |
| 143 | + match e with |
| 144 | + | Num _ -> e |
| 145 | + | Plus (e1, e2) -> |
| 146 | + begin match eval e1, eval e2 with |
| 147 | + | Num n1, Num n2 -> Num (n1 + n2) |
| 148 | + | _ -> invalid_arg (pp_exp e) |
| 149 | + end |
| 150 | + | _ -> unimp "eval" |
| 151 | + |
| 152 | +(**********************************************************************) |
| 153 | +(** {1 Reduction} *) |
| 154 | + |
| 155 | +let step: exp -> exp = fun e -> unimp "step" |
| 156 | +let steps_pap: typ -> exp -> exp = fun tau e -> unimp "step_pap" |
| 157 | + |
0 commit comments