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