Simple Bool with Nat, Let, Records, Variants, Fix, Ref from Types and Programming Languages, simplified based on https://github.com/hsk/simpletapl

sb7.ml

type ty =
| TArrow of ty * ty
| TBool
| TNat
| TRecord of (string * ty) list
| TVariant of (string * ty) list
| TUnit
| TRef of ty

type exp =
| EVar of string
| EAbs of string * ty * exp
| EApp of exp * exp
| ETrue
| EFalse
| EIf of exp * exp * exp
| ENat of int
| EAdd of exp * exp
| EIsZero of exp
| ELet of string * exp * exp
| ERecord of (string * exp) list
| EProj of exp * string
| ETag of string * exp * ty
| ECase of exp * (string * (string * exp)) list
| EFix of exp
| ERef of exp
| EDeref of exp
| EAssign of exp * exp

let rec typeof env = function
| EVar var -> List.assoc var env
| EAbs(var, t1, e1) -> TArrow(t1, typeof ((var,t1)::env) e1)
| EApp(e1, e2) -> (match typeof env e1 with
   | TArrow(t11, t12) when typeof env e2 = t11 -> t12
   | TArrow _ -> failwith "parameter type mismatch"
   | _ -> failwith "non-arrow type in function position")
| ETrue | EFalse -> TBool
| EIf(e1,e2,e3) ->
  if typeof env e1 != TBool
    then failwith "guard of conditional not boolean"
    else
      let t2 = typeof env e2 in
      if typeof env e3 = t2 then t2
      else failwith "type mismatch in arms of conditional"
| ENat _ -> TNat
| EAdd(e1,e2) ->
  if typeof env e1 = TNat && typeof env e2 = TNat then TNat
  else failwith "non-nat argument(s) to add"
| EIsZero e ->
  if typeof env e = TNat then TBool
  else failwith "non-nat argument to iszero"
| ELet(var,e1,e2) -> typeof ((var, typeof env e1)::env) e2
| ERecord les -> TRecord (List.map (fun (l,e)->(l, typeof env e)) les)
| EProj(e,l) -> (match typeof env e with
    | TRecord(lts) -> List.assoc l lts
    | _ -> failwith "record type expected")
| ETag(l,e,t) -> (match t with
    | TVariant lts -> 
      let t' = List.assoc l lts in
      if typeof env e = t' then t
      else failwith "field does not have expected type"
    | _ -> failwith "annotation is not a variant type")
| ECase(e, cases) -> (match typeof env e with
    | TVariant lts ->
      let labels = List.map fst cases in
      let is_label_in_type l = List.mem_assoc l lts in
      if not (List.for_all is_label_in_type labels) then failwith "label mismatch between case and type";
      let typeof_case_exp (l,(var,exp)) = typeof ((var,List.assoc l lts)::env) exp in
      let ts = List.map typeof_case_exp cases in
      if not (List.for_all (fun t -> t = List.hd ts) ts) then failwith "type mismatch in arms of case";
      List.hd ts
    | _ -> failwith "variant type expected")
| EFix e -> (match typeof env e with
    | TArrow(t11,t12) when t11 = t12 -> t11
    | TArrow _ -> failwith "type mismatch between parameter and return of fix"
    | _ -> failwith "arrow type expected")
| ERef e -> TRef (typeof env e)
| EDeref e -> (match typeof env e with
    | TRef t -> t
    | _ -> failwith "non-ref passed to deref")
| EAssign(e1,e2) -> (match typeof env e1 with
    | TRef t when t = typeof env e2 -> TUnit
    | TRef _ -> failwith "type mismatch between ref and value"
    | _ -> failwith "ref type expected")