code_include with attach
authorhaftmann
Mon Dec 01 12:17:04 2008 +0100 (2008-12-01)
changeset 28926530b83967c82
parent 28925 1cb9596498c0
child 28927 7e631979922f
code_include with attach
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_target.ML	Mon Dec 01 12:17:03 2008 +0100
     1.2 +++ b/src/Tools/code/code_target.ML	Mon Dec 01 12:17:04 2008 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4    serial: serial,
     1.5    serializer: serializer_entry,
     1.6    reserved: string list,
     1.7 -  includes: Pretty.T Symtab.table,
     1.8 +  includes: (Pretty.T * string list) Symtab.table,
     1.9    name_syntax_table: name_syntax_table,
    1.10    module_alias: string Symtab.table
    1.11  };
    1.12 @@ -310,17 +310,20 @@
    1.13        else insert (op =) sym syms
    1.14    in map_reserved target o add end;
    1.15  
    1.16 -fun add_include target =
    1.17 +fun gen_add_include read_const target args thy =
    1.18    let
    1.19 -    fun add (name, SOME content) incls =
    1.20 +    fun add (name, SOME (content, raw_cs)) incls =
    1.21            let
    1.22              val _ = if Symtab.defined incls name
    1.23                then warning ("Overwriting existing include " ^ name)
    1.24                else ();
    1.25 -          in Symtab.update (name, str content) incls end
    1.26 -      | add (name, NONE) incls =
    1.27 -          Symtab.delete name incls;
    1.28 -  in map_includes target o add end;
    1.29 +            val cs = map (read_const thy) raw_cs;
    1.30 +          in Symtab.update (name, (str content, cs)) incls end
    1.31 +      | add (name, NONE) incls = Symtab.delete name incls;
    1.32 +  in map_includes target (add args) thy end;
    1.33 +
    1.34 +val add_include = gen_add_include Code_Unit.check_const;
    1.35 +val add_include_cmd = gen_add_include Code_Unit.read_const;
    1.36  
    1.37  fun add_module_alias target =
    1.38    map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
    1.39 @@ -394,7 +397,7 @@
    1.40          val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
    1.41        in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
    1.42  
    1.43 -fun invoke_serializer thy abortable serializer reserved includes 
    1.44 +fun invoke_serializer thy abortable serializer reserved abs_includes 
    1.45      module_alias class instance tyco const module args naming program2 names1 =
    1.46    let
    1.47      fun distill_names lookup_name src_tab = Symtab.empty
    1.48 @@ -411,6 +414,7 @@
    1.49      val names2 = subtract (op =) names_hidden names1;
    1.50      val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
    1.51      val names_all = Graph.all_succs program2 names2;
    1.52 +    val includes = abs_includes names_all;
    1.53      val program4 = Graph.subgraph (member (op =) names_all) program3;
    1.54      val empty_funs = filter_out (member (op =) abortable)
    1.55        (Code_Thingol.empty_funs program3);
    1.56 @@ -423,7 +427,7 @@
    1.57        naming program4 names2
    1.58    end;
    1.59  
    1.60 -fun mount_serializer thy alt_serializer target module args naming program =
    1.61 +fun mount_serializer thy alt_serializer target module args naming program names =
    1.62    let
    1.63      val (targets, abortable) = CodeTargetData.get thy;
    1.64      fun collapse_hierarchy target =
    1.65 @@ -441,20 +445,27 @@
    1.66      val (serializer, _) = the_default (case the_serializer data
    1.67       of Serializer seri => seri) alt_serializer;
    1.68      val reserved = the_reserved data;
    1.69 -    val includes = Symtab.dest (the_includes data);
    1.70 +    fun select_include names_all (name, (content, cs)) =
    1.71 +      if null cs then SOME (name, content)
    1.72 +      else if exists (fn c => case Code_Thingol.lookup_const naming c
    1.73 +       of SOME name => member (op =) names_all name
    1.74 +        | NONE => false) cs
    1.75 +      then SOME (name, content) else NONE;
    1.76 +    fun includes names_all = map_filter (select_include names_all)
    1.77 +      ((Symtab.dest o the_includes) data);
    1.78      val module_alias = the_module_alias data;
    1.79      val { class, instance, tyco, const } = the_name_syntax data;
    1.80    in
    1.81      invoke_serializer thy abortable serializer reserved
    1.82 -      includes module_alias class instance tyco const module args naming (modify program)
    1.83 +      includes module_alias class instance tyco const module args naming (modify program) names
    1.84    end;
    1.85  
    1.86  in
    1.87  
    1.88  fun serialize thy = mount_serializer thy NONE;
    1.89  
    1.90 -fun serialize_custom thy (target_name, seri) naming program cs =
    1.91 -  mount_serializer thy (SOME seri) target_name NONE [] naming program cs (String [])
    1.92 +fun serialize_custom thy (target_name, seri) naming program names =
    1.93 +  mount_serializer thy (SOME seri) target_name NONE [] naming program names (String [])
    1.94    |> the;
    1.95  
    1.96  end; (* local *)
    1.97 @@ -565,9 +576,10 @@
    1.98  
    1.99  val _ =
   1.100    OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
   1.101 -    P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s))
   1.102 -    >> (fn ((target, name), content) => (Toplevel.theory o add_include target)
   1.103 -      (name, content))
   1.104 +    P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
   1.105 +      | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
   1.106 +    >> (fn ((target, name), content_consts) =>
   1.107 +        (Toplevel.theory o add_include_cmd target) (name, content_consts))
   1.108    );
   1.109  
   1.110  val _ =