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