src/Tools/code/code_target.ML
changeset 30240 5b25fee0362c
parent 28926 530b83967c82
child 30242 aea5d7fa7ef5
equal deleted inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c
     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')