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