(* Copyright (C) 2005, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(* let _profiler = <:profiler<_profiler>>;; *)

(* $Id$ *)

module Index = Equality_indexing.DT (* discrimination tree based indexing *)
(*
module Index = Equality_indexing.DT (* path tree based indexing *)
*)

let debug_print = Utils.debug_print;;

(* 
for debugging 
let check_equation env equation msg =
  let w, proof, (eq_ty, left, right, order), metas, args = equation in
  let metasenv, context, ugraph = env 
  let metasenv' = metasenv @ metas in
    try
      CicTypeChecker.type_of_aux' metasenv' context left ugraph;
      CicTypeChecker.type_of_aux' metasenv' context right ugraph;
      ()
    with 
        CicUtil.Meta_not_found _ as exn ->
          begin
            prerr_endline msg; 
            prerr_endline (CicPp.ppterm left);
            prerr_endline (CicPp.ppterm right);
            raise exn
          end 
*)

type retrieval_mode = Matching | Unification;;

let string_of_res ?env =
  function
      None -> "None"
    | Some (t, s, m, u, (p,e)) ->
        Printf.sprintf "Some: (%s, %s, %s)" 
          (Utils.string_of_pos p)
          (Equality.string_of_equality ?env e)
          (CicPp.ppterm t)
;;

let print_res ?env res = 
  prerr_endline 
    (String.concat "\n"
       (List.map (string_of_res ?env) res))
;;

let print_candidates ?env mode term res =
  let _ =
    match mode with
    | Matching ->
        prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
    | Unification ->
        prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
  in
  prerr_endline 
    (String.concat "\n"
       (List.map
          (fun (p, e) ->
             Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
               (Equality.string_of_equality ?env e))
          res));
;;


let apply_subst = Subst.apply_subst

let index = Index.index
let remove_index = Index.remove_index
let in_index = Index.in_index
let empty = Index.empty 
let init_index = Index.init_index

let check_disjoint_invariant subst metasenv msg =
  if (List.exists 
        (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
  then 
    begin 
      prerr_endline ("not disjoint: " ^ msg);
      assert false
    end
;;

let check_for_duplicates metas msg =
  if List.length metas <> 
  List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
    begin 
      prerr_endline ("DUPLICATI " ^ msg);
      prerr_endline (CicMetaSubst.ppmetasenv [] metas);
      assert false
    end
;;

let check_res res msg =
  match res with
      Some (t, subst, menv, ug, eq_found) ->
        let eqs = Equality.string_of_equality (snd eq_found) in
        check_disjoint_invariant subst menv msg;
        check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
    | None -> ()
;;

let check_target bag context target msg =
  let w, proof, (eq_ty, left, right, order), metas,_ = 
    Equality.open_equality target in
  (* check that metas does not contains duplicates *)
  let eqs = Equality.string_of_equality target in
  let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
  let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
    @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof)  in
  let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
  let _ = if menv <> metas then 
    begin 
      prerr_endline ("extra metas " ^ msg);
      prerr_endline (CicMetaSubst.ppmetasenv [] metas);
      prerr_endline "**********************";
      prerr_endline (CicMetaSubst.ppmetasenv [] menv);
      prerr_endline ("left: " ^ (CicPp.ppterm left));
      prerr_endline ("right: " ^ (CicPp.ppterm right)); 
      prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
      assert false
    end
  else () in ()
(*
  try 
      ignore(CicTypeChecker.type_of_aux'
        metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
  with e ->  
      prerr_endline msg;
      prerr_endline (Founif.string_of_proof proof);
      prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
      prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
      prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); 
      raise e 
*)


(* returns a list of all the equalities in the tree that are in relation
   "mode" with the given term, where mode can be either Matching or
   Unification.

   Format of the return value: list of tuples in the form:
   (position - Left or Right - of the term that matched the given one in this
     equality,
    equality found)
   
   Note that if equality is "left = right", if the ordering is left > right,
   the position will always be Left, and if the ordering is left < right,
   position will be Right.
*)

let get_candidates ?env mode tree term =
  let s = 
    match mode with
    | Matching -> 
        Index.retrieve_generalizations tree term
    | Unification -> 
        Index.retrieve_unifiables tree term
        
  in
  Index.PosEqSet.elements s
;;

(*
  finds the first equality in the index that matches "term", of type "termty"
  termty can be Implicit if it is not needed. The result (one of the sides of
  the equality, actually) should be not greater (wrt the term ordering) than
  term

  Format of the return value:

  (term to substitute, [Cic.Rel 1 properly lifted - see the various
                        build_newtarget functions inside the various
                        demodulation_* functions]
   substitution used for the matching,
   metasenv,
   ugraph, [substitution, metasenv and ugraph have the same meaning as those
   returned by CicUnification.fo_unif]
   (equality where the matching term was found, [i.e. the equality to use as
                                                rewrite rule]
    uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
         the equality: this is used to build the proof term, again see one of
         the build_newtarget functions]
   ))
*)
let rec find_matches bag metasenv context ugraph lift_amount term termty =
  let module C = Cic in
  let module U = Utils in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let cmp = !Utils.compare_terms in
  let check = match termty with C.Implicit None -> false | _ -> true in
  function
    | [] -> None
    | candidate::tl ->
        let pos, equality = candidate in
        let (_, proof, (ty, left, right, o), metas,_) = 
          Equality.open_equality equality 
        in
        if Utils.debug_metas then 
          ignore(check_target bag context (snd candidate) "find_matches");
        if Utils.debug_res then 
          begin
            let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
            let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
            let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
(*
            let p="proof = "^
              (CicPp.ppterm(Equality.build_proof_term proof))^"\n" 
            in
*)
              check_for_duplicates metas "gia nella metas";
              check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
          end;
        if check && not (fst (CicReduction.are_convertible
                                ~metasenv context termty ty ugraph)) then (
          find_matches bag metasenv context ugraph lift_amount term termty tl
        ) else
          let do_match c =
            let subst', metasenv', ugraph' =
              Founif.matching 
                metasenv metas context term (S.lift lift_amount c) ugraph
            in
            Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
          in
          let c, other =
            if pos = Utils.Left then left, right
            else right, left
          in
          if o <> U.Incomparable then
            let res =
              try
                do_match c 
              with Founif.MatchingFailure ->
                find_matches bag metasenv context ugraph lift_amount term termty tl
            in
              if Utils.debug_res then ignore (check_res res "find1");
              res
          else
            let res =
              try do_match c 
              with Founif.MatchingFailure -> None
            in
            if Utils.debug_res then ignore (check_res res "find2");
            match res with
            | Some (_, s, _, _, _) ->
                let c' = apply_subst s c in
                (* 
             let other' = U.guarded_simpl context (apply_subst s other) in *)
                let other' = apply_subst s other in
                let order = cmp c' other' in
                if order = U.Gt then
                  res
                else
                  find_matches bag
                    metasenv context ugraph lift_amount term termty tl
            | None ->
                find_matches bag metasenv context ugraph lift_amount term termty tl
;;

let find_matches metasenv context ugraph lift_amount term termty =
  find_matches metasenv context ugraph lift_amount term termty
;;

(*
  as above, but finds all the matching equalities, and the matching condition
  can be either Founif.matching or Inference.unification
*)
(* XXX termty unused *)
let rec find_all_matches ?(unif_fun=Founif.unification)
    metasenv context ugraph lift_amount term termty =
  let module C = Cic in
  let module U = Utils in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let cmp = !Utils.compare_terms in
  function
    | [] -> []
    | candidate::tl ->
        let pos, equality = candidate in 
        let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
        let do_match c =
          let subst', metasenv', ugraph' =
            unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
          in
          (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
        in
        let c, other =
          if pos = Utils.Left then left, right
          else right, left
        in
        if o <> U.Incomparable then
          try
            let res = do_match c in
            res::(find_all_matches ~unif_fun metasenv context ugraph
                    lift_amount term termty tl)
          with
          | Founif.MatchingFailure
          | CicUnification.UnificationFailure _
          | CicUnification.Uncertain _ ->
              find_all_matches ~unif_fun metasenv context ugraph
                lift_amount term termty tl
        else
          try
            let res = do_match c in
            match res with
            | _, s, _, _, _ ->
                let c' = apply_subst s c
                and other' = apply_subst s other in
                let order = cmp c' other' in
                if order <> U.Lt && order <> U.Le then
                  res::(find_all_matches ~unif_fun metasenv context ugraph
                          lift_amount term termty tl)
                else
                  find_all_matches ~unif_fun metasenv context ugraph
                    lift_amount term termty tl
          with
          | Founif.MatchingFailure
          | CicUnification.UnificationFailure _
          | CicUnification.Uncertain _ ->
              find_all_matches ~unif_fun metasenv context ugraph
                lift_amount term termty tl
;;

let find_all_matches 
  ?unif_fun metasenv context ugraph lift_amount term termty l 
=
    find_all_matches 
      ?unif_fun metasenv context ugraph lift_amount term termty l 
  (*prerr_endline "CANDIDATES:";
  List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
  prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
  (List.length rc));*)
;;
(*
  returns true if target is subsumed by some equality in table
*)
(*
let print_res l =
  prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
    ((pos,equation),_)) -> Equality.string_of_equality equation)l))
;;
*)

let subsumption_aux use_unification env table target = 
  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
  let _, context, ugraph = env in
  let metasenv = tmetas in
  let predicate, unif_fun = 
    if use_unification then
      Unification, Founif.unification
    else
      Matching, Founif.matching
  in
  let leftr =
    match left with
    | Cic.Meta _ when not use_unification -> []   
    | _ ->
        let leftc = get_candidates predicate table left in
        find_all_matches ~unif_fun
          metasenv context ugraph 0 left ty leftc
  in
  let rec ok what leftorright = function
    | [] -> None
    | (_, subst, menv, ug, (pos,equation))::tl ->
        let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
        try
          let other = if pos = Utils.Left then r else l in
          let what' = Subst.apply_subst subst what in
          let other' = Subst.apply_subst subst other in
          let subst', menv', ug' =
            unif_fun metasenv m context what' other' ugraph
          in
          (match Subst.merge_subst_if_possible subst subst' with
          | None -> ok what leftorright tl
          | Some s -> Some (s, equation, leftorright <> pos ))
        with 
        | Founif.MatchingFailure 
        | CicUnification.UnificationFailure _ -> ok what leftorright tl
  in
  match ok right Utils.Left leftr with
  | Some _ as res -> res
  | None -> 
      let rightr =
        match right with
          | Cic.Meta _ when not use_unification -> [] 
          | _ ->
              let rightc = get_candidates predicate table right in
                find_all_matches ~unif_fun
                  metasenv context ugraph 0 right ty rightc
      in
        ok left Utils.Right rightr 
;;

let subsumption x y z =
  subsumption_aux false x y z
;;

let unification x y z = 
  subsumption_aux true x y z
;;

let subsumption_aux_all use_unification env table target = 
  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
  let _, context, ugraph = env in
  let metasenv = tmetas in
  let predicate, unif_fun = 
    if use_unification then
      Unification, Founif.unification
    else
      Matching, Founif.matching
  in
  let leftr =
    match left with
    | Cic.Meta _ when not use_unification -> []   
    | _ ->
        let leftc = get_candidates predicate table left in
        find_all_matches ~unif_fun
          metasenv context ugraph 0 left ty leftc
  in
  let rightr =
        match right with
          | Cic.Meta _ when not use_unification -> [] 
          | _ ->
              let rightc = get_candidates predicate table right in
                find_all_matches ~unif_fun
                  metasenv context ugraph 0 right ty rightc
  in
  let rec ok_all what leftorright = function
    | [] -> []
    | (_, subst, menv, ug, (pos,equation))::tl ->
        let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
        try
          let other = if pos = Utils.Left then r else l in
          let what' = Subst.apply_subst subst what in
          let other' = Subst.apply_subst subst other in
          let subst', menv', ug' =
            unif_fun metasenv m context what' other' ugraph
          in
          (match Subst.merge_subst_if_possible subst subst' with
          | None -> ok_all what leftorright tl
          | Some s -> 
	      (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
        with 
        | Founif.MatchingFailure 
        | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
  in
  (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
;;

let subsumption_all x y z =
  subsumption_aux_all false x y z
;;

let unification_all x y z = 
  subsumption_aux_all true x y z
;;
let rec demodulation_aux bag ?from ?(typecheck=false) 
  metasenv context ugraph table lift_amount term =
(*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let candidates = 
    get_candidates 
      ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
  in
  let res =
    match term with
      | C.Meta _ -> None
      | term ->
          let termty, ugraph =
            if typecheck then
              CicTypeChecker.type_of_aux' metasenv context term ugraph
            else
              C.Implicit None, ugraph
          in
          let res =
            find_matches bag metasenv context ugraph lift_amount term termty candidates
          in
          if Utils.debug_res then ignore(check_res res "demod1"); 
            if res <> None then
              res
            else
              match term with
                | C.Appl l ->
                    let res, ll = 
                      List.fold_left
                        (fun (res, tl) t ->
                           if res <> None then
                             (res, tl @ [S.lift 1 t])
                           else 
                             let r =
                               demodulation_aux bag ~from:"1" metasenv context ugraph table
                                 lift_amount t
                             in
                               match r with
                                 | None -> (None, tl @ [S.lift 1 t])
                                 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
                        (None, []) l
                    in (
                        match res with
                          | None -> None
                          | Some (_, subst, menv, ug, eq_found) ->
                              Some (C.Appl ll, subst, menv, ug, eq_found)
                      )
                | C.Prod (nn, s, t) ->
                    let r1 =
                      demodulation_aux bag ~from:"2"
                        metasenv context ugraph table lift_amount s in (
                        match r1 with
                          | None ->
                              let r2 =
                                demodulation_aux bag metasenv
                                  ((Some (nn, C.Decl s))::context) ugraph
                                  table (lift_amount+1) t
                              in (
                                  match r2 with
                                    | None -> None
                                    | Some (t', subst, menv, ug, eq_found) ->
                                        Some (C.Prod (nn, (S.lift 1 s), t'),
                                              subst, menv, ug, eq_found)
                                )
                          | Some (s', subst, menv, ug, eq_found) ->
                              Some (C.Prod (nn, s', (S.lift 1 t)),
                                    subst, menv, ug, eq_found)
                      )
                | C.Lambda (nn, s, t) ->
                    let r1 =
                      demodulation_aux bag
                        metasenv context ugraph table lift_amount s in (
                        match r1 with
                          | None ->
                              let r2 =
                                demodulation_aux bag metasenv
                                  ((Some (nn, C.Decl s))::context) ugraph
                                  table (lift_amount+1) t
                              in (
                                  match r2 with
                                    | None -> None
                                    | Some (t', subst, menv, ug, eq_found) ->
                                        Some (C.Lambda (nn, (S.lift 1 s), t'),
                                              subst, menv, ug, eq_found)
                                )
                          | Some (s', subst, menv, ug, eq_found) ->
                              Some (C.Lambda (nn, s', (S.lift 1 t)),
                                    subst, menv, ug, eq_found)
                      )
                | t ->
                    None
  in
  if Utils.debug_res then ignore(check_res res "demod_aux output"); 
  res
;;

exception Foo

(** demodulation, when target is an equality *)
let rec demodulation_equality bag ?from eq_uri newmeta env table target =
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let module U = Utils in
  let metasenv, context, ugraph = env in
  let w, proof, (eq_ty, left, right, order), metas, id = 
    Equality.open_equality target 
  in
  (* first, we simplify *)
(*   let right = U.guarded_simpl context right in *)
(*   let left = U.guarded_simpl context left in *)
(*   let order = !Utils.compare_terms left right in *)
(*   let stat = (eq_ty, left, right, order) in  *)
(*  let w = Utils.compute_equality_weight stat in*)
  (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
  if Utils.debug_metas then 
    ignore(check_target bag context target "demod equalities input");
  let metasenv' = (* metasenv @ *) metas in
  let maxmeta = ref newmeta in
  
  let build_newtarget is_left (t, subst, menv, ug, eq_found) =
    
    if Utils.debug_metas then
      begin
        ignore(check_for_duplicates menv "input1");
        ignore(check_disjoint_invariant subst menv "input2");
        let substs = Subst.ppsubst subst in 
        ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
      end;
    let pos, equality = eq_found in
    let (_, proof', 
        (ty, what, other, _), menv',id') = Equality.open_equality equality in
    let ty =
      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
      with CicUtil.Meta_not_found _ -> ty
    in
    let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
    let what, other = if pos = Utils.Left then what, other else other, what in
    let newterm, newproof =
      let bo = 
        Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
(*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
      let name = C.Name "x" in
      let bo' =
        let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
          C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
      in
          (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
          (Cic.Lambda (name, ty, bo'))))))
    in
    let newmenv = menv in
    let left, right = if is_left then newterm, right else left, newterm in
    let ordering = !Utils.compare_terms left right in
    let stat = (eq_ty, left, right, ordering) in
    let res =
      let w = Utils.compute_equality_weight stat in
          (Equality.mk_equality bag (w, newproof, stat,newmenv))
    in
    if Utils.debug_metas then 
      ignore(check_target bag context res "buildnew_target output");
    !maxmeta, res 
  in

  let res = 
    demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left 
  in
  if Utils.debug_res then check_res res "demod result";
  let newmeta, newtarget = 
    match res with
    | Some t ->
        let newmeta, newtarget = build_newtarget true t in
          (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
          if (Equality.is_weak_identity newtarget) (* || *)
            (*Equality.meta_convertibility_eq target newtarget*) then
              newmeta, newtarget
          else 
            demodulation_equality bag ?from eq_uri newmeta env table newtarget
    | None ->
        let res = demodulation_aux bag metasenv' context ugraph table 0 right in
        if Utils.debug_res then check_res res "demod result 1"; 
          match res with
          | Some t ->
              let newmeta, newtarget = build_newtarget false t in
                if (Equality.is_weak_identity newtarget) ||
                  (Equality.meta_convertibility_eq target newtarget) then
                    newmeta, newtarget
                else
                   demodulation_equality bag ?from eq_uri newmeta env table newtarget
          | None ->
              newmeta, target
  in
  (* newmeta, newtarget *)
  newmeta,newtarget 
;;

(**
   Performs the beta expansion of the term "term" w.r.t. "table",
   i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
   in table.
*)
let rec betaexpand_term 
  ?(subterms_only=false) metasenv context ugraph table lift_amount term 
=
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  
  let res, lifted_term = 
    match term with
    | C.Meta (i, l) ->
        let l = [] in
        let l', lifted_l =
          List.fold_right
            (fun arg (res, lifted_tl) ->
               match arg with
               | Some arg ->
                   let arg_res, lifted_arg =
                     betaexpand_term metasenv context ugraph table
                       lift_amount arg in
                   let l1 =
                     List.map
                       (fun (t, s, m, ug, eq_found) ->
                          (Some t)::lifted_tl, s, m, ug, eq_found)
                       arg_res
                   in
                   (l1 @
                      (List.map
                         (fun (l, s, m, ug, eq_found) ->
                            (Some lifted_arg)::l, s, m, ug, eq_found)
                         res),
                    (Some lifted_arg)::lifted_tl)
               | None ->
                   (List.map
                      (fun (r, s, m, ug, eq_found) ->
                         None::r, s, m, ug, eq_found) res,
                    None::lifted_tl)
            ) l ([], [])
        in
        let e =
          List.map
            (fun (l, s, m, ug, eq_found) ->
               (C.Meta (i, l), s, m, ug, eq_found)) l'
        in
        e, C.Meta (i, lifted_l)
          
    | C.Rel m ->
        [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
          
    | C.Prod (nn, s, t) ->
        let l1, lifted_s =
          betaexpand_term metasenv context ugraph table lift_amount s in
        let l2, lifted_t =
          betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
            table (lift_amount+1) t in
        let l1' =
          List.map
            (fun (t, s, m, ug, eq_found) ->
               C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
        and l2' =
          List.map
            (fun (t, s, m, ug, eq_found) ->
               C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
        l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
          
    | C.Lambda (nn, s, t) ->
        let l1, lifted_s =
          betaexpand_term metasenv context ugraph table lift_amount s in
        let l2, lifted_t =
          betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
            table (lift_amount+1) t in
        let l1' =
          List.map
            (fun (t, s, m, ug, eq_found) ->
               C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
        and l2' =
          List.map
            (fun (t, s, m, ug, eq_found) ->
               C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
        l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)

    | C.Appl l ->
        let l', lifted_l =
          List.fold_left
            (fun (res, lifted_tl) arg ->
               let arg_res, lifted_arg =
                 betaexpand_term metasenv context ugraph table lift_amount arg
               in
               let l1 =
                 List.map
                   (fun (a, s, m, ug, eq_found) ->
                      a::lifted_tl, s, m, ug, eq_found)
                   arg_res
               in
               (l1 @
                  (List.map
                     (fun (r, s, m, ug, eq_found) ->
                        lifted_arg::r, s, m, ug, eq_found)
                     res),
                lifted_arg::lifted_tl)
            ) ([], []) (List.rev l)
        in
        (List.map
           (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
         C.Appl lifted_l)

    | t -> [], (S.lift lift_amount t)
  in
  match term with
  | C.Meta (i, l) -> res, lifted_term
  | term ->
      let termty, ugraph =
        C.Implicit None, ugraph
(*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
      in
      let candidates = get_candidates Unification table term in
      let r = 
        if subterms_only then 
          [] 
        else 
          find_all_matches
            metasenv context ugraph lift_amount term termty candidates
      in
      r @ res, lifted_term
;;

(**
   superposition_right
   returns a list of new clauses inferred with a right superposition step
   between the positive equation "target" and one in the "table" "newmeta" is
   the first free meta index, i.e. the first number above the highest meta
   index: its updated value is also returned
*)
let superposition_right bag
  ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
  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 module U = Utils in 
  let w, eqproof, (eq_ty, left, right, ordering), newmetas,id = 
    Equality.open_equality target 
  in 
  if Utils.debug_metas then 
    ignore (check_target bag context target "superpositionright");
  let metasenv' = newmetas in
  let maxmeta = ref newmeta in
  let res1, res2 =
    match ordering with
    | U.Gt -> 
        fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
    | U.Lt -> 
        [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
    | _ ->
        let res l r =
          List.filter
            (fun (_, subst, _, _, _) ->
               let subst = apply_subst subst in
               let o = !Utils.compare_terms (subst l) (subst r) in
               o <> U.Lt && o <> U.Le)
            (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
        in
        (res left right), (res right left)
  in
  let build_new ordering (bo, s, m, ug, eq_found) =
    if Utils.debug_metas then 
      ignore (check_target bag context (snd eq_found) "buildnew1" );
    
    let pos, equality =  eq_found in
    let (_, proof', (ty, what, other, _), menv',id') = 
      Equality.open_equality  equality in
    let what, other = if pos = Utils.Left then what, other else other, what in

    let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
    let newgoal, newproof =
      (* qua *)
      let bo' =
        Utils.guarded_simpl context (apply_subst s (S.subst other bo)) 
      in
      let name = C.Name "x" in
      let bo'' =
        let l, r =
          if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
        C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
      in
      bo',
        Equality.Step 
          (s,(Equality.SuperpositionRight,
               id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
    in
    let newmeta, newequality = 
      let left, right =
        if ordering = U.Gt then newgoal, apply_subst s right
        else apply_subst s left, newgoal in
      let neworder = !Utils.compare_terms left right in
      let newmenv = (* Founif.filter s *) m in
      let stat = (eq_ty, left, right, neworder) in
      let eq' =
        let w = Utils.compute_equality_weight stat in
        Equality.mk_equality bag (w, newproof, stat, newmenv) in
      if Utils.debug_metas then 
        ignore (check_target bag context eq' "buildnew3");
      let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
      if Utils.debug_metas then 
        ignore (check_target bag context eq' "buildnew4");
      newm, eq'
    in
    maxmeta := newmeta;
    if Utils.debug_metas then 
      ignore(check_target bag context newequality "buildnew2"); 
    newequality
  in
  let new1 = List.map (build_new U.Gt) res1
  and new2 = List.map (build_new U.Lt) res2 in
  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
  (!maxmeta,
   (List.filter ok (new1 @ new2)))
;;

(** demodulation, when the target is a theorem *)
let rec demodulation_theorem bag newmeta env table theorem =
  let module C = Cic in
  let module S = CicSubstitution in
  let module M = CicMetaSubst in
  let module HL = HelmLibraryObjects in
  let metasenv, context, ugraph = env in
  let maxmeta = ref newmeta in
  let term, termty, metas = theorem in
  let metasenv' = metas in
  
  let build_newtheorem (t, subst, menv, ug, eq_found) =
    let pos, equality = eq_found in
    let (_, proof', (ty, what, other, _), menv',id) = 
      Equality.open_equality equality in
    let what, other = if pos = Utils.Left then what, other else other, what in
    let newterm, newty =
      let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
(*      let bo' = apply_subst subst t in *)
(*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
(*
      let newproofold =
        Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
                              Equality.BasicProof (Equality.empty_subst,term))
      in
      (Equality.build_proof_term_old newproofold, bo)
*)
      (* TODO, not ported to the new proofs *) 
      if true then assert false; term, bo
    in    
    !maxmeta, (newterm, newty, menv)
  in  
  let res =
    demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
  in
  match res with
  | Some t ->
      let newmeta, newthm = build_newtheorem t in
      let newt, newty, _ = newthm in
      if Equality.meta_convertibility termty newty then
        newmeta, newthm
      else
        demodulation_theorem bag newmeta env table newthm
  | None ->
      newmeta, theorem
;;

(*****************************************************************************)
(**                         OPERATIONS ON GOALS                             **)
(**                                                                         **)
(**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
(*****************************************************************************)

let open_goal g =
  match g with
  | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> 
      (* assert (LibraryObjects.is_eq_URI uri); *)
      proof,menv,eq,ty,l,r
  | _ -> assert false
;;

let ty_of_goal (_,_,ty) = ty ;;

(* checks if two goals are metaconvertible *)
let goal_metaconvertibility_eq g1 g2 = 
  Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
;;

(* when the betaexpand_term function is called on the left/right side of the
 * goal, the predicate has to be fixed
 * C[x] ---> (eq ty unchanged C[x])
 * [posu] is the side of the [unchanged] term in the original goal
 *)
let fix_expansion goal posu (t, subst, menv, ug, eq_f) = 
  let _,_,eq,ty,l,r = open_goal goal in
  let unchanged = if posu = Utils.Left then l else r in
  let unchanged = CicSubstitution.lift 1 unchanged in
  let ty = CicSubstitution.lift 1 ty in
  let pred = 
    match posu with
    | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
    | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
  in
  (pred, subst, menv, ug, eq_f)
;;

(* ginve the old [goal], the side that has not changed [posu] and the 
 * expansion builds a new goal *)
let build_newgoal bag context goal posu rule expansion =
  let goalproof,_,_,_,_,_ = open_goal goal in
  let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
  let pos, equality = eq_found in
  let (_, proof', (ty, what, other, _), menv',id) = 
    Equality.open_equality equality in
  let what, other = if pos = Utils.Left then what, other else other, what in
  let newterm, newgoalproof =
    let bo = 
      Utils.guarded_simpl context 
        (apply_subst subst (CicSubstitution.subst other t)) 
    in
    let bo' = apply_subst subst t in
    let ty = apply_subst subst ty in 
    let name = Cic.Name "x" in 
    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
    bo, (newgoalproofstep::goalproof)
  in
  let newmetasenv = (* Founif.filter subst *) menv in
  (newgoalproof, newmetasenv, newterm)
;;

(**
   superposition_left 
   returns a list of new clauses inferred with a left superposition step
   the negative equation "target" and one of the positive equations in "table"
*)
let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = 
  let names = Utils.names_of_context context in
  let proof,menv,eq,ty,l,r = open_goal goal in
  let c = !Utils.compare_terms l r in
  let newgoals = 
    if c = Utils.Incomparable then
      begin
      let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
      let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
      (* prerr_endline "incomparable"; 
      prerr_endline (string_of_int (List.length expansionsl));
      prerr_endline (string_of_int (List.length expansionsr));
      *)
      List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
      @
      List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
      end
    else
        match c with 
        | Utils.Gt -> (* prerr_endline "GT"; *) 
            let big,small,possmall = l,r,Utils.Right in
            let expansions, _ = betaexpand_term menv context ugraph table 0 big in
            List.map 
              (build_newgoal bag context goal possmall Equality.SuperpositionLeft) 
              expansions
        | Utils.Lt -> (* prerr_endline "LT"; *) 
            let big,small,possmall = r,l,Utils.Left in
            let expansions, _ = betaexpand_term menv context ugraph table 0 big in
            List.map 
              (build_newgoal bag context goal possmall Equality.SuperpositionLeft) 
              expansions
        | Utils.Eq -> []
        | _ ->
            prerr_endline 
              ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
            assert false
  in
  (* rinfresco le meta *)
  List.fold_right
    (fun g (max,acc) -> 
       let max,g = Equality.fix_metas_goal max g in max,g::acc) 
    newgoals (maxmeta,[])
;;

(** demodulation, when the target is a goal *)
let rec demodulation_goal bag env table goal =
  let goalproof,menv,_,_,left,right = open_goal goal in
  let _, context, ugraph = env in
(*  let term = Utils.guarded_simpl (~debug:true) context term in*)
  let do_right () = 
      let resright = demodulation_aux bag menv context ugraph table 0 right in
      match resright with
      | Some t ->
          let newg = 
            build_newgoal bag context goal Utils.Left Equality.Demodulation t 
          in
          if goal_metaconvertibility_eq goal newg then
            false, goal
          else
            true, snd (demodulation_goal bag env table newg)
      | None -> false, goal
  in
  let resleft = demodulation_aux bag menv context ugraph table 0 left in
  match resleft with
  | Some t ->
      let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
      if goal_metaconvertibility_eq goal newg then
        do_right ()
      else
        true, snd (demodulation_goal bag env table newg)
  | None -> do_right ()
;;

type next = L | R 
type solved = Yes of Equality.goal | No of Equality.goal list

(* returns all the 1 step demodulations *)
module C = Cic;; 
module S = CicSubstitution;;
let rec demodulation_all_aux 
  metasenv context ugraph table lift_amount term 
=
  let candidates = 
    get_candidates ~env:(metasenv,context,ugraph) Matching table term 
  in
  match term with
  | C.Meta _ -> []
  | _ ->
      let termty, ugraph = C.Implicit None, ugraph in
      let res =
        find_all_matches 
          metasenv context ugraph lift_amount term termty candidates
      in
      match term with
      | C.Appl l ->
         let res, _, _ = 
           List.fold_left
            (fun (res,l,r) t ->
               res @ 
               List.map 
                 (fun (rel, s, m, ug, c) -> 
                   (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
                 (demodulation_all_aux 
                   metasenv context ugraph table lift_amount t),
               l@[List.hd r], List.tl r)
            (res, [], List.map (S.lift 1) l) l
         in
         res
      | C.Prod (nn, s, t) 
      | C.Lambda (nn, s, t) ->
          let context = (Some (nn, C.Decl s))::context in
          let mk s t = 
            match term with 
            | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
          in
          res @ 
          List.map
            (fun (rel, subst, m, ug, c) -> 
               mk (S.lift 1 s) rel, subst, m, ug, c)
            (demodulation_all_aux
              metasenv context ugraph table (lift_amount+1) t)
              (* we could demodulate also in s, but then t may be badly
               * typed... *)
      | t -> res
;;

let solve_demodulating bag env table initgoal steps =
  let _, context, ugraph = env in
  let solved goal res side = 
    let newg = build_newgoal bag context goal side Equality.Demodulation res in
    match newg with
    | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) 
      when LibraryObjects.is_eq_URI uri ->
        (try 
          let _ = 
            Founif.unification m m context left right CicUniv.empty_ugraph 
          in
          Yes newg
        with CicUnification.UnificationFailure _ -> No [newg])
    | _ -> No [newg]
  in
  let solved goal res_list side = 
    let newg = List.map (fun x -> solved goal x side) res_list in
    try
      List.find (function Yes _ -> true | _ -> false) newg
    with Not_found -> 
      No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
  in
  let rec first f l =
    match l with
    | [] -> None
    | x::tl -> 
       match f x with
       | None -> first f tl
       | Some x as ok -> ok
  in
  let rec aux steps next goal = 
    if steps = 0 then None else
    let goalproof,menv,_,_,left,right = open_goal goal in
    let do_step t = 
      demodulation_all_aux menv context ugraph table 0 t
    in
    match next with
    | L -> 
        (match do_step left with
        | _::_ as res -> 
            (match solved goal res Utils.Right with
            | No newgoals -> 
                 (match first (aux (steps - 1) L) newgoals with
                 | Some g as success -> success
                 | None -> aux steps R goal)
            | Yes newgoal -> Some newgoal)
        | [] -> aux steps R goal)
    | R -> 
        (match do_step right with
        | _::_ as res -> 
            (match solved goal res Utils.Left with
            | No newgoals -> 
                 (match first (aux (steps - 1) L) newgoals with
                 | Some g as success -> success
                 | None -> None)
            | Yes newgoal -> Some newgoal)
        | [] -> None) 
  in
  aux steps L initgoal
;;

let get_stats () = "" ;;