(* 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$ *)

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 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 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 s = 
    match mode with
    | Matching -> 
        let _ = <:start<retrieve_generalizations>> in
        <:stop<retrieve_generalizations
        Index.retrieve_generalizations tree term
        >>
    | Unification -> 
        let _ = <:start<retrieve_unifiables>> in
        <:stop<retrieve_unifiables
        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 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 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 =
            let subst', metasenv', ugraph' =
              Inference.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 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 
              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
;;

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 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 =
          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
          | 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 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 
=
    find_all_matches 
      ?unif_fun metasenv context ugraph lift_amount term termty l 
  (*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));*)
;;
(*
  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 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
  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 
        | Inference.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 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
;;

exception Foo

(** demodulation, when target is an equality *)
let rec demodulation_equality ?from eq_uri 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) =
    
    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
      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
      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 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 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 eq_uri 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 eq_uri 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 
  ?(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 
  ?(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 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 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 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 = (* 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;
    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 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) =
    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 (* ~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
;;

(*****************************************************************************)
(**                         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 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 name = Cic.Name "x" in
    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
    bo, (newgoalproofstep::goalproof)
  in
  let newmetasenv = (* Inference.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 (metasenv, context, ugraph) table goal = 
  let proof,menv,eq,ty,l,r = open_goal goal in
  let c = !Utils.compare_terms l r in
  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 context goal Utils.Right Equality.SuperpositionLeft) expansionsl
    @
    List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
    end
  else
    let big,small,possmall = 
      match c with 
        Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right 
      | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left
      | _ -> assert false
    in
    let expansions, _ = betaexpand_term menv context ugraph table 0 big in
    List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
;;

(** demodulation, when the target is a goal *)
let rec demodulation_goal 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 menv context ugraph table 0 right in
      match resright with
      | Some t ->
          let newg = 
            build_newgoal context goal Utils.Left Equality.Demodulation 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 menv context ugraph table 0 left in
  match resleft with
  | Some t ->
      let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
      if goal_metaconvertibility_eq goal newg then
        do_right ()
      else
        true, snd (demodulation_goal env table newg)
  | None -> do_right ()
;;

let get_stats () = <:show<Indexing.>> ;;