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