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");