42 |
42 |
43 val allow_abort: string -> theory -> theory |
43 val allow_abort: string -> theory -> theory |
44 val add_syntax_class: string -> class -> string option -> theory -> theory |
44 val add_syntax_class: string -> class -> string option -> theory -> theory |
45 val add_syntax_inst: string -> string * class -> bool -> theory -> theory |
45 val add_syntax_inst: string -> string * class -> bool -> theory -> theory |
46 val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory |
46 val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory |
47 val add_syntax_const: string -> string -> const_syntax option -> theory -> theory |
47 val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory |
48 val add_reserved: string -> string -> theory -> theory |
48 val add_reserved: string -> string -> theory -> theory |
49 end; |
49 end; |
50 |
50 |
51 structure Code_Target : CODE_TARGET = |
51 structure Code_Target : CODE_TARGET = |
52 struct |
52 struct |
84 |
84 |
85 datatype name_syntax_table = NameSyntaxTable of { |
85 datatype name_syntax_table = NameSyntaxTable of { |
86 class: string Symtab.table, |
86 class: string Symtab.table, |
87 instance: unit Symreltab.table, |
87 instance: unit Symreltab.table, |
88 tyco: tyco_syntax Symtab.table, |
88 tyco: tyco_syntax Symtab.table, |
89 const: const_syntax Symtab.table |
89 const: proto_const_syntax Symtab.table |
90 }; |
90 }; |
91 |
91 |
92 fun mk_name_syntax_table ((class, instance), (tyco, const)) = |
92 fun mk_name_syntax_table ((class, instance), (tyco, const)) = |
93 NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const }; |
93 NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const }; |
94 fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) = |
94 fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) = |
110 -> (string * Pretty.T) list (*includes*) |
110 -> (string * Pretty.T) list (*includes*) |
111 -> (string -> string option) (*module aliasses*) |
111 -> (string -> string option) (*module aliasses*) |
112 -> (string -> string option) (*class syntax*) |
112 -> (string -> string option) (*class syntax*) |
113 -> (string -> tyco_syntax option) |
113 -> (string -> tyco_syntax option) |
114 -> (string -> const_syntax option) |
114 -> (string -> const_syntax option) |
115 -> Code_Thingol.naming |
|
116 -> Code_Thingol.program |
115 -> Code_Thingol.program |
117 -> string list (*selected statements*) |
116 -> string list (*selected statements*) |
118 -> serialization; |
117 -> serialization; |
119 |
118 |
120 datatype serializer_entry = Serializer of serializer * literals |
119 datatype serializer_entry = Serializer of serializer * literals |
400 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let |
399 | Code_Thingol.Classinst ((class, (tyco, _)), _) => let |
401 val Code_Thingol.Class (class, _) = Graph.get_node program class |
400 val Code_Thingol.Class (class, _) = Graph.get_node program class |
402 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco |
401 val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco |
403 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end |
402 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end |
404 |
403 |
405 fun invoke_serializer thy abortable serializer reserved abs_includes |
404 fun activate_syntax lookup_name src_tab = Symtab.empty |
|
405 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier |
|
406 of SOME name => (SOME name, |
|
407 Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab) |
|
408 | NONE => (NONE, tab)) (Symtab.keys src_tab) |
|
409 |>> map_filter I; |
|
410 |
|
411 fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming) |
|
412 |> fold_map (fn thing_identifier => fn (tab, naming) => |
|
413 case Code_Thingol.lookup_const naming thing_identifier |
|
414 of SOME name => let |
|
415 val (syn, naming') = Code_Printer.activate_const_syntax thy |
|
416 literals (the (Symtab.lookup src_tab thing_identifier)) naming |
|
417 in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end |
|
418 | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab) |
|
419 |>> map_filter I; |
|
420 |
|
421 fun invoke_serializer thy abortable serializer literals reserved abs_includes |
406 module_alias class instance tyco const module args naming program2 names1 = |
422 module_alias class instance tyco const module args naming program2 names1 = |
407 let |
423 let |
408 fun distill_names lookup_name src_tab = Symtab.empty |
424 val (names_class, class') = |
409 |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier |
425 activate_syntax (Code_Thingol.lookup_class naming) class; |
410 of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab) |
|
411 | NONE => (NONE, tab)) (Symtab.keys src_tab) |
|
412 |>> map_filter I; |
|
413 val (names_class, class') = distill_names Code_Thingol.lookup_class class; |
|
414 val names_inst = map_filter (Code_Thingol.lookup_instance naming) |
426 val names_inst = map_filter (Code_Thingol.lookup_instance naming) |
415 (Symreltab.keys instance); |
427 (Symreltab.keys instance); |
416 val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco; |
428 val (names_tyco, tyco') = |
417 val (names_const, const') = distill_names Code_Thingol.lookup_const const; |
429 activate_syntax (Code_Thingol.lookup_tyco naming) tyco; |
|
430 val (names_const, (const', _)) = |
|
431 activate_const_syntax thy literals const naming; |
418 val names_hidden = names_class @ names_inst @ names_tyco @ names_const; |
432 val names_hidden = names_class @ names_inst @ names_tyco @ names_const; |
419 val names2 = subtract (op =) names_hidden names1; |
433 val names2 = subtract (op =) names_hidden names1; |
420 val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; |
434 val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; |
421 val names_all = Graph.all_succs program3 names2; |
435 val names_all = Graph.all_succs program3 names2; |
422 val includes = abs_includes names_all; |
436 val includes = abs_includes names_all; |
427 ^ commas (map (Sign.extern_const thy) empty_funs)); |
441 ^ commas (map (Sign.extern_const thy) empty_funs)); |
428 in |
442 in |
429 serializer module args (labelled_name thy program2) reserved includes |
443 serializer module args (labelled_name thy program2) reserved includes |
430 (Symtab.lookup module_alias) (Symtab.lookup class') |
444 (Symtab.lookup module_alias) (Symtab.lookup class') |
431 (Symtab.lookup tyco') (Symtab.lookup const') |
445 (Symtab.lookup tyco') (Symtab.lookup const') |
432 naming program4 names2 |
446 program4 names2 |
433 end; |
447 end; |
434 |
448 |
435 fun mount_serializer thy alt_serializer target module args naming program names = |
449 fun mount_serializer thy alt_serializer target module args naming program names = |
436 let |
450 let |
437 val (targets, abortable) = CodeTargetData.get thy; |
451 val (targets, abortable) = CodeTargetData.get thy; |
458 then SOME (name, content) else NONE; |
472 then SOME (name, content) else NONE; |
459 fun includes names_all = map_filter (select_include names_all) |
473 fun includes names_all = map_filter (select_include names_all) |
460 ((Symtab.dest o the_includes) data); |
474 ((Symtab.dest o the_includes) data); |
461 val module_alias = the_module_alias data; |
475 val module_alias = the_module_alias data; |
462 val { class, instance, tyco, const } = the_name_syntax data; |
476 val { class, instance, tyco, const } = the_name_syntax data; |
|
477 val literals = the_literals thy target; |
463 in |
478 in |
464 invoke_serializer thy abortable serializer reserved |
479 invoke_serializer thy abortable serializer literals reserved |
465 includes module_alias class instance tyco const module args naming (modify program) names |
480 includes module_alias class instance tyco const module args naming (modify program) names |
466 end; |
481 end; |
467 |
482 |
468 in |
483 in |
469 |
484 |