1signature ThyDataSexp =
2sig
3
4datatype t =
5         Int of int
6       | String of string
7       | List of t list
8       | Term of Term.term
9       | Type of Type.hol_type
10       | Thm of Thm.thm
11       | Sym of string
12       | Bool of bool
13       | Char of char
14       | Option of t option
15
16val uptodate : t -> bool
17val compare : t * t -> order
18
19(* note that merge functions must take identical "types" on both sides.
20   Thus, if the theory data is a list of values, both old and new should be
21   lists and the merge will effectively be an append.  If there's just one
22   value being "merged", it should still be a singleton list.
23
24   Similarly, if the data is a dictionary, represented as an alist, then the
25   new data (representing a single key-value maplet) should be a singleton
26   alist
27*)
28val alist_merge : {old: t, new : t} -> t
29val append_merge : {old : t, new : t} -> t
30
31val new : {thydataty : string,
32           merge : {old : t, new : t} -> t,
33           load : {thyname : string, data : t} -> unit,
34           other_tds : t * TheoryDelta.t -> t} ->
35          {export : t -> unit, segment_data : {thyname : string} -> t option}
36
37val pp_sexp : Type.hol_type PP.pprinter -> Term.term PP.pprinter ->
38              Thm.thm PP.pprinter -> t PP.pprinter
39
40end
41