author | wenzelm |
Tue, 11 Jul 2006 12:16:54 +0200 | |
changeset 20071 | 8f3e1ddb50e6 |
parent 18921 | f47c46d7d654 |
child 20897 | 3f8d2834b2c4 |
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/hol4rews.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 |
structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord); |
7 |
||
8 |
type holthm = (term * term) list * thm |
|
9 |
||
10 |
datatype ImportStatus = |
|
11 |
NoImport |
|
12 |
| Generating of string |
|
13 |
| Replaying of string |
|
14 |
||
15 |
structure HOL4DefThyArgs: THEORY_DATA_ARGS = |
|
16 |
struct |
|
17 |
val name = "HOL4/import_status" |
|
18 |
type T = ImportStatus |
|
19 |
val empty = NoImport |
|
20 |
val copy = I |
|
16424 | 21 |
val extend = I |
22 |
fun merge _ (NoImport,NoImport) = NoImport |
|
23 |
| merge _ _ = (warning "Import status set during merge"; NoImport) |
|
14516 | 24 |
fun print sg import_status = |
25 |
Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname))) |
|
26 |
end; |
|
27 |
||
28 |
structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs); |
|
29 |
||
30 |
structure ImportSegmentArgs: THEORY_DATA_ARGS = |
|
31 |
struct |
|
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset
|
32 |
val name = "HOL4/import_segment" |
14516 | 33 |
type T = string |
34 |
val empty = "" |
|
35 |
val copy = I |
|
16424 | 36 |
val extend = I |
37 |
fun merge _ ("",arg) = arg |
|
38 |
| merge _ (arg,"") = arg |
|
39 |
| merge _ (s1,s2) = |
|
14516 | 40 |
if s1 = s2 |
41 |
then s1 |
|
42 |
else error "Trying to merge two different import segments" |
|
43 |
fun print sg import_segment = |
|
44 |
Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment)) |
|
45 |
end; |
|
46 |
||
47 |
structure ImportSegment = TheoryDataFun(ImportSegmentArgs); |
|
48 |
||
49 |
val get_import_segment = ImportSegment.get |
|
50 |
val set_import_segment = ImportSegment.put |
|
51 |
||
52 |
structure HOL4UNamesArgs: THEORY_DATA_ARGS = |
|
53 |
struct |
|
54 |
val name = "HOL4/used_names" |
|
55 |
type T = string list |
|
56 |
val empty = [] |
|
57 |
val copy = I |
|
16424 | 58 |
val extend = I |
59 |
fun merge _ ([],[]) = [] |
|
60 |
| merge _ _ = error "Used names not empty during merge" |
|
14516 | 61 |
fun print sg used_names = |
62 |
Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented") |
|
63 |
end; |
|
64 |
||
65 |
structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs); |
|
66 |
||
67 |
structure HOL4DumpArgs: THEORY_DATA_ARGS = |
|
68 |
struct |
|
69 |
val name = "HOL4/dump_data" |
|
70 |
type T = string * string * string list |
|
71 |
val empty = ("","",[]) |
|
72 |
val copy = I |
|
16424 | 73 |
val extend = I |
74 |
fun merge _ (("","",[]),("","",[])) = ("","",[]) |
|
75 |
| merge _ _ = error "Dump data not empty during merge" |
|
14516 | 76 |
fun print sg dump_data = |
77 |
Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented") |
|
78 |
end; |
|
79 |
||
80 |
structure HOL4Dump = TheoryDataFun(HOL4DumpArgs); |
|
81 |
||
82 |
structure HOL4MovesArgs: THEORY_DATA_ARGS = |
|
83 |
struct |
|
84 |
val name = "HOL4/moves" |
|
85 |
type T = string Symtab.table |
|
86 |
val empty = Symtab.empty |
|
87 |
val copy = I |
|
16424 | 88 |
val extend = I |
89 |
fun merge _ : T * T -> T = Symtab.merge (K true) |
|
14516 | 90 |
fun print sg tab = |
91 |
Pretty.writeln (Pretty.big_list "HOL4 moves:" |
|
92 |
(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab))) |
|
93 |
end; |
|
94 |
||
95 |
structure HOL4Moves = TheoryDataFun(HOL4MovesArgs); |
|
96 |
||
97 |
structure HOL4ImportsArgs: THEORY_DATA_ARGS = |
|
98 |
struct |
|
99 |
val name = "HOL4/imports" |
|
100 |
type T = string Symtab.table |
|
101 |
val empty = Symtab.empty |
|
102 |
val copy = I |
|
16424 | 103 |
val extend = I |
104 |
fun merge _ : T * T -> T = Symtab.merge (K true) |
|
14516 | 105 |
fun print sg tab = |
106 |
Pretty.writeln (Pretty.big_list "HOL4 imports:" |
|
107 |
(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab))) |
|
108 |
end; |
|
109 |
||
110 |
structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs); |
|
111 |
||
112 |
fun get_segment2 thyname thy = |
|
17412 | 113 |
Symtab.lookup (HOL4Imports.get thy) thyname |
14516 | 114 |
|
115 |
fun set_segment thyname segname thy = |
|
116 |
let |
|
117 |
val imps = HOL4Imports.get thy |
|
17412 | 118 |
val imps' = Symtab.update_new (thyname,segname) imps |
14516 | 119 |
in |
120 |
HOL4Imports.put imps' thy |
|
121 |
end |
|
122 |
||
123 |
structure HOL4CMovesArgs: THEORY_DATA_ARGS = |
|
124 |
struct |
|
125 |
val name = "HOL4/constant_moves" |
|
126 |
type T = string Symtab.table |
|
127 |
val empty = Symtab.empty |
|
128 |
val copy = I |
|
16424 | 129 |
val extend = I |
130 |
fun merge _ : T * T -> T = Symtab.merge (K true) |
|
14516 | 131 |
fun print sg tab = |
132 |
Pretty.writeln (Pretty.big_list "HOL4 constant moves:" |
|
133 |
(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab))) |
|
134 |
end; |
|
135 |
||
136 |
structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs); |
|
137 |
||
138 |
structure HOL4MapsArgs: THEORY_DATA_ARGS = |
|
139 |
struct |
|
140 |
val name = "HOL4/mappings" |
|
141 |
type T = (string option) StringPair.table |
|
142 |
val empty = StringPair.empty |
|
143 |
val copy = I |
|
16424 | 144 |
val extend = I |
145 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 146 |
fun print sg tab = |
147 |
Pretty.writeln (Pretty.big_list "HOL4 mappings:" |
|
15531 | 148 |
(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab))) |
14516 | 149 |
end; |
150 |
||
151 |
structure HOL4Maps = TheoryDataFun(HOL4MapsArgs); |
|
152 |
||
153 |
structure HOL4ThmsArgs: THEORY_DATA_ARGS = |
|
154 |
struct |
|
155 |
val name = "HOL4/theorems" |
|
156 |
type T = holthm StringPair.table |
|
157 |
val empty = StringPair.empty |
|
158 |
val copy = I |
|
16424 | 159 |
val extend = I |
160 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 161 |
fun print sg tab = |
162 |
Pretty.writeln (Pretty.big_list "HOL4 mappings:" |
|
163 |
(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab))) |
|
164 |
end; |
|
165 |
||
166 |
structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs); |
|
167 |
||
168 |
structure HOL4ConstMapsArgs: THEORY_DATA_ARGS = |
|
169 |
struct |
|
170 |
val name = "HOL4/constmappings" |
|
171 |
type T = (bool * string * typ option) StringPair.table |
|
172 |
val empty = StringPair.empty |
|
173 |
val copy = I |
|
16424 | 174 |
val extend = I |
175 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 176 |
fun print sg tab = |
177 |
Pretty.writeln (Pretty.big_list "HOL4 constant mappings:" |
|
178 |
(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab))) |
|
179 |
end; |
|
180 |
||
181 |
structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs); |
|
182 |
||
183 |
structure HOL4RenameArgs: THEORY_DATA_ARGS = |
|
184 |
struct |
|
185 |
val name = "HOL4/renamings" |
|
186 |
type T = string StringPair.table |
|
187 |
val empty = StringPair.empty |
|
188 |
val copy = I |
|
16424 | 189 |
val extend = I |
190 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 191 |
fun print sg tab = |
192 |
Pretty.writeln (Pretty.big_list "HOL4 constant renamings:" |
|
193 |
(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab))) |
|
194 |
end; |
|
195 |
||
196 |
structure HOL4Rename = TheoryDataFun(HOL4RenameArgs); |
|
197 |
||
198 |
structure HOL4DefMapsArgs: THEORY_DATA_ARGS = |
|
199 |
struct |
|
200 |
val name = "HOL4/def_maps" |
|
201 |
type T = string StringPair.table |
|
202 |
val empty = StringPair.empty |
|
203 |
val copy = I |
|
16424 | 204 |
val extend = I |
205 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 206 |
fun print sg tab = |
207 |
Pretty.writeln (Pretty.big_list "HOL4 constant definitions:" |
|
208 |
(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab))) |
|
209 |
end; |
|
210 |
||
211 |
structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs); |
|
212 |
||
213 |
structure HOL4TypeMapsArgs: THEORY_DATA_ARGS = |
|
214 |
struct |
|
215 |
val name = "HOL4/typemappings" |
|
216 |
type T = (bool * string) StringPair.table |
|
217 |
val empty = StringPair.empty |
|
218 |
val copy = I |
|
16424 | 219 |
val extend = I |
220 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 221 |
fun print sg tab = |
222 |
Pretty.writeln (Pretty.big_list "HOL4 type mappings:" |
|
223 |
(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab))) |
|
224 |
end; |
|
225 |
||
226 |
structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs); |
|
227 |
||
228 |
structure HOL4PendingArgs: THEORY_DATA_ARGS = |
|
229 |
struct |
|
230 |
val name = "HOL4/pending" |
|
231 |
type T = ((term * term) list * thm) StringPair.table |
|
232 |
val empty = StringPair.empty |
|
233 |
val copy = I |
|
16424 | 234 |
val extend = I |
235 |
fun merge _ : T * T -> T = StringPair.merge (K true) |
|
14516 | 236 |
fun print sg tab = |
237 |
Pretty.writeln (Pretty.big_list "HOL4 pending theorems:" |
|
238 |
(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab))) |
|
239 |
end; |
|
240 |
||
241 |
structure HOL4Pending = TheoryDataFun(HOL4PendingArgs); |
|
242 |
||
243 |
structure HOL4RewritesArgs: THEORY_DATA_ARGS = |
|
244 |
struct |
|
245 |
val name = "HOL4/rewrites" |
|
246 |
type T = thm list |
|
247 |
val empty = [] |
|
248 |
val copy = I |
|
16424 | 249 |
val extend = I |
250 |
fun merge _ = Library.gen_union Thm.eq_thm |
|
14516 | 251 |
fun print sg thms = |
252 |
Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:" |
|
253 |
(map Display.pretty_thm thms)) |
|
254 |
end; |
|
255 |
||
256 |
structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs); |
|
257 |
||
258 |
val hol4_debug = ref false |
|
259 |
fun message s = if !hol4_debug then writeln s else () |
|
260 |
||
18728 | 261 |
fun add_hol4_rewrite (context, th) = |
14516 | 262 |
let |
18728 | 263 |
val thy = Context.the_theory context; |
14516 | 264 |
val _ = message "Adding HOL4 rewrite" |
265 |
val th1 = th RS eq_reflection |
|
266 |
val current_rews = HOL4Rewrites.get thy |
|
18921 | 267 |
val new_rews = insert Thm.eq_thm th1 current_rews |
14516 | 268 |
val updated_thy = HOL4Rewrites.put new_rews thy |
269 |
in |
|
18728 | 270 |
(Context.Theory updated_thy,th1) |
14516 | 271 |
end; |
272 |
||
273 |
fun ignore_hol4 bthy bthm thy = |
|
274 |
let |
|
275 |
val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) |
|
276 |
val curmaps = HOL4Maps.get thy |
|
17412 | 277 |
val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps |
14516 | 278 |
val upd_thy = HOL4Maps.put newmaps thy |
279 |
in |
|
280 |
upd_thy |
|
281 |
end |
|
282 |
||
283 |
val opt_get_output_thy = #2 o HOL4Dump.get |
|
284 |
||
285 |
fun get_output_thy thy = |
|
286 |
case #2 (HOL4Dump.get thy) of |
|
287 |
"" => error "No theory file being output" |
|
288 |
| thyname => thyname |
|
289 |
||
290 |
val get_output_dir = #1 o HOL4Dump.get |
|
291 |
||
292 |
fun add_hol4_move bef aft thy = |
|
293 |
let |
|
294 |
val curmoves = HOL4Moves.get thy |
|
17412 | 295 |
val newmoves = Symtab.update_new (bef, aft) curmoves |
14516 | 296 |
in |
297 |
HOL4Moves.put newmoves thy |
|
298 |
end |
|
299 |
||
300 |
fun get_hol4_move bef thy = |
|
17412 | 301 |
Symtab.lookup (HOL4Moves.get thy) bef |
14516 | 302 |
|
303 |
fun follow_name thmname thy = |
|
304 |
let |
|
305 |
val moves = HOL4Moves.get thy |
|
306 |
fun F thmname = |
|
17412 | 307 |
case Symtab.lookup moves thmname of |
15531 | 308 |
SOME name => F name |
309 |
| NONE => thmname |
|
14516 | 310 |
in |
311 |
F thmname |
|
312 |
end |
|
313 |
||
314 |
fun add_hol4_cmove bef aft thy = |
|
315 |
let |
|
316 |
val curmoves = HOL4CMoves.get thy |
|
17412 | 317 |
val newmoves = Symtab.update_new (bef, aft) curmoves |
14516 | 318 |
in |
319 |
HOL4CMoves.put newmoves thy |
|
320 |
end |
|
321 |
||
322 |
fun get_hol4_cmove bef thy = |
|
17412 | 323 |
Symtab.lookup (HOL4CMoves.get thy) bef |
14516 | 324 |
|
325 |
fun follow_cname thmname thy = |
|
326 |
let |
|
327 |
val moves = HOL4CMoves.get thy |
|
328 |
fun F thmname = |
|
17412 | 329 |
case Symtab.lookup moves thmname of |
15531 | 330 |
SOME name => F name |
331 |
| NONE => thmname |
|
14516 | 332 |
in |
333 |
F thmname |
|
334 |
end |
|
335 |
||
336 |
fun add_hol4_mapping bthy bthm isathm thy = |
|
17644 | 337 |
let |
338 |
(* val _ = writeln ("Before follow_name: "^isathm) *) |
|
339 |
val isathm = follow_name isathm thy |
|
340 |
(* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*) |
|
14516 | 341 |
val curmaps = HOL4Maps.get thy |
17412 | 342 |
val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps |
14516 | 343 |
val upd_thy = HOL4Maps.put newmaps thy |
344 |
in |
|
345 |
upd_thy |
|
346 |
end; |
|
347 |
||
348 |
fun get_hol4_type_mapping bthy tycon thy = |
|
349 |
let |
|
350 |
val maps = HOL4TypeMaps.get thy |
|
351 |
in |
|
17412 | 352 |
StringPair.lookup maps (bthy,tycon) |
14516 | 353 |
end |
354 |
||
355 |
fun get_hol4_mapping bthy bthm thy = |
|
356 |
let |
|
357 |
val curmaps = HOL4Maps.get thy |
|
358 |
in |
|
17412 | 359 |
StringPair.lookup curmaps (bthy,bthm) |
14516 | 360 |
end; |
361 |
||
362 |
fun add_hol4_const_mapping bthy bconst internal isaconst thy = |
|
363 |
let |
|
364 |
val thy = case opt_get_output_thy thy of |
|
365 |
"" => thy |
|
366 |
| output_thy => if internal |
|
367 |
then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy |
|
368 |
else thy |
|
369 |
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
|
370 |
val curmaps = HOL4ConstMaps.get thy |
|
17412 | 371 |
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps |
14516 | 372 |
val upd_thy = HOL4ConstMaps.put newmaps thy |
373 |
in |
|
374 |
upd_thy |
|
375 |
end; |
|
376 |
||
377 |
fun add_hol4_const_renaming bthy bconst newname thy = |
|
378 |
let |
|
379 |
val currens = HOL4Rename.get thy |
|
380 |
val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname) |
|
17412 | 381 |
val newrens = StringPair.update_new ((bthy,bconst),newname) currens |
14516 | 382 |
val upd_thy = HOL4Rename.put newrens thy |
383 |
in |
|
384 |
upd_thy |
|
385 |
end; |
|
386 |
||
387 |
fun get_hol4_const_renaming bthy bconst thy = |
|
388 |
let |
|
389 |
val currens = HOL4Rename.get thy |
|
390 |
in |
|
17412 | 391 |
StringPair.lookup currens (bthy,bconst) |
14516 | 392 |
end; |
393 |
||
394 |
fun get_hol4_const_mapping bthy bconst thy = |
|
395 |
let |
|
396 |
val bconst = case get_hol4_const_renaming bthy bconst thy of |
|
15531 | 397 |
SOME name => name |
398 |
| NONE => bconst |
|
14516 | 399 |
val maps = HOL4ConstMaps.get thy |
400 |
in |
|
17412 | 401 |
StringPair.lookup maps (bthy,bconst) |
14516 | 402 |
end |
403 |
||
404 |
fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy = |
|
405 |
let |
|
406 |
val thy = case opt_get_output_thy thy of |
|
407 |
"" => thy |
|
408 |
| output_thy => if internal |
|
409 |
then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy |
|
410 |
else thy |
|
411 |
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
|
412 |
val curmaps = HOL4ConstMaps.get thy |
|
17412 | 413 |
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps |
14516 | 414 |
val upd_thy = HOL4ConstMaps.put newmaps thy |
415 |
in |
|
416 |
upd_thy |
|
417 |
end; |
|
418 |
||
419 |
fun add_hol4_type_mapping bthy bconst internal isaconst thy = |
|
420 |
let |
|
421 |
val curmaps = HOL4TypeMaps.get thy |
|
17322 | 422 |
val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
17412 | 423 |
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps |
424 |
handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in |
|
17322 | 425 |
warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end |
426 |
val upd_thy = HOL4TypeMaps.put newmaps thy |
|
14516 | 427 |
in |
428 |
upd_thy |
|
429 |
end; |
|
430 |
||
431 |
fun add_hol4_pending bthy bthm hth thy = |
|
432 |
let |
|
433 |
val thmname = Sign.full_name (sign_of thy) bthm |
|
434 |
val _ = message ("Add pending " ^ bthy ^ "." ^ bthm) |
|
435 |
val curpend = HOL4Pending.get thy |
|
17412 | 436 |
val newpend = StringPair.update_new ((bthy,bthm),hth) curpend |
14516 | 437 |
val upd_thy = HOL4Pending.put newpend thy |
438 |
val thy' = case opt_get_output_thy upd_thy of |
|
439 |
"" => add_hol4_mapping bthy bthm thmname upd_thy |
|
440 |
| output_thy => |
|
441 |
let |
|
442 |
val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm |
|
443 |
in |
|
444 |
upd_thy |> add_hol4_move thmname new_thmname |
|
445 |
|> add_hol4_mapping bthy bthm new_thmname |
|
446 |
end |
|
447 |
in |
|
448 |
thy' |
|
449 |
end; |
|
450 |
||
451 |
fun get_hol4_theorem thyname thmname thy = |
|
452 |
let |
|
453 |
val isathms = HOL4Thms.get thy |
|
454 |
in |
|
17412 | 455 |
StringPair.lookup isathms (thyname,thmname) |
14516 | 456 |
end |
457 |
||
458 |
fun add_hol4_theorem thyname thmname hth thy = |
|
459 |
let |
|
460 |
val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname) |
|
461 |
val isathms = HOL4Thms.get thy |
|
17412 | 462 |
val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms |
14516 | 463 |
val thy' = HOL4Thms.put isathms' thy |
464 |
in |
|
465 |
thy' |
|
466 |
end |
|
467 |
||
468 |
fun export_hol4_pending thy = |
|
469 |
let |
|
470 |
val rews = HOL4Rewrites.get thy |
|
471 |
val outthy = get_output_thy thy |
|
472 |
fun process (thy,((bthy,bthm),hth as (_,thm))) = |
|
473 |
let |
|
474 |
val sg = sign_of thy |
|
16424 | 475 |
val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm) |
14516 | 476 |
val thm2 = standard thm1 |
18358 | 477 |
val thy2 = PureThy.store_thm ((bthm, thm2), []) thy |> snd |
14516 | 478 |
val thy5 = add_hol4_theorem bthy bthm hth thy2 |
479 |
in |
|
480 |
thy5 |
|
481 |
end |
|
482 |
||
483 |
val pending = HOL4Pending.get thy |
|
484 |
val thy1 = StringPair.foldl process (thy,pending) |
|
485 |
val thy2 = HOL4Pending.put (StringPair.empty) thy1 |
|
486 |
in |
|
487 |
thy2 |
|
488 |
end; |
|
489 |
||
490 |
fun setup_dump (dir,thyname) thy = |
|
15647 | 491 |
HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy |
14516 | 492 |
|
493 |
fun add_dump str thy = |
|
494 |
let |
|
495 |
val (dir,thyname,curdump) = HOL4Dump.get thy |
|
496 |
in |
|
497 |
HOL4Dump.put (dir,thyname,str::curdump) thy |
|
498 |
end |
|
499 |
||
500 |
fun flush_dump thy = |
|
501 |
let |
|
502 |
val (dir,thyname,dumpdata) = HOL4Dump.get thy |
|
503 |
val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir, |
|
504 |
file=thyname ^ ".thy"}) |
|
505 |
val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata) |
|
506 |
val _ = TextIO.closeOut os |
|
507 |
in |
|
508 |
HOL4Dump.put ("","",[]) thy |
|
509 |
end |
|
510 |
||
511 |
fun set_generating_thy thyname thy = |
|
512 |
case HOL4DefThy.get thy of |
|
513 |
NoImport => HOL4DefThy.put (Generating thyname) thy |
|
514 |
| _ => error "Import already in progess" |
|
515 |
||
516 |
fun set_replaying_thy thyname thy = |
|
517 |
case HOL4DefThy.get thy of |
|
518 |
NoImport => HOL4DefThy.put (Replaying thyname) thy |
|
519 |
| _ => error "Import already in progess" |
|
520 |
||
521 |
fun clear_import_thy thy = |
|
522 |
case HOL4DefThy.get thy of |
|
523 |
NoImport => error "No import in progress" |
|
524 |
| _ => HOL4DefThy.put NoImport thy |
|
525 |
||
526 |
fun get_generating_thy thy = |
|
527 |
case HOL4DefThy.get thy of |
|
528 |
Generating thyname => thyname |
|
529 |
| _ => error "No theory being generated" |
|
530 |
||
531 |
fun get_replaying_thy thy = |
|
532 |
case HOL4DefThy.get thy of |
|
533 |
Replaying thyname => thyname |
|
534 |
| _ => error "No theory being replayed" |
|
535 |
||
536 |
fun get_import_thy thy = |
|
537 |
case HOL4DefThy.get thy of |
|
538 |
Replaying thyname => thyname |
|
539 |
| Generating thyname => thyname |
|
540 |
| _ => error "No theory being imported" |
|
541 |
||
542 |
fun should_ignore thyname thy thmname = |
|
543 |
case get_hol4_mapping thyname thmname thy of |
|
15531 | 544 |
SOME NONE => true |
14516 | 545 |
| _ => false |
546 |
||
547 |
val trans_string = |
|
548 |
let |
|
549 |
fun quote s = "\"" ^ s ^ "\"" |
|
550 |
fun F [] = [] |
|
551 |
| F (#"\\" :: cs) = patch #"\\" cs |
|
552 |
| F (#"\"" :: cs) = patch #"\"" cs |
|
553 |
| F (c :: cs) = c :: F cs |
|
554 |
and patch c rest = #"\\" :: c :: F rest |
|
555 |
in |
|
556 |
quote o String.implode o F o String.explode |
|
557 |
end |
|
558 |
||
559 |
fun dump_import_thy thyname thy = |
|
560 |
let |
|
561 |
val output_dir = get_output_dir thy |
|
562 |
val output_thy = get_output_thy thy |
|
17607
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
563 |
val input_thy = Context.theory_name thy |
14516 | 564 |
val import_segment = get_import_segment thy |
565 |
val sg = sign_of thy |
|
566 |
val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir, |
|
567 |
file=thyname ^ ".imp"}) |
|
568 |
fun out s = TextIO.output(os,s) |
|
569 |
val (ignored,mapped) = |
|
570 |
StringPair.foldl (fn ((ign,map),((bthy,bthm),v)) => |
|
571 |
if bthy = thyname |
|
572 |
then (case v of |
|
15531 | 573 |
NONE => (bthm::ign,map) |
574 |
| SOME w => (ign,(bthm,w)::map)) |
|
14516 | 575 |
else (ign,map)) |
576 |
(([],[]),HOL4Maps.get thy) |
|
577 |
val constmaps = |
|
578 |
StringPair.foldl (fn (map,((bthy,bthm),v)) => |
|
579 |
if bthy = thyname |
|
580 |
then (bthm,v)::map |
|
581 |
else map) |
|
582 |
([],HOL4ConstMaps.get thy) |
|
583 |
||
584 |
val constrenames = |
|
585 |
StringPair.foldl (fn (map,((bthy,bthm),v)) => |
|
586 |
if bthy = thyname |
|
587 |
then (bthm,v)::map |
|
588 |
else map) |
|
589 |
([],HOL4Rename.get thy) |
|
590 |
||
591 |
val typemaps = |
|
592 |
StringPair.foldl (fn (map,((bthy,bthm),v)) => |
|
593 |
if bthy = thyname |
|
594 |
then (bthm,v)::map |
|
595 |
else map) |
|
596 |
([],HOL4TypeMaps.get thy) |
|
597 |
||
598 |
val defmaps = |
|
599 |
StringPair.foldl (fn (map,((bthy,bthm),v)) => |
|
600 |
if bthy = thyname |
|
601 |
then (bthm,v)::map |
|
602 |
else map) |
|
603 |
([],HOL4DefMaps.get thy) |
|
604 |
||
605 |
fun new_name internal isa = |
|
606 |
if internal |
|
607 |
then |
|
608 |
let |
|
609 |
val paths = NameSpace.unpack isa |
|
15570 | 610 |
val i = Library.drop(length paths - 2,paths) |
14516 | 611 |
in |
612 |
case i of |
|
613 |
[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con |
|
614 |
| _ => error "hol4rews.dump internal error" |
|
615 |
end |
|
616 |
else |
|
617 |
isa |
|
618 |
||
619 |
val _ = out "import\n\n" |
|
620 |
||
621 |
val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n") |
|
622 |
val _ = if null defmaps |
|
623 |
then () |
|
624 |
else out "def_maps" |
|
625 |
val _ = app (fn (hol,isa) => |
|
626 |
out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps |
|
627 |
val _ = if null defmaps |
|
628 |
then () |
|
629 |
else out "\n\n" |
|
630 |
||
631 |
val _ = if null typemaps |
|
632 |
then () |
|
633 |
else out "type_maps" |
|
634 |
val _ = app (fn (hol,(internal,isa)) => |
|
635 |
out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps |
|
636 |
val _ = if null typemaps |
|
637 |
then () |
|
638 |
else out "\n\n" |
|
639 |
||
640 |
val _ = if null constmaps |
|
641 |
then () |
|
642 |
else out "const_maps" |
|
643 |
val _ = app (fn (hol,(internal,isa,opt_ty)) => |
|
644 |
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); |
|
645 |
case opt_ty of |
|
15531 | 646 |
SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"") |
647 |
| NONE => ())) constmaps |
|
14516 | 648 |
val _ = if null constmaps |
649 |
then () |
|
650 |
else out "\n\n" |
|
651 |
||
652 |
val _ = if null constrenames |
|
653 |
then () |
|
654 |
else out "const_renames" |
|
655 |
val _ = app (fn (old,new) => |
|
656 |
out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames |
|
657 |
val _ = if null constrenames |
|
658 |
then () |
|
659 |
else out "\n\n" |
|
660 |
||
17607
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
661 |
fun gen2replay in_thy out_thy s = |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
662 |
let |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
663 |
val ss = NameSpace.unpack s |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
664 |
in |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
665 |
if (hd ss = in_thy) then |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
666 |
NameSpace.pack (out_thy::(tl ss)) |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
667 |
else |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
668 |
s |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
669 |
end |
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
670 |
|
14516 | 671 |
val _ = if null mapped |
672 |
then () |
|
673 |
else out "thm_maps" |
|
17607
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
674 |
val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped |
14516 | 675 |
val _ = if null mapped |
676 |
then () |
|
677 |
else out "\n\n" |
|
678 |
||
679 |
val _ = if null ignored |
|
680 |
then () |
|
681 |
else out "ignore_thms" |
|
682 |
val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored |
|
683 |
val _ = if null ignored |
|
684 |
then () |
|
685 |
else out "\n\n" |
|
686 |
||
687 |
val _ = out "end\n" |
|
688 |
val _ = TextIO.closeOut os |
|
689 |
in |
|
690 |
thy |
|
691 |
end |
|
692 |
||
693 |
fun set_used_names names thy = |
|
694 |
let |
|
695 |
val unames = HOL4UNames.get thy |
|
696 |
in |
|
697 |
case unames of |
|
698 |
[] => HOL4UNames.put names thy |
|
699 |
| _ => error "hol4rews.set_used_names called on initialized data!" |
|
700 |
end |
|
701 |
||
702 |
val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty |
|
703 |
||
704 |
fun get_defmap thyname const thy = |
|
705 |
let |
|
706 |
val maps = HOL4DefMaps.get thy |
|
707 |
in |
|
17412 | 708 |
StringPair.lookup maps (thyname,const) |
14516 | 709 |
end |
710 |
||
711 |
fun add_defmap thyname const defname thy = |
|
712 |
let |
|
713 |
val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname) |
|
714 |
val maps = HOL4DefMaps.get thy |
|
17412 | 715 |
val maps' = StringPair.update_new ((thyname,const),defname) maps |
14516 | 716 |
val thy' = HOL4DefMaps.put maps' thy |
717 |
in |
|
718 |
thy' |
|
719 |
end |
|
720 |
||
721 |
fun get_defname thyname name thy = |
|
722 |
let |
|
723 |
val maps = HOL4DefMaps.get thy |
|
724 |
fun F dname = (dname,add_defmap thyname name dname thy) |
|
725 |
in |
|
17412 | 726 |
case StringPair.lookup maps (thyname,name) of |
15531 | 727 |
SOME thmname => (thmname,thy) |
728 |
| NONE => |
|
14516 | 729 |
let |
730 |
val used = HOL4UNames.get thy |
|
731 |
val defname = def_name name |
|
732 |
val pdefname = name ^ "_primdef" |
|
733 |
in |
|
734 |
if not (defname mem used) |
|
735 |
then F defname (* name_def *) |
|
736 |
else if not (pdefname mem used) |
|
737 |
then F pdefname (* name_primdef *) |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
18921
diff
changeset
|
738 |
else F (Name.variant used pdefname) (* last resort *) |
14516 | 739 |
end |
740 |
end |
|
741 |
||
742 |
local |
|
743 |
fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x |
|
744 |
| handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x |
|
745 |
| handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x |
|
746 |
| handle_meta [x] = Appl[Constant "Trueprop",x] |
|
14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
747 |
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" |
14516 | 748 |
in |
749 |
val smarter_trueprop_parsing = [("Trueprop",handle_meta)] |
|
750 |
end |
|
751 |
||
752 |
local |
|
753 |
fun initial_maps thy = |
|
754 |
thy |> add_hol4_type_mapping "min" "bool" false "bool" |
|
755 |
|> add_hol4_type_mapping "min" "fun" false "fun" |
|
756 |
|> add_hol4_type_mapping "min" "ind" false "Nat.ind" |
|
757 |
|> add_hol4_const_mapping "min" "=" false "op =" |
|
758 |
|> add_hol4_const_mapping "min" "==>" false "op -->" |
|
759 |
|> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps" |
|
760 |
in |
|
761 |
val hol4_setup = |
|
18708 | 762 |
HOL4Rewrites.init #> |
763 |
HOL4Maps.init #> |
|
764 |
HOL4UNames.init #> |
|
765 |
HOL4DefMaps.init #> |
|
766 |
HOL4Moves.init #> |
|
767 |
HOL4CMoves.init #> |
|
768 |
HOL4ConstMaps.init #> |
|
769 |
HOL4Rename.init #> |
|
770 |
HOL4TypeMaps.init #> |
|
771 |
HOL4Pending.init #> |
|
772 |
HOL4Thms.init #> |
|
773 |
HOL4Dump.init #> |
|
774 |
HOL4DefThy.init #> |
|
775 |
HOL4Imports.init #> |
|
776 |
ImportSegment.init #> |
|
777 |
initial_maps #> |
|
778 |
Attrib.add_attributes |
|
18728 | 779 |
[("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")] |
14516 | 780 |
end |