1.1 --- a/src/Tools/Code/code_target.ML Fri Sep 17 08:41:07 2010 +0200
1.2 +++ b/src/Tools/Code/code_target.ML Fri Sep 17 09:21:49 2010 +0200
1.3 @@ -241,7 +241,7 @@
1.4
1.5 local
1.6
1.7 -fun activate_target_for thy target naming program =
1.8 +fun activate_target thy target =
1.9 let
1.10 val ((targets, abortable), default_width) = Targets.get thy;
1.11 fun collapse_hierarchy target =
1.12 @@ -250,13 +250,13 @@
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 + of Fundamental _ => (K I, data)
1.18 | Extension (super, modify) => let
1.19 val (modify', data') = collapse_hierarchy super
1.20 - in (modify' #> modify naming, merge_target false target (data', data)) end
1.21 + in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
1.22 end;
1.23 val (modify, data) = collapse_hierarchy target;
1.24 - in (default_width, abortable, data, modify program) end;
1.25 + in (default_width, abortable, data, modify) end;
1.26
1.27 fun activate_syntax lookup_name src_tab = Symtab.empty
1.28 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
1.29 @@ -303,7 +303,7 @@
1.30 val program4 = Graph.subgraph (member (op =) names4) program3;
1.31 in (names4, program4) end;
1.32
1.33 -fun invoke_serializer thy abortable serializer literals reserved abs_includes
1.34 +fun invoke_serializer thy abortable serializer literals reserved all_includes
1.35 module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
1.36 module_name args naming proto_program names =
1.37 let
1.38 @@ -311,7 +311,12 @@
1.39 activate_symbol_syntax thy literals naming
1.40 proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
1.41 val (names_all, program) = project_program thy abortable names_hidden names proto_program;
1.42 - val includes = abs_includes names_all;
1.43 + fun select_include (name, (content, cs)) =
1.44 + if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
1.45 + of SOME name => member (op =) names_all name
1.46 + | NONE => false) cs
1.47 + then SOME (name, content) else NONE;
1.48 + val includes = map_filter select_include (Symtab.dest all_includes);
1.49 in
1.50 serializer args {
1.51 labelled_name = Code_Thingol.labelled_name thy proto_program,
1.52 @@ -324,29 +329,20 @@
1.53 program = program }
1.54 end;
1.55
1.56 -fun mount_serializer thy target some_width module_name args naming proto_program names =
1.57 +fun mount_serializer thy target some_width module_name args =
1.58 let
1.59 - val (default_width, abortable, data, program) =
1.60 - activate_target_for thy target naming proto_program;
1.61 + val (default_width, abortable, data, modify) = activate_target thy target;
1.62 val serializer = case the_description data
1.63 of Fundamental seri => #serializer seri;
1.64 val reserved = the_reserved data;
1.65 - fun select_include names_all (name, (content, cs)) =
1.66 - if null cs then SOME (name, content)
1.67 - else if exists (fn c => case Code_Thingol.lookup_const naming c
1.68 - of SOME name => member (op =) names_all name
1.69 - | NONE => false) cs
1.70 - then SOME (name, content) else NONE;
1.71 - fun includes names_all = map_filter (select_include names_all)
1.72 - ((Symtab.dest o the_includes) data);
1.73 val module_alias = the_module_alias data
1.74 val { class, instance, tyco, const } = the_symbol_syntax data;
1.75 val literals = the_literals thy target;
1.76 val width = the_default default_width some_width;
1.77 - in
1.78 + in fn naming => fn program => fn names =>
1.79 invoke_serializer thy abortable serializer literals reserved
1.80 - includes module_alias class instance tyco const module_name args
1.81 - naming program names width
1.82 + (the_includes data) module_alias class instance tyco const module_name args
1.83 + naming (modify naming program) names width
1.84 end;
1.85
1.86 fun assert_module_name "" = error ("Empty module name not allowed.")
1.87 @@ -354,16 +350,22 @@
1.88
1.89 in
1.90
1.91 -fun export_code_for thy some_path target some_width some_module_name args naming program names =
1.92 - export some_path (mount_serializer thy target some_width some_module_name args naming program names);
1.93 +fun export_code_for thy some_path target some_width module_name args =
1.94 + export some_path ooo mount_serializer thy target some_width module_name args;
1.95
1.96 -fun produce_code_for thy target some_width module_name args naming program names =
1.97 +fun produce_code_for thy target some_width module_name args =
1.98 let
1.99 - val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
1.100 - in (s, map deresolve names) end;
1.101 + val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
1.102 + in fn naming => fn program => fn names =>
1.103 + produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
1.104 + end;
1.105
1.106 -fun present_code_for thy target some_width module_name args naming program (names, selects) =
1.107 - present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
1.108 +fun present_code_for thy target some_width module_name args =
1.109 + let
1.110 + val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
1.111 + in fn naming => fn program => fn (names, selects) =>
1.112 + present selects (serializer naming program names)
1.113 + end;
1.114
1.115 fun check_code_for thy target strict args naming program names_cs =
1.116 let