tuned inner structure
authorhaftmann
Mon Dec 07 11:48:40 2009 +0100 (2009-12-07)
changeset 34021e820ed4bfd94
parent 34009 8c0ef28ec159
child 34022 bb37c95f0b8e
tuned inner structure
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Sun Dec 06 08:28:36 2009 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Dec 07 11:48:40 2009 +0100
     1.3 @@ -217,12 +217,164 @@
     1.4    map_target_data target o apsnd o apsnd o apsnd;
     1.5  
     1.6  
     1.7 +(** serializer usage **)
     1.8 +
     1.9 +(* montage *)
    1.10 +
    1.11 +fun the_literals thy =
    1.12 +  let
    1.13 +    val (targets, _) = CodeTargetData.get thy;
    1.14 +    fun literals target = case Symtab.lookup targets target
    1.15 +     of SOME data => (case the_serializer data
    1.16 +         of Serializer (_, literals) => literals
    1.17 +          | Extends (super, _) => literals super)
    1.18 +      | NONE => error ("Unknown code target language: " ^ quote target);
    1.19 +  in literals end;
    1.20 +
    1.21 +local
    1.22 +
    1.23 +fun activate_syntax lookup_name src_tab = Symtab.empty
    1.24 +  |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
    1.25 +       of SOME name => (SOME name,
    1.26 +            Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
    1.27 +        | NONE => (NONE, tab)) (Symtab.keys src_tab)
    1.28 +  |>> map_filter I;
    1.29 +
    1.30 +fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
    1.31 +  |> fold_map (fn thing_identifier => fn (tab, naming) =>
    1.32 +      case Code_Thingol.lookup_const naming thing_identifier
    1.33 +       of SOME name => let
    1.34 +              val (syn, naming') = Code_Printer.activate_const_syntax thy
    1.35 +                literals (the (Symtab.lookup src_tab thing_identifier)) naming
    1.36 +            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
    1.37 +        | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
    1.38 +  |>> map_filter I;
    1.39 +
    1.40 +fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    1.41 +    module_alias class instance tyco const module args naming program2 names1 =
    1.42 +  let
    1.43 +    val (names_class, class') =
    1.44 +      activate_syntax (Code_Thingol.lookup_class naming) class;
    1.45 +    val names_inst = map_filter (Code_Thingol.lookup_instance naming)
    1.46 +      (Symreltab.keys instance);
    1.47 +    val (names_tyco, tyco') =
    1.48 +      activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
    1.49 +    val (names_const, (const', _)) =
    1.50 +      activate_const_syntax thy literals const naming;
    1.51 +    val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
    1.52 +    val names2 = subtract (op =) names_hidden names1;
    1.53 +    val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
    1.54 +    val names_all = Graph.all_succs program3 names2;
    1.55 +    val includes = abs_includes names_all;
    1.56 +    val program4 = Graph.subgraph (member (op =) names_all) program3;
    1.57 +    val empty_funs = filter_out (member (op =) abortable)
    1.58 +      (Code_Thingol.empty_funs program3);
    1.59 +    val _ = if null empty_funs then () else error ("No code equations for "
    1.60 +      ^ commas (map (Sign.extern_const thy) empty_funs));
    1.61 +  in
    1.62 +    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    1.63 +      (Symtab.lookup module_alias) (Symtab.lookup class')
    1.64 +      (Symtab.lookup tyco') (Symtab.lookup const')
    1.65 +      program4 names2
    1.66 +  end;
    1.67 +
    1.68 +fun mount_serializer thy alt_serializer target module args naming program names =
    1.69 +  let
    1.70 +    val (targets, abortable) = CodeTargetData.get thy;
    1.71 +    fun collapse_hierarchy target =
    1.72 +      let
    1.73 +        val data = case Symtab.lookup targets target
    1.74 +         of SOME data => data
    1.75 +          | NONE => error ("Unknown code target language: " ^ quote target);
    1.76 +      in case the_serializer data
    1.77 +       of Serializer _ => (I, data)
    1.78 +        | Extends (super, modify) => let
    1.79 +            val (modify', data') = collapse_hierarchy super
    1.80 +          in (modify' #> modify naming, merge_target false target (data', data)) end
    1.81 +      end;
    1.82 +    val (modify, data) = collapse_hierarchy target;
    1.83 +    val (serializer, _) = the_default (case the_serializer data
    1.84 +     of Serializer seri => seri) alt_serializer;
    1.85 +    val reserved = the_reserved data;
    1.86 +    fun select_include names_all (name, (content, cs)) =
    1.87 +      if null cs then SOME (name, content)
    1.88 +      else if exists (fn c => case Code_Thingol.lookup_const naming c
    1.89 +       of SOME name => member (op =) names_all name
    1.90 +        | NONE => false) cs
    1.91 +      then SOME (name, content) else NONE;
    1.92 +    fun includes names_all = map_filter (select_include names_all)
    1.93 +      ((Symtab.dest o the_includes) data);
    1.94 +    val module_alias = the_module_alias data;
    1.95 +    val { class, instance, tyco, const } = the_name_syntax data;
    1.96 +    val literals = the_literals thy target;
    1.97 +  in
    1.98 +    invoke_serializer thy abortable serializer literals reserved
    1.99 +      includes module_alias class instance tyco const module args naming (modify program) names
   1.100 +  end;
   1.101 +
   1.102 +in
   1.103 +
   1.104 +fun serialize thy = mount_serializer thy NONE;
   1.105 +
   1.106 +fun serialize_custom thy (target_name, seri) naming program names =
   1.107 +  mount_serializer thy (SOME seri) target_name NONE [] naming program names (String [])
   1.108 +  |> the;
   1.109 +
   1.110 +end; (* local *)
   1.111 +
   1.112 +
   1.113 +(* code presentation *)
   1.114 +
   1.115 +fun code_of thy target module_name cs names_stmt =
   1.116 +  let
   1.117 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
   1.118 +  in
   1.119 +    string (names_stmt naming) (serialize thy target (SOME module_name) []
   1.120 +      naming program names_cs)
   1.121 +  end;
   1.122 +
   1.123 +
   1.124 +(* code generation *)
   1.125 +
   1.126 +fun transitivly_non_empty_funs thy naming program =
   1.127 +  let
   1.128 +    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
   1.129 +    val names = map_filter (Code_Thingol.lookup_const naming) cs;
   1.130 +  in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
   1.131 +
   1.132 +fun read_const_exprs thy cs =
   1.133 +  let
   1.134 +    val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
   1.135 +    val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
   1.136 +    val names4 = transitivly_non_empty_funs thy naming program;
   1.137 +    val cs5 = map_filter
   1.138 +      (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
   1.139 +  in fold (insert (op =)) cs5 cs1 end;
   1.140 +
   1.141 +fun cached_program thy = 
   1.142 +  let
   1.143 +    val (naming, program) = Code_Thingol.cached_program thy;
   1.144 +  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
   1.145 +
   1.146 +fun export_code thy cs seris =
   1.147 +  let
   1.148 +    val (cs', (naming, program)) = if null cs then cached_program thy
   1.149 +      else Code_Thingol.consts_program thy cs;
   1.150 +    fun mk_seri_dest dest = case dest
   1.151 +     of NONE => compile
   1.152 +      | SOME "-" => export
   1.153 +      | SOME f => file (Path.explode f)
   1.154 +    val _ = map (fn (((target, module), dest), args) =>
   1.155 +      (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
   1.156 +  in () end;
   1.157 +
   1.158 +fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
   1.159 +
   1.160 +
   1.161  (** serializer configuration **)
   1.162  
   1.163  (* data access *)
   1.164  
   1.165 -local
   1.166 -
   1.167  fun cert_class thy class =
   1.168    let
   1.169      val _ = AxClass.get_info thy class;
   1.170 @@ -345,6 +497,8 @@
   1.171  
   1.172  (* concrete syntax *)
   1.173  
   1.174 +local
   1.175 +
   1.176  structure P = OuterParse
   1.177  and K = OuterKeyword
   1.178  
   1.179 @@ -369,166 +523,12 @@
   1.180  val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
   1.181  val allow_abort_cmd = gen_allow_abort Code.read_const;
   1.182  
   1.183 -fun the_literals thy =
   1.184 -  let
   1.185 -    val (targets, _) = CodeTargetData.get thy;
   1.186 -    fun literals target = case Symtab.lookup targets target
   1.187 -     of SOME data => (case the_serializer data
   1.188 -         of Serializer (_, literals) => literals
   1.189 -          | Extends (super, _) => literals super)
   1.190 -      | NONE => error ("Unknown code target language: " ^ quote target);
   1.191 -  in literals end;
   1.192 -
   1.193 -
   1.194 -(** serializer usage **)
   1.195 -
   1.196 -(* montage *)
   1.197 -
   1.198 -local
   1.199 -
   1.200 -fun activate_syntax lookup_name src_tab = Symtab.empty
   1.201 -  |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
   1.202 -       of SOME name => (SOME name,
   1.203 -            Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
   1.204 -        | NONE => (NONE, tab)) (Symtab.keys src_tab)
   1.205 -  |>> map_filter I;
   1.206 -
   1.207 -fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
   1.208 -  |> fold_map (fn thing_identifier => fn (tab, naming) =>
   1.209 -      case Code_Thingol.lookup_const naming thing_identifier
   1.210 -       of SOME name => let
   1.211 -              val (syn, naming') = Code_Printer.activate_const_syntax thy
   1.212 -                literals (the (Symtab.lookup src_tab thing_identifier)) naming
   1.213 -            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
   1.214 -        | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
   1.215 -  |>> map_filter I;
   1.216 -
   1.217 -fun invoke_serializer thy abortable serializer literals reserved abs_includes 
   1.218 -    module_alias class instance tyco const module args naming program2 names1 =
   1.219 -  let
   1.220 -    val (names_class, class') =
   1.221 -      activate_syntax (Code_Thingol.lookup_class naming) class;
   1.222 -    val names_inst = map_filter (Code_Thingol.lookup_instance naming)
   1.223 -      (Symreltab.keys instance);
   1.224 -    val (names_tyco, tyco') =
   1.225 -      activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
   1.226 -    val (names_const, (const', _)) =
   1.227 -      activate_const_syntax thy literals const naming;
   1.228 -    val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
   1.229 -    val names2 = subtract (op =) names_hidden names1;
   1.230 -    val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
   1.231 -    val names_all = Graph.all_succs program3 names2;
   1.232 -    val includes = abs_includes names_all;
   1.233 -    val program4 = Graph.subgraph (member (op =) names_all) program3;
   1.234 -    val empty_funs = filter_out (member (op =) abortable)
   1.235 -      (Code_Thingol.empty_funs program3);
   1.236 -    val _ = if null empty_funs then () else error ("No code equations for "
   1.237 -      ^ commas (map (Sign.extern_const thy) empty_funs));
   1.238 -  in
   1.239 -    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
   1.240 -      (Symtab.lookup module_alias) (Symtab.lookup class')
   1.241 -      (Symtab.lookup tyco') (Symtab.lookup const')
   1.242 -      program4 names2
   1.243 -  end;
   1.244 -
   1.245 -fun mount_serializer thy alt_serializer target module args naming program names =
   1.246 -  let
   1.247 -    val (targets, abortable) = CodeTargetData.get thy;
   1.248 -    fun collapse_hierarchy target =
   1.249 -      let
   1.250 -        val data = case Symtab.lookup targets target
   1.251 -         of SOME data => data
   1.252 -          | NONE => error ("Unknown code target language: " ^ quote target);
   1.253 -      in case the_serializer data
   1.254 -       of Serializer _ => (I, data)
   1.255 -        | Extends (super, modify) => let
   1.256 -            val (modify', data') = collapse_hierarchy super
   1.257 -          in (modify' #> modify naming, merge_target false target (data', data)) end
   1.258 -      end;
   1.259 -    val (modify, data) = collapse_hierarchy target;
   1.260 -    val (serializer, _) = the_default (case the_serializer data
   1.261 -     of Serializer seri => seri) alt_serializer;
   1.262 -    val reserved = the_reserved data;
   1.263 -    fun select_include names_all (name, (content, cs)) =
   1.264 -      if null cs then SOME (name, content)
   1.265 -      else if exists (fn c => case Code_Thingol.lookup_const naming c
   1.266 -       of SOME name => member (op =) names_all name
   1.267 -        | NONE => false) cs
   1.268 -      then SOME (name, content) else NONE;
   1.269 -    fun includes names_all = map_filter (select_include names_all)
   1.270 -      ((Symtab.dest o the_includes) data);
   1.271 -    val module_alias = the_module_alias data;
   1.272 -    val { class, instance, tyco, const } = the_name_syntax data;
   1.273 -    val literals = the_literals thy target;
   1.274 -  in
   1.275 -    invoke_serializer thy abortable serializer literals reserved
   1.276 -      includes module_alias class instance tyco const module args naming (modify program) names
   1.277 -  end;
   1.278 -
   1.279 -in
   1.280 -
   1.281 -fun serialize thy = mount_serializer thy NONE;
   1.282 -
   1.283 -fun serialize_custom thy (target_name, seri) naming program names =
   1.284 -  mount_serializer thy (SOME seri) target_name NONE [] naming program names (String [])
   1.285 -  |> the;
   1.286 -
   1.287 -end; (* local *)
   1.288 -
   1.289  fun parse_args f args =
   1.290    case Scan.read OuterLex.stopper f args
   1.291     of SOME x => x
   1.292      | NONE => error "Bad serializer arguments";
   1.293  
   1.294  
   1.295 -(* code presentation *)
   1.296 -
   1.297 -fun code_of thy target module_name cs names_stmt =
   1.298 -  let
   1.299 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
   1.300 -  in
   1.301 -    string (names_stmt naming) (serialize thy target (SOME module_name) []
   1.302 -      naming program names_cs)
   1.303 -  end;
   1.304 -
   1.305 -
   1.306 -(* code generation *)
   1.307 -
   1.308 -fun transitivly_non_empty_funs thy naming program =
   1.309 -  let
   1.310 -    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
   1.311 -    val names = map_filter (Code_Thingol.lookup_const naming) cs;
   1.312 -  in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
   1.313 -
   1.314 -fun read_const_exprs thy cs =
   1.315 -  let
   1.316 -    val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
   1.317 -    val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
   1.318 -    val names4 = transitivly_non_empty_funs thy naming program;
   1.319 -    val cs5 = map_filter
   1.320 -      (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
   1.321 -  in fold (insert (op =)) cs5 cs1 end;
   1.322 -
   1.323 -fun cached_program thy = 
   1.324 -  let
   1.325 -    val (naming, program) = Code_Thingol.cached_program thy;
   1.326 -  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
   1.327 -
   1.328 -fun export_code thy cs seris =
   1.329 -  let
   1.330 -    val (cs', (naming, program)) = if null cs then cached_program thy
   1.331 -      else Code_Thingol.consts_program thy cs;
   1.332 -    fun mk_seri_dest dest = case dest
   1.333 -     of NONE => compile
   1.334 -      | SOME "-" => export
   1.335 -      | SOME f => file (Path.explode f)
   1.336 -    val _ = map (fn (((target, module), dest), args) =>
   1.337 -      (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
   1.338 -  in () end;
   1.339 -
   1.340 -fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
   1.341 -
   1.342 -
   1.343  (** Isar setup **)
   1.344  
   1.345  val (inK, module_nameK, fileK) = ("in", "module_name", "file");