author | wenzelm |
Mon, 02 May 2011 16:33:21 +0200 | |
changeset 42616 | 92715b528e78 |
parent 42224 | 578a51fae383 |
child 43324 | 2b47822868e4 |
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 |
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 |
|
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
30528
diff
changeset
|
5 |
structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord); |
14516 | 6 |
|
7 |
type holthm = (term * term) list * thm |
|
8 |
||
9 |
datatype ImportStatus = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
10 |
NoImport |
14516 | 11 |
| Generating of string |
12 |
| Replaying of string |
|
13 |
||
33522 | 14 |
structure HOL4DefThy = Theory_Data |
22846 | 15 |
( |
16 |
type T = ImportStatus |
|
17 |
val empty = NoImport |
|
18 |
val extend = I |
|
33522 | 19 |
fun merge (NoImport, NoImport) = NoImport |
20 |
| merge _ = (warning "Import status set during merge"; NoImport) |
|
22846 | 21 |
) |
14516 | 22 |
|
33522 | 23 |
structure ImportSegment = Theory_Data |
22846 | 24 |
( |
25 |
type T = string |
|
26 |
val empty = "" |
|
27 |
val extend = I |
|
33522 | 28 |
fun merge ("",arg) = arg |
29 |
| merge (arg,"") = arg |
|
30 |
| merge (s1,s2) = |
|
22846 | 31 |
if s1 = s2 |
32 |
then s1 |
|
33 |
else error "Trying to merge two different import segments" |
|
34 |
) |
|
14516 | 35 |
|
36 |
val get_import_segment = ImportSegment.get |
|
37 |
val set_import_segment = ImportSegment.put |
|
38 |
||
33522 | 39 |
structure HOL4UNames = Theory_Data |
22846 | 40 |
( |
41 |
type T = string list |
|
42 |
val empty = [] |
|
43 |
val extend = I |
|
33522 | 44 |
fun merge ([], []) = [] |
45 |
| merge _ = error "Used names not empty during merge" |
|
22846 | 46 |
) |
14516 | 47 |
|
33522 | 48 |
structure HOL4Dump = Theory_Data |
22846 | 49 |
( |
50 |
type T = string * string * string list |
|
51 |
val empty = ("","",[]) |
|
52 |
val extend = I |
|
33522 | 53 |
fun merge (("","",[]),("","",[])) = ("","",[]) |
54 |
| merge _ = error "Dump data not empty during merge" |
|
22846 | 55 |
) |
14516 | 56 |
|
33522 | 57 |
structure HOL4Moves = Theory_Data |
22846 | 58 |
( |
59 |
type T = string Symtab.table |
|
60 |
val empty = Symtab.empty |
|
61 |
val extend = I |
|
33522 | 62 |
fun merge data = Symtab.merge (K true) data |
22846 | 63 |
) |
14516 | 64 |
|
33522 | 65 |
structure HOL4Imports = Theory_Data |
22846 | 66 |
( |
67 |
type T = string Symtab.table |
|
68 |
val empty = Symtab.empty |
|
69 |
val extend = I |
|
33522 | 70 |
fun merge data = Symtab.merge (K true) data |
22846 | 71 |
) |
14516 | 72 |
|
73 |
fun get_segment2 thyname thy = |
|
17412 | 74 |
Symtab.lookup (HOL4Imports.get thy) thyname |
14516 | 75 |
|
76 |
fun set_segment thyname segname thy = |
|
77 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
78 |
val imps = HOL4Imports.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
79 |
val imps' = Symtab.update_new (thyname,segname) imps |
14516 | 80 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
81 |
HOL4Imports.put imps' thy |
14516 | 82 |
end |
83 |
||
33522 | 84 |
structure HOL4CMoves = Theory_Data |
22846 | 85 |
( |
86 |
type T = string Symtab.table |
|
87 |
val empty = Symtab.empty |
|
88 |
val extend = I |
|
33522 | 89 |
fun merge data = Symtab.merge (K true) data |
22846 | 90 |
) |
14516 | 91 |
|
33522 | 92 |
structure HOL4Maps = Theory_Data |
22846 | 93 |
( |
33522 | 94 |
type T = string option StringPair.table |
22846 | 95 |
val empty = StringPair.empty |
96 |
val extend = I |
|
33522 | 97 |
fun merge data = StringPair.merge (K true) data |
22846 | 98 |
) |
14516 | 99 |
|
33522 | 100 |
structure HOL4Thms = Theory_Data |
22846 | 101 |
( |
102 |
type T = holthm StringPair.table |
|
103 |
val empty = StringPair.empty |
|
104 |
val extend = I |
|
33522 | 105 |
fun merge data = StringPair.merge (K true) data |
22846 | 106 |
) |
14516 | 107 |
|
33522 | 108 |
structure HOL4ConstMaps = Theory_Data |
22846 | 109 |
( |
110 |
type T = (bool * string * typ option) StringPair.table |
|
111 |
val empty = StringPair.empty |
|
112 |
val extend = I |
|
33522 | 113 |
fun merge data = StringPair.merge (K true) data |
22846 | 114 |
) |
14516 | 115 |
|
33522 | 116 |
structure HOL4Rename = Theory_Data |
22846 | 117 |
( |
118 |
type T = string StringPair.table |
|
119 |
val empty = StringPair.empty |
|
120 |
val extend = I |
|
33522 | 121 |
fun merge data = StringPair.merge (K true) data |
22846 | 122 |
) |
14516 | 123 |
|
33522 | 124 |
structure HOL4DefMaps = Theory_Data |
22846 | 125 |
( |
126 |
type T = string StringPair.table |
|
127 |
val empty = StringPair.empty |
|
128 |
val extend = I |
|
33522 | 129 |
fun merge data = StringPair.merge (K true) data |
22846 | 130 |
) |
14516 | 131 |
|
33522 | 132 |
structure HOL4TypeMaps = Theory_Data |
22846 | 133 |
( |
134 |
type T = (bool * string) StringPair.table |
|
135 |
val empty = StringPair.empty |
|
136 |
val extend = I |
|
33522 | 137 |
fun merge data = StringPair.merge (K true) data |
22846 | 138 |
) |
14516 | 139 |
|
33522 | 140 |
structure HOL4Pending = Theory_Data |
22846 | 141 |
( |
142 |
type T = ((term * term) list * thm) StringPair.table |
|
143 |
val empty = StringPair.empty |
|
144 |
val extend = I |
|
33522 | 145 |
fun merge data = StringPair.merge (K true) data |
22846 | 146 |
) |
14516 | 147 |
|
33522 | 148 |
structure HOL4Rewrites = Theory_Data |
22846 | 149 |
( |
150 |
type T = thm list |
|
151 |
val empty = [] |
|
152 |
val extend = I |
|
33522 | 153 |
val merge = Thm.merge_thms |
22846 | 154 |
) |
14516 | 155 |
|
32740 | 156 |
val hol4_debug = Unsynchronized.ref false |
14516 | 157 |
fun message s = if !hol4_debug then writeln s else () |
158 |
||
20897 | 159 |
fun add_hol4_rewrite (Context.Theory thy, th) = |
14516 | 160 |
let |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
161 |
val _ = message "Adding HOL4 rewrite" |
39159 | 162 |
val th1 = th RS @{thm eq_reflection} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
163 |
val current_rews = HOL4Rewrites.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
164 |
val new_rews = insert Thm.eq_thm th1 current_rews |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
165 |
val updated_thy = HOL4Rewrites.put new_rews thy |
14516 | 166 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
167 |
(Context.Theory updated_thy,th1) |
20897 | 168 |
end |
21546 | 169 |
| add_hol4_rewrite (context, th) = (context, th RS eq_reflection); |
14516 | 170 |
|
171 |
fun ignore_hol4 bthy bthm thy = |
|
172 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
173 |
val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
174 |
val curmaps = HOL4Maps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
175 |
val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
176 |
val upd_thy = HOL4Maps.put newmaps thy |
14516 | 177 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
178 |
upd_thy |
14516 | 179 |
end |
180 |
||
181 |
val opt_get_output_thy = #2 o HOL4Dump.get |
|
182 |
||
183 |
fun get_output_thy thy = |
|
184 |
case #2 (HOL4Dump.get thy) of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
185 |
"" => error "No theory file being output" |
14516 | 186 |
| thyname => thyname |
187 |
||
188 |
val get_output_dir = #1 o HOL4Dump.get |
|
189 |
||
190 |
fun add_hol4_move bef aft thy = |
|
191 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
192 |
val curmoves = HOL4Moves.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
193 |
val newmoves = Symtab.update_new (bef, aft) curmoves |
14516 | 194 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
195 |
HOL4Moves.put newmoves thy |
14516 | 196 |
end |
197 |
||
198 |
fun get_hol4_move bef thy = |
|
17412 | 199 |
Symtab.lookup (HOL4Moves.get thy) bef |
14516 | 200 |
|
201 |
fun follow_name thmname thy = |
|
202 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
203 |
val moves = HOL4Moves.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
204 |
fun F thmname = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
205 |
case Symtab.lookup moves thmname of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
206 |
SOME name => F name |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
207 |
| NONE => thmname |
14516 | 208 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
209 |
F thmname |
14516 | 210 |
end |
211 |
||
212 |
fun add_hol4_cmove bef aft thy = |
|
213 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
214 |
val curmoves = HOL4CMoves.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
215 |
val newmoves = Symtab.update_new (bef, aft) curmoves |
14516 | 216 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
217 |
HOL4CMoves.put newmoves thy |
14516 | 218 |
end |
219 |
||
220 |
fun get_hol4_cmove bef thy = |
|
17412 | 221 |
Symtab.lookup (HOL4CMoves.get thy) bef |
14516 | 222 |
|
223 |
fun follow_cname thmname thy = |
|
224 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
225 |
val moves = HOL4CMoves.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
226 |
fun F thmname = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
227 |
case Symtab.lookup moves thmname of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
228 |
SOME name => F name |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
229 |
| NONE => thmname |
14516 | 230 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
231 |
F thmname |
14516 | 232 |
end |
233 |
||
234 |
fun add_hol4_mapping bthy bthm isathm thy = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
235 |
let |
17644 | 236 |
(* val _ = writeln ("Before follow_name: "^isathm) *) |
237 |
val isathm = follow_name isathm thy |
|
238 |
(* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
239 |
val curmaps = HOL4Maps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
240 |
val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
241 |
val upd_thy = HOL4Maps.put newmaps thy |
14516 | 242 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
243 |
upd_thy |
14516 | 244 |
end; |
245 |
||
246 |
fun get_hol4_type_mapping bthy tycon thy = |
|
247 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
248 |
val maps = HOL4TypeMaps.get thy |
14516 | 249 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
250 |
StringPair.lookup maps (bthy,tycon) |
14516 | 251 |
end |
252 |
||
253 |
fun get_hol4_mapping bthy bthm thy = |
|
254 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
255 |
val curmaps = HOL4Maps.get thy |
14516 | 256 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
257 |
StringPair.lookup curmaps (bthy,bthm) |
14516 | 258 |
end; |
259 |
||
260 |
fun add_hol4_const_mapping bthy bconst internal isaconst thy = |
|
261 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
262 |
val thy = case opt_get_output_thy thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
263 |
"" => thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
264 |
| output_thy => if internal |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
265 |
then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
266 |
else thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
267 |
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
268 |
val curmaps = HOL4ConstMaps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
269 |
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
270 |
val upd_thy = HOL4ConstMaps.put newmaps thy |
14516 | 271 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
272 |
upd_thy |
14516 | 273 |
end; |
274 |
||
275 |
fun add_hol4_const_renaming bthy bconst newname thy = |
|
276 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
277 |
val currens = HOL4Rename.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
278 |
val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
279 |
val newrens = StringPair.update_new ((bthy,bconst),newname) currens |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
280 |
val upd_thy = HOL4Rename.put newrens thy |
14516 | 281 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
282 |
upd_thy |
14516 | 283 |
end; |
284 |
||
285 |
fun get_hol4_const_renaming bthy bconst thy = |
|
286 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
287 |
val currens = HOL4Rename.get thy |
14516 | 288 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
289 |
StringPair.lookup currens (bthy,bconst) |
14516 | 290 |
end; |
291 |
||
292 |
fun get_hol4_const_mapping bthy bconst thy = |
|
293 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
294 |
val bconst = case get_hol4_const_renaming bthy bconst thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
295 |
SOME name => name |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
296 |
| NONE => bconst |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
297 |
val maps = HOL4ConstMaps.get thy |
14516 | 298 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
299 |
StringPair.lookup maps (bthy,bconst) |
14516 | 300 |
end |
301 |
||
302 |
fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy = |
|
303 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
304 |
val thy = case opt_get_output_thy thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
305 |
"" => thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
306 |
| output_thy => if internal |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
307 |
then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
308 |
else thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
309 |
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
310 |
val curmaps = HOL4ConstMaps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
311 |
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
312 |
val upd_thy = HOL4ConstMaps.put newmaps thy |
14516 | 313 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
314 |
upd_thy |
14516 | 315 |
end; |
316 |
||
317 |
fun add_hol4_type_mapping bthy bconst internal isaconst thy = |
|
318 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
319 |
val curmaps = HOL4TypeMaps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
320 |
val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
321 |
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps |
41522
42d13d00ccfb
more FIXMEs concerning bad catch-all exception handlers;
wenzelm
parents:
39557
diff
changeset
|
322 |
(* FIXME avoid handle x *) |
17412 | 323 |
handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in |
17322 | 324 |
warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end |
325 |
val upd_thy = HOL4TypeMaps.put newmaps thy |
|
14516 | 326 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
327 |
upd_thy |
14516 | 328 |
end; |
329 |
||
330 |
fun add_hol4_pending bthy bthm hth thy = |
|
331 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
332 |
val thmname = Sign.full_bname thy bthm |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
333 |
val _ = message ("Add pending " ^ bthy ^ "." ^ bthm) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
334 |
val curpend = HOL4Pending.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
335 |
val newpend = StringPair.update_new ((bthy,bthm),hth) curpend |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
336 |
val upd_thy = HOL4Pending.put newpend thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
337 |
val thy' = case opt_get_output_thy upd_thy of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
338 |
"" => add_hol4_mapping bthy bthm thmname upd_thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
339 |
| output_thy => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
340 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
341 |
val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
342 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
343 |
upd_thy |> add_hol4_move thmname new_thmname |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
344 |
|> add_hol4_mapping bthy bthm new_thmname |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
345 |
end |
14516 | 346 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
347 |
thy' |
14516 | 348 |
end; |
349 |
||
350 |
fun get_hol4_theorem thyname thmname thy = |
|
21056 | 351 |
let |
352 |
val isathms = HOL4Thms.get thy |
|
353 |
in |
|
354 |
StringPair.lookup isathms (thyname,thmname) |
|
355 |
end; |
|
14516 | 356 |
|
21056 | 357 |
fun add_hol4_theorem thyname thmname hth = |
358 |
let |
|
359 |
val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname) |
|
360 |
in |
|
361 |
HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth)) |
|
362 |
end; |
|
14516 | 363 |
|
364 |
fun export_hol4_pending thy = |
|
21056 | 365 |
let |
366 |
val rews = HOL4Rewrites.get thy; |
|
367 |
val pending = HOL4Pending.get thy; |
|
368 |
fun process ((bthy,bthm), hth as (_,thm)) thy = |
|
369 |
let |
|
370 |
val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm); |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33955
diff
changeset
|
371 |
val thm2 = Drule.export_without_context thm1; |
21056 | 372 |
in |
373 |
thy |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39159
diff
changeset
|
374 |
|> Global_Theory.store_thm (Binding.name bthm, thm2) |
21056 | 375 |
|> snd |
376 |
|> add_hol4_theorem bthy bthm hth |
|
377 |
end; |
|
378 |
in |
|
379 |
thy |
|
380 |
|> StringPair.fold process pending |
|
381 |
|> HOL4Pending.put StringPair.empty |
|
382 |
end; |
|
14516 | 383 |
|
384 |
fun setup_dump (dir,thyname) thy = |
|
15647 | 385 |
HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy |
14516 | 386 |
|
387 |
fun add_dump str thy = |
|
388 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
389 |
val (dir,thyname,curdump) = HOL4Dump.get thy |
14516 | 390 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
391 |
HOL4Dump.put (dir,thyname,str::curdump) thy |
14516 | 392 |
end |
393 |
||
394 |
fun flush_dump thy = |
|
395 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
396 |
val (dir,thyname,dumpdata) = HOL4Dump.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
397 |
val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
398 |
file=thyname ^ ".thy"}) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
399 |
val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
400 |
val _ = TextIO.closeOut os |
14516 | 401 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
402 |
HOL4Dump.put ("","",[]) thy |
14516 | 403 |
end |
404 |
||
405 |
fun set_generating_thy thyname thy = |
|
406 |
case HOL4DefThy.get thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
407 |
NoImport => HOL4DefThy.put (Generating thyname) thy |
14516 | 408 |
| _ => error "Import already in progess" |
409 |
||
410 |
fun set_replaying_thy thyname thy = |
|
411 |
case HOL4DefThy.get thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
412 |
NoImport => HOL4DefThy.put (Replaying thyname) thy |
14516 | 413 |
| _ => error "Import already in progess" |
414 |
||
415 |
fun clear_import_thy thy = |
|
416 |
case HOL4DefThy.get thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
417 |
NoImport => error "No import in progress" |
14516 | 418 |
| _ => HOL4DefThy.put NoImport thy |
419 |
||
420 |
fun get_generating_thy thy = |
|
421 |
case HOL4DefThy.get thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
422 |
Generating thyname => thyname |
14516 | 423 |
| _ => error "No theory being generated" |
424 |
||
425 |
fun get_replaying_thy thy = |
|
426 |
case HOL4DefThy.get thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
427 |
Replaying thyname => thyname |
14516 | 428 |
| _ => error "No theory being replayed" |
429 |
||
430 |
fun get_import_thy thy = |
|
431 |
case HOL4DefThy.get thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
432 |
Replaying thyname => thyname |
14516 | 433 |
| Generating thyname => thyname |
434 |
| _ => error "No theory being imported" |
|
435 |
||
436 |
fun should_ignore thyname thy thmname = |
|
437 |
case get_hol4_mapping thyname thmname thy of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
438 |
SOME NONE => true |
14516 | 439 |
| _ => false |
440 |
||
441 |
val trans_string = |
|
442 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
443 |
fun quote s = "\"" ^ s ^ "\"" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
444 |
fun F [] = [] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
445 |
| F (#"\\" :: cs) = patch #"\\" cs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
446 |
| F (#"\"" :: cs) = patch #"\"" cs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
447 |
| F (c :: cs) = c :: F cs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
448 |
and patch c rest = #"\\" :: c :: F rest |
14516 | 449 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
450 |
quote o String.implode o F o String.explode |
14516 | 451 |
end |
452 |
||
453 |
fun dump_import_thy thyname thy = |
|
454 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
455 |
val output_dir = get_output_dir thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
456 |
val output_thy = get_output_thy thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
457 |
val input_thy = Context.theory_name thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
458 |
val import_segment = get_import_segment thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
459 |
val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
460 |
file=thyname ^ ".imp"}) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
461 |
fun out s = TextIO.output(os,s) |
21056 | 462 |
val (ignored, mapped) = StringPair.fold |
463 |
(fn ((bthy, bthm), v) => fn (ign, map) => |
|
464 |
if bthy = thyname |
|
465 |
then case v |
|
466 |
of NONE => (bthm :: ign, map) |
|
467 |
| SOME w => (ign, (bthm, w) :: map) |
|
468 |
else (ign, map)) (HOL4Maps.get thy) ([],[]); |
|
469 |
fun mk init = StringPair.fold |
|
470 |
(fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init []; |
|
471 |
val constmaps = mk (HOL4ConstMaps.get thy); |
|
472 |
val constrenames = mk (HOL4Rename.get thy); |
|
473 |
val typemaps = mk (HOL4TypeMaps.get thy); |
|
474 |
val defmaps = mk (HOL4DefMaps.get thy); |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
475 |
fun new_name internal isa = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
476 |
if internal |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
477 |
then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
478 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
479 |
val paths = Long_Name.explode isa |
33955 | 480 |
val i = drop (length paths - 2) paths |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
481 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
482 |
case i of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
483 |
[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
484 |
| _ => error "hol4rews.dump internal error" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
485 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
486 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
487 |
isa |
14516 | 488 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
489 |
val _ = out "import\n\n" |
14516 | 490 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
491 |
val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
492 |
val _ = if null defmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
493 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
494 |
else out "def_maps" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
495 |
val _ = app (fn (hol,isa) => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
496 |
out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
497 |
val _ = if null defmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
498 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
499 |
else out "\n\n" |
14516 | 500 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
501 |
val _ = if null typemaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
502 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
503 |
else out "type_maps" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
504 |
val _ = app (fn (hol,(internal,isa)) => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
505 |
out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
506 |
val _ = if null typemaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
507 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
508 |
else out "\n\n" |
14516 | 509 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
510 |
val _ = if null constmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
511 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
512 |
else out "const_maps" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
513 |
val _ = app (fn (hol,(internal,isa,opt_ty)) => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
514 |
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
515 |
case opt_ty of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
516 |
SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
517 |
| NONE => ())) constmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
518 |
val _ = if null constmaps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
519 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
520 |
else out "\n\n" |
14516 | 521 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
522 |
val _ = if null constrenames |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
523 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
524 |
else out "const_renames" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
525 |
val _ = app (fn (old,new) => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
526 |
out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
527 |
val _ = if null constrenames |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
528 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
529 |
else out "\n\n" |
14516 | 530 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
531 |
fun gen2replay in_thy out_thy s = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
532 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
533 |
val ss = Long_Name.explode s |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
534 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
535 |
if (hd ss = in_thy) then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
536 |
Long_Name.implode (out_thy::(tl ss)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
537 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
538 |
s |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
539 |
end |
17607
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17412
diff
changeset
|
540 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
541 |
val _ = if null mapped |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
542 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
543 |
else out "thm_maps" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
544 |
val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
545 |
val _ = if null mapped |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
546 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
547 |
else out "\n\n" |
14516 | 548 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
549 |
val _ = if null ignored |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
550 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
551 |
else out "ignore_thms" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
552 |
val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
553 |
val _ = if null ignored |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
554 |
then () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
555 |
else out "\n\n" |
14516 | 556 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
557 |
val _ = out "end\n" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
558 |
val _ = TextIO.closeOut os |
14516 | 559 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
560 |
thy |
14516 | 561 |
end |
562 |
||
563 |
fun set_used_names names thy = |
|
564 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
565 |
val unames = HOL4UNames.get thy |
14516 | 566 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
567 |
case unames of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
568 |
[] => HOL4UNames.put names thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
569 |
| _ => error "hol4rews.set_used_names called on initialized data!" |
14516 | 570 |
end |
571 |
||
22846 | 572 |
val clear_used_names = HOL4UNames.put []; |
14516 | 573 |
|
574 |
fun get_defmap thyname const thy = |
|
575 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
576 |
val maps = HOL4DefMaps.get thy |
14516 | 577 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
578 |
StringPair.lookup maps (thyname,const) |
14516 | 579 |
end |
580 |
||
581 |
fun add_defmap thyname const defname thy = |
|
582 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
583 |
val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
584 |
val maps = HOL4DefMaps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
585 |
val maps' = StringPair.update_new ((thyname,const),defname) maps |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
586 |
val thy' = HOL4DefMaps.put maps' thy |
14516 | 587 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
588 |
thy' |
14516 | 589 |
end |
590 |
||
591 |
fun get_defname thyname name thy = |
|
592 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
593 |
val maps = HOL4DefMaps.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
594 |
fun F dname = (dname,add_defmap thyname name dname thy) |
14516 | 595 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
596 |
case StringPair.lookup maps (thyname,name) of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
597 |
SOME thmname => (thmname,thy) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
598 |
| NONE => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
599 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
600 |
val used = HOL4UNames.get thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
601 |
val defname = Thm.def_name name |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
602 |
val pdefname = name ^ "_primdef" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
603 |
in |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35250
diff
changeset
|
604 |
if not (member (op =) used defname) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
605 |
then F defname (* name_def *) |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35250
diff
changeset
|
606 |
else if not (member (op =) used pdefname) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
607 |
then F pdefname (* name_primdef *) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
608 |
else F (Name.variant used pdefname) (* last resort *) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
609 |
end |
14516 | 610 |
end |
611 |
||
612 |
local |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41522
diff
changeset
|
613 |
fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41522
diff
changeset
|
614 |
| handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41522
diff
changeset
|
615 |
| handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41522
diff
changeset
|
616 |
| handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x] |
14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset
|
617 |
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" |
14516 | 618 |
in |
35250 | 619 |
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)] |
14516 | 620 |
end |
621 |
||
622 |
local |
|
623 |
fun initial_maps thy = |
|
38551 | 624 |
thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
625 |
|> add_hol4_type_mapping "min" "fun" false "fun" |
38551 | 626 |
|> add_hol4_type_mapping "min" "ind" false @{type_name ind} |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38786
diff
changeset
|
627 |
|> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq} |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38556
diff
changeset
|
628 |
|> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies} |
38551 | 629 |
|> add_hol4_const_mapping "min" "@" false @{const_name "Eps"} |
14516 | 630 |
in |
631 |
val hol4_setup = |
|
18708 | 632 |
initial_maps #> |
30528 | 633 |
Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule" |
634 |
||
14516 | 635 |
end |