1structure ThyDataSexp :> ThyDataSexp =
2struct
3
4open Feedback Term Thm Theory
5
6val ERR = mk_HOL_ERR "ThyDataSexp"
7
8val theory_debug_trace = get_tracefn "Theory.debug"
9
10fun DPRINT f =
11    if theory_debug_trace() <> 0 then
12      print ("ThyDataSexp/DEBUG: " ^ f () ^ "\n")
13    else ()
14
15datatype t =
16         Int of int
17       | String of string
18       | SharedString of string
19       | List of t list
20       | Term of Term.term
21       | Type of Type.hol_type
22       | Thm of Thm.thm
23       | Sym of string
24       | Bool of bool
25       | Char of char
26       | Option of t option
27       | KName of KernelSig.kernelname
28
29fun pp_sexp typ tmp thp s =
30  let
31    open PP
32    val pp = pp_sexp typ tmp thp
33    fun safechar c = Char.isGraph c andalso c <> #"\""
34  in
35    case s of
36        Int i => add_string (Int.toString i)
37      | String s => add_string ("\"" ^ String.toString s ^ "\"")
38      | SharedString s => add_string ("shared\"" ^ String.toString s ^"\"")
39      | List sl => block INCONSISTENT 1 (
40                    add_string "(" ::
41                    pr_list pp [add_break(1,0)] sl @
42                    [add_string ")"]
43                  )
44      | Term tm => tmp tm
45      | Type ty => typ ty
46      | Thm th => thp th
47      | Sym s => if CharVector.all safechar s then
48                   add_string s
49                 else add_string ("|\"" ^ String.toString s ^ "\"|")
50      | Bool b => if b then add_string "'t" else add_string "'f"
51      | Char c => add_string ("#\"" ^ Char.toString c ^ "\"")
52      | Option NONE => add_string "NONE"
53      | Option (SOME s) =>
54          block INCONSISTENT 1 [
55            add_string "(", add_string "SOME",
56            add_break(1,0), pp s, add_string ")"
57          ]
58      | KName {Thy,Name} =>
59          block CONSISTENT 1 [
60            add_string "{",
61            block CONSISTENT 0 [
62              add_string "Thy = ", add_break (1, 2),
63              add_string ("\"" ^ String.toString Thy ^ "\""),
64              add_string ","
65            ],
66            add_break (1,0),
67            block CONSISTENT 0 [
68              add_string "Name = ", add_break(1,2),
69              add_string ("\"" ^ String.toString Name ^ "\"")
70            ], add_string "}"
71          ]
72  end
73
74val bare_toString =
75    PP.pp_to_string 70 (pp_sexp (fn _ => PP.add_string "<type>")
76                                (fn _ => PP.add_string "<term>")
77                                (fn _ => PP.add_string "<thm>"))
78
79fun uptodate s =
80  case s of
81      Term tm => Term.uptodate_term tm
82    | Type ty => Type.uptodate_type ty
83    | Thm th => Theory.uptodate_thm th
84    | List sl => List.all uptodate sl
85    | Option NONE => true
86    | Option (SOME s0) => uptodate s0
87    | _ => true
88
89fun compare (s1, s2) =
90  case (s1, s2) of
91      (Int i1, Int i2) => Int.compare(i1,i2)
92    | (Int _, _) => LESS
93    | (_, Int _) => GREATER
94
95    | (String s1, String s2) => String.compare(s1,s2)
96    | (String _, _) => LESS
97    | (_, String _) => GREATER
98
99    | (SharedString s1, SharedString s2) => String.compare(s1,s2)
100    | (SharedString _, _) => LESS
101    | (_, SharedString _) => GREATER
102
103    | (List l1, List l2) => Lib.list_compare compare (l1, l2)
104    | (List _, _) => LESS
105    | (_, List _) => GREATER
106
107    | (Term t1, Term t2) => Term.compare(t1,t2)
108    | (Term _, _) => LESS
109    | (_, Term _) => GREATER
110
111    | (Type ty1, Type ty2) => Type.compare(ty1, ty2)
112    | (Type _, _) => LESS
113    | (_, Type _) => GREATER
114
115    | (Thm th1, Thm th2) =>
116      Lib.pair_compare (Lib.list_compare Term.compare, Term.compare)
117                       ((hyp th1, concl th1), (hyp th2, concl th2))
118    | (Thm _, _) => LESS
119    | (_, Thm _) => GREATER
120
121    | (Sym s1, Sym s2) => String.compare (s1, s2)
122    | (Sym _, _) => LESS
123    | (_, Sym _) => GREATER
124
125    | (Bool b1, Bool b2) => Lib.bool_compare(b1, b2)
126    | (Bool _, _) => LESS
127    | (_, Bool _) => GREATER
128
129    | (Char c1, Char c2) => Char.compare (c1, c2)
130    | (Char _, _) => LESS
131    | (_, Char _) => GREATER
132
133    | (Option opt1, Option opt2) => Lib.option_compare compare (opt1, opt2)
134    | (Option _, _) => LESS
135    | (_, Option _) => GREATER
136
137    | (KName {Thy=th1,Name=n1}, KName{Thy=th2,Name=n2}) =>
138      Lib.pair_compare (String.compare, String.compare) ((th1,n1), (th2,n2))
139
140
141fun update_alist (kv, es) =
142  let
143    val k = case kv of List[k,_] => k | _=> raise ERR "update_alist" "kv shape"
144    fun recurse es =
145      case es of
146          [] => [kv]
147        | (e as List [k',_])::rest =>
148            if compare(k, k') = EQUAL then kv::rest
149            else e :: recurse rest
150        | _ => raise ERR "update_alist" "alist of bad shape"
151  in
152    recurse es
153  end
154
155fun alist_merge {old = s1, new = s2} =
156  case (s1, s2) of
157      (List dict, List updates) =>
158      let
159        val dict' = foldl update_alist dict updates
160      in
161        List dict'
162      end
163    | _ => raise ERR "alist_merge" "bad inputs"
164
165fun append_merge {old, new} =
166  case (old, new) of
167      (List l1, List l2) => List (l1 @ l2)
168    | _ => raise ERR "append_merge" "bad inputs"
169
170fun sterms0 (s, acc as (strs,tms)) =
171  case s of
172      List sl => List.foldl sterms0 acc sl
173    | SharedString s => (s::strs,tms)
174    | Term tm => (strs,tm::tms)
175    | Thm th => (strs, concl th :: (hyp th @ tms))
176    | Type ty => (strs, Term.mk_var("x", ty) :: tms)
177    | Option (SOME s0) => sterms0 (s0, acc)
178    | KName{Thy,Name} => (Thy::Name::strs,tms)
179    | _ => acc
180fun sterms s = sterms0 (s,([],[]))
181
182infix >~ >> ||
183fun (f >~ g) = Option.mapPartial g o f
184fun (f >> g) = Option.map g o f
185fun (f || g) = fn x => case f x of NONE => g x | res => res
186
187val list_decode = HOLsexp.list_decode
188val string_decode = HOLsexp.string_decode
189val symbol_decode = HOLsexp.symbol_decode
190val pair_decode = HOLsexp.pair_decode
191val pair4_decode = HOLsexp.pair4_decode
192val int_decode = HOLsexp.int_decode
193val tagged_decode = HOLsexp.tagged_decode
194fun dlwrite (s, ilist) =
195    let open HOLsexp
196    in
197      pair_encode (String, list_encode Integer) (s,ilist)
198    end
199val dlreader = pair_decode (string_decode, list_decode int_decode)
200
201fun tagwrite t =
202  let
203    val dep = Tag.dep_of t
204    val (ocl, _) = Tag.dest_tag t
205    val ((s,n), thydl) =
206        case dep of
207            Dep.DEP_SAVED p => p
208          | _ => raise mk_HOL_ERR "ThyDataSexp" "tagwrite" "Bad dep"
209    open HOLsexp
210  in
211    pair4_encode (String, Integer, list_encode dlwrite, list_encode String)
212                 (s, n, thydl, ocl)
213  end
214
215val tagreader =
216    let
217      fun combine (s,n,dls,ocls) : Thm.depdisk * string list =
218        (((s,n), dls), ocls)
219    in
220      pair4_decode (string_decode, int_decode, list_decode dlreader,
221                    list_decode string_decode) >>
222      combine
223    end
224
225fun deps_saved th =
226  case Tag.dep_of (Thm.tag th) of
227      Dep.DEP_SAVED _ => true
228    | _ => false
229
230fun thmwrite tmw th0 =
231  let
232    val th = if deps_saved th0 then th0
233             else Thm.save_dep (Theory.current_theory()) th0
234  in
235    HOLsexp.pair_encode (tagwrite, HOLsexp.list_encode (HOLsexp.String o tmw))
236                        (Thm.tag th, concl th :: hyp th)
237  end
238fun thmreader tmr =
239    pair_decode (tagreader, list_decode (string_decode >> tmr)) >> Thm.disk_thm
240
241fun tag s enc x = HOLsexp.tagged_encode s enc x
242fun write (wrt as {strings,terms}) s =
243  case s of
244      Int i => HOLsexp.Integer i
245    | String s => HOLsexp.String s
246    | SharedString s => tag "tag-str" (HOLsexp.Integer o strings) s
247    | List sl => HOLsexp.list_encode (write wrt) sl
248    | Term tm => tag "tag-tm" HOLsexp.String (terms tm)
249    | Type ty => tag "tag-ty" HOLsexp.String (terms (Term.mk_var("x", ty)))
250    | Thm th => tag "tag-th" (thmwrite terms) th
251    | Sym s => HOLsexp.Symbol s
252    | Char c => tag "tag-ch" (HOLsexp.Integer o Char.ord) c
253    | Bool b => tag "tag-b" (fn b => if b then HOLsexp.Symbol "t"
254                                     else HOLsexp.Symbol "f") b
255    | Option NONE => tag "tag-none" (fn () => HOLsexp.Nil) ()
256    | Option (SOME s) => tag "tag-some" (write wrt) s
257    | KName {Thy,Name} => tag "tag-knm"
258                              (HOLsexp.pair_encode (HOLsexp.Integer o strings,
259                                                    HOLsexp.Integer o strings))
260                              (Thy,Name)
261
262fun reader (rd as {strings,terms}) s = (* necessary eta-expansion! *)
263  let
264    fun opt_chr i = if i < 256 then SOME (Char.chr i) else NONE
265    val core =
266        (int_decode >> Int) ||
267        (string_decode >> String) ||
268        (symbol_decode >> (fn s => if s = "nil" then List [] else Sym s)) ||
269        (tagged_decode "tag-str" (int_decode >> strings >> SharedString)) ||
270        (tagged_decode "tag-tm" string_decode >> terms >> Term) ||
271        (tagged_decode "tag-ty" string_decode >> terms >> type_of >> Type) ||
272        (tagged_decode "tag-th" (thmreader terms) >> Thm) ||
273        (tagged_decode "tag-ch" int_decode >~ opt_chr >> Char) ||
274        (tagged_decode "tag-b"
275                       (fn d => if d = HOLsexp.Symbol "f" then SOME (Bool false)
276                                else if d = HOLsexp.Symbol "t" then
277                                  SOME (Bool true)
278                                else NONE)) ||
279        (tagged_decode "tag-some" (reader rd) >> SOME >> Option) ||
280        (tagged_decode "tag-none" (fn d => if d = HOLsexp.Nil then
281                                         SOME (Option NONE)
282                                       else NONE)) ||
283        (tagged_decode "tag-knm"
284                       (pair_decode (int_decode >> strings,
285                                     int_decode >> strings)) >~
286                       (fn (thy,name) => SOME (KName {Thy=thy,Name=name}))) ||
287        (list_decode (reader rd) >> List)
288  in
289    core s
290  end
291
292structure LTD = LoadableThyData
293fun new {thydataty, load, other_tds, merge} =
294  let
295    val (todata, fromdata) =
296        LTD.new{thydataty = thydataty, pp = bare_toString,
297                merge = (fn (t1,t2) => merge {old = t1, new = t2}),
298                terms = #2 o sterms, strings = #1 o sterms,
299                read = reader, write = write}
300    fun segment_data {thyname} =
301      Option.join
302        (Option.map fromdata
303                    (LTD.segment_data{thy = thyname, thydataty = thydataty}))
304
305    fun onload thyname =
306      case segment_data{thyname = thyname} of
307          NONE => load {thyname = thyname, data = NONE}
308        | SOME s =>
309            load {thyname = thyname, data = SOME s}
310
311    fun hook0 td =
312      case segment_data {thyname = current_theory()} of
313          NONE => DPRINT (fn _ => "No seg-data to update for " ^ thydataty ^
314                                  "; return ()")
315        | SOME d0 =>
316          let
317          in
318            case other_tds(d0,td) of
319                NONE => DPRINT (fn _ => "Seg-data for " ^ thydataty ^ " is " ^
320                                        bare_toString d0 ^
321                                        " but leaving it alone")
322              | SOME newdata => (
323                  DPRINT (fn _ => thydataty ^ " hook causes write of " ^
324                                  bare_toString newdata);
325                  LTD.set_theory_data {thydataty = thydataty,
326                                       data = todata newdata}
327              )
328          end
329
330    fun hook (TheoryDelta.TheoryLoaded s) = onload s
331      | hook td = (DPRINT (fn _ => "Calling "^thydataty^"'s delta-hook");
332                   hook0 td)
333
334    fun export s =
335      (load {thyname = current_theory(), data = SOME s};
336       LTD.write_data_update {thydataty = thydataty, data = todata s})
337
338    fun set t =
339        LTD.set_theory_data{thydataty = thydataty, data = todata t}
340
341  in
342    register_hook ("ThmSetData.onload." ^ thydataty, hook);
343    List.app onload (ancestry "-");
344    {export = export, segment_data = segment_data, set = set}
345  end
346
347fun bind NONE f = NONE
348  | bind (SOME a) f = f a
349
350fun mmap f [] = SOME []
351  | mmap f (h::t) =
352    bind (f h) (fn h' => bind (mmap f t) (fn t' => SOME (h'::t')))
353
354fun list_decode d t =
355    case t of
356        List ts => mmap d ts
357      | _ => NONE
358
359fun mk_list m ts = List (map m ts)
360
361fun string_decode (String s) = SOME s
362  | string_decode _ = NONE
363
364fun int_decode (Int i) = SOME i
365  | int_decode _ = NONE
366
367fun char_decode (Char c) = SOME c
368  | char_decode _ = NONE
369
370fun kname_decode (KName v) = SOME v
371  | kname_decode _ = NONE
372
373fun type_decode (Type ty) = SOME ty
374  | type_decode _ = NONE
375
376fun term_decode (Term tm) = SOME tm
377  | term_decode _ = NONE
378
379fun bool_decode (Bool b) = SOME b
380  | bool_decode _ = NONE
381
382fun fail t = NONE
383fun first decoders =
384    case decoders of
385        [] => fail
386      | d::ds => d || first ds
387
388fun require_tag s t =
389    case t of
390        Sym s' => if s = s' then SOME () else NONE
391      | _ => NONE
392
393type 'a dec = t -> 'a option
394type 'a enc = 'a -> t
395
396fun option_encode enc NONE = Option NONE
397  | option_encode enc (SOME x) = Option (SOME (enc x))
398fun option_decode dec t =
399    case t of
400        Option NONE => SOME NONE
401      | Option (SOME x) =>
402          (case dec x of NONE => NONE | SOME v => SOME (SOME v))
403      | _ => NONE
404
405
406val pair_decode : 'a dec * 'b dec -> ('a*'b) dec =
407    fn (d1,d2) => fn t =>
408       case t of
409           List [e1,e2] => Option.mapPartial
410                             (fn r1 => Option.map (fn r2 => (r1,r2)) (d2 e2))
411                             (d1 e1)
412         | _ => NONE
413fun pair_encode (e1,e2) (x,y) = List [e1 x, e2 y]
414
415fun pair3_encode (e1,e2,e3) (x,y,z) = List [e1 x, e2 y, e3 z]
416fun pair3_decode (d1,d2,d3) t =
417    case t of
418        List [t1, t2, t3] => (case (d1 t1, d2 t2, d3 t3) of
419                                  (SOME x, SOME y, SOME z) => SOME (x,y,z)
420                                | _ => NONE)
421      | _ => NONE
422
423fun pair4_encode (e1,e2,e3,e4) (a,b,c,d) = List [e1 a, e2 b, e3 c, e4 d]
424fun pair4_decode (d1,d2,d3,d4) t =
425    case t of
426        List [t1,t2,t3,t4] =>
427        (case (d1 t1, d2 t2, d3 t3, d4 t4) of
428             (SOME a, SOME b, SOME c, SOME d) => SOME(a,b,c,d)
429           | _ => NONE)
430      | _ => NONE
431
432fun tag_decode s d t =
433    case t of
434        List [Sym s', t0] => if s = s' then d t0 else NONE
435      | List (Sym s' :: rest) => if s = s' then d (List rest) else NONE
436      | _ => NONE
437
438fun tag_encode s e x =
439    case e x of
440        List [t] => List [Sym s, List [t]]
441      | List els => List (Sym s :: els)
442      | t => List [Sym s, t]
443
444end
445