(**************************************************************
 *         CS101: Homework 2 --- Types                        *
 **************************************************************)

(*
 * Introduce a type alias to make it more obvious which strings are meant
 * to be interpreted as variable names
 *)
type var = string

(*
 * Lambda-calculus types:
 *   t := int
 *     |  t -> t
 *)
type lc_type =
   TyInt
 | TyFun of lc_type * lc_type

(*
 * Lambda-calculus binary operations: +, -, *
 *)
type lc_binop =
   OpPlus
 | OpMinus
 | OpTimes

(*
 * Lambda-calculus expressions:
 *   e := n
 *     |  x
 *     |  e op e
 *     |  e e
 *     | lambda x: t. e
 *)
type lc_exp =
   ExpInt of int
 | ExpVar of var
 | ExpBinop of lc_binop * lc_exp * lc_exp
 | ExpApply of lc_exp * lc_exp
 | ExpLambda of var * lc_type * lc_exp

(*
 * Type errors:
 *   - "Expression e has type t1, but is used with type t2"
 *   - "Expression e of non-functional type t is used in a function position"
 *   - "Variable v is not bound"
 *)
type lc_error =
      ErrTypeMismatch of lc_exp * lc_type * lc_type
   |  ErrTypeFunApp of lc_exp * lc_type
   |  ErrUnknownVariable of var

exception LcError of lc_error
exception InternalError of string