src/HOL/Import/hol4rews.ML
author haftmann
Tue Nov 24 17:28:25 2009 +0100 (2009-11-24)
changeset 33955 fff6f11b1f09
parent 33522 737589bb9bb8
child 35021 c839a4c670c6
permissions -rw-r--r--
curried take/drop
     1 (*  Title:      HOL/Import/hol4rews.ML
     2     Author:     Sebastian Skalberg (TU Muenchen)
     3 *)
     4 
     5 structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord);
     6 
     7 type holthm = (term * term) list * thm
     8 
     9 datatype ImportStatus =
    10          NoImport
    11        | Generating of string
    12        | Replaying of string
    13 
    14 structure HOL4DefThy = Theory_Data
    15 (
    16   type T = ImportStatus
    17   val empty = NoImport
    18   val extend = I
    19   fun merge (NoImport, NoImport) = NoImport
    20     | merge _ = (warning "Import status set during merge"; NoImport)
    21 )
    22 
    23 structure ImportSegment = Theory_Data
    24 (
    25   type T = string
    26   val empty = ""
    27   val extend = I
    28   fun merge ("",arg) = arg
    29     | merge (arg,"") = arg
    30     | merge (s1,s2) =
    31       if s1 = s2
    32       then s1
    33       else error "Trying to merge two different import segments"
    34 )
    35 
    36 val get_import_segment = ImportSegment.get
    37 val set_import_segment = ImportSegment.put
    38 
    39 structure HOL4UNames = Theory_Data
    40 (
    41   type T = string list
    42   val empty = []
    43   val extend = I
    44   fun merge ([], []) = []
    45     | merge _ = error "Used names not empty during merge"
    46 )
    47 
    48 structure HOL4Dump = Theory_Data
    49 (
    50   type T = string * string * string list
    51   val empty = ("","",[])
    52   val extend = I
    53   fun merge (("","",[]),("","",[])) = ("","",[])
    54     | merge _ = error "Dump data not empty during merge"
    55 )
    56 
    57 structure HOL4Moves = Theory_Data
    58 (
    59   type T = string Symtab.table
    60   val empty = Symtab.empty
    61   val extend = I
    62   fun merge data = Symtab.merge (K true) data
    63 )
    64 
    65 structure HOL4Imports = Theory_Data
    66 (
    67   type T = string Symtab.table
    68   val empty = Symtab.empty
    69   val extend = I
    70   fun merge data = Symtab.merge (K true) data
    71 )
    72 
    73 fun get_segment2 thyname thy =
    74   Symtab.lookup (HOL4Imports.get thy) thyname
    75 
    76 fun set_segment thyname segname thy =
    77     let
    78         val imps = HOL4Imports.get thy
    79         val imps' = Symtab.update_new (thyname,segname) imps
    80     in
    81         HOL4Imports.put imps' thy
    82     end
    83 
    84 structure HOL4CMoves = Theory_Data
    85 (
    86   type T = string Symtab.table
    87   val empty = Symtab.empty
    88   val extend = I
    89   fun merge data = Symtab.merge (K true) data
    90 )
    91 
    92 structure HOL4Maps = Theory_Data
    93 (
    94   type T = string option StringPair.table
    95   val empty = StringPair.empty
    96   val extend = I
    97   fun merge data = StringPair.merge (K true) data
    98 )
    99 
   100 structure HOL4Thms = Theory_Data
   101 (
   102   type T = holthm StringPair.table
   103   val empty = StringPair.empty
   104   val extend = I
   105   fun merge data = StringPair.merge (K true) data
   106 )
   107 
   108 structure HOL4ConstMaps = Theory_Data
   109 (
   110   type T = (bool * string * typ option) StringPair.table
   111   val empty = StringPair.empty
   112   val extend = I
   113   fun merge data = StringPair.merge (K true) data
   114 )
   115 
   116 structure HOL4Rename = Theory_Data
   117 (
   118   type T = string StringPair.table
   119   val empty = StringPair.empty
   120   val extend = I
   121   fun merge data = StringPair.merge (K true) data
   122 )
   123 
   124 structure HOL4DefMaps = Theory_Data
   125 (
   126   type T = string StringPair.table
   127   val empty = StringPair.empty
   128   val extend = I
   129   fun merge data = StringPair.merge (K true) data
   130 )
   131 
   132 structure HOL4TypeMaps = Theory_Data
   133 (
   134   type T = (bool * string) StringPair.table
   135   val empty = StringPair.empty
   136   val extend = I
   137   fun merge data = StringPair.merge (K true) data
   138 )
   139 
   140 structure HOL4Pending = Theory_Data
   141 (
   142   type T = ((term * term) list * thm) StringPair.table
   143   val empty = StringPair.empty
   144   val extend = I
   145   fun merge data = StringPair.merge (K true) data
   146 )
   147 
   148 structure HOL4Rewrites = Theory_Data
   149 (
   150   type T = thm list
   151   val empty = []
   152   val extend = I
   153   val merge = Thm.merge_thms
   154 )
   155 
   156 val hol4_debug = Unsynchronized.ref false
   157 fun message s = if !hol4_debug then writeln s else ()
   158 
   159 local
   160   val eq_reflection = thm "eq_reflection"
   161 in
   162 fun add_hol4_rewrite (Context.Theory thy, th) =
   163     let
   164         val _ = message "Adding HOL4 rewrite"
   165         val th1 = th RS eq_reflection
   166         val current_rews = HOL4Rewrites.get thy
   167         val new_rews = insert Thm.eq_thm th1 current_rews
   168         val updated_thy  = HOL4Rewrites.put new_rews thy
   169     in
   170         (Context.Theory updated_thy,th1)
   171     end
   172   | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
   173 end
   174 
   175 fun ignore_hol4 bthy bthm thy =
   176     let
   177         val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
   178         val curmaps = HOL4Maps.get thy
   179         val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
   180         val upd_thy = HOL4Maps.put newmaps thy
   181     in
   182         upd_thy
   183     end
   184 
   185 val opt_get_output_thy = #2 o HOL4Dump.get
   186 
   187 fun get_output_thy thy =
   188     case #2 (HOL4Dump.get thy) of
   189         "" => error "No theory file being output"
   190       | thyname => thyname
   191 
   192 val get_output_dir = #1 o HOL4Dump.get
   193 
   194 fun add_hol4_move bef aft thy =
   195     let
   196         val curmoves = HOL4Moves.get thy
   197         val newmoves = Symtab.update_new (bef, aft) curmoves
   198     in
   199         HOL4Moves.put newmoves thy
   200     end
   201 
   202 fun get_hol4_move bef thy =
   203   Symtab.lookup (HOL4Moves.get thy) bef
   204 
   205 fun follow_name thmname thy =
   206     let
   207         val moves = HOL4Moves.get thy
   208         fun F thmname =
   209             case Symtab.lookup moves thmname of
   210                 SOME name => F name
   211               | NONE => thmname
   212     in
   213         F thmname
   214     end
   215 
   216 fun add_hol4_cmove bef aft thy =
   217     let
   218         val curmoves = HOL4CMoves.get thy
   219         val newmoves = Symtab.update_new (bef, aft) curmoves
   220     in
   221         HOL4CMoves.put newmoves thy
   222     end
   223 
   224 fun get_hol4_cmove bef thy =
   225   Symtab.lookup (HOL4CMoves.get thy) bef
   226 
   227 fun follow_cname thmname thy =
   228     let
   229         val moves = HOL4CMoves.get thy
   230         fun F thmname =
   231             case Symtab.lookup moves thmname of
   232                 SOME name => F name
   233               | NONE => thmname
   234     in
   235         F thmname
   236     end
   237 
   238 fun add_hol4_mapping bthy bthm isathm thy =
   239     let 
   240        (* val _ = writeln ("Before follow_name: "^isathm)  *)
   241       val isathm = follow_name isathm thy
   242        (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
   243         val curmaps = HOL4Maps.get thy
   244         val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
   245         val upd_thy = HOL4Maps.put newmaps thy
   246     in
   247         upd_thy
   248     end;
   249 
   250 fun get_hol4_type_mapping bthy tycon thy =
   251     let
   252         val maps = HOL4TypeMaps.get thy
   253     in
   254         StringPair.lookup maps (bthy,tycon)
   255     end
   256 
   257 fun get_hol4_mapping bthy bthm thy =
   258     let
   259         val curmaps = HOL4Maps.get thy
   260     in
   261         StringPair.lookup curmaps (bthy,bthm)
   262     end;
   263 
   264 fun add_hol4_const_mapping bthy bconst internal isaconst thy =
   265     let
   266         val thy = case opt_get_output_thy thy of
   267                       "" => thy
   268                     | output_thy => if internal
   269                                     then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   270                                     else thy
   271         val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   272         val curmaps = HOL4ConstMaps.get thy
   273         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
   274         val upd_thy = HOL4ConstMaps.put newmaps thy
   275     in
   276         upd_thy
   277     end;
   278 
   279 fun add_hol4_const_renaming bthy bconst newname thy =
   280     let
   281         val currens = HOL4Rename.get thy
   282         val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
   283         val newrens = StringPair.update_new ((bthy,bconst),newname) currens
   284         val upd_thy = HOL4Rename.put newrens thy
   285     in
   286         upd_thy
   287     end;
   288 
   289 fun get_hol4_const_renaming bthy bconst thy =
   290     let
   291         val currens = HOL4Rename.get thy
   292     in
   293         StringPair.lookup currens (bthy,bconst)
   294     end;
   295 
   296 fun get_hol4_const_mapping bthy bconst thy =
   297     let
   298         val bconst = case get_hol4_const_renaming bthy bconst thy of
   299                          SOME name => name
   300                        | NONE => bconst
   301         val maps = HOL4ConstMaps.get thy
   302     in
   303         StringPair.lookup maps (bthy,bconst)
   304     end
   305 
   306 fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
   307     let
   308         val thy = case opt_get_output_thy thy of
   309                       "" => thy
   310                     | output_thy => if internal
   311                                     then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   312                                     else thy
   313         val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   314         val curmaps = HOL4ConstMaps.get thy
   315         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
   316         val upd_thy = HOL4ConstMaps.put newmaps thy
   317     in
   318         upd_thy
   319     end;
   320 
   321 fun add_hol4_type_mapping bthy bconst internal isaconst thy =
   322     let
   323         val curmaps = HOL4TypeMaps.get thy
   324         val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   325         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
   326                handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
   327                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
   328         val upd_thy = HOL4TypeMaps.put newmaps thy
   329     in
   330         upd_thy
   331     end;
   332 
   333 fun add_hol4_pending bthy bthm hth thy =
   334     let
   335         val thmname = Sign.full_bname thy bthm
   336         val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
   337         val curpend = HOL4Pending.get thy
   338         val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
   339         val upd_thy = HOL4Pending.put newpend thy
   340         val thy' = case opt_get_output_thy upd_thy of
   341                        "" => add_hol4_mapping bthy bthm thmname upd_thy
   342                      | output_thy =>
   343                        let
   344                            val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
   345                        in
   346                            upd_thy |> add_hol4_move thmname new_thmname
   347                                    |> add_hol4_mapping bthy bthm new_thmname
   348                        end
   349     in
   350         thy'
   351     end;
   352 
   353 fun get_hol4_theorem thyname thmname thy =
   354   let
   355     val isathms = HOL4Thms.get thy
   356   in
   357     StringPair.lookup isathms (thyname,thmname)
   358   end;
   359 
   360 fun add_hol4_theorem thyname thmname hth =
   361   let
   362     val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
   363   in
   364     HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
   365   end;
   366 
   367 fun export_hol4_pending thy =
   368   let
   369     val rews = HOL4Rewrites.get thy;
   370     val pending = HOL4Pending.get thy;
   371     fun process ((bthy,bthm), hth as (_,thm)) thy =
   372       let
   373         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
   374         val thm2 = Drule.standard thm1;
   375       in
   376         thy
   377         |> PureThy.store_thm (Binding.name bthm, thm2)
   378         |> snd
   379         |> add_hol4_theorem bthy bthm hth
   380       end;
   381   in
   382     thy
   383     |> StringPair.fold process pending
   384     |> HOL4Pending.put StringPair.empty
   385   end;
   386 
   387 fun setup_dump (dir,thyname) thy =
   388     HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
   389 
   390 fun add_dump str thy =
   391     let
   392         val (dir,thyname,curdump) = HOL4Dump.get thy
   393     in
   394         HOL4Dump.put (dir,thyname,str::curdump) thy
   395     end
   396 
   397 fun flush_dump thy =
   398     let
   399         val (dir,thyname,dumpdata) = HOL4Dump.get thy
   400         val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
   401                                                       file=thyname ^ ".thy"})
   402         val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
   403         val  _ = TextIO.closeOut os
   404     in
   405         HOL4Dump.put ("","",[]) thy
   406     end
   407 
   408 fun set_generating_thy thyname thy =
   409     case HOL4DefThy.get thy of
   410         NoImport => HOL4DefThy.put (Generating thyname) thy
   411       | _ => error "Import already in progess"
   412 
   413 fun set_replaying_thy thyname thy =
   414     case HOL4DefThy.get thy of
   415         NoImport => HOL4DefThy.put (Replaying thyname) thy
   416       | _ => error "Import already in progess"
   417 
   418 fun clear_import_thy thy =
   419     case HOL4DefThy.get thy of
   420         NoImport => error "No import in progress"
   421       | _ => HOL4DefThy.put NoImport thy
   422 
   423 fun get_generating_thy thy =
   424     case HOL4DefThy.get thy of
   425         Generating thyname => thyname
   426       | _ => error "No theory being generated"
   427 
   428 fun get_replaying_thy thy =
   429     case HOL4DefThy.get thy of
   430         Replaying thyname => thyname
   431       | _ => error "No theory being replayed"
   432 
   433 fun get_import_thy thy =
   434     case HOL4DefThy.get thy of
   435         Replaying thyname => thyname
   436       | Generating thyname => thyname
   437       | _ => error "No theory being imported"
   438 
   439 fun should_ignore thyname thy thmname =
   440     case get_hol4_mapping thyname thmname thy of
   441         SOME NONE => true 
   442       | _ => false
   443 
   444 val trans_string =
   445     let
   446         fun quote s = "\"" ^ s ^ "\""
   447         fun F [] = []
   448           | F (#"\\" :: cs) = patch #"\\" cs
   449           | F (#"\"" :: cs) = patch #"\"" cs
   450           | F (c     :: cs) = c :: F cs
   451         and patch c rest = #"\\" :: c :: F rest
   452     in
   453         quote o String.implode o F o String.explode
   454     end
   455 
   456 fun dump_import_thy thyname thy =
   457     let
   458         val output_dir = get_output_dir thy
   459         val output_thy = get_output_thy thy
   460         val input_thy = Context.theory_name thy
   461         val import_segment = get_import_segment thy
   462         val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
   463                                                       file=thyname ^ ".imp"})
   464         fun out s = TextIO.output(os,s)
   465     val (ignored, mapped) = StringPair.fold
   466       (fn ((bthy, bthm), v) => fn (ign, map) =>
   467         if bthy = thyname
   468         then case v
   469          of NONE => (bthm :: ign, map)
   470           | SOME w => (ign, (bthm, w) :: map)
   471         else (ign, map)) (HOL4Maps.get thy) ([],[]);
   472     fun mk init = StringPair.fold
   473       (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
   474     val constmaps = mk (HOL4ConstMaps.get thy);
   475     val constrenames = mk (HOL4Rename.get thy);
   476     val typemaps = mk (HOL4TypeMaps.get thy);
   477     val defmaps = mk (HOL4DefMaps.get thy);
   478         fun new_name internal isa =
   479             if internal
   480             then
   481                 let
   482                     val paths = Long_Name.explode isa
   483                     val i = drop (length paths - 2) paths
   484                 in
   485                     case i of
   486                         [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
   487                       | _ => error "hol4rews.dump internal error"
   488                 end
   489             else
   490                 isa
   491 
   492         val _ = out "import\n\n"
   493 
   494         val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
   495         val _ = if null defmaps
   496                 then ()
   497                 else out "def_maps"
   498         val _ = app (fn (hol,isa) =>
   499                         out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
   500         val _ = if null defmaps
   501                 then ()
   502                 else out "\n\n"
   503 
   504         val _ = if null typemaps
   505                 then ()
   506                 else out "type_maps"
   507         val _ = app (fn (hol,(internal,isa)) =>
   508                         out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
   509         val _ = if null typemaps
   510                 then ()
   511                 else out "\n\n"
   512 
   513         val _ = if null constmaps
   514                 then ()
   515                 else out "const_maps"
   516         val _ = app (fn (hol,(internal,isa,opt_ty)) =>
   517                         (out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
   518                          case opt_ty of
   519                              SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
   520                            | NONE => ())) constmaps
   521         val _ = if null constmaps
   522                 then ()
   523                 else out "\n\n"
   524 
   525         val _ = if null constrenames
   526                 then ()
   527                 else out "const_renames"
   528         val _ = app (fn (old,new) =>
   529                         out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
   530         val _ = if null constrenames
   531                 then ()
   532                 else out "\n\n"
   533 
   534         fun gen2replay in_thy out_thy s = 
   535             let
   536                 val ss = Long_Name.explode s
   537             in
   538                 if (hd ss = in_thy) then 
   539                     Long_Name.implode (out_thy::(tl ss))
   540                 else
   541                     s
   542             end 
   543 
   544         val _ = if null mapped
   545                 then ()
   546                 else out "thm_maps"
   547         val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
   548         val _ = if null mapped 
   549                 then ()
   550                 else out "\n\n"
   551 
   552         val _ = if null ignored
   553                 then ()
   554                 else out "ignore_thms"
   555         val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored
   556         val _ = if null ignored
   557                 then ()
   558                 else out "\n\n"
   559 
   560         val _ = out "end\n"
   561         val _ = TextIO.closeOut os
   562     in
   563         thy
   564     end
   565 
   566 fun set_used_names names thy =
   567     let
   568         val unames = HOL4UNames.get thy
   569     in
   570         case unames of
   571             [] => HOL4UNames.put names thy
   572           | _ => error "hol4rews.set_used_names called on initialized data!"
   573     end
   574 
   575 val clear_used_names = HOL4UNames.put [];
   576 
   577 fun get_defmap thyname const thy =
   578     let
   579         val maps = HOL4DefMaps.get thy
   580     in
   581         StringPair.lookup maps (thyname,const)
   582     end
   583 
   584 fun add_defmap thyname const defname thy =
   585     let
   586         val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
   587         val maps = HOL4DefMaps.get thy
   588         val maps' = StringPair.update_new ((thyname,const),defname) maps
   589         val thy' = HOL4DefMaps.put maps' thy
   590     in
   591         thy'
   592     end
   593 
   594 fun get_defname thyname name thy =
   595     let
   596         val maps = HOL4DefMaps.get thy
   597         fun F dname = (dname,add_defmap thyname name dname thy)
   598     in
   599         case StringPair.lookup maps (thyname,name) of
   600             SOME thmname => (thmname,thy)
   601           | NONE =>
   602             let
   603                 val used = HOL4UNames.get thy
   604                 val defname = Thm.def_name name
   605                 val pdefname = name ^ "_primdef"
   606             in
   607                 if not (defname mem used)
   608                 then F defname                 (* name_def *)
   609                 else if not (pdefname mem used)
   610                 then F pdefname                (* name_primdef *)
   611                 else F (Name.variant used pdefname) (* last resort *)
   612             end
   613     end
   614 
   615 local
   616     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
   617       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
   618       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
   619       | handle_meta [x] = Appl[Constant "Trueprop",x]
   620       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
   621 in
   622 val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
   623 end
   624 
   625 local
   626     fun initial_maps thy =
   627         thy |> add_hol4_type_mapping "min" "bool" false "bool"
   628             |> add_hol4_type_mapping "min" "fun" false "fun"
   629             |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
   630             |> add_hol4_const_mapping "min" "=" false "op ="
   631             |> add_hol4_const_mapping "min" "==>" false "op -->"
   632             |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
   633 in
   634 val hol4_setup =
   635   initial_maps #>
   636   Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
   637 
   638 end