1structure DiskThms :> DiskThms = 2struct 3 4 open HolKernel SharingTables 5 6 fun to_sexp thms = 7 let 8 val ed = {named_terms = [], unnamed_terms = [], 9 named_types = [], unnamed_types = [], 10 theorems = thms} : extract_data 11 val sdo = build_sharing_data ed 12 in 13 enc_sdata sdo 14 end 15 16 fun write_stream hnd named_thms = 17 HOLPP.prettyPrint ((fn s => TextIO.output(hnd, s)), 75) 18 (HOLsexp.printer (to_sexp named_thms)) 19 20 fun write_file fname named_thms = let 21 open TextIO 22 val outstream = TextIO.openOut fname 23 in 24 write_stream outstream named_thms before TextIO.closeOut outstream 25 end 26 27 fun read_stream instream = 28 let 29 val t = HOLsexp.fromStream instream 30 handle Interrupt => raise Interrupt 31 | _ => raise Fail "Couldn't parse sexp from file" 32 in 33 case dec_sdata {with_strings = fn _ => (), with_stridty = fn _ => ()} t 34 of 35 NONE => raise Fail "Couldn't decode sexp" 36 | SOME sdi => 37 #theorems (export_from_sharing_data sdi) 38 end 39 40 fun read_file fname = 41 let 42 val strm = TextIO.openIn fname 43 val r = Exn.capture read_stream strm 44 val _ = TextIO.closeIn strm 45 in 46 Exn.release r 47 end 48 49end (* struct *) 50