wneuper/isa: src/HOL/Import/import.ML@b8c7eb0c2f89

     1 (*  Title:      HOL/Import/import.ML

     2     Author:     Sebastian Skalberg (TU Muenchen)

     3 *)

     5 signature IMPORT =

     6 sig

     7     val debug      : bool Unsynchronized.ref

     8     val import_tac : Proof.context -> string * string -> tactic

     9     val setup      : theory -> theory

    10 end

    12 structure ImportData = Theory_Data

    13 (

    14   type T = ProofKernel.thm option array option  (* FIXME mutable array !??!!! *)

    15   val empty = NONE

    16   val extend = I

    17   fun merge _ = NONE

    18 )

    20 structure Import : IMPORT =

    21 struct

    23 val debug = Unsynchronized.ref false

    24 fun message s = if !debug then writeln s else ()

    26 fun import_tac ctxt (thyname, thmname) =

    27     if ! quick_and_dirty

    28     then Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)

    29     else

    30      fn th =>

    31         let

    32             val thy = Proof_Context.theory_of ctxt

    33             val prem = hd (prems_of th)

    34             val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)

    35             val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)

    36             val int_thms = case ImportData.get thy of

    37                                NONE => fst (Replay.setup_int_thms thyname thy)

    38                              | SOME a => a

    39             val proof = snd (ProofKernel.import_proof thyname thmname thy) thy

    40             val importerthm = snd (Replay.replay_proof int_thms thyname thmname proof thy)

    41             val thm = snd (ProofKernel.to_isa_thm importerthm)

    42             val rew = ProofKernel.rewrite_importer_term (concl_of thm) thy

    43             val thm = Thm.equal_elim rew thm

    44             val prew = ProofKernel.rewrite_importer_term prem thy

    45             val prem' = #2 (Logic.dest_equals (prop_of prew))

    46             val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)

    47             val thm = ProofKernel.disambiguate_frees thm

    48             val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)

    49         in

    50             case Shuffler.set_prop thy prem' [("",thm)] of

    51                 SOME (_,thm) =>

    52                 let

    53                     val _ = if prem' aconv (prop_of thm)

    54                             then message "import: Terms match up"

    55                             else message "import: Terms DO NOT match up"

    56                     val thm' = Thm.equal_elim (Thm.symmetric prew) thm

    57                     val res = Thm.bicompose true (false,thm',0) 1 th

    58                 in

    59                     res

    60                 end

    61               | NONE => (message "import: set_prop didn't succeed"; no_tac th)

    62         end

    64 val setup = Method.setup @{binding import}

    65   (Scan.lift (Args.name -- Args.name) >>

    66     (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))

    67   "import external theorem"

    69 (* Parsers *)

    71 val import_segment = Parse.name >> set_import_segment

    74 val import_theory = (Parse.name -- Parse.name) >> (fn (location, thyname) =>

    75                                fn thy =>

    76                                   thy |> set_generating_thy thyname

    77                                       |> Sign.add_path thyname

    78                                       |> add_dump ("setup_theory " ^ quote location ^ " " ^ thyname))

    80 fun end_import toks =

    81     Scan.succeed

    82         (fn thy =>

    83             let

    84                 val thyname = get_generating_thy thy

    85                 val segname = get_import_segment thy

    86                 val (int_thms,facts) = Replay.setup_int_thms thyname thy

    87                 val thmnames = filter_out (should_ignore thyname thy) facts

    88                 fun replay thy = Replay.import_thms thyname int_thms thmnames thy

    89             in

    90                 thy |> clear_import_thy

    91                     |> set_segment thyname segname

    92                     |> set_used_names facts

    93                     |> replay

    94                     |> clear_used_names

    95                     |> export_importer_pending

    96                     |> Sign.parent_path

    97                     |> dump_import_thy thyname

    98                     |> add_dump ";end_setup"

    99             end) toks

   101 val ignore_thms = Scan.repeat1 Parse.name

   102                                >> (fn ignored =>

   103                                    fn thy =>

   104                                       let

   105                                           val thyname = get_import_thy thy

   106                                       in

   107                                           Library.foldl (fn (thy,thmname) => ignore_importer thyname thmname thy) (thy,ignored)

   108                                       end)

   110 val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)

   111                             >> (fn thmmaps =>

   112                                 fn thy =>

   113                                    let

   114                                        val thyname = get_import_thy thy

   115                                    in

   116                                        Library.foldl (fn (thy,(hol,isa)) => add_importer_mapping thyname hol isa thy) (thy,thmmaps)

   117                                    end)

   119 val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)

   120                              >> (fn typmaps =>

   121                                  fn thy =>

   122                                     let

   123                                         val thyname = get_import_thy thy

   124                                     in

   125                                         Library.foldl (fn (thy,(hol,isa)) => add_importer_type_mapping thyname hol false isa thy) (thy,typmaps)

   126                                     end)

   128 val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)

   129                             >> (fn defmaps =>

   130                                 fn thy =>

   131                                    let

   132                                        val thyname = get_import_thy thy

   133                                    in

   134                                        Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)

   135                                    end)

   137 val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)

   138                                  >> (fn renames =>

   139                                      fn thy =>

   140                                         let

   141                                             val thyname = get_import_thy thy

   142                                         in

   143                                             Library.foldl (fn (thy,(hol,isa)) => add_importer_const_renaming thyname hol isa thy) (thy,renames)

   144                                         end)

   146 val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))

   147                               >> (fn constmaps =>

   148                                   fn thy =>

   149                                      let

   150                                          val thyname = get_import_thy thy

   151                                      in

   152                                          Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol false isa thy

   153                                                  | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)

   154                                      end)

   156 val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))

   157                                >> (fn constmaps =>

   158                                    fn thy =>

   159                                       let

   160                                           val thyname = get_import_thy thy

   161                                       in

   162                                           Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol true isa thy

   163                                                   | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)

   164                                       end)

   166 fun import_thy location s =

   167     let

   168         val src_location = Path.append (Path.explode location) (Path.basic (s ^ ".imp"))

   169         val is = TextIO.openIn (File.platform_path src_location)

   170         val inp = TextIO.inputAll is

   171         val _ = TextIO.closeIn is

   172         val orig_source = Source.of_string inp

   173         val symb_source = Symbol.source orig_source

   174         val lexes =

   175           (Scan.make_lexicon

   176             (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),

   177                   Scan.empty_lexicon)

   178         val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source

   179         val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)

   180         val import_segmentP = Parse.$$$ "import_segment" |-- import_segment

   181         val type_mapsP = Parse.$$$ "type_maps" |-- type_maps

   182         val def_mapsP = Parse.$$$ "def_maps" |-- def_maps

   183         val const_mapsP = Parse.$$$ "const_maps" |-- const_maps

   184         val const_movesP = Parse.$$$ "const_moves" |-- const_moves

   185         val const_renamesP = Parse.$$$ "const_renames" |-- const_renames

   186         val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms

   187         val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps

   188         val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP

   189         val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"

   190         fun apply [] thy = thy

   191           | apply (f::fs) thy = apply fs (f thy)

   192     in

   193         apply (set_replaying_thy s :: Sign.add_path s :: fst (importP token_list))

   194     end

   196 fun create_int_thms thyname thy =

   197     if ! quick_and_dirty

   198     then thy

   199     else

   200         case ImportData.get thy of

   201             NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy

   202           | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"

   204 fun clear_int_thms thy =

   205     if ! quick_and_dirty

   206     then thy

   207     else

   208         case ImportData.get thy of

   209             NONE => error "Import data already cleared - forgotten a setup_theory?"

   210           | SOME _ => ImportData.put NONE thy

   212 val setup_theory = (Parse.name -- Parse.name)

   213                        >>

   214                        (fn (location, thyname) =>

   215                         fn thy =>

   216                            (case Importer_DefThy.get thy of

   217                                 NoImport => thy

   218                               | Generating _ => error "Currently generating a theory!"

   219                               | Replaying _ => thy |> clear_import_thy)

   220                                |> import_thy location thyname

   221                                |> create_int_thms thyname)

   223 fun end_setup toks =

   224     Scan.succeed

   225         (fn thy =>

   226             let

   227                 val thyname = get_import_thy thy

   228                 val segname = get_import_segment thy

   229             in

   230                 thy |> set_segment thyname segname

   231                     |> clear_import_thy

   232                     |> clear_int_thms

   233                     |> Sign.parent_path

   234             end) toks

   236 val set_dump  = Parse.string -- Parse.string   >> setup_dump

   237 fun fl_dump toks  = Scan.succeed flush_dump toks

   238 val append_dump = (Parse.verbatim || Parse.string) >> add_dump

   240 val _ =

   241   (Outer_Syntax.command "import_segment"

   242                        "Set import segment name"

   243                        Keyword.thy_decl (import_segment >> Toplevel.theory);

   244    Outer_Syntax.command "import_theory"

   245                        "Set default external theory name"

   246                        Keyword.thy_decl (import_theory >> Toplevel.theory);

   247    Outer_Syntax.command "end_import"

   248                        "End external import"

   249                        Keyword.thy_decl (end_import >> Toplevel.theory);

   250    Outer_Syntax.command "setup_theory"

   251                        "Setup external theory replaying"

   252                        Keyword.thy_decl (setup_theory >> Toplevel.theory);

   253    Outer_Syntax.command "end_setup"

   254                        "End external setup"

   255                        Keyword.thy_decl (end_setup >> Toplevel.theory);

   256    Outer_Syntax.command "setup_dump"

   257                        "Setup the dump file name"

   258                        Keyword.thy_decl (set_dump >> Toplevel.theory);

   259    Outer_Syntax.command "append_dump"

   260                        "Add text to dump file"

   261                        Keyword.thy_decl (append_dump >> Toplevel.theory);

   262    Outer_Syntax.command "flush_dump"

   263                        "Write the dump to file"

   264                        Keyword.thy_decl (fl_dump >> Toplevel.theory);

   265    Outer_Syntax.command "ignore_thms"

   266                        "Theorems to ignore in next external theory import"

   267                        Keyword.thy_decl (ignore_thms >> Toplevel.theory);

   268    Outer_Syntax.command "type_maps"

   269                        "Map external type names to existing Isabelle/HOL type names"

   270                        Keyword.thy_decl (type_maps >> Toplevel.theory);

   271    Outer_Syntax.command "def_maps"

   272                        "Map external constant names to their primitive definitions"

   273                        Keyword.thy_decl (def_maps >> Toplevel.theory);

   274    Outer_Syntax.command "thm_maps"

   275                        "Map external theorem names to existing Isabelle/HOL theorem names"

   276                        Keyword.thy_decl (thm_maps >> Toplevel.theory);

   277    Outer_Syntax.command "const_renames"

   278                        "Rename external const names"

   279                        Keyword.thy_decl (const_renames >> Toplevel.theory);

   280    Outer_Syntax.command "const_moves"

   281                        "Rename external const names to other external constants"

   282                        Keyword.thy_decl (const_moves >> Toplevel.theory);

   283    Outer_Syntax.command "const_maps"

   284                        "Map external const names to existing Isabelle/HOL const names"

   285                        Keyword.thy_decl (const_maps >> Toplevel.theory));

   287 end

author	wenzelm
	Thu, 15 Mar 2012 19:02:34 +0100
changeset 47821	b8c7eb0c2f89
parent 47676	50dbdb9e28ad
child 47836	5c6955f487e5
permissions	-rw-r--r--