src/HOL/Import/hol4rews.ML
author wenzelm
Wed Jan 12 15:15:51 2011 +0100 (2011-01-12)
changeset 41522 42d13d00ccfb
parent 39557 fe5722fce758
child 42224 578a51fae383
permissions -rw-r--r--
more FIXMEs concerning bad catch-all exception handlers;
     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 fun add_hol4_rewrite (Context.Theory thy, th) =
   160     let
   161         val _ = message "Adding HOL4 rewrite"
   162         val th1 = th RS @{thm eq_reflection}
   163         val current_rews = HOL4Rewrites.get thy
   164         val new_rews = insert Thm.eq_thm th1 current_rews
   165         val updated_thy  = HOL4Rewrites.put new_rews thy
   166     in
   167         (Context.Theory updated_thy,th1)
   168     end
   169   | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
   170 
   171 fun ignore_hol4 bthy bthm thy =
   172     let
   173         val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
   174         val curmaps = HOL4Maps.get thy
   175         val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
   176         val upd_thy = HOL4Maps.put newmaps thy
   177     in
   178         upd_thy
   179     end
   180 
   181 val opt_get_output_thy = #2 o HOL4Dump.get
   182 
   183 fun get_output_thy thy =
   184     case #2 (HOL4Dump.get thy) of
   185         "" => error "No theory file being output"
   186       | thyname => thyname
   187 
   188 val get_output_dir = #1 o HOL4Dump.get
   189 
   190 fun add_hol4_move bef aft thy =
   191     let
   192         val curmoves = HOL4Moves.get thy
   193         val newmoves = Symtab.update_new (bef, aft) curmoves
   194     in
   195         HOL4Moves.put newmoves thy
   196     end
   197 
   198 fun get_hol4_move bef thy =
   199   Symtab.lookup (HOL4Moves.get thy) bef
   200 
   201 fun follow_name thmname thy =
   202     let
   203         val moves = HOL4Moves.get thy
   204         fun F thmname =
   205             case Symtab.lookup moves thmname of
   206                 SOME name => F name
   207               | NONE => thmname
   208     in
   209         F thmname
   210     end
   211 
   212 fun add_hol4_cmove bef aft thy =
   213     let
   214         val curmoves = HOL4CMoves.get thy
   215         val newmoves = Symtab.update_new (bef, aft) curmoves
   216     in
   217         HOL4CMoves.put newmoves thy
   218     end
   219 
   220 fun get_hol4_cmove bef thy =
   221   Symtab.lookup (HOL4CMoves.get thy) bef
   222 
   223 fun follow_cname thmname thy =
   224     let
   225         val moves = HOL4CMoves.get thy
   226         fun F thmname =
   227             case Symtab.lookup moves thmname of
   228                 SOME name => F name
   229               | NONE => thmname
   230     in
   231         F thmname
   232     end
   233 
   234 fun add_hol4_mapping bthy bthm isathm thy =
   235     let 
   236        (* val _ = writeln ("Before follow_name: "^isathm)  *)
   237       val isathm = follow_name isathm thy
   238        (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
   239         val curmaps = HOL4Maps.get thy
   240         val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
   241         val upd_thy = HOL4Maps.put newmaps thy
   242     in
   243         upd_thy
   244     end;
   245 
   246 fun get_hol4_type_mapping bthy tycon thy =
   247     let
   248         val maps = HOL4TypeMaps.get thy
   249     in
   250         StringPair.lookup maps (bthy,tycon)
   251     end
   252 
   253 fun get_hol4_mapping bthy bthm thy =
   254     let
   255         val curmaps = HOL4Maps.get thy
   256     in
   257         StringPair.lookup curmaps (bthy,bthm)
   258     end;
   259 
   260 fun add_hol4_const_mapping bthy bconst internal isaconst thy =
   261     let
   262         val thy = case opt_get_output_thy thy of
   263                       "" => thy
   264                     | output_thy => if internal
   265                                     then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   266                                     else thy
   267         val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   268         val curmaps = HOL4ConstMaps.get thy
   269         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
   270         val upd_thy = HOL4ConstMaps.put newmaps thy
   271     in
   272         upd_thy
   273     end;
   274 
   275 fun add_hol4_const_renaming bthy bconst newname thy =
   276     let
   277         val currens = HOL4Rename.get thy
   278         val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
   279         val newrens = StringPair.update_new ((bthy,bconst),newname) currens
   280         val upd_thy = HOL4Rename.put newrens thy
   281     in
   282         upd_thy
   283     end;
   284 
   285 fun get_hol4_const_renaming bthy bconst thy =
   286     let
   287         val currens = HOL4Rename.get thy
   288     in
   289         StringPair.lookup currens (bthy,bconst)
   290     end;
   291 
   292 fun get_hol4_const_mapping bthy bconst thy =
   293     let
   294         val bconst = case get_hol4_const_renaming bthy bconst thy of
   295                          SOME name => name
   296                        | NONE => bconst
   297         val maps = HOL4ConstMaps.get thy
   298     in
   299         StringPair.lookup maps (bthy,bconst)
   300     end
   301 
   302 fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
   303     let
   304         val thy = case opt_get_output_thy thy of
   305                       "" => thy
   306                     | output_thy => if internal
   307                                     then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   308                                     else thy
   309         val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   310         val curmaps = HOL4ConstMaps.get thy
   311         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
   312         val upd_thy = HOL4ConstMaps.put newmaps thy
   313     in
   314         upd_thy
   315     end;
   316 
   317 fun add_hol4_type_mapping bthy bconst internal isaconst thy =
   318     let
   319         val curmaps = HOL4TypeMaps.get thy
   320         val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   321         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
   322                (* FIXME avoid handle x *)
   323                handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
   324                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
   325         val upd_thy = HOL4TypeMaps.put newmaps thy
   326     in
   327         upd_thy
   328     end;
   329 
   330 fun add_hol4_pending bthy bthm hth thy =
   331     let
   332         val thmname = Sign.full_bname thy bthm
   333         val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
   334         val curpend = HOL4Pending.get thy
   335         val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
   336         val upd_thy = HOL4Pending.put newpend thy
   337         val thy' = case opt_get_output_thy upd_thy of
   338                        "" => add_hol4_mapping bthy bthm thmname upd_thy
   339                      | output_thy =>
   340                        let
   341                            val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
   342                        in
   343                            upd_thy |> add_hol4_move thmname new_thmname
   344                                    |> add_hol4_mapping bthy bthm new_thmname
   345                        end
   346     in
   347         thy'
   348     end;
   349 
   350 fun get_hol4_theorem thyname thmname thy =
   351   let
   352     val isathms = HOL4Thms.get thy
   353   in
   354     StringPair.lookup isathms (thyname,thmname)
   355   end;
   356 
   357 fun add_hol4_theorem thyname thmname hth =
   358   let
   359     val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
   360   in
   361     HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
   362   end;
   363 
   364 fun export_hol4_pending thy =
   365   let
   366     val rews = HOL4Rewrites.get thy;
   367     val pending = HOL4Pending.get thy;
   368     fun process ((bthy,bthm), hth as (_,thm)) thy =
   369       let
   370         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
   371         val thm2 = Drule.export_without_context thm1;
   372       in
   373         thy
   374         |> Global_Theory.store_thm (Binding.name bthm, thm2)
   375         |> snd
   376         |> add_hol4_theorem bthy bthm hth
   377       end;
   378   in
   379     thy
   380     |> StringPair.fold process pending
   381     |> HOL4Pending.put StringPair.empty
   382   end;
   383 
   384 fun setup_dump (dir,thyname) thy =
   385     HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
   386 
   387 fun add_dump str thy =
   388     let
   389         val (dir,thyname,curdump) = HOL4Dump.get thy
   390     in
   391         HOL4Dump.put (dir,thyname,str::curdump) thy
   392     end
   393 
   394 fun flush_dump thy =
   395     let
   396         val (dir,thyname,dumpdata) = HOL4Dump.get thy
   397         val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
   398                                                       file=thyname ^ ".thy"})
   399         val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
   400         val  _ = TextIO.closeOut os
   401     in
   402         HOL4Dump.put ("","",[]) thy
   403     end
   404 
   405 fun set_generating_thy thyname thy =
   406     case HOL4DefThy.get thy of
   407         NoImport => HOL4DefThy.put (Generating thyname) thy
   408       | _ => error "Import already in progess"
   409 
   410 fun set_replaying_thy thyname thy =
   411     case HOL4DefThy.get thy of
   412         NoImport => HOL4DefThy.put (Replaying thyname) thy
   413       | _ => error "Import already in progess"
   414 
   415 fun clear_import_thy thy =
   416     case HOL4DefThy.get thy of
   417         NoImport => error "No import in progress"
   418       | _ => HOL4DefThy.put NoImport thy
   419 
   420 fun get_generating_thy thy =
   421     case HOL4DefThy.get thy of
   422         Generating thyname => thyname
   423       | _ => error "No theory being generated"
   424 
   425 fun get_replaying_thy thy =
   426     case HOL4DefThy.get thy of
   427         Replaying thyname => thyname
   428       | _ => error "No theory being replayed"
   429 
   430 fun get_import_thy thy =
   431     case HOL4DefThy.get thy of
   432         Replaying thyname => thyname
   433       | Generating thyname => thyname
   434       | _ => error "No theory being imported"
   435 
   436 fun should_ignore thyname thy thmname =
   437     case get_hol4_mapping thyname thmname thy of
   438         SOME NONE => true 
   439       | _ => false
   440 
   441 val trans_string =
   442     let
   443         fun quote s = "\"" ^ s ^ "\""
   444         fun F [] = []
   445           | F (#"\\" :: cs) = patch #"\\" cs
   446           | F (#"\"" :: cs) = patch #"\"" cs
   447           | F (c     :: cs) = c :: F cs
   448         and patch c rest = #"\\" :: c :: F rest
   449     in
   450         quote o String.implode o F o String.explode
   451     end
   452 
   453 fun dump_import_thy thyname thy =
   454     let
   455         val output_dir = get_output_dir thy
   456         val output_thy = get_output_thy thy
   457         val input_thy = Context.theory_name thy
   458         val import_segment = get_import_segment thy
   459         val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
   460                                                       file=thyname ^ ".imp"})
   461         fun out s = TextIO.output(os,s)
   462     val (ignored, mapped) = StringPair.fold
   463       (fn ((bthy, bthm), v) => fn (ign, map) =>
   464         if bthy = thyname
   465         then case v
   466          of NONE => (bthm :: ign, map)
   467           | SOME w => (ign, (bthm, w) :: map)
   468         else (ign, map)) (HOL4Maps.get thy) ([],[]);
   469     fun mk init = StringPair.fold
   470       (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
   471     val constmaps = mk (HOL4ConstMaps.get thy);
   472     val constrenames = mk (HOL4Rename.get thy);
   473     val typemaps = mk (HOL4TypeMaps.get thy);
   474     val defmaps = mk (HOL4DefMaps.get thy);
   475         fun new_name internal isa =
   476             if internal
   477             then
   478                 let
   479                     val paths = Long_Name.explode isa
   480                     val i = drop (length paths - 2) paths
   481                 in
   482                     case i of
   483                         [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
   484                       | _ => error "hol4rews.dump internal error"
   485                 end
   486             else
   487                 isa
   488 
   489         val _ = out "import\n\n"
   490 
   491         val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
   492         val _ = if null defmaps
   493                 then ()
   494                 else out "def_maps"
   495         val _ = app (fn (hol,isa) =>
   496                         out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
   497         val _ = if null defmaps
   498                 then ()
   499                 else out "\n\n"
   500 
   501         val _ = if null typemaps
   502                 then ()
   503                 else out "type_maps"
   504         val _ = app (fn (hol,(internal,isa)) =>
   505                         out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
   506         val _ = if null typemaps
   507                 then ()
   508                 else out "\n\n"
   509 
   510         val _ = if null constmaps
   511                 then ()
   512                 else out "const_maps"
   513         val _ = app (fn (hol,(internal,isa,opt_ty)) =>
   514                         (out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
   515                          case opt_ty of
   516                              SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
   517                            | NONE => ())) constmaps
   518         val _ = if null constmaps
   519                 then ()
   520                 else out "\n\n"
   521 
   522         val _ = if null constrenames
   523                 then ()
   524                 else out "const_renames"
   525         val _ = app (fn (old,new) =>
   526                         out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
   527         val _ = if null constrenames
   528                 then ()
   529                 else out "\n\n"
   530 
   531         fun gen2replay in_thy out_thy s = 
   532             let
   533                 val ss = Long_Name.explode s
   534             in
   535                 if (hd ss = in_thy) then 
   536                     Long_Name.implode (out_thy::(tl ss))
   537                 else
   538                     s
   539             end 
   540 
   541         val _ = if null mapped
   542                 then ()
   543                 else out "thm_maps"
   544         val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
   545         val _ = if null mapped 
   546                 then ()
   547                 else out "\n\n"
   548 
   549         val _ = if null ignored
   550                 then ()
   551                 else out "ignore_thms"
   552         val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored
   553         val _ = if null ignored
   554                 then ()
   555                 else out "\n\n"
   556 
   557         val _ = out "end\n"
   558         val _ = TextIO.closeOut os
   559     in
   560         thy
   561     end
   562 
   563 fun set_used_names names thy =
   564     let
   565         val unames = HOL4UNames.get thy
   566     in
   567         case unames of
   568             [] => HOL4UNames.put names thy
   569           | _ => error "hol4rews.set_used_names called on initialized data!"
   570     end
   571 
   572 val clear_used_names = HOL4UNames.put [];
   573 
   574 fun get_defmap thyname const thy =
   575     let
   576         val maps = HOL4DefMaps.get thy
   577     in
   578         StringPair.lookup maps (thyname,const)
   579     end
   580 
   581 fun add_defmap thyname const defname thy =
   582     let
   583         val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
   584         val maps = HOL4DefMaps.get thy
   585         val maps' = StringPair.update_new ((thyname,const),defname) maps
   586         val thy' = HOL4DefMaps.put maps' thy
   587     in
   588         thy'
   589     end
   590 
   591 fun get_defname thyname name thy =
   592     let
   593         val maps = HOL4DefMaps.get thy
   594         fun F dname = (dname,add_defmap thyname name dname thy)
   595     in
   596         case StringPair.lookup maps (thyname,name) of
   597             SOME thmname => (thmname,thy)
   598           | NONE =>
   599             let
   600                 val used = HOL4UNames.get thy
   601                 val defname = Thm.def_name name
   602                 val pdefname = name ^ "_primdef"
   603             in
   604                 if not (member (op =) used defname)
   605                 then F defname                 (* name_def *)
   606                 else if not (member (op =) used pdefname)
   607                 then F pdefname                (* name_primdef *)
   608                 else F (Name.variant used pdefname) (* last resort *)
   609             end
   610     end
   611 
   612 local
   613     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
   614       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
   615       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
   616       | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
   617       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
   618 in
   619 val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
   620 end
   621 
   622 local
   623     fun initial_maps thy =
   624         thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
   625             |> add_hol4_type_mapping "min" "fun" false "fun"
   626             |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
   627             |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
   628             |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
   629             |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
   630 in
   631 val hol4_setup =
   632   initial_maps #>
   633   Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
   634 
   635 end