type kind = 
    ARROW of kind * kind
  | TYP

type tycon = 
  | TyVar of int
  | FUN
  | LIST
  | STRING

type typ = 
    TyForall of kind * typ
  | TyApp of tycon * typ list

type exp = 
  | AbsTm of typ * exp
  | Var of int
  | App of exp * exp
  | String of string
  | AbsTy of kind * exp
  | AppTy of exp * typ

type ttyp =
  | TTyFun of ttyp * ttyp
  | TTyList of ttyp
  | TTyString
  | TTyAny
  | TTyVar of int
  | TTyForall of ttyp

type texp =
  | TAbsTm of  ttyp * texp
  | TVar of int
  | TApp of texp * texp
  | TString of string
  | TLetTy of texp * texp
  | TCast of texp * ttyp

  | TAppTy of texp * ttyp
  | TAbsTy of texp

 
let (-->) x y = TyApp (FUN, [x;y])
let (--->) x y = TTyFun (x,y)

let rec trans_kind = function
    ARROW (k1,k2) -> (trans_kind k1 ---> trans_kind k2)
  | TYP -> (TTyForall TANY ---> TTyAny)

let rec trans_typ_arg_aux = function
    (* TyForall (k,ty) -> TAbsTm (trans_kind k, TAbsTy (trans_typ ty)) ??? *)
  | TyApp (TyVar tv, args) -> failwith "unreduced"
  | ty -> TAbsTm (trans_kind k, TAbsTy (trans_typ ty))failwith "unreduced"
  | 
let rec trans_typ_arg env = function
  | TyApp (FUN, []) -> 
      TAbsTm 
	(trans_kind TYP, 
	 TLetTy (TVar 0, 
		 TAbsTm 
		   (trans_kind TYP, 
		    TLetTy (TVar 0, 
			    TAbsTm 
			      (TTyForall TANY, 
			       TAppTy (TVar 0, TTyFun (TTyVar 0, TTyVar 1)))))))
  | TyApp (TyVar tv, args) -> 
      try List.assoc (tv,args) env 
      with Not_found -> failwith "trans_typ: unreduced type variable"
  | ty -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, trans_typ env ty))
(*
  | TyApp (STRING, []) -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, TTyString))
  | TyApp (FUN, [l;r]) -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, TTyFun (trans_typ l, trans_typ r)))
*)


let rec trans_typ env = function
    TyForall (k,ty) -> (trans_kind k ---> TTyAny)
  | TyApp (TyVar tv, args) -> 
      try List.assoc (tv,args) env 
      with Not_found -> failwith "trans_typ: unreduced type variable"
  | TyApp (FUN, [l;r]) -> TTyFun (trans_typ env l, trans_typ env r)
  | TyApp (STRING, []) -> TTyString
  | _ -> failwith "trans_typ: badly formed input type"


let rec trans_exp env = function
  | AbsTm (ty,e) -> TAbsTm(trans_typ ty, trans_exp e)
  | Var n -> TVar n
  | App (l,r) -> TApp(trans_exp l, trans_exp r)
  | String s -> TString s
  | AbsTy (k,e) -> TAbsTm(trans_kind k, reduce env e)
  | AppTy (tm,ty) -> TAppTy(trans_exp tm, trans_typ_arg env ty)


open Format;;


let rec pp_print_exp pps = function
    L e -> fprintf pps "\