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 val read_const_exprs: theory -> string list -> string list |
11 val read_const_exprs: theory -> string list -> string list |
12 |
12 |
13 val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list |
13 val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list |
14 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit |
14 -> Code_Thingol.program -> Code_Symbol.symbol list -> unit |
15 val produce_code_for: theory -> string -> int option -> string -> Token.T list |
15 val produce_code_for: theory -> string -> int option -> string -> Token.T list |
16 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list |
16 -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list |
17 val present_code_for: theory -> string -> int option -> string -> Token.T list |
17 val present_code_for: theory -> string -> int option -> string -> Token.T list |
18 -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string |
18 -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string |
19 val check_code_for: theory -> string -> bool -> Token.T list |
19 val check_code_for: theory -> string -> bool -> Token.T list |
20 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit |
20 -> Code_Thingol.program -> Code_Symbol.symbol list -> unit |
21 |
21 |
22 val export_code: theory -> string list |
22 val export_code: theory -> string list |
23 -> (((string * string) * Path.T option) * Token.T list) list -> unit |
23 -> (((string * string) * Path.T option) * Token.T list) list -> unit |
24 val produce_code: theory -> string list |
24 val produce_code: theory -> string list |
25 -> string -> int option -> string -> Token.T list -> (string * string) list * string option list |
25 -> string -> int option -> string -> Token.T list -> (string * string) list * string option list |
26 val present_code: theory -> string list -> (Code_Thingol.naming -> string list) |
26 val present_code: theory -> string list -> Code_Symbol.symbol list |
27 -> string -> int option -> string -> Token.T list -> string |
27 -> string -> int option -> string -> Token.T list -> string |
28 val check_code: theory -> string list |
28 val check_code: theory -> string list |
29 -> ((string * bool) * Token.T list) list -> unit |
29 -> ((string * bool) * Token.T list) list -> unit |
30 |
30 |
31 val generatedN: string |
31 val generatedN: string |
32 val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program |
32 val evaluator: theory -> string -> Code_Thingol.program |
33 -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm |
33 -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm |
34 -> (string * string) list * string |
34 -> (string * string) list * string |
35 |
35 |
36 type serializer |
36 type serializer |
37 type literals = Code_Printer.literals |
37 type literals = Code_Printer.literals |
38 val add_target: string * { serializer: serializer, literals: literals, |
38 val add_target: string * { serializer: serializer, literals: literals, |
39 check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } |
39 check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } |
40 -> theory -> theory |
40 -> theory -> theory |
41 val extend_target: string * |
41 val extend_target: string * |
42 (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program)) |
42 (string * (Code_Thingol.program -> Code_Thingol.program)) |
43 -> theory -> theory |
43 -> theory -> theory |
44 val assert_target: theory -> string -> string |
44 val assert_target: theory -> string -> string |
45 val the_literals: theory -> string -> literals |
45 val the_literals: theory -> string -> literals |
46 type serialization |
46 type serialization |
47 val parse_args: 'a parser -> Token.T list -> 'a |
47 val parse_args: 'a parser -> Token.T list -> 'a |
48 val serialization: (int -> Path.T option -> 'a -> unit) |
48 val serialization: (int -> Path.T option -> 'a -> unit) |
49 -> (string list -> int -> 'a -> (string * string) list * (string -> string option)) |
49 -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option)) |
50 -> 'a -> serialization |
50 -> 'a -> serialization |
51 val set_default_code_width: int -> theory -> theory |
51 val set_default_code_width: int -> theory -> theory |
52 |
52 |
53 type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl |
53 type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl |
54 type identifier_data |
54 type identifier_data |
152 |
152 |
153 (** serializations and serializer **) |
153 (** serializations and serializer **) |
154 |
154 |
155 (* serialization: abstract nonsense to cover different destinies for generated code *) |
155 (* serialization: abstract nonsense to cover different destinies for generated code *) |
156 |
156 |
157 datatype destination = Export of Path.T option | Produce | Present of string list; |
157 datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list; |
158 type serialization = int -> destination -> ((string * string) list * (string -> string option)) option; |
158 type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option; |
159 |
159 |
160 fun serialization output _ content width (Export some_path) = |
160 fun serialization output _ content width (Export some_path) = |
161 (output width some_path content; NONE) |
161 (output width some_path content; NONE) |
162 | serialization _ string content width Produce = |
162 | serialization _ string content width Produce = |
163 string [] width content |> SOME |
163 string [] width content |> SOME |
164 | serialization _ string content width (Present stmt_names) = |
164 | serialization _ string content width (Present syms) = |
165 string stmt_names width content |
165 string syms width content |
166 |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str) |
166 |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str) |
167 |> SOME; |
167 |> SOME; |
168 |
168 |
169 fun export some_path f = (f (Export some_path); ()); |
169 fun export some_path f = (f (Export some_path); ()); |
170 fun produce f = the (f Produce); |
170 fun produce f = the (f Produce); |
171 fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names))))); |
171 fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms))))); |
172 |
172 |
173 |
173 |
174 (* serializers: functions producing serializations *) |
174 (* serializers: functions producing serializations *) |
175 |
175 |
176 type serializer = Token.T list |
176 type serializer = Token.T list |
177 -> Proof.context |
177 -> Proof.context |
178 -> { |
178 -> { |
179 symbol_of: string -> Code_Symbol.symbol, |
|
180 module_name: string, |
179 module_name: string, |
181 reserved_syms: string list, |
180 reserved_syms: string list, |
182 identifiers: identifier_data, |
181 identifiers: identifier_data, |
183 includes: (string * Pretty.T) list, |
182 includes: (string * Pretty.T) list, |
184 class_syntax: string -> string option, |
183 class_syntax: string -> string option, |
324 let |
323 let |
325 val (_, default_width) = Targets.get thy; |
324 val (_, default_width) = Targets.get thy; |
326 val (modify, data) = collapse_hierarchy thy target; |
325 val (modify, data) = collapse_hierarchy thy target; |
327 in (default_width, data, modify) end; |
326 in (default_width, data, modify) end; |
328 |
327 |
329 fun activate_const_syntax thy literals cs_data naming = |
328 fun activate_symbol_syntax thy literals printings = |
330 (Symtab.empty, naming) |
329 (Code_Symbol.symbols_of printings, |
331 |> fold_map (fn (c, data) => fn (tab, naming) => |
330 (Symtab.lookup (Code_Symbol.mapped_const_data (Code_Printer.activate_const_syntax thy literals) printings), |
332 case Code_Thingol.lookup_const naming c |
331 Code_Symbol.lookup_type_constructor_data printings, Code_Symbol.lookup_type_class_data printings)) |
333 of SOME name => let |
332 |
334 val (syn, naming') = |
333 fun project_program thy syms_hidden syms1 program2 = |
335 Code_Printer.activate_const_syntax thy literals c data naming |
|
336 in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end |
|
337 | NONE => (NONE, (tab, naming))) cs_data |
|
338 |>> map_filter I; |
|
339 |
|
340 fun activate_syntax lookup_name things = |
|
341 Symtab.empty |
|
342 |> fold_map (fn (thing_identifier, data) => fn tab => case lookup_name thing_identifier |
|
343 of SOME name => (SOME name, Symtab.update_new (name, data) tab) |
|
344 | NONE => (NONE, tab)) things |
|
345 |>> map_filter I; |
|
346 |
|
347 fun activate_symbol_syntax thy literals naming printings = |
|
348 let |
|
349 val (names_const, (const_syntax, _)) = |
|
350 activate_const_syntax thy literals (Code_Symbol.dest_constant_data printings) naming; |
|
351 val (names_tyco, tyco_syntax) = |
|
352 activate_syntax (Code_Thingol.lookup_tyco naming) (Code_Symbol.dest_type_constructor_data printings); |
|
353 val (names_class, class_syntax) = |
|
354 activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings); |
|
355 val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst) |
|
356 (Code_Symbol.dest_class_instance_data printings); |
|
357 in |
|
358 (names_const @ names_tyco @ names_class @ names_inst, |
|
359 (Symtab.lookup const_syntax, Symtab.lookup tyco_syntax, Symtab.lookup class_syntax)) |
|
360 end; |
|
361 |
|
362 fun project_program thy names_hidden names1 program2 = |
|
363 let |
334 let |
364 val ctxt = Proof_Context.init_global thy; |
335 val ctxt = Proof_Context.init_global thy; |
365 val names2 = subtract (op =) names_hidden names1; |
336 val syms2 = subtract (op =) syms_hidden syms1; |
366 val program3 = Graph.restrict (not o member (op =) names_hidden) program2; |
337 val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2; |
367 val names4 = Graph.all_succs program3 names2; |
338 val syms4 = Code_Symbol.Graph.all_succs program3 syms2; |
368 val unimplemented = Code_Thingol.unimplemented program3; |
339 val unimplemented = Code_Thingol.unimplemented program3; |
369 val _ = |
340 val _ = |
370 if null unimplemented then () |
341 if null unimplemented then () |
371 else error ("No code equations for " ^ |
342 else error ("No code equations for " ^ |
372 commas (map (Proof_Context.extern_const ctxt) unimplemented)); |
343 commas (map (Proof_Context.extern_const ctxt) unimplemented)); |
373 val program4 = Graph.restrict (member (op =) names4) program3; |
344 val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3; |
374 in (names4, program4) end; |
345 in (syms4, program4) end; |
375 |
346 |
376 fun prepare_serializer thy (serializer : serializer) literals reserved identifiers |
347 fun prepare_serializer thy (serializer : serializer) literals reserved identifiers |
377 printings module_name args naming proto_program names = |
348 printings module_name args proto_program syms = |
378 let |
349 let |
379 val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) = |
350 val (syms_hidden, (const_syntax, tyco_syntax, class_syntax)) = |
380 activate_symbol_syntax thy literals naming printings; |
351 activate_symbol_syntax thy literals printings; |
381 val (names_all, program) = project_program thy names_hidden names proto_program; |
352 val (syms_all, program) = project_program thy syms_hidden syms proto_program; |
382 fun select_include (name, (content, cs)) = |
353 fun select_include (name, (content, cs)) = |
383 if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c |
354 if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs |
384 of SOME name => member (op =) names_all name |
|
385 | NONE => false) cs |
|
386 then SOME (name, content) else NONE; |
355 then SOME (name, content) else NONE; |
387 val includes = map_filter select_include (Code_Symbol.dest_module_data printings); |
356 val includes = map_filter select_include (Code_Symbol.dest_module_data printings); |
388 in |
357 in |
389 (serializer args (Proof_Context.init_global thy) { |
358 (serializer args (Proof_Context.init_global thy) { |
390 symbol_of = Code_Thingol.symbol_of proto_program, |
|
391 module_name = module_name, |
359 module_name = module_name, |
392 reserved_syms = reserved, |
360 reserved_syms = reserved, |
393 identifiers = identifiers, |
361 identifiers = identifiers, |
394 includes = includes, |
362 includes = includes, |
395 const_syntax = const_syntax, |
363 const_syntax = const_syntax, |
396 tyco_syntax = tyco_syntax, |
364 tyco_syntax = tyco_syntax, |
397 class_syntax = class_syntax }, |
365 class_syntax = class_syntax }, |
398 program) |
366 program) |
399 end; |
367 end; |
400 |
368 |
401 fun mount_serializer thy target some_width module_name args naming program names = |
369 fun mount_serializer thy target some_width module_name args program syms = |
402 let |
370 let |
403 val (default_width, data, modify) = activate_target thy target; |
371 val (default_width, data, modify) = activate_target thy target; |
404 val serializer = case the_description data |
372 val serializer = case the_description data |
405 of Fundamental seri => #serializer seri; |
373 of Fundamental seri => #serializer seri; |
406 val (prepared_serializer, prepared_program) = |
374 val (prepared_serializer, prepared_program) = |
407 prepare_serializer thy serializer (the_literals thy target) |
375 prepare_serializer thy serializer (the_literals thy target) |
408 (the_reserved data) (the_identifiers data) (the_printings data) |
376 (the_reserved data) (the_identifiers data) (the_printings data) |
409 module_name args naming (modify naming program) names |
377 module_name args (modify program) syms |
410 val width = the_default default_width some_width; |
378 val width = the_default default_width some_width; |
411 in (fn program => prepared_serializer program width, prepared_program) end; |
379 in (fn program => prepared_serializer program width, prepared_program) end; |
412 |
380 |
413 fun invoke_serializer thy target some_width module_name args naming program names = |
381 fun invoke_serializer thy target some_width module_name args program syms = |
414 let |
382 let |
415 val check = if module_name = "" then I else check_name true; |
383 val check = if module_name = "" then I else check_name true; |
416 val (mounted_serializer, prepared_program) = mount_serializer thy |
384 val (mounted_serializer, prepared_program) = mount_serializer thy |
417 target some_width (check module_name) args naming program names; |
385 target some_width (check module_name) args program syms; |
418 in mounted_serializer prepared_program end; |
386 in mounted_serializer prepared_program end; |
419 |
387 |
420 fun assert_module_name "" = error "Empty module name not allowed here" |
388 fun assert_module_name "" = error "Empty module name not allowed here" |
421 | assert_module_name module_name = module_name; |
389 | assert_module_name module_name = module_name; |
422 |
390 |
427 |
395 |
428 val generatedN = "Generated_Code"; |
396 val generatedN = "Generated_Code"; |
429 |
397 |
430 fun export_code_for thy some_path target some_width module_name args = |
398 fun export_code_for thy some_path target some_width module_name args = |
431 export (using_master_directory thy some_path) |
399 export (using_master_directory thy some_path) |
432 ooo invoke_serializer thy target some_width module_name args; |
400 oo invoke_serializer thy target some_width module_name args; |
433 |
401 |
434 fun produce_code_for thy target some_width module_name args = |
402 fun produce_code_for thy target some_width module_name args = |
435 let |
403 let |
436 val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; |
404 val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; |
437 in fn naming => fn program => fn names => |
405 in fn program => fn syms => |
438 produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names) |
406 produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms) |
439 end; |
407 end; |
440 |
408 |
441 fun present_code_for thy target some_width module_name args = |
409 fun present_code_for thy target some_width module_name args = |
442 let |
410 let |
443 val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; |
411 val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; |
444 in fn naming => fn program => fn (names, selects) => |
412 in fn program => fn (syms, selects) => |
445 present selects (serializer naming program names) |
413 present selects (serializer program syms) |
446 end; |
414 end; |
447 |
415 |
448 fun check_code_for thy target strict args naming program names_cs = |
416 fun check_code_for thy target strict args program syms = |
449 let |
417 let |
450 val { env_var, make_destination, make_command } = |
418 val { env_var, make_destination, make_command } = |
451 (#check o the_fundamental thy) target; |
419 (#check o the_fundamental thy) target; |
452 fun ext_check p = |
420 fun ext_check p = |
453 let |
421 let |
454 val destination = make_destination p; |
422 val destination = make_destination p; |
455 val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) |
423 val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) |
456 generatedN args naming program names_cs); |
424 generatedN args program syms); |
457 val cmd = make_command generatedN; |
425 val cmd = make_command generatedN; |
458 in |
426 in |
459 if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 |
427 if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 |
460 then error ("Code check failed for " ^ target ^ ": " ^ cmd) |
428 then error ("Code check failed for " ^ target ^ ": " ^ cmd) |
461 else () |
429 else () |
466 then error (env_var ^ " not set; cannot check code for " ^ target) |
434 then error (env_var ^ " not set; cannot check code for " ^ target) |
467 else warning (env_var ^ " not set; skipped checking code for " ^ target) |
435 else warning (env_var ^ " not set; skipped checking code for " ^ target) |
468 else Isabelle_System.with_tmp_dir "Code_Test" ext_check |
436 else Isabelle_System.with_tmp_dir "Code_Test" ext_check |
469 end; |
437 end; |
470 |
438 |
471 fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) = |
439 fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) = |
472 let |
440 let |
473 val _ = if Code_Thingol.contains_dict_var t then |
441 val _ = if Code_Thingol.contains_dict_var t then |
474 error "Term to be evaluated contains free dictionaries" else (); |
442 error "Term to be evaluated contains free dictionaries" else (); |
475 val v' = singleton (Name.variant_list (map fst vs)) "a"; |
443 val v' = singleton (Name.variant_list (map fst vs)) "a"; |
476 val vs' = (v', []) :: vs; |
444 val vs' = (v', []) :: vs; |
477 val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty]; |
445 val ty' = ITyVar v' `-> ty; |
478 val value_name = "Value.value.value" |
|
479 val program = prepared_program |
446 val program = prepared_program |
480 |> Graph.new_node (value_name, |
447 |> Code_Symbol.Graph.new_node (Code_Symbol.value, |
481 Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))) |
448 Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)) |
482 |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts; |
449 |> fold (curry (perhaps o try o |
|
450 Code_Symbol.Graph.add_edge) Code_Symbol.value) syms; |
483 val (program_code, deresolve) = produce (mounted_serializer program); |
451 val (program_code, deresolve) = produce (mounted_serializer program); |
484 val value_name' = the (deresolve value_name); |
452 val value_name = the (deresolve Code_Symbol.value); |
485 in (program_code, value_name') end; |
453 in (program_code, value_name) end; |
486 |
454 |
487 fun evaluator thy target naming program consts = |
455 fun evaluator thy target program syms = |
488 let |
456 let |
489 val (mounted_serializer, prepared_program) = mount_serializer thy |
457 val (mounted_serializer, prepared_program) = |
490 target NONE generatedN [] naming program consts; |
458 mount_serializer thy target NONE generatedN [] program syms; |
491 in evaluation mounted_serializer prepared_program consts end; |
459 in evaluation mounted_serializer prepared_program syms end; |
492 |
460 |
493 end; (* local *) |
461 end; (* local *) |
494 |
462 |
495 |
463 |
496 (* code generation *) |
464 (* code generation *) |
497 |
465 |
498 fun implemented_functions thy naming program = |
466 fun read_const_exprs thy const_exprs = |
499 let |
467 let |
500 val cs = Code_Thingol.unimplemented program; |
468 val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs; |
501 val names = map_filter (Code_Thingol.lookup_const naming) cs; |
469 val program = Code_Thingol.consts_program thy true cs2; |
502 in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end; |
470 val cs3 = Code_Thingol.implemented_deps program; |
503 |
|
504 fun read_const_exprs thy cs = |
|
505 let |
|
506 val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs; |
|
507 val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2; |
|
508 val names3 = implemented_functions thy naming program; |
|
509 val cs3 = map_filter (fn (c, name) => |
|
510 if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); |
|
511 in union (op =) cs3 cs1 end; |
471 in union (op =) cs3 cs1 end; |
512 |
472 |
513 fun prep_destination "" = NONE |
473 fun prep_destination "" = NONE |
514 | prep_destination s = SOME (Path.explode s); |
474 | prep_destination s = SOME (Path.explode s); |
515 |
475 |
516 fun export_code thy cs seris = |
476 fun export_code thy cs seris = |
517 let |
477 let |
518 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; |
478 val program = Code_Thingol.consts_program thy false cs; |
519 val _ = map (fn (((target, module_name), some_path), args) => |
479 val _ = map (fn (((target, module_name), some_path), args) => |
520 export_code_for thy some_path target NONE module_name args naming program names_cs) seris; |
480 export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris; |
521 in () end; |
481 in () end; |
522 |
482 |
523 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) |
483 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) |
524 ((map o apfst o apsnd) prep_destination seris); |
484 ((map o apfst o apsnd) prep_destination seris); |
525 |
485 |
526 fun produce_code thy cs target some_width some_module_name args = |
486 fun produce_code thy cs target some_width some_module_name args = |
527 let |
487 let |
528 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; |
488 val program = Code_Thingol.consts_program thy false cs; |
529 in produce_code_for thy target some_width some_module_name args naming program names_cs end; |
489 in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end; |
530 |
490 |
531 fun present_code thy cs names_stmt target some_width some_module_name args = |
491 fun present_code thy cs syms target some_width some_module_name args = |
532 let |
492 let |
533 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; |
493 val program = Code_Thingol.consts_program thy false cs; |
534 in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end; |
494 in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end; |
535 |
495 |
536 fun check_code thy cs seris = |
496 fun check_code thy cs seris = |
537 let |
497 let |
538 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; |
498 val program = Code_Thingol.consts_program thy false cs; |
539 val _ = map (fn ((target, strict), args) => |
499 val _ = map (fn ((target, strict), args) => |
540 check_code_for thy target strict args naming program names_cs) seris; |
500 check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris; |
541 in () end; |
501 in () end; |
542 |
502 |
543 fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris; |
503 fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris; |
544 |
504 |
545 local |
505 local |
546 |
506 |
547 val parse_const_terms = Scan.repeat1 Args.term |
507 val parse_const_terms = Scan.repeat1 Args.term |
548 >> (fn ts => fn thy => map (Code.check_const thy) ts); |
508 >> (fn ts => fn thy => map (Code.check_const thy) ts); |
549 |
509 |
550 fun parse_names category parse internalize lookup = |
510 fun parse_names category parse internalize mark_symbol = |
551 Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse |
511 Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse |
552 >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs); |
512 >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs); |
553 |
513 |
554 val parse_consts = parse_names "consts" Args.term |
514 val parse_consts = parse_names "consts" Args.term |
555 Code.check_const Code_Thingol.lookup_const; |
515 Code.check_const Code_Symbol.Constant; |
556 |
516 |
557 val parse_types = parse_names "types" (Scan.lift Args.name) |
517 val parse_types = parse_names "types" (Scan.lift Args.name) |
558 Sign.intern_type Code_Thingol.lookup_tyco; |
518 Sign.intern_type Code_Symbol.Type_Constructor; |
559 |
519 |
560 val parse_classes = parse_names "classes" (Scan.lift Args.name) |
520 val parse_classes = parse_names "classes" (Scan.lift Args.name) |
561 Sign.intern_class Code_Thingol.lookup_class; |
521 Sign.intern_class Code_Symbol.Type_Class; |
562 |
522 |
563 val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) |
523 val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) |
564 (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco)) |
524 (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) |
565 Code_Thingol.lookup_instance; |
525 Code_Symbol.Class_Instance; |
566 |
526 |
567 in |
527 in |
568 |
528 |
569 val antiq_setup = |
529 val antiq_setup = |
570 Thy_Output.antiquotation @{binding code_stmts} |
530 Thy_Output.antiquotation @{binding code_stmts} |