tuned
authorhaftmann
Tue Aug 31 14:43:27 2010 +0200 (2010-08-31)
changeset 38927544f4702d621
parent 38926 24f82786cc57
child 38928 0e6f54c9d201
tuned
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 14:21:06 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 14:43:27 2010 +0200
     1.3 @@ -239,6 +239,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun activate_target_for thy target naming program =
     1.8 +  let
     1.9 +    val ((targets, abortable), default_width) = Targets.get thy;
    1.10 +    fun collapse_hierarchy target =
    1.11 +      let
    1.12 +        val data = case Symtab.lookup targets target
    1.13 +         of SOME data => data
    1.14 +          | NONE => error ("Unknown code target language: " ^ quote target);
    1.15 +      in case the_description data
    1.16 +       of Fundamental _ => (I, data)
    1.17 +        | Extension (super, modify) => let
    1.18 +            val (modify', data') = collapse_hierarchy super
    1.19 +          in (modify' #> modify naming, merge_target false target (data', data)) end
    1.20 +      end;
    1.21 +    val (modify, data) = collapse_hierarchy target;
    1.22 +  in (default_width, abortable, data, modify program) end;
    1.23 +
    1.24  fun activate_syntax lookup_name src_tab = Symtab.empty
    1.25    |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
    1.26         of SOME name => (SOME name,
    1.27 @@ -256,59 +273,63 @@
    1.28          | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
    1.29    |>> map_filter I;
    1.30  
    1.31 -fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    1.32 -    module_alias class instance tyco const module_name args naming program2 (names1, presentation_names) width =
    1.33 +fun activate_symbol_syntax thy literals naming
    1.34 +    class_syntax instance_syntax tyco_syntax const_syntax =
    1.35    let
    1.36 -    val (names_class, class') =
    1.37 -      activate_syntax (Code_Thingol.lookup_class naming) class;
    1.38 +    val (names_class, class_syntax') =
    1.39 +      activate_syntax (Code_Thingol.lookup_class naming) class_syntax;
    1.40      val names_inst = map_filter (Code_Thingol.lookup_instance naming)
    1.41 -      (Symreltab.keys instance);
    1.42 -    val (names_tyco, tyco') =
    1.43 -      activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
    1.44 -    val (names_const, (const', _)) =
    1.45 -      activate_const_syntax thy literals const naming;
    1.46 -    val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
    1.47 +      (Symreltab.keys instance_syntax);
    1.48 +    val (names_tyco, tyco_syntax') =
    1.49 +      activate_syntax (Code_Thingol.lookup_tyco naming) tyco_syntax;
    1.50 +    val (names_const, (const_syntax', _)) =
    1.51 +      activate_const_syntax thy literals const_syntax naming;
    1.52 +  in
    1.53 +    (names_class @ names_inst @ names_tyco @ names_const,
    1.54 +      (class_syntax', tyco_syntax', const_syntax'))
    1.55 +  end;
    1.56 +
    1.57 +fun project_program thy abortable names_hidden names1 program2 =
    1.58 +  let
    1.59      val names2 = subtract (op =) names_hidden names1;
    1.60      val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
    1.61      val names_all = Graph.all_succs program3 names2;
    1.62 -    val includes = abs_includes names_all;
    1.63 -    val program4 = Graph.subgraph (member (op =) names_all) program3;
    1.64      val empty_funs = filter_out (member (op =) abortable)
    1.65        (Code_Thingol.empty_funs program3);
    1.66      val _ = if null empty_funs then () else error ("No code equations for "
    1.67        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.68 +  in (names_all, program3) end;
    1.69 +
    1.70 +fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    1.71 +    module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
    1.72 +    module_name args naming proto_program (names, presentation_names) =
    1.73 +  let
    1.74 +    val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
    1.75 +      activate_symbol_syntax thy literals naming
    1.76 +        proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
    1.77 +    val (names_all, program) = project_program thy abortable names_hidden names proto_program;
    1.78 +    val includes = abs_includes names_all;
    1.79    in
    1.80      serializer args {
    1.81 -      labelled_name = Code_Thingol.labelled_name thy program2,
    1.82 +      labelled_name = Code_Thingol.labelled_name thy proto_program,
    1.83        reserved_syms = reserved,
    1.84        includes = includes,
    1.85        single_module = is_some module_name,
    1.86        module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
    1.87 -      class_syntax = Symtab.lookup class',
    1.88 -      tyco_syntax = Symtab.lookup tyco',
    1.89 -      const_syntax = Symtab.lookup const',
    1.90 -      program = program3,
    1.91 -      names = names1,
    1.92 -      presentation_names = presentation_names } width
    1.93 +      class_syntax = Symtab.lookup class_syntax,
    1.94 +      tyco_syntax = Symtab.lookup tyco_syntax,
    1.95 +      const_syntax = Symtab.lookup const_syntax,
    1.96 +      program = program,
    1.97 +      names = names,
    1.98 +      presentation_names = presentation_names }
    1.99    end;
   1.100  
   1.101 -fun mount_serializer thy target some_width raw_module_name args naming program names destination =
   1.102 +fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination =
   1.103    let
   1.104 -    val ((targets, abortable), default_width) = Targets.get thy;
   1.105 -    fun collapse_hierarchy target =
   1.106 -      let
   1.107 -        val data = case Symtab.lookup targets target
   1.108 -         of SOME data => data
   1.109 -          | NONE => error ("Unknown code target language: " ^ quote target);
   1.110 -      in case the_description data
   1.111 -       of Fundamental _ => (I, data)
   1.112 -        | Extension (super, modify) => let
   1.113 -            val (modify', data') = collapse_hierarchy super
   1.114 -          in (modify' #> modify naming, merge_target false target (data', data)) end
   1.115 -      end;
   1.116 -    val (modify, data) = collapse_hierarchy target;
   1.117 +    val (default_width, abortable, data, program) =
   1.118 +      activate_target_for thy target naming proto_program;
   1.119      val serializer = case the_description data
   1.120 -    of Fundamental seri => #serializer seri;
   1.121 +     of Fundamental seri => #serializer seri;
   1.122      val presentation_names = stmt_names_of_destination destination;
   1.123      val module_name = if null presentation_names
   1.124        then raw_module_name else SOME "Code";
   1.125 @@ -328,7 +349,7 @@
   1.126    in
   1.127      invoke_serializer thy abortable serializer literals reserved
   1.128        includes module_alias class instance tyco const module_name args
   1.129 -        naming (modify program) (names, presentation_names) width destination
   1.130 +        naming program (names, presentation_names) width destination
   1.131    end;
   1.132  
   1.133  in