1signature Theory =
2sig
3
4  type hol_type  = Type.hol_type
5  type term      = Term.term
6  type thm       = Thm.thm
7  type thy_addon = {sig_ps    : (unit -> HOLPP.pretty) option,
8                    struct_ps : (unit -> HOLPP.pretty) option}
9  type num = Arbnum.num
10
11(* Create a new theory *)
12
13  val new_theory         : string -> unit
14
15(* Add to the current theory segment *)
16
17  val temp_binding       : string -> string
18  val is_temp_binding    : string -> bool
19  val dest_temp_binding  : string -> string
20  val new_type           : string * int -> unit
21  val new_constant       : string * hol_type -> unit
22  val new_axiom          : string * term -> thm
23  val save_thm           : string * thm -> thm
24
25(* Delete from the current theory segment *)
26
27  val delete_type        : string -> unit
28  val delete_const       : string -> unit
29  val delete_binding     : string -> unit
30
31(* Information on the current theory segment *)
32
33  val current_theory     : unit -> string
34  val stamp              : string -> Time.time
35  val parents            : string -> string list
36  val ancestry           : string -> string list
37  val types              : string -> (string * int) list
38  val constants          : string -> term list
39  val current_axioms     : unit -> (string * thm) list
40  val current_theorems   : unit -> (string * thm) list
41  val current_definitions : unit -> (string * thm) list
42  val current_ML_deps    : unit -> string list
43
44(* Support for persistent theories *)
45
46  val adjoin_to_theory       : thy_addon -> unit
47  val quote_adjoin_to_theory : string quotation -> string quotation -> unit
48  val export_theory          : unit -> unit
49
50(* Make hooks available so that theory changes can be seen by
51   "interested parties" *)
52  val register_hook : string * (TheoryDelta.t -> unit) -> unit
53  val delete_hook : string -> unit
54  val get_hooks : unit -> (string * (TheoryDelta.t -> unit)) list
55  val disable_hook : string -> ('a -> 'b) -> 'a -> 'b
56  val enable_hook : string -> ('a -> 'b) -> 'a -> 'b
57
58(* -- and persistent data added to theories *)
59  structure LoadableThyData : sig
60    type t
61    val new : {thydataty : string,
62               merge : 'a * 'a -> 'a,
63               terms : 'a -> term list,
64               read : (string -> term) -> string -> 'a option,
65               write : (term -> string) -> 'a -> string} ->
66              ('a -> t) * (t -> 'a option)
67    val segment_data : {thy: string, thydataty: string} -> t option
68
69    val write_data_update : {thydataty : string, data : t} -> unit
70    val set_theory_data : {thydataty : string, data : t} -> unit
71    (* call these in a session to update and record something for later -
72       these will update segment data, and  also cause a call to
73       temp_encoded_update to appear in the theory file meaning that the
74       change to the data will persist/be exported.  The first,
75       write_data_update uses the merge functionality to augment what has
76       already been stored.  The set_theory_data function overrides whatever
77       might have been there. *)
78
79    val temp_encoded_update : {thy : string, thydataty : string,
80                               read : string -> term,
81                               data : string} -> unit
82    (* updates segment data using an encoded string *)
83  end
84
85(* Extensions by definition *)
86  structure Definition : sig
87    val new_type_definition    : string * thm -> thm
88    val new_definition         : string * term -> thm
89    val new_specification      : string * string list * thm -> thm
90    val gen_new_specification  : string * thm -> thm
91
92    val new_definition_hook    : ((term -> term list * term) *
93                                  (term list * thm -> thm)) ref
94  end
95
96(* Freshness information on HOL objects *)
97
98  val uptodate_type      : hol_type -> bool
99  val uptodate_term      : term -> bool
100  val uptodate_thm       : thm -> bool
101  val scrub              : unit -> unit
102
103  val try_theory_extension : ('a -> 'b) -> 'a -> 'b
104
105(* Changing internal bindings of ML-level names to theory objects *)
106
107  val set_MLname         : string -> string -> unit
108
109(* recording a dependency of the theory on an ML module *)
110  val add_ML_dependency  : string -> unit
111
112(* For internal use *)
113
114  val pp_thm             : (thm -> HOLPP.pretty) ref
115  val link_parents       : string*num*num -> (string*num*num) list -> unit
116  val incorporate_types  : string -> (string*int) list -> unit
117
118
119  val store_definition   : string * thm -> thm
120  val incorporate_consts : string -> hol_type Vector.vector ->
121                           (string*int) list -> unit
122  (* Theory files (which are just SML source code) call this function as
123     the last thing done when they load.  This will in turn cause a
124     TheoryDelta event to be sent to all registered listeners *)
125  val load_complete : string -> unit
126
127end
128