1structure ThyDataSexp :> ThyDataSexp =
2struct
3
4open Feedback Term Thm Theory
5
6val ERR = mk_HOL_ERR "ThyDataSexp"
7
8datatype t =
9         Int of int
10       | String of string
11       | List of t list
12       | Term of Term.term
13       | Type of Type.hol_type
14       | Thm of Thm.thm
15       | Sym of string
16       | Bool of bool
17       | Char of char
18       | Option of t option
19
20fun pp_sexp typ tmp thp s =
21  let
22    open PP
23    val pp = pp_sexp typ tmp thp
24    fun safechar c = Char.isGraph c andalso c <> #"\""
25  in
26    case s of
27        Int i => add_string (Int.toString i)
28      | String s => add_string ("\"" ^ String.toString s ^ "\"")
29      | List sl => block INCONSISTENT 1 (
30                    add_string "(" ::
31                    pr_list pp [add_break(1,0)] sl @
32                    [add_string ")"]
33                  )
34      | Term tm => tmp tm
35      | Type ty => typ ty
36      | Thm th => thp th
37      | Sym s => if CharVector.all safechar s then
38                   add_string s
39                 else add_string ("|\"" ^ String.toString s ^ "\"|")
40      | Bool b => if b then add_string "'t" else add_string "'f"
41      | Char c => add_string ("#\"" ^ Char.toString c ^ "\"")
42      | Option NONE => add_string "NONE"
43      | Option (SOME s) =>
44          block INCONSISTENT 1 [
45            add_string "(", add_string "SOME",
46            add_break(1,0), pp s, add_string ")"
47          ]
48  end
49
50fun uptodate s =
51  case s of
52      Term tm => Term.uptodate_term tm
53    | Type ty => Type.uptodate_type ty
54    | Thm th => Theory.uptodate_thm th
55    | List sl => List.all uptodate sl
56    | Option NONE => true
57    | Option (SOME s0) => uptodate s0
58    | _ => true
59
60fun compare (s1, s2) =
61  case (s1, s2) of
62      (Int i1, Int i2) => Int.compare(i1,i2)
63    | (Int _, _) => LESS
64    | (_, Int _) => GREATER
65
66    | (String s1, String s2) => String.compare(s1,s2)
67    | (String _, _) => LESS
68    | (_, String _) => GREATER
69
70    | (List l1, List l2) => Lib.list_compare compare (l1, l2)
71    | (List _, _) => LESS
72    | (_, List _) => GREATER
73
74    | (Term t1, Term t2) => Term.compare(t1,t2)
75    | (Term _, _) => LESS
76    | (_, Term _) => GREATER
77
78    | (Type ty1, Type ty2) => Type.compare(ty1, ty2)
79    | (Type _, _) => LESS
80    | (_, Type _) => GREATER
81
82    | (Thm th1, Thm th2) =>
83      Lib.pair_compare (Lib.list_compare Term.compare, Term.compare)
84                       ((hyp th1, concl th1), (hyp th2, concl th2))
85    | (Thm _, _) => LESS
86    | (_, Thm _) => GREATER
87
88    | (Sym s1, Sym s2) => String.compare (s1, s2)
89    | (Sym _, _) => LESS
90    | (_, Sym _) => GREATER
91
92    | (Bool b1, Bool b2) => Lib.bool_compare(b1, b2)
93    | (Bool _, _) => LESS
94    | (_, Bool _) => GREATER
95
96    | (Char c1, Char c2) => Char.compare (c1, c2)
97    | (Char _, _) => LESS
98    | (_, Char _) => GREATER
99
100    | (Option opt1, Option opt2) => Lib.option_compare compare (opt1, opt2)
101
102fun update_alist (kv, es) =
103  let
104    val k = case kv of List[k,_] => k | _=> raise ERR "update_alist" "kv shape"
105    fun recurse es =
106      case es of
107          [] => [kv]
108        | (e as List [k',_])::rest =>
109            if compare(k, k') = EQUAL then kv::rest
110            else e :: recurse rest
111        | _ => raise ERR "update_alist" "alist of bad shape"
112  in
113    recurse es
114  end
115
116fun alist_merge {old = s1, new = s2} =
117  case (s1, s2) of
118      (List dict, List updates) =>
119      let
120        val dict' = foldl update_alist dict updates
121      in
122        List dict'
123      end
124    | _ => raise ERR "alist_merge" "bad inputs"
125
126fun append_merge {old, new} =
127  case (old, new) of
128      (List l1, List l2) => List (l1 @ l2)
129    | _ => raise ERR "append_merge" "bad inputs"
130
131fun sterms0 (s, acc) =
132  case s of
133      List sl => List.foldl sterms0 acc sl
134    | Term tm => tm::acc
135    | Thm th => concl th :: (hyp th @ acc)
136    | Type ty => Term.mk_var("x", ty) :: acc
137    | Option (SOME s0) => sterms0 (s0, acc)
138    | _ => acc
139fun sterms s = sterms0 (s, [])
140
141open Coding
142fun listwrite w l =
143  IntData.encode (length l) ^ String.concat (List.map w l)
144val >~ = op>-
145infix 2 >~ >* >>
146infix 0 ||
147fun ntimes n r =
148  if n <= 0 then return []
149  else r >~ (fn h => ntimes (n-1) r >~ (fn t => return (h::t)))
150fun listreader r =
151  IntData.reader >~ (fn i => ntimes i r)
152
153fun dlwrite (s, ilist) =
154  StringData.encode s ^ listwrite IntData.encode ilist
155val dlreader = StringData.reader >* listreader IntData.reader
156
157fun tagwrite t =
158  let
159    val dep = Tag.dep_of t
160    val (ocl, _) = Tag.dest_tag t
161    val ((s,n), thydl) =
162        case dep of
163            Dep.DEP_SAVED p => p
164          | _ => raise mk_HOL_ERR "ThyDataSexp" "tagwrite" "Bad dep"
165  in
166    StringData.encode s ^ IntData.encode n ^
167    listwrite dlwrite thydl ^
168    listwrite StringData.encode ocl
169  end
170
171val tagreader =
172    let
173      fun combine (s,(n,(dls,ocls))) : Thm.depdisk * string list =
174        (((s,n), dls), ocls)
175    in
176      map combine
177          (StringData.reader >* (
178              IntData.reader >*
179                (listreader dlreader >* listreader StringData.reader)))
180    end
181
182fun deps_saved th =
183  case Tag.dep_of (Thm.tag th) of
184      Dep.DEP_SAVED _ => true
185    | _ => false
186
187fun thmwrite tmw th0 =
188  let
189    val th = if deps_saved th0 then th0
190             else Thm.save_dep (Theory.current_theory()) th0
191  in
192    tagwrite (Thm.tag th) ^
193    listwrite (StringData.encode o tmw) (concl th :: hyp th)
194  end
195fun thmreader tmr =
196  map Thm.disk_thm (tagreader >* listreader (map tmr StringData.reader))
197
198fun write tmw s =
199  case s of
200      Int i => "I" ^ Coding.IntData.encode i
201    | String s => "S" ^ Coding.StringData.encode s
202    | List sl => "L" ^ listwrite (write tmw) sl
203    | Term tm => "T" ^ StringData.encode (tmw tm)
204    | Type ty => "Y" ^ StringData.encode (tmw (Term.mk_var("x", ty)))
205    | Thm th => "H" ^ thmwrite tmw th
206    | Sym s => "M" ^ StringData.encode s
207    | Char c => "C" ^ CharData.encode c
208    | Bool b => "B" ^ BoolData.encode b
209    | Option NONE => "N"
210    | Option (SOME s) => "S" ^ write tmw s
211
212fun reader tmr s = (* necessary eta-expansion! *)
213  let
214    val core =
215        literal "I" >> map Int (IntData.reader) ||
216        literal "S" >> map String (StringData.reader) ||
217        literal "L" >> map List (listreader (reader tmr)) ||
218        literal "T" >> map (Term o tmr) (StringData.reader) ||
219        literal "Y" >> map (Type o type_of o tmr) (StringData.reader) ||
220        literal "H" >> map Thm (thmreader tmr) ||
221        literal "M" >> map Sym StringData.reader ||
222        literal "C" >> map Char CharData.reader ||
223        literal "B" >> map Bool BoolData.reader ||
224        literal "N" >> return (Option NONE) ||
225        literal "S" >> map (Option o SOME) (reader tmr)
226  in
227    core s
228  end
229
230structure LTD = LoadableThyData
231fun new {thydataty, load, other_tds, merge} =
232  let
233    val (todata, fromdata) =
234        LTD.new{thydataty = thydataty,
235                merge = (fn (t1,t2) => merge {old = t1, new = t2}),
236                terms = sterms, read = lift o reader, write = write}
237    fun segment_data {thyname} =
238      Option.join
239        (Option.map fromdata
240                    (LTD.segment_data{thy = thyname, thydataty = thydataty}))
241
242    fun onload thyname =
243      case segment_data{thyname = thyname} of
244          NONE => ()
245        | SOME s =>
246            load {thyname = thyname, data = s}
247
248    fun hook0 td =
249      case segment_data {thyname = current_theory()} of
250          NONE => ()
251        | SOME d0 =>
252            LTD.set_theory_data {thydataty = thydataty,
253                                 data = todata (other_tds(d0,td))}
254
255    fun hook (TheoryDelta.TheoryLoaded s) = onload s
256      | hook td = hook0 td
257
258    fun export s =
259      (load {thyname = current_theory(), data = s};
260       LTD.write_data_update {thydataty = thydataty, data = todata s})
261
262  in
263    register_hook ("ThmSetData.onload." ^ thydataty, hook);
264    List.app onload (ancestry "-");
265    {export = export, segment_data = segment_data}
266  end
267
268end
269