binding.ml

type binding =
    NameBind
  | VarBind of ty

context.ml

type context = (string * binding) list

examples

lambda x:Bool. x; -> (lambda x:Bool. x) : Bool -> Bool


(lambda x:Bool->Bool. if x false then true else false)
  (lambda x:Bool. if x then false else true); -> true : Bool

main.ml

let rec process_command ctx cmd = match cmd with
    Eval(fi,t) ->
      let tyT = typeof ctx t in
      let t' = eval ctx t in
      printtm_ATerm true ctx t';
      print_break 1 2;
      pr ": ";
      printty tyT;
      force_newline();
      ctx

term.ml

type term =
    TmTrue of info
  | TmFalse of info
  | TmIf of into * term * term * term
  | TmVar of info * int * int
  | TmAbs of info * string * ty * term
  | TmApp of info * term * term

terms.bnf

t ::=                             terms:
      x                         variable
      \x:T .t                abstraction
      t t                    application


v ::=                            values:
      \x:T .t          abstraction value


T ::=                             types:
      T -> T           type of functions


Ⲅ ::=                          contexts:
      φ                    empty context
      Ⲅ, x:T      terms variable binding

ty.ml

type ty =
    TyTop
  | TyBot
  | TyArr ty * ty

typeof1.ml

let rec typeof ctx t =
  match t with
      TmTrue(_) ->
        TyBool
    | TmFalse(_) ->
        TyBool
    | TmIf(fi, t1, t2, t3) ->
        if (=) (typeof ctx t1) TyBool then
          let tyT2 = typeof ctx t2 in
            if (=) tyT2 (typeof ctx t3) then tyT2
            else error fi "arms of conditions have different types"
        else error fi "guard of conditional not a boolean"

typeof2.ml

let rec typeof ctx t =
  match t with
      TmVar(fi, i, _) ->
        getTypeFromContext fi ctx i
    | TmAbs(fi, x, tyT1, t2) ->
        let ctx' = addbinding ctx x (VarBind(tyT1)) in
        let tyT2 = typeof ctx' t2 in
          TyArr(tyT1, tyT2)
    | TmApp(fi, t2, t2) ->
        let tyT1 = typeof ctx t1 in
        let tyT2 = typeof ctx t2 in
          (match tyT1 with
               TyArr(tyT11, tyT12) ->
                 if (=) tyT2 tyT11 then tyT12
                 else error fi "parameter type mismatch"
             | _ -> error fi "arrow type expected")