1signature holfootLib =
2sig
3  include Abbrev
4
5   structure holfoot_param : sig
6    include Abbrev;
7
8    val combinator_thmL              : thm list
9    val predicate_ssfrag             : int -> simpLib.ssfrag
10    val final_decision_procedure     : thm list -> term -> thm;
11    val combinator_terms             : term * term * term;
12    val resource_proccall_free_thmL  : thm list
13    val inital_prop_rewrite_thmL     : thm list
14    val abstrL                       : separationLogicLib.asl_program_abstraction list
15    val comments_step_convL          : (conv->conv) list
16    val quantifier_heuristicsL       : quantHeuristicsLib.quant_param list
17    val var_res_prop_implies___GENERATE :
18       (term list -> int -> (bool * simpLib.ssfrag) -> thm list -> term * term * term * term -> thm list) list
19
20    val hoare_triple_case_splitL     : (term -> term) list
21    val frame_split_case_splitL      : (term -> term) list
22
23    structure var_res_base : sig
24       include Abbrev;
25
26       val var_res_prove              : Abbrev.term -> Abbrev.thm
27       val var_res_prove___no_expn    : Abbrev.term -> Abbrev.thm
28       val var_res_assumptions_prove  : Abbrev.thm -> Abbrev.thm
29       val var_res_precondition_prove : Abbrev.thm -> Abbrev.thm
30       val var_res_precondition_assumption_prove :
31                                        Abbrev.term option -> Abbrev.thm -> Abbrev.thm
32       val raise_var_res_prove_expn   : exn -> 'a
33
34       val COND_REWR_CONV             : Abbrev.thm -> Abbrev.conv
35       val COND_REWRITE_CONV          : bool -> Abbrev.thm list -> Abbrev.conv
36       val GUARDED_COND_REWRITE_CONV  : bool -> (Abbrev.term -> bool) -> Abbrev.thm list -> Abbrev.conv
37
38       val VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV : conv -> conv
39       val VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV : conv -> conv
40       val VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV : (term -> bool) -> conv
41
42       val var_res_prop___VAR_EQ_PROPAGATE : conv
43       val VAR_RES_COND_INFERENCE___CONST_INTRO___CONV : term -> string option -> term -> (bool * term * thm)
44       val VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm
45       val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_INTRO___CONV : term -> string option -> term -> thm
46       val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm
47
48       val var_res_prop_equal_unequal___NORMALISE_CONV : conv
49       val VAR_RES_PROP_REWRITE_CONV : (bool * simpLib.ssfrag) -> thm list -> term -> thm
50       val get_const_name_for_exp    : string -> term -> string
51
52       val VAR_RES_COND_HOARE_TRIPLE___RESORT_PRECOND_CONV : int list -> conv
53       val var_res_prop___COND_RESORT_CONV : int list -> conv
54
55       val cond_rewrite___varlist_update : thm list -> conv
56       val GENERATE___var_res_exp_varlist_update___REWRITES : term -> term -> term -> (term * thm list)
57       val var_res_prop___var_res_prop_varlist_update___EVAL : term -> conv;
58       val VAR_RES_COND_INFERENCE___PRECOND_var_res_prop_varlist_update___EVAL : term -> conv
59
60       val BAG_NORMALISE_CONV : conv;
61       val VAR_RES_FRAME_SPLIT___imp_CONV               : conv -> conv
62       val VAR_RES_FRAME_SPLIT___split_CONV             : conv -> conv
63       val VAR_RES_FRAME_SPLIT___context_CONV           : conv -> conv
64       val VAR_RES_FRAME_SPLIT___context_split_imp_CONV : conv -> conv
65       val VAR_RES_FRAME_SPLIT___PROP_CONV              : conv -> conv
66
67       type var_res_inference_param =
68         {fast           : bool,
69          do_prop_simps  : bool,
70          prop_simp_ss   : simpLib.ssfrag,
71          expands_level  : int};
72
73       type var_res_inference = var_res_inference_param -> thm list -> ConseqConv.directed_conseq_conv
74
75       val no_context_conseq_conv                    : ConseqConv.directed_conseq_conv -> var_res_inference;
76       val no_context_strengthen_conseq_conv         : conv -> var_res_inference;
77       val context_strengthen_conseq_conv            : (thm list -> conv) -> var_res_inference;
78       val simpset_strengthen_conseq_conv            : ((bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference;
79       val simpset_no_context_strengthen_conseq_conv : ((bool * simpLib.ssfrag) -> conv) -> var_res_inference;
80       val expands_strengthen_conseq_conv            : (int -> (bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference;
81    end
82
83    val INFERENCES_LIST___simulate_command          : (string * var_res_base.var_res_inference) list
84    val INFERENCES_LIST___simulate_minor_command    : (string * var_res_base.var_res_inference) list
85    val INFERENCES_LIST___expensive_simplifications : (string * var_res_base.var_res_inference) list
86    val INFERENCES_LIST___entailment_steps          : (string * var_res_base.var_res_inference) list
87
88    val VAR_RES_IS_PURE_PROPOSITION___provers : (term -> term -> thm) list
89  end
90
91  structure holfoot_tactics : sig
92   type var_res_inference_group =
93     (* group name (used for debug) *)
94     string *
95     (* group guard, inferences are just applied to
96        terms that satisfy this guard *)
97     (Abbrev.term -> bool) *
98     (* apply before working on subterms *)
99     bool *
100     (* use this inference group to clean up after a "bigger" step *)
101     bool *
102     (* the members of the group, each with a name for debugging *)
103     (string * holfoot_param.var_res_base.var_res_inference) list;
104
105   type user_rewrite_param = (Abbrev.thm list * Abbrev.conv list * simpLib.ssfrag list);
106   type gen_step_param = {use_asms       : bool,
107                          do_case_splits : bool,
108                          expands_level  : int,
109                          generate_vcs   : bool,
110                          fast           : bool,
111                          stop_evals     : (Abbrev.term -> bool) list,
112                          prop_simp_level: int,
113                          inferences     : (int * var_res_inference_group) list *
114                                           (int * var_res_inference_group) list *
115                                           (int * var_res_inference_group) list};
116
117   datatype gen_step_tac_opt =
118       case_splits_flag of bool
119     | expands_level of int
120     | fast_flag of bool
121     | prop_simp_level of int
122     | use_asms_flag of bool
123     | generate_vcs_flag of bool
124     | add_rewrites of Abbrev.thm list
125     | add_convs of Abbrev.conv list
126     | add_ssfrags of simpLib.ssfrag list
127     | stop_evals of (Abbrev.term -> bool) list
128     | combined_gen_step_tac_opt of gen_step_tac_opt list
129     | add_inference_groups of (int * var_res_inference_group) list *
130                               (int * var_res_inference_group) list *
131                               (int * var_res_inference_group) list;
132
133   val no_case_splits        : gen_step_tac_opt;
134   val do_case_splits        : gen_step_tac_opt;
135   val no_expands            : gen_step_tac_opt;
136   val do_expands            : gen_step_tac_opt;
137   val full_expands          : gen_step_tac_opt;
138   val no_case_split_expands : gen_step_tac_opt;
139   val generate_vcs          : gen_step_tac_opt;
140   val dont_generate_vcs     : gen_step_tac_opt;
141   val no_asms               : gen_step_tac_opt;
142   val use_asms              : gen_step_tac_opt;
143   val no_prop_simps         : gen_step_tac_opt;
144   val simple_prop_simps     : gen_step_tac_opt;
145   val conservative          : gen_step_tac_opt; (* not fast *)
146   val careful               : gen_step_tac_opt; (* no asms. no case splits, no expands *)
147   val stop_at_cond          : gen_step_tac_opt;
148   val stop_at_while         : gen_step_tac_opt;
149   val stop_at_abstraction   : gen_step_tac_opt;
150   val stop_at_frame_calc    : gen_step_tac_opt;
151   val stop_at_hoare_triple  : gen_step_tac_opt;
152   val stop_at_block_spec    : gen_step_tac_opt;
153
154   val gen_step_param___update_use_asms   : gen_step_param -> bool -> gen_step_param
155   val gen_step_param___update_cs         : gen_step_param -> bool -> gen_step_param
156   val gen_step_param___update_vcs        : gen_step_param -> bool -> gen_step_param
157   val gen_step_param___update_expands    : gen_step_param -> int  -> gen_step_param
158   val gen_step_param___update_fast       : gen_step_param -> bool -> gen_step_param
159   val gen_step_param___update_prop_simps : gen_step_param -> int  -> gen_step_param
160   val gen_step_param___update_stop_evals : gen_step_param -> (Abbrev.term -> bool) list -> gen_step_param
161   val gen_step_param___update_inferences : gen_step_param -> (
162                               (int * var_res_inference_group) list *
163                               (int * var_res_inference_group) list *
164                               (int * var_res_inference_group) list) -> gen_step_param
165
166   val gen_step_param___add_inferences    : gen_step_param -> (
167                               (int * var_res_inference_group) list *
168                               (int * var_res_inference_group) list *
169                               (int * var_res_inference_group) list) -> gen_step_param
170
171   val VAR_RES_GEN_STEP_CONSEQ_CONV : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv
172   val VAR_RES_GEN_STEP_TAC         : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.tactic
173   val xVAR_RES_GEN_STEP_CONSEQ_CONV: gen_step_tac_opt list -> int option -> int -> Abbrev.conv
174   val xVAR_RES_GEN_STEP_TAC        : gen_step_tac_opt list -> int option -> int -> Abbrev.tactic
175
176   val VAR_RES_PURE_VC_TAC          : Abbrev.tactic;
177   val VAR_RES_ELIM_COMMENTS_TAC    : Abbrev.tactic
178   val VAR_RES_VC_TAC               : Abbrev.tactic;
179   val VAR_RES_SPECIFICATION___CONSEQ_CONV : ConseqConv.conseq_conv
180   val VAR_RES_SPECIFICATION_TAC    : Abbrev.tactic
181   val VAR_RES_ENTAILMENT_INIT___CONSEQ_CONV : ConseqConv.conseq_conv
182   val VAR_RES_ENTAILMENT_INIT_TAC   : Abbrev.tactic
183end
184
185
186   val add_rewrites : Abbrev.thm list -> holfoot_tactics.gen_step_tac_opt;
187   val add_convs : Abbrev.conv list -> holfoot_tactics.gen_step_tac_opt;
188   val add_ssfrags : simpLib.ssfrag list -> holfoot_tactics.gen_step_tac_opt;
189   val combined_gen_step_tac_opt : holfoot_tactics.gen_step_tac_opt list -> holfoot_tactics.gen_step_tac_opt;
190   val add_inference_groups  : (int * holfoot_tactics.var_res_inference_group) list *
191                               (int * holfoot_tactics.var_res_inference_group) list *
192                               (int * holfoot_tactics.var_res_inference_group) list -> holfoot_tactics.gen_step_tac_opt
193   val no_case_splits        : holfoot_tactics.gen_step_tac_opt;
194   val do_case_splits        : holfoot_tactics.gen_step_tac_opt;
195   val no_expands            : holfoot_tactics.gen_step_tac_opt;
196   val do_expands            : holfoot_tactics.gen_step_tac_opt;
197   val full_expands          : holfoot_tactics.gen_step_tac_opt;
198   val no_case_split_expands : holfoot_tactics.gen_step_tac_opt;
199   val generate_vcs          : holfoot_tactics.gen_step_tac_opt;
200   val dont_generate_vcs     : holfoot_tactics.gen_step_tac_opt;
201   val no_asms               : holfoot_tactics.gen_step_tac_opt;
202   val use_asms              : holfoot_tactics.gen_step_tac_opt;
203   val no_prop_simps         : holfoot_tactics.gen_step_tac_opt;
204   val simple_prop_simps     : holfoot_tactics.gen_step_tac_opt;
205   val conservative          : holfoot_tactics.gen_step_tac_opt; (* not fast *)
206   val careful               : holfoot_tactics.gen_step_tac_opt; (* no asms. no case splits, no expands *)
207   val stop_at_cond          : holfoot_tactics.gen_step_tac_opt;
208   val stop_at_while         : holfoot_tactics.gen_step_tac_opt;
209   val stop_at_abstraction   : holfoot_tactics.gen_step_tac_opt;
210   val stop_at_frame_calc    : holfoot_tactics.gen_step_tac_opt;
211   val stop_at_hoare_triple  : holfoot_tactics.gen_step_tac_opt;
212   val stop_at_block_spec    : holfoot_tactics.gen_step_tac_opt;
213
214   val default_holfoot_gst_optL : holfoot_tactics.gen_step_tac_opt list ref;
215
216   val HF_GEN_STEP_CONSEQ_CONV : holfoot_tactics.gen_step_param -> holfoot_tactics.user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv
217   val HF_GEN_STEP_TAC         : holfoot_tactics.gen_step_param -> holfoot_tactics.user_rewrite_param -> int option -> int -> Abbrev.tactic
218   val xHF_GEN_STEP_CONSEQ_CONV: holfoot_tactics.gen_step_tac_opt list -> int option -> int -> Abbrev.conv
219   val xHF_GEN_STEP_TAC        : holfoot_tactics.gen_step_tac_opt list -> int option -> int -> Abbrev.tactic
220
221   val xHF_STEP_TAC            : holfoot_tactics.gen_step_tac_opt list -> int -> Abbrev.tactic;
222   val xHF_STEP_TAC_n          : holfoot_tactics.gen_step_tac_opt list -> int -> int option -> Abbrev.tactic;
223   val xHF_SOLVE_TAC           : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic;
224   val xHF_CONTINUE_TAC        : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic;
225   val xHF_SIMPLIFY_TAC        : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic;
226
227   val HF_STEP_TAC             : int -> Abbrev.tactic;
228   val HF_STEP_TAC_n           : int -> int option -> Abbrev.tactic;
229   val HF_SOLVE_TAC            : Abbrev.tactic;
230   val HF_CONTINUE_TAC         : Abbrev.tactic;
231   val HF_SIMPLIFY_TAC         : Abbrev.tactic;
232   val HF_VC_SOLVE_TAC         : Abbrev.tactic;
233
234   val HF_PURE_VC_TAC          : Abbrev.tactic;
235   val HF_ELIM_COMMENTS_TAC    : Abbrev.tactic
236   val HF_VC_TAC               : Abbrev.tactic;
237   val HF_SPECIFICATION_TAC    : Abbrev.tactic
238   val HF_INIT_TAC             : Abbrev.tactic
239   val HF_SPECIFICATION_CONSEQ_CONV : ConseqConv.conseq_conv
240
241
242   val holfoot_set_goal                : string -> proofManagerLib.proofs
243   val holfoot_set_goal_preprocess     : string -> proofManagerLib.proofs
244   val holfoot_set_goal_specs          : string -> string list -> proofManagerLib.proofs
245   val holfoot_set_goal_procedures     : string -> string list -> proofManagerLib.proofs
246   val holfoot_auto_verify_spec        : string -> thm
247   val holfoot_verify_spec             : string -> holfoot_tactics.gen_step_tac_opt list -> thm
248   val holfoot_tac_verify_spec         : string -> (holfoot_tactics.gen_step_tac_opt list) option -> (string * tactic) list -> thm
249   val holfoot_interactive_verify_spec : bool -> bool -> string -> (holfoot_tactics.gen_step_tac_opt list) option -> (string * tactic) list -> (thm * bool)
250   val holfoot_prove_remaining         : (thm * tactic) -> thm
251   val holfoot_set_remaining_goal      : thm -> proofManagerLib.proofs
252
253   val holfoot_prover_extras_1 : thm list ref;
254   val holfoot_prover_extras_2 : thm list ref;
255   val holfoot_varlist_rwts    : thm list ref;
256   val update_var_res_param    : unit -> unit;
257end
258