(*********************************************************************
stlc.ml

Type-checking simple typed lambda calculus as an example of using 
general abstraction types in Fresh O'Caml.

AM Pitts
10 June 2003

**********************************************************************)

type t;;

type vid = t name;;

type expr = 
    Vid of vid
  | Fn of <<vid * typ>>expr (* N.B. this type for Fn only makes sense 
			       because typ is "pure" *)
  | App of expr * expr
and typ = 
    Ground of string
  | Fun of typ * typ;;

exception NotTypeable;;

(* typeOf : <<(vid * typ) list>>expr -> typ *)
let rec typeOf config =
  match config with
      <<[]>>(Vid x) -> 
	raise NotTypeable
    | <<(x, t)::tyenv>>(Vid y) -> 
	if x = y 
	then t 
	else typeOf (<<tyenv>>(Vid y))
    | <<tyenv>>(Fn(<<(x,t)>>e)) -> 
	Fun(t, typeOf (<<(x,t)::tyenv>>e))
    | <<tyenv>>(App(e1,e2)) ->
	match typeOf (<<tyenv>>e1) with
	    Fun(t1,t2) -> 
	      if (typeOf(<<tyenv>>e2)) = t1
	      then t2
	      else raise NotTypeable
	  | _ -> raise NotTypeable;;

(* example *)

let nat = Ground "nat";;

let natfun = Fun(nat,nat);;

let x,f = (fresh:vid),(fresh:vid);;

let eval = Fn(<<(f,natfun)>>(
		Fn(<<(x,nat)>>(
		      App(Vid f, Vid x)))));;

typeOf (<<[]>>eval);;
	
(* end of stlc.ml *)