module V = Value
module E = Eval
module M = Metaenv

exception Unequal (* todo, better exception *)

let rec conv_tp (len : int) (v1 : V.value) (v2 : V.value) =
  match E.force v1, E.force v2 with
  | Type,                Type                    -> ()
  | T0,                  T0                      -> ()
  | T1,                  T1                      -> ()
  | TNat,                TNat                    -> ()
  | TBool,               TBool                   -> ()
  | Pi (i1, a1, C (env1, b1)), Pi (i2, a2, C (env2, b2)) ->
     if i1 != i2 then raise Unequal else
     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)
  | 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) =
  let v1 = E.force v1'
  and v2 = E.force v2' in
  match E.force ty with
  | Type               -> conv_tp len v1 v2
  | T1                 -> () (* unit η-law, this still requires evaluation :/ *)
  | T0                 -> () (* might be nice, why not? *)
  | Pi (i, 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 i v1 a) (E.app i 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
      | Zero,  Zero  -> ()
      | Suc n, Suc m -> conv_tr len ty n m
      | True,  True  -> ()
      | False, False -> ()
      | Stuck (s1, _), Stuck (s2, _) -> conv_stuck len s1 s2
      | _ -> raise Unequal
      end

(* does not need to force as things are forced in subsequent calls *)
and conv_sp (len : int) (sp1 : V.spine) (sp2 : V.spine) =
  match sp1, sp2 with
  | (x1, i1, t1) :: xs1 , (x2, i2, t2) :: xs2 ->
     if i1 != i2 then failwith "TODO: MIXED ICITY WAAAA :((" else
     conv_sp len xs1 xs2;
     conv_tp len t1 t2;
     conv_tr len t1 x1 x2
  | [] , [] -> ()
  | _ -> raise Unequal

(* does not force as it is called by functions which do force *)
and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) =
  match s1, s2 with
  | Var (Lvl i),       Var (Lvl j)       -> if i == j then () else raise Unequal
  | Fst p1,            Fst p2            -> conv_stuck len p1 p2
  | Snd p1,            Snd p2            -> conv_stuck len p1 p2
  | App (f1, xs1),     App (f2, xs2) ->
    conv_stuck len f1 f2;
    conv_sp len xs1 xs2
  | Ind0 (C (env1, a1), _), Ind0 (C (env2, a2), _) -> (* _ are definitionally equal *)
    let fresh = V.Stuck (V.Var (V.Lvl len), V.T0) in
    conv_tp (len+1) (E.eval (fresh :: env1) a1) (E.eval (fresh :: env2) a2)
  | IndN (C (aenv1, a1), z1, C2 (senv1, s1), st1), IndN (C (aenv2, a2), z2, C2 (senv2, s2), st2) ->
    conv_stuck len st1 st2;
    let fresh1 = V.Stuck (V.Var (V.Lvl len), V.TNat) in
    let ev1fr1 = E.eval (fresh1 :: aenv1) a1 in
    conv_tp (len+1) ev1fr1 (E.eval (fresh1 :: aenv2) a2);
    conv_tr len (E.eval (Zero :: aenv1) a1) z1 z2;
    let fresh2 = V.Stuck (V.Var (V.Lvl len), ev1fr1) in
    conv_tr (len+2) (E.eval (V.Suc fresh1 :: senv1) a1)
                    (E.eval (fresh2 :: fresh1 :: senv1) s1)
                    (E.eval (fresh2 :: fresh1 :: senv2) s2)
  | IndB (C (env1, a1), t1, f1, st1), IndB (C (env2, a2), t2, f2, st2) ->
    conv_stuck len st1 st2;
    let fresh = V.Stuck (V.Var (V.Lvl len), V.TBool) in
    conv_tp (len+1) (E.eval (fresh :: env1) a1) (E.eval (fresh :: env2) a2);
    conv_tr len (E.eval (V.True  :: env1) a1) t1 t2;
    conv_tr len (E.eval (V.False :: env1) a1) f1 f2
  | Meta (Mv i1), Meta (Mv i2) -> if i1 == i2 then () else raise Unequal
  | _ -> raise Unequal