src/HOL/Import/import_syntax.ML
author wenzelm
Wed Jan 12 15:15:51 2011 +0100 (2011-01-12)
changeset 41522 42d13d00ccfb
parent 40526 ca3c6b1bfcdb
child 43785 2bd54d4b5f3d
permissions -rw-r--r--
more FIXMEs concerning bad catch-all exception handlers;
     1 (*  Title:      HOL/Import/import_syntax.ML
     2     Author:     Sebastian Skalberg (TU Muenchen)
     3 *)
     4 
     5 signature HOL4_IMPORT_SYNTAX =
     6 sig
     7     val import_segment: (theory -> theory) parser
     8     val import_theory : (theory -> theory) parser
     9     val end_import    : (theory -> theory) parser
    10                         
    11     val setup_theory  : (theory -> theory) parser
    12     val end_setup     : (theory -> theory) parser
    13                         
    14     val thm_maps      : (theory -> theory) parser
    15     val ignore_thms   : (theory -> theory) parser
    16     val type_maps     : (theory -> theory) parser
    17     val def_maps      : (theory -> theory) parser
    18     val const_maps    : (theory -> theory) parser
    19     val const_moves   : (theory -> theory) parser
    20     val const_renames : (theory -> theory) parser
    21 
    22     val skip_import_dir : (theory -> theory) parser
    23     val skip_import     : (theory -> theory) parser
    24 
    25     val setup        : unit -> unit
    26 end
    27 
    28 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
    29 struct
    30 
    31 (* Parsers *)
    32 
    33 val import_segment = Parse.name >> set_import_segment
    34 
    35 
    36 val import_theory = Parse.name >> (fn thyname =>
    37                                fn thy =>
    38                                   thy |> set_generating_thy thyname
    39                                       |> Sign.add_path thyname
    40                                       |> add_dump (";setup_theory " ^ thyname))
    41 
    42 fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I: theory -> theory)
    43 val skip_import_dir = Parse.string >> do_skip_import_dir
    44 
    45 val lower = String.map Char.toLower
    46 fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I: theory -> theory)
    47 val skip_import = Parse.short_ident >> do_skip_import
    48 
    49 fun end_import toks =
    50     Scan.succeed
    51         (fn thy =>
    52             let
    53                 val thyname = get_generating_thy thy
    54                 val segname = get_import_segment thy
    55                 val (int_thms,facts) = Replay.setup_int_thms thyname thy
    56                 val thmnames = filter_out (should_ignore thyname thy) facts
    57                 fun replay thy = 
    58                     let
    59                         val _ = ImportRecorder.load_history thyname
    60                         val thy = Replay.import_thms thyname int_thms thmnames thy
    61                             handle x => (ImportRecorder.save_history thyname; raise x)  (* FIXME avoid handle x ?? *)
    62                         val _ = ImportRecorder.save_history thyname
    63                         val _ = ImportRecorder.clear_history ()
    64                     in
    65                         thy
    66                     end                                 
    67             in
    68                 thy |> clear_import_thy
    69                     |> set_segment thyname segname
    70                     |> set_used_names facts
    71                     |> replay 
    72                     |> clear_used_names
    73                     |> export_hol4_pending
    74                     |> Sign.parent_path
    75                     |> dump_import_thy thyname
    76                     |> add_dump ";end_setup"
    77             end) toks
    78 
    79 val ignore_thms = Scan.repeat1 Parse.name
    80                                >> (fn ignored =>
    81                                    fn thy =>
    82                                       let
    83                                           val thyname = get_import_thy thy
    84                                       in
    85                                           Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
    86                                       end)
    87 
    88 val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
    89                             >> (fn thmmaps =>
    90                                 fn thy =>
    91                                    let
    92                                        val thyname = get_import_thy thy
    93                                    in
    94                                        Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
    95                                    end)
    96 
    97 val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
    98                              >> (fn typmaps =>
    99                                  fn thy =>
   100                                     let
   101                                         val thyname = get_import_thy thy
   102                                     in
   103                                         Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
   104                                     end)
   105 
   106 val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
   107                             >> (fn defmaps =>
   108                                 fn thy =>
   109                                    let
   110                                        val thyname = get_import_thy thy
   111                                    in
   112                                        Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
   113                                    end)
   114 
   115 val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
   116                                  >> (fn renames =>
   117                                      fn thy =>
   118                                         let
   119                                             val thyname = get_import_thy thy
   120                                         in
   121                                             Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
   122                                         end)
   123                                                                                                                                       
   124 val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
   125                               >> (fn constmaps =>
   126                                   fn thy =>
   127                                      let
   128                                          val thyname = get_import_thy thy
   129                                      in
   130                                          Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
   131                                                  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
   132                                      end)
   133 
   134 val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
   135                                >> (fn constmaps =>
   136                                    fn thy =>
   137                                       let
   138                                           val thyname = get_import_thy thy
   139                                       in
   140                                           Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
   141                                                   | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
   142                                       end)
   143 
   144 fun import_thy s =
   145     let
   146         val is = TextIO.openIn(s ^ ".imp")
   147         val inp = TextIO.inputAll is
   148         val _ = TextIO.closeIn is
   149         val orig_source = Source.of_string inp
   150         val symb_source = Symbol.source orig_source
   151         val lexes =
   152           (Scan.make_lexicon
   153             (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
   154                   Scan.empty_lexicon)
   155         val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source
   156         val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
   157         val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
   158         val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
   159         val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
   160         val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
   161         val const_movesP = Parse.$$$ "const_moves" |-- const_moves
   162         val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
   163         val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
   164         val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
   165         val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
   166         val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
   167         fun apply [] thy = thy
   168           | apply (f::fs) thy = apply fs (f thy)
   169     in
   170         apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
   171     end
   172 
   173 fun create_int_thms thyname thy =
   174     if ! quick_and_dirty
   175     then thy
   176     else
   177         case ImportData.get thy of
   178             NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy
   179           | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
   180 
   181 fun clear_int_thms thy =
   182     if ! quick_and_dirty
   183     then thy
   184     else
   185         case ImportData.get thy of
   186             NONE => error "Import data already cleared - forgotten a setup_theory?"
   187           | SOME _ => ImportData.put NONE thy
   188 
   189 val setup_theory = Parse.name
   190                        >>
   191                        (fn thyname =>
   192                         fn thy =>
   193                            (case HOL4DefThy.get thy of
   194                                 NoImport => thy
   195                               | Generating _ => error "Currently generating a theory!"
   196                               | Replaying _ => thy |> clear_import_thy)
   197                                |> import_thy thyname
   198                                |> create_int_thms thyname)
   199 
   200 fun end_setup toks =
   201     Scan.succeed
   202         (fn thy =>
   203             let
   204                 val thyname = get_import_thy thy
   205                 val segname = get_import_segment thy
   206             in
   207                 thy |> set_segment thyname segname
   208                     |> clear_import_thy
   209                     |> clear_int_thms
   210                     |> Sign.parent_path
   211             end) toks
   212 
   213 val set_dump  = Parse.string -- Parse.string   >> setup_dump
   214 fun fl_dump toks  = Scan.succeed flush_dump toks
   215 val append_dump = (Parse.verbatim || Parse.string) >> add_dump
   216 
   217 fun setup () =
   218   (Keyword.keyword ">";
   219    Outer_Syntax.command "import_segment"
   220                        "Set import segment name"
   221                        Keyword.thy_decl (import_segment >> Toplevel.theory);
   222    Outer_Syntax.command "import_theory"
   223                        "Set default HOL4 theory name"
   224                        Keyword.thy_decl (import_theory >> Toplevel.theory);
   225    Outer_Syntax.command "end_import"
   226                        "End HOL4 import"
   227                        Keyword.thy_decl (end_import >> Toplevel.theory);
   228    Outer_Syntax.command "skip_import_dir" 
   229                        "Sets caching directory for skipping importing"
   230                        Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
   231    Outer_Syntax.command "skip_import" 
   232                        "Switches skipping importing on or off"
   233                        Keyword.thy_decl (skip_import >> Toplevel.theory);                   
   234    Outer_Syntax.command "setup_theory"
   235                        "Setup HOL4 theory replaying"
   236                        Keyword.thy_decl (setup_theory >> Toplevel.theory);
   237    Outer_Syntax.command "end_setup"
   238                        "End HOL4 setup"
   239                        Keyword.thy_decl (end_setup >> Toplevel.theory);
   240    Outer_Syntax.command "setup_dump"
   241                        "Setup the dump file name"
   242                        Keyword.thy_decl (set_dump >> Toplevel.theory);
   243    Outer_Syntax.command "append_dump"
   244                        "Add text to dump file"
   245                        Keyword.thy_decl (append_dump >> Toplevel.theory);
   246    Outer_Syntax.command "flush_dump"
   247                        "Write the dump to file"
   248                        Keyword.thy_decl (fl_dump >> Toplevel.theory);
   249    Outer_Syntax.command "ignore_thms"
   250                        "Theorems to ignore in next HOL4 theory import"
   251                        Keyword.thy_decl (ignore_thms >> Toplevel.theory);
   252    Outer_Syntax.command "type_maps"
   253                        "Map HOL4 type names to existing Isabelle/HOL type names"
   254                        Keyword.thy_decl (type_maps >> Toplevel.theory);
   255    Outer_Syntax.command "def_maps"
   256                        "Map HOL4 constant names to their primitive definitions"
   257                        Keyword.thy_decl (def_maps >> Toplevel.theory);
   258    Outer_Syntax.command "thm_maps"
   259                        "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
   260                        Keyword.thy_decl (thm_maps >> Toplevel.theory);
   261    Outer_Syntax.command "const_renames"
   262                        "Rename HOL4 const names"
   263                        Keyword.thy_decl (const_renames >> Toplevel.theory);
   264    Outer_Syntax.command "const_moves"
   265                        "Rename HOL4 const names to other HOL4 constants"
   266                        Keyword.thy_decl (const_moves >> Toplevel.theory);
   267    Outer_Syntax.command "const_maps"
   268                        "Map HOL4 const names to existing Isabelle/HOL const names"
   269                        Keyword.thy_decl (const_maps >> Toplevel.theory));
   270 
   271 end