author | haftmann |
Fri, 17 Mar 2006 14:19:24 +0100 | |
changeset 19280 | 5091dc43817b |
parent 19253 | f3ce97b5661a |
child 19283 | 88172041c084 |
permissions | -rw-r--r-- |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
1 |
(* Title: Pure/Tools/codegen_package.ML |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
2 |
ID: $Id$ |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
4 |
|
18217 | 5 |
Code generator from Isabelle theories to |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
6 |
intermediate language ("Thin-gol"). |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
7 |
*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
8 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
9 |
signature CODEGEN_PACKAGE = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
10 |
sig |
18454 | 11 |
type auxtab; |
18702 | 12 |
type eqextr = theory -> auxtab |
19008 | 13 |
-> string * typ -> (thm list * typ) option; |
14 |
type eqextr_default = theory -> auxtab |
|
15 |
-> string * typ -> ((thm list * term option) * typ) option; |
|
18702 | 16 |
type appgen = theory -> auxtab |
18756 | 17 |
-> (string * typ) * term list -> CodegenThingol.transact |
18 |
-> CodegenThingol.iexpr * CodegenThingol.transact; |
|
18702 | 19 |
|
18516 | 20 |
val add_appconst: string * ((int * int) * appgen) -> theory -> theory; |
18517 | 21 |
val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory; |
18702 | 22 |
val add_eqextr: string * eqextr -> theory -> theory; |
19008 | 23 |
val add_eqextr_default: string * eqextr_default -> theory -> theory; |
18963 | 24 |
val add_prim_class: xstring -> (string * string) |
18517 | 25 |
-> theory -> theory; |
18963 | 26 |
val add_prim_tyco: xstring -> (string * string) |
18517 | 27 |
-> theory -> theory; |
19136 | 28 |
val add_prim_const: xstring -> (string * string) |
18517 | 29 |
-> theory -> theory; |
18963 | 30 |
val add_prim_i: string -> (string * CodegenThingol.prim list) |
18517 | 31 |
-> theory -> theory; |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
32 |
val add_pretty_list: string -> string -> string * (int * string) |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
33 |
-> theory -> theory; |
18217 | 34 |
val add_alias: string * string -> theory -> theory; |
18455 | 35 |
val set_get_all_datatype_cons : (theory -> (string * string) list) |
18454 | 36 |
-> theory -> theory; |
18963 | 37 |
val set_get_datatype: (theory -> string -> ((string * sort) list * (string * typ list) list) option) |
38 |
-> theory -> theory; |
|
18702 | 39 |
val set_int_tyco: string -> theory -> theory; |
18217 | 40 |
|
19150 | 41 |
val codegen_term: term -> theory -> CodegenThingol.iexpr * theory; |
19136 | 42 |
val is_dtcon: string -> bool; |
19150 | 43 |
val consts_of_idfs: theory -> string list -> (string * typ) list; |
44 |
val idfs_of_consts: theory -> (string * typ) list -> string list; |
|
45 |
val get_root_module: theory -> CodegenThingol.module; |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
46 |
val get_ml_fun_datatype: theory -> (string -> string) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
47 |
-> ((string * CodegenThingol.funn) list -> Pretty.T) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
48 |
* ((string * CodegenThingol.datatyp) list -> Pretty.T); |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
49 |
|
18702 | 50 |
val appgen_default: appgen; |
18335 | 51 |
val appgen_let: (int -> term -> term list * term) |
52 |
-> appgen; |
|
53 |
val appgen_split: (int -> term -> term list * term) |
|
54 |
-> appgen; |
|
18915 | 55 |
val appgen_number_of: (term -> term) -> (theory -> term -> IntInf.int) -> string -> string |
18335 | 56 |
-> appgen; |
19038 | 57 |
val appgen_wfrec: appgen; |
19008 | 58 |
val eqextr_eq: (theory -> string -> thm list) -> term |
59 |
-> eqextr_default; |
|
18702 | 60 |
val add_case_const: (theory -> string -> (string * int) list option) -> xstring |
18517 | 61 |
-> theory -> theory; |
18702 | 62 |
val add_case_const_i: (theory -> string -> (string * int) list option) -> string |
18517 | 63 |
-> theory -> theory; |
18217 | 64 |
|
19008 | 65 |
val print_code: theory -> unit; |
18454 | 66 |
val rename_inconsistent: theory -> theory; |
18517 | 67 |
val ensure_datatype_case_consts: (theory -> string list) |
68 |
-> (theory -> string -> (string * int) list option) |
|
69 |
-> theory -> theory; |
|
18515 | 70 |
|
71 |
(*debugging purpose only*) |
|
18454 | 72 |
structure InstNameMangler: NAME_MANGLER; |
73 |
structure ConstNameMangler: NAME_MANGLER; |
|
74 |
structure DatatypeconsNameMangler: NAME_MANGLER; |
|
18231 | 75 |
structure CodegenData: THEORY_DATA; |
18454 | 76 |
val mk_tabs: theory -> auxtab; |
77 |
val alias_get: theory -> string -> string; |
|
18515 | 78 |
val idf_of_name: theory -> string -> string -> string; |
79 |
val idf_of_const: theory -> auxtab -> string * typ -> string; |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
80 |
end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
81 |
|
18217 | 82 |
structure CodegenPackage : CODEGEN_PACKAGE = |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
83 |
struct |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
84 |
|
18850 | 85 |
open CodegenThingol; |
18217 | 86 |
|
18702 | 87 |
(* shallow name spaces *) |
18217 | 88 |
|
19038 | 89 |
val alias_ref = ref (fn thy : theory => fn s : string => s, fn thy : theory => fn s : string => s); |
90 |
fun alias_get name = (fst o !) alias_ref name; |
|
91 |
fun alias_rev name = (snd o !) alias_ref name; |
|
92 |
||
18885 | 93 |
val nsp_module = ""; (* a dummy by convention *) |
18217 | 94 |
val nsp_class = "class"; |
18454 | 95 |
val nsp_tyco = "tyco"; |
18217 | 96 |
val nsp_const = "const"; |
18454 | 97 |
val nsp_overl = "overl"; |
98 |
val nsp_dtcon = "dtcon"; |
|
18217 | 99 |
val nsp_mem = "mem"; |
100 |
val nsp_inst = "inst"; |
|
19213 | 101 |
val nsp_instmem = "instmem"; |
18217 | 102 |
|
19038 | 103 |
fun add_nsp shallow name = |
104 |
name |
|
105 |
|> NameSpace.unpack |
|
106 |
|> split_last |
|
107 |
|> apsnd (single #> cons shallow) |
|
108 |
|> (op @) |
|
109 |
|> NameSpace.pack; |
|
110 |
||
111 |
fun dest_nsp nsp idf = |
|
112 |
let |
|
113 |
val idf' = NameSpace.unpack idf; |
|
114 |
val (idf'', idf_base) = split_last idf'; |
|
115 |
val (modl, shallow) = split_last idf''; |
|
116 |
in |
|
117 |
if nsp = shallow |
|
118 |
then (SOME o NameSpace.pack) (modl @ [idf_base]) |
|
119 |
else NONE |
|
120 |
end; |
|
121 |
||
122 |
fun idf_of_name thy shallow name = |
|
123 |
name |
|
124 |
|> alias_get thy |
|
125 |
|> add_nsp shallow; |
|
126 |
||
127 |
fun name_of_idf thy shallow idf = |
|
128 |
idf |
|
129 |
|> dest_nsp shallow |
|
130 |
|> Option.map (alias_rev thy); |
|
131 |
||
18217 | 132 |
|
18702 | 133 |
(* code generator basics *) |
18454 | 134 |
|
19038 | 135 |
type deftab = (typ * (thm * string)) list Symtab.table; |
136 |
||
137 |
fun eq_typ thy (ty1, ty2) = |
|
138 |
Sign.typ_instance thy (ty1, ty2) |
|
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset
|
139 |
andalso Sign.typ_instance thy (ty2, ty1); |
19008 | 140 |
|
19136 | 141 |
fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c |
19202 | 142 |
of [] => true |
19136 | 143 |
| [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c)) |
144 |
| _ => true; |
|
145 |
||
18454 | 146 |
structure InstNameMangler = NameManglerFun ( |
147 |
type ctxt = theory; |
|
148 |
type src = string * (class * string); |
|
149 |
val ord = prod_ord string_ord (prod_ord string_ord string_ord); |
|
150 |
fun mk thy ((thyname, (cls, tyco)), i) = |
|
19008 | 151 |
(NameSpace.base o alias_get thy) cls ^ "_" ^ (NameSpace.base o alias_get thy) tyco ^ implode (replicate i "'") |
18454 | 152 |
|> NameSpace.append thyname; |
153 |
fun is_valid _ _ = true; |
|
154 |
fun maybe_unique _ _ = NONE; |
|
155 |
fun re_mangle _ dst = error ("no such instance: " ^ quote dst); |
|
156 |
); |
|
157 |
||
158 |
structure ConstNameMangler = NameManglerFun ( |
|
19136 | 159 |
type ctxt = theory; |
160 |
type src = string * typ; |
|
161 |
val ord = prod_ord string_ord Term.typ_ord; |
|
162 |
fun mk thy ((c, ty), i) = |
|
18454 | 163 |
let |
19038 | 164 |
val c' = idf_of_name thy nsp_overl c; |
19202 | 165 |
val prefix = |
166 |
case (AList.lookup (eq_typ thy) |
|
167 |
(Defs.specifications_of (Theory.defs_of thy) c)) ty |
|
168 |
of SOME thyname => NameSpace.append thyname nsp_overl |
|
169 |
| NONE => if c = "op =" |
|
170 |
then |
|
171 |
NameSpace.append |
|
172 |
(((fn s => Codegen.thyname_of_type s thy) o fst o dest_Type o hd o fst o strip_type) ty) |
|
173 |
nsp_overl |
|
174 |
else |
|
175 |
NameSpace.drop_base c'; |
|
19136 | 176 |
val c'' = NameSpace.append prefix (NameSpace.base c'); |
18454 | 177 |
fun mangle (Type (tyco, tys)) = |
19008 | 178 |
(NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME |
18454 | 179 |
| mangle _ = |
180 |
NONE |
|
181 |
in |
|
182 |
Vartab.empty |
|
19136 | 183 |
|> Sign.typ_match thy (Sign.the_const_type thy c, ty) |
18454 | 184 |
|> map (snd o snd) o Vartab.dest |
185 |
|> List.mapPartial mangle |
|
186 |
|> Library.flat |
|
187 |
|> null ? K ["x"] |
|
19038 | 188 |
|> cons c'' |
18454 | 189 |
|> space_implode "_" |
190 |
|> curry (op ^ o swap) ((implode oo replicate) i "'") |
|
191 |
end; |
|
192 |
fun is_valid _ _ = true; |
|
19150 | 193 |
fun maybe_unique thy (c, ty) = |
19136 | 194 |
if is_overloaded thy c |
195 |
then NONE |
|
196 |
else (SOME o idf_of_name thy nsp_const) c; |
|
197 |
fun re_mangle thy idf = |
|
198 |
case name_of_idf thy nsp_const idf |
|
199 |
of NONE => error ("no such constant: " ^ quote idf) |
|
200 |
| SOME c => (c, Sign.the_const_type thy c); |
|
18454 | 201 |
); |
202 |
||
203 |
structure DatatypeconsNameMangler = NameManglerFun ( |
|
204 |
type ctxt = theory; |
|
205 |
type src = string * string; |
|
206 |
val ord = prod_ord string_ord string_ord; |
|
18702 | 207 |
fun mk thy ((co, dtco), i) = |
18454 | 208 |
let |
209 |
fun basename 0 = NameSpace.base co |
|
18455 | 210 |
| basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co |
18454 | 211 |
| basename i = NameSpace.base dtco ^ "_" ^ NameSpace.base co ^ "_" ^ (implode oo replicate) (i-1) "'"; |
212 |
fun strip_dtco name = |
|
213 |
case (rev o NameSpace.unpack) name |
|
214 |
of x1::x2::xs => |
|
215 |
if x2 = NameSpace.base dtco |
|
216 |
then NameSpace.pack (x1::xs) |
|
217 |
else name |
|
218 |
| _ => name; |
|
219 |
in |
|
220 |
NameSpace.append (NameSpace.drop_base dtco) (basename i) |
|
221 |
|> strip_dtco |
|
222 |
end; |
|
223 |
fun is_valid _ _ = true; |
|
224 |
fun maybe_unique _ _ = NONE; |
|
225 |
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); |
|
226 |
); |
|
227 |
||
19213 | 228 |
type auxtab = deftab |
19136 | 229 |
* (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T) |
18865 | 230 |
* DatatypeconsNameMangler.T); |
18702 | 231 |
type eqextr = theory -> auxtab |
19008 | 232 |
-> string * typ -> (thm list * typ) option; |
233 |
type eqextr_default = theory -> auxtab |
|
234 |
-> string * typ -> ((thm list * term option) * typ) option; |
|
18865 | 235 |
type appgen = theory -> auxtab |
236 |
-> (string * typ) * term list -> transact -> iexpr * transact; |
|
18217 | 237 |
|
18702 | 238 |
val serializers = ref ( |
239 |
Symtab.empty |
|
240 |
|> Symtab.update ( |
|
241 |
#ml CodegenSerializer.serializers |
|
242 |
|> apsnd (fn seri => seri |
|
18865 | 243 |
(nsp_dtcon, nsp_class, K false) |
19213 | 244 |
[[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]] |
18702 | 245 |
) |
246 |
) |
|
247 |
|> Symtab.update ( |
|
248 |
#haskell CodegenSerializer.serializers |
|
249 |
|> apsnd (fn seri => seri |
|
18919 | 250 |
[nsp_module, nsp_class, nsp_tyco, nsp_dtcon] |
19213 | 251 |
[[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]] |
18702 | 252 |
) |
253 |
) |
|
254 |
); |
|
18217 | 255 |
|
256 |
||
18454 | 257 |
(* theory data for code generator *) |
18217 | 258 |
|
18912 | 259 |
fun merge_opt _ (x1, NONE) = x1 |
260 |
| merge_opt _ (NONE, x2) = x2 |
|
261 |
| merge_opt eq (SOME x1, SOME x2) = |
|
262 |
if eq (x1, x2) then SOME x1 else error ("incompatible options during merge"); |
|
263 |
||
18217 | 264 |
type gens = { |
18516 | 265 |
appconst: ((int * int) * (appgen * stamp)) Symtab.table, |
19008 | 266 |
eqextrs: (string * (eqextr_default * stamp)) list |
18217 | 267 |
}; |
268 |
||
18865 | 269 |
fun map_gens f { appconst, eqextrs } = |
18217 | 270 |
let |
18865 | 271 |
val (appconst, eqextrs) = |
272 |
f (appconst, eqextrs) |
|
273 |
in { appconst = appconst, eqextrs = eqextrs } : gens end; |
|
18217 | 274 |
|
275 |
fun merge_gens |
|
18865 | 276 |
({ appconst = appconst1 , eqextrs = eqextrs1 }, |
277 |
{ appconst = appconst2 , eqextrs = eqextrs2 }) = |
|
18516 | 278 |
{ appconst = Symtab.merge |
18865 | 279 |
(fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 |
280 |
andalso stamp1 = stamp2) |
|
18516 | 281 |
(appconst1, appconst2), |
18865 | 282 |
eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2) |
18702 | 283 |
} : gens; |
18217 | 284 |
|
285 |
type logic_data = { |
|
18455 | 286 |
get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option, |
18963 | 287 |
get_datatype: ((theory -> string -> ((string * sort) list * (string * typ list) list) option) * stamp) option, |
18217 | 288 |
alias: string Symtab.table * string Symtab.table |
289 |
}; |
|
290 |
||
18963 | 291 |
fun map_logic_data f { get_all_datatype_cons, get_datatype, alias } = |
18217 | 292 |
let |
18963 | 293 |
val ((get_all_datatype_cons, get_datatype), alias) = |
294 |
f ((get_all_datatype_cons, get_datatype), alias) |
|
295 |
in { get_all_datatype_cons = get_all_datatype_cons, |
|
296 |
get_datatype = get_datatype, alias = alias } : logic_data end; |
|
18217 | 297 |
|
298 |
fun merge_logic_data |
|
18963 | 299 |
({ get_all_datatype_cons = get_all_datatype_cons1, |
300 |
get_datatype = get_datatype1, alias = alias1 }, |
|
301 |
{ get_all_datatype_cons = get_all_datatype_cons2, |
|
302 |
get_datatype = get_datatype2, alias = alias2 }) = |
|
18217 | 303 |
let |
304 |
in |
|
18963 | 305 |
{ get_all_datatype_cons = merge_opt (eq_snd (op =)) |
18865 | 306 |
(get_all_datatype_cons1, get_all_datatype_cons2), |
18963 | 307 |
get_datatype = merge_opt (eq_snd (op =)) |
308 |
(get_datatype1, get_datatype2), |
|
18217 | 309 |
alias = (Symtab.merge (op =) (fst alias1, fst alias2), |
18304 | 310 |
Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data |
18217 | 311 |
end; |
312 |
||
18702 | 313 |
type target_data = { |
18865 | 314 |
syntax_class: string Symtab.table, |
18516 | 315 |
syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, |
316 |
syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table |
|
18217 | 317 |
}; |
318 |
||
18865 | 319 |
fun map_target_data f { syntax_class, syntax_tyco, syntax_const } = |
18217 | 320 |
let |
18865 | 321 |
val (syntax_class, syntax_tyco, syntax_const) = |
322 |
f (syntax_class, syntax_tyco, syntax_const) |
|
323 |
in { |
|
324 |
syntax_class = syntax_class, |
|
325 |
syntax_tyco = syntax_tyco, |
|
326 |
syntax_const = syntax_const } : target_data |
|
18454 | 327 |
end; |
18217 | 328 |
|
18702 | 329 |
fun merge_target_data |
18865 | 330 |
({ syntax_class = syntax_class1, syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, |
331 |
{ syntax_class = syntax_class2, syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = |
|
332 |
{ syntax_class = Symtab.merge (op =) (syntax_class1, syntax_class2), |
|
333 |
syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), |
|
18702 | 334 |
syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data; |
18217 | 335 |
|
336 |
structure CodegenData = TheoryDataFun |
|
337 |
(struct |
|
338 |
val name = "Pure/codegen_package"; |
|
339 |
type T = { |
|
340 |
modl: module, |
|
341 |
gens: gens, |
|
342 |
logic_data: logic_data, |
|
18702 | 343 |
target_data: target_data Symtab.table |
18217 | 344 |
}; |
345 |
val empty = { |
|
346 |
modl = empty_module, |
|
18865 | 347 |
gens = { appconst = Symtab.empty, eqextrs = [] } : gens, |
18963 | 348 |
logic_data = { get_all_datatype_cons = NONE, |
349 |
get_datatype = NONE, |
|
18454 | 350 |
alias = (Symtab.empty, Symtab.empty) } : logic_data, |
18702 | 351 |
target_data = |
18217 | 352 |
Symtab.empty |
18702 | 353 |
|> Symtab.fold (fn (target, _) => |
18865 | 354 |
Symtab.update (target, |
355 |
{ syntax_class = Symtab.empty, syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |
|
18702 | 356 |
) (! serializers) |
18217 | 357 |
} : T; |
358 |
val copy = I; |
|
359 |
val extend = I; |
|
360 |
fun merge _ ( |
|
18702 | 361 |
{ modl = modl1, gens = gens1, |
362 |
target_data = target_data1, logic_data = logic_data1 }, |
|
363 |
{ modl = modl2, gens = gens2, |
|
364 |
target_data = target_data2, logic_data = logic_data2 } |
|
18217 | 365 |
) = { |
366 |
modl = merge_module (modl1, modl2), |
|
367 |
gens = merge_gens (gens1, gens2), |
|
368 |
logic_data = merge_logic_data (logic_data1, logic_data2), |
|
19025 | 369 |
target_data = Symtab.join (K merge_target_data) (target_data1, target_data2) |
18217 | 370 |
}; |
18708 | 371 |
fun print _ _ = (); |
18217 | 372 |
end); |
373 |
||
18708 | 374 |
val _ = Context.add_setup CodegenData.init; |
375 |
||
18217 | 376 |
fun map_codegen_data f thy = |
377 |
case CodegenData.get thy |
|
18702 | 378 |
of { modl, gens, target_data, logic_data } => |
379 |
let val (modl, gens, target_data, logic_data) = |
|
380 |
f (modl, gens, target_data, logic_data) |
|
381 |
in CodegenData.put { modl = modl, gens = gens, |
|
382 |
target_data = target_data, logic_data = logic_data } thy end; |
|
18217 | 383 |
|
19008 | 384 |
fun print_code thy = |
18517 | 385 |
let |
386 |
val module = (#modl o CodegenData.get) thy; |
|
387 |
in |
|
19008 | 388 |
(Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module] |
18517 | 389 |
end; |
18217 | 390 |
|
391 |
||
19038 | 392 |
(* advanced name handling *) |
18217 | 393 |
|
394 |
fun add_alias (src, dst) = |
|
395 |
map_codegen_data |
|
18702 | 396 |
(fn (modl, gens, target_data, logic_data) => |
397 |
(modl, gens, target_data, |
|
18217 | 398 |
logic_data |> map_logic_data |
399 |
(apsnd (fn (tab, tab_rev) => |
|
400 |
(tab |> Symtab.update (src, dst), |
|
401 |
tab_rev |> Symtab.update (dst, src)))))); |
|
402 |
||
19038 | 403 |
val _ = alias_ref := (perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get, |
404 |
perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get); |
|
18702 | 405 |
|
19213 | 406 |
fun idf_of_const thy (tabs as (deftab, (_, (overltab1, overltab2), dtcontab))) |
18865 | 407 |
(c, ty) = |
18454 | 408 |
let |
18515 | 409 |
fun get_overloaded (c, ty) = |
19202 | 410 |
(case Symtab.lookup overltab1 c |
19136 | 411 |
of SOME tys => |
18515 | 412 |
(case find_first (curry (Sign.typ_instance thy) ty) tys |
19136 | 413 |
of SOME ty' => ConstNameMangler.get thy overltab2 |
414 |
(c, ty') |> SOME |
|
18515 | 415 |
| _ => NONE) |
19202 | 416 |
| _ => NONE) |
18515 | 417 |
fun get_datatypecons (c, ty) = |
418 |
case (snd o strip_type) ty |
|
419 |
of Type (tyco, _) => |
|
420 |
try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco) |
|
421 |
| _ => NONE; |
|
18702 | 422 |
in case get_datatypecons (c, ty) |
423 |
of SOME c' => idf_of_name thy nsp_dtcon c' |
|
424 |
| NONE => case get_overloaded (c, ty) |
|
18515 | 425 |
of SOME idf => idf |
19213 | 426 |
| NONE => case ClassPackage.lookup_const_class thy c |
18515 | 427 |
of SOME _ => idf_of_name thy nsp_mem c |
428 |
| NONE => idf_of_name thy nsp_const c |
|
429 |
end; |
|
18217 | 430 |
|
19177 | 431 |
fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = |
18454 | 432 |
case name_of_idf thy nsp_const idf |
18702 | 433 |
of SOME c => SOME (c, Sign.the_const_type thy c) |
18454 | 434 |
| NONE => ( |
435 |
case dest_nsp nsp_overl idf |
|
436 |
of SOME _ => |
|
437 |
idf |
|
19136 | 438 |
|> ConstNameMangler.rev thy overltab2 |
18454 | 439 |
|> SOME |
440 |
| NONE => NONE |
|
441 |
); |
|
442 |
||
19177 | 443 |
fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf = |
444 |
case recconst_of_idf thy tabs idf |
|
445 |
of SOME c_ty => SOME c_ty |
|
446 |
| NONE => case dest_nsp nsp_mem idf |
|
447 |
of SOME c => SOME (c, Sign.the_const_constraint thy c) |
|
448 |
| NONE => case name_of_idf thy nsp_dtcon idf |
|
449 |
of SOME idf' => let |
|
450 |
val c = (fst o DatatypeconsNameMangler.rev thy dtcontab) idf' |
|
451 |
in SOME (c, Sign.the_const_type thy c) end |
|
452 |
| NONE => NONE; |
|
18865 | 453 |
|
454 |
(* further theory data accessors *) |
|
455 |
||
456 |
fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy = |
|
18454 | 457 |
let |
18865 | 458 |
val c = prep_const thy raw_c; |
459 |
in map_codegen_data |
|
460 |
(fn (modl, gens, target_data, logic_data) => |
|
461 |
(modl, |
|
462 |
gens |> map_gens |
|
463 |
(fn (appconst, eqextrs) => |
|
464 |
(appconst |
|
465 |
|> Symtab.update (c, (bounds, (ag, stamp ()))), |
|
466 |
eqextrs)), target_data, logic_data)) thy |
|
18454 | 467 |
end; |
18217 | 468 |
|
18865 | 469 |
val add_appconst = gen_add_appconst Sign.intern_const; |
470 |
val add_appconst_i = gen_add_appconst (K I); |
|
471 |
||
472 |
fun add_eqextr (name, eqx) = |
|
473 |
map_codegen_data |
|
474 |
(fn (modl, gens, target_data, logic_data) => |
|
475 |
(modl, |
|
476 |
gens |> map_gens |
|
477 |
(fn (appconst, eqextrs) => |
|
478 |
(appconst, eqextrs |
|
479 |
|> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) |
|
19008 | 480 |
(name, ((Option.map o apfst o rpair) NONE ooo eqx , stamp ())))), |
481 |
target_data, logic_data)); |
|
482 |
||
483 |
fun add_eqextr_default (name, eqx) = |
|
484 |
map_codegen_data |
|
485 |
(fn (modl, gens, target_data, logic_data) => |
|
486 |
(modl, |
|
487 |
gens |> map_gens |
|
488 |
(fn (appconst, eqextrs) => |
|
489 |
(appconst, eqextrs |
|
19150 | 490 |
|> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) |
18865 | 491 |
(name, (eqx, stamp ())))), |
492 |
target_data, logic_data)); |
|
493 |
||
494 |
fun get_eqextrs thy tabs = |
|
19008 | 495 |
(map (fn (name, (eqx, _)) => (name, eqx thy tabs)) o #eqextrs o #gens o CodegenData.get) thy; |
18865 | 496 |
|
497 |
fun set_get_all_datatype_cons f = |
|
498 |
map_codegen_data |
|
499 |
(fn (modl, gens, target_data, logic_data) => |
|
500 |
(modl, gens, target_data, |
|
501 |
logic_data |
|
18963 | 502 |
|> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype) |
503 |
=> (SOME (f, stamp ()), get_datatype)))))); |
|
18865 | 504 |
|
505 |
fun get_all_datatype_cons thy = |
|
506 |
case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy |
|
507 |
of NONE => [] |
|
508 |
| SOME (f, _) => f thy; |
|
509 |
||
18963 | 510 |
fun set_get_datatype f = |
18865 | 511 |
map_codegen_data |
512 |
(fn (modl, gens, target_data, logic_data) => |
|
513 |
(modl, gens, target_data, |
|
514 |
logic_data |
|
18963 | 515 |
|> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype) |
516 |
=> (get_all_datatype_cons, SOME (f, stamp ()))))))); |
|
18865 | 517 |
|
18963 | 518 |
fun get_datatype thy = |
519 |
case (#get_datatype o #logic_data o CodegenData.get) thy |
|
520 |
of NONE => K NONE |
|
521 |
| SOME (f, _) => f thy; |
|
18865 | 522 |
|
523 |
fun set_int_tyco tyco thy = |
|
524 |
(serializers := ( |
|
525 |
! serializers |
|
526 |
|> Symtab.update ( |
|
527 |
#ml CodegenSerializer.serializers |
|
528 |
|> apsnd (fn seri => seri |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
529 |
(nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco) |
19213 | 530 |
[[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_instmem]] |
18865 | 531 |
) |
532 |
) |
|
533 |
); thy); |
|
534 |
||
535 |
||
18912 | 536 |
(* sophisticated devarification *) |
537 |
||
538 |
fun devarify_typs tys = |
|
539 |
let |
|
19008 | 540 |
fun add_rename (vi as (v, _), sorts) used = |
18912 | 541 |
let |
18918 | 542 |
val v' = "'" ^ variant used (unprefix "'" v) |
19008 | 543 |
in (map (fn sort => (((vi, sort), TFree (v', sort)), (v', TVar (vi, sort)))) sorts, v' :: used) end; |
18912 | 544 |
fun typ_names (Type (tyco, tys)) (vars, names) = |
545 |
(vars, names |> insert (op =) (NameSpace.base tyco)) |
|
546 |
|> fold typ_names tys |
|
547 |
| typ_names (TFree (v, _)) (vars, names) = |
|
18918 | 548 |
(vars, names |> insert (op =) (unprefix "'" v)) |
549 |
| typ_names (TVar (vi, sort)) (vars, names) = |
|
19008 | 550 |
(vars |
551 |
|> AList.default (op =) (vi, []) |
|
552 |
|> AList.map_entry (op =) vi (cons sort), |
|
553 |
names); |
|
18912 | 554 |
val (vars, used) = fold typ_names tys ([], []); |
19008 | 555 |
val (renames, reverse) = fold_map add_rename vars used |> fst |> Library.flat |> split_list; |
18912 | 556 |
in |
18918 | 557 |
(reverse, map (Term.instantiateT renames) tys) |
18912 | 558 |
end; |
559 |
||
560 |
fun burrow_typs_yield f ts = |
|
561 |
let |
|
562 |
val typtab = |
|
563 |
fold (fold_types (fn ty => Typtab.update (ty, dummyT))) |
|
564 |
ts Typtab.empty; |
|
565 |
val typs = Typtab.keys typtab; |
|
566 |
val (x, typs') = f typs; |
|
567 |
val typtab' = fold2 (Typtab.update oo pair) typs typs' typtab; |
|
568 |
in |
|
569 |
(x, (map o map_term_types) (the o Typtab.lookup typtab') ts) |
|
570 |
end; |
|
571 |
||
572 |
fun devarify_terms ts = |
|
573 |
let |
|
19008 | 574 |
fun add_rename (vi as (v, _), tys) used = |
18912 | 575 |
let |
576 |
val v' = variant used v |
|
19008 | 577 |
in (map (fn ty => (((vi, ty), Free (v', ty)), (v', Var (vi, ty)))) tys, v' :: used) end; |
18912 | 578 |
fun term_names (Const (c, _)) (vars, names) = |
579 |
(vars, names |> insert (op =) (NameSpace.base c)) |
|
580 |
| term_names (Free (v, _)) (vars, names) = |
|
581 |
(vars, names |> insert (op =) v) |
|
19008 | 582 |
| term_names (Var (vi, ty)) (vars, names) = |
583 |
(vars |
|
584 |
|> AList.default (op =) (vi, []) |
|
585 |
|> AList.map_entry (op =) vi (cons ty), |
|
586 |
names) |
|
18912 | 587 |
| term_names (Bound _) vars_names = |
588 |
vars_names |
|
589 |
| term_names (Abs (v, _, _)) (vars, names) = |
|
590 |
(vars, names |> insert (op =) v) |
|
591 |
| term_names (t1 $ t2) vars_names = |
|
592 |
vars_names |> term_names t1 |> term_names t2 |
|
593 |
val (vars, used) = fold term_names ts ([], []); |
|
19008 | 594 |
val (renames, reverse) = fold_map add_rename vars used |> fst |> Library.flat |> split_list; |
18912 | 595 |
in |
18918 | 596 |
(reverse, map (Term.instantiate ([], renames)) ts) |
18912 | 597 |
end; |
598 |
||
599 |
fun devarify_term_typs ts = |
|
600 |
ts |
|
601 |
|> devarify_terms |
|
602 |
|-> (fn reverse => burrow_typs_yield devarify_typs |
|
603 |
#-> (fn reverseT => pair (reverseT, reverse))); |
|
604 |
||
18865 | 605 |
(* definition and expression generators *) |
606 |
||
607 |
fun ensure_def_class thy tabs cls trns = |
|
18454 | 608 |
let |
18865 | 609 |
fun defgen_class thy (tabs as (_, (insttab, _, _))) cls trns = |
610 |
case name_of_idf thy nsp_class cls |
|
611 |
of SOME cls => |
|
612 |
let |
|
613 |
val cs = (snd o ClassPackage.the_consts_sign thy) cls; |
|
614 |
val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs; |
|
615 |
val idfs = map (idf_of_name thy nsp_mem o fst) cs; |
|
616 |
in |
|
617 |
trns |
|
618 |
|> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) |
|
619 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
620 |
||>> (exprsgen_type thy tabs o map snd) cs |
18865 | 621 |
||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts |
622 |
|-> (fn ((supcls, memtypes), sortctxts) => succeed |
|
19038 | 623 |
(Class (supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))))) |
18865 | 624 |
end |
625 |
| _ => |
|
626 |
trns |
|
627 |
|> fail ("no class definition found for " ^ quote cls); |
|
628 |
val cls' = idf_of_name thy nsp_class cls; |
|
18454 | 629 |
in |
630 |
trns |
|
18865 | 631 |
|> debug 4 (fn _ => "generating class " ^ quote cls) |
19136 | 632 |
|> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls' |
18865 | 633 |
|> pair cls' |
634 |
end |
|
635 |
and ensure_def_tyco thy tabs tyco trns = |
|
636 |
let |
|
18963 | 637 |
fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns = |
638 |
case name_of_idf thy nsp_tyco dtco |
|
639 |
of SOME dtco => |
|
19008 | 640 |
(case get_datatype thy dtco |
18963 | 641 |
of SOME (vars, cos) => |
642 |
let |
|
643 |
val cos' = map (fn (co, tys) => (DatatypeconsNameMangler.get thy dtcontab (co, dtco) |> |
|
644 |
idf_of_name thy nsp_dtcon, tys)) cos; |
|
645 |
in |
|
646 |
trns |
|
647 |
|> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) |
|
648 |
|> fold_map (exprgen_tyvar_sort thy tabs) vars |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
649 |
||>> fold_map (fn (c, ty) => exprsgen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos' |
18963 | 650 |
|-> (fn (sorts, cos'') => succeed (Datatype |
19038 | 651 |
(sorts, cos''))) |
18963 | 652 |
end |
653 |
| NONE => |
|
654 |
trns |
|
655 |
|> fail ("no datatype found for " ^ quote dtco)) |
|
656 |
| NONE => |
|
657 |
trns |
|
658 |
|> fail ("not a type constructor: " ^ quote dtco) |
|
18865 | 659 |
val tyco' = idf_of_name thy nsp_tyco tyco; |
660 |
in |
|
661 |
trns |
|
662 |
|> debug 4 (fn _ => "generating type constructor " ^ quote tyco) |
|
19136 | 663 |
|> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco' |
18865 | 664 |
|> pair tyco' |
665 |
end |
|
666 |
and exprgen_tyvar_sort thy tabs (v, sort) trns = |
|
18516 | 667 |
trns |
18885 | 668 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort) |
18865 | 669 |
|-> (fn sort => pair (unprefix "'" v, sort)) |
670 |
and exprgen_type thy tabs (TVar _) trns = |
|
18516 | 671 |
error "TVar encountered during code generation" |
18702 | 672 |
| exprgen_type thy tabs (TFree v_s) trns = |
18516 | 673 |
trns |
18702 | 674 |
|> exprgen_tyvar_sort thy tabs v_s |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
675 |
|-> (fn (v, sort) => pair (ITyVar v)) |
18516 | 676 |
| exprgen_type thy tabs (Type ("fun", [t1, t2])) trns = |
677 |
trns |
|
678 |
|> exprgen_type thy tabs t1 |
|
679 |
||>> exprgen_type thy tabs t2 |
|
680 |
|-> (fn (t1', t2') => pair (t1' `-> t2')) |
|
681 |
| exprgen_type thy tabs (Type (tyco, tys)) trns = |
|
682 |
trns |
|
683 |
|> ensure_def_tyco thy tabs tyco |
|
684 |
||>> fold_map (exprgen_type thy tabs) tys |
|
18912 | 685 |
|-> (fn (tyco, tys) => pair (tyco `%% tys)) |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
686 |
and exprsgen_type thy tabs = |
18912 | 687 |
fold_map (exprgen_type thy tabs) o snd o devarify_typs; |
18516 | 688 |
|
18885 | 689 |
fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns = |
18517 | 690 |
trns |
18885 | 691 |
|> ensure_def_inst thy tabs inst |
692 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls |
|
693 |
|-> (fn (inst, ls) => pair (Instance (inst, ls))) |
|
19253 | 694 |
| exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, (i, j)))) trns = |
18516 | 695 |
trns |
18517 | 696 |
|> fold_map (ensure_def_class thy tabs) clss |
19253 | 697 |
|-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i)))) |
19213 | 698 |
and mk_fun thy tabs restrict (c, ty1) trns = |
699 |
case get_first (fn (name, eqx) => (eqx (c, ty1))) (get_eqextrs thy tabs) |
|
700 |
of SOME ((eq_thms, default), ty2) => |
|
18865 | 701 |
let |
19213 | 702 |
val ty3 = if restrict then ty1 else ty2; |
703 |
val sortctxt = ClassPackage.extract_sortctxt thy ty3; |
|
704 |
val instantiate = if restrict |
|
705 |
then |
|
706 |
let |
|
707 |
val tab_lookup = snd o the o Vartab.lookup (Sign.typ_match thy (ty2, ty1) Vartab.empty); |
|
708 |
in map_term_types (map_atyps (fn (TVar (vi, _)) => tab_lookup vi |
|
709 |
| ty => ty)) end |
|
710 |
else I |
|
18865 | 711 |
fun dest_eqthm eq_thm = |
712 |
let |
|
713 |
val ((t, args), rhs) = |
|
19213 | 714 |
(apfst strip_comb o Logic.dest_equals o instantiate |
715 |
o prop_of o Drule.zero_var_indexes) eq_thm; |
|
18865 | 716 |
in case t |
717 |
of Const (c', _) => if c' = c then (args, rhs) |
|
718 |
else error ("illegal function equation for " ^ quote c |
|
719 |
^ ", actually defining " ^ quote c') |
|
720 |
| _ => error ("illegal function equation for " ^ quote c) |
|
721 |
end; |
|
19008 | 722 |
fun mk_default t = |
723 |
let |
|
19213 | 724 |
val (tys, ty') = strip_type ty3; |
19008 | 725 |
val vs = Term.invent_names (add_term_names (t, [])) "x" (length tys); |
726 |
in |
|
727 |
if (not o eq_typ thy) (type_of t, ty') |
|
728 |
then error ("inconsistent type for default rule") |
|
729 |
else (map2 (curry Free) vs tys, t) |
|
730 |
end; |
|
18865 | 731 |
in |
18517 | 732 |
trns |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
733 |
|> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
734 |
||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default |
19213 | 735 |
||>> exprsgen_type thy tabs [ty3] |
18865 | 736 |
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt |
19253 | 737 |
|-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) ((eqs @ eq_default, (sortctxt, ty)), ty3)) |
18865 | 738 |
end |
739 |
| NONE => (NONE, trns) |
|
740 |
and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = |
|
741 |
let |
|
742 |
fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns = |
|
743 |
case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) |
|
18885 | 744 |
of SOME (_, (class, tyco)) => |
18865 | 745 |
let |
18885 | 746 |
val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco); |
18865 | 747 |
fun gen_suparity supclass trns = |
748 |
trns |
|
19136 | 749 |
|> ensure_def_class thy tabs supclass |
18885 | 750 |
||>> ensure_def_inst thy tabs (supclass, tyco) |
19136 | 751 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
19213 | 752 |
(ClassPackage.extract_classlookup_inst thy (class, tyco) supclass) |
19136 | 753 |
|-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss))); |
18865 | 754 |
fun gen_membr (m, ty) trns = |
755 |
trns |
|
19213 | 756 |
|> mk_fun thy tabs true (m, ty) |
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset
|
757 |
|-> (fn NONE => error ("could not derive definition for member " |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset
|
758 |
^ quote m ^ " :: " ^ Sign.string_of_typ thy ty) |
19253 | 759 |
| SOME (funn, ty_use) => |
760 |
(fold_map o fold_map) (exprgen_classlookup thy tabs) |
|
761 |
(ClassPackage.extract_classlookup_member thy (ty, ty_use)) |
|
762 |
#-> (fn lss => |
|
763 |
pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss)))); |
|
18865 | 764 |
in |
765 |
trns |
|
766 |
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls |
|
767 |
^ ", " ^ quote tyco ^ ")") |
|
18885 | 768 |
|> ensure_def_class thy tabs class |
18865 | 769 |
||>> ensure_def_tyco thy tabs tyco |
770 |
||>> fold_map (exprgen_tyvar_sort thy tabs) arity |
|
18885 | 771 |
||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class) |
18865 | 772 |
||>> fold_map gen_membr memdefs |
18885 | 773 |
|-> (fn ((((class, tyco), arity), suparities), memdefs) => |
774 |
succeed (Classinst (((class, (tyco, arity)), suparities), memdefs))) |
|
18865 | 775 |
end |
776 |
| _ => |
|
777 |
trns |> fail ("no class instance found for " ^ quote inst); |
|
19213 | 778 |
val (_, thyname) = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; |
18865 | 779 |
val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); |
780 |
in |
|
781 |
trns |
|
782 |
|> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) |
|
19136 | 783 |
|> ensure_def [("instance", defgen_inst thy tabs)] |
18865 | 784 |
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst |
785 |
|> pair inst |
|
786 |
end |
|
19213 | 787 |
and ensure_def_const thy (tabs as (_, (_, overltab, dtcontab))) (c, ty) trns = |
18865 | 788 |
let |
789 |
fun defgen_funs thy tabs c trns = |
|
790 |
case recconst_of_idf thy tabs c |
|
791 |
of SOME (c, ty) => |
|
792 |
trns |
|
19213 | 793 |
|> mk_fun thy tabs false (c, ty) |
19253 | 794 |
|-> (fn SOME (funn, _) => succeed (Fun funn) |
18865 | 795 |
| NONE => fail ("no defining equations found for " ^ quote c)) |
796 |
| NONE => |
|
797 |
trns |
|
798 |
|> fail ("not a constant: " ^ quote c); |
|
18963 | 799 |
fun defgen_clsmem thy tabs m trns = |
800 |
case name_of_idf thy nsp_mem m |
|
801 |
of SOME m => |
|
802 |
trns |
|
803 |
|> debug 5 (fn _ => "trying defgen class member for " ^ quote m) |
|
804 |
|> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) |
|
805 |
|-> (fn cls => succeed Undef) |
|
806 |
| _ => |
|
807 |
trns |> fail ("no class member found for " ^ quote m) |
|
18865 | 808 |
fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns = |
809 |
case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) |
|
810 |
of SOME (co, dtco) => |
|
811 |
trns |
|
812 |
|> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) |
|
813 |
|> ensure_def_tyco thy tabs dtco |
|
814 |
|-> (fn dtco => succeed Undef) |
|
815 |
| _ => |
|
816 |
trns |
|
817 |
|> fail ("not a datatype constructor: " ^ quote co); |
|
18963 | 818 |
fun get_defgen idf = |
819 |
if (is_some oo name_of_idf thy) nsp_const idf |
|
820 |
orelse (is_some oo name_of_idf thy) nsp_overl idf |
|
821 |
then ("funs", defgen_funs thy tabs) |
|
822 |
else if (is_some oo name_of_idf thy) nsp_mem idf |
|
823 |
then ("clsmem", defgen_clsmem thy tabs) |
|
824 |
else if (is_some oo name_of_idf thy) nsp_dtcon idf |
|
825 |
then ("datatypecons", defgen_datatypecons thy tabs) |
|
826 |
else error ("illegal shallow name space for constant: " ^ quote idf); |
|
827 |
val idf = idf_of_const thy tabs (c, ty); |
|
18865 | 828 |
in |
829 |
trns |
|
830 |
|> debug 4 (fn _ => "generating constant " ^ quote c) |
|
19136 | 831 |
|> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf |
18963 | 832 |
|> pair idf |
18865 | 833 |
end |
18517 | 834 |
and exprgen_term thy tabs (Const (f, ty)) trns = |
835 |
trns |
|
836 |
|> appgen thy tabs ((f, ty), []) |
|
18516 | 837 |
|-> (fn e => pair e) |
18912 | 838 |
| exprgen_term thy tabs (Var _) trns = |
839 |
error "Var encountered during code generation" |
|
18516 | 840 |
| exprgen_term thy tabs (Free (v, ty)) trns = |
841 |
trns |
|
18912 | 842 |
|> exprgen_type thy tabs ty |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
843 |
|-> (fn ty => pair (IVar v)) |
19136 | 844 |
| exprgen_term thy tabs (Abs (abs as (_, ty, _))) trns = |
845 |
let |
|
846 |
val (v, t) = Term.variant_abs abs |
|
847 |
in |
|
848 |
trns |
|
849 |
|> exprgen_type thy tabs ty |
|
850 |
||>> exprgen_term thy tabs t |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
851 |
|-> (fn (ty, e) => pair ((v, ty) `|-> e)) |
19136 | 852 |
end |
18516 | 853 |
| exprgen_term thy tabs (t as t1 $ t2) trns = |
854 |
let |
|
855 |
val (t', ts) = strip_comb t |
|
856 |
in case t' |
|
857 |
of Const (f, ty) => |
|
858 |
trns |
|
18517 | 859 |
|> appgen thy tabs ((f, ty), ts) |
18516 | 860 |
|-> (fn e => pair e) |
861 |
| _ => |
|
862 |
trns |
|
863 |
|> exprgen_term thy tabs t' |
|
864 |
||>> fold_map (exprgen_term thy tabs) ts |
|
865 |
|-> (fn (e, es) => pair (e `$$ es)) |
|
18865 | 866 |
end |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
867 |
and exprsgen_term thy tabs = |
18912 | 868 |
fold_map (exprgen_term thy tabs) o snd o devarify_term_typs |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
869 |
and exprsgen_eqs thy tabs = |
18912 | 870 |
apfst (map (fn (rhs::args) => (args, rhs))) |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
871 |
oo fold_burrow (exprsgen_term thy tabs) |
18912 | 872 |
o map (fn (args, rhs) => (rhs :: args)) |
18865 | 873 |
and appgen_default thy tabs ((c, ty), ts) trns = |
874 |
trns |
|
875 |
|> ensure_def_const thy tabs (c, ty) |
|
19202 | 876 |
||>> exprsgen_type thy tabs [ty] |
18885 | 877 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
878 |
(ClassPackage.extract_classlookup thy (c, ty)) |
|
18912 | 879 |
||>> fold_map (exprgen_term thy tabs) ts |
19202 | 880 |
|-> (fn (((c, [ty]), ls), es) => |
881 |
pair (IConst (c, (ls, ty)) `$$ es)) |
|
18865 | 882 |
and appgen thy tabs ((f, ty), ts) trns = |
883 |
case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f |
|
884 |
of SOME ((imin, imax), (ag, _)) => |
|
885 |
if length ts < imin then |
|
886 |
let |
|
887 |
val d = imin - length ts; |
|
888 |
val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d; |
|
889 |
val tys = Library.take (d, ((fst o strip_type) ty)); |
|
890 |
in |
|
891 |
trns |
|
892 |
|> debug 10 (fn _ => "eta-expanding") |
|
18912 | 893 |
|> fold_map (exprgen_type thy tabs) tys |
18865 | 894 |
||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys) |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
895 |
|-> (fn (tys, e) => pair (vs ~~ tys `|--> e)) |
18865 | 896 |
end |
897 |
else if length ts > imax then |
|
898 |
trns |
|
899 |
|> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " |
|
900 |
^ string_of_int (length ts) ^ ")") |
|
901 |
|> ag thy tabs ((f, ty), Library.take (imax, ts)) |
|
902 |
||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
903 |
|-> (fn (e, es) => pair (e `$$ es)) |
18865 | 904 |
else |
905 |
trns |
|
906 |
|> debug 10 (fn _ => "keeping arguments") |
|
907 |
|> ag thy tabs ((f, ty), ts) |
|
908 |
| NONE => |
|
909 |
trns |
|
910 |
|> appgen_default thy tabs ((f, ty), ts); |
|
18516 | 911 |
|
18702 | 912 |
|
913 |
(* function extractors *) |
|
914 |
||
19213 | 915 |
fun eqextr_defs thy (deftab, _) (c, ty) = |
19253 | 916 |
Option.mapPartial (get_first (fn (ty', (thm, _)) => |
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset
|
917 |
if Sign.typ_instance thy (ty, ty') |
19008 | 918 |
then SOME ([thm], ty') |
919 |
else NONE |
|
920 |
)) (Symtab.lookup deftab c); |
|
18517 | 921 |
|
922 |
||
18217 | 923 |
(* parametrized generators, for instantiation in HOL *) |
924 |
||
19213 | 925 |
fun appgen_split strip_abs thy tabs (app as (c_ty, [t])) trns = |
926 |
case strip_abs 1 (Const c_ty $ t) |
|
19202 | 927 |
of ([vt], bt) => |
19150 | 928 |
trns |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
929 |
|> exprgen_term thy tabs vt |
19202 | 930 |
||>> exprgen_type thy tabs (type_of vt) |
931 |
||>> exprgen_term thy tabs bt |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
932 |
||>> appgen_default thy tabs app |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
933 |
|-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0))) |
19150 | 934 |
| _ => |
935 |
trns |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
936 |
|> appgen_default thy tabs app; |
18335 | 937 |
|
19202 | 938 |
fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns = |
939 |
case strip_abs 1 ct |
|
940 |
of ([st], bt) => |
|
941 |
trns |
|
942 |
|> exprgen_term thy tabs dt |
|
943 |
||>> exprgen_type thy tabs (type_of dt) |
|
944 |
||>> exprgen_term thy tabs st |
|
945 |
||>> exprgen_term thy tabs bt |
|
946 |
||>> appgen_default thy tabs app |
|
947 |
|-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0))) |
|
948 |
| _ => |
|
949 |
trns |
|
950 |
|> appgen_default thy tabs app; |
|
951 |
||
18702 | 952 |
fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_, |
953 |
Type (_, [_, ty as Type (tyco, [])])), [bin]) trns = |
|
19202 | 954 |
if tyco = tyco_nat then |
18702 | 955 |
trns |
19202 | 956 |
|> exprgen_term thy tabs (mk_int_to_nat bin) (*should be a preprocessor's work*) |
957 |
else |
|
958 |
let |
|
959 |
val i = bin_to_int thy bin; |
|
960 |
val _ = if i < 0 then error ("negative numeral: " ^ IntInf.toString i) else (); |
|
961 |
(*should be a preprocessor's work*) |
|
962 |
in |
|
963 |
trns |
|
964 |
|> exprgen_type thy tabs ty |
|
965 |
|-> (fn ty => pair (CodegenThingol.INum ((i, ty), ()))) |
|
966 |
end; |
|
18217 | 967 |
|
19038 | 968 |
fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns = |
969 |
let |
|
970 |
val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c; |
|
971 |
val ty' = (op ---> o apfst tl o strip_type) ty; |
|
972 |
val idf = idf_of_const thy tabs (c, ty); |
|
973 |
in |
|
974 |
trns |
|
19136 | 975 |
|> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf |
976 |
|> exprgen_type thy tabs ty' |
|
977 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
|
978 |
(ClassPackage.extract_classlookup thy (c, ty)) |
|
979 |
||>> exprsgen_type thy tabs [ty_def] |
|
980 |
||>> exprgen_term thy tabs tf |
|
981 |
||>> exprgen_term thy tabs tx |
|
19202 | 982 |
|-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx)) |
19038 | 983 |
end; |
984 |
||
19008 | 985 |
fun eqextr_eq f fals thy tabs ("op =", ty) = |
986 |
(case ty |
|
987 |
of Type ("fun", [Type (dtco, _), _]) => |
|
988 |
(case f thy dtco |
|
989 |
of [] => NONE |
|
990 |
| [eq] => SOME ((Codegen.preprocess thy [eq], NONE), ty) |
|
991 |
| eqs => SOME ((Codegen.preprocess thy eqs, SOME fals), ty)) |
|
992 |
| _ => NONE) |
|
993 |
| eqextr_eq f fals thy tabs _ = |
|
994 |
NONE; |
|
995 |
||
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
996 |
fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns = |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
997 |
let |
18517 | 998 |
val (ts', t) = split_last ts; |
999 |
val (tys, dty) = (split_last o fst o strip_type) ty; |
|
1000 |
fun gen_names i = |
|
1001 |
variantlist (replicate i "x", foldr add_term_names |
|
1002 |
(map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts); |
|
1003 |
fun cg_case_d (((cname, i), ty), t) trns = |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1004 |
let |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1005 |
val vs = gen_names i; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1006 |
val tys = Library.take (i, (fst o strip_type) ty); |
18330 | 1007 |
val frees = map2 (curry Free) vs tys; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1008 |
val t' = Envir.beta_norm (list_comb (t, frees)); |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1009 |
in |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1010 |
trns |
18516 | 1011 |
|> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees)) |
1012 |
||>> exprgen_term thy tabs t' |
|
18865 | 1013 |
|-> (fn (ep, e) => pair (ep, e)) |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1014 |
end; |
18517 | 1015 |
in |
1016 |
trns |
|
1017 |
|> exprgen_term thy tabs t |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
1018 |
||>> exprgen_type thy tabs dty |
18517 | 1019 |
||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts') |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
1020 |
||>> appgen_default thy tabs app |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
1021 |
|-> (fn (((de, dty), bses), e0) => pair (ICase (((de, dty), bses), e0))) |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1022 |
end; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1023 |
|
18702 | 1024 |
fun gen_add_case_const prep_c get_case_const_data raw_c thy = |
18517 | 1025 |
let |
1026 |
val c = prep_c thy raw_c; |
|
18702 | 1027 |
val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_type thy) c; |
18517 | 1028 |
val cos = (the o get_case_const_data thy) c; |
1029 |
val n_eta = length cos + 1; |
|
1030 |
in |
|
1031 |
thy |
|
1032 |
|> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos)) |
|
1033 |
end; |
|
1034 |
||
18702 | 1035 |
val add_case_const = gen_add_case_const Sign.intern_const; |
1036 |
val add_case_const_i = gen_add_case_const (K I); |
|
18517 | 1037 |
|
18217 | 1038 |
|
18516 | 1039 |
|
1040 |
(** theory interface **) |
|
18217 | 1041 |
|
18454 | 1042 |
fun mk_tabs thy = |
18217 | 1043 |
let |
18454 | 1044 |
fun extract_defs thy = |
18217 | 1045 |
let |
19038 | 1046 |
fun dest thm = |
18454 | 1047 |
let |
19038 | 1048 |
val (lhs, rhs) = Logic.dest_equals (prop_of thm); |
18702 | 1049 |
val (t, args) = strip_comb lhs; |
1050 |
val (c, ty) = dest_Const t |
|
19038 | 1051 |
in if forall is_Var args then SOME ((c, ty), thm) else NONE |
18454 | 1052 |
end handle TERM _ => NONE; |
1053 |
fun prep_def def = (case Codegen.preprocess thy [def] of |
|
19008 | 1054 |
[def'] => def' | _ => error "mk_tabs: bad preprocessor"); |
19038 | 1055 |
fun add_def thyname (name, _) = |
18702 | 1056 |
case (dest o prep_def o Thm.get_axiom thy) name |
19038 | 1057 |
of SOME ((c, ty), thm) => |
1058 |
Symtab.default (c, []) |
|
1059 |
#> Symtab.map_entry c (cons (ty, (thm, thyname))) |
|
18702 | 1060 |
| NONE => I |
19038 | 1061 |
fun get_defs thy = |
1062 |
let |
|
1063 |
val thyname = Context.theory_name thy; |
|
1064 |
val defs = (snd o #axioms o Theory.rep_theory) thy; |
|
1065 |
in Symtab.fold (add_def thyname) defs end; |
|
18217 | 1066 |
in |
18454 | 1067 |
Symtab.empty |
19038 | 1068 |
|> fold get_defs (thy :: Theory.ancestors_of thy) |
18217 | 1069 |
end; |
18454 | 1070 |
fun mk_insttab thy = |
1071 |
InstNameMangler.empty |
|
1072 |
|> Symtab.fold_map |
|
19213 | 1073 |
(fn (cls, clsinsts) => fold_map |
18454 | 1074 |
(fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts) |
1075 |
(ClassPackage.get_classtab thy) |
|
1076 |
|-> (fn _ => I); |
|
19136 | 1077 |
fun mk_overltabs thy = |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1078 |
(Symtab.empty, ConstNameMangler.empty) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1079 |
|> Symtab.fold |
19136 | 1080 |
(fn (c, _) => |
1081 |
let |
|
1082 |
val deftab = Defs.specifications_of (Theory.defs_of thy) c |
|
1083 |
val is_overl = (is_none o ClassPackage.lookup_const_class thy) c |
|
1084 |
andalso case deftab |
|
1085 |
of [] => false |
|
1086 |
| [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c)) |
|
1087 |
| _ => true; |
|
1088 |
in if is_overl then (fn (overltab1, overltab2) => ( |
|
1089 |
overltab1 |
|
1090 |
|> Symtab.update_new (c, map fst deftab), |
|
1091 |
overltab2 |
|
1092 |
|> fold_map (fn (ty, _) => ConstNameMangler.declare thy (c, ty)) deftab |
|
1093 |
|-> (fn _ => I))) else I |
|
1094 |
end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy) |
|
1095 |
|> (fn (overltab1, overltab2) => |
|
1096 |
let |
|
1097 |
val c = "op ="; |
|
1098 |
val ty = Sign.the_const_type thy c; |
|
19150 | 1099 |
fun inst dtco = |
19136 | 1100 |
map_atyps (fn _ => Type (dtco, |
1101 |
(map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty |
|
1102 |
val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) []; |
|
1103 |
val tys = map inst dtcos; |
|
1104 |
in |
|
1105 |
(overltab1 |
|
1106 |
|> Symtab.update_new (c, tys), |
|
1107 |
overltab2 |
|
1108 |
|> fold (fn ty => ConstNameMangler.declare thy (c, ty) #> snd) tys) |
|
1109 |
end); |
|
18454 | 1110 |
fun mk_dtcontab thy = |
1111 |
DatatypeconsNameMangler.empty |
|
1112 |
|> fold_map |
|
18455 | 1113 |
(fn (_, co_dtco) => DatatypeconsNameMangler.declare_multi thy co_dtco) |
1114 |
(fold (fn (co, dtco) => |
|
1115 |
let |
|
19008 | 1116 |
val key = ((NameSpace.drop_base o NameSpace.drop_base) co, NameSpace.base co); |
18455 | 1117 |
in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end |
1118 |
) (get_all_datatype_cons thy) []) |
|
18454 | 1119 |
|-> (fn _ => I); |
18702 | 1120 |
val deftab = extract_defs thy; |
18454 | 1121 |
val insttab = mk_insttab thy; |
19136 | 1122 |
val overltabs = mk_overltabs thy; |
18454 | 1123 |
val dtcontab = mk_dtcontab thy; |
19213 | 1124 |
in (deftab, (insttab, overltabs, dtcontab)) end; |
18217 | 1125 |
|
18756 | 1126 |
fun get_serializer target = |
1127 |
case Symtab.lookup (!serializers) target |
|
1128 |
of SOME seri => seri |
|
19008 | 1129 |
| NONE => Scan.fail_with (fn _ => "unknown code target language: " ^ quote target) (); |
18335 | 1130 |
|
18516 | 1131 |
fun map_module f = |
18702 | 1132 |
map_codegen_data (fn (modl, gens, target_data, logic_data) => |
1133 |
(f modl, gens, target_data, logic_data)); |
|
18516 | 1134 |
|
19136 | 1135 |
fun expand_module init gen arg thy = |
18516 | 1136 |
(#modl o CodegenData.get) thy |
19136 | 1137 |
|> start_transact init (gen thy (mk_tabs thy) arg) |
18516 | 1138 |
|-> (fn x:'a => fn modl => (x, map_module (K modl) thy)); |
1139 |
||
1140 |
fun rename_inconsistent thy = |
|
18217 | 1141 |
let |
18516 | 1142 |
fun get_inconsistent thyname = |
1143 |
let |
|
1144 |
val thy = theory thyname; |
|
1145 |
fun own_tables get = |
|
1146 |
(get thy) |
|
1147 |
|> fold (Symtab.fold (Symtab.remove (K true)) o get) (Theory.parents_of thy) |
|
1148 |
|> Symtab.keys; |
|
1149 |
val names = own_tables (#2 o #types o Type.rep_tsig o Sign.tsig_of) |
|
18960 | 1150 |
@ own_tables (#2 o #constants o Consts.dest o #consts o Sign.rep_sg); |
18516 | 1151 |
fun diff names = |
1152 |
fold (fn name => |
|
1153 |
if is_prefix (op =) (NameSpace.unpack thyname) (NameSpace.unpack name) |
|
1154 |
then I |
|
1155 |
else cons (name, NameSpace.append thyname (NameSpace.base name))) names []; |
|
1156 |
in diff names end; |
|
1157 |
val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat; |
|
1158 |
fun add (src, dst) thy = |
|
1159 |
if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src |
|
1160 |
then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy) |
|
1161 |
else add_alias (src, dst) thy |
|
1162 |
in fold add inconsistent thy end; |
|
1163 |
||
18517 | 1164 |
fun ensure_datatype_case_consts get_datatype_case_consts get_case_const_data thy = |
1165 |
let |
|
1166 |
fun ensure case_c thy = |
|
1167 |
if |
|
1168 |
Symtab.defined ((#appconst o #gens o CodegenData.get) thy) case_c |
|
1169 |
then |
|
1170 |
(warning ("case constant " ^ quote case_c ^ " already present in application table, will not overwrite"); thy) |
|
1171 |
else |
|
18702 | 1172 |
add_case_const_i get_case_const_data case_c thy; |
18517 | 1173 |
in |
1174 |
fold ensure (get_datatype_case_consts thy) thy |
|
1175 |
end; |
|
1176 |
||
19150 | 1177 |
fun codegen_term t thy = |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1178 |
thy |
19177 | 1179 |
|> expand_module NONE exprsgen_term [Codegen.preprocess_term thy t] |
19150 | 1180 |
|-> (fn [t] => pair t); |
19136 | 1181 |
|
1182 |
val is_dtcon = has_nsp nsp_dtcon; |
|
1183 |
||
1184 |
fun consts_of_idfs thy = |
|
19177 | 1185 |
map (the o const_of_idf thy (mk_tabs thy)); |
19150 | 1186 |
|
1187 |
fun idfs_of_consts thy = |
|
1188 |
map (idf_of_const thy (mk_tabs thy)); |
|
1189 |
||
1190 |
val get_root_module = (#modl o CodegenData.get); |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1191 |
|
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1192 |
fun get_ml_fun_datatype thy resolv = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1193 |
let |
19150 | 1194 |
val target_data = |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1195 |
((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1196 |
in |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1197 |
CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1198 |
((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1199 |
(Option.map fst oo Symtab.lookup o #syntax_const) target_data) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1200 |
resolv |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1201 |
end; |
18516 | 1202 |
|
1203 |
||
1204 |
(** target languages **) |
|
1205 |
||
1206 |
(* primitive definitions *) |
|
1207 |
||
18702 | 1208 |
fun read_typ thy = |
1209 |
Sign.read_typ (thy, K NONE); |
|
1210 |
||
19136 | 1211 |
fun read_const thy = |
1212 |
(dest_Const o Sign.read_term thy); |
|
18517 | 1213 |
|
18963 | 1214 |
fun read_quote get reader gen raw thy = |
18912 | 1215 |
thy |
18963 | 1216 |
|> expand_module ((SOME o get) thy) |
19136 | 1217 |
(fn thy => fn tabs => gen thy tabs o single o reader thy) raw |
18912 | 1218 |
|-> (fn [x] => pair x); |
18702 | 1219 |
|
18963 | 1220 |
fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) thy = |
18516 | 1221 |
let |
18702 | 1222 |
val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target |
18516 | 1223 |
then () else error ("unknown target language: " ^ quote target); |
1224 |
val tabs = mk_tabs thy; |
|
1225 |
val name = prep_name thy tabs raw_name; |
|
1226 |
val primdef = prep_primdef raw_primdef; |
|
18217 | 1227 |
in |
18516 | 1228 |
thy |
18963 | 1229 |
|> map_module (CodegenThingol.add_prim name (target, primdef)) |
18217 | 1230 |
end; |
1231 |
||
18516 | 1232 |
val add_prim_i = gen_add_prim ((K o K) I) I; |
1233 |
val add_prim_class = gen_add_prim |
|
1234 |
(fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy)) |
|
18963 | 1235 |
CodegenSerializer.parse_targetdef; |
18516 | 1236 |
val add_prim_tyco = gen_add_prim |
1237 |
(fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy)) |
|
18963 | 1238 |
CodegenSerializer.parse_targetdef; |
18516 | 1239 |
val add_prim_const = gen_add_prim |
18517 | 1240 |
(fn thy => fn tabs => idf_of_const thy tabs o read_const thy) |
18963 | 1241 |
CodegenSerializer.parse_targetdef; |
18516 | 1242 |
|
19008 | 1243 |
val ensure_prim = map_module oo CodegenThingol.ensure_prim; |
18217 | 1244 |
|
18517 | 1245 |
|
18217 | 1246 |
(* syntax *) |
1247 |
||
18865 | 1248 |
fun gen_add_syntax_class prep_class class target pretty thy = |
1249 |
thy |
|
1250 |
|> map_codegen_data |
|
1251 |
(fn (modl, gens, target_data, logic_data) => |
|
1252 |
(modl, gens, |
|
1253 |
target_data |> Symtab.map_entry target |
|
1254 |
(map_target_data |
|
1255 |
(fn (syntax_class, syntax_tyco, syntax_const) => |
|
1256 |
(syntax_class |
|
1257 |
|> Symtab.update (prep_class thy class, pretty), syntax_tyco, syntax_const))), |
|
1258 |
logic_data)); |
|
1259 |
||
1260 |
val add_syntax_class = gen_add_syntax_class Sign.intern_class; |
|
1261 |
||
18963 | 1262 |
fun parse_syntax_tyco raw_tyco = |
18217 | 1263 |
let |
18963 | 1264 |
fun check_tyco thy tyco = |
1265 |
if Sign.declared_tyname thy tyco |
|
1266 |
then tyco |
|
1267 |
else error ("no such type constructor: " ^ quote tyco); |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1268 |
fun prep_tyco thy raw_tyco = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1269 |
raw_tyco |
18963 | 1270 |
|> Sign.intern_type thy |
1271 |
|> check_tyco thy |
|
1272 |
|> idf_of_name thy nsp_tyco; |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1273 |
fun no_args_tyco thy raw_tyco = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1274 |
AList.lookup (op =) ((NameSpace.dest_table o #types o Type.rep_tsig o Sign.tsig_of) thy) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1275 |
(Sign.intern_type thy raw_tyco) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1276 |
|> (fn SOME ((Type.LogicalType i), _) => i); |
18963 | 1277 |
fun mk reader target thy = |
18702 | 1278 |
let |
18756 | 1279 |
val _ = get_serializer target; |
18702 | 1280 |
val tyco = prep_tyco thy raw_tyco; |
1281 |
in |
|
1282 |
thy |
|
1283 |
|> ensure_prim tyco target |
|
1284 |
|> reader |
|
1285 |
|-> (fn pretty => map_codegen_data |
|
1286 |
(fn (modl, gens, target_data, logic_data) => |
|
1287 |
(modl, gens, |
|
1288 |
target_data |> Symtab.map_entry target |
|
1289 |
(map_target_data |
|
18865 | 1290 |
(fn (syntax_class, syntax_tyco, syntax_const) => |
1291 |
(syntax_class, syntax_tyco |> Symtab.update |
|
18702 | 1292 |
(tyco, (pretty, stamp ())), |
1293 |
syntax_const))), |
|
1294 |
logic_data))) |
|
1295 |
end; |
|
18217 | 1296 |
in |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1297 |
CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1298 |
(read_quote (fn thy => prep_tyco thy raw_tyco) read_typ exprsgen_type) |
18702 | 1299 |
#-> (fn reader => pair (mk reader)) |
18217 | 1300 |
end; |
1301 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1302 |
fun add_pretty_syntax_const c target pretty = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1303 |
map_codegen_data |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1304 |
(fn (modl, gens, target_data, logic_data) => |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1305 |
(modl, gens, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1306 |
target_data |> Symtab.map_entry target |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1307 |
(map_target_data |
18865 | 1308 |
(fn (syntax_class, syntax_tyco, syntax_const) => |
1309 |
(syntax_class, syntax_tyco, |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1310 |
syntax_const |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1311 |
|> Symtab.update |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1312 |
(c, (pretty, stamp ()))))), |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1313 |
logic_data)); |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1314 |
|
18963 | 1315 |
fun parse_syntax_const raw_const = |
18217 | 1316 |
let |
18963 | 1317 |
fun prep_const thy raw_const = |
1318 |
idf_of_const thy (mk_tabs thy) (read_const thy raw_const); |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1319 |
fun no_args_const thy raw_const = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1320 |
(length o fst o strip_type o snd o read_const thy) raw_const; |
18963 | 1321 |
fun mk reader target thy = |
18702 | 1322 |
let |
18756 | 1323 |
val _ = get_serializer target; |
18963 | 1324 |
val c = prep_const thy raw_const; |
18702 | 1325 |
in |
1326 |
thy |
|
1327 |
|> ensure_prim c target |
|
1328 |
|> reader |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1329 |
|-> (fn pretty => add_pretty_syntax_const c target pretty) |
18702 | 1330 |
end; |
18217 | 1331 |
in |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1332 |
CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
1333 |
(read_quote (fn thy => prep_const thy raw_const) Sign.read_term exprsgen_term) |
18702 | 1334 |
#-> (fn reader => pair (mk reader)) |
18217 | 1335 |
end; |
1336 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1337 |
fun add_pretty_list raw_nil raw_cons (target, seri) thy = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1338 |
let |
18756 | 1339 |
val _ = get_serializer target; |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1340 |
val tabs = mk_tabs thy; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1341 |
fun mk_const raw_name = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1342 |
let |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1343 |
val name = Sign.intern_const thy raw_name; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1344 |
in idf_of_const thy tabs (name, Sign.the_const_type thy name) end; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1345 |
val nil' = mk_const raw_nil; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1346 |
val cons' = mk_const raw_cons; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1347 |
val pr' = CodegenSerializer.pretty_list nil' cons' seri; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1348 |
in |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1349 |
thy |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1350 |
|> ensure_prim cons' target |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1351 |
|> add_pretty_syntax_const cons' target pr' |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1352 |
end; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1353 |
|
18217 | 1354 |
|
18516 | 1355 |
|
18756 | 1356 |
(** toplevel interface **) |
1357 |
||
1358 |
local |
|
19150 | 1359 |
|
18756 | 1360 |
fun generate_code (SOME raw_consts) thy = |
19150 | 1361 |
let |
18756 | 1362 |
val consts = map (read_const thy) raw_consts; |
1363 |
in |
|
1364 |
thy |
|
19136 | 1365 |
|> expand_module NONE (fold_map oo ensure_def_const) consts |
18756 | 1366 |
|-> (fn cs => pair (SOME cs)) |
1367 |
end |
|
1368 |
| generate_code NONE thy = |
|
1369 |
(NONE, thy); |
|
1370 |
||
1371 |
fun serialize_code target seri raw_consts thy = |
|
18217 | 1372 |
let |
18756 | 1373 |
fun serialize cs thy = |
18702 | 1374 |
let |
18756 | 1375 |
val module = (#modl o CodegenData.get) thy; |
18702 | 1376 |
val target_data = |
1377 |
thy |
|
1378 |
|> CodegenData.get |
|
1379 |
|> #target_data |
|
1380 |
|> (fn data => (the oo Symtab.lookup) data target); |
|
18756 | 1381 |
in (seri ( |
18865 | 1382 |
(Symtab.lookup o #syntax_class) target_data, |
18702 | 1383 |
(Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, |
1384 |
(Option.map fst oo Symtab.lookup o #syntax_const) target_data |
|
18850 | 1385 |
) cs module : unit; thy) end; |
18217 | 1386 |
in |
1387 |
thy |
|
18756 | 1388 |
|> generate_code raw_consts |
1389 |
|-> (fn cs => serialize cs) |
|
18217 | 1390 |
end; |
1391 |
||
1392 |
structure P = OuterParse |
|
1393 |
and K = OuterKeyword |
|
1394 |
||
1395 |
in |
|
1396 |
||
18850 | 1397 |
val (generateK, serializeK, |
18517 | 1398 |
primclassK, primtycoK, primconstK, |
18865 | 1399 |
syntax_classK, syntax_tycoK, syntax_constK, aliasK) = |
18850 | 1400 |
("code_generate", "code_serialize", |
18517 | 1401 |
"code_primclass", "code_primtyco", "code_primconst", |
18865 | 1402 |
"code_syntax_class", "code_syntax_tyco", "code_syntax_const", "code_alias"); |
18335 | 1403 |
|
18217 | 1404 |
val generateP = |
18282 | 1405 |
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( |
19136 | 1406 |
Scan.repeat1 P.term |
18756 | 1407 |
>> (fn raw_consts => |
1408 |
Toplevel.theory (generate_code (SOME raw_consts) #> snd)) |
|
18217 | 1409 |
); |
1410 |
||
1411 |
val serializeP = |
|
18282 | 1412 |
OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( |
18217 | 1413 |
P.name |
19136 | 1414 |
-- Scan.option (Scan.repeat1 P.term) |
18756 | 1415 |
#-> (fn (target, raw_consts) => |
18850 | 1416 |
P.$$$ "(" |
1417 |
|-- get_serializer target |
|
1418 |
--| P.$$$ ")" |
|
18756 | 1419 |
>> (fn seri => |
1420 |
Toplevel.theory (serialize_code target seri raw_consts) |
|
1421 |
)) |
|
18217 | 1422 |
); |
1423 |
||
1424 |
val aliasP = |
|
18282 | 1425 |
OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( |
18702 | 1426 |
Scan.repeat1 (P.name -- P.name) |
1427 |
>> (Toplevel.theory oo fold) add_alias |
|
18217 | 1428 |
); |
1429 |
||
18517 | 1430 |
val primclassP = |
1431 |
OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl ( |
|
1432 |
P.xname |
|
1433 |
-- Scan.repeat1 (P.name -- P.text) |
|
18963 | 1434 |
>> (fn (raw_class, primdefs) => |
1435 |
(Toplevel.theory oo fold) (add_prim_class raw_class) primdefs) |
|
18517 | 1436 |
); |
1437 |
||
1438 |
val primtycoP = |
|
1439 |
OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl ( |
|
1440 |
P.xname |
|
1441 |
-- Scan.repeat1 (P.name -- P.text) |
|
18963 | 1442 |
>> (fn (raw_tyco, primdefs) => |
1443 |
(Toplevel.theory oo fold) (add_prim_tyco raw_tyco) primdefs) |
|
18517 | 1444 |
); |
1445 |
||
1446 |
val primconstP = |
|
1447 |
OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl ( |
|
19136 | 1448 |
P.term |
18517 | 1449 |
-- Scan.repeat1 (P.name -- P.text) |
18963 | 1450 |
>> (fn (raw_const, primdefs) => |
1451 |
(Toplevel.theory oo fold) (add_prim_const raw_const) primdefs) |
|
18517 | 1452 |
); |
1453 |
||
18865 | 1454 |
val syntax_classP = |
1455 |
OuterSyntax.command syntax_tycoK "define code syntax for class" K.thy_decl ( |
|
1456 |
Scan.repeat1 ( |
|
1457 |
P.xname |
|
1458 |
-- Scan.repeat1 ( |
|
1459 |
P.name -- P.string |
|
1460 |
) |
|
1461 |
) |
|
1462 |
>> (Toplevel.theory oo fold) (fn (raw_class, syns) => |
|
1463 |
fold (fn (target, p) => add_syntax_class raw_class target p) syns) |
|
1464 |
); |
|
1465 |
||
18217 | 1466 |
val syntax_tycoP = |
1467 |
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( |
|
18702 | 1468 |
Scan.repeat1 ( |
1469 |
P.xname |
|
18963 | 1470 |
#-> (fn raw_tyco => Scan.repeat1 ( |
1471 |
P.name -- parse_syntax_tyco raw_tyco |
|
1472 |
)) |
|
18702 | 1473 |
) |
18963 | 1474 |
>> (Toplevel.theory oo fold o fold) |
1475 |
(fn (target, modifier) => modifier target) |
|
18217 | 1476 |
); |
1477 |
||
1478 |
val syntax_constP = |
|
1479 |
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl ( |
|
18702 | 1480 |
Scan.repeat1 ( |
19136 | 1481 |
P.term |
18963 | 1482 |
#-> (fn raw_const => Scan.repeat1 ( |
1483 |
P.name -- parse_syntax_const raw_const |
|
1484 |
)) |
|
18702 | 1485 |
) |
19008 | 1486 |
>> (Toplevel.theory oo fold o fold) |
18963 | 1487 |
(fn (target, modifier) => modifier target) |
18217 | 1488 |
); |
1489 |
||
18850 | 1490 |
val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP, |
18517 | 1491 |
primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP]; |
18217 | 1492 |
|
1493 |
||
18516 | 1494 |
|
18708 | 1495 |
(** theory setup **) |
18516 | 1496 |
|
18850 | 1497 |
val _ = Context.add_setup ( |
1498 |
add_eqextr ("defs", eqextr_defs) |
|
1499 |
); |
|
18217 | 1500 |
|
1501 |
end; (* local *) |
|
1502 |
||
1503 |
end; (* struct *) |