signature quantHeuristicsLibBase =
sig
  include Abbrev


(*some general conversions, that might be useful
  in other context as well *)
  val TOP_ONCE_REWRITE_CONV        : thm list -> conv;
  val NEG_NEG_INTRO_CONV           : conv;
  val NEG_NEG_ELIM_CONV            : conv;
  val NOT_FORALL_LIST_CONV         : conv;
  val NOT_EXISTS_LIST_CONV         : conv;
  val STRIP_NUM_QUANT_CONV         : int -> conv -> conv;
  val BOUNDED_NOT_EXISTS_LIST_CONV : int -> conv;
  val BOUNDED_REPEATC              : int -> conv -> conv;

  val EXISTS_NOT_LIST_CONV         : conv;
  val FORALL_NOT_LIST_CONV         : conv;
  val QUANT_SIMP_CONV              : conv;

  val NOT_OR_CONV                  : conv;
  val NOT_AND_CONV                 : conv;
  val AND_NOT_CONV                 : conv;
  val OR_NOT_CONV                  : conv;

  val VARIANT_TAC                  : term list -> tactic
  val VARIANT_CONV                 : term list -> conv


  datatype guess_type =
      gty_exists | gty_exists_gap | gty_exists_point
    | gty_forall | gty_forall_gap | gty_forall_point

  datatype guess =
       guess_general of term * term list
     | guess_term of guess_type * term * term list * term
     | guess_thm of guess_type * term * term list * thm

  val is_guess_general : guess -> bool
  val is_guess_thm     : guess_type -> guess -> bool
  val is_guess_term    : guess_type -> guess -> bool
  val is_guess         : guess_type -> guess -> bool
  val guess_has_thm    : guess -> bool
  val guess_has_no_free_vars     : guess -> bool
  val guess_has_thm_no_free_vars : guess -> bool

  val guess_type2string   : guess_type -> string
  val guess_type2term     : guess_type -> term
  val guess_term2type     : term -> guess_type
  val make_guess_thm_term : guess_type -> term -> term -> term -> term list -> term
  val guess_remove_thm    : term -> term -> guess -> guess
  val make_set_guess_thm  : guess -> (term -> thm) -> guess
  val mk_guess            : guess_type -> term -> term -> term -> term list -> guess
  val mk_guess_opt        : guess_type option -> term -> term -> term -> term list -> guess

  val make_guess___dummy  : guess_type -> term -> term -> term -> term list -> guess
  val make_guess___assume : guess_type -> term -> term -> term -> term list -> guess
  val make_guess___simple : guess_type -> term -> term -> term -> term list -> guess

  val make_set_guess_thm___dummy  : guess -> guess
  val make_set_guess_thm___simple : guess -> guess
  val make_set_guess_thm___assume : guess -> guess

  val guess_extract       : guess -> term * term list
  val guess_extract_thm   : guess -> guess_type * term * term list * thm * bool
  val guess2term          : guess -> term option
  val guess2thm           : guess -> bool * thm
  val guess2thm_opt       : guess -> thm option
  val guess_extract_type  : guess -> guess_type option


  val guess_thm_to_guess  : bool -> (term * term list) option -> thm -> guess
  val dest_guess_tm       : term -> guess_type * term * term * term
  val is_guess_tm         : term -> bool

  val guess_to_string : bool -> guess -> string


  (*guesses are organised in collections. They are used to
    store the different types of guesses separately. Moreover,
    rewrite theorems, that might come in handy, are there as well.*)
  type guess_collection =
   {rewrites     : thm list,
    general      : guess list,
    exists_point : guess list,
    forall_point : guess list,
    forall       : guess list,
    exists       : guess list,
    forall_gap   : guess list,
    exists_gap   : guess list}

  val guess_collection_guess_type : guess_type -> guess_collection -> guess list

  val empty_guess_collection    : guess_collection;
  val is_empty_guess_collection : guess_collection -> bool;
  val guess_collection_append   : guess_collection -> guess_collection -> guess_collection;
  val guess_collection_flatten  : guess_collection option list -> guess_collection;
  val guess_list2collection     : thm list * guess list -> guess_collection;
  val guess_collection2list     : guess_collection -> thm list * guess list;
  val guess_collection___get_exists_weaken     : guess_collection -> guess list;
  val guess_collection___get_forall_weaken : guess_collection -> guess list;



  val guess_weaken       : guess -> guess
  val check_guess        : term -> term -> guess -> bool
  val correct_guess      : term -> term -> guess -> guess option
  val correct_guess_list : term -> term -> guess list -> guess list;
  val correct_guess_collection :
     term -> term -> guess_collection -> guess_collection


  type inference_collection =
     {exists_point : thm list,
      forall_point : thm list,
      exists       : thm list,
      forall       : thm list,
      exists_gap   : thm list,
      forall_gap   : thm list};

  val GUESS_THM_list2collection : thm list -> inference_collection;


  exception QUANT_INSTANTIATE_HEURISTIC___no_guess_exp;

(*Basic types*)
  type quant_heuristic_base = term -> term -> guess_collection;
  type quant_heuristic      = quant_heuristic_base -> quant_heuristic_base;
  type quant_heuristic_cache;

  val mk_quant_heuristic_cache : unit -> quant_heuristic_cache;


(* Quantifier Heuristics Parameters are the main way to configure the behaviour. They
   are a record of theorems, conversion and full heuristics used during proof search. *)

  type quant_param;

(* constructing quantifier heuristics parameters*)

  val distinct_qp      : thm list -> quant_param
  val cases_qp         : thm list -> quant_param
  val rewrite_qp       : thm list -> quant_param
  val inst_filter_qp   : (term -> term -> term -> term list -> bool) list -> quant_param
  val instantiation_qp : thm list -> quant_param
  val imp_qp           : thm list -> quant_param
  val fixed_context_qp : thm list -> quant_param
  val inference_qp     : thm list -> quant_param
  val convs_qp         : conv list -> quant_param
  val filter_qp        : (term -> term -> bool) list -> quant_param
  val top_heuristics_qp: quant_heuristic list -> quant_param
  val context_heuristics_qp : (thm list -> quant_heuristic) list -> quant_param
  val context_top_heuristics_qp : (thm list -> quant_heuristic) list -> quant_param
  val heuristics_qp    : quant_heuristic list -> quant_param
  val oracle_qp        : (term -> term -> (term * term list) option) -> quant_param (* creates heuristic that produces oracle guesses *)
  val context_oracle_qp: (thm list -> term -> term -> (term * term list) option) -> quant_param (* creates heuristic that produces oracle guesses *)
  val final_rewrite_qp : thm list -> quant_param

  (* a stateful version and combining several*)
  val clear_stateful_qp : unit -> unit
  val stateful_qp___add_combine_arguments :
     quant_param list -> unit;

  val empty_qp           : quant_param;
  val basic_qp           : quant_param; (* the basic things that should always be turned on *)
  val direct_context_qp  : quant_param; (* use the context, but don't recurse *)
  val context_qp         : quant_param; (* use the context *)
  val stateful_qp        : unit -> quant_param;
  val pure_stateful_qp   : unit -> quant_param;
  val TypeBase_qp        : quant_param;
  val get_qp___for_types : hol_type list -> quant_param

  val combine_qp :
     quant_param -> quant_param ->
     quant_param;

  val combine_qps :
     quant_param list -> quant_param;


  val COMBINE_HEURISTIC_FUNS : (unit -> guess_collection) list -> guess_collection;

(*Heuristics that might be useful to write own ones*)
  val QUANT_INSTANTIATE_HEURISTIC___CONV                : conv -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct   : thm list -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases  : thm -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___one_case            : thm -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___cases               : thm -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION : bool -> thm list -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN   : thm list -> quant_heuristic;
  val QUANT_INSTANTIATE_HEURISTIC___QUANT               : bool -> quant_heuristic;

  val QUANT_INSTANTIATE_HEURISTIC___max_rec_depth : int ref

  (*use this to create sys for debugging own heuristics*)
  val qp_to_heuristic : quant_param -> quant_heuristic_cache ref option -> thm list -> term -> term -> guess_collection
  val debug_sys : term -> term -> guess_collection

 (*The most important functions *)
  val EXTENSIBLE_QUANT_INSTANTIATE_CONV : quant_heuristic_cache ref option ->
      bool -> bool -> bool -> thm list -> quant_param -> quant_param list -> conv;
  val QUANT_INSTANTIATE_TAC             : quant_param list -> tactic;
  val ASM_QUANT_INSTANTIATE_TAC         : quant_param list -> tactic;
  val QUANT_INSTANTIATE_CONV            : quant_param list -> conv;
  val FAST_QUANT_INSTANTIATE_CONV       : quant_param list -> conv;
  val FAST_QUANT_INSTANTIATE_TAC        : quant_param list -> tactic;
  val FAST_ASM_QUANT_INSTANTIATE_TAC    : quant_param list -> tactic;
  val EXPAND_QUANT_INSTANTIATE_CONV     : quant_param list -> conv;
  val FAST_EXPAND_QUANT_INSTANTIATE_CONV: quant_param list -> conv;

  val NORE_QUANT_INSTANTIATE_CONV        : quant_param list -> conv;
  val NORE_EXPAND_QUANT_INSTANTIATE_CONV : quant_param list -> conv;


  val EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV :
      quant_heuristic_cache ref option -> bool -> bool -> quant_param -> quant_param list -> ConseqConv.directed_conseq_conv;
  val EXTENSIBLE_QUANT_INSTANTIATE_STEP_CONSEQ_CONV :
      quant_heuristic_cache ref option -> bool -> quant_param -> quant_param list -> ConseqConv.directed_conseq_conv;
  val QUANT_INSTANTIATE_CONSEQ_CONV :
      quant_param list -> ConseqConv.directed_conseq_conv;
  val QUANT_INSTANTIATE_CONSEQ_TAC : quant_param list -> tactic;
  val NORE_QUANT_INSTANTIATE_CONSEQ_CONV :
      quant_param list -> ConseqConv.directed_conseq_conv;
  val FAST_QUANT_INSTANTIATE_CONSEQ_CONV :
      quant_param list -> ConseqConv.directed_conseq_conv;


  val INST_QUANT_CONV : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list
   -> conv;
  val QUANT_TAC  : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list
   -> tactic;

(* Predefined filters to use with filter_qp *)
val subterm_filter       : term list -> term -> term -> bool
val subterm_match_filter : term list -> term -> term -> bool
val type_filter          : hol_type list -> term -> term -> bool
val type_match_filter    : hol_type list -> term -> term -> bool
val neg_filter           : (term -> term -> bool) -> term -> term -> bool

(*combination with simplifier*)
  val QUANT_INST_ss        : quant_param list -> simpLib.ssfrag;
  val EXPAND_QUANT_INST_ss : quant_param list -> simpLib.ssfrag;
  val FAST_QUANT_INST_ss   : quant_param list -> simpLib.ssfrag;

(* Traces *)
(* "QUANT_INST_DEBUG" can be used to get debug information on
   how guesses are obtained

   "QUANT_INST___print_term_length" used for printing debug concisely


   "QUANT_INST___REC_DEPTH" can set the maximal recursion depth, default is 250.
   If the search is aborted, because the depth is not big enough, a warning
   is printed. Decrease for speed and increase if the warning appears and you want to search deeper.
*)



end