module V = Value
module E = Eval

exception Unequal (* todo, better exception *)

let rec conv_tp (len : int) (v1 : V.value) (v2 : V.value) =
  match v1, v2 with
  | Type,                Type                    -> ()
  | T0,                  T0                      -> ()
  | T1,                  T1                      -> ()
  | TNat,                TNat                    -> ()
  | TBool,               TBool                   -> ()
  | Pi (a1, C (env1, b1)), Pi (a2, C (env2, b2)) (* fallthrough *)
  | Sg (a1, C (env1, b1)), Sg (a2, C (env2, b2)) -> 
      conv_tp len a1 a2;
      let fresh = V.Stuck (V.Var (V.Lvl len), a1) in
      conv_tp (len+1) (E.eval (fresh :: env1) b1) (E.eval (fresh :: env2) b2)
  | Stuck (s1, Type), Stuck (s2, Type)           -> conv_stuck len s1 s2
  | _ -> raise Unequal

and conv_tr (len : int) (ty : V.value) (v1 : V.value) (v2 : V.value) =
  match ty with
  | Type -> conv_tp len v1 v2
  | T1                 -> () (* unit η-law, this still requires evaluation :/ *)
  | Pi (a, C (env, b)) ->
      let fresh = V.Stuck (V.Var (V.Lvl len), a) in
      conv_tr (len+1) (E.eval (fresh :: env) b) (E.app v1 a) (E.app v2 a)
  | Sg (a, C (env, b)) ->
      let f1 = E.fst v1 in
      conv_tr len a                      f1         (E.fst v2);
      conv_tr len (E.eval (f1 :: env) b) (E.snd v1) (E.snd v2)
  | _ ->
      begin match v1, v2 with
      | _ -> failwith "todo"
      end

and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) =
  failwith "todo"