src/Tools/Code/code_target.ML
changeset 39484 505f95975a5a
parent 39480 a2ed61449dcc
child 39646 64fdbee67135
equal deleted inserted replaced
39482:1c37d19e3d58 39484:505f95975a5a
   239 
   239 
   240 fun the_literals thy = #literals o the_fundamental thy;
   240 fun the_literals thy = #literals o the_fundamental thy;
   241 
   241 
   242 local
   242 local
   243 
   243 
   244 fun activate_target_for thy target naming program =
   244 fun activate_target thy target =
   245   let
   245   let
   246     val ((targets, abortable), default_width) = Targets.get thy;
   246     val ((targets, abortable), default_width) = Targets.get thy;
   247     fun collapse_hierarchy target =
   247     fun collapse_hierarchy target =
   248       let
   248       let
   249         val data = case Symtab.lookup targets target
   249         val data = case Symtab.lookup targets target
   250          of SOME data => data
   250          of SOME data => data
   251           | NONE => error ("Unknown code target language: " ^ quote target);
   251           | NONE => error ("Unknown code target language: " ^ quote target);
   252       in case the_description data
   252       in case the_description data
   253        of Fundamental _ => (I, data)
   253        of Fundamental _ => (K I, data)
   254         | Extension (super, modify) => let
   254         | Extension (super, modify) => let
   255             val (modify', data') = collapse_hierarchy super
   255             val (modify', data') = collapse_hierarchy super
   256           in (modify' #> modify naming, merge_target false target (data', data)) end
   256           in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
   257       end;
   257       end;
   258     val (modify, data) = collapse_hierarchy target;
   258     val (modify, data) = collapse_hierarchy target;
   259   in (default_width, abortable, data, modify program) end;
   259   in (default_width, abortable, data, modify) end;
   260 
   260 
   261 fun activate_syntax lookup_name src_tab = Symtab.empty
   261 fun activate_syntax lookup_name src_tab = Symtab.empty
   262   |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
   262   |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
   263        of SOME name => (SOME name,
   263        of SOME name => (SOME name,
   264             Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
   264             Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
   301     val _ = if null empty_funs then () else error ("No code equations for "
   301     val _ = if null empty_funs then () else error ("No code equations for "
   302       ^ commas (map (Sign.extern_const thy) empty_funs));
   302       ^ commas (map (Sign.extern_const thy) empty_funs));
   303     val program4 = Graph.subgraph (member (op =) names4) program3;
   303     val program4 = Graph.subgraph (member (op =) names4) program3;
   304   in (names4, program4) end;
   304   in (names4, program4) end;
   305 
   305 
   306 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
   306 fun invoke_serializer thy abortable serializer literals reserved all_includes
   307     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   307     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   308     module_name args naming proto_program names =
   308     module_name args naming proto_program names =
   309   let
   309   let
   310     val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
   310     val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
   311       activate_symbol_syntax thy literals naming
   311       activate_symbol_syntax thy literals naming
   312         proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
   312         proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
   313     val (names_all, program) = project_program thy abortable names_hidden names proto_program;
   313     val (names_all, program) = project_program thy abortable names_hidden names proto_program;
   314     val includes = abs_includes names_all;
   314     fun select_include (name, (content, cs)) =
       
   315       if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
       
   316        of SOME name => member (op =) names_all name
       
   317         | NONE => false) cs
       
   318       then SOME (name, content) else NONE;
       
   319     val includes = map_filter select_include (Symtab.dest all_includes);
   315   in
   320   in
   316     serializer args {
   321     serializer args {
   317       labelled_name = Code_Thingol.labelled_name thy proto_program,
   322       labelled_name = Code_Thingol.labelled_name thy proto_program,
   318       reserved_syms = reserved,
   323       reserved_syms = reserved,
   319       includes = includes,
   324       includes = includes,
   322       tyco_syntax = Symtab.lookup tyco_syntax,
   327       tyco_syntax = Symtab.lookup tyco_syntax,
   323       const_syntax = Symtab.lookup const_syntax,
   328       const_syntax = Symtab.lookup const_syntax,
   324       program = program }
   329       program = program }
   325   end;
   330   end;
   326 
   331 
   327 fun mount_serializer thy target some_width module_name args naming proto_program names =
   332 fun mount_serializer thy target some_width module_name args =
   328   let
   333   let
   329     val (default_width, abortable, data, program) =
   334     val (default_width, abortable, data, modify) = activate_target thy target;
   330       activate_target_for thy target naming proto_program;
       
   331     val serializer = case the_description data
   335     val serializer = case the_description data
   332      of Fundamental seri => #serializer seri;
   336      of Fundamental seri => #serializer seri;
   333     val reserved = the_reserved data;
   337     val reserved = the_reserved data;
   334     fun select_include names_all (name, (content, cs)) =
       
   335       if null cs then SOME (name, content)
       
   336       else if exists (fn c => case Code_Thingol.lookup_const naming c
       
   337        of SOME name => member (op =) names_all name
       
   338         | NONE => false) cs
       
   339       then SOME (name, content) else NONE;
       
   340     fun includes names_all = map_filter (select_include names_all)
       
   341       ((Symtab.dest o the_includes) data);
       
   342     val module_alias = the_module_alias data 
   338     val module_alias = the_module_alias data 
   343     val { class, instance, tyco, const } = the_symbol_syntax data;
   339     val { class, instance, tyco, const } = the_symbol_syntax data;
   344     val literals = the_literals thy target;
   340     val literals = the_literals thy target;
   345     val width = the_default default_width some_width;
   341     val width = the_default default_width some_width;
   346   in
   342   in fn naming => fn program => fn names =>
   347     invoke_serializer thy abortable serializer literals reserved
   343     invoke_serializer thy abortable serializer literals reserved
   348       includes module_alias class instance tyco const module_name args
   344       (the_includes data) module_alias class instance tyco const module_name args
   349         naming program names width
   345         naming (modify naming program) names width
   350   end;
   346   end;
   351 
   347 
   352 fun assert_module_name "" = error ("Empty module name not allowed.")
   348 fun assert_module_name "" = error ("Empty module name not allowed.")
   353   | assert_module_name module_name = module_name;
   349   | assert_module_name module_name = module_name;
   354 
   350 
   355 in
   351 in
   356 
   352 
   357 fun export_code_for thy some_path target some_width some_module_name args naming program names =
   353 fun export_code_for thy some_path target some_width module_name args =
   358   export some_path (mount_serializer thy target some_width some_module_name args naming program names);
   354   export some_path ooo mount_serializer thy target some_width module_name args;
   359 
   355 
   360 fun produce_code_for thy target some_width module_name args naming program names =
   356 fun produce_code_for thy target some_width module_name args =
   361   let
   357   let
   362     val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
   358     val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
   363   in (s, map deresolve names) end;
   359   in fn naming => fn program => fn names =>
   364 
   360     produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
   365 fun present_code_for thy target some_width module_name args naming program (names, selects) =
   361   end;
   366   present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
   362 
       
   363 fun present_code_for thy target some_width module_name args =
       
   364   let
       
   365     val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
       
   366   in fn naming => fn program => fn (names, selects) =>
       
   367     present selects (serializer naming program names)
       
   368   end;
   367 
   369 
   368 fun check_code_for thy target strict args naming program names_cs =
   370 fun check_code_for thy target strict args naming program names_cs =
   369   let
   371   let
   370     val module_name = "Code";
   372     val module_name = "Code";
   371     val { env_var, make_destination, make_command } =
   373     val { env_var, make_destination, make_command } =