(* 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/.
 *)

(* $Id$ *)

type goal = Equality.goal_proof * Cic.metasenv * Cic.term

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

let beta_expand_time = ref 0.;;

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), eq_URI)) ->
        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 indexing_retrieval_time = ref 0.;;


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, eq_URI)) ->
        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 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 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 (Inference.build_proof_term proof) CicUniv.empty_ugraph)
  with e ->  
      prerr_endline msg;
      prerr_endline (Inference.string_of_proof proof);
      prerr_endline (CicPp.ppterm (Inference.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 t1 = Unix.gettimeofday () in
  let res =
    let s = 
      match mode with
      | Matching -> Index.retrieve_generalizations tree term
      | Unification -> Index.retrieve_unifiables tree term
    in
    Index.PosEqSet.elements s
  in
(*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
(*   print_newline (); *)
  let t2 = Unix.gettimeofday () in
  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1); 
 (* make fresh instances *)
  res 
;;

let profiler = HExtlib.profile "P/Indexing.get_candidates"

let get_candidates ?env mode tree term =
  profiler.HExtlib.profile (get_candidates ?env mode tree) term

let match_unif_time_ok = ref 0.;;
let match_unif_time_no = ref 0.;;


(*
  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 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
        prerr_endline (". " ^ Equality.string_of_equality equality);
        let (_, proof, (ty, left, right, o), metas,_) = 
          Equality.open_equality equality 
        in
        if Utils.debug_metas then 
          ignore(check_target 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 metasenv context ugraph lift_amount term termty tl
        ) else
          let do_match c eq_URI =
            let subst', metasenv', ugraph' =
              let t1 = Unix.gettimeofday () in
              try
                let r =
                  ( Inference.matching metasenv metas context 
                    term (S.lift lift_amount c)) ugraph
                in
                let t2 = Unix.gettimeofday () in
                match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
                r
              with 
                | Inference.MatchingFailure as e ->
                let t2 = Unix.gettimeofday () in
                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                  raise e
                | CicUtil.Meta_not_found _ as exn -> raise exn
            in
            Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
                  (candidate, eq_URI))
          in
          let c, other, eq_URI =
            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
            else right, left, Utils.eq_ind_r_URI ()
          in
          if o <> U.Incomparable then
            let res =
              try
                do_match c eq_URI
              with Inference.MatchingFailure ->
                find_matches 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 eq_URI
              with Inference.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
                    metasenv context ugraph lift_amount term termty tl
            | None ->
                find_matches metasenv context ugraph lift_amount term termty tl
;;

(*
  as above, but finds all the matching equalities, and the matching condition
  can be either Inference.matching or Inference.unification
*)
let rec find_all_matches ?(unif_fun=Inference.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 eq_URI =
          let subst', metasenv', ugraph' =
            let t1 = Unix.gettimeofday () in
            try
                let term = 
                  match c,term with
                  | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r] 
                    when  LibraryObjects.is_eq_URI u -> l
(*
                      if Utils.compare_weights (Utils.weight_of_term l)
                         (Utils.weight_of_term r) = Utils.Gt 
                      then l else r
*)
                  | _ -> term
                in
              
              let r = 
                unif_fun metasenv metas context
                  term (S.lift lift_amount c) ugraph in
              let t2 = Unix.gettimeofday () in
              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
              r
            with
            | Inference.MatchingFailure
            | CicUnification.UnificationFailure _
            | CicUnification.Uncertain _ as e ->
                let t2 = Unix.gettimeofday () in
                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                raise e
          in
          (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
           (candidate, eq_URI))
        in
        let c, other, eq_URI =
          if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
          else right, left, Utils.eq_ind_r_URI ()
        in
        if o <> U.Incomparable then
          try
            let res = do_match c eq_URI in
            res::(find_all_matches ~unif_fun metasenv context ugraph
                    lift_amount term termty tl)
          with
          | Inference.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 eq_URI 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
          | Inference.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 
=
  let rc = 
    find_all_matches 
      ?unif_fun metasenv context ugraph lift_amount term termty l 
  in
  (*prerr_endline "CANDIDATES:";
  List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
  prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
  (List.length rc));*)
  rc

(*
  returns true if target is subsumed by some equality in table
*)
let subsumption_aux use_unification env table target = 
(*  let print_res l =*)
(*    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
(*    ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
(*  in*)
  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
  let metasenv, context, ugraph = env in
  let metasenv = tmetas in
  let predicate, unif_fun = 
    if use_unification then
      Unification, Inference.unification
    else
      Matching, Inference.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
(*  print_res leftr;*)
  let rec ok what = 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 subst', menv', ug' =
            unif_fun metasenv m context what' other ugraph
          in
          (match Subst.merge_subst_if_possible subst subst' with
          | None -> ok what tl
          | Some s -> Some (s, equation))
        with 
        | Inference.MatchingFailure 
        | CicUnification.UnificationFailure _ -> ok what tl
  in
  match ok right 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
(*        print_res rightr;*)
        ok left rightr
(*     (if r then  *)
(*        debug_print  *)
(*          (lazy *)
(*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
(*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
;;

let subsumption = subsumption_aux false;;
let unification = subsumption_aux true;;

let rec demodulation_aux ?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 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 ~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 ~from:"2"
                        metasenv context ugraph table lift_amount s in (
                        match r1 with
                          | None ->
                              let r2 =
                                demodulation_aux 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 
                        metasenv context ugraph table lift_amount s in (
                        match r1 with
                          | None ->
                              let r2 =
                                demodulation_aux 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
;;


let build_newtarget_time = ref 0.;;


let demod_counter = ref 1;;

exception Foo

let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"

(** demodulation, when target is an equality *)
let rec demodulation_equality ?from newmeta env table sign 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 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, eq_URI)) =
    let time1 = Unix.gettimeofday () in
    
    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 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 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
      incr demod_counter;
      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 (LibraryObjects.eq_URI (), 0, []);
                  S.lift 1 eq_ty; l; r]
      in
      if sign = Utils.Positive then
          (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
          (Cic.Lambda (name, ty, bo'))))))
      else
        assert false
(*
        begin
        prerr_endline "***************************************negative";
        let metaproof = 
          incr maxmeta;
          let irl =
            CicMkImplicit.identity_relocation_list_for_metavariable context in
(*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
(*        print_newline (); *)
          C.Meta (!maxmeta, irl)
        in
          let eq_found =
            let proof'_old' =
              let termlist =
                if pos = Utils.Left then [ty; what; other]
                else [ty; other; what]
              in
              Equality.ProofSymBlock (termlist, proof'_old)
            in
            let proof'_new' = assert false (* not implemented *) in
            let what, other =
              if pos = Utils.Left then what, other else other, what
            in
            pos, 
              Equality.mk_equality 
                (0, (proof'_new',proof'_old'), 
                (ty, other, what, Utils.Incomparable),menv')
          in
          let target_proof =
            let pb =
              Equality.ProofBlock 
                (subst, eq_URI, (name, ty), bo',
                 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
            in
            assert false, (* not implemented *)
            (match snd proof with
            | Equality.BasicProof _ ->
                (* print_endline "replacing a BasicProof"; *)
                pb
            | Equality.ProofGoalBlock (_, parent_proof) ->
  (* print_endline "replacing another ProofGoalBlock"; *)
                Equality.ProofGoalBlock (pb, parent_proof)
            | _ -> assert false)
          in
        let refl =
          C.Appl [C.MutConstruct (* reflexivity *)
                    (LibraryObjects.eq_URI (), 0, 1, []);
                  eq_ty; if is_left then right else left]          
        in
        (bo,
         (assert false, (* not implemented *)
         Equality.ProofGoalBlock 
           (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
      end
*)
    in
    let newmenv = (* Inference.filter subst *) menv in
    let _ = 
      if Utils.debug_metas then 
        try ignore(CicTypeChecker.type_of_aux'
          newmenv context 
            (Equality.build_proof_term newproof) ugraph);
          () 
        with exc ->                   
          prerr_endline "sempre lui";
          prerr_endline (Subst.ppsubst subst);
          prerr_endline (CicPp.ppterm 
            (Equality.build_proof_term newproof));
          prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
          prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
          prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
          prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
            newmenv));
          raise exc;
      else () 
    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 time2 = Unix.gettimeofday () in
    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
    let res =
      let w = Utils.compute_equality_weight stat in
      Equality.mk_equality (w, newproof, stat,newmenv) 
    in
    if Utils.debug_metas then 
      ignore(check_target context res "buildnew_target output");
    !maxmeta, res 
  in
  let build_newtarget is_left x =
    profiler.HExtlib.profile (build_newtarget is_left) x
  in

  let res = demodulation_aux ~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 ?from newmeta env table sign newtarget
    | None ->
        let res = demodulation_aux 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 ?from newmeta env table sign 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 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 candidates = get_candidates Unification table term in
  
  let res, lifted_term = 
    match term with
    | 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 =
                     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_right
            (fun arg (res, lifted_tl) ->
               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)
            ) 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 r = 
        find_all_matches
          metasenv context ugraph lift_amount term termty candidates
      in
      r @ res, lifted_term
;;

let profiler = HExtlib.profile "P/Indexing.betaexpand_term"

let betaexpand_term metasenv context ugraph table lift_amount term =
  profiler.HExtlib.profile 
    (betaexpand_term metasenv context ugraph table lift_amount) term


let sup_l_counter = ref 1;;

(**
   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 fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) = 
  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)
;;
  
let build_newgoal context goalproof goal_info expansion =
  let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info 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 name = Cic.Name "x" in
    let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
    bo, (newgoalproofstep::goalproof)
  in
  let newmetasenv = (* Inference.filter subst *) menv in
  (newgoalproof, newmetasenv, newterm)
;;

let superposition_left 
  (metasenv, context, ugraph) table (proof,menv,ty)
= 
  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 big,small,pos,eq,ty = 
    match ty with
    | Cic.Appl [eq;ty;l;r] ->
       let c = 
         Utils.compare_weights ~normalize:true
           (Utils.weight_of_term l) (Utils.weight_of_term r)
       in
       (match c with 
       | Utils.Gt -> l,r,Utils.Right,eq,ty
       | _ -> r,l,Utils.Left,eq,ty)
    | _ -> 
        let names = Utils.names_of_context context in 
        prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
        assert false
  in
  let expansions, _ = betaexpand_term menv context ugraph table 0 big in
  List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
;;

let sup_r_counter = ref 1;;

(**
   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 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 context target "superpositionright");
  let metasenv' = newmetas in
  let maxmeta = ref newmeta in
  let res1, res2 =
    let betaexpand_term metasenv context ugraph table d term =
      let t1 = Unix.gettimeofday () in
      let res = betaexpand_term metasenv context ugraph table d term in
      let t2 = Unix.gettimeofday () in
        beta_expand_time := !beta_expand_time  +. (t2 -. t1);
        res
    in
    match ordering with
    | U.Gt -> 
        fst (betaexpand_term metasenv' context ugraph table 0 left), []
    | U.Lt -> 
        [], fst (betaexpand_term 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 metasenv' context ugraph table 0 l))
        in
        (res left right), (res right left)
  in
  let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
    if Utils.debug_metas then 
      ignore (check_target context (snd eq_found) "buildnew1" );
    let time1 = Unix.gettimeofday () 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 newgoal, newproof =
      (* qua *)
      let bo' =
        Utils.guarded_simpl context (apply_subst s (S.subst other bo)) 
      in
      let name = C.Name "x" in
      incr sup_r_counter;
      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 (LibraryObjects.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 = (* Inference.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 (w, newproof, stat, newmenv) in
      if Utils.debug_metas then 
        ignore (check_target context eq' "buildnew3");
      let newm, eq' = Equality.fix_metas !maxmeta eq' in
      if Utils.debug_metas then 
        ignore (check_target context eq' "buildnew4");
      newm, eq'
    in
    maxmeta := newmeta;
    let time2 = Unix.gettimeofday () in
    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
    if Utils.debug_metas then 
      ignore(check_target 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 goal *)
let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) = 
  Equality.meta_convertibility g1 g2
;;

let rec demodulation_goal env table goal =
  let metasenv, context, ugraph = env in
  let goalproof, metas, term = goal in
  let term = Utils.guarded_simpl (~debug:true) context term in
  let goal = goalproof, metas, term in
  let metasenv' = metas in

  let left,right,eq,ty = 
    match term with
    | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
    | _ -> assert false
  in
  let do_right () = 
      let resright = demodulation_aux metasenv' context ugraph table 0 right in
      match resright with
      | Some t ->
          let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
          if goal_metaconvertibility_eq goal newg then
            false, goal
          else
            true, snd (demodulation_goal env table newg)
      | None -> false, goal
  in
  let resleft =
    demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
  in
  match resleft with
  | Some t ->
      let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
      if goal_metaconvertibility_eq goal newg then
        do_right ()
      else
        true, snd (demodulation_goal env table newg)
  | None -> do_right ()
;;

(** demodulation, when the target is a theorem *)
let rec demodulation_theorem 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, eq_URI)) =
    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*)
      incr demod_counter;
(*
      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 (* ~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 newmeta env table newthm
  | None ->
      newmeta, theorem
;;