(* 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 debug_print = Utils.debug_print;;


type retrieval_mode = Matching | Unification;;


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


let indexing_retrieval_time = ref 0.;;


let apply_subst = CicMetaSubst.apply_subst



(*
(* NO INDEXING *)
let init_index () = ()
  
let empty_table () = []

let index table equality =
  let _, _, (_, l, r, ordering), _, _ = equality in
  match ordering with
  | Utils.Gt -> (Utils.Left, equality)::table
  | Utils.Lt -> (Utils.Right, equality)::table
  | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
;;

let remove_index table equality =
  List.filter (fun (p, e) -> e != equality) table
;;

let in_index table equality =
  List.exists (fun (p, e) -> e == equality) table
;;

let get_candidates mode table term = table
*)


(*
(* PATH INDEXING *)
let init_index () = ()

let empty_table () =
  Path_indexing.PSTrie.empty
;;

let index = Path_indexing.index
and remove_index = Path_indexing.remove_index
and in_index = Path_indexing.in_index;;
  
let get_candidates mode trie term =
  let t1 = Unix.gettimeofday () in
  let res = 
    let s = 
      match mode with
      | Matching -> Path_indexing.retrieve_generalizations trie term
      | Unification -> Path_indexing.retrieve_unifiables trie term
(*       Path_indexing.retrieve_all trie term *)
    in
    Path_indexing.PosEqSet.elements s
  in
(*   print_candidates mode term res; *)
  let t2 = Unix.gettimeofday () in
  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
  res
;;
*)


(* DISCRIMINATION TREES *)
let init_index () =
  Hashtbl.clear Discrimination_tree.arities;
;;

let empty_table () =
  Discrimination_tree.DiscriminationTree.empty
;;

let index = Discrimination_tree.index
and remove_index = Discrimination_tree.remove_index
and in_index = Discrimination_tree.in_index;;

let get_candidates mode tree term =
  let t1 = Unix.gettimeofday () in
  let res =
    let s = 
      match mode with
      | Matching -> Discrimination_tree.retrieve_generalizations tree term
      | Unification -> Discrimination_tree.retrieve_unifiables tree term
    in
    Discrimination_tree.PosEqSet.elements s
  in
(*   print_candidates mode term res; *)
(*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
(*   print_newline (); *)
  let t2 = Unix.gettimeofday () in
  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
  res
;;


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
*)
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, (_, proof, (ty, left, right, o), metas, args) = candidate in
        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
            in
            Some (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
              do_match c eq_URI
            with Inference.MatchingFailure ->
              find_matches metasenv context ugraph lift_amount term termty tl
          else
            let res =
              try do_match c eq_URI
              with Inference.MatchingFailure -> None
            in
            match res with
            | Some (_, s, _, _, _) ->
                let c' = apply_subst s c
                and other' = apply_subst s other in
                let order = cmp c' other' in
                let names = U.names_of_context context 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, (_, _, (ty, left, right, o), metas, args) = candidate in
        let do_match c eq_URI =
          let subst', metasenv', ugraph' =
            let t1 = Unix.gettimeofday () in
            try
              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
                let names = U.names_of_context context 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
;;


(*
  returns true if target is subsumed by some equality in table
*)
let subsumption env table target =
  let _, _, (ty, left, right, _), tmetas, _ = target in
  let metasenv, context, ugraph = env in
  let metasenv = metasenv @ tmetas in
  let samesubst subst subst' =
    let tbl = Hashtbl.create (List.length subst) in
    List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
    List.for_all
      (fun (m, (c, t1, t2)) ->
         try
           let c', t1', t2' = Hashtbl.find tbl m in
           if (c = c') && (t1 = t1') && (t2 = t2') then true
           else false
         with Not_found ->
           true)
      subst'
  in
  let leftr =
    match left with
    | Cic.Meta _ -> []
    | _ ->
        let leftc = get_candidates Matching table left in
        find_all_matches ~unif_fun:Inference.matching
          metasenv context ugraph 0 left ty leftc
  in
  let rec ok what = function
    | [] -> false, []
    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
        try
          let other = if pos = Utils.Left then r else l in
          let subst', menv', ug' =
            let t1 = Unix.gettimeofday () in
            try
              let r = 
                Inference.matching (metasenv @ menv @ m) context what other 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
          in
          if samesubst subst subst' then
            true, subst
          else
            ok what tl
        with Inference.MatchingFailure ->
          ok what tl
  in
  let r, subst = ok right leftr in
  let r, s =
    if r then
      true, subst
    else
      let rightr =
	match right with
	  | Cic.Meta _ -> []
	  | _ ->
              let rightc = get_candidates Matching table right in
		find_all_matches ~unif_fun:Inference.matching
		  metasenv context ugraph 0 right ty rightc
      in
	ok left rightr
  in
    (if r then 
       debug_print 
	 (lazy
	    (Printf.sprintf "SUBSUMPTION! %s\n%s\n"
	       (Inference.string_of_equality target) (Utils.print_subst s))));
    r, s
;;


let rec demodulation_aux ?(typecheck=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 candidates = get_candidates Matching table term in
  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 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 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 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
;;


let build_newtarget_time = ref 0.;;


let demod_counter = ref 1;;

(** demodulation, when target is an equality *)
let rec demodulation_equality 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 metasenv, context, ugraph = env in
  let _, proof, (eq_ty, left, right, order), metas, args = target in
  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
    
    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found 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 = apply_subst subst (S.subst other t) in
      let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) 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,
         Inference.ProofBlock (
           subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
      else
        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' =
              let termlist =
                if pos = Utils.Left then [ty; what; other]
                else [ty; other; what]
              in
              Inference.ProofSymBlock (termlist, proof')
            in
            let what, other =
              if pos = Utils.Left then what, other else other, what
            in
            pos, (0, proof', (ty, other, what, Utils.Incomparable),
                  menv', args')
          in
          let target_proof =
            let pb =
              Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
                                    eq_found, Inference.BasicProof metaproof)
            in
            match proof with
            | Inference.BasicProof _ ->
                print_endline "replacing a BasicProof";
                pb
            | Inference.ProofGoalBlock (_, parent_proof) ->
                print_endline "replacing another ProofGoalBlock";
                Inference.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,
         Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
    in
    let left, right = if is_left then newterm, right else left, newterm in
    let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
    let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
    and newargs = args
    in
    let ordering = !Utils.compare_terms left right in

    let time2 = Unix.gettimeofday () in
    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);

    let res =
      let w = Utils.compute_equality_weight eq_ty left right in
      (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
    in
    !maxmeta, res
  in
  let res = demodulation_aux metasenv' context ugraph table 0 left in
  let newmeta, newtarget = 
    match res with
    | Some t ->
	let newmeta, newtarget = build_newtarget true t in
	  if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
            (Inference.meta_convertibility_eq target newtarget) then
	      newmeta, newtarget
	  else
            demodulation_equality newmeta env table sign newtarget
    | None ->
	let res = demodulation_aux metasenv' context ugraph table 0 right in
	  match res with
	  | Some t ->
	      let newmeta, newtarget = build_newtarget false t in
		if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
		  (Inference.meta_convertibility_eq target newtarget) then
		    newmeta, newtarget
		else
		  demodulation_equality newmeta env table sign newtarget
	  | None ->
	      newmeta, target
  in
  (* newmeta, newtarget *)
  (* tentiamo di ridurre usando CicReduction.normalize *)
  let w, p, (ty, left, right, o), m, a = newtarget in
  let left' = ProofEngineReduction.simpl context left in
  let right' = ProofEngineReduction.simpl context right in
  let newleft =
    if !Utils.compare_terms left' left = Utils.Lt then left' else left in
  let newright = 
    if !Utils.compare_terms right' right = Utils.Lt then right' else right in
  if newleft != left || newright != right then (
    debug_print
      (lazy
	 (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n"
	    (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right)
	    (CicPp.ppterm right')))
  );
  let w' = Utils.compute_equality_weight ty newleft newright in
  let o' = !Utils.compare_terms newleft newright in
  newmeta, (w', p, (ty, newleft, newright, o'), m, a)
;;


(**
   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 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 superposition_left 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 weight, proof, (eq_ty, left, right, ordering), _, _ = target in
  let expansions, _ =
    let term = if ordering = U.Gt then left else right in
    betaexpand_term metasenv context ugraph table 0 term
  in
  let maxmeta = ref newmeta in
  let build_new (bo, s, m, ug, (eq_found, eq_URI)) =

    debug_print (lazy "\nSUPERPOSITION LEFT\n");

    let time1 = Unix.gettimeofday () in
    
    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
    let what, other = if pos = Utils.Left then what, other else other, what in
    let newgoal, newproof =
      let bo' = apply_subst s (S.subst other bo) in
      let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
      incr sup_l_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
      incr maxmeta;
      let metaproof =
        let irl =
          CicMkImplicit.identity_relocation_list_for_metavariable context in
        C.Meta (!maxmeta, irl)
      in
      let eq_found =
        let proof' =
          let termlist =
            if pos = Utils.Left then [ty; what; other]
            else [ty; other; what]
          in
          Inference.ProofSymBlock (termlist, proof')
        in
        let what, other =
          if pos = Utils.Left then what, other else other, what
        in
        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
      in
      let target_proof =
        let pb =
          Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
                                Inference.BasicProof metaproof)
        in
        match proof with
        | Inference.BasicProof _ ->
            debug_print (lazy "replacing a BasicProof");
            pb
        | Inference.ProofGoalBlock (_, parent_proof) ->
            debug_print (lazy "replacing another ProofGoalBlock");
            Inference.ProofGoalBlock (pb, parent_proof)
        | _ -> assert false
      in
      let refl =
        C.Appl [C.MutConstruct (* reflexivity *)
                  (LibraryObjects.eq_URI (), 0, 1, []);
                eq_ty; if ordering = U.Gt then right else left]
      in
      (bo',
       Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
    in
    let left, right =
      if ordering = U.Gt then newgoal, right else left, newgoal in
    let neworder = !Utils.compare_terms left right in

    let time2 = Unix.gettimeofday () in
    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);

    let res =
      let w = Utils.compute_equality_weight eq_ty left right in
      (w, newproof, (eq_ty, left, right, neworder), [], [])
    in
    res
  in
  !maxmeta, List.map build_new 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 _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
  let metasenv' = metasenv @ newmetas in
  let maxmeta = ref newmeta in
  let res1, res2 =
    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)) =

    let time1 = Unix.gettimeofday () in
    
    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
    let what, other = if pos = Utils.Left then what, other else other, what in
    let newgoal, newproof =
      let bo' = apply_subst s (S.subst other bo) in
      let t' =
        let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
        incr sup_r_counter;
        let l, r =
          if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
        (name, ty, S.lift 1 eq_ty, l, r)
      in
      let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) 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',
      Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
    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 
      and newmenv = newmetas @ menv'
      and newargs = args @ args' in
      let eq' =
        let w = Utils.compute_equality_weight eq_ty left right in
        (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
      and env = (metasenv, context, ugraph) in
      let newm, eq' = Inference.fix_metas !maxmeta eq' in
      newm, eq'
    in
    maxmeta := newmeta;

    let time2 = Unix.gettimeofday () in
    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);

    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 (Inference.is_identity (metasenv, context, ugraph) e) in
  (!maxmeta,
   (List.filter ok (new1 @ new2)))
;;


(** demodulation, when the target is a goal *)
let rec demodulation_goal newmeta env table goal =
  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 proof, metas, term = goal in
  let metasenv' = metasenv @ metas in

  let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
    let what, other = if pos = Utils.Left then what, other else other, what in
    let ty =
      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
      with CicUtil.Meta_not_found _ -> ty
    in
    let newterm, newproof =
      let bo = apply_subst subst (S.subst other t) in
      let bo' = apply_subst subst t in 
      let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
      incr demod_counter;
      let metaproof = 
        incr maxmeta;
        let irl =
          CicMkImplicit.identity_relocation_list_for_metavariable context in
        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
        C.Meta (!maxmeta, irl)
      in
      let eq_found =
        let proof' =
          let termlist =
            if pos = Utils.Left then [ty; what; other]
            else [ty; other; what]
          in
          Inference.ProofSymBlock (termlist, proof')
        in
        let what, other =
          if pos = Utils.Left then what, other else other, what
        in
        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
      in
      let goal_proof =
        let pb =
          Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
                                eq_found, Inference.BasicProof metaproof)
        in
        let rec repl = function
          | Inference.NoProof ->
              debug_print (lazy "replacing a NoProof");
              pb
          | Inference.BasicProof _ ->
              debug_print (lazy "replacing a BasicProof");
              pb
          | Inference.ProofGoalBlock (_, parent_proof) ->
              debug_print (lazy "replacing another ProofGoalBlock");
              Inference.ProofGoalBlock (pb, parent_proof)
          | (Inference.SubProof (term, meta_index, p) as subproof) ->
              debug_print
                (lazy
                   (Printf.sprintf "replacing %s"
                      (Inference.string_of_proof subproof)));
              Inference.SubProof (term, meta_index, repl p)
          | _ -> assert false
        in repl proof
      in
      bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
    in
    let m = Inference.metas_of_term newterm in
    let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
    !maxmeta, (newproof, newmetasenv, newterm)
  in  
  let res =
    demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
  in
  match res with
  | Some t ->
      let newmeta, newgoal = build_newgoal t in
      let _, _, newg = newgoal in
      if Inference.meta_convertibility term newg then
        newmeta, newgoal
      else
        demodulation_goal newmeta env table newgoal
  | None ->
      newmeta, goal
;;


(** 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 proof, metas, term = theorem in
  let term, termty, metas = theorem in
  let metasenv' = metasenv @ metas in

  let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
    let what, other = if pos = Utils.Left then what, other else other, what in
    let newterm, newty =
      let bo = 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 newproof =
        Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
                              Inference.BasicProof term)
      in
      (Inference.build_proof_term newproof, bo)
    in
    let m = Inference.metas_of_term newterm in
    let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
    !maxmeta, (newterm, newty, newmetasenv)
  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 Inference.meta_convertibility termty newty then
        newmeta, newthm
      else
        demodulation_theorem newmeta env table newthm
  | None ->
      newmeta, theorem
;;