author | haftmann |
Sat, 03 Mar 2012 21:00:04 +0100 | |
changeset 46780 | ab4f3f765f91 |
parent 43918 | 6ca79a354c51 |
child 46799 | f21494dc0bf6 |
permissions | -rw-r--r-- |
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 | 5 |
signature HOL4_IMPORT_SYNTAX = |
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 | 21 |
|
22 |
val setup : unit -> unit |
|
23 |
end |
|
24 |
||
25 |
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX = |
|
26 |
struct |
|
27 |
||
28 |
(* Parsers *) |
|
29 |
||
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
30 |
val import_segment = Parse.name >> set_import_segment |
14516 | 31 |
|
19064 | 32 |
|
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
33 |
val import_theory = (Parse.name -- Parse.name) >> (fn (location, thyname) => |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
34 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
35 |
thy |> set_generating_thy thyname |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
36 |
|> Sign.add_path thyname |
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
37 |
|> add_dump ("setup_theory " ^ quote location ^ " " ^ thyname)) |
14516 | 38 |
|
14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
39 |
fun end_import toks = |
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
40 |
Scan.succeed |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
41 |
(fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
42 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
43 |
val thyname = get_generating_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
44 |
val segname = get_import_segment thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
45 |
val (int_thms,facts) = Replay.setup_int_thms thyname thy |
33317 | 46 |
val thmnames = filter_out (should_ignore thyname thy) facts |
43918
6ca79a354c51
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43785
diff
changeset
|
47 |
fun replay thy = Replay.import_thms thyname int_thms thmnames thy |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
48 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
49 |
thy |> clear_import_thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
50 |
|> set_segment thyname segname |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
51 |
|> set_used_names facts |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
52 |
|> replay |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
53 |
|> clear_used_names |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
54 |
|> export_hol4_pending |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
55 |
|> Sign.parent_path |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
56 |
|> dump_import_thy thyname |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
57 |
|> add_dump ";end_setup" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
58 |
end) toks |
14516 | 59 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
60 |
val ignore_thms = Scan.repeat1 Parse.name |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
61 |
>> (fn ignored => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
62 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
63 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
64 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
65 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
66 |
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
|
67 |
end) |
14516 | 68 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
69 |
val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
70 |
>> (fn thmmaps => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
71 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
72 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
73 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
74 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
75 |
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
|
76 |
end) |
14516 | 77 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
78 |
val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
79 |
>> (fn typmaps => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
80 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
81 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
82 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
83 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
84 |
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
|
85 |
end) |
14516 | 86 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
87 |
val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
88 |
>> (fn defmaps => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
89 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
90 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
91 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
92 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
93 |
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
|
94 |
end) |
14516 | 95 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
96 |
val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
97 |
>> (fn renames => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
98 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
99 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
100 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
101 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
102 |
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
|
103 |
end) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
104 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
105 |
val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ)) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
106 |
>> (fn constmaps => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
107 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
108 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
109 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
110 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
111 |
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
|
112 |
| (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
|
113 |
end) |
14516 | 114 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
115 |
val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ)) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
116 |
>> (fn constmaps => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
117 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
118 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
119 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
120 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
121 |
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
|
122 |
| (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
|
123 |
end) |
14516 | 124 |
|
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
125 |
fun import_thy location s = |
14516 | 126 |
let |
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
127 |
val src_location = Path.append (Path.explode location) (Path.basic (s ^ ".imp")) |
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
128 |
val is = TextIO.openIn (File.platform_path src_location) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
129 |
val inp = TextIO.inputAll is |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
130 |
val _ = TextIO.closeIn is |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
131 |
val orig_source = Source.of_string inp |
40526 | 132 |
val symb_source = Symbol.source orig_source |
38803 | 133 |
val lexes = |
134 |
(Scan.make_lexicon |
|
135 |
(map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]), |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
136 |
Scan.empty_lexicon) |
38803 | 137 |
val token_source = Token.source {do_recover = NONE} (K lexes) Position.start symb_source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
33317
diff
changeset
|
138 |
val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source) |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
139 |
val import_segmentP = Parse.$$$ "import_segment" |-- import_segment |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
140 |
val type_mapsP = Parse.$$$ "type_maps" |-- type_maps |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
141 |
val def_mapsP = Parse.$$$ "def_maps" |-- def_maps |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
142 |
val const_mapsP = Parse.$$$ "const_maps" |-- const_maps |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
143 |
val const_movesP = Parse.$$$ "const_moves" |-- const_moves |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
144 |
val const_renamesP = Parse.$$$ "const_renames" |-- const_renames |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
145 |
val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
146 |
val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
147 |
val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
148 |
val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
149 |
fun apply [] thy = thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
150 |
| apply (f::fs) thy = apply fs (f thy) |
14516 | 151 |
in |
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
152 |
apply (set_replaying_thy s :: Sign.add_path s :: fst (importP token_list)) |
14516 | 153 |
end |
154 |
||
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset
|
155 |
fun create_int_thms thyname thy = |
17370 | 156 |
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
|
157 |
then thy |
5d137da82f03
Forgot a couple of checks for the quick_and_dirty flag the other day.
skalberg
parents:
14620
diff
changeset
|
158 |
else |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
159 |
case ImportData.get thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
160 |
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
|
161 |
| 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
|
162 |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset
|
163 |
fun clear_int_thms thy = |
17370 | 164 |
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
|
165 |
then thy |
5d137da82f03
Forgot a couple of checks for the quick_and_dirty flag the other day.
skalberg
parents:
14620
diff
changeset
|
166 |
else |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
167 |
case ImportData.get thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
168 |
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
|
169 |
| SOME _ => ImportData.put NONE thy |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset
|
170 |
|
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
171 |
val setup_theory = (Parse.name -- Parse.name) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
172 |
>> |
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
173 |
(fn (location, thyname) => |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
174 |
fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
175 |
(case HOL4DefThy.get thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
176 |
NoImport => thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
177 |
| Generating _ => error "Currently generating a theory!" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
178 |
| Replaying _ => thy |> clear_import_thy) |
46780
ab4f3f765f91
explicit locations for import_theory and setup_theory, for better user interface conformance
haftmann
parents:
43918
diff
changeset
|
179 |
|> import_thy location thyname |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
180 |
|> create_int_thms thyname) |
14516 | 181 |
|
14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
182 |
fun end_setup toks = |
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
183 |
Scan.succeed |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
184 |
(fn thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
185 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
186 |
val thyname = get_import_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
187 |
val segname = get_import_segment thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
188 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
189 |
thy |> set_segment thyname segname |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
190 |
|> clear_import_thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
191 |
|> clear_int_thms |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
192 |
|> Sign.parent_path |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
193 |
end) toks |
14516 | 194 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
195 |
val set_dump = Parse.string -- Parse.string >> setup_dump |
14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
196 |
fun fl_dump toks = Scan.succeed flush_dump toks |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
197 |
val append_dump = (Parse.verbatim || Parse.string) >> add_dump |
14516 | 198 |
|
24867 | 199 |
fun setup () = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
200 |
(Keyword.keyword ">"; |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
201 |
Outer_Syntax.command "import_segment" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
202 |
"Set import segment name" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
203 |
Keyword.thy_decl (import_segment >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
204 |
Outer_Syntax.command "import_theory" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
205 |
"Set default HOL4 theory name" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
206 |
Keyword.thy_decl (import_theory >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
207 |
Outer_Syntax.command "end_import" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
208 |
"End HOL4 import" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
209 |
Keyword.thy_decl (end_import >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
210 |
Outer_Syntax.command "setup_theory" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
211 |
"Setup HOL4 theory replaying" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
212 |
Keyword.thy_decl (setup_theory >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
213 |
Outer_Syntax.command "end_setup" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
214 |
"End HOL4 setup" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
215 |
Keyword.thy_decl (end_setup >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
216 |
Outer_Syntax.command "setup_dump" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
217 |
"Setup the dump file name" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
218 |
Keyword.thy_decl (set_dump >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
219 |
Outer_Syntax.command "append_dump" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
220 |
"Add text to dump file" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
221 |
Keyword.thy_decl (append_dump >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
222 |
Outer_Syntax.command "flush_dump" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
223 |
"Write the dump to file" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
224 |
Keyword.thy_decl (fl_dump >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
225 |
Outer_Syntax.command "ignore_thms" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
226 |
"Theorems to ignore in next HOL4 theory import" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
227 |
Keyword.thy_decl (ignore_thms >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
228 |
Outer_Syntax.command "type_maps" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
229 |
"Map HOL4 type names to existing Isabelle/HOL type names" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
230 |
Keyword.thy_decl (type_maps >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
231 |
Outer_Syntax.command "def_maps" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
232 |
"Map HOL4 constant names to their primitive definitions" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
233 |
Keyword.thy_decl (def_maps >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
234 |
Outer_Syntax.command "thm_maps" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
235 |
"Map HOL4 theorem names to existing Isabelle/HOL theorem names" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
236 |
Keyword.thy_decl (thm_maps >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
237 |
Outer_Syntax.command "const_renames" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
238 |
"Rename HOL4 const names" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
239 |
Keyword.thy_decl (const_renames >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
240 |
Outer_Syntax.command "const_moves" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
241 |
"Rename HOL4 const names to other HOL4 constants" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
242 |
Keyword.thy_decl (const_moves >> Toplevel.theory); |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
243 |
Outer_Syntax.command "const_maps" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
244 |
"Map HOL4 const names to existing Isabelle/HOL const names" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
245 |
Keyword.thy_decl (const_maps >> Toplevel.theory)); |
14516 | 246 |
|
247 |
end |