1signature quantHeuristicsLibBase =
2sig
3  include Abbrev
4
5
6(*some general conversions, that might be useful
7  in other context as well *)
8  val TOP_ONCE_REWRITE_CONV        : thm list -> conv;
9  val NEG_NEG_INTRO_CONV           : conv;
10  val NEG_NEG_ELIM_CONV            : conv;
11  val NOT_FORALL_LIST_CONV         : conv;
12  val NOT_EXISTS_LIST_CONV         : conv;
13  val STRIP_NUM_QUANT_CONV         : int -> conv -> conv;
14  val BOUNDED_NOT_EXISTS_LIST_CONV : int -> conv;
15  val BOUNDED_REPEATC              : int -> conv -> conv;
16
17  val EXISTS_NOT_LIST_CONV         : conv;
18  val FORALL_NOT_LIST_CONV         : conv;
19  val QUANT_SIMP_CONV              : conv;
20
21  val NOT_OR_CONV                  : conv;
22  val NOT_AND_CONV                 : conv;
23  val AND_NOT_CONV                 : conv;
24  val OR_NOT_CONV                  : conv;
25
26  val VARIANT_TAC                  : term list -> tactic
27  val VARIANT_CONV                 : term list -> conv
28
29
30  datatype guess_type =
31      gty_exists | gty_exists_gap | gty_exists_point
32    | gty_forall | gty_forall_gap | gty_forall_point
33
34  datatype guess =
35       guess_general of term * term list
36     | guess_term of guess_type * term * term list * term
37     | guess_thm of guess_type * term * term list * thm
38
39  val is_guess_general : guess -> bool
40  val is_guess_thm     : guess_type -> guess -> bool
41  val is_guess_term    : guess_type -> guess -> bool
42  val is_guess         : guess_type -> guess -> bool
43  val guess_has_thm    : guess -> bool
44  val guess_has_no_free_vars     : guess -> bool
45  val guess_has_thm_no_free_vars : guess -> bool
46
47  val guess_type2string   : guess_type -> string
48  val guess_type2term     : guess_type -> term
49  val guess_term2type     : term -> guess_type
50  val make_guess_thm_term : guess_type -> term -> term -> term -> term list -> term
51  val guess_remove_thm    : term -> term -> guess -> guess
52  val make_set_guess_thm  : guess -> (term -> thm) -> guess
53  val mk_guess            : guess_type -> term -> term -> term -> term list -> guess
54  val mk_guess_opt        : guess_type option -> term -> term -> term -> term list -> guess
55
56  val make_guess___dummy  : guess_type -> term -> term -> term -> term list -> guess
57  val make_guess___assume : guess_type -> term -> term -> term -> term list -> guess
58  val make_guess___simple : guess_type -> term -> term -> term -> term list -> guess
59
60  val make_set_guess_thm___dummy  : guess -> guess
61  val make_set_guess_thm___simple : guess -> guess
62  val make_set_guess_thm___assume : guess -> guess
63
64  val guess_extract       : guess -> term * term list
65  val guess_extract_thm   : guess -> guess_type * term * term list * thm * bool
66  val guess2term          : guess -> term option
67  val guess2thm           : guess -> bool * thm
68  val guess2thm_opt       : guess -> thm option
69  val guess_extract_type  : guess -> guess_type option
70
71
72  val guess_thm_to_guess  : bool -> (term * term list) option -> thm -> guess
73  val dest_guess_tm       : term -> guess_type * term * term * term
74  val is_guess_tm         : term -> bool
75
76  val guess_to_string : bool -> guess -> string
77
78
79  (*guesses are organised in collections. They are used to
80    store the different types of guesses separately. Moreover,
81    rewrite theorems, that might come in handy, are there as well.*)
82  type guess_collection =
83   {rewrites     : thm list,
84    general      : guess list,
85    exists_point : guess list,
86    forall_point : guess list,
87    forall       : guess list,
88    exists       : guess list,
89    forall_gap   : guess list,
90    exists_gap   : guess list}
91
92  val guess_collection_guess_type : guess_type -> guess_collection -> guess list
93
94  val empty_guess_collection    : guess_collection;
95  val is_empty_guess_collection : guess_collection -> bool;
96  val guess_collection_append   : guess_collection -> guess_collection -> guess_collection;
97  val guess_collection_flatten  : guess_collection option list -> guess_collection;
98  val guess_list2collection     : thm list * guess list -> guess_collection;
99  val guess_collection2list     : guess_collection -> thm list * guess list;
100  val guess_collection___get_exists_weaken     : guess_collection -> guess list;
101  val guess_collection___get_forall_weaken : guess_collection -> guess list;
102
103
104
105  val guess_weaken       : guess -> guess
106  val check_guess        : term -> term -> guess -> bool
107  val correct_guess      : term -> term -> guess -> guess option
108  val correct_guess_list : term -> term -> guess list -> guess list;
109  val correct_guess_collection :
110     term -> term -> guess_collection -> guess_collection
111
112
113  type inference_collection =
114     {exists_point : thm list,
115      forall_point : thm list,
116      exists       : thm list,
117      forall       : thm list,
118      exists_gap   : thm list,
119      forall_gap   : thm list};
120
121  val GUESS_THM_list2collection : thm list -> inference_collection;
122
123
124  exception QUANT_INSTANTIATE_HEURISTIC___no_guess_exp;
125
126(*Basic types*)
127  type quant_heuristic_base = term -> term -> guess_collection;
128  type quant_heuristic      = quant_heuristic_base -> quant_heuristic_base;
129  type quant_heuristic_cache;
130
131  val mk_quant_heuristic_cache : unit -> quant_heuristic_cache;
132
133
134(* Quantifier Heuristics Parameters are the main way to configure the behaviour. They
135   are a record of theorems, conversion and full heuristics used during proof search. *)
136
137  type quant_param;
138
139(* constructing quantifier heuristics parameters*)
140
141  val distinct_qp      : thm list -> quant_param
142  val cases_qp         : thm list -> quant_param
143  val rewrite_qp       : thm list -> quant_param
144  val inst_filter_qp   : (term -> term -> term -> term list -> bool) list -> quant_param
145  val instantiation_qp : thm list -> quant_param
146  val imp_qp           : thm list -> quant_param
147  val fixed_context_qp : thm list -> quant_param
148  val inference_qp     : thm list -> quant_param
149  val convs_qp         : conv list -> quant_param
150  val filter_qp        : (term -> term -> bool) list -> quant_param
151  val top_heuristics_qp: quant_heuristic list -> quant_param
152  val context_heuristics_qp : (thm list -> quant_heuristic) list -> quant_param
153  val context_top_heuristics_qp : (thm list -> quant_heuristic) list -> quant_param
154  val heuristics_qp    : quant_heuristic list -> quant_param
155  val oracle_qp        : (term -> term -> (term * term list) option) -> quant_param (* creates heuristic that produces oracle guesses *)
156  val context_oracle_qp: (thm list -> term -> term -> (term * term list) option) -> quant_param (* creates heuristic that produces oracle guesses *)
157  val final_rewrite_qp : thm list -> quant_param
158
159  (* a stateful version and combining several*)
160  val clear_stateful_qp : unit -> unit
161  val stateful_qp___add_combine_arguments :
162     quant_param list -> unit;
163
164  val empty_qp           : quant_param;
165  val basic_qp           : quant_param; (* the basic things that should always be turned on *)
166  val direct_context_qp  : quant_param; (* use the context, but don't recurse *)
167  val context_qp         : quant_param; (* use the context *)
168  val stateful_qp        : unit -> quant_param;
169  val pure_stateful_qp   : unit -> quant_param;
170  val TypeBase_qp        : quant_param;
171  val get_qp___for_types : hol_type list -> quant_param
172
173  val combine_qp :
174     quant_param -> quant_param ->
175     quant_param;
176
177  val combine_qps :
178     quant_param list -> quant_param;
179
180
181  val COMBINE_HEURISTIC_FUNS : (unit -> guess_collection) list -> guess_collection;
182
183(*Heuristics that might be useful to write own ones*)
184  val QUANT_INSTANTIATE_HEURISTIC___CONV                : conv -> quant_heuristic;
185  val QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct   : thm list -> quant_heuristic;
186  val QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases  : thm -> quant_heuristic;
187  val QUANT_INSTANTIATE_HEURISTIC___one_case            : thm -> quant_heuristic;
188  val QUANT_INSTANTIATE_HEURISTIC___cases               : thm -> quant_heuristic;
189  val QUANT_INSTANTIATE_HEURISTIC___GIVEN_INSTANTIATION : bool -> thm list -> quant_heuristic;
190  val QUANT_INSTANTIATE_HEURISTIC___STRENGTHEN_WEAKEN   : thm list -> quant_heuristic;
191  val QUANT_INSTANTIATE_HEURISTIC___QUANT               : bool -> quant_heuristic;
192
193  val QUANT_INSTANTIATE_HEURISTIC___max_rec_depth : int ref
194
195  (*use this to create sys for debugging own heuristics*)
196  val qp_to_heuristic : quant_param -> quant_heuristic_cache ref option -> thm list -> term -> term -> guess_collection
197  val debug_sys : term -> term -> guess_collection
198
199 (*The most important functions *)
200  val EXTENSIBLE_QUANT_INSTANTIATE_CONV : quant_heuristic_cache ref option ->
201      bool -> bool -> bool -> thm list -> quant_param -> quant_param list -> conv;
202  val QUANT_INSTANTIATE_TAC             : quant_param list -> tactic;
203  val ASM_QUANT_INSTANTIATE_TAC         : quant_param list -> tactic;
204  val QUANT_INSTANTIATE_CONV            : quant_param list -> conv;
205  val FAST_QUANT_INSTANTIATE_CONV       : quant_param list -> conv;
206  val FAST_QUANT_INSTANTIATE_TAC        : quant_param list -> tactic;
207  val FAST_ASM_QUANT_INSTANTIATE_TAC    : quant_param list -> tactic;
208  val EXPAND_QUANT_INSTANTIATE_CONV     : quant_param list -> conv;
209  val FAST_EXPAND_QUANT_INSTANTIATE_CONV: quant_param list -> conv;
210
211  val NORE_QUANT_INSTANTIATE_CONV        : quant_param list -> conv;
212  val NORE_EXPAND_QUANT_INSTANTIATE_CONV : quant_param list -> conv;
213
214
215  val EXTENSIBLE_QUANT_INSTANTIATE_CONSEQ_CONV :
216      quant_heuristic_cache ref option -> bool -> bool -> quant_param -> quant_param list -> ConseqConv.directed_conseq_conv;
217  val EXTENSIBLE_QUANT_INSTANTIATE_STEP_CONSEQ_CONV :
218      quant_heuristic_cache ref option -> bool -> quant_param -> quant_param list -> ConseqConv.directed_conseq_conv;
219  val QUANT_INSTANTIATE_CONSEQ_CONV :
220      quant_param list -> ConseqConv.directed_conseq_conv;
221  val QUANT_INSTANTIATE_CONSEQ_TAC : quant_param list -> tactic;
222  val NORE_QUANT_INSTANTIATE_CONSEQ_CONV :
223      quant_param list -> ConseqConv.directed_conseq_conv;
224  val FAST_QUANT_INSTANTIATE_CONSEQ_CONV :
225      quant_param list -> ConseqConv.directed_conseq_conv;
226
227
228  val INST_QUANT_CONV : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list
229   -> conv;
230  val QUANT_TAC  : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list
231   -> tactic;
232
233(* Predefined filters to use with filter_qp *)
234val subterm_filter       : term list -> term -> term -> bool
235val subterm_match_filter : term list -> term -> term -> bool
236val type_filter          : hol_type list -> term -> term -> bool
237val type_match_filter    : hol_type list -> term -> term -> bool
238val neg_filter           : (term -> term -> bool) -> term -> term -> bool
239
240(*combination with simplifier*)
241  val QUANT_INST_ss        : quant_param list -> simpLib.ssfrag;
242  val EXPAND_QUANT_INST_ss : quant_param list -> simpLib.ssfrag;
243  val FAST_QUANT_INST_ss   : quant_param list -> simpLib.ssfrag;
244
245(* Traces *)
246(* "QUANT_INST_DEBUG" can be used to get debug information on
247   how guesses are obtained
248
249   "QUANT_INST___print_term_length" used for printing debug concisely
250
251
252   "QUANT_INST___REC_DEPTH" can set the maximal recursion depth, default is 250.
253   If the search is aborted, because the depth is not big enough, a warning
254   is printed. Decrease for speed and increase if the warning appears and you want to search deeper.
255*)
256
257
258
259end
260