1 (* Title: HOL/Import/hol4rews.ML
2 Author: Sebastian Skalberg (TU Muenchen)
5 structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord);
7 type holthm = (term * term) list * thm
9 datatype ImportStatus =
11 | Generating of string
14 structure HOL4DefThy = TheoryDataFun
20 fun merge _ (NoImport,NoImport) = NoImport
21 | merge _ _ = (warning "Import status set during merge"; NoImport)
24 structure ImportSegment = TheoryDataFun
30 fun merge _ ("",arg) = arg
31 | merge _ (arg,"") = arg
35 else error "Trying to merge two different import segments"
38 val get_import_segment = ImportSegment.get
39 val set_import_segment = ImportSegment.put
41 structure HOL4UNames = TheoryDataFun
47 fun merge _ ([],[]) = []
48 | merge _ _ = error "Used names not empty during merge"
51 structure HOL4Dump = TheoryDataFun
53 type T = string * string * string list
54 val empty = ("","",[])
57 fun merge _ (("","",[]),("","",[])) = ("","",[])
58 | merge _ _ = error "Dump data not empty during merge"
61 structure HOL4Moves = TheoryDataFun
63 type T = string Symtab.table
64 val empty = Symtab.empty
67 fun merge _ : T * T -> T = Symtab.merge (K true)
70 structure HOL4Imports = TheoryDataFun
72 type T = string Symtab.table
73 val empty = Symtab.empty
76 fun merge _ : T * T -> T = Symtab.merge (K true)
79 fun get_segment2 thyname thy =
80 Symtab.lookup (HOL4Imports.get thy) thyname
82 fun set_segment thyname segname thy =
84 val imps = HOL4Imports.get thy
85 val imps' = Symtab.update_new (thyname,segname) imps
87 HOL4Imports.put imps' thy
90 structure HOL4CMoves = TheoryDataFun
92 type T = string Symtab.table
93 val empty = Symtab.empty
96 fun merge _ : T * T -> T = Symtab.merge (K true)
99 structure HOL4Maps = TheoryDataFun
101 type T = (string option) StringPair.table
102 val empty = StringPair.empty
105 fun merge _ : T * T -> T = StringPair.merge (K true)
108 structure HOL4Thms = TheoryDataFun
110 type T = holthm StringPair.table
111 val empty = StringPair.empty
114 fun merge _ : T * T -> T = StringPair.merge (K true)
117 structure HOL4ConstMaps = TheoryDataFun
119 type T = (bool * string * typ option) StringPair.table
120 val empty = StringPair.empty
123 fun merge _ : T * T -> T = StringPair.merge (K true)
126 structure HOL4Rename = TheoryDataFun
128 type T = string StringPair.table
129 val empty = StringPair.empty
132 fun merge _ : T * T -> T = StringPair.merge (K true)
135 structure HOL4DefMaps = TheoryDataFun
137 type T = string StringPair.table
138 val empty = StringPair.empty
141 fun merge _ : T * T -> T = StringPair.merge (K true)
144 structure HOL4TypeMaps = TheoryDataFun
146 type T = (bool * string) StringPair.table
147 val empty = StringPair.empty
150 fun merge _ : T * T -> T = StringPair.merge (K true)
153 structure HOL4Pending = TheoryDataFun
155 type T = ((term * term) list * thm) StringPair.table
156 val empty = StringPair.empty
159 fun merge _ : T * T -> T = StringPair.merge (K true)
162 structure HOL4Rewrites = TheoryDataFun
168 fun merge _ = Library.gen_union Thm.eq_thm
171 val hol4_debug = Unsynchronized.ref false
172 fun message s = if !hol4_debug then writeln s else ()
175 val eq_reflection = thm "eq_reflection"
177 fun add_hol4_rewrite (Context.Theory thy, th) =
179 val _ = message "Adding HOL4 rewrite"
180 val th1 = th RS eq_reflection
181 val current_rews = HOL4Rewrites.get thy
182 val new_rews = insert Thm.eq_thm th1 current_rews
183 val updated_thy = HOL4Rewrites.put new_rews thy
185 (Context.Theory updated_thy,th1)
187 | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
190 fun ignore_hol4 bthy bthm thy =
192 val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
193 val curmaps = HOL4Maps.get thy
194 val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
195 val upd_thy = HOL4Maps.put newmaps thy
200 val opt_get_output_thy = #2 o HOL4Dump.get
202 fun get_output_thy thy =
203 case #2 (HOL4Dump.get thy) of
204 "" => error "No theory file being output"
207 val get_output_dir = #1 o HOL4Dump.get
209 fun add_hol4_move bef aft thy =
211 val curmoves = HOL4Moves.get thy
212 val newmoves = Symtab.update_new (bef, aft) curmoves
214 HOL4Moves.put newmoves thy
217 fun get_hol4_move bef thy =
218 Symtab.lookup (HOL4Moves.get thy) bef
220 fun follow_name thmname thy =
222 val moves = HOL4Moves.get thy
224 case Symtab.lookup moves thmname of
231 fun add_hol4_cmove bef aft thy =
233 val curmoves = HOL4CMoves.get thy
234 val newmoves = Symtab.update_new (bef, aft) curmoves
236 HOL4CMoves.put newmoves thy
239 fun get_hol4_cmove bef thy =
240 Symtab.lookup (HOL4CMoves.get thy) bef
242 fun follow_cname thmname thy =
244 val moves = HOL4CMoves.get thy
246 case Symtab.lookup moves thmname of
253 fun add_hol4_mapping bthy bthm isathm thy =
255 (* val _ = writeln ("Before follow_name: "^isathm) *)
256 val isathm = follow_name isathm thy
257 (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
258 val curmaps = HOL4Maps.get thy
259 val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
260 val upd_thy = HOL4Maps.put newmaps thy
265 fun get_hol4_type_mapping bthy tycon thy =
267 val maps = HOL4TypeMaps.get thy
269 StringPair.lookup maps (bthy,tycon)
272 fun get_hol4_mapping bthy bthm thy =
274 val curmaps = HOL4Maps.get thy
276 StringPair.lookup curmaps (bthy,bthm)
279 fun add_hol4_const_mapping bthy bconst internal isaconst thy =
281 val thy = case opt_get_output_thy thy of
283 | output_thy => if internal
284 then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
286 val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
287 val curmaps = HOL4ConstMaps.get thy
288 val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
289 val upd_thy = HOL4ConstMaps.put newmaps thy
294 fun add_hol4_const_renaming bthy bconst newname thy =
296 val currens = HOL4Rename.get thy
297 val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
298 val newrens = StringPair.update_new ((bthy,bconst),newname) currens
299 val upd_thy = HOL4Rename.put newrens thy
304 fun get_hol4_const_renaming bthy bconst thy =
306 val currens = HOL4Rename.get thy
308 StringPair.lookup currens (bthy,bconst)
311 fun get_hol4_const_mapping bthy bconst thy =
313 val bconst = case get_hol4_const_renaming bthy bconst thy of
316 val maps = HOL4ConstMaps.get thy
318 StringPair.lookup maps (bthy,bconst)
321 fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
323 val thy = case opt_get_output_thy thy of
325 | output_thy => if internal
326 then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
328 val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
329 val curmaps = HOL4ConstMaps.get thy
330 val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
331 val upd_thy = HOL4ConstMaps.put newmaps thy
336 fun add_hol4_type_mapping bthy bconst internal isaconst thy =
338 val curmaps = HOL4TypeMaps.get thy
339 val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
340 val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
341 handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
342 warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
343 val upd_thy = HOL4TypeMaps.put newmaps thy
348 fun add_hol4_pending bthy bthm hth thy =
350 val thmname = Sign.full_bname thy bthm
351 val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
352 val curpend = HOL4Pending.get thy
353 val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
354 val upd_thy = HOL4Pending.put newpend thy
355 val thy' = case opt_get_output_thy upd_thy of
356 "" => add_hol4_mapping bthy bthm thmname upd_thy
359 val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
361 upd_thy |> add_hol4_move thmname new_thmname
362 |> add_hol4_mapping bthy bthm new_thmname
368 fun get_hol4_theorem thyname thmname thy =
370 val isathms = HOL4Thms.get thy
372 StringPair.lookup isathms (thyname,thmname)
375 fun add_hol4_theorem thyname thmname hth =
377 val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
379 HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
382 fun export_hol4_pending thy =
384 val rews = HOL4Rewrites.get thy;
385 val pending = HOL4Pending.get thy;
386 fun process ((bthy,bthm), hth as (_,thm)) thy =
388 val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
389 val thm2 = standard thm1;
392 |> PureThy.store_thm (Binding.name bthm, thm2)
394 |> add_hol4_theorem bthy bthm hth
398 |> StringPair.fold process pending
399 |> HOL4Pending.put StringPair.empty
402 fun setup_dump (dir,thyname) thy =
403 HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
405 fun add_dump str thy =
407 val (dir,thyname,curdump) = HOL4Dump.get thy
409 HOL4Dump.put (dir,thyname,str::curdump) thy
414 val (dir,thyname,dumpdata) = HOL4Dump.get thy
415 val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
416 file=thyname ^ ".thy"})
417 val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
418 val _ = TextIO.closeOut os
420 HOL4Dump.put ("","",[]) thy
423 fun set_generating_thy thyname thy =
424 case HOL4DefThy.get thy of
425 NoImport => HOL4DefThy.put (Generating thyname) thy
426 | _ => error "Import already in progess"
428 fun set_replaying_thy thyname thy =
429 case HOL4DefThy.get thy of
430 NoImport => HOL4DefThy.put (Replaying thyname) thy
431 | _ => error "Import already in progess"
433 fun clear_import_thy thy =
434 case HOL4DefThy.get thy of
435 NoImport => error "No import in progress"
436 | _ => HOL4DefThy.put NoImport thy
438 fun get_generating_thy thy =
439 case HOL4DefThy.get thy of
440 Generating thyname => thyname
441 | _ => error "No theory being generated"
443 fun get_replaying_thy thy =
444 case HOL4DefThy.get thy of
445 Replaying thyname => thyname
446 | _ => error "No theory being replayed"
448 fun get_import_thy thy =
449 case HOL4DefThy.get thy of
450 Replaying thyname => thyname
451 | Generating thyname => thyname
452 | _ => error "No theory being imported"
454 fun should_ignore thyname thy thmname =
455 case get_hol4_mapping thyname thmname thy of
461 fun quote s = "\"" ^ s ^ "\""
463 | F (#"\\" :: cs) = patch #"\\" cs
464 | F (#"\"" :: cs) = patch #"\"" cs
465 | F (c :: cs) = c :: F cs
466 and patch c rest = #"\\" :: c :: F rest
468 quote o String.implode o F o String.explode
471 fun dump_import_thy thyname thy =
473 val output_dir = get_output_dir thy
474 val output_thy = get_output_thy thy
475 val input_thy = Context.theory_name thy
476 val import_segment = get_import_segment thy
477 val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
478 file=thyname ^ ".imp"})
479 fun out s = TextIO.output(os,s)
480 val (ignored, mapped) = StringPair.fold
481 (fn ((bthy, bthm), v) => fn (ign, map) =>
484 of NONE => (bthm :: ign, map)
485 | SOME w => (ign, (bthm, w) :: map)
486 else (ign, map)) (HOL4Maps.get thy) ([],[]);
487 fun mk init = StringPair.fold
488 (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
489 val constmaps = mk (HOL4ConstMaps.get thy);
490 val constrenames = mk (HOL4Rename.get thy);
491 val typemaps = mk (HOL4TypeMaps.get thy);
492 val defmaps = mk (HOL4DefMaps.get thy);
493 fun new_name internal isa =
497 val paths = Long_Name.explode isa
498 val i = Library.drop(length paths - 2,paths)
501 [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
502 | _ => error "hol4rews.dump internal error"
507 val _ = out "import\n\n"
509 val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
510 val _ = if null defmaps
513 val _ = app (fn (hol,isa) =>
514 out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
515 val _ = if null defmaps
519 val _ = if null typemaps
522 val _ = app (fn (hol,(internal,isa)) =>
523 out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
524 val _ = if null typemaps
528 val _ = if null constmaps
530 else out "const_maps"
531 val _ = app (fn (hol,(internal,isa,opt_ty)) =>
532 (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
534 SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
535 | NONE => ())) constmaps
536 val _ = if null constmaps
540 val _ = if null constrenames
542 else out "const_renames"
543 val _ = app (fn (old,new) =>
544 out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
545 val _ = if null constrenames
549 fun gen2replay in_thy out_thy s =
551 val ss = Long_Name.explode s
553 if (hd ss = in_thy) then
554 Long_Name.implode (out_thy::(tl ss))
559 val _ = if null mapped
562 val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
563 val _ = if null mapped
567 val _ = if null ignored
569 else out "ignore_thms"
570 val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored
571 val _ = if null ignored
576 val _ = TextIO.closeOut os
581 fun set_used_names names thy =
583 val unames = HOL4UNames.get thy
586 [] => HOL4UNames.put names thy
587 | _ => error "hol4rews.set_used_names called on initialized data!"
590 val clear_used_names = HOL4UNames.put [];
592 fun get_defmap thyname const thy =
594 val maps = HOL4DefMaps.get thy
596 StringPair.lookup maps (thyname,const)
599 fun add_defmap thyname const defname thy =
601 val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
602 val maps = HOL4DefMaps.get thy
603 val maps' = StringPair.update_new ((thyname,const),defname) maps
604 val thy' = HOL4DefMaps.put maps' thy
609 fun get_defname thyname name thy =
611 val maps = HOL4DefMaps.get thy
612 fun F dname = (dname,add_defmap thyname name dname thy)
614 case StringPair.lookup maps (thyname,name) of
615 SOME thmname => (thmname,thy)
618 val used = HOL4UNames.get thy
619 val defname = Thm.def_name name
620 val pdefname = name ^ "_primdef"
622 if not (defname mem used)
623 then F defname (* name_def *)
624 else if not (pdefname mem used)
625 then F pdefname (* name_primdef *)
626 else F (Name.variant used pdefname) (* last resort *)
631 fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
632 | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
633 | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
634 | handle_meta [x] = Appl[Constant "Trueprop",x]
635 | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
637 val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
641 fun initial_maps thy =
642 thy |> add_hol4_type_mapping "min" "bool" false "bool"
643 |> add_hol4_type_mapping "min" "fun" false "fun"
644 |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
645 |> add_hol4_const_mapping "min" "=" false "op ="
646 |> add_hol4_const_mapping "min" "==>" false "op -->"
647 |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
651 Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"