open Utils;;


type equality =
    int  *               (* weight *)
    (Cic.term *          (* type *)
     Cic.term *          (* left side *)
     Cic.term *          (* right side *)
     Utils.comparison) * (* ordering *)  
    Cic.metasenv *       (* environment for metas *)
    Cic.term list        (* arguments *)
;;


type proof =
  | BasicProof of Cic.term
  | ProofBlock of
      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
        equality
  | NoProof
;;


let string_of_equality ?env =
  match env with
  | None -> (
      function
        | _, (ty, left, right, o), _, _ ->
            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
              (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
    )
  | Some (_, context, _) -> (
      let names = names_of_context context in
      function
        | _, (ty, left, right, o), _, _ ->
            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
              (CicPp.pp left names) (string_of_comparison o)
              (CicPp.pp right names)
    )
;;


let prooftable = Hashtbl.create 2001;;

let store_proof equality proof =
  if not (Hashtbl.mem prooftable equality) then
    Hashtbl.add prooftable equality proof
;;


let delete_proof equality =
(*   Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
(*   print_newline (); *)
  Hashtbl.remove prooftable equality
;;


let rec build_term_proof equality =
(*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
(*   print_newline (); *)
  let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
  match proof with
  | NoProof ->
      Printf.fprintf stderr "WARNING: no proof for %s\n"
        (string_of_equality equality);
      Cic.Implicit None
  | BasicProof term -> term
  | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
(*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
(*         (string_of_equality eq) (string_of_equality eq'); *)
(*       print_newline (); *)
      let proof' = build_term_proof eq in
      let eqproof = build_term_proof eq' in
      let _, (ty, what, other, _), menv', args' = eq in
      let what, other = if pos = Utils.Left then what, other else other, what in
      CicMetaSubst.apply_subst subst
        (Cic.Appl [Cic.Const (eq_URI, []); ty;
                   what; t'; eqproof; other; proof'])
;;


let rec metas_of_term = function
  | Cic.Meta (i, c) -> [i]
  | Cic.Var (_, ens) 
  | Cic.Const (_, ens) 
  | Cic.MutInd (_, _, ens) 
  | Cic.MutConstruct (_, _, _, ens) ->
      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
  | Cic.Cast (s, t)
  | Cic.Prod (_, s, t)
  | Cic.Lambda (_, s, t)
  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
  | Cic.MutCase (uri, i, s, t, l) ->
      (metas_of_term s) @ (metas_of_term t) @
        (List.flatten (List.map metas_of_term l))
  | Cic.Fix (i, il) ->
      List.flatten
        (List.map (fun (s, i, t1, t2) ->
                     (metas_of_term t1) @ (metas_of_term t2)) il)
  | Cic.CoFix (i, il) ->
      List.flatten
        (List.map (fun (s, t1, t2) ->
                     (metas_of_term t1) @ (metas_of_term t2)) il)
  | _ -> []
;;      


exception NotMetaConvertible;;

let meta_convertibility_aux table t1 t2 =
  let module C = Cic in
  let print_table t =
    String.concat ", "
      (List.map
         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
  in
  let rec aux ((table_l, table_r) as table) t1 t2 =
(*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
(*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
(*       (print_table table_l) (print_table table_r); *)
    match t1, t2 with
    | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
        let m1_binding, table_l =
          try List.assoc m1 table_l, table_l
          with Not_found -> m2, (m1, m2)::table_l
        and m2_binding, table_r =
          try List.assoc m2 table_r, table_r
          with Not_found -> m1, (m2, m1)::table_r
        in
(*         let m1_binding, m2_binding, table = *)
(*           let m1b, table =  *)
(*             try List.assoc m1 table, table *)
(*             with Not_found -> m2, (m1, m2)::table *)
(*           in *)
(*           let m2b, table =  *)
(*             try List.assoc m2 table, table *)
(*             with Not_found -> m1, (m2, m1)::table *)
(*           in *)
(*           m1b, m2b, table *)
(*         in *)
(*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
(*           (print_table table_l) (print_table table_r); *)
        if (m1_binding <> m2) || (m2_binding <> m1) then
          raise NotMetaConvertible
        else (
          try
            List.fold_left2
              (fun res t1 t2 ->
                 match t1, t2 with
                 | None, Some _ | Some _, None -> raise NotMetaConvertible
                 | None, None -> res
                 | Some t1, Some t2 -> (aux res t1 t2))
              (table_l, table_r) tl1 tl2
          with Invalid_argument _ ->
            raise NotMetaConvertible
        )
    | C.Var (u1, ens1), C.Var (u2, ens2)
    | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
        aux_ens table ens1 ens2
    | C.Cast (s1, t1), C.Cast (s2, t2)
    | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
    | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
    | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
        let table = aux table s1 s2 in
        aux table t1 t2
    | C.Appl l1, C.Appl l2 -> (
        try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
        with Invalid_argument _ -> raise NotMetaConvertible
      )
    | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
        when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
    | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
        when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
        aux_ens table ens1 ens2
    | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
        when (UriManager.eq u1 u2) && i1 = i2 ->
        let table = aux table s1 s2 in
        let table = aux table t1 t2 in (
          try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
          with Invalid_argument _ -> raise NotMetaConvertible
        )
    | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
        try
          List.fold_left2
            (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
               if i1 <> i2 then raise NotMetaConvertible
               else
                 let res = (aux res s1 s2) in aux res t1 t2)
            table il1 il2
        with Invalid_argument _ -> raise NotMetaConvertible
      )
    | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
        try
          List.fold_left2
            (fun res (n1, s1, t1) (n2, s2, t2) ->
               let res = aux res s1 s2 in aux res t1 t2)
            table il1 il2
        with Invalid_argument _ -> raise NotMetaConvertible
      )
    | t1, t2 when t1 = t2 -> table
    | _, _ -> raise NotMetaConvertible
        
  and aux_ens table ens1 ens2 =
    let cmp (u1, t1) (u2, t2) =
      compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
    in
    let ens1 = List.sort cmp ens1
    and ens2 = List.sort cmp ens2 in
    try
      List.fold_left2
        (fun res (u1, t1) (u2, t2) ->
           if not (UriManager.eq u1 u2) then raise NotMetaConvertible
           else aux res t1 t2)
        table ens1 ens2
    with Invalid_argument _ -> raise NotMetaConvertible
  in
  aux table t1 t2
;;


let meta_convertibility_eq eq1 eq2 =
  let _, (ty, left, right, _), _, _ = eq1
  and _, (ty', left', right', _), _, _ = eq2 in
  if ty <> ty' then
    false
  else if (left = left') && (right = right') then
    true
  else if (left = right') && (right = left') then
    true
  else
    try
      let table = meta_convertibility_aux ([], []) left left' in
      let _ = meta_convertibility_aux table right right' in
      true
    with NotMetaConvertible ->
      try
        let table = meta_convertibility_aux ([], []) left right' in
        let _ = meta_convertibility_aux table right left' in
        true
      with NotMetaConvertible ->
        false
;;


let meta_convertibility t1 t2 =
  let f t =
    String.concat ", "
      (List.map
         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
  in
  if t1 = t2 then
    true
  else
    try
      let l, r = meta_convertibility_aux ([], []) t1 t2 in
      (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
      true
    with NotMetaConvertible ->
      false
;;


let replace_metas (* context *) term =
  let module C = Cic in
  let rec aux = function
    | C.Meta (i, c) ->
(*         let irl = *)
(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
(*         in *)
(*         if c = irl then *)
(*           C.Implicit (Some (`MetaIndex i)) *)
(*         else ( *)
(*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
(*             (String.concat "\n" *)
(*                (List.map *)
(*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
(*           C.Meta (i, c) *)
(*         ) *)
        C.Implicit (Some (`MetaInfo (i, c)))
    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
    | C.Cast (s, t) -> C.Cast (aux s, aux t)
    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
    | C.Appl l -> C.Appl (List.map aux l)
    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
    | C.MutCase (uri, i, s, t, l) ->
        C.MutCase (uri, i, aux s, aux t, List.map aux l)
    | C.Fix (i, il) ->
        let il' =
          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
        C.Fix (i, il')
    | C.CoFix (i, il) ->
        let il' =
          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
        C.CoFix (i, il')
    | t -> t
  and aux_ens ens =
    List.map (fun (u, t) -> (u, aux t)) ens
  in
  aux term
;;


let restore_metas (* context *) term =
  let module C = Cic in
  let rec aux = function
    | C.Implicit (Some (`MetaInfo (i, c))) ->
(*         let c = *)
(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
(*         in *)
(*         C.Meta (i, c) *)
(*         let local_context:(C.term option) list = *)
(*           Marshal.from_string mc 0 *)
(*         in *)
(*         C.Meta (i, local_context) *)
        C.Meta (i, c)
    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
    | C.Cast (s, t) -> C.Cast (aux s, aux t)
    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
    | C.Appl l -> C.Appl (List.map aux l)
    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
    | C.MutCase (uri, i, s, t, l) ->
        C.MutCase (uri, i, aux s, aux t, List.map aux l)
    | C.Fix (i, il) ->
        let il' =
          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
        C.Fix (i, il')
    | C.CoFix (i, il) ->
        let il' =
          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
        C.CoFix (i, il')
    | t -> t
  and aux_ens ens =
    List.map (fun (u, t) -> (u, aux t)) ens
  in
  aux term
;;


let rec restore_subst (* context *) subst =
  List.map
    (fun (i, (c, t, ty)) ->
       i, (c, restore_metas (* context *) t, ty))
    subst
;;


let rec check_irl start = function
  | [] -> true
  | None::tl -> check_irl (start+1) tl
  | (Some (Cic.Rel x))::tl ->
      if x = start then check_irl (start+1) tl else false
  | _ -> false
;;

let rec is_simple_term = function
  | Cic.Appl ((Cic.Meta _)::_) -> false
  | Cic.Appl l -> List.for_all is_simple_term l
  | Cic.Meta (i, l) -> check_irl 1 l
  | Cic.Rel _ -> true
  | _ -> false
;;


let lookup_subst meta subst =
  match meta with
  | Cic.Meta (i, _) -> (
      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
      with Not_found -> meta
    )
  | _ -> assert false
;;


let unification_simple metasenv context t1 t2 ugraph =
  let module C = Cic in
  let module M = CicMetaSubst in
  let module U = CicUnification in
  let lookup = lookup_subst in
  let rec occurs_check subst what where =
    (*       Printf.printf "occurs_check %s %s" *)
    (*         (CicPp.ppterm what) (CicPp.ppterm where); *)
    (*       print_newline (); *)
    match where with
    | t when what = t -> true
    | C.Appl l -> List.exists (occurs_check subst what) l
    | C.Meta _ ->
        let t = lookup where subst in
        if t <> where then occurs_check subst what t else false
    | _ -> false
  in
  let rec unif subst menv s t =
(*     Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
(*       (print_subst subst); *)
(*     print_newline (); *)
    let s = match s with C.Meta _ -> lookup s subst | _ -> s
    and t = match t with C.Meta _ -> lookup t subst | _ -> t
    in
    (*       Printf.printf "after apply_subst: %s %s\n%s" *)
    (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
    (*       print_newline (); *)
    match s, t with
    | s, t when s = t -> subst, menv
    | C.Meta (i, _), C.Meta (j, _) when i > j ->
        unif subst menv t s
    | C.Meta _, t when occurs_check subst s t ->
        raise (U.UnificationFailure "Inference.unification.unif")
(*     | C.Meta (i, l), C.Meta (j, l') -> *)
(*         let _, _, ty = CicUtil.lookup_meta i menv in *)
(*         let _, _, ty' = CicUtil.lookup_meta j menv in *)
(*         let binding1 = lookup s subst in *)
(*         let binding2 = lookup t subst in *)
(*         let subst, menv =  *)
(*           if binding1 != s then *)
(*             if binding2 != t then *)
(*               unif subst menv binding1 binding2 *)
(*             else *)
(*               if binding1 = t then *)
(*                 subst, menv *)
(*               else *)
(*                 ((j, (context, binding1, ty'))::subst, *)
(*                  List.filter (fun (m, _, _) -> j <> m) menv) *)
(*           else *)
(*             if binding2 != t then *)
(*               if s = binding2 then *)
(*                 subst, menv *)
(*               else *)
(*                 ((i, (context, binding2, ty))::subst, *)
(*                  List.filter (fun (m, _, _) -> i <> m) menv) *)
(*             else *)
(*               ((i, (context, t, ty))::subst, *)
(*                List.filter (fun (m, _, _) -> i <> m) menv) *)
(*         in *)
(*         subst, menv *)
        
    | C.Meta (i, l), t ->
        let _, _, ty = CicUtil.lookup_meta i menv in
        let subst =
          if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
          else subst
        in
        let menv = List.filter (fun (m, _, _) -> i <> m) menv in
        subst, menv
    | _, C.Meta _ -> unif subst menv t s
    | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
        raise (U.UnificationFailure "Inference.unification.unif")
    | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
        try
          List.fold_left2
            (fun (subst', menv) s t -> unif subst' menv s t)
            (subst, menv) tls tlt
        with e ->
          raise (U.UnificationFailure "Inference.unification.unif")
      )
    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
  in
  let subst, menv = unif [] metasenv t1 t2 in
  (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
  (*     print_newline (); *)
(*   let rec fix_term = function *)
(*     | (C.Meta (i, l) as t) -> *)
(*         lookup t subst *)
(*     | C.Appl l -> C.Appl (List.map fix_term l) *)
(*     | t -> t *)
(*   in *)
(*   let rec fix_subst = function *)
(*     | [] -> [] *)
(*     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
(*   in *)
(*   List.rev (fix_subst subst), menv, ugraph *)
  List.rev subst, menv, ugraph
;;


let unification metasenv context t1 t2 ugraph =
(*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
  let subst, menv, ug =
    if not (is_simple_term t1) || not (is_simple_term t2) then
      CicUnification.fo_unif metasenv context t1 t2 ugraph
    else
      unification_simple metasenv context t1 t2 ugraph
  in
  let rec fix_term = function
    | (Cic.Meta (i, l) as t) ->
        let t' = lookup_subst t subst in
        if t <> t' then fix_term t' else t
    | Cic.Appl l -> Cic.Appl (List.map fix_term l)
    | t -> t
  in
  let rec fix_subst = function
    | [] -> []
    | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
  in
(*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
(*   print_endline "|"; *)
  (* fix_subst *) subst, menv, ug
;;

(* let unification = CicUnification.fo_unif;; *)

exception MatchingFailure;;


let matching_simple metasenv context t1 t2 ugraph =
  let module C = Cic in
  let module M = CicMetaSubst in
  let module U = CicUnification in
  let lookup meta subst =
    match meta with
    | C.Meta (i, _) -> (
        try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
        with Not_found -> meta
      )
    | _ -> assert false
  in
  let rec do_match subst menv s t =
(*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
(*       (print_subst subst); *)
(*     print_newline (); *)
(*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
(*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
    (*       Printf.printf "after apply_subst: %s %s\n%s" *)
    (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
    (*       print_newline (); *)
    match s, t with
    | s, t when s = t -> subst, menv
(*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
(*         do_match subst menv t s *)
(*     | C.Meta _, t when occurs_check subst s t -> *)
(*         raise MatchingFailure *)
(*     | s, C.Meta _ when occurs_check subst t s -> *)
(*         raise MatchingFailure *)
    | s, C.Meta (i, l) ->
        let filter_menv i menv =
          List.filter (fun (m, _, _) -> i <> m) menv
        in
        let subst, menv =
          let value = lookup t subst in
          match value with
(*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
(*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
          | value when value = t ->
              let _, _, ty = CicUtil.lookup_meta i menv in
              (i, (context, s, ty))::subst, filter_menv i menv
          | value when value <> s ->
              raise MatchingFailure
          | value -> do_match subst menv s value
        in
        subst, menv
(*           else if value <> s then *)
(*             raise MatchingFailure *)
(*           else subst *)
(*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
(*           else subst *)
(*         in *)
(*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
(*         subst, menv *)
(*     | _, C.Meta _ -> do_match subst menv t s *)
(*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
(*         raise MatchingFailure *)
    | C.Appl ls, C.Appl lt -> (
        try
          List.fold_left2
            (fun (subst, menv) s t -> do_match subst menv s t)
            (subst, menv) ls lt
        with e ->
(*           print_endline (Printexc.to_string e); *)
(*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
(*           print_newline ();           *)
          raise MatchingFailure
      )
    | _, _ ->
(*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
(*         print_newline (); *)
        raise MatchingFailure
  in
  let subst, menv = do_match [] metasenv t1 t2 in
  (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
  (*     print_newline (); *)
  subst, menv, ugraph
;;


let matching metasenv context t1 t2 ugraph =
(*   if (is_simple_term t1) && (is_simple_term t2) then *)
(*     let subst, menv, ug = *)
(*       matching_simple metasenv context t1 t2 ugraph in *)
(* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
(* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
(* (\*     print_newline (); *\) *)
(*     subst, menv, ug *)
(*   else *)
    try
      let subst, metasenv, ugraph =
        (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
        unification metasenv context t1 t2 ugraph
      in
      let t' = CicMetaSubst.apply_subst subst t1 in
      if not (meta_convertibility t1 t') then
        raise MatchingFailure
      else
        let metas = metas_of_term t1 in
        let fix_subst = function
          | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
              (j, (c, Cic.Meta (i, lc), ty))
          | s -> s
        in
        let subst = List.map fix_subst subst in

(*         Printf.printf "matching %s %s:\n%s\n" *)
(*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
(*         print_newline (); *)

        subst, metasenv, ugraph
    with e ->
(*       Printf.printf "failed to match %s %s\n" *)
(*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
      raise MatchingFailure
;;

(* let matching = *)
(*   let profile = CicUtil.profile "Inference.matching" in *)
(*   (fun metasenv context t1 t2 ugraph -> *)
(*      profile (matching metasenv context t1 t2) ugraph) *)
(* ;; *)


let beta_expand ?(metas_ok=true) ?(match_only=false)
    what type_of_what where context metasenv ugraph = 
  let module S = CicSubstitution in
  let module C = Cic in

  let print_info = false in
  
(*   let _ = *)
(*     let names = names_of_context context in *)
(*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
(*       (CicPp.pp what names) (CicPp.ppterm what) *)
(*       (CicPp.pp where names) (CicPp.ppterm where); *)
(*     print_newline (); *)
(*   in *)
  (*
    return value:
    ((list of all possible beta expansions, subst, metasenv, ugraph),
     lifted term)
  *)
  let rec aux lift_amount term context metasenv subst ugraph =
(*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
    let res, lifted_term = 
      match term with
      | C.Rel m  ->
          [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
            
      | C.Var (uri, exp_named_subst) ->
          let ens', lifted_ens =
            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
          in
          let expansions = 
            List.map
              (fun (e, s, m, ug) ->
                 (C.Var (uri, e), s, m, ug)) ens'
          in
          expansions, C.Var (uri, lifted_ens)
            
      | C.Meta (i, l) ->
          let l', lifted_l = 
            List.fold_right
              (fun arg (res, lifted_tl) ->
                 match arg with
                 | Some arg ->
                     let arg_res, lifted_arg =
                       aux lift_amount arg context metasenv subst ugraph in
                     let l1 =
                       List.map
                         (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
                         arg_res
                     in
                     (l1 @
                        (List.map
                           (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
                           res),
                      (Some lifted_arg)::lifted_tl)
                 | None ->
                     (List.map
                        (fun (r, s, m, ug) -> None::r, s, m, ug)
                        res, 
                      None::lifted_tl)
              ) l ([], [])
          in
          let e = 
            List.map
              (fun (l, s, m, ug) ->
                 (C.Meta (i, l), s, m, ug)) l'
          in
          e, C.Meta (i, lifted_l)
            
      | C.Sort _
      | C.Implicit _ as t -> [], t
          
      | C.Cast (s, t) ->
          let l1, lifted_s =
            aux lift_amount s context metasenv subst ugraph in
          let l2, lifted_t =
            aux lift_amount t context metasenv subst ugraph
          in
          let l1' =
            List.map
              (fun (t, s, m, ug) ->
                 C.Cast (t, lifted_t), s, m, ug) l1 in
          let l2' =
            List.map
              (fun (t, s, m, ug) ->
                 C.Cast (lifted_s, t), s, m, ug) l2 in
          l1'@l2', C.Cast (lifted_s, lifted_t)
            
      | C.Prod (nn, s, t) ->
          let l1, lifted_s =
            aux lift_amount s context metasenv subst ugraph in
          let l2, lifted_t =
            aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
              metasenv subst ugraph
          in
          let l1' =
            List.map
              (fun (t, s, m, ug) ->
                 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
          let l2' =
            List.map
              (fun (t, s, m, ug) ->
                 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
          l1'@l2', C.Prod (nn, lifted_s, lifted_t)

      | C.Lambda (nn, s, t) ->
          let l1, lifted_s =
            aux lift_amount s context metasenv subst ugraph in
          let l2, lifted_t =
            aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
              metasenv subst ugraph
          in
          let l1' =
            List.map
              (fun (t, s, m, ug) ->
                 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
          let l2' =
            List.map
              (fun (t, s, m, ug) ->
                 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
          l1'@l2', C.Lambda (nn, lifted_s, lifted_t)

      | C.LetIn (nn, s, t) ->
          let l1, lifted_s =
            aux lift_amount s context metasenv subst ugraph in
          let l2, lifted_t =
            aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
              metasenv subst ugraph
          in
          let l1' =
            List.map
              (fun (t, s, m, ug) ->
                 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
          let l2' =
            List.map
              (fun (t, s, m, ug) ->
                 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
          l1'@l2', C.LetIn (nn, lifted_s, lifted_t)

      | C.Appl l ->
          let l', lifted_l =
            aux_list lift_amount l context metasenv subst ugraph
          in
          (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
           C.Appl lifted_l)
            
      | C.Const (uri, exp_named_subst) ->
          let ens', lifted_ens =
            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
          in
          let expansions = 
            List.map
              (fun (e, s, m, ug) ->
                 (C.Const (uri, e), s, m, ug)) ens'
          in
          (expansions, C.Const (uri, lifted_ens))

      | C.MutInd (uri, i ,exp_named_subst) ->
          let ens', lifted_ens =
            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
          in
          let expansions = 
            List.map
              (fun (e, s, m, ug) ->
                 (C.MutInd (uri, i, e), s, m, ug)) ens'
          in
          (expansions, C.MutInd (uri, i, lifted_ens))

      | C.MutConstruct (uri, i, j, exp_named_subst) ->
          let ens', lifted_ens =
            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
          in
          let expansions = 
            List.map
              (fun (e, s, m, ug) ->
                 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
          in
          (expansions, C.MutConstruct (uri, i, j, lifted_ens))

      | C.MutCase (sp, i, outt, t, pl) ->
          let pl_res, lifted_pl =
            aux_list lift_amount pl context metasenv subst ugraph
          in
          let l1, lifted_outt =
            aux lift_amount outt context metasenv subst ugraph in
          let l2, lifted_t =
            aux lift_amount t context metasenv subst ugraph in

          let l1' =
            List.map
              (fun (outt, s, m, ug) ->
                 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
          let l2' =
            List.map
              (fun (t, s, m, ug) ->
                 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
          let l3' =
            List.map
              (fun (pl, s, m, ug) ->
                 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
          in
          (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))

      | C.Fix (i, fl) ->
          let len = List.length fl in
          let fl', lifted_fl =
            List.fold_right
              (fun (nm, idx, ty, bo) (res, lifted_tl) ->
                 let lifted_ty = S.lift lift_amount ty in
                 let bo_res, lifted_bo =
                   aux (lift_amount+len) bo context metasenv subst ugraph in
                 let l1 =
                   List.map
                     (fun (a, s, m, ug) ->
                        (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
                     bo_res
                 in
                 (l1 @
                    (List.map
                       (fun (r, s, m, ug) ->
                          (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
                  (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
              ) fl ([], [])
          in
          (List.map
             (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
           C.Fix (i, lifted_fl))
            
      | C.CoFix (i, fl) ->
          let len = List.length fl in
          let fl', lifted_fl =
            List.fold_right
              (fun (nm, ty, bo) (res, lifted_tl) ->
                 let lifted_ty = S.lift lift_amount ty in
                 let bo_res, lifted_bo =
                   aux (lift_amount+len) bo context metasenv subst ugraph in
                 let l1 =
                   List.map
                     (fun (a, s, m, ug) ->
                        (nm, lifted_ty, a)::lifted_tl, s, m, ug)
                     bo_res
                 in
                 (l1 @
                    (List.map
                       (fun (r, s, m, ug) ->
                          (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
                  (nm, lifted_ty, lifted_bo)::lifted_tl)
              ) fl ([], [])
          in
          (List.map
             (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
           C.CoFix (i, lifted_fl))
    in
    let retval = 
      match term with
      | C.Meta _ when (not metas_ok) ->
          res, lifted_term
      | _ ->
(*           let term' = *)
(*             if match_only then replace_metas context term *)
(*             else term *)
(*           in *)
          try
            let subst', metasenv', ugraph' =
(*               Printf.printf "provo a unificare %s e %s\n" *)
(*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
              if match_only then
                matching metasenv context term (S.lift lift_amount what) ugraph
              else
                CicUnification.fo_unif metasenv context
                  (S.lift lift_amount what) term ugraph
            in
(*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
(*             (CicPp.ppterm (S.lift lift_amount what)); *)
(*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
(*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
            (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
(*             if match_only then *)
(*               let t' = CicMetaSubst.apply_subst subst' term in *)
(*               if not (meta_convertibility term t') then ( *)
(*                 res, lifted_term *)
(*               ) else ( *)
(*                 let metas = metas_of_term term in *)
(*                 let fix_subst = function *)
(*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
(*                       (j, (c, C.Meta (i, lc), ty)) *)
(*                   | s -> s *)
(*                 in *)
(*                 let subst' = List.map fix_subst subst' in *)
(*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
(*                  lifted_term) *)
(*               ) *)
(*             else *)
              ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
               lifted_term)
          with e ->
            if print_info then (
              print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
            );
            res, lifted_term
    in
(*     Printf.printf "exit aux\n"; *)
    retval

  and aux_list lift_amount l context metasenv subst ugraph =
    List.fold_right
      (fun arg (res, lifted_tl) ->
         let arg_res, lifted_arg =
           aux lift_amount arg context metasenv subst ugraph in
         let l1 = List.map
           (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
         in
         (l1 @ (List.map
                  (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
          lifted_arg::lifted_tl)
      ) l ([], [])

  and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
    List.fold_right
      (fun (u, arg) (res, lifted_tl) ->
         let arg_res, lifted_arg =
           aux lift_amount arg context metasenv subst ugraph in
         let l1 =
           List.map
             (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
         in
         (l1 @ (List.map (fun (r, s, m, ug) ->
                            (u, lifted_arg)::r, s, m, ug) res),
          (u, lifted_arg)::lifted_tl)
      ) exp_named_subst ([], [])

  in
  let expansions, _ =
(*     let where = *)
(*       if match_only then replace_metas (\* context *\) where *)
(*       else where *)
(*     in *)
    if print_info then (
      Printf.printf "searching %s inside %s\n"
        (CicPp.ppterm what) (CicPp.ppterm where);
    );
    aux 0 where context metasenv [] ugraph
  in
  let mapfun =
(*     if match_only then *)
(*       (fun (term, subst, metasenv, ugraph) -> *)
(*          let term' = *)
(*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
(*          and subst = restore_subst subst in *)
(*          (term', subst, metasenv, ugraph)) *)
(*     else *)
      (fun (term, subst, metasenv, ugraph) ->
         let term' = C.Lambda (C.Anonymous, type_of_what, term) in
         (term', subst, metasenv, ugraph))
  in
  List.map mapfun expansions
;;


let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
  let module C = Cic in
  let module S = CicSubstitution in
  let module T = CicTypeChecker in
  let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
  let rec aux index newmeta = function
    | [] -> [], newmeta
    | (Some (_, C.Decl (term)))::tl ->
        let do_find context term =
          match term with
          | C.Prod (name, s, t) ->
(*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
              let (head, newmetas, args, _) =
                PrimitiveTactics.new_metasenv_for_apply newmeta proof
                  context (S.lift index term)
              in
              let newmeta =
                List.fold_left
                  (fun maxm arg ->
                     match arg with
                     | C.Meta (i, _) -> (max maxm i)
                     | _ -> assert false)
                  newmeta args
              in
              let p =
                if List.length args = 0 then
                  C.Rel index
                else
                  C.Appl ((C.Rel index)::args)
              in (
                match head with
                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
                    Printf.printf "OK: %s\n" (CicPp.ppterm term);
                    let o = !Utils.compare_terms t1 t2 in
                    let w = compute_equality_weight ty t1 t2 in
                    let e = (w, (ty, t1, t2, o), newmetas, args) in
                    store_proof e (BasicProof p);
                    Some e, (newmeta+1)
                | _ -> None, newmeta
              )
          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
              let t1 = S.lift index t1
              and t2 = S.lift index t2 in
              let o = !Utils.compare_terms t1 t2 in
              let w = compute_equality_weight ty t1 t2 in
              let e = (w, (ty, t1, t2, o), [], []) in
              store_proof e (BasicProof (C.Rel index));
              Some e, (newmeta+1)
          | _ -> None, newmeta
        in (
          match do_find context term with
          | Some p, newmeta ->
              let tl, newmeta' = (aux (index+1) newmeta tl) in
              p::tl, max newmeta newmeta'
          | None, _ ->
              aux (index+1) newmeta tl
        )
    | _::tl ->
        aux (index+1) newmeta tl
  in
  aux 1 newmeta context
;;


let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
  let table = Hashtbl.create (List.length args) in
  let newargs, _ =
    List.fold_right
      (fun t (newargs, index) ->
         match t with
         | Cic.Meta (i, l) ->
             Hashtbl.add table i index;
             ((Cic.Meta (index, l))::newargs, index+1)
         | _ -> assert false)
      args ([], newmeta)
  in
  let repl where =
    ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
      ~where
  in
  let menv' =
    List.fold_right
      (fun (i, context, term) menv ->
         try
           let index = Hashtbl.find table i in
           (index, context, term)::menv
         with Not_found ->
           (i, context, term)::menv)
      menv []
  in
  let ty = repl ty
  and left = repl left
  and right = repl right in
  let metas = (metas_of_term left) @ (metas_of_term right) in
  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
  and newargs =
    List.filter
      (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
  in
  (newmeta + (List.length newargs) + 1,
   (weight, (ty, left, right, o), menv', newargs))
;;


exception TermIsNotAnEquality;;

let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
      let o = !Utils.compare_terms t1 t2 in
      let w = compute_equality_weight ty t1 t2 in
      let e = (w, (ty, t1, t2, o), [], []) in
      store_proof e (BasicProof proof);
      e
(*       (proof, (ty, t1, t2, o), [], []) *)
  | _ ->
      raise TermIsNotAnEquality
;;


type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;


(*
let superposition_left (metasenv, context, ugraph) target source =
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let module CR = CicReduction in
  (* we assume that target is ground (does not contain metavariables): this
   * should always be the case (I hope, at least) *)
  let proof, (eq_ty, left, right, t_order), _, _ = target in
  let eqproof, (ty, t1, t2, s_order), newmetas, args = source in

  let compare_terms = !Utils.compare_terms in

  if eq_ty <> ty then
    []
  else    
    let where, is_left =
      match t_order (* compare_terms left right *) with
      | Lt -> right, false
      | Gt -> left, true
      | _ -> (
          Printf.printf "????????? %s = %s" (CicPp.ppterm left)
            (CicPp.ppterm right);
          print_newline ();
          assert false (* again, for ground terms this shouldn't happen... *)
        )
    in
    let metasenv' = newmetas @ metasenv in
    let result = s_order (* compare_terms t1 t2 *) in
    let res1, res2 = 
      match result with
      | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
      | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
      | _ ->
          let res1 =
            List.filter
              (fun (t, s, m, ug) ->
                 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
              (beta_expand t1 ty where context metasenv' ugraph)
          and res2 =
            List.filter
              (fun (t, s, m, ug) ->
                 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
              (beta_expand t2 ty where context metasenv' ugraph)
          in
          res1, res2
    in
    (*   let what, other = *)
    (*     if is_left then left, right *)
    (*     else right, left *)
    (*   in *)
    let build_new what other eq_URI (t, s, m, ug) =
      let newgoal, newgoalproof =
        match t with
        | C.Lambda (nn, ty, bo) ->
            let bo' = S.subst (M.apply_subst s other) bo in
            let bo'' =
              C.Appl (
                [C.MutInd (HL.Logic.eq_URI, 0, []);
                 S.lift 1 eq_ty] @
                  if is_left then [bo'; S.lift 1 right]
                  else [S.lift 1 left; bo'])
            in
            let t' = C.Lambda (nn, ty, bo'') in
            S.subst (M.apply_subst s other) bo,
            M.apply_subst s
              (C.Appl [C.Const (eq_URI, []); ty; what; t';
                       proof; other; eqproof])
        | _ -> assert false
      in
      let equation =
        if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
        else (eq_ty, left, newgoal, compare_terms left newgoal)
      in
      (newgoalproof (* eqproof *), equation, [], [])
    in
    let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
    and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
    new1 @ new2
;;


let superposition_right newmeta (metasenv, context, ugraph) target source =
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let module CR = CicReduction in
  let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
  let eqp', (ty', t1, t2, s_order), newm', args' = source in
  let maxmeta = ref newmeta in

  let compare_terms = !Utils.compare_terms in

  if eq_ty <> ty' then
    newmeta, []
  else
    (*   let ok term subst other other_eq_side ugraph = *)
    (*     match term with *)
    (*     | C.Lambda (nn, ty, bo) -> *)
    (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
    (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
    (*         not res *)
    (*     |  _ -> assert false *)
    (*   in *)
    let condition left right what other (t, s, m, ug) =
      let subst = M.apply_subst s in
      let cmp1 = compare_terms (subst what) (subst other) in
      let cmp2 = compare_terms (subst left) (subst right) in
      (*     cmp1 = Gt && cmp2 = Gt *)
      cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
        (*     && (ok t s other right ug) *)
    in
    let metasenv' = metasenv @ newmetas @ newm' in
    let beta_expand = beta_expand ~metas_ok:false in
    let cmp1 = t_order (* compare_terms left right *)
    and cmp2 = s_order (* compare_terms t1 t2 *) in
    let res1, res2, res3, res4 =
      let res l r s t =
        List.filter
          (condition l r s t)
          (beta_expand s eq_ty l context metasenv' ugraph)
      in
      match cmp1, cmp2 with
      | Gt, Gt ->
          (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
      | Gt, Lt ->
          [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
      | Lt, Gt ->
          [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
      | Lt, Lt ->
          [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
      | Gt, _ ->
          let res1 = res left right t1 t2
          and res2 = res left right t2 t1 in
          res1, res2, [], []
      | Lt, _ ->
          let res3 = res right left t1 t2
          and res4 = res right left t2 t1 in
          [], [], res3, res4
      | _, Gt ->
          let res1 = res left right t1 t2
          and res3 = res right left t1 t2 in
          res1, [], res3, []
      | _, Lt ->
          let res2 = res left right t2 t1
          and res4 = res right left t2 t1 in
          [], res2, [], res4
      | _, _ ->
          let res1 = res left right t1 t2
          and res2 = res left right t2 t1
          and res3 = res right left t1 t2
          and res4 = res right left t2 t1 in
          res1, res2, res3, res4
    in
    let newmetas = newmetas @ newm' in
    let newargs = args @ args' in
    let build_new what other is_left eq_URI (t, s, m, ug) =
      (*     let what, other = *)
      (*       if is_left then left, right *)
      (*       else right, left *)
      (*     in *)
      let newterm, neweqproof =
        match t with
        | C.Lambda (nn, ty, bo) ->
            let bo' = M.apply_subst s (S.subst other bo) in
            let bo'' =
              C.Appl (
                [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
                  if is_left then [bo'; S.lift 1 right]
                  else [S.lift 1 left; bo'])
            in
            let t' = C.Lambda (nn, ty, bo'') in
            bo',
            M.apply_subst s
              (C.Appl [C.Const (eq_URI, []); ty; what; t';
                       eqproof; other; eqp'])
        | _ -> assert false
      in
      let newmeta, newequality =
        let left, right =
          if is_left then (newterm, M.apply_subst s right)
          else (M.apply_subst s left, newterm) in
        let neworder = compare_terms left right in
        fix_metas !maxmeta
          (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
      in
      maxmeta := newmeta;
      newequality
    in
    let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
    and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
    and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
    and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
    let ok = function
      | _, (_, left, right, _), _, _ ->
          not (fst (CR.are_convertible context left right ugraph))
    in
    (!maxmeta,
     (List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
*)


let is_identity ((_, context, ugraph) as env) = function
  | ((_, (ty, left, right, _), _, _) as equality) ->
      let res =
        (left = right ||
            (fst (CicReduction.are_convertible context left right ugraph)))
      in
(*       if res then ( *)
(*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
(*         print_newline (); *)
(*       ); *)
      res
;;


(*
let demodulation newmeta (metasenv, context, ugraph) target source =
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let module CR = CicReduction in

  let proof, (eq_ty, left, right, t_order), metas, args = target
  and proof', (ty, t1, t2, s_order), metas', args' = source in

  let compare_terms = !Utils.compare_terms in
  
  if eq_ty <> ty then
    newmeta, target
  else
    let first_step, get_params = 
      match s_order (* compare_terms t1 t2 *) with
      | Gt -> 1, (function
                    | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
                    | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
                    | _ -> assert false)
      | Lt -> 1, (function
                    | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
                    | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
                    | _ -> assert false)
      | _ ->
          let first_step = 3 in
          let get_params step =
            match step with
            | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
            | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
            | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
            | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
            | _ -> assert false
          in
          first_step, get_params
    in
    let rec demodulate newmeta step metasenv target =
      let proof, (eq_ty, left, right, t_order), metas, args = target in
      let is_left, what, other, eq_URI = get_params step in

      let env = metasenv, context, ugraph in
      let names = names_of_context context in
(*       Printf.printf *)
(*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
(*         (string_of_equality ~env target) (CicPp.pp what names) *)
(*         (CicPp.pp other names) (string_of_bool is_left); *)
(*       Printf.printf "step: %d" step; *)
(*       print_newline (); *)

      let ok (t, s, m, ug) =
        compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
      in
      let res =
        let r = (beta_expand ~metas_ok:false ~match_only:true
                   what ty (if is_left then left else right)
                   context (metasenv @ metas) ugraph) 
        in
(*         let m' = metas_of_term what *)
(*         and m'' = metas_of_term (if is_left then left else right) in *)
(*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
(*           Printf.printf *)
(*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
(*             (string_of_equality ~env target) (CicPp.pp what names) *)
(*             (CicPp.pp other names) (string_of_bool is_left); *)
(*           Printf.printf "step: %d" step; *)
(*           print_newline (); *)
(*           print_endline "res:"; *)
(*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
(*           print_newline (); *)
(*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
(*           print_newline (); *)
(*         ); *)
        List.filter ok r
      in
      match res with
      | [] ->
          if step = 0 then newmeta, target
          else demodulate newmeta (step-1) metasenv target
      | (t, s, m, ug)::_ -> 
          let newterm, newproof =
            match t with
            | C.Lambda (nn, ty, bo) ->
(*                 let bo' = M.apply_subst s (S.subst other bo) in *)
                let bo' = S.subst (M.apply_subst s other) bo in
                let bo'' =
                  C.Appl (
                    [C.MutInd (HL.Logic.eq_URI, 0, []);
                     S.lift 1 eq_ty] @
                      if is_left then [bo'; S.lift 1 right]
                      else [S.lift 1 left; bo'])
                in
                let t' = C.Lambda (nn, ty, bo'') in
(*                 M.apply_subst s (S.subst other bo), *)
                bo', 
                M.apply_subst s
                  (C.Appl [C.Const (eq_URI, []); ty; what; t';
                           proof; other; proof'])
            | _ -> assert false
          in
          let newmeta, newtarget =
            let left, right =
(*               if is_left then (newterm, M.apply_subst s right) *)
(*               else (M.apply_subst s left, newterm) in *)
              if is_left then newterm, right
              else left, newterm
            in
            let neworder = compare_terms left right in
(*             let newmetasenv = metasenv @ metas in *)
(*             let newargs = args @ args' in *)
(*             fix_metas newmeta *)
(*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
            let m = (metas_of_term left) @ (metas_of_term right) in
            let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
            and newargs =
              List.filter
                (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
                args
            in
            newmeta,
            (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
          in
(*           Printf.printf *)
(*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
(*             (string_of_equality ~env newtarget) *)
(*             (string_of_equality ~env target); *)
(* (\*           let _, _, newm, newa = newtarget in *\) *)
(* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
(* (\*             (print_metasenv newm) *\) *)
(* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
(*           print_newline (); *)
          if is_identity env newtarget then
            newmeta, newtarget
          else
            demodulate newmeta first_step metasenv newtarget
    in
    demodulate newmeta first_step (metasenv @ metas') target
;;


(*
let demodulation newmeta env target source =
  newmeta, target
;;
*)


let subsumption env target source =
  let _, (ty, tl, tr, _), tmetas, _ = target
  and _, (ty', sl, sr, _), smetas, _ = source in
  if ty <> ty' then
    false
  else
    let metasenv, context, ugraph = env in
    let metasenv = metasenv @ tmetas @ smetas in
    let names = names_of_context context in
    let samesubst subst subst' =
(*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
(*         (print_subst subst) (print_subst subst'); *)
(*       print_newline (); *)
      let tbl = Hashtbl.create (List.length subst) in
      List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
      List.for_all
        (fun (m, (c, t1, t2)) ->
           try
             let c', t1', t2' = Hashtbl.find tbl m in
             if (c = c') && (t1 = t1') && (t2 = t2') then true
             else false
           with Not_found ->
             true)
        subst'
    in
    let subsaux left right left' right' =
      try
        let subst, menv, ug = matching metasenv context left left' ugraph
        and subst', menv', ug' = matching metasenv context right right' ugraph
        in
(*         Printf.printf "left = right: %s = %s\n" *)
(*           (CicPp.pp left names) (CicPp.pp right names); *)
(*         Printf.printf "left' = right': %s = %s\n" *)
(*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
        samesubst subst subst'
      with e ->
(*         print_endline (Printexc.to_string e); *)
        false
    in
    let res = 
      if subsaux tl tr sl sr then true
      else subsaux tl tr sr sl
    in
    if res then (
      Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
        (string_of_equality ~env target) (string_of_equality ~env source);
      print_newline ();
    );
    res
;;
*)


let extract_differing_subterms t1 t2 =
  let module C = Cic in
  let rec aux t1 t2 =
    match t1, t2 with
    | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
        [(t1, t2)]
    | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
        let res = List.concat (List.map2 aux tl1 tl2) in
        if h1 <> h2 then
          if res = [] then [(h1, h2)] else [(t1, t2)]
        else
          if List.length res > 1 then [(t1, t2)] else res
    | t1, t2 ->
        if t1 <> t2 then [(t1, t2)] else []
  in
  let res = aux t1 t2 in
  match res with
  | hd::[] -> Some hd
  | _ -> None
;;