(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2018 - Inria
 * Copyright (c) - 2012--2018 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-C-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
open EcUtils
open EcTypes
open EcEnv

(* -------------------------------------------------------------------- *)
type 'a eqtest  = env -> 'a -> 'a -> bool

(* -------------------------------------------------------------------- *)
let rec for_type env t1 t2 =
  ty_equal t1 t2 || for_type_r env t1 t2

(* -------------------------------------------------------------------- *)
and for_type_r env t1 t2 =
  match t1.ty_node, t2.ty_node with
  | Tunivar uid1, Tunivar uid2 -> EcUid.uid_equal uid1 uid2

  | Tvar i1, Tvar i2 -> i1 = i2

  | Ttuple lt1, Ttuple lt2 ->
        List.length lt1 = List.length lt2
     && List.all2 (for_type env) lt1 lt2

  | Tfun (t1, t2), Tfun (t1', t2') ->
      for_type env t1 t1' && for_type env t2 t2'

  | Tglob m1, Tglob m2 -> EcIdent.id_equal m1 m2

  | Tconstr (p1, lt1), Tconstr (p2, lt2) when EcPath.p_equal p1 p2 ->
      if
           List.length lt1 = List.length lt2
        && List.all2 (for_type env) lt1 lt2
      then true
      else
        if   Ty.defined p1 env
        then for_type env (Ty.unfold p1 lt1 env) (Ty.unfold p2 lt2 env)
        else false

  | Tconstr (p1, lt1), _ when Ty.defined p1 env ->
      for_type env (Ty.unfold p1 lt1 env) t2

  | _, Tconstr (p2, lt2) when Ty.defined p2 env ->
      for_type env t1 (Ty.unfold p2 lt2 env)

  | _, _ -> false

(* -------------------------------------------------------------------- *)
let rec for_etyarg env ((ty1, tcws1) : etyarg) ((ty2, tcws2) : etyarg) =
  for_type env ty1 ty2 && for_tcws env tcws1 tcws2

and for_etyargs env (tyargs1 : etyarg list) (tyargs2 : etyarg list) =
     List.length tyargs1 = List.length tyargs2
  && List.for_all2 (for_etyarg env) tyargs1 tyargs2

and for_tcw env ((tyargs1, p1) : tcwitness) ((tyargs2, p2) : tcwitness) =
  EcPath.p_equal p1 p2 && for_etyargs env tyargs1 tyargs2

and for_tcws env (tcws1 : tcwitness list) (tcws2 : tcwitness list) =
    List.length tcws1 = List.length tcws2
 && List.for_all2 (for_tcw env) tcws1 tcws2