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