# HG changeset patch # User haftmann # Date 1283258607 -7200 # Node ID 544f4702d621658dd8699b5cbfd8f5e1e922d1cb # Parent 24f82786cc570459ebab952891fcfc919d411925 tuned diff -r 24f82786cc57 -r 544f4702d621 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Aug 31 14:21:06 2010 +0200 +++ b/src/Tools/Code/code_target.ML Tue Aug 31 14:43:27 2010 +0200 @@ -239,6 +239,23 @@ local +fun activate_target_for thy target naming program = + let + val ((targets, abortable), default_width) = Targets.get thy; + fun collapse_hierarchy target = + let + val data = case Symtab.lookup targets target + of SOME data => data + | NONE => error ("Unknown code target language: " ^ quote target); + in case the_description data + of Fundamental _ => (I, data) + | Extension (super, modify) => let + val (modify', data') = collapse_hierarchy super + in (modify' #> modify naming, merge_target false target (data', data)) end + end; + val (modify, data) = collapse_hierarchy target; + in (default_width, abortable, data, modify program) end; + fun activate_syntax lookup_name src_tab = Symtab.empty |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier of SOME name => (SOME name, @@ -256,59 +273,63 @@ | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab) |>> map_filter I; -fun invoke_serializer thy abortable serializer literals reserved abs_includes - module_alias class instance tyco const module_name args naming program2 (names1, presentation_names) width = +fun activate_symbol_syntax thy literals naming + class_syntax instance_syntax tyco_syntax const_syntax = let - val (names_class, class') = - activate_syntax (Code_Thingol.lookup_class naming) class; + val (names_class, class_syntax') = + activate_syntax (Code_Thingol.lookup_class naming) class_syntax; val names_inst = map_filter (Code_Thingol.lookup_instance naming) - (Symreltab.keys instance); - val (names_tyco, tyco') = - activate_syntax (Code_Thingol.lookup_tyco naming) tyco; - val (names_const, (const', _)) = - activate_const_syntax thy literals const naming; - val names_hidden = names_class @ names_inst @ names_tyco @ names_const; + (Symreltab.keys instance_syntax); + val (names_tyco, tyco_syntax') = + activate_syntax (Code_Thingol.lookup_tyco naming) tyco_syntax; + val (names_const, (const_syntax', _)) = + activate_const_syntax thy literals const_syntax naming; + in + (names_class @ names_inst @ names_tyco @ names_const, + (class_syntax', tyco_syntax', const_syntax')) + end; + +fun project_program thy abortable names_hidden names1 program2 = + let val names2 = subtract (op =) names_hidden names1; val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; val names_all = Graph.all_succs program3 names2; - val includes = abs_includes names_all; - val program4 = Graph.subgraph (member (op =) names_all) program3; val empty_funs = filter_out (member (op =) abortable) (Code_Thingol.empty_funs program3); val _ = if null empty_funs then () else error ("No code equations for " ^ commas (map (Sign.extern_const thy) empty_funs)); + in (names_all, program3) end; + +fun invoke_serializer thy abortable serializer literals reserved abs_includes + module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax + module_name args naming proto_program (names, presentation_names) = + let + val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) = + activate_symbol_syntax thy literals naming + proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax; + val (names_all, program) = project_program thy abortable names_hidden names proto_program; + val includes = abs_includes names_all; in serializer args { - labelled_name = Code_Thingol.labelled_name thy program2, + labelled_name = Code_Thingol.labelled_name thy proto_program, reserved_syms = reserved, includes = includes, single_module = is_some module_name, module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias, - class_syntax = Symtab.lookup class', - tyco_syntax = Symtab.lookup tyco', - const_syntax = Symtab.lookup const', - program = program3, - names = names1, - presentation_names = presentation_names } width + class_syntax = Symtab.lookup class_syntax, + tyco_syntax = Symtab.lookup tyco_syntax, + const_syntax = Symtab.lookup const_syntax, + program = program, + names = names, + presentation_names = presentation_names } end; -fun mount_serializer thy target some_width raw_module_name args naming program names destination = +fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination = let - val ((targets, abortable), default_width) = Targets.get thy; - fun collapse_hierarchy target = - let - val data = case Symtab.lookup targets target - of SOME data => data - | NONE => error ("Unknown code target language: " ^ quote target); - in case the_description data - of Fundamental _ => (I, data) - | Extension (super, modify) => let - val (modify', data') = collapse_hierarchy super - in (modify' #> modify naming, merge_target false target (data', data)) end - end; - val (modify, data) = collapse_hierarchy target; + val (default_width, abortable, data, program) = + activate_target_for thy target naming proto_program; val serializer = case the_description data - of Fundamental seri => #serializer seri; + of Fundamental seri => #serializer seri; val presentation_names = stmt_names_of_destination destination; val module_name = if null presentation_names then raw_module_name else SOME "Code"; @@ -328,7 +349,7 @@ in invoke_serializer thy abortable serializer literals reserved includes module_alias class instance tyco const module_name args - naming (modify program) (names, presentation_names) width destination + naming program (names, presentation_names) width destination end; in