1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/Code/code_target.ML Tue Jun 23 12:09:30 2009 +0200
1.3 @@ -0,0 +1,629 @@
1.4 +(* Title: Tools/code/code_target.ML
1.5 + Author: Florian Haftmann, TU Muenchen
1.6 +
1.7 +Serializer from intermediate language ("Thin-gol") to target languages.
1.8 +*)
1.9 +
1.10 +signature CODE_TARGET =
1.11 +sig
1.12 + include CODE_PRINTER
1.13 +
1.14 + type serializer
1.15 + val add_target: string * (serializer * literals) -> theory -> theory
1.16 + val extend_target: string *
1.17 + (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
1.18 + -> theory -> theory
1.19 + val assert_target: theory -> string -> string
1.20 +
1.21 + type destination
1.22 + type serialization
1.23 + val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
1.24 + -> OuterLex.token list -> 'a
1.25 + val stmt_names_of_destination: destination -> string list
1.26 + val code_of_pretty: Pretty.T -> string
1.27 + val code_writeln: Pretty.T -> unit
1.28 + val mk_serialization: string -> ('a -> unit) option
1.29 + -> (Path.T option -> 'a -> unit)
1.30 + -> ('a -> string * string option list)
1.31 + -> 'a -> serialization
1.32 + val serialize: theory -> string -> string option -> OuterLex.token list
1.33 + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
1.34 + val serialize_custom: theory -> string * (serializer * literals)
1.35 + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
1.36 + val the_literals: theory -> string -> literals
1.37 + val compile: serialization -> unit
1.38 + val export: serialization -> unit
1.39 + val file: Path.T -> serialization -> unit
1.40 + val string: string list -> serialization -> string
1.41 + val code_of: theory -> string -> string
1.42 + -> string list -> (Code_Thingol.naming -> string list) -> string
1.43 + val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
1.44 + val code_width: int ref
1.45 +
1.46 + val allow_abort: string -> theory -> theory
1.47 + val add_syntax_class: string -> class -> string option -> theory -> theory
1.48 + val add_syntax_inst: string -> string * class -> bool -> theory -> theory
1.49 + val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
1.50 + val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
1.51 + val add_reserved: string -> string -> theory -> theory
1.52 +end;
1.53 +
1.54 +structure Code_Target : CODE_TARGET =
1.55 +struct
1.56 +
1.57 +open Basic_Code_Thingol;
1.58 +open Code_Printer;
1.59 +
1.60 +(** basics **)
1.61 +
1.62 +datatype destination = Compile | Export | File of Path.T | String of string list;
1.63 +type serialization = destination -> (string * string option list) option;
1.64 +
1.65 +val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
1.66 +fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
1.67 +fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
1.68 +fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
1.69 +
1.70 +(*FIXME why another code_setmp?*)
1.71 +fun compile f = (code_setmp f Compile; ());
1.72 +fun export f = (code_setmp f Export; ());
1.73 +fun file p f = (code_setmp f (File p); ());
1.74 +fun string stmts f = fst (the (code_setmp f (String stmts)));
1.75 +
1.76 +fun stmt_names_of_destination (String stmts) = stmts
1.77 + | stmt_names_of_destination _ = [];
1.78 +
1.79 +fun mk_serialization target (SOME comp) _ _ code Compile = (comp code; NONE)
1.80 + | mk_serialization target NONE _ _ _ Compile = error (target ^ ": no internal compilation")
1.81 + | mk_serialization target _ output _ code Export = (output NONE code ; NONE)
1.82 + | mk_serialization target _ output _ code (File file) = (output (SOME file) code; NONE)
1.83 + | mk_serialization target _ _ string code (String _) = SOME (string code);
1.84 +
1.85 +
1.86 +(** theory data **)
1.87 +
1.88 +datatype name_syntax_table = NameSyntaxTable of {
1.89 + class: string Symtab.table,
1.90 + instance: unit Symreltab.table,
1.91 + tyco: tyco_syntax Symtab.table,
1.92 + const: proto_const_syntax Symtab.table
1.93 +};
1.94 +
1.95 +fun mk_name_syntax_table ((class, instance), (tyco, const)) =
1.96 + NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
1.97 +fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
1.98 + mk_name_syntax_table (f ((class, instance), (tyco, const)));
1.99 +fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
1.100 + NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
1.101 + mk_name_syntax_table (
1.102 + (Symtab.join (K snd) (class1, class2),
1.103 + Symreltab.join (K snd) (instance1, instance2)),
1.104 + (Symtab.join (K snd) (tyco1, tyco2),
1.105 + Symtab.join (K snd) (const1, const2))
1.106 + );
1.107 +
1.108 +type serializer =
1.109 + string option (*module name*)
1.110 + -> OuterLex.token list (*arguments*)
1.111 + -> (string -> string) (*labelled_name*)
1.112 + -> string list (*reserved symbols*)
1.113 + -> (string * Pretty.T) list (*includes*)
1.114 + -> (string -> string option) (*module aliasses*)
1.115 + -> (string -> string option) (*class syntax*)
1.116 + -> (string -> tyco_syntax option)
1.117 + -> (string -> const_syntax option)
1.118 + -> Code_Thingol.program
1.119 + -> string list (*selected statements*)
1.120 + -> serialization;
1.121 +
1.122 +datatype serializer_entry = Serializer of serializer * literals
1.123 + | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
1.124 +
1.125 +datatype target = Target of {
1.126 + serial: serial,
1.127 + serializer: serializer_entry,
1.128 + reserved: string list,
1.129 + includes: (Pretty.T * string list) Symtab.table,
1.130 + name_syntax_table: name_syntax_table,
1.131 + module_alias: string Symtab.table
1.132 +};
1.133 +
1.134 +fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
1.135 + Target { serial = serial, serializer = serializer, reserved = reserved,
1.136 + includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
1.137 +fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
1.138 + make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
1.139 +fun merge_target strict target (Target { serial = serial1, serializer = serializer,
1.140 + reserved = reserved1, includes = includes1,
1.141 + name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
1.142 + Target { serial = serial2, serializer = _,
1.143 + reserved = reserved2, includes = includes2,
1.144 + name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
1.145 + if serial1 = serial2 orelse not strict then
1.146 + make_target ((serial1, serializer),
1.147 + ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
1.148 + (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
1.149 + Symtab.join (K snd) (module_alias1, module_alias2))
1.150 + ))
1.151 + else
1.152 + error ("Incompatible serializers: " ^ quote target);
1.153 +
1.154 +structure CodeTargetData = TheoryDataFun
1.155 +(
1.156 + type T = target Symtab.table * string list;
1.157 + val empty = (Symtab.empty, []);
1.158 + val copy = I;
1.159 + val extend = I;
1.160 + fun merge _ ((target1, exc1) : T, (target2, exc2)) =
1.161 + (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
1.162 +);
1.163 +
1.164 +fun the_serializer (Target { serializer, ... }) = serializer;
1.165 +fun the_reserved (Target { reserved, ... }) = reserved;
1.166 +fun the_includes (Target { includes, ... }) = includes;
1.167 +fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
1.168 +fun the_module_alias (Target { module_alias , ... }) = module_alias;
1.169 +
1.170 +val abort_allowed = snd o CodeTargetData.get;
1.171 +
1.172 +fun assert_target thy target =
1.173 + case Symtab.lookup (fst (CodeTargetData.get thy)) target
1.174 + of SOME data => target
1.175 + | NONE => error ("Unknown code target language: " ^ quote target);
1.176 +
1.177 +fun put_target (target, seri) thy =
1.178 + let
1.179 + val lookup_target = Symtab.lookup (fst (CodeTargetData.get thy));
1.180 + val _ = case seri
1.181 + of Extends (super, _) => if is_some (lookup_target super) then ()
1.182 + else error ("Unknown code target language: " ^ quote super)
1.183 + | _ => ();
1.184 + val overwriting = case (Option.map the_serializer o lookup_target) target
1.185 + of NONE => false
1.186 + | SOME (Extends _) => true
1.187 + | SOME (Serializer _) => (case seri
1.188 + of Extends _ => error ("Will not overwrite existing target " ^ quote target)
1.189 + | _ => true);
1.190 + val _ = if overwriting
1.191 + then warning ("Overwriting existing target " ^ quote target)
1.192 + else ();
1.193 + in
1.194 + thy
1.195 + |> (CodeTargetData.map o apfst oo Symtab.map_default)
1.196 + (target, make_target ((serial (), seri), (([], Symtab.empty),
1.197 + (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
1.198 + Symtab.empty))))
1.199 + ((map_target o apfst o apsnd o K) seri)
1.200 + end;
1.201 +
1.202 +fun add_target (target, seri) = put_target (target, Serializer seri);
1.203 +fun extend_target (target, (super, modify)) =
1.204 + put_target (target, Extends (super, modify));
1.205 +
1.206 +fun map_target_data target f thy =
1.207 + let
1.208 + val _ = assert_target thy target;
1.209 + in
1.210 + thy
1.211 + |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
1.212 + end;
1.213 +
1.214 +fun map_reserved target =
1.215 + map_target_data target o apsnd o apfst o apfst;
1.216 +fun map_includes target =
1.217 + map_target_data target o apsnd o apfst o apsnd;
1.218 +fun map_name_syntax target =
1.219 + map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
1.220 +fun map_module_alias target =
1.221 + map_target_data target o apsnd o apsnd o apsnd;
1.222 +
1.223 +
1.224 +(** serializer configuration **)
1.225 +
1.226 +(* data access *)
1.227 +
1.228 +local
1.229 +
1.230 +fun cert_class thy class =
1.231 + let
1.232 + val _ = AxClass.get_info thy class;
1.233 + in class end;
1.234 +
1.235 +fun read_class thy = cert_class thy o Sign.intern_class thy;
1.236 +
1.237 +fun cert_tyco thy tyco =
1.238 + let
1.239 + val _ = if Sign.declared_tyname thy tyco then ()
1.240 + else error ("No such type constructor: " ^ quote tyco);
1.241 + in tyco end;
1.242 +
1.243 +fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
1.244 +
1.245 +fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
1.246 + let
1.247 + val class = prep_class thy raw_class;
1.248 + in case raw_syn
1.249 + of SOME syntax =>
1.250 + thy
1.251 + |> (map_name_syntax target o apfst o apfst)
1.252 + (Symtab.update (class, syntax))
1.253 + | NONE =>
1.254 + thy
1.255 + |> (map_name_syntax target o apfst o apfst)
1.256 + (Symtab.delete_safe class)
1.257 + end;
1.258 +
1.259 +fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
1.260 + let
1.261 + val inst = (prep_class thy raw_class, prep_tyco thy raw_tyco);
1.262 + in if add_del then
1.263 + thy
1.264 + |> (map_name_syntax target o apfst o apsnd)
1.265 + (Symreltab.update (inst, ()))
1.266 + else
1.267 + thy
1.268 + |> (map_name_syntax target o apfst o apsnd)
1.269 + (Symreltab.delete_safe inst)
1.270 + end;
1.271 +
1.272 +fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
1.273 + let
1.274 + val tyco = prep_tyco thy raw_tyco;
1.275 + fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
1.276 + then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
1.277 + else syntax
1.278 + in case raw_syn
1.279 + of SOME syntax =>
1.280 + thy
1.281 + |> (map_name_syntax target o apsnd o apfst)
1.282 + (Symtab.update (tyco, check_args syntax))
1.283 + | NONE =>
1.284 + thy
1.285 + |> (map_name_syntax target o apsnd o apfst)
1.286 + (Symtab.delete_safe tyco)
1.287 + end;
1.288 +
1.289 +fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
1.290 + let
1.291 + val c = prep_const thy raw_c;
1.292 + fun check_args (syntax as (n, _)) = if n > Code.no_args thy c
1.293 + then error ("Too many arguments in syntax for constant " ^ quote c)
1.294 + else syntax;
1.295 + in case raw_syn
1.296 + of SOME syntax =>
1.297 + thy
1.298 + |> (map_name_syntax target o apsnd o apsnd)
1.299 + (Symtab.update (c, check_args syntax))
1.300 + | NONE =>
1.301 + thy
1.302 + |> (map_name_syntax target o apsnd o apsnd)
1.303 + (Symtab.delete_safe c)
1.304 + end;
1.305 +
1.306 +fun add_reserved target =
1.307 + let
1.308 + fun add sym syms = if member (op =) syms sym
1.309 + then error ("Reserved symbol " ^ quote sym ^ " already declared")
1.310 + else insert (op =) sym syms
1.311 + in map_reserved target o add end;
1.312 +
1.313 +fun gen_add_include read_const target args thy =
1.314 + let
1.315 + fun add (name, SOME (content, raw_cs)) incls =
1.316 + let
1.317 + val _ = if Symtab.defined incls name
1.318 + then warning ("Overwriting existing include " ^ name)
1.319 + else ();
1.320 + val cs = map (read_const thy) raw_cs;
1.321 + in Symtab.update (name, (str content, cs)) incls end
1.322 + | add (name, NONE) incls = Symtab.delete name incls;
1.323 + in map_includes target (add args) thy end;
1.324 +
1.325 +val add_include = gen_add_include Code.check_const;
1.326 +val add_include_cmd = gen_add_include Code.read_const;
1.327 +
1.328 +fun add_module_alias target (thyname, modlname) =
1.329 + let
1.330 + val xs = Long_Name.explode modlname;
1.331 + val xs' = map (Name.desymbolize true) xs;
1.332 + in if xs' = xs
1.333 + then map_module_alias target (Symtab.update (thyname, modlname))
1.334 + else error ("Invalid module name: " ^ quote modlname ^ "\n"
1.335 + ^ "perhaps try " ^ quote (Long_Name.implode xs'))
1.336 + end;
1.337 +
1.338 +fun gen_allow_abort prep_const raw_c thy =
1.339 + let
1.340 + val c = prep_const thy raw_c;
1.341 + in thy |> (CodeTargetData.map o apsnd) (insert (op =) c) end;
1.342 +
1.343 +fun zip_list (x::xs) f g =
1.344 + f
1.345 + #-> (fn y =>
1.346 + fold_map (fn x => g |-- f >> pair x) xs
1.347 + #-> (fn xys => pair ((x, y) :: xys)));
1.348 +
1.349 +
1.350 +(* concrete syntax *)
1.351 +
1.352 +structure P = OuterParse
1.353 +and K = OuterKeyword
1.354 +
1.355 +fun parse_multi_syntax parse_thing parse_syntax =
1.356 + P.and_list1 parse_thing
1.357 + #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
1.358 + (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
1.359 +
1.360 +in
1.361 +
1.362 +val add_syntax_class = gen_add_syntax_class cert_class (K I);
1.363 +val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
1.364 +val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
1.365 +val add_syntax_const = gen_add_syntax_const (K I);
1.366 +val allow_abort = gen_allow_abort (K I);
1.367 +val add_reserved = add_reserved;
1.368 +
1.369 +val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const;
1.370 +val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
1.371 +val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
1.372 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
1.373 +val allow_abort_cmd = gen_allow_abort Code.read_const;
1.374 +
1.375 +fun the_literals thy =
1.376 + let
1.377 + val (targets, _) = CodeTargetData.get thy;
1.378 + fun literals target = case Symtab.lookup targets target
1.379 + of SOME data => (case the_serializer data
1.380 + of Serializer (_, literals) => literals
1.381 + | Extends (super, _) => literals super)
1.382 + | NONE => error ("Unknown code target language: " ^ quote target);
1.383 + in literals end;
1.384 +
1.385 +
1.386 +(** serializer usage **)
1.387 +
1.388 +(* montage *)
1.389 +
1.390 +local
1.391 +
1.392 +fun labelled_name thy program name = case Graph.get_node program name
1.393 + of Code_Thingol.Fun (c, _) => quote (Code.string_of_const thy c)
1.394 + | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
1.395 + | Code_Thingol.Datatypecons (c, _) => quote (Code.string_of_const thy c)
1.396 + | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
1.397 + | Code_Thingol.Classrel (sub, super) => let
1.398 + val Code_Thingol.Class (sub, _) = Graph.get_node program sub
1.399 + val Code_Thingol.Class (super, _) = Graph.get_node program super
1.400 + in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
1.401 + | Code_Thingol.Classparam (c, _) => quote (Code.string_of_const thy c)
1.402 + | Code_Thingol.Classinst ((class, (tyco, _)), _) => let
1.403 + val Code_Thingol.Class (class, _) = Graph.get_node program class
1.404 + val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
1.405 + in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
1.406 +
1.407 +fun activate_syntax lookup_name src_tab = Symtab.empty
1.408 + |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
1.409 + of SOME name => (SOME name,
1.410 + Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
1.411 + | NONE => (NONE, tab)) (Symtab.keys src_tab)
1.412 + |>> map_filter I;
1.413 +
1.414 +fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
1.415 + |> fold_map (fn thing_identifier => fn (tab, naming) =>
1.416 + case Code_Thingol.lookup_const naming thing_identifier
1.417 + of SOME name => let
1.418 + val (syn, naming') = Code_Printer.activate_const_syntax thy
1.419 + literals (the (Symtab.lookup src_tab thing_identifier)) naming
1.420 + in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
1.421 + | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
1.422 + |>> map_filter I;
1.423 +
1.424 +fun invoke_serializer thy abortable serializer literals reserved abs_includes
1.425 + module_alias class instance tyco const module args naming program2 names1 =
1.426 + let
1.427 + val (names_class, class') =
1.428 + activate_syntax (Code_Thingol.lookup_class naming) class;
1.429 + val names_inst = map_filter (Code_Thingol.lookup_instance naming)
1.430 + (Symreltab.keys instance);
1.431 + val (names_tyco, tyco') =
1.432 + activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
1.433 + val (names_const, (const', _)) =
1.434 + activate_const_syntax thy literals const naming;
1.435 + val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
1.436 + val names2 = subtract (op =) names_hidden names1;
1.437 + val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
1.438 + val names_all = Graph.all_succs program3 names2;
1.439 + val includes = abs_includes names_all;
1.440 + val program4 = Graph.subgraph (member (op =) names_all) program3;
1.441 + val empty_funs = filter_out (member (op =) abortable)
1.442 + (Code_Thingol.empty_funs program3);
1.443 + val _ = if null empty_funs then () else error ("No code equations for "
1.444 + ^ commas (map (Sign.extern_const thy) empty_funs));
1.445 + in
1.446 + serializer module args (labelled_name thy program2) reserved includes
1.447 + (Symtab.lookup module_alias) (Symtab.lookup class')
1.448 + (Symtab.lookup tyco') (Symtab.lookup const')
1.449 + program4 names2
1.450 + end;
1.451 +
1.452 +fun mount_serializer thy alt_serializer target module args naming program names =
1.453 + let
1.454 + val (targets, abortable) = CodeTargetData.get thy;
1.455 + fun collapse_hierarchy target =
1.456 + let
1.457 + val data = case Symtab.lookup targets target
1.458 + of SOME data => data
1.459 + | NONE => error ("Unknown code target language: " ^ quote target);
1.460 + in case the_serializer data
1.461 + of Serializer _ => (I, data)
1.462 + | Extends (super, modify) => let
1.463 + val (modify', data') = collapse_hierarchy super
1.464 + in (modify' #> modify naming, merge_target false target (data', data)) end
1.465 + end;
1.466 + val (modify, data) = collapse_hierarchy target;
1.467 + val (serializer, _) = the_default (case the_serializer data
1.468 + of Serializer seri => seri) alt_serializer;
1.469 + val reserved = the_reserved data;
1.470 + fun select_include names_all (name, (content, cs)) =
1.471 + if null cs then SOME (name, content)
1.472 + else if exists (fn c => case Code_Thingol.lookup_const naming c
1.473 + of SOME name => member (op =) names_all name
1.474 + | NONE => false) cs
1.475 + then SOME (name, content) else NONE;
1.476 + fun includes names_all = map_filter (select_include names_all)
1.477 + ((Symtab.dest o the_includes) data);
1.478 + val module_alias = the_module_alias data;
1.479 + val { class, instance, tyco, const } = the_name_syntax data;
1.480 + val literals = the_literals thy target;
1.481 + in
1.482 + invoke_serializer thy abortable serializer literals reserved
1.483 + includes module_alias class instance tyco const module args naming (modify program) names
1.484 + end;
1.485 +
1.486 +in
1.487 +
1.488 +fun serialize thy = mount_serializer thy NONE;
1.489 +
1.490 +fun serialize_custom thy (target_name, seri) naming program names =
1.491 + mount_serializer thy (SOME seri) target_name NONE [] naming program names (String [])
1.492 + |> the;
1.493 +
1.494 +end; (* local *)
1.495 +
1.496 +fun parse_args f args =
1.497 + case Scan.read OuterLex.stopper f args
1.498 + of SOME x => x
1.499 + | NONE => error "Bad serializer arguments";
1.500 +
1.501 +
1.502 +(* code presentation *)
1.503 +
1.504 +fun code_of thy target module_name cs names_stmt =
1.505 + let
1.506 + val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
1.507 + in
1.508 + string (names_stmt naming) (serialize thy target (SOME module_name) []
1.509 + naming program names_cs)
1.510 + end;
1.511 +
1.512 +
1.513 +(* code generation *)
1.514 +
1.515 +fun transitivly_non_empty_funs thy naming program =
1.516 + let
1.517 + val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
1.518 + val names = map_filter (Code_Thingol.lookup_const naming) cs;
1.519 + in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
1.520 +
1.521 +fun read_const_exprs thy cs =
1.522 + let
1.523 + val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
1.524 + val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
1.525 + val names4 = transitivly_non_empty_funs thy naming program;
1.526 + val cs5 = map_filter
1.527 + (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
1.528 + in fold (insert (op =)) cs5 cs1 end;
1.529 +
1.530 +fun cached_program thy =
1.531 + let
1.532 + val (naming, program) = Code_Thingol.cached_program thy;
1.533 + in (transitivly_non_empty_funs thy naming program, (naming, program)) end
1.534 +
1.535 +fun export_code thy cs seris =
1.536 + let
1.537 + val (cs', (naming, program)) = if null cs then cached_program thy
1.538 + else Code_Thingol.consts_program thy cs;
1.539 + fun mk_seri_dest dest = case dest
1.540 + of NONE => compile
1.541 + | SOME "-" => export
1.542 + | SOME f => file (Path.explode f)
1.543 + val _ = map (fn (((target, module), dest), args) =>
1.544 + (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
1.545 + in () end;
1.546 +
1.547 +fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
1.548 +
1.549 +
1.550 +(** Isar setup **)
1.551 +
1.552 +val (inK, module_nameK, fileK) = ("in", "module_name", "file");
1.553 +
1.554 +val code_exprP =
1.555 + (Scan.repeat P.term_group
1.556 + -- Scan.repeat (P.$$$ inK |-- P.name
1.557 + -- Scan.option (P.$$$ module_nameK |-- P.name)
1.558 + -- Scan.option (P.$$$ fileK |-- P.name)
1.559 + -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
1.560 + ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
1.561 +
1.562 +val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
1.563 +
1.564 +val _ =
1.565 + OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
1.566 + parse_multi_syntax P.xname (Scan.option P.string)
1.567 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.568 + fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
1.569 + );
1.570 +
1.571 +val _ =
1.572 + OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
1.573 + parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
1.574 + ((P.minus >> K true) || Scan.succeed false)
1.575 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.576 + fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
1.577 + );
1.578 +
1.579 +val _ =
1.580 + OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
1.581 + parse_multi_syntax P.xname (parse_syntax I)
1.582 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.583 + fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
1.584 + );
1.585 +
1.586 +val _ =
1.587 + OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
1.588 + parse_multi_syntax P.term_group (parse_syntax fst)
1.589 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.590 + fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
1.591 + (Code_Printer.simple_const_syntax syn)) syns)
1.592 + );
1.593 +
1.594 +val _ =
1.595 + OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
1.596 + P.name -- Scan.repeat1 P.name
1.597 + >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
1.598 + );
1.599 +
1.600 +val _ =
1.601 + OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
1.602 + P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
1.603 + | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
1.604 + >> (fn ((target, name), content_consts) =>
1.605 + (Toplevel.theory o add_include_cmd target) (name, content_consts))
1.606 + );
1.607 +
1.608 +val _ =
1.609 + OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
1.610 + P.name -- Scan.repeat1 (P.name -- P.name)
1.611 + >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
1.612 + );
1.613 +
1.614 +val _ =
1.615 + OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
1.616 + Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
1.617 + );
1.618 +
1.619 +val _ =
1.620 + OuterSyntax.command "export_code" "generate executable code for constants"
1.621 + K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
1.622 +
1.623 +fun shell_command thyname cmd = Toplevel.program (fn _ =>
1.624 + (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
1.625 + ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
1.626 + of SOME f => (writeln "Now generating code..."; f (theory thyname))
1.627 + | NONE => error ("Bad directive " ^ quote cmd)))
1.628 + handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
1.629 +
1.630 +end; (*local*)
1.631 +
1.632 +end; (*struct*)