equal
deleted
inserted
replaced
1 (* Title: Tools/code/code_target.ML |
1 (* Title: Tools/code/code_target.ML |
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
4 |
3 |
5 Serializer from intermediate language ("Thin-gol") to target languages. |
4 Serializer from intermediate language ("Thin-gol") to target languages. |
6 *) |
5 *) |
7 |
6 |
416 val names_all = Graph.all_succs program2 names2; |
415 val names_all = Graph.all_succs program2 names2; |
417 val includes = abs_includes names_all; |
416 val includes = abs_includes names_all; |
418 val program4 = Graph.subgraph (member (op =) names_all) program3; |
417 val program4 = Graph.subgraph (member (op =) names_all) program3; |
419 val empty_funs = filter_out (member (op =) abortable) |
418 val empty_funs = filter_out (member (op =) abortable) |
420 (Code_Thingol.empty_funs program3); |
419 (Code_Thingol.empty_funs program3); |
421 val _ = if null empty_funs then () else error ("No defining equations for " |
420 val _ = if null empty_funs then () else error ("No code equations for " |
422 ^ commas (map (Sign.extern_const thy) empty_funs)); |
421 ^ commas (map (Sign.extern_const thy) empty_funs)); |
423 in |
422 in |
424 serializer module args (labelled_name thy program2) reserved includes |
423 serializer module args (labelled_name thy program2) reserved includes |
425 (Symtab.lookup module_alias) (Symtab.lookup class') |
424 (Symtab.lookup module_alias) (Symtab.lookup class') |
426 (Symtab.lookup tyco') (Symtab.lookup const') |
425 (Symtab.lookup tyco') (Symtab.lookup const') |