1signature stateLib = 2sig 3 include Abbrev 4 5 type footprint_extra = (term * term) * (term -> term) * (term -> term) 6 val chunks_intro: bool -> thm -> rule 7 val chunks_intro_pre_process: thm -> rule 8 val define_map_component: string * string * thm -> thm * thm 9 val dest_code_access: term -> int * term 10 val fix_precond: thm list -> thm list 11 val generate_temporal: unit -> bool 12 val get_delta: term -> term -> int option 13 val get_pc_delta: (term -> bool) -> thm -> int option 14 val group_into_chunks: 15 (term -> term * term) * int * bool -> term list -> 16 {redex: term, residue: term} list list * (term * term) list 17 val gvar: string -> hol_type -> term 18 val introduce_triple_definition: bool * thm -> rule 19 val introduce_map_definition: thm * conv -> rule 20 val is_code_access: string * term -> term -> bool 21 val list_mk_code_pool: term * term * term list -> term 22 val mk_code_pool: term * term * term -> term 23 val mk_pre_post: 24 thm -> thm list -> (thm -> term * term * term) -> footprint_extra list -> 25 (term list * term list * term -> term list * term list) -> 26 (term list -> term list) -> 27 thm -> term 28 val pick_endian_rule: (term -> bool) * rule * rule -> rule 29 val pool_select_state_thm: thm -> thm list -> thm -> thm 30 val read_footprint: 31 thm -> thm list -> (thm -> term * term * term) -> footprint_extra list -> 32 thm -> term list * term * term * term 33 val register_combinations: 34 (term -> term * term) * int * (term -> int) option * conv * conv * conv * 35 term -> thm * term -> (thm * term) list 36 val rename_vars: 37 (string -> (term list -> string) option) * string list -> thm -> thm 38 val sep_array_intro: bool -> thm -> thm list -> rule 39 val sep_definitions: 40 string -> string list list -> string list list -> thm -> thm list 41 val set_temporal: bool -> unit 42 val spec: 43 thm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> 44 hol_type list -> tactic -> tactic -> thm * term -> thm 45 val split_cond: bool -> (term -> term) -> thm -> thm list 46 val star_select_state_thm: thm -> thm list -> term list * thm -> thm 47 val update_frame_state_thm: thm -> string list -> thm 48 val update_hidden_frame_state_thm: thm -> term list -> thm 49 val vvar: hol_type -> term 50 val varReset: unit -> unit 51 val write_footprint: 52 (string -> term * (term -> term) * (term -> term) * (term -> bool)) -> 53 (string -> term * (term * term -> term) * (term -> term * term) * 54 (term -> bool)) -> 55 (string * string * term) list -> 56 (string * string) list -> 57 (string * string) list -> 58 (string * (term list * term list * term -> term list * term list)) list -> 59 (string * term list -> bool) -> 60 term list * term list * term -> term list * term list 61 val MOVE_COND_CONV: conv 62 val MOVE_COND_RULE: term -> rule 63 val PC_CONV: string -> conv 64 val PRE_COND_CONV: conv -> conv 65end 66