(* Copyright (C) 2002, 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/.
 *)

open AutoTypes;;
open AutoCache;;

let debug = false;;
let debug_print s = 
  if debug then () else prerr_endline (Lazy.force s);;

(* functions for retrieving theorems *)

exception FillingFailure of AutoCache.cache * int

let rec unfold context = function
  | Cic.Prod(name,s,t) -> 
      let t' = unfold ((Some (name,Cic.Decl s))::context) t in
	Cic.Prod(name,s,t')	
  | t -> ProofEngineReduction.unfold context t

let find_library_theorems dbd proof goal = 
  let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
  let terms = List.map CicUtil.term_of_uri univ in
  List.map 
    (fun t -> 
       (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph))) 
    terms

let find_context_theorems context metasenv =
  let l,_ =
    List.fold_left
      (fun (res,i) ctxentry ->
	 match ctxentry with
	   | Some (_,Cic.Decl t) -> 
               (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
	   | Some (_,Cic.Def (_,Some t)) ->
               (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
	   | Some (_,Cic.Def (_,None)) ->
	       let t = Cic.Rel i in
	       let ty,_ = 
		 CicTypeChecker.type_of_aux' 
		   metasenv context t CicUniv.empty_ugraph
               in
		 (t,ty)::res,i+1
	   |  _ -> res,i+1)
      ([],1) context
  in l

let rec is_an_equality = function
  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] 
    when (LibraryObjects.is_eq_URI uri) -> true
  | Cic.Prod (_, _, t) -> is_an_equality t
  | _ -> false
;;

let partition_equalities =
  List.partition (fun (_,ty) -> is_an_equality ty)


let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; 


let is_unit_equation context metasenv oldnewmeta term = 
  let head, metasenv, args, newmeta =
    ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
  in
  let propositional_args = 
    HExtlib.filter_map
      (function 
      | Cic.Meta(i,_) -> 
          let _,_,mt = CicUtil.lookup_meta i metasenv in
          let sort,u = 
            CicTypeChecker.type_of_aux' metasenv context mt 
              CicUniv.empty_ugraph
          in
          let b, _ = 
            CicReduction.are_convertible ~metasenv context 
              sort (Cic.Sort Cic.Prop) u
          in
	  if b then Some i else None 
      | _ -> assert false)
    args
  in
    if propositional_args = [] then 
      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
	Some (args,metasenv,newmetas,head,newmeta)
    else None
;;

let get_candidates universe cache t =
  let candidates= 
    (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
  in 
  let debug_msg =
    (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^ 
	     (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
  debug_print debug_msg;
  candidates
;;

let only signature context t =
  try
    let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
    let consts = MetadataConstraints.constants_of ty in
    let b = MetadataConstraints.UriManagerSet.subset consts signature in
    if b then b 
    else
      try
	let ty' = unfold context ty in
	let consts' = MetadataConstraints.constants_of ty' in
	MetadataConstraints.UriManagerSet.subset consts' signature 
      with _-> false
  with _ -> false
;;

let not_default_eq_term t =
  try
    let uri = CicUtil.uri_of_term t in
      not (LibraryObjects.in_eq_URIs uri)
  with Invalid_argument _ -> true

let retrieve_equations signature universe cache context=
  match LibraryObjects.eq_URI() with
    | None -> [] 
    | Some eq_uri -> 
	let eq_uri = UriManager.strip_xpointer eq_uri in
	let fake= Cic.Meta(-1,[]) in
	let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
	let candidates = get_candidates universe cache fake_eq in
    (* defaults eq uris are built-in in auto *)
        let candidates = List.filter not_default_eq_term candidates in
	let candidates = List.filter (only signature context) candidates in
	List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
	candidates

let build_equality bag head args proof newmetas maxmeta = 
  match head with
  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
      let p =
        if args = [] then proof else Cic.Appl (proof::args)
      in 
      let o = !Utils.compare_terms t1 t2 in
      let stat = (ty,t1,t2,o) in
      (* let w = compute_equality_weight stat in *)
      let w = 0 in 
      let proof = Equality.Exact p in
      let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
      (* to clean the local context of metas *)
      Equality.fix_metas bag maxmeta e
  | _ -> assert false
;;

let partition_unit_equalities context metasenv newmeta bag equations =
  List.fold_left
    (fun (units,other,maxmeta)(t,ty) ->
       match is_unit_equation context metasenv maxmeta ty with
	 | Some (args,metasenv,newmetas,head,newmeta') ->
	     let maxmeta,equality =
	       build_equality bag head args t newmetas newmeta' in
	     equality::units,other,maxmeta
	 | None -> 
	     units,(t,ty)::other,maxmeta)
    ([],[],newmeta) equations

let empty_tables = 
  (Saturation.make_active [], 
   Saturation.make_passive [],
   Equality.mk_equality_bag)

let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
  (* the local cache in initially empty  *)
  let cache = AutoCache.cache_empty in
  let _, metasenv, _, _ = proof in
  let signature = MetadataQuery.signature_of metasenv goal in
  let newmeta = CicMkImplicit.new_meta metasenv [] in
  let _,context,_ = CicUtil.lookup_meta goal metasenv in
  let ct = find_context_theorems context metasenv in
  prerr_endline 
    ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
  let lt = 
    if use_library then 
       find_library_theorems dbd metasenv goal 
    else [] in
  prerr_endline 
    ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
  let cache = cache_add_list cache context (ct@lt) in  
  let equations = 
    retrieve_equations signature universe cache context in
  prerr_endline 
    ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
  let eqs_and_types =
    HExtlib.filter_map 
      (fun t -> 
	 let ty,_ =
	   CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
           (* retrieve_equations could also return flexible terms *)
	   if is_an_equality ty then Some(t,ty) 
	   else
	     try
               let ty' = unfold context ty in
		 if is_an_equality ty' then Some(t,ty') else None
             with _ -> None) (* catturare l'eccezione giusta di unfold *)
      equations in
  let bag = Equality.mk_equality_bag () in
  let units, other_equalities, newmeta = 
    partition_unit_equalities context metasenv newmeta bag eqs_and_types in
  (* let env = (metasenv, context, CicUniv.empty_ugraph) in 
    let equalities = 
    let eq_uri = 
    match LibraryObjects.eq_URI() with
      | None ->assert false
      | Some eq_uri -> eq_uri in
    Saturation.simplify_equalities bag eq_uri env units in *)
  let passive = Saturation.make_passive units in
  let no = List.length units in
  let active = Saturation.make_active [] in
  let active,passive,newmeta = 
    if paramod then active,passive,newmeta
    else
      Saturation.pump_actives 
	context bag newmeta active passive (no+1) infinity
  in 
    (active,passive,bag),cache,newmeta

let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = 
  let head, metasenv, args, newmeta =
    ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
  in
  let propositional_args = 
    HExtlib.filter_map
      (function 
      | Cic.Meta(i,_) -> 
          let _,_,mt = CicUtil.lookup_meta i metasenv in
          let sort,u = 
            CicTypeChecker.type_of_aux' metasenv context mt 
              CicUniv.empty_ugraph
          in
          let b, _ = 
            CicReduction.are_convertible ~metasenv context 
              sort (Cic.Sort Cic.Prop) u
          in
          if b then Some i else None 
      | _ -> assert false)
    args
  in
  let results,cache,newmeta = 
    if propositional_args = [] then 
      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
      [args,metasenv,newmetas,head,newmeta],cache,newmeta
    else
      (*
      let proof = 
        None,metasenv,term,term (* term non e' significativo *)
      in *)
      let flags = 
        if fast then
          {AutoTypes.default_flags() with 
           AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
           maxwidth = 2;maxdepth = 2;
           use_paramod=true;use_only_paramod=false}
        else
          {AutoTypes.default_flags() with
           AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
           maxwidth = 2;maxdepth = 4;
           use_paramod=true;use_only_paramod=false} 
      in
      match auto newmeta tables universe cache context metasenv propositional_args flags with
      | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
      | substs,cache,newmeta ->
          List.map 
            (fun subst ->
              let metasenv = 
                CicMetaSubst.apply_subst_metasenv subst metasenv
              in
              let head = CicMetaSubst.apply_subst subst head in
              let newmetas = 
                List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv 
              in
              let args = List.map (CicMetaSubst.apply_subst subst) args in
              let newm = CicMkImplicit.new_meta metasenv subst in
		args,metasenv,newmetas,head,max newm newmeta)
            substs, cache, newmeta
  in
  results,cache,newmeta

let build_equalities auto context metasenv tables universe cache newmeta equations =
  List.fold_left 
    (fun (facts,cache,newmeta) (t,ty) ->
       (* in any case we add the equation to the cache *)
       let cache = AutoCache.cache_add_list cache context [(t,ty)] in
       try
         let saturated,cache,newmeta = 
           fill_hypothesis context metasenv newmeta ty tables universe cache auto true
         in
         let (active,passive,bag) = tables in
         let eqs,bag,newmeta = 
           List.fold_left 
             (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
		let maxmeta,equality =
		  build_equality bag head args t newmetas newmeta'
                in
                  equality::acc,bag,maxmeta)
             ([],bag,newmeta) saturated
         in
           (eqs@facts, cache, newmeta)
       with FillingFailure (cache,newmeta) ->
	 (* if filling hypothesis fails we add the equation to
	    the cache *)
	 (facts,cache,newmeta)
      )
    ([],cache,newmeta) equations

let close_more tables maxmeta context status auto universe cache =
  let (active,passive,bag) = tables in
  let proof, goalno = status in
  let _, metasenv,_,_ = proof in  
  let signature = MetadataQuery.signature_of metasenv goalno in
  let equations = retrieve_equations signature universe cache context in
  let eqs_and_types =
    HExtlib.filter_map 
      (fun t -> 
	 let ty,_ =
	   CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
           (* retrieve_equations could also return flexible terms *)
	   if is_an_equality ty then Some(t,ty) else None)
      equations in
  let units, cache, maxm = 
      build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
  prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
    string_of_int maxm);
  List.iter
    (fun e -> prerr_endline (Equality.string_of_equality e)) 
    units;
  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
  let passive = Saturation.add_to_passive units passive in
  let no = List.length units in
  prerr_endline ("No = " ^ (string_of_int no));
  let active,passive,newmeta = 
    Saturation.pump_actives context bag maxm active passive (no+1) infinity
  in 
    (active,passive,bag),cache,newmeta

let find_context_equalities 
  maxmeta bag context proof (universe:Universe.universe) cache 
=
  let module C = Cic in
  let module S = CicSubstitution in
  let module T = CicTypeChecker in
  let _,metasenv,_,_ = proof in
  let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
  (* if use_auto is true, we try to close the hypothesis of equational
    statements using auto; a naif, and probably wrong approach *)
  let rec aux cache index newmeta = function
    | [] -> [], newmeta,cache
    | (Some (_, C.Decl (term)))::tl ->
        debug_print
          (lazy
             (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
        let do_find context term =
          match term with
          | C.Prod (name, s, t) when is_an_equality t ->
              (try 
                
                let term = S.lift index term in
                let saturated,cache,newmeta = 
                  fill_hypothesis context metasenv newmeta term 
                    empty_tables universe cache default_auto false
                in
                let eqs,newmeta = 
                  List.fold_left 
                   (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
                     let newmeta, equality = 
                       build_equality
                         bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
                     in
                     equality::acc, newmeta + 1)
                   ([],newmeta) saturated
                in
                 eqs, newmeta, cache
              with FillingFailure (cache,newmeta) ->
                [],newmeta,cache)
          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
              when LibraryObjects.is_eq_URI uri ->
              let term = S.lift index term in
              let newmeta, e = 
                build_equality bag term [] (Cic.Rel index) [] newmeta
              in
              [e], (newmeta+1),cache
          | _ -> [], newmeta, cache
        in 
        let eqs, newmeta, cache = do_find context term in
        let rest, newmeta,cache = aux cache (index+1) newmeta tl in
        List.map (fun x -> index,x) eqs @ rest, newmeta, cache
    | _::tl ->
        aux cache (index+1) newmeta tl
  in
  let il, maxm, cache = 
    aux cache 1 newmeta context 
  in
  let indexes, equalities = List.split il in
  indexes, equalities, maxm, cache
;;

(***************** applyS *******************)

let new_metasenv_and_unify_and_t 
 dbd flags universe proof goal ?tables newmeta' metasenv' 
 context term' ty termty goal_arity 
=
 let (consthead,newmetasenv,arguments,_) =
   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
 let term'' = 
   match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) 
 in
 let proof',oldmetasenv =
  let (puri,metasenv,pbo,pty) = proof in
   (puri,newmetasenv,pbo,pty),metasenv
 in
 let goal_for_paramod =
  match LibraryObjects.eq_URI () with
  | Some uri -> 
      Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
  | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
 in
 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
 let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
 let proof''',goals =
  ProofEngineTypes.apply_tactic
    (EqualityTactics.rewrite_tac ~direction:`RightToLeft
      ~pattern:(ProofEngineTypes.conclusion_pattern None) 
        (Cic.Meta(newmeta,irl)))
   (proof'',goal)
 in
 let goal = match goals with [g] -> g | _ -> assert false in
 let subst, (proof'''', _), _ =
   PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) 
 in
 match 
   let (active, passive,bag), cache, maxmeta =
     init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
   in
     Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
       max_int max_int flags.timeout
 with
 | None, _,_,_ -> 
     raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
 | Some (_,proof''''',_), active,passive,_  ->
     subst,proof''''',
     ProofEngineHelpers.compare_metasenvs ~oldmetasenv
       ~newmetasenv:(let _,m,_,_ = proof''''' in m),  active, passive
;;

let rec count_prods context ty =
 match CicReduction.whd context ty with
    Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
  | _ -> 0

let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
 let module T = CicTypeChecker in
 let module R = CicReduction in
 let module C = Cic in
  let (_,metasenv,_,_) = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  let newmeta = CicMkImplicit.new_meta metasenv subst in
   let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
    match term with
       C.Var (uri,exp_named_subst) ->
        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
          exp_named_subst
        in
         exp_named_subst_diff,newmeta',newmetasenvfragment,
          C.Var (uri,exp_named_subst')
     | C.Const (uri,exp_named_subst) ->
        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
          exp_named_subst
        in
         exp_named_subst_diff,newmeta',newmetasenvfragment,
          C.Const (uri,exp_named_subst')
     | C.MutInd (uri,tyno,exp_named_subst) ->
        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
          exp_named_subst
        in
         exp_named_subst_diff,newmeta',newmetasenvfragment,
          C.MutInd (uri,tyno,exp_named_subst')
     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
          exp_named_subst
        in
         exp_named_subst_diff,newmeta',newmetasenvfragment,
          C.MutConstruct (uri,tyno,consno,exp_named_subst')
     | _ -> [],newmeta,[],term
   in
   let metasenv' = metasenv@newmetasenvfragment in
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
   in
   let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
   let goal_arity = count_prods context ty in
   let subst, proof, gl, active, passive =
    new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
     newmeta' metasenv' context term' ty termty goal_arity
   in
    subst, proof, gl, active, passive
;;

(****************** AUTO ********************)

let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
let ugraph = CicUniv.empty_ugraph;;
let typeof = CicTypeChecker.type_of_aux';;
let ppterm ctx t = 
  let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
  CicPp.pp t names
;;
let is_in_prop context subst metasenv ty =
  let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
;;

let assert_proof_is_valid proof metasenv context goalty =
  if debug then
    begin
      let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
      let b,_ = CicReduction.are_convertible context ty goalty u in
	if not b then
	  begin
	    let names = 
              List.map (function None -> None | Some (x,_) -> Some x) context 
	    in
	      prerr_endline ("PROOF:" ^ CicPp.pp proof names);
	      prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
	      prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
	      prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
	  end;
	assert b
    end
  else ()
;;

let assert_subst_are_disjoint subst subst' =
  if debug then
    assert(List.for_all
	     (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
	     subst)
  else ()
;;

let sort_new_elems = 
  List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) 
;;

let split_goals_in_prop metasenv subst gl =
  List.partition 
    (fun g ->
      let _,context,ty = CicUtil.lookup_meta g metasenv in
      try
        let sort,u = typeof ~subst metasenv context ty ugraph in
        let b,_ = 
	  CicReduction.are_convertible 
	    ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
	b
      with 
      | CicTypeChecker.AssertFailure s 
      | CicTypeChecker.TypeCheckerFailure s -> 
          debug_print 
	    (lazy (ppterm context (CicMetaSubst.apply_subst subst ty)));
          debug_print s;
          false)
    (* FIXME... they should type! *)
    gl
;;

let split_goals_with_metas metasenv subst gl =
  List.partition 
    (fun g ->
      let _,context,ty = CicUtil.lookup_meta g metasenv in
      let ty = CicMetaSubst.apply_subst subst ty in
      CicUtil.is_meta_closed ty)
    gl
;;

let order_new_goals metasenv subst open_goals ppterm =
  let prop,rest = split_goals_in_prop metasenv subst open_goals in
  let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
  let open_goals =
    (List.map (fun x -> x,P) (closed_prop @ open_prop)) 
    @ 
    (List.map (fun x -> x,T) rest)
  in
  let tys = 
    List.map 
      (fun (i,sort) -> 
        let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals 
  in
  debug_print (lazy ("   OPEN: "^
    String.concat "\n" 
      (List.map 
	 (function
	    | (i,t,P) -> string_of_int i   (* ":"^ppterm t^ "Prop" *)
	    | (i,t,T) -> string_of_int i ) (* ":"^ppterm t^ "Type")*)
	 tys)));
  open_goals
;;

let is_an_equational_goal = function
  | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
  | _ -> false
;;

let equational_case 
  tables maxm cache depth fake_proof goalno goalty subst context 
    flags
=
  let active,passive,bag = tables in
  let ppterm = ppterm context in
  let status = (fake_proof,goalno) in
    if flags.use_only_paramod then
      begin
	prerr_endline ("PARAMODULATION SU: " ^ 
			 string_of_int goalno ^ " " ^ ppterm goalty );
	let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in
	match
	  Saturation.given_clause bag maxm status active passive 
	    goal_steps saturation_steps timeout
	with 
	  | None, active, passive, maxmeta -> 
	      [], (active,passive,bag), cache, maxmeta, flags
	  | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
	      assert_subst_are_disjoint subst subst';
	      let subst = subst@subst' in
	      let open_goals = order_new_goals metasenv subst open_goals ppterm in
	      let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
		[metasenv,subst,open_goals], (active,passive,bag), 
	      cache, maxmeta, flags
      end
    else
      begin
	prerr_endline ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
	let res, maxmeta = Saturation.all_subsumed bag maxm status active passive in
        assert (maxmeta >= maxm);
	let res' =
	  List.map 
	    (fun subst',(_,metasenv,proof,_),open_goals ->
	       assert_subst_are_disjoint subst subst';
	       let subst = subst@subst' in
	       let open_goals = order_new_goals metasenv subst open_goals ppterm in
	       let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
		 metasenv,subst,open_goals)
	    res in
	  res', (active,passive,bag), cache, maxmeta, flags 
      end

(*
  let active,passive,bag,cache,maxmeta,flags,goal_steps,saturation_steps,timeout =
    given_clause_params 
      tables maxm auto cache subst flags context status in
  match
    Saturation.given_clause bag maxmeta status active passive 
      goal_steps saturation_steps timeout
  with 
  | None, active, passive, maxmeta -> 
      None, (active,passive,bag), cache, maxmeta, flags
  | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
      assert_subst_are_disjoint subst subst';
      let subst = subst@subst' in
      let open_goals = order_new_goals metasenv subst open_goals ppterm in
      let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
      Some [metasenv,subst,open_goals], (active,passive,bag), cache, maxmeta, flags
*)
;;

let try_candidate 
  goalty tables maxm subst fake_proof goalno depth context cand 
=
  let ppterm = ppterm context in
  try 
    let subst', ((_,metasenv,_,_), open_goals), maxmeta =
      PrimitiveTactics.apply_with_subst 
        ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) 
    in
    debug_print (lazy ("   OK: " ^ ppterm cand));
    let metasenv = CicRefine.pack_coercion_metasenv metasenv in
    assert_subst_are_disjoint subst subst';
    let subst = subst@subst' in
    let open_goals = order_new_goals metasenv subst open_goals ppterm in
    let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
    Some (metasenv,subst,open_goals), tables , maxmeta
  with 
    | ProofEngineTypes.Fail s -> 
    (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
    | CicUnification.Uncertain s ->  
    (*debug_print("   BECCATO: "^Lazy.force s);*)None,tables, maxm
;;

let applicative_case 
  tables maxm depth subst fake_proof goalno goalty metasenv context universe
  cache
= 
  let candidates = get_candidates universe cache goalty in
  let tables, elems, maxm = 
    List.fold_left 
      (fun (tables,elems,maxm) cand ->
        match 
          try_candidate goalty
            tables maxm subst fake_proof goalno depth context cand
        with
        | None, tables,maxm  -> tables,elems, maxm 
        | Some x, tables, maxm -> tables,x::elems, maxm)
      (tables,[],maxm) candidates
  in
  let elems = sort_new_elems elems in
  elems, tables, cache, maxm 
;;

(* Works if there is no dependency over proofs *)
let is_a_green_cut goalty =
  CicUtil.is_meta_closed goalty
;;

let prop = function (_,_,P) -> true | _ -> false;;
let calculate_timeout flags = 
    if flags.timeout = 0. then 
      (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
    else 
      flags 
;;
let is_equational_case goalty flags =
  let ensure_equational t = 
    if is_an_equational_goal t then true 
    else false
    (*
      let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
      raise (ProofEngineTypes.Fail (lazy msg))
    *)
  in
  (flags.use_paramod && is_an_equational_goal goalty) || 
  (flags.use_only_paramod && ensure_equational goalty)
;;
let cache_add_success sort cache k v =
  if sort = P then cache_add_success cache k v else cache_remove_underinspection
  cache k
;;

let rec auto_main tables maxm context flags elems universe cache =
  let flags = calculate_timeout flags in
  let ppterm = ppterm context in
  let irl = mk_irl context in
  let rec aux flags tables maxm cache = function (* elems in OR *)
    | [] -> Fail "no more steps can be done", tables, cache, maxm
         (*COMPLETE FAILURE*)
    | (metasenv,subst,[])::tl -> 
        Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
    | (metasenv,subst,goals)::tl when 
      List.length (List.filter prop goals) > flags.maxwidth -> 
        debug_print 
	  (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
        aux flags tables maxm cache tl (* FAILURE (width) *)
    | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> 
        if Unix.gettimeofday() > flags.timeout then 
          Fail "timeout",tables,cache,maxm 
        else
        try
          let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
          debug_print 
	    (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
          debug_print (lazy (AutoCache.cache_print context cache));
          if sort = T && tl <> [] then (* FIXME!!!! *)
            (debug_print 
	       (lazy (" FAILURE(not in prop)"));
            aux flags tables maxm cache tl (* FAILURE (not in prop) *))
          else
          match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
          | Fail s, tables, cache, maxm' -> 
              let maxm = maxm' in
              debug_print
                (lazy 
		   (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
              let cache = 
                if flags.dont_cache_failures then 
                  cache_remove_underinspection cache goalty
                else cache_add_failure cache goalty depth 
              in
              aux flags tables maxm cache tl
          | Success (metasenv,subst,others), tables, cache, maxm' ->
              let maxm = maxm' in
              (* others are alternatives in OR *)
              try
                let goal = Cic.Meta(goalno,irl) in
                let proof = CicMetaSubst.apply_subst subst goal in
                debug_print 
		  (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
                if is_a_green_cut goalty then
                  (assert_proof_is_valid proof metasenv context goalty;
                  let cache = cache_add_success sort cache goalty proof in
                  aux flags tables maxm cache ((metasenv,subst,gl)::tl))
                else
                  (let goalty = CicMetaSubst.apply_subst subst goalty in
                  assert_proof_is_valid proof metasenv context goalty;
                  let cache = 
                    if is_a_green_cut goalty then
                      cache_add_success sort cache goalty proof
                    else
                      cache
                  in
                  let others = 
                    List.map 
                      (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) 
                    others
                  in 
                  aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
              with CicUtil.Meta_not_found i when i = goalno ->
                assert false
        with CicUtil.Meta_not_found i when i = goalno -> 
          (* goalno was closed by sideeffect *)
          debug_print 
	    (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
          aux flags tables maxm cache ((metasenv,subst,gl)::tl)

  and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
    let goalty = CicMetaSubst.apply_subst subst goalty in
(*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
      (* FAILURE (euristic cut) *)
    match cache_examine cache goalty with
    | Failed_in d when d >= depth -> 
        Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
        tables,cache,maxm(*FAILURE(depth)*)
    | Succeded t -> 
        let entry = goalno, (cc, t,goalty) in
        assert_subst_are_disjoint subst [entry];
        let subst = entry :: subst in
        let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
        debug_print (lazy ("  CACHE HIT!"));
        Success (metasenv, subst, []), tables, cache, maxm
    | UnderInspection -> Fail "looping",tables,cache, maxm
    | Notfound 
    | Failed_in _ when depth > 0 -> (* we have more depth now *)
        let cache = cache_add_underinspection cache goalty depth in
        let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
        let elems, tables, cache, maxm, flags =
          if is_equational_case goalty flags then
            let elems,tables,cache,maxm1, flags =
              equational_case tables maxm cache
                depth fake_proof goalno goalty subst context flags in
	      let maxm = maxm1 in
	    let more_elems, tables, cache, maxm1 =
	      if flags.use_only_paramod then
		[],tables, cache, maxm
	      else
		applicative_case 
		  tables maxm depth subst fake_proof goalno 
		  goalty metasenv context universe cache in
	      let maxm = maxm1 in
	      elems@more_elems, tables, cache, maxm, flags            
          else
	    let elems, tables, cache, maxm =
            applicative_case tables maxm depth subst fake_proof goalno 
              goalty metasenv context universe cache in
	    elems, tables, cache, maxm, flags  
        in
        aux flags tables maxm cache elems
    | _ -> Fail "??",tables,cache,maxm 
  in
    aux flags tables maxm cache elems

and
  auto_all_solutions maxm tables universe cache context metasenv gl flags 
=
  let goals = order_new_goals metasenv [] gl CicPp.ppterm in
  let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
  let elems = [metasenv,[],goals] in
  let rec aux tables maxm solutions cache elems flags =
    match auto_main tables maxm context flags elems universe cache with
    | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
    | Success (metasenv,subst,others),tables,cache,maxm -> 
        if Unix.gettimeofday () > flags.timeout then
          ((subst,metasenv)::solutions), cache, maxm
        else
          aux tables maxm ((subst,metasenv)::solutions) cache others flags
  in
  let rc = aux tables maxm [] cache elems flags in
    match rc with
    | [],cache,maxm -> [],cache,maxm
    | solutions,cache,maxm -> 
        let solutions = 
          HExtlib.filter_map
            (fun (subst,newmetasenv) ->
              let opened = 
                ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
              in
              if opened = [] then Some subst else None)
            solutions
        in
         solutions,cache,maxm
;;

(* }}} ****************** AUTO ***************)

let auto_all tables universe cache context metasenv gl flags =
  let solutions, cache, _ = 
    auto_all_solutions 0 tables universe cache context metasenv gl flags
  in
  solutions, cache
;;

let auto flags metasenv tables universe cache context metasenv gl =
  let initial_time = Unix.gettimeofday() in
  let goals = order_new_goals metasenv [] gl CicPp.ppterm in
  let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
  let elems = [metasenv,[],goals] in
  match auto_main tables 0 context flags elems universe cache with
  | Success (metasenv,subst,_), tables,cache,_ -> 
      prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
      Some (subst,metasenv), cache
  | Fail s,tables,cache,maxm -> None,cache
;;

let bool params name default =
    try 
      let s = List.assoc name params in 
      if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
      else if s = "0" || s = "false" || s = "no" || s= "off" then false
      else 
        let msg = "Unrecognized value for parameter "^name^"\n" in
        let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
        raise (ProofEngineTypes.Fail (lazy msg))
    with Not_found -> default
;; 

let string params name default =
    try List.assoc name params with
    | Not_found -> default
;; 

let int params name default =
    try int_of_string (List.assoc name params) with
    | Not_found -> default
    | Failure _ -> 
        raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;  

let flags_of_params params ?(for_applyS=false) () =
 let int = int params in
 let bool = bool params in
 let close_more = bool "close_more" false in
 let use_paramod = bool "use_paramod" true in
 let use_only_paramod =
  if for_applyS then true else bool "paramodulation" false in
 let use_library = bool "library"  
   ((AutoTypes.default_flags()).AutoTypes.use_library) in
 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
 let timeout = int "timeout" 0 in
  { AutoTypes.maxdepth = 
      if use_only_paramod then 2 else depth;
    AutoTypes.maxwidth = width;
    AutoTypes.timeout = 
      if timeout = 0 then
       if for_applyS then Unix.gettimeofday () +. 30.0
       else
         infinity
      else
       Unix.gettimeofday() +. (float_of_int timeout);
    AutoTypes.use_library = use_library; 
    AutoTypes.use_paramod = use_paramod;
    AutoTypes.use_only_paramod = use_only_paramod;
    AutoTypes.close_more = close_more;
    AutoTypes.dont_cache_failures = false;
  }

let applyS_tac ~dbd ~term ~params ~universe =
 ProofEngineTypes.mk_tactic
  (fun status ->
    try 
      let _, proof, gl,_,_ =
       apply_smart ~dbd ~term ~subst:[] ~universe
        (flags_of_params params ~for_applyS:true ()) status
      in 
       proof, gl
    with 
    | CicUnification.UnificationFailure msg
    | CicTypeChecker.TypeCheckerFailure msg ->
        raise (ProofEngineTypes.Fail msg))

(* SUPERPOSITION *)

(* Syntax: 
 *   auto superposition target = NAME 
 *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
 *
 *  - if table is omitted no superposition will be performed
 *  - if demod_table is omitted no demodulation will be prformed
 *  - subterms_only is passed to Indexing.superposition_right
 *
 *  lists are coded using _ (example: H_H1_H2)
 *)

let eq_and_ty_of_goal = function
  | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
      uri,t
  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;

let rec find_in_ctx i name = function
  | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
  | Some (Cic.Name name', _)::tl when name = name' -> i
  | _::tl -> find_in_ctx (i+1) name tl
;;

let rec position_of i x = function
  | [] -> assert false
  | j::tl when j <> x -> position_of (i+1) x tl
  | _ -> i
;;


let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
  Saturation.reset_refs();
  let proof,goalno = status in 
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
  let eq_uri,tty = eq_and_ty_of_goal ty in
  let env = (metasenv, context, CicUniv.empty_ugraph) in
  let names = Utils.names_of_context context in
  let bag = Equality.mk_equality_bag () in
  let eq_index, equalities, maxm,cache  = 
    find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty 
  in
  let eq_what = 
    let what = find_in_ctx 1 target context in
    List.nth equalities (position_of 0 what eq_index)
  in
  let eq_other = 
    if table <> "" then
      let other = 
        let others = Str.split (Str.regexp "_") table in 
        List.map (fun other -> find_in_ctx 1 other context) others 
      in
      List.map 
        (fun other -> List.nth equalities (position_of 0 other eq_index)) 
        other 
    else
      []
  in
  let index = List.fold_left Indexing.index Indexing.empty eq_other in
  let maxm, eql = 
    if table = "" then maxm,[eq_what] else 
    Indexing.superposition_right bag
      ~subterms_only eq_uri maxm env index eq_what
  in
  prerr_endline ("Superposition right:");
  prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
  prerr_endline ("\n table: ");
  List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
  prerr_endline ("\n result: ");
  List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
  prerr_endline ("\n result (cut&paste): ");
  List.iter 
    (fun e -> 
      let t = Equality.term_of_equality eq_uri e in
      prerr_endline (CicPp.pp t names)) 
  eql;
  prerr_endline ("\n result proofs: ");
  List.iter (fun e -> 
    prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
    let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
    Subst.ppsubst s ^ "\n" ^ 
    CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
  if demod_table <> "" then
    begin
      let eql = 
        if eql = [] then [eq_what] else eql
      in
      let demod = 
        let demod = Str.split (Str.regexp "_") demod_table in 
        List.map (fun other -> find_in_ctx 1 other context) demod 
      in
      let eq_demod = 
        List.map 
          (fun demod -> List.nth equalities (position_of 0 demod eq_index)) 
          demod 
      in
      let table = List.fold_left Indexing.index Indexing.empty eq_demod in
      let maxm,eql = 
        List.fold_left 
          (fun (maxm,acc) e -> 
            let maxm,eq = 
              Indexing.demodulation_equality bag eq_uri maxm env table e
            in
            maxm,eq::acc) 
          (maxm,[]) eql
      in
      let eql = List.rev eql in
      prerr_endline ("\n result [demod]: ");
      List.iter 
        (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
      prerr_endline ("\n result [demod] (cut&paste): ");
      List.iter 
        (fun e -> 
          let t = Equality.term_of_equality eq_uri e in
          prerr_endline (CicPp.pp t names)) 
      eql;
    end;
  proof,[goalno]
;;

let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
  (* argument parsing *)
  let string = string params in
  let bool = bool params in
  (* hacks to debug paramod *)
  let superposition = bool "superposition" false in
  let target = string "target" "" in
  let table = string "table" "" in
  let subterms_only = bool "subterms_only" false in
  let demod_table = string "demod_table" "" in
  match superposition with
  | true -> 
      (* this is the ugly hack to debug paramod *)
      superposition_tac 
        ~target ~table ~subterms_only ~demod_table (proof,goal)
  | false -> 
      (* this is the real auto *)
      let _,metasenv,_,_ = proof in
      let _,context,_ = CicUtil.lookup_meta goal metasenv in
      let flags = flags_of_params params () in
      (* just for testing *)
      let use_library = flags.use_library in
      let tables,cache,newmeta =
	init_cache_and_tables dbd use_library flags.use_only_paramod 
	  universe (proof, goal) in
      let tables,cache,newmeta =
        if flags.close_more then
	  close_more 
	    tables newmeta context (proof, goal) auto_all_solutions universe cache 
	else tables,cache,newmeta in
      let initial_time = Unix.gettimeofday() in
      let (_,oldmetasenv,_,_) = proof in
      let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
      match auto_main tables newmeta context flags [elem] universe cache with
	| Success (metasenv,subst,_), tables,cache,_ -> 
	    prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
	    let proof,metasenv = 
            ProofEngineHelpers.subst_meta_and_metasenv_in_proof
              proof goal (CicMetaSubst.apply_subst subst) metasenv
            in
            let opened = 
              ProofEngineHelpers.compare_metasenvs ~oldmetasenv
		~newmetasenv:metasenv
            in
              proof,opened
	| Fail s,tables,cache,maxm -> 
	    raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
;;

let auto_tac ~dbd ~params ~universe = 
  ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;

let eq_of_goal = function
  | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
      uri
  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;

(* DEMODULATE *)
let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
  let initgoal = [], [], ty in
  let eq_uri = eq_of_goal ty in
  let (active,passive,bag), cache, maxm =
     init_cache_and_tables dbd true true Universe.empty (proof,goal) in
  let equalities = (Saturation.list_of_passive passive) in
  (* we demodulate using both actives passives *)
  let table = 
    List.fold_left 
      (fun tbl eq -> Indexing.index tbl eq) 
      (snd active) equalities
  in
  let changed,(newproof,newmetasenv, newty) = 
    Indexing.demodulation_goal bag
      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
  in
  if changed then
    begin
      let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
      let proofterm,_ = 
        Equality.build_goal_proof bag
          eq_uri newproof opengoal ty [] context metasenv
      in
        let extended_metasenv = (maxm,context,newty)::metasenv in
        let extended_status = 
          (curi,extended_metasenv,pbo,pty),goal in
        let (status,newgoals) = 
          ProofEngineTypes.apply_tactic 
            (PrimitiveTactics.apply_tac ~term:proofterm)
            extended_status in
        (status,maxm::newgoals)
    end
  else (* if newty = ty then *)
    raise (ProofEngineTypes.Fail (lazy "no progress"))
  (*else ProofEngineTypes.apply_tactic 
    (ReductionTactics.simpl_tac
      ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
;;

let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;