124 |
124 |
125 datatype target = Target of { |
125 datatype target = Target of { |
126 serial: serial, |
126 serial: serial, |
127 serializer: serializer_entry, |
127 serializer: serializer_entry, |
128 reserved: string list, |
128 reserved: string list, |
129 includes: Pretty.T Symtab.table, |
129 includes: (Pretty.T * string list) Symtab.table, |
130 name_syntax_table: name_syntax_table, |
130 name_syntax_table: name_syntax_table, |
131 module_alias: string Symtab.table |
131 module_alias: string Symtab.table |
132 }; |
132 }; |
133 |
133 |
134 fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) = |
134 fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) = |
308 fun add sym syms = if member (op =) syms sym |
308 fun add sym syms = if member (op =) syms sym |
309 then error ("Reserved symbol " ^ quote sym ^ " already declared") |
309 then error ("Reserved symbol " ^ quote sym ^ " already declared") |
310 else insert (op =) sym syms |
310 else insert (op =) sym syms |
311 in map_reserved target o add end; |
311 in map_reserved target o add end; |
312 |
312 |
313 fun add_include target = |
313 fun gen_add_include read_const target args thy = |
314 let |
314 let |
315 fun add (name, SOME content) incls = |
315 fun add (name, SOME (content, raw_cs)) incls = |
316 let |
316 let |
317 val _ = if Symtab.defined incls name |
317 val _ = if Symtab.defined incls name |
318 then warning ("Overwriting existing include " ^ name) |
318 then warning ("Overwriting existing include " ^ name) |
319 else (); |
319 else (); |
320 in Symtab.update (name, str content) incls end |
320 val cs = map (read_const thy) raw_cs; |
321 | add (name, NONE) incls = |
321 in Symtab.update (name, (str content, cs)) incls end |
322 Symtab.delete name incls; |
322 | add (name, NONE) incls = Symtab.delete name incls; |
323 in map_includes target o add end; |
323 in map_includes target (add args) thy end; |
|
324 |
|
325 val add_include = gen_add_include Code_Unit.check_const; |
|
326 val add_include_cmd = gen_add_include Code_Unit.read_const; |
324 |
327 |
325 fun add_module_alias target = |
328 fun add_module_alias target = |
326 map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename; |
329 map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename; |
327 |
330 |
328 fun gen_allow_abort prep_const raw_c thy = |
331 fun gen_allow_abort prep_const raw_c thy = |
392 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let |
395 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let |
393 val Code_Thingol.Class (class, _) = Graph.get_node program class |
396 val Code_Thingol.Class (class, _) = Graph.get_node program class |
394 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco |
397 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco |
395 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end |
398 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end |
396 |
399 |
397 fun invoke_serializer thy abortable serializer reserved includes |
400 fun invoke_serializer thy abortable serializer reserved abs_includes |
398 module_alias class instance tyco const module args naming program2 names1 = |
401 module_alias class instance tyco const module args naming program2 names1 = |
399 let |
402 let |
400 fun distill_names lookup_name src_tab = Symtab.empty |
403 fun distill_names lookup_name src_tab = Symtab.empty |
401 |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier |
404 |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier |
402 of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab) |
405 of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab) |
409 val (names_const, const') = distill_names Code_Thingol.lookup_const const; |
412 val (names_const, const') = distill_names Code_Thingol.lookup_const const; |
410 val names_hidden = names_class @ names_inst @ names_tyco @ names_const; |
413 val names_hidden = names_class @ names_inst @ names_tyco @ names_const; |
411 val names2 = subtract (op =) names_hidden names1; |
414 val names2 = subtract (op =) names_hidden names1; |
412 val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; |
415 val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; |
413 val names_all = Graph.all_succs program2 names2; |
416 val names_all = Graph.all_succs program2 names2; |
|
417 val includes = abs_includes names_all; |
414 val program4 = Graph.subgraph (member (op =) names_all) program3; |
418 val program4 = Graph.subgraph (member (op =) names_all) program3; |
415 val empty_funs = filter_out (member (op =) abortable) |
419 val empty_funs = filter_out (member (op =) abortable) |
416 (Code_Thingol.empty_funs program3); |
420 (Code_Thingol.empty_funs program3); |
417 val _ = if null empty_funs then () else error ("No defining equations for " |
421 val _ = if null empty_funs then () else error ("No defining equations for " |
418 ^ commas (map (Sign.extern_const thy) empty_funs)); |
422 ^ commas (map (Sign.extern_const thy) empty_funs)); |
421 (Symtab.lookup module_alias) (Symtab.lookup class') |
425 (Symtab.lookup module_alias) (Symtab.lookup class') |
422 (Symtab.lookup tyco') (Symtab.lookup const') |
426 (Symtab.lookup tyco') (Symtab.lookup const') |
423 naming program4 names2 |
427 naming program4 names2 |
424 end; |
428 end; |
425 |
429 |
426 fun mount_serializer thy alt_serializer target module args naming program = |
430 fun mount_serializer thy alt_serializer target module args naming program names = |
427 let |
431 let |
428 val (targets, abortable) = CodeTargetData.get thy; |
432 val (targets, abortable) = CodeTargetData.get thy; |
429 fun collapse_hierarchy target = |
433 fun collapse_hierarchy target = |
430 let |
434 let |
431 val data = case Symtab.lookup targets target |
435 val data = case Symtab.lookup targets target |
439 end; |
443 end; |
440 val (modify, data) = collapse_hierarchy target; |
444 val (modify, data) = collapse_hierarchy target; |
441 val (serializer, _) = the_default (case the_serializer data |
445 val (serializer, _) = the_default (case the_serializer data |
442 of Serializer seri => seri) alt_serializer; |
446 of Serializer seri => seri) alt_serializer; |
443 val reserved = the_reserved data; |
447 val reserved = the_reserved data; |
444 val includes = Symtab.dest (the_includes data); |
448 fun select_include names_all (name, (content, cs)) = |
|
449 if null cs then SOME (name, content) |
|
450 else if exists (fn c => case Code_Thingol.lookup_const naming c |
|
451 of SOME name => member (op =) names_all name |
|
452 | NONE => false) cs |
|
453 then SOME (name, content) else NONE; |
|
454 fun includes names_all = map_filter (select_include names_all) |
|
455 ((Symtab.dest o the_includes) data); |
445 val module_alias = the_module_alias data; |
456 val module_alias = the_module_alias data; |
446 val { class, instance, tyco, const } = the_name_syntax data; |
457 val { class, instance, tyco, const } = the_name_syntax data; |
447 in |
458 in |
448 invoke_serializer thy abortable serializer reserved |
459 invoke_serializer thy abortable serializer reserved |
449 includes module_alias class instance tyco const module args naming (modify program) |
460 includes module_alias class instance tyco const module args naming (modify program) names |
450 end; |
461 end; |
451 |
462 |
452 in |
463 in |
453 |
464 |
454 fun serialize thy = mount_serializer thy NONE; |
465 fun serialize thy = mount_serializer thy NONE; |
455 |
466 |
456 fun serialize_custom thy (target_name, seri) naming program cs = |
467 fun serialize_custom thy (target_name, seri) naming program names = |
457 mount_serializer thy (SOME seri) target_name NONE [] naming program cs (String []) |
468 mount_serializer thy (SOME seri) target_name NONE [] naming program names (String []) |
458 |> the; |
469 |> the; |
459 |
470 |
460 end; (* local *) |
471 end; (* local *) |
461 |
472 |
462 fun parse_args f args = |
473 fun parse_args f args = |
563 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds) |
574 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds) |
564 ); |
575 ); |
565 |
576 |
566 val _ = |
577 val _ = |
567 OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl ( |
578 OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl ( |
568 P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s)) |
579 P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE |
569 >> (fn ((target, name), content) => (Toplevel.theory o add_include target) |
580 | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME)) |
570 (name, content)) |
581 >> (fn ((target, name), content_consts) => |
|
582 (Toplevel.theory o add_include_cmd target) (name, content_consts)) |
571 ); |
583 ); |
572 |
584 |
573 val _ = |
585 val _ = |
574 OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl ( |
586 OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl ( |
575 P.name -- Scan.repeat1 (P.name -- P.name) |
587 P.name -- Scan.repeat1 (P.name -- P.name) |