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