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