load "Int";

infixr -->;

val counter = ref 0;

fun newindex () = let val _ = counter := !counter + 1
                   in !counter
                  end;

fun setcounter n = counter := n;   

type T_var = int;

datatype Ty = tvar of T_var
            | --> of Ty * Ty
            | all of T_var * 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
                | oTabstr of T_var * O_term
                | oTappl of O_term * Ty
                | u2o of U_deconst * T_var
and U_const     = uabstr of U_var * U_const
                | uTabstr of T_var * U_const
                | deconst of U_deconst
                | o2u of O_term * T_var
and U_deconst   = uvar of U_var
                | uappl of U_deconst * U_const
                | uTappl of U_deconst * Ty;

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

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 (oTabstr (tv,ot)) = 
       "(LLA a" ^ (Int.toString tv) ^ " . " ^ (pp_o ot) ^ ")"
  | pp_o (oTappl (ot,ty)) = 
       "(" ^ (pp_o ot) ^ " ## " ^ (pp_type ty) ^ ")"
  | pp_o (u2o (ud,tv)) = 
       pp_ud ud
and pp_uc (uabstr (uv,uc)) = 
       "(la y" ^ (Int.toString uv) ^ " . " ^ (pp_uc uc) ^ ")"
  | pp_uc (uTabstr (tv,uc)) = 
       "(LA a" ^ (Int.toString tv) ^ " . " ^ (pp_uc uc) ^ ")"
  | pp_uc (deconst ud) = 
       pp_ud ud
  | pp_uc (o2u (ot,tv)) = 
       pp_o ot
and pp_ud (uvar uv) =
       "y" ^ (Int.toString uv)
  | pp_ud (uappl (ud,uc)) = 
       "(" ^ (pp_ud ud) ^ " @ " ^ (pp_uc uc) ^ ")"
  | pp_ud (uTappl (ud,ty)) = 
       "(" ^ (pp_ud ud) ^ " # " ^ (pp_type ty) ^ ")";
  
datatype Envval = envval of O_term * (int -> Envval) * (int -> Ty);

val voidtype = tvar ~1;

val voidterm = ovar ~1;

exception unbound_variable of string;

exception ill_formed_term_or_wrong_type of string;
                                        
val init_env = (fn var => raise unbound_variable ("- " ^(Int.toString var)));

fun aug_env tenv var closure = 
  (fn var2 => if var=var2 
   then closure
   else (tenv var2) handle unbound_variable str 
                   => raise unbound_variable ((Int.toString var) ^ " " ^ str));

fun type_subst (tvar var) type_env =
      ((type_env var)
       handle unbound_variable str => (tvar var))
  | type_subst (t1 --> t2) type_env =
      (type_subst t1 type_env) --> (type_subst t2 type_env)
  | type_subst (all (tv,t)) type_env =
      let val tv1 =newindex()
       in (all (tv1,(type_subst t (aug_env type_env tv (tvar tv1)))))
      end;

fun down (tvar var) e = 
      o2u (e,var)
  | down (t1 --> t2) e =
      let val var = newindex()
       in uabstr (var,(down t2 (oappl (e, up t1 (uvar var)))))
      end 
  | down (all (v, t)) e =
      let val v1 = newindex()
          val t1 = type_subst t (aug_env init_env v (tvar v1))                
       in uTabstr (v1, down t1 (oTappl (e, tvar v1)))
      end   
and up (tvar var) d = 
      u2o (d,var)
  | up (t1 --> t2) d =
      let val var = newindex()
       in oabstr (var,(up t2 (uappl (d, down t1 (ovar var)))))
      end
  | up (all (v, t)) d =
      let val v1 = newindex()
          val t1 = type_subst t (aug_env init_env v (tvar v1))
       in oTabstr (v1, up t1 (uTappl (d, (tvar v1))))
      end;

fun o_eval (ovar ov) term_env type_env =
      let val envval (ot,term_env1,type_env1) = (term_env ov) 
       in o_eval ot term_env1 type_env1
      end 
  | o_eval (oabstr (ov,ot)) term_env type_env =
      ((oabstr (ov,ot)),term_env,type_env)
  | o_eval (oappl (ot1,ot2)) term_env type_env =
      (let val (ot3,term_env1,type_env1) = o_eval ot1 term_env type_env 
        in (case ot3
             of (oabstr (ov,ot4))
                  => o_eval ot4 
                            (aug_env term_env1 ov (envval (ot2,term_env,type_env))) 
                            type_env1
              | _ => raise ill_formed_term_or_wrong_type ((pp_o ot3) 
                             ^ " -- excepted abstraction at fct type"))
       end)
  | o_eval (oTabstr (tv,ot)) term_env type_env =
      ((oTabstr (tv,ot)),term_env,type_env)
  | o_eval (oTappl (ot,ty)) term_env type_env =
      (let val (ot1,term_env1,type_env1) = o_eval ot term_env type_env
        in (case ot1
             of (oTabstr (tv,ot2))
                  => o_eval ot2 term_env1 
                            (aug_env type_env1 tv (type_subst ty type_env))
              | _ => raise ill_formed_term_or_wrong_type ((pp_o ot1)
                             ^ " -- expected type abstraction at quant type"))
       end)
  | o_eval (u2o (ud,tv)) term_env type_env = 
      let val ty = ((type_env tv) handle unbound_variable str => (tvar tv))
       in case ty
            of (tvar tv1) 
                 => (u2o (ud_eval ud term_env type_env,tv1),init_env,init_env)
             | _ => (up ty ud,term_env,type_env)
      end 
and uc_eval (uabstr (uv,uc)) term_env type_env = 
       uabstr (uv,(uc_eval uc term_env type_env))
  | uc_eval (uTabstr (tv,uc)) term_env type_env = 
       uTabstr (tv,(uc_eval uc term_env type_env))
  | uc_eval (deconst ud) term_env type_env = 
       deconst (ud_eval ud term_env type_env)
  | uc_eval (o2u (ot,tv)) term_env type_env = 
      let val ty = ((type_env tv) handle unbound_variable str => (tvar tv))
       in case ty
            of (tvar tv1) 
                 => let val (ot1,term_env1,type_env1) = o_eval ot term_env type_env
                     in o2u (ot1,tv1)
                    end 
             | _ => uc_eval (down ty ot) term_env type_env
      end 
and ud_eval (uvar uv) term_env type_env = 
       uvar uv
  | ud_eval (uappl (ud,uc)) term_env type_env = 
       uappl ((ud_eval ud term_env type_env),(uc_eval uc term_env type_env))
  | ud_eval (uTappl (ud,ty)) term_env type_env = 
       uTappl ((ud_eval ud term_env type_env),type_subst ty type_env);

fun eval term = uc_eval term init_env init_env;

fun max m n = if m<n then n else m;

fun maxval_o  (ovar var) = var
  | maxval_o  (oabstr (ov,ot)) = max ov (maxval_o ot)
  | maxval_o  (oappl (ot1,ot2)) = max (maxval_o ot1) (maxval_o ot2)
  | maxval_o  (oTabstr (tv,ot)) = max tv (maxval_o ot)
  | maxval_o  (oTappl (ot,ty)) = max (maxval_o ot) (maxval_t ty)
  | maxval_o  (u2o (ud,tv)) = max (maxval_ud ud) tv
and maxval_uc (uabstr (uv,uc)) = max uv (maxval_uc uc)
  | maxval_uc (uTabstr (tv,uc)) = max tv (maxval_uc uc)
  | maxval_uc (deconst ud) = maxval_ud ud
  | maxval_uc (o2u (ot,tv)) = max (maxval_o ot) tv
and maxval_ud (uvar uv) = uv
  | maxval_ud (uappl (ud,uc)) = max (maxval_ud ud) (maxval_uc uc)
  | maxval_ud (uTappl (ud,ty)) = max (maxval_ud ud) (maxval_t ty) 
and maxval_t  (tvar v) = v
  | maxval_t  (t1 --> t2) = max (maxval_t t1) (maxval_t t2)
  | maxval_t  (all (v,t)) = max v (maxval_t t);
  
fun nbe ty term = let val _ = setcounter (maxval_o term)
                   in pp_uc (uc_eval (down ty term) init_env init_env)
                  end