load "Int";

use "abstract-syntax.sml";
use "simple-examples.sml";

val counter = ref 0;

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

fun setcounter n = counter := n;

datatype Envval = envval of O_term * (int -> Envval) * (int -> U_deconst);

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 down (tvar var) e =
      o2u e
  | down (t1 --> t2) e =
      let val var = newindex()
       in uabstr (var,(down t2 (oappl (e, up t1 (uvar var)))))
      end
and up (tvar var) d =
      u2o d
  | up (t1 --> t2) d =
      let val var = newindex()
       in oabstr (var,(up t2 (uappl (d, down t1 (ovar var)))))
      end;

fun o_eval (ovar ov) term_env rename_env =
      let val envval (ot,term_env1,rename_env1) = (term_env ov)
       in o_eval ot term_env1 rename_env1
      end
  | o_eval (oabstr (ov,ot)) term_env rename_env =
      ((oabstr (ov,ot)),term_env,rename_env)
  | o_eval (oappl (ot1,ot2)) term_env rename_env =
      (let val (ot3,term_env1, rename_env1) = o_eval ot1 term_env rename_env
        in (case ot3
             of (oabstr (ov,ot4))
                  => o_eval ot4
                            (aug_env term_env1 ov (envval (ot2,term_env,rename_env)))
                            rename_env1
              | _ => raise ill_formed_term_or_wrong_type ((pp_o ot3)
                             ^ " ** excepted abstraction at fct type"))
       end)
  | o_eval (u2o ud) term_env rename_env =
      (u2o (ud_eval ud term_env rename_env),init_env,init_env)
and uc_eval (uabstr (uv,uc)) term_env rename_env=
       let val var = newindex()
         in uabstr (var,(uc_eval uc term_env (aug_env rename_env uv (uvar var))))
       end
  | uc_eval (deconst ud) term_env rename_env =
       deconst (ud_eval ud term_env rename_env)
  | uc_eval (o2u ot) term_env rename_env =
      let val (ot1,_,_) = o_eval ot term_env rename_env
       in (o2u ot1)
      end
and ud_eval (uvar uv) term_env rename_env =
       rename_env uv
  | ud_eval (uappl (ud,uc)) term_env rename_env =
       uappl ((ud_eval ud term_env rename_env),(uc_eval uc term_env rename_env));

fun nbe ty term = let val _ = setcounter 0
                   in pp_uc (uc_eval (down ty term) init_env init_env)
                  end;