(* 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_print s = () (*prerr_endline s;;*)

(* {{{ *********** local given_clause wrapper ***********)

let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
  let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
    match tables with
    | None -> 
        (* first time, do a huge saturation *)
        let bag, equalities, cache, maxmeta = 
          Saturation.find_equalities dbd status smart_flag auto cache
        in
        let passive = Saturation.make_passive equalities in
        let active = Saturation.make_active [] in
        let goal_steps, saturation_steps, timeout =
          if flags.use_only_paramod then max_int,max_int,flags.timeout
          else 82, 82, infinity
        in
        let maxm = max maxm maxmeta in
        active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
    | Some (active,passive,bag,oldcache) -> 
        (* saturate a bit more if cache cahnged *)
        let bag, equalities, cache, maxm = 
          if cache_size oldcache <> cache_size cache then 
            Saturation.close_more
              bag active maxm status smart_flag auto cache
          else
            bag, [], cache, maxm
        in
        let minsteps = List.length equalities in
        let passive = Saturation.add_to_passive equalities passive in
        let goal_steps, saturation_steps, timeout =
          if flags.use_only_paramod then max_int,max_int,flags.timeout
          else max 50 minsteps, minsteps, infinity
        in
        active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
  in
  let res,actives,passives,maxmeta = 
    Saturation.given_clause bag maxmeta status active passive 
      goal_steps saturation_steps timeout
  in
  res,actives,passives,bag,cache,maxmeta
;;

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

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

let new_metasenv_and_unify_and_t 
 dbd flags 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 cache = cache_empty in
   given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) 
 with
 | None, active, passive, bag,_,_ -> 
     raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
 | Some (_,proof''''',_), active, passive,bag,_,_  ->
     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 ?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 proof goal ?tables
     newmeta' metasenv' context term' ty termty goal_arity
   in
    subst, proof, gl, active, passive
;;

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

(* {{{ ***************** 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 (Cic.Sort Cic.Prop) sort u)
;;
let assert_proof_is_valid proof metasenv context goalty =
  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 ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
    end;
  assert b
;;
let assert_subst_are_disjoint subst subst' =
  assert(List.for_all
    (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
    subst)
;;
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
        fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
      with 
      | CicTypeChecker.AssertFailure s 
      | CicTypeChecker.TypeCheckerFailure s -> 
          debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
          debug_print (Lazy.force 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,_) -> 
        let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals 
  in
  debug_print ("   OPEN: "^
    String.concat " " 
      (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) 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 
  dbd tables maxm auto cache depth fake_proof goalno goalty subst context 
    flags
=
  let ppterm = ppterm context in
  prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
(*
  prerr_endline "<CACHE>";
  prerr_endline (cache_print context cache);
  prerr_endline "</CACHE>";
*)
  match 
    given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno) 
  with
  | None, active,passive, bag, cache, maxmeta -> 
      let tables = Some (active,passive,bag,cache) in
      None, tables, cache, maxmeta
  | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
      let tables = Some (active,passive,bag,cache) 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, cache, maxmeta
;;

let try_candidate 
  goalty dbd 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 ("   OK: " ^ ppterm cand);
    assert (maxmeta >= maxm);
    (*FIXME:sicuro che posso @?*)
    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
;;

let applicative_case 
  dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
= 
  let candidates = get_candidates cache goalty in
  let tables, elems, maxm = 
    List.fold_left 
      (fun (tables,elems,maxm) cand ->
        match 
          try_candidate goalty
            dbd 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 dbd tables maxm context flags elems cache =
  let callback_for_paramod maxm flags proof commonctx cache l = 
    let flags = {flags with use_paramod = false;dont_cache_failures=true} in
    let _,metasenv,_,_ = proof in
    let oldmetasenv = metasenv in
    match
      auto_all_solutions
        dbd tables maxm cache commonctx metasenv l flags
    with
    | [],cache,maxm -> [],cache,maxm
    | solutions,cache,maxm -> 
        let solutions = 
          HExtlib.filter_map
            (fun (subst,newmetasenv) ->
              let opened = 
                ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
              in
              if opened = [] then Some subst else None)
            solutions
        in
         solutions,cache,maxm
  in
  let flags = calculate_timeout flags in
  let ppterm = ppterm context in
  let irl = mk_irl context in
  let rec aux 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 (" FAILURE(width): " ^ string_of_int (List.length goals));
        aux 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 ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
          if sort = T && tl <> [] then (* FIXME!!!! *)
            (debug_print (" FAILURE(not in prop)");
            aux tables maxm cache tl (* FAILURE (not in prop) *))
          else
          match aux_single tables maxm cache metasenv subst elem goalty cc with
          | Fail s, tables, cache, maxm' -> 
              assert(maxm' >= maxm);let maxm = maxm' in
              debug_print
                (" 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 tables maxm cache tl
          | Success (metasenv,subst,others), tables, cache, maxm' ->
              assert(maxm' >= 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 ("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 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 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 ("Goal "^string_of_int goalno^" closed by sideeffect");
          aux tables maxm cache ((metasenv,subst,gl)::tl)
  and aux_single tables maxm 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 -> 
        assert(List.for_all (fun (i,_) -> i <> goalno) subst);
        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 ("  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 =
          if is_equational_case goalty flags then
            match 
              equational_case dbd tables maxm
                (Some callback_for_paramod) cache
                depth fake_proof goalno goalty subst context flags 
            with
            | Some elems, tables, cache, maxm -> 
                elems, tables, cache, maxm 
            | None, tables,cache,maxm -> 
                applicative_case dbd tables maxm depth subst fake_proof goalno 
                  goalty metasenv context cache
          else
            applicative_case dbd tables maxm depth subst fake_proof goalno 
              goalty metasenv context cache
        in
        aux tables maxm cache elems
    | _ -> Fail "??",tables,cache,maxm 
  in
    aux tables maxm cache elems

and
  auto_all_solutions dbd tables maxm 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 dbd tables maxm context flags elems 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
  prerr_endline "fine auto all solutions";
  rc
;;

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

let auto_all_solutions dbd cache context metasenv gl flags =
  let solutions, cache, _ = 
    auto_all_solutions dbd None 0 cache context metasenv gl flags
  in
  solutions, cache
;;

let auto dbd cache context metasenv gl flags =
  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 dbd None 0 context flags elems 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 use_paramod = bool "use_paramod" true in
 let use_only_paramod =
  if for_applyS then true else bool "paramodulation" false 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
        0.0
      else
       Unix.gettimeofday() +. (float_of_int timeout); 
    AutoTypes.use_paramod = use_paramod;
    AutoTypes.use_only_paramod = use_only_paramod;
    AutoTypes.dont_cache_failures = false
  }

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

let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
  (* argument parsing *)
  let string = string params in
  let bool = bool params in
  let use_only_paramod = bool "paramodulation" false 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 *)
      Saturation.superposition_tac 
        ~target ~table ~subterms_only ~demod_table (proof,goal)
  | false -> 
      (* this is the real auto *)
      let _, metasenv, _, _ = proof in
      let _, context, goalty = CicUtil.lookup_meta goal metasenv in
      let cache = 
        let cache = 
          AutoCache.cache_add_context context metasenv AutoCache.cache_empty 
        in
        if use_only_paramod then (* only paramod *)
          cache
        else
          AutoCache.cache_add_library dbd proof [goal] cache
      in 
      let oldmetasenv = metasenv in
      let flags = flags_of_params params () in
      match auto dbd cache context metasenv [goal] flags with
      | None,cache -> 
          raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
      | Some (subst,metasenv),cache -> 
          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
;;

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