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