The top portion of the file contains datatype definitions of the simple language.

(* t ::= int | t -> t *)
datatype typ = Int | Fun of typ * typ

(* use strings to represent variables *)
type var = string

(* syntactic values; as discussed in class, we include variables
 * here -- even though the result of an evaluation must be closed
 * and, therefore, cannot be a variable *)
datatype value = Var of var	(* x *)
	       | Num of int	(* n *)
	       | Lam of var * typ * exp (* \x:t.e *)

(* expressions *)
and exp = Val of value		(* v *)
	| Suc of exp		(* succ(e) *)
	| Prd of exp		(* pred(e) *)
	| If0 of exp * exp * exp (* if0 e then e else e *)
	| App of exp * exp	 (* e e *)

(* We represent typing enironment as a (partial) function from 
 * variables to types: *)
type env = var -> typ option

(* The empty environment is a function that always returns NONE: *)
fun empty _ = NONE

(* \Gamma[x\mapsto v]: augmenting an environment with an additional
 * binding: *)
fun augment (gamma, x, v) y = if x = y then SOME v else gamma y

This is a partial function from expression to types. For ill-formed expressions, we return NONE. Fill your solution:

fun typecheck e =
    let (* split the work between values... *)

in (* a well-formed toplevel expression must type-check
    * in an empty environment: *)
    expty (empty, e)
end