infixr -->;

type T_var = int;

datatype Ty = tvar of T_var
            | --> of Ty * Ty;

type O_var = int;

type U_var = int;

datatype O_term = ovar of O_var
                | oabstr of O_var * O_term
                | oappl of O_term * O_term
                | u2o of U_deconst
and U_const     = uabstr of U_var * U_const
                | deconst of U_deconst
                | o2u of O_term
and U_deconst   = uvar of U_var
                | uappl of U_deconst * U_const;

val voidtype = tvar ~1;

val voidterm = ovar ~1;

fun pp_type (tvar tv) =
       "a" ^ (Int.toString tv)
  | pp_type (ty1 --> ty2) =
       "(" ^ (pp_type ty1) ^ " -> " ^ (pp_type ty2) ^ ")";

fun pp_o (ovar ov) =
       "x" ^ (Int.toString ov)
  | pp_o (oabstr (ov,ot)) =
       "(lla x" ^ (Int.toString ov) ^ " . " ^ (pp_o ot) ^ ")"
  | pp_o (oappl (ot1,ot2)) =
       "(" ^ (pp_o ot1) ^ " @@ " ^ (pp_o ot2) ^ ")"
  | pp_o (u2o ud) =
       pp_ud ud
and pp_uc (uabstr (uv,uc)) =
       "(la y" ^ (Int.toString uv) ^ " . " ^ (pp_uc uc) ^ ")"
  | pp_uc (deconst ud) =
       pp_ud ud
  | pp_uc (o2u ot) =
       pp_o ot
and pp_ud (uvar uv) =
       "y" ^ (Int.toString uv)
  | pp_ud (uappl (ud,uc)) =
       "(" ^ (pp_ud ud) ^ " @ " ^ (pp_uc uc) ^ ")";