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