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