(* Title: HOL/Import/hol4rews.ML ID: $Id: hol4rews.ML,v 1.14 2005/09/26 00:27:14 obua Exp $ Author: Sebastian Skalberg (TU Muenchen) *) structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord); type holthm = (term * term) list * thm datatype ImportStatus = NoImport | Generating of string | Replaying of string structure HOL4DefThyArgs: THEORY_DATA_ARGS = struct val name = "HOL4/import_status" type T = ImportStatus val empty = NoImport val copy = I val extend = I fun merge _ (NoImport,NoImport) = NoImport | merge _ _ = (warning "Import status set during merge"; NoImport) fun print sg import_status = Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname))) end; structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs); structure ImportSegmentArgs: THEORY_DATA_ARGS = struct val name = "HOL4/import_segment" type T = string val empty = "" val copy = I val extend = I fun merge _ ("",arg) = arg | merge _ (arg,"") = arg | merge _ (s1,s2) = if s1 = s2 then s1 else error "Trying to merge two different import segments" fun print sg import_segment = Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment)) end; structure ImportSegment = TheoryDataFun(ImportSegmentArgs); val get_import_segment = ImportSegment.get val set_import_segment = ImportSegment.put structure HOL4UNamesArgs: THEORY_DATA_ARGS = struct val name = "HOL4/used_names" type T = string list val empty = [] val copy = I val extend = I fun merge _ ([],[]) = [] | merge _ _ = error "Used names not empty during merge" fun print sg used_names = Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented") end; structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs); structure HOL4DumpArgs: THEORY_DATA_ARGS = struct val name = "HOL4/dump_data" type T = string * string * string list val empty = ("","",[]) val copy = I val extend = I fun merge _ (("","",[]),("","",[])) = ("","",[]) | merge _ _ = error "Dump data not empty during merge" fun print sg dump_data = Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented") end; structure HOL4Dump = TheoryDataFun(HOL4DumpArgs); structure HOL4MovesArgs: THEORY_DATA_ARGS = struct val name = "HOL4/moves" type T = string Symtab.table val empty = Symtab.empty val copy = I val extend = I fun merge _ : T * T -> T = Symtab.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 moves:" (Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab))) end; structure HOL4Moves = TheoryDataFun(HOL4MovesArgs); structure HOL4ImportsArgs: THEORY_DATA_ARGS = struct val name = "HOL4/imports" type T = string Symtab.table val empty = Symtab.empty val copy = I val extend = I fun merge _ : T * T -> T = Symtab.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 imports:" (Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab))) end; structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs); fun get_segment2 thyname thy = Symtab.lookup (HOL4Imports.get thy) thyname fun set_segment thyname segname thy = let val imps = HOL4Imports.get thy val imps' = Symtab.update_new (thyname,segname) imps in HOL4Imports.put imps' thy end structure HOL4CMovesArgs: THEORY_DATA_ARGS = struct val name = "HOL4/constant_moves" type T = string Symtab.table val empty = Symtab.empty val copy = I val extend = I fun merge _ : T * T -> T = Symtab.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant moves:" (Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab))) end; structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs); structure HOL4MapsArgs: THEORY_DATA_ARGS = struct val name = "HOL4/mappings" type T = (string option) StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 mappings:" (StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab))) end; structure HOL4Maps = TheoryDataFun(HOL4MapsArgs); structure HOL4ThmsArgs: THEORY_DATA_ARGS = struct val name = "HOL4/theorems" type T = holthm StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 mappings:" (StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab))) end; structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs); structure HOL4ConstMapsArgs: THEORY_DATA_ARGS = struct val name = "HOL4/constmappings" type T = (bool * string * typ option) StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant mappings:" (StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab))) end; structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs); structure HOL4RenameArgs: THEORY_DATA_ARGS = struct val name = "HOL4/renamings" type T = string StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant renamings:" (StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab))) end; structure HOL4Rename = TheoryDataFun(HOL4RenameArgs); structure HOL4DefMapsArgs: THEORY_DATA_ARGS = struct val name = "HOL4/def_maps" type T = string StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant definitions:" (StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab))) end; structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs); structure HOL4TypeMapsArgs: THEORY_DATA_ARGS = struct val name = "HOL4/typemappings" type T = (bool * string) StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 type mappings:" (StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab))) end; structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs); structure HOL4PendingArgs: THEORY_DATA_ARGS = struct val name = "HOL4/pending" type T = ((term * term) list * thm) StringPair.table val empty = StringPair.empty val copy = I val extend = I fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 pending theorems:" (StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab))) end; structure HOL4Pending = TheoryDataFun(HOL4PendingArgs); structure HOL4RewritesArgs: THEORY_DATA_ARGS = struct val name = "HOL4/rewrites" type T = thm list val empty = [] val copy = I val extend = I fun merge _ = Library.gen_union Thm.eq_thm fun print sg thms = Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:" (map Display.pretty_thm thms)) end; structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs); val hol4_debug = ref false fun message s = if !hol4_debug then writeln s else () fun add_hol4_rewrite (thy,th) = let val _ = message "Adding HOL4 rewrite" val th1 = th RS eq_reflection val current_rews = HOL4Rewrites.get thy val new_rews = gen_ins Thm.eq_thm (th1,current_rews) val updated_thy = HOL4Rewrites.put new_rews thy in (updated_thy,th1) end; fun ignore_hol4 bthy bthm thy = let val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) val curmaps = HOL4Maps.get thy val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps val upd_thy = HOL4Maps.put newmaps thy in upd_thy end val opt_get_output_thy = #2 o HOL4Dump.get fun get_output_thy thy = case #2 (HOL4Dump.get thy) of "" => error "No theory file being output" | thyname => thyname val get_output_dir = #1 o HOL4Dump.get fun add_hol4_move bef aft thy = let val curmoves = HOL4Moves.get thy val newmoves = Symtab.update_new (bef, aft) curmoves in HOL4Moves.put newmoves thy end fun get_hol4_move bef thy = Symtab.lookup (HOL4Moves.get thy) bef fun follow_name thmname thy = let val moves = HOL4Moves.get thy fun F thmname = case Symtab.lookup moves thmname of SOME name => F name | NONE => thmname in F thmname end fun add_hol4_cmove bef aft thy = let val curmoves = HOL4CMoves.get thy val newmoves = Symtab.update_new (bef, aft) curmoves in HOL4CMoves.put newmoves thy end fun get_hol4_cmove bef thy = Symtab.lookup (HOL4CMoves.get thy) bef fun follow_cname thmname thy = let val moves = HOL4CMoves.get thy fun F thmname = case Symtab.lookup moves thmname of SOME name => F name | NONE => thmname in F thmname end fun add_hol4_mapping bthy bthm isathm thy = let (* val _ = writeln ("Before follow_name: "^isathm) *) val isathm = follow_name isathm thy (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*) val curmaps = HOL4Maps.get thy val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps val upd_thy = HOL4Maps.put newmaps thy in upd_thy end; fun get_hol4_type_mapping bthy tycon thy = let val maps = HOL4TypeMaps.get thy in StringPair.lookup maps (bthy,tycon) end fun get_hol4_mapping bthy bthm thy = let val curmaps = HOL4Maps.get thy in StringPair.lookup curmaps (bthy,bthm) end; fun add_hol4_const_mapping bthy bconst internal isaconst thy = let val thy = case opt_get_output_thy thy of "" => thy | output_thy => if internal then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy else thy val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) val curmaps = HOL4ConstMaps.get thy val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps val upd_thy = HOL4ConstMaps.put newmaps thy in upd_thy end; fun add_hol4_const_renaming bthy bconst newname thy = let val currens = HOL4Rename.get thy val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname) val newrens = StringPair.update_new ((bthy,bconst),newname) currens val upd_thy = HOL4Rename.put newrens thy in upd_thy end; fun get_hol4_const_renaming bthy bconst thy = let val currens = HOL4Rename.get thy in StringPair.lookup currens (bthy,bconst) end; fun get_hol4_const_mapping bthy bconst thy = let val bconst = case get_hol4_const_renaming bthy bconst thy of SOME name => name | NONE => bconst val maps = HOL4ConstMaps.get thy in StringPair.lookup maps (bthy,bconst) end fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy = let val thy = case opt_get_output_thy thy of "" => thy | output_thy => if internal then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy else thy val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) val curmaps = HOL4ConstMaps.get thy val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps val upd_thy = HOL4ConstMaps.put newmaps thy in upd_thy end; fun add_hol4_type_mapping bthy bconst internal isaconst thy = let val curmaps = HOL4TypeMaps.get thy val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end val upd_thy = HOL4TypeMaps.put newmaps thy in upd_thy end; fun add_hol4_pending bthy bthm hth thy = let val thmname = Sign.full_name (sign_of thy) bthm val _ = message ("Add pending " ^ bthy ^ "." ^ bthm) val curpend = HOL4Pending.get thy val newpend = StringPair.update_new ((bthy,bthm),hth) curpend val upd_thy = HOL4Pending.put newpend thy val thy' = case opt_get_output_thy upd_thy of "" => add_hol4_mapping bthy bthm thmname upd_thy | output_thy => let val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm in upd_thy |> add_hol4_move thmname new_thmname |> add_hol4_mapping bthy bthm new_thmname end in thy' end; fun get_hol4_theorem thyname thmname thy = let val isathms = HOL4Thms.get thy in StringPair.lookup isathms (thyname,thmname) end fun add_hol4_theorem thyname thmname hth thy = let val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname) val isathms = HOL4Thms.get thy val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms val thy' = HOL4Thms.put isathms' thy in thy' end fun export_hol4_pending thy = let val rews = HOL4Rewrites.get thy val outthy = get_output_thy thy fun process (thy,((bthy,bthm),hth as (_,thm))) = let val sg = sign_of thy val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm) val thm2 = standard thm1 val (thy2,_) = PureThy.store_thm((bthm,thm2),[]) thy val thy5 = add_hol4_theorem bthy bthm hth thy2 in thy5 end val pending = HOL4Pending.get thy val thy1 = StringPair.foldl process (thy,pending) val thy2 = HOL4Pending.put (StringPair.empty) thy1 in thy2 end; fun setup_dump (dir,thyname) thy = HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy fun add_dump str thy = let val (dir,thyname,curdump) = HOL4Dump.get thy in HOL4Dump.put (dir,thyname,str::curdump) thy end fun flush_dump thy = let val (dir,thyname,dumpdata) = HOL4Dump.get thy val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir, file=thyname ^ ".thy"}) val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata) val _ = TextIO.closeOut os in HOL4Dump.put ("","",[]) thy end fun set_generating_thy thyname thy = case HOL4DefThy.get thy of NoImport => HOL4DefThy.put (Generating thyname) thy | _ => error "Import already in progess" fun set_replaying_thy thyname thy = case HOL4DefThy.get thy of NoImport => HOL4DefThy.put (Replaying thyname) thy | _ => error "Import already in progess" fun clear_import_thy thy = case HOL4DefThy.get thy of NoImport => error "No import in progress" | _ => HOL4DefThy.put NoImport thy fun get_generating_thy thy = case HOL4DefThy.get thy of Generating thyname => thyname | _ => error "No theory being generated" fun get_replaying_thy thy = case HOL4DefThy.get thy of Replaying thyname => thyname | _ => error "No theory being replayed" fun get_import_thy thy = case HOL4DefThy.get thy of Replaying thyname => thyname | Generating thyname => thyname | _ => error "No theory being imported" fun should_ignore thyname thy thmname = case get_hol4_mapping thyname thmname thy of SOME NONE => true | _ => false val trans_string = let fun quote s = "\"" ^ s ^ "\"" fun F [] = [] | F (#"\\" :: cs) = patch #"\\" cs | F (#"\"" :: cs) = patch #"\"" cs | F (c :: cs) = c :: F cs and patch c rest = #"\\" :: c :: F rest in quote o String.implode o F o String.explode end fun dump_import_thy thyname thy = let val output_dir = get_output_dir thy val output_thy = get_output_thy thy val input_thy = Context.theory_name thy val import_segment = get_import_segment thy val sg = sign_of thy val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir, file=thyname ^ ".imp"}) fun out s = TextIO.output(os,s) val (ignored,mapped) = StringPair.foldl (fn ((ign,map),((bthy,bthm),v)) => if bthy = thyname then (case v of NONE => (bthm::ign,map) | SOME w => (ign,(bthm,w)::map)) else (ign,map)) (([],[]),HOL4Maps.get thy) val constmaps = StringPair.foldl (fn (map,((bthy,bthm),v)) => if bthy = thyname then (bthm,v)::map else map) ([],HOL4ConstMaps.get thy) val constrenames = StringPair.foldl (fn (map,((bthy,bthm),v)) => if bthy = thyname then (bthm,v)::map else map) ([],HOL4Rename.get thy) val typemaps = StringPair.foldl (fn (map,((bthy,bthm),v)) => if bthy = thyname then (bthm,v)::map else map) ([],HOL4TypeMaps.get thy) val defmaps = StringPair.foldl (fn (map,((bthy,bthm),v)) => if bthy = thyname then (bthm,v)::map else map) ([],HOL4DefMaps.get thy) fun new_name internal isa = if internal then let val paths = NameSpace.unpack isa val i = Library.drop(length paths - 2,paths) in case i of [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con | _ => error "hol4rews.dump internal error" end else isa val _ = out "import\n\n" val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n") val _ = if null defmaps then () else out "def_maps" val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps val _ = if null defmaps then () else out "\n\n" val _ = if null typemaps then () else out "type_maps" val _ = app (fn (hol,(internal,isa)) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps val _ = if null typemaps then () else out "\n\n" val _ = if null constmaps then () else out "const_maps" val _ = app (fn (hol,(internal,isa,opt_ty)) => (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); case opt_ty of SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"") | NONE => ())) constmaps val _ = if null constmaps then () else out "\n\n" val _ = if null constrenames then () else out "const_renames" val _ = app (fn (old,new) => out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames val _ = if null constrenames then () else out "\n\n" fun gen2replay in_thy out_thy s = let val ss = NameSpace.unpack s in if (hd ss = in_thy) then NameSpace.pack (out_thy::(tl ss)) else s end val _ = if null mapped then () else out "thm_maps" val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped val _ = if null mapped then () else out "\n\n" val _ = if null ignored then () else out "ignore_thms" val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored val _ = if null ignored then () else out "\n\n" val _ = out "end\n" val _ = TextIO.closeOut os in thy end fun set_used_names names thy = let val unames = HOL4UNames.get thy in case unames of [] => HOL4UNames.put names thy | _ => error "hol4rews.set_used_names called on initialized data!" end val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty fun get_defmap thyname const thy = let val maps = HOL4DefMaps.get thy in StringPair.lookup maps (thyname,const) end fun add_defmap thyname const defname thy = let val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname) val maps = HOL4DefMaps.get thy val maps' = StringPair.update_new ((thyname,const),defname) maps val thy' = HOL4DefMaps.put maps' thy in thy' end fun get_defname thyname name thy = let val maps = HOL4DefMaps.get thy fun F dname = (dname,add_defmap thyname name dname thy) in case StringPair.lookup maps (thyname,name) of SOME thmname => (thmname,thy) | NONE => let val used = HOL4UNames.get thy val defname = def_name name val pdefname = name ^ "_primdef" in if not (defname mem used) then F defname (* name_def *) else if not (pdefname mem used) then F pdefname (* name_primdef *) else F (variant used pdefname) (* last resort *) end end local fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x | handle_meta [x] = Appl[Constant "Trueprop",x] | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" in val smarter_trueprop_parsing = [("Trueprop",handle_meta)] end local fun initial_maps thy = thy |> add_hol4_type_mapping "min" "bool" false "bool" |> add_hol4_type_mapping "min" "fun" false "fun" |> add_hol4_type_mapping "min" "ind" false "Nat.ind" |> add_hol4_const_mapping "min" "=" false "op =" |> add_hol4_const_mapping "min" "==>" false "op -->" |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps" in val hol4_setup = [HOL4Rewrites.init, HOL4Maps.init, HOL4UNames.init, HOL4DefMaps.init, HOL4Moves.init, HOL4CMoves.init, HOL4ConstMaps.init, HOL4Rename.init, HOL4TypeMaps.init, HOL4Pending.init, HOL4Thms.init, HOL4Dump.init, HOL4DefThy.init, HOL4Imports.init, ImportSegment.init, initial_maps, Attrib.add_attributes [("hol4rew", (Attrib.no_args add_hol4_rewrite, Attrib.no_args Attrib.undef_local_attribute), "HOL4 rewrite rule")]] end