1signature helperLib =
2sig
3
4    include Abbrev
5
6    type instruction =
7        (thm * int * int option) * (thm * int * int option) option
8
9    (* (derive spec, generate branch, status thm, program counter term) *)
10    type decompiler_tools =
11      (string -> instruction) * (term -> term -> int -> bool -> string * int) *
12      Thm.thm * Term.term
13
14    datatype ftree_type =
15      FUN_IF of term * ftree_type * ftree_type
16    | FUN_LET of term * term * ftree_type
17    | FUN_COND of term * ftree_type
18    | FUN_VAL of term;
19
20    val \\                     : tactic * tactic -> tactic
21    val RW                     : thm list -> rule
22    val RW1                    : thm list -> rule
23
24    val echo                   : int -> string -> unit
25    val set_echo               : int -> unit
26
27    val cache                  : (string -> 'a) -> string -> 'a
28    val to_lower               : string -> string
29    val remove_whitespace      : string -> string
30    val quote_to_strings       : 'a quotation -> string list
31
32    val instruction_apply      : (thm -> thm) -> instruction -> instruction
33
34    val all_distinct           : ''a list -> ''a list
35    val replace_terml          : (term -> term) -> term -> term
36    val collect_term_of_type   : hol_type -> term -> term list
37    val find_terml             : (term -> bool) -> term -> term list
38    val find_terml_all         : (term -> bool) -> term -> term list
39    val remove_primes          : thm -> thm
40
41    val car                    : term -> term
42    val cdr                    : term -> term
43    val list_dest              : ('a -> 'a * 'a) -> 'a -> 'a list
44    val list_mk                : (term * term -> term) -> term list -> term -> term
45    val is_normal_char         : char -> bool
46    val mk_cond_star           : term * term -> term
47    val mk_sidecond_star       : term * term -> term
48    val mk_star                : term * term -> term
49    val mk_sep_disj            : term * term -> term
50    val mk_sep_hide            : term -> term
51    val mk_sep_exists          : term * term -> term
52    val dest_star              : term -> term * term
53    val dest_sep_disj          : term -> term * term
54    val dest_sep_hide          : term -> term
55    val dest_sep_exists        : term -> term * term
56    val dest_spec              : term -> term * term * term * term
57    val get_sep_domain         : term -> term
58    val list_mk_star           : term list -> hol_type -> term
59    val word_patterns          : term list
60
61    val eval_term_ss           : string -> term -> simpLib.ssfrag
62    val sep_cond_ss            : simpLib.ssfrag
63    val star_ss                : simpLib.ssfrag
64    val sw2sw_ss               : simpLib.ssfrag
65    val w2w_ss                 : simpLib.ssfrag
66    val pbeta_ss               : simpLib.ssfrag
67
68    val EVAL_ANY_MATCH_CONV    : term list -> conv
69    val EVERY_MATCH_MOVE_OUT_CONV : term -> conv
70    val FIX_WORD32_ARITH_CONV  : conv
71    val FORCE_PBETA_CONV       : conv
72    val GEN_MOVE_OUT_CONV      : (term list -> term list) -> conv
73    val LIST_MOVE_OUT_CONV     : bool -> term list -> conv
74    val MATCH_MOVE_OUT_CONV    : term list -> conv
75    val MERGE_CONDS_CONV       : conv
76    val MOVE_OUT_CONV          : term -> conv
77    val MOVE_STAR_CONV         : term -> conv
78    val POST_CONV              : conv -> conv
79    val PRE_CONV               : conv -> conv
80    val PRE_POST_CONV          : conv -> conv
81    val SEP_EXISTS_AC_CONV     : conv
82    val STAR_AC_CONV           : conv
83    val STAR_REVERSE_CONV      : conv
84    val STAR_REWRITE_CONV      : thm -> conv
85
86    val tm2ftree               : term -> ftree_type
87    val ftree2tm               : ftree_type -> term
88
89    val MATCH_INST             : thm -> term -> thm
90
91    val BASIC_SEP_REWRITE_RULE : thm -> rule
92    val EXISTS_PRE             : term frag list -> rule
93    val EXISTS_SEP_REWRITE_RULE : thm -> rule
94    val HIDE_POST_RULE         : term -> rule
95    val HIDE_PRE_RULE          : term -> rule
96    val HIDE_PRE_STATUS_RULE   : thm -> rule
97    val HIDE_STATUS_RULE       : bool -> thm -> rule
98    val INST_SPEC              : thm -> rule
99    val LIST_HIDE_POST_RULE    : term list -> rule
100    val MERGE_CONDS_RULE       : rule
101    val MOVE_COND_RULE         : term -> rule
102    val PRE_POST_RULE          : conv -> rule
103    val SEP_EXISTS_ELIM_RULE   : rule
104    val SEP_EXISTS_POST_RULE   : term -> rule
105    val SEP_EXISTS_PRE_RULE    : term -> rule
106    val SEP_REWRITE_RULE       : thm list -> rule
107    val SUBST_INST             : {redex: term, residue: term} list -> rule
108    val UNHIDE_PRE_RULE        : term -> rule
109
110    val HIDE_SEP_IMP_POST_RULE      : term -> rule
111    val LIST_HIDE_SEP_IMP_POST_RULE : term list -> rule
112    val SEP_EXISTS_SEP_IMP          : term -> term -> thm
113
114    val SPEC_STRENGTHEN_RULE   : thm -> term -> thm * term
115    val SPEC_WEAKEN_RULE       : thm -> term -> thm * term
116    val SPEC_BOOL_FRAME_RULE   : thm -> term -> thm
117    val SPEC_FRAME_RULE        : thm -> term -> thm
118    val SPECC_FRAME_RULE       : term -> rule
119    val SPECL_FRAME_RULE       : term list -> rule
120    val SPEC_COMPOSE_RULE      : thm list -> thm
121    val SPEC_SORT_CODE_RULE    : rule
122
123    val SPEC_PROVE_TAC         : thm list -> tactic
124
125    val ALIGNED_TAC            : tactic
126    val SEP_READ_TAC           : tactic
127    val SEP_WRITE_TAC          : tactic
128    val SEP_NEQ_TAC            : tactic
129
130    val CLEAN_TAC              : tactic
131    val EXPAND_TAC             : tactic
132    val SEP_F_TAC              : tactic
133    val SEP_I_TAC              : string -> tactic
134    val SEP_W_TAC              : tactic
135    val SEP_R_TAC              : tactic
136    val SEP_S_TAC              : string list -> thm -> tactic
137    val SEP_IMP_TAC            : tactic
138
139    val auto_prove             : string -> term * tactic -> thm
140
141    val add_executable_data_name    : string -> unit
142    val remove_executable_data_name : string -> unit
143    val parse_renamer               : string -> string * (thm -> thm) * bool
144
145end
146