closures separate serializer initialization from serializer invocation as far as appropriate
authorhaftmann
Fri Sep 17 09:21:49 2010 +0200 (2010-09-17)
changeset 39484505f95975a5a
parent 39482 1c37d19e3d58
child 39485 f7270a5e2550
closures separate serializer initialization from serializer invocation as far as appropriate
src/Tools/Code/code_target.ML
     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