equal
deleted
inserted
replaced
9 val cert_tyco: theory -> string -> string |
9 val cert_tyco: theory -> string -> string |
10 val read_tyco: theory -> string -> string |
10 val read_tyco: theory -> string -> string |
11 |
11 |
12 type serializer |
12 type serializer |
13 type literals = Code_Printer.literals |
13 type literals = Code_Printer.literals |
14 val add_target: string * { serializer: serializer, literals: literals, check: unit } |
14 val add_target: string * { serializer: serializer, literals: literals, |
15 -> theory -> theory |
15 check: { env_var: string, make_destination: Path.T -> Path.T, |
|
16 make_command: string -> Path.T -> string -> string } } -> theory -> theory |
16 val extend_target: string * |
17 val extend_target: string * |
17 (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program)) |
18 (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program)) |
18 -> theory -> theory |
19 -> theory -> theory |
19 val assert_target: theory -> string -> string |
20 val assert_target: theory -> string -> string |
20 |
21 |
33 val export: serialization -> unit |
34 val export: serialization -> unit |
34 val file: Path.T -> serialization -> unit |
35 val file: Path.T -> serialization -> unit |
35 val string: string list -> serialization -> string |
36 val string: string list -> serialization -> string |
36 val code_of: theory -> string -> int option -> string |
37 val code_of: theory -> string -> int option -> string |
37 -> string list -> (Code_Thingol.naming -> string list) -> string |
38 -> string list -> (Code_Thingol.naming -> string list) -> string |
38 val external_check: theory -> string -> string |
39 val check: theory -> string -> unit |
39 -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit |
|
40 val set_default_code_width: int -> theory -> theory |
40 val set_default_code_width: int -> theory -> theory |
41 val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit |
41 val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit |
42 |
42 |
43 val allow_abort: string -> theory -> theory |
43 val allow_abort: string -> theory -> theory |
44 type tyco_syntax = Code_Printer.tyco_syntax |
44 type tyco_syntax = Code_Printer.tyco_syntax |
113 -> ((Pretty.T -> string) * (Pretty.T -> unit)) |
113 -> ((Pretty.T -> string) * (Pretty.T -> unit)) |
114 -> Code_Thingol.program |
114 -> Code_Thingol.program |
115 -> string list (*selected statements*) |
115 -> string list (*selected statements*) |
116 -> serialization; |
116 -> serialization; |
117 |
117 |
118 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit } |
118 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, |
|
119 check: { env_var: string, make_destination: Path.T -> Path.T, |
|
120 make_command: string -> Path.T -> string -> string } } |
119 | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); |
121 | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); |
120 |
122 |
121 datatype target = Target of { |
123 datatype target = Target of { |
122 serial: serial, |
124 serial: serial, |
123 description: description, |
125 description: description, |
219 |
221 |
220 (** serializer usage **) |
222 (** serializer usage **) |
221 |
223 |
222 (* montage *) |
224 (* montage *) |
223 |
225 |
224 fun the_literals thy = |
226 fun the_fundamental thy = |
225 let |
227 let |
226 val ((targets, _), _) = Targets.get thy; |
228 val ((targets, _), _) = Targets.get thy; |
227 fun literals target = case Symtab.lookup targets target |
229 fun fundamental target = case Symtab.lookup targets target |
228 of SOME data => (case the_description data |
230 of SOME data => (case the_description data |
229 of Fundamental { literals, ... } => literals |
231 of Fundamental data => data |
230 | Extension (super, _) => literals super) |
232 | Extension (super, _) => fundamental super) |
231 | NONE => error ("Unknown code target language: " ^ quote target); |
233 | NONE => error ("Unknown code target language: " ^ quote target); |
232 in literals end; |
234 in fundamental end; |
|
235 |
|
236 fun the_literals thy = #literals o the_fundamental thy; |
233 |
237 |
234 local |
238 local |
235 |
239 |
236 fun activate_syntax lookup_name src_tab = Symtab.empty |
240 fun activate_syntax lookup_name src_tab = Symtab.empty |
237 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier |
241 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier |
351 val names3 = transitivly_non_empty_funs thy naming program; |
355 val names3 = transitivly_non_empty_funs thy naming program; |
352 val cs3 = map_filter (fn (c, name) => |
356 val cs3 = map_filter (fn (c, name) => |
353 if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); |
357 if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); |
354 in union (op =) cs3 cs1 end; |
358 in union (op =) cs3 cs1 end; |
355 |
359 |
356 fun external_check thy target env_var make_destination make_command = |
360 fun check thy target = |
357 let |
361 let |
|
362 val { env_var, make_destination, make_command } = |
|
363 (#check o the_fundamental thy) target; |
358 val env_param = getenv env_var; |
364 val env_param = getenv env_var; |
359 fun ext_check env_param p = |
365 fun ext_check env_param p = |
360 let |
366 let |
361 val module_name = "Code_Test"; |
367 val module_name = "Code_Test"; |
362 val (cs, (naming, program)) = |
368 val (cs, (naming, program)) = |
372 in if env_param = "" |
378 in if env_param = "" |
373 then warning (env_var ^ " not set; skipped code check for " ^ target) |
379 then warning (env_var ^ " not set; skipped code check for " ^ target) |
374 else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param) |
380 else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param) |
375 end; |
381 end; |
376 |
382 |
|
383 |
377 fun export_code thy cs seris = |
384 fun export_code thy cs seris = |
378 let |
385 let |
379 val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs; |
386 val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs; |
380 fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export |
387 fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export |
381 else file (Path.explode dest); |
388 else file (Path.explode dest); |