open Utils;;


exception NotMetaConvertible;;

let meta_convertibility_aux table t1 t2 =
  let module C = Cic in
  let rec aux table t1 t2 =
    match t1, t2 with
    | t1, t2 when t1 = t2 -> table
    | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
        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
        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 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
      )
    | _, _ -> 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
    let print_table t w =
      Printf.printf "table %s is:\n" w;
      List.iter
        (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
        t;
      print_newline ();
    in
    try
      let table = meta_convertibility_aux [] left left' in
      let _ = meta_convertibility_aux table right right' in
(*       Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
(*         (string_of_equality eq1) (string_of_equality eq2); *)
(*       print_newline (); *)
      true
    with NotMetaConvertible ->
      try
        let table = meta_convertibility_aux [] left right' in
        let _ = meta_convertibility_aux table right left' in
(*         Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
(*           (string_of_equality eq1) (string_of_equality eq2); *)
(*         print_newline (); *)
        true
      with NotMetaConvertible ->
        false
;;


let meta_convertibility t1 t2 =
  try
    let _ = meta_convertibility_aux [] t1 t2 in
    true
  with NotMetaConvertible ->
    false
;;


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 _ = *)
(*     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
      | _ ->
          try
            let subst', metasenv', ugraph' =
(*               Printf.printf "provo a unificare %s e %s\n" *)
(*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
              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 (
                let names = names_of_context context in
(*                 Printf.printf "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
(*                   (CicPp.pp term names) (CicPp.pp t' names); *)
                res, lifted_term
              )
              else
                ((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 ->
(*             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, _ = aux 0 where context metasenv [] ugraph in
  List.map
    (fun (term, subst, metasenv, ugraph) ->
       let term' = C.Lambda (C.Anonymous, type_of_what, term) in
(*        Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
(*          (CicPp.ppterm term') (print_subst subst); *)
       (term', subst, metasenv, ugraph))
    expansions
;;


type equality =
    Cic.term  *    (* proof *)
    (Cic.term *    (* type *)
     Cic.term *    (* left side *)
     Cic.term) *   (* right side *)
    Cic.metasenv * (* environment for metas *)
    Cic.term list  (* arguments *)
;;


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);
                    Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
                | _ -> None, newmeta
              )
          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
              Some (C.Rel index,
                    (ty, S.lift index t1, S.lift index t2), [], []), (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 ((proof, (ty, left, right), 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
  (newmeta + (List.length newargs) + 1,
   (repl proof, (repl ty, repl left, repl right), 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 ->
      (proof, (ty, t1, t2), [], [])
  | _ ->
      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), _, _ = target in
  let eqproof, (ty, t1, t2), newmetas, args = source in

  (* ALB: TODO check that ty and eq_ty are indeed equal... *)
  (* assert (eq_ty = ty); *)

  if eq_ty <> ty then
    []
  else    
    let where, is_left =
      match nonrec_kbo 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 res1 =
      List.filter
        (fun (t, s, m, ug) ->
           nonrec_kbo (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) ->
           nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
        (beta_expand t2 ty where context metasenv' ugraph)
    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)
        else (eq_ty, left, newgoal)
      in
      (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), newmetas, args = target in
  let eqp', (ty', t1, t2), newm', args' = source in
  let maxmeta = ref newmeta in

  (* TODO check if ty and ty' are equal... *)
  (* assert (eq_ty = ty'); *)

  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 = nonrec_kbo (subst what) (subst other) in
      let cmp2 = nonrec_kbo (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 res1 =
      List.filter
        (condition left right t1 t2)
        (beta_expand t1 eq_ty left context metasenv' ugraph)
    and res2 =
      List.filter
        (condition left right t2 t1)
        (beta_expand t2 eq_ty left context metasenv' ugraph)
    and res3 =
      List.filter
        (condition right left t1 t2)
        (beta_expand t1 eq_ty right context metasenv' ugraph)
    and res4 =
      List.filter
        (condition right left t2 t1)
        (beta_expand t2 eq_ty right context metasenv' ugraph)
    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
        fix_metas !maxmeta
          (neweqproof, (eq_ty, left, right), 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), metas, args = target
  and proof', (ty, t1, t2), metas', args' = source in
  if eq_ty <> ty then
    newmeta, target
  else
    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
    let rec demodulate newmeta step metasenv target =
      let proof, (eq_ty, left, right), 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) =
        nonrec_kbo (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
(*         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'' =
                  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),
                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
            let newmetasenv = metasenv @ metas in
            let newargs = args @ args' in
            fix_metas newmeta
              (newproof, (eq_ty, left, right), newmetasenv, newargs)
          in
          Printf.printf
            "demodulate, newtarget: %s\ntarget was: %s\n"
            (string_of_equality ~env newtarget)
            (string_of_equality ~env target);
          print_newline ();
          if is_identity env newtarget then
            newmeta, newtarget
          else
            demodulate newmeta step metasenv newtarget
    in
    demodulate newmeta 3 (metasenv @ metas') target
;;


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