1(*---------------------------------------------------------------------------* 2 * * 3 * HOL theories interpreted by SML structures. * 4 * * 5 *---------------------------------------------------------------------------*) 6 7structure TheoryPP :> TheoryPP = 8struct 9 10type thm = Thm.thm; 11type term = Term.term 12type hol_type = Type.hol_type 13type shared_writemaps = {strings : string -> int, terms : Term.term -> string} 14type shared_readmaps = {strings : int -> string, terms : string -> Term.term} 15type struct_info_record = { 16 theory : string*Arbnum.num*Arbnum.num, 17 parents : (string*Arbnum.num*Arbnum.num) list, 18 types : (string*int) list, 19 constants : (string*hol_type) list, 20 axioms : (string * thm) list, 21 definitions : (string * thm) list, 22 theorems : (string * thm) list, 23 struct_ps : (unit -> PP.pretty) option list, 24 struct_pcps : (unit -> PP.pretty) list, 25 mldeps : string list, 26 thydata : string list * Term.term list * 27 (string,shared_writemaps -> HOLsexp.t)Binarymap.dict 28 } 29 30open Feedback Lib Portable Dep; 31 32val ERR = mk_HOL_ERR "TheoryPP"; 33 34val temp_binding_pfx = "@temp" 35val is_temp_binding = String.isPrefix temp_binding_pfx 36fun temp_binding s = temp_binding_pfx ^ s 37fun dest_temp_binding s = 38 if is_temp_binding s then 39 String.extract(s, size temp_binding_pfx, NONE) 40 else raise ERR "dest_temp_binding" "String not a temp-binding" 41 42 43val pp_sig_hook = ref (fn () => ()); 44 45val concat = String.concat; 46val sort = Lib.sort (fn s1:string => fn s2 => s1<=s2); 47val psort = Lib.sort (fn (s1:string,_:Thm.thm) => fn (s2,_:Thm.thm) => s1<=s2); 48fun Thry s = s^"Theory"; 49fun ThrySig s = Thry s 50 51fun with_parens pfn x = 52 let open Portable PP 53 in [add_string "(", pfn x, add_string ")"] 54 end 55 56fun pp_type mvartype mtype ty = 57 let open Portable Type PP 58 val pp_type = pp_type mvartype mtype 59 in 60 if is_vartype ty 61 then case dest_vartype ty 62 of "'a" => add_string "alpha" 63 | "'b" => add_string "beta" 64 | "'c" => add_string "gamma" 65 | "'d" => add_string "delta" 66 | s => add_string (mvartype^quote s) 67 else 68 case dest_thy_type ty 69 of {Tyop="bool",Thy="min", Args=[]} => add_string "bool" 70 | {Tyop="ind", Thy="min", Args=[]} => add_string "ind" 71 | {Tyop="fun", Thy="min", Args=[d,r]} => 72 block INCONSISTENT 1 [ 73 add_string "(", 74 pp_type d, 75 add_string " -->", 76 add_break (1,0), 77 pp_type r, 78 add_string ")" 79 ] 80 | {Tyop,Thy,Args} => 81 block INCONSISTENT (size mtype) [ 82 add_string mtype, 83 add_string (quote Tyop), 84 add_break (1,0), 85 add_string (quote Thy), 86 add_break (1,0), 87 add_string "[", 88 block INCONSISTENT 1 ( 89 pr_list pp_type [add_string ",", add_break (1,0)] Args 90 ), 91 add_string "]" 92 ] 93 end 94 95val include_docs = ref true 96val _ = Feedback.register_btrace ("TheoryPP.include_docs", include_docs) 97 98fun pp_sig pp_thm info_record = let 99 open PP 100 val {name,parents,axioms,definitions,theorems,sig_ps} = info_record 101 val parents' = sort parents 102 val rm_temp = List.filter (fn (s, _) => not (is_temp_binding s)) 103 val axioms' = psort axioms |> rm_temp 104 val definitions' = psort definitions |> rm_temp 105 val theorems' = psort theorems |> rm_temp 106 val thml = axioms@definitions@theorems 107 fun vblock(header, ob_pr, obs) = 108 block CONSISTENT 2 [ 109 add_string ("(* "^header^ " *)"), NL, 110 block CONSISTENT 0 (pr_list ob_pr [NL] obs) 111 ] 112 fun pparent s = String.concat ["structure ",Thry s," : ",ThrySig s] 113 val parentstring = "Parent theory of "^Lib.quote name 114 fun pr_parent s = block CONSISTENT 0 [ 115 add_string (String.concat ["[", s, "]"]), 116 add_break(1,0), 117 add_string parentstring] 118 fun pr_parents [] = [] 119 | pr_parents slist = 120 [block CONSISTENT 0 (pr_list pr_parent [NL, NL] slist), NL, NL] 121 122 fun pr_thm class (s,th) = 123 block CONSISTENT 3 [ 124 add_string (String.concat ["[", s, "]"]), 125 add_string (" "^class), NL, NL, 126 if null (Thm.hyp th) andalso 127 (Tag.isEmpty (Thm.tag th) orelse Tag.isDisk (Thm.tag th)) 128 then pp_thm th 129 else 130 with_flag(Globals.show_tags,true) 131 (with_flag(Globals.show_assums, true) pp_thm) th 132 ] 133 handle e => (print ("Failed to print theorem in theory export: "^s^"\n"); 134 print (General.exnMessage e ^ "\n"); 135 raise e) 136 fun pr_thms _ [] = [] 137 | pr_thms heading plist = 138 [block CONSISTENT 0 (pr_list (pr_thm heading) [NL,NL] plist), NL, NL] 139 fun pr_sig_ps NONE = [] (* won't be fired because of filtering below *) 140 | pr_sig_ps (SOME pp) = [pp()] 141 fun pr_sig_psl [] = [] 142 | pr_sig_psl l = 143 [NL, NL, 144 block CONSISTENT 0 145 (pr_list (block CONSISTENT 0 o pr_sig_ps) [NL, NL] l)] 146 147 fun pr_docs() = 148 if !include_docs then 149 (!pp_sig_hook(); 150 [block CONSISTENT 3 ( 151 [add_string "(*", NL] @ 152 pr_parents parents' @ 153 pr_thms "Axiom" axioms' @ 154 pr_thms "Definition" definitions' @ 155 pr_thms "Theorem" theorems' 156 ), NL, 157 add_string "*)", NL]) 158 else [] 159 fun pthms (heading, ths) = 160 vblock(heading, 161 (fn (s,th) => block CONSISTENT 0 162 (if is_temp_binding s then [] 163 else 164 [add_string("val "^ s ^ " : thm")])), 165 ths) 166in 167 block CONSISTENT 0 ( 168 [add_string ("signature "^ThrySig name^" ="), NL, 169 block CONSISTENT 2 [ 170 add_string "sig", NL, 171 block CONSISTENT 0 ( 172 [add_string"type thm = Thm.thm"] @ 173 (if null axioms' then [] 174 else [NL, NL, pthms ("Axioms",axioms')]) @ 175 (if null definitions' then [] 176 else [NL, NL, pthms("Definitions", definitions')]) @ 177 (if null theorems' then [] 178 else [NL, NL, pthms ("Theorems", theorems')]) @ 179 pr_sig_psl (filter (fn NONE => false | _ => true) sig_ps) 180 ) 181 ], NL 182 ] @ 183 pr_docs() @ 184 [add_string"end", NL] 185 ) 186end; 187 188(*--------------------------------------------------------------------------- 189 * Print a theory as a module. 190 *---------------------------------------------------------------------------*) 191 192val stringify = Lib.mlquote 193 194fun is_atom t = Term.is_var t orelse Term.is_const t 195fun strip_comb t = let 196 fun recurse acc t = let 197 val (f, x) = Term.dest_comb t 198 in 199 recurse (x::acc) f 200 end handle HOL_ERR _ => (t, List.rev acc) 201in 202 recurse [] t 203end 204 205infix >> 206open smpp 207 208fun mlower s m = 209 case m ((), []) of 210 NONE => raise Fail ("Couldn't print Theory" ^ s) 211 | SOME(_, (_, ps)) => PP.block PP.CONSISTENT 0 ps 212 213fun pp_struct (info_record : struct_info_record) = let 214 open Term Thm 215 val {theory as (name,i1,i2), parents=parents0, thydata, mldeps, axioms, 216 definitions,theorems,types,constants,struct_ps, 217 struct_pcps} = info_record 218 val parents1 = 219 List.mapPartial (fn (s,_,_) => if "min"=s then NONE else SOME (Thry s)) 220 parents0 221 val thml = axioms@definitions@theorems 222 val jump = add_newline >> add_newline 223 fun pblock(ob_pr, obs) = 224 case obs of 225 [] => nothing 226 | _ => 227 block CONSISTENT 0 228 ( 229 add_string "local open " >> 230 block INCONSISTENT 0 (pr_list ob_pr (add_break (1,0)) obs) >> 231 add_break(1,0) >> 232 add_string "in end;" 233 ) 234 235 fun pparent (s,i,j) = Thry s 236 237 fun pr_bind(s, th) = let 238 val (tg, asl, w) = (Thm.tag th, Thm.hyp th, Thm.concl th) 239 val addsbl = pr_list add_string (add_break(1,2)) 240 in 241 if is_temp_binding s then nothing 242 else 243 (* this rigmarole is necessary to allow ML bindings where the name is 244 a datatype constructor or an infix, or both *) 245 block CONSISTENT 0 246 (block INCONSISTENT 0 (addsbl ["fun","op",s,"_","=","()"]) >> 247 add_break(1,0) >> 248 block INCONSISTENT 0 (addsbl ["val","op",s,"=","TDB.find",mlquote s])) 249 end 250 251 val bind_theorems = 252 block CONSISTENT 0 ( 253 if null thml then nothing 254 else 255 block CONSISTENT 0 (pr_list pr_bind add_newline thml) >> 256 add_newline 257 ) 258 259 fun pr_ps NONE = nothing 260 | pr_ps (SOME pp) = block CONSISTENT 0 (lift pp ()) 261 262 fun pr_psl l = 263 block CONSISTENT 0 264 (pr_list pr_ps (add_newline >> add_newline) l) 265 fun pr_pcl l = 266 block CONSISTENT 0 ( 267 pr_list (fn pf => block CONSISTENT 0 (lift pf ())) 268 (add_newline >> add_newline) 269 l 270 ) 271 val datfile = 272 mlquote ( 273 holpathdb.reverse_lookup { 274 path = OS.Path.concat(OS.FileSys.getDir(), name ^ "Theory.dat") 275 } 276 ) 277 val m = 278 block CONSISTENT 0 ( 279 add_string (String.concatWith " " 280 ["structure",Thry name,":>", ThrySig name,"="]) >> 281 add_newline >> 282 block CONSISTENT 2 ( 283 add_string "struct" >> jump >> 284 block CONSISTENT 0 ( 285 block CONSISTENT 0 ( 286 add_string ("val _ = if !Globals.print_thy_loads") >> 287 add_break (1,2) >> 288 add_string 289 ("then TextIO.print \"Loading "^ Thry name ^ " ... \"") >> 290 add_break (1,2) >> 291 add_string "else ()") >> jump >> 292 add_string "open Type Term Thm" >> add_newline >> 293 pblock (add_string, 294 Listsort.sort String.compare parents1 @ mldeps) >> 295 add_newline >> add_newline >> 296 block CONSISTENT 0 ( 297 add_string "structure TDB = struct" >> add_break(1,2) >> 298 add_string "val thydata = " >> add_break(1,4) >> 299 block INCONSISTENT 0 ( 300 add_string "TheoryReader.load_thydata" >> add_break (1,2) >> 301 add_string (mlquote name) >> add_break (1,2) >> 302 add_string ("(holpathdb.subst_pathvars "^datfile^")") 303 ) >> add_break(1,2) >> 304 add_string ("fun find s = Redblackmap.find (thydata,s)") >> 305 add_break(1,0) >> add_string "end" 306 ) >> jump >> 307 bind_theorems >> 308 add_newline >> 309 pr_psl struct_ps 310 ) 311 ) >> add_break(0,0) >> 312 add_string "val _ = if !Globals.print_thy_loads then TextIO.print \ 313 \\"done\\n\" else ()" >> add_newline >> 314 add_string ("val _ = Theory.load_complete "^ stringify name) >> 315 jump >> 316 pr_pcl struct_pcps >> 317 add_string "end" >> add_newline) 318in 319 mlower ": struct" m 320end 321 322(*--------------------------------------------------------------------------- 323 * Print theory data separately. 324 *---------------------------------------------------------------------------*) 325 326 327fun pp_thydata (info_record : struct_info_record) = let 328 open Term Thm 329 val {theory as (name,i1,i2), parents=parents0, 330 thydata = (thydata_strings,thydata_tms, thydata), mldeps, 331 axioms,definitions,theorems,types,constants,...} = info_record 332 val parents1 = 333 List.mapPartial (fn (s,_,_) => if "min"=s then NONE else SOME (Thry s)) 334 parents0 335 val thml = axioms@definitions@theorems 336 open SharingTables 337 338 val share_data = build_sharing_data { 339 named_terms = [], named_types = [], unnamed_terms = [], 340 unnamed_types = [], theorems = thml 341 } 342 val share_data = add_strings thydata_strings share_data 343 val share_data = add_terms thydata_tms share_data 344 345 local open HOLsexp in 346 fun enc_thid(s,i,j) = 347 List[String s, String (Arbnum.toString i), String (Arbnum.toString j)] 348 val enc_thid_and_parents = 349 curry (pair_encode(enc_thid, list_encode enc_thid)) 350 end (* local *) 351 352 fun enc_incorporate_types types = 353 let open HOLsexp 354 in 355 tagged_encode "incorporate-types" 356 (list_encode (pair_encode(String,Integer))) types 357 end 358 359 fun enc_incorporate_constants constants = 360 let open HOLsexp 361 in 362 tagged_encode "incorporate-consts" 363 (list_encode 364 (pair_encode(String, Integer o write_type share_data))) 365 constants 366 end 367 368 val enc_dblist = 369 let 370 open HOLsexp 371 val enc_db = Integer o write_string share_data 372 val enc_dbl = list_encode enc_db 373 val check = 374 List.mapPartial (fn (nm, _) => if is_temp_binding nm then NONE 375 else SOME nm) 376 val axl = check axioms 377 val defl = check definitions 378 val thml = check theorems 379 in 380 tagged_encode "thm-classes" 381 (pair3_encode (enc_dbl, enc_dbl, enc_dbl)) (axl,defl,thml) 382 end 383 384 fun chunks w s = 385 if String.size s <= w then [s] 386 else String.substring(s, 0, w) :: chunks w (String.extract(s, w, NONE)) 387 388 val enc_cpl = HOLsexp.pair_encode(HOLsexp.String, fn x => x) 389 390 fun list_loadable shared_writers thydata_map = 391 Binarymap.foldl 392 (fn (k, data, rest) => (k, data shared_writers) :: rest) 393 [] 394 thydata_map 395 fun enc_loadable shared_writers thydata_map = 396 let open HOLsexp in 397 tagged_encode "loadable-thydata" (list_encode enc_cpl) 398 (list_loadable shared_writers thydata_map) 399 end 400 val thysexp = 401 let open HOLsexp 402 in 403 List [ 404 Symbol "theory", 405 enc_thid_and_parents theory parents0, 406 enc_sdata share_data, 407 tagged_encode "incorporate" ( 408 pair_encode(enc_incorporate_types, enc_incorporate_constants) 409 ) (types, constants), 410 enc_dblist, 411 enc_loadable {terms = write_term share_data, 412 strings = write_string share_data} 413 thydata 414 ] 415 end 416in 417 mlower ": dat" (lift HOLsexp.printer thysexp) 418end handle e as Interrupt => raise e 419 | e => raise ERR "pp_thydata" 420 ("Caught exception: " ^ General.exnMessage e) 421 422 423 424end; (* TheoryPP *) 425