1(*  Title:      Tools/Code/code_target.ML
2    Author:     Florian Haftmann, TU Muenchen
3
4Generic infrastructure for target language data.
5*)
6
7signature CODE_TARGET =
8sig
9  val cert_tyco: Proof.context -> string -> string
10  val read_tyco: Proof.context -> string -> string
11
12  val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
13    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
14  val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
15    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
16  val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
17    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
18  val check_code_for: Proof.context -> string -> bool -> Token.T list
19    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
20
21  val export_code: Proof.context -> bool -> string list
22    -> (((string * string) * Path.T option) * Token.T list) list -> unit
23  val produce_code: Proof.context -> bool -> string list
24    -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
25  val present_code: Proof.context -> string list -> Code_Symbol.T list
26    -> string -> int option -> string -> Token.T list -> string
27  val check_code: Proof.context -> bool -> string list
28    -> ((string * bool) * Token.T list) list -> unit
29
30  val generatedN: string
31  val compilation_text: Proof.context -> string -> Code_Thingol.program
32    -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
33    -> (string * string) list * string
34  val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
35    -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
36    -> ((string * string) list * string) * (Code_Symbol.T -> string option)
37
38  type serializer
39  type literals = Code_Printer.literals
40  type language
41  type ancestry
42  val assert_target: theory -> string -> string
43  val add_language: string * language -> theory -> theory
44  val add_derived_target: string * ancestry -> theory -> theory
45  val the_literals: Proof.context -> string -> literals
46  type serialization
47  val parse_args: 'a parser -> Token.T list -> 'a
48  val serialization: (int -> Path.T option -> 'a -> unit)
49    -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
50    -> 'a -> serialization
51  val default_code_width: int Config.T
52
53  type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
54  val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
55    -> theory -> theory
56  val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
57    -> theory -> theory
58  val add_reserved: string -> string -> theory -> theory
59end;
60
61structure Code_Target : CODE_TARGET =
62struct
63
64open Basic_Code_Symbol;
65open Basic_Code_Thingol;
66
67type literals = Code_Printer.literals;
68type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl =
69  (string * (string * 'a option) list, string * (string * 'b option) list,
70    class * (string * 'c option) list, (class * class) * (string * 'd option) list,
71    (class * string) * (string * 'e option) list,
72    string * (string * 'f option) list) Code_Symbol.attr;
73
74type tyco_syntax = Code_Printer.tyco_syntax;
75type raw_const_syntax = Code_Printer.raw_const_syntax;
76
77
78(** checking and parsing of symbols **)
79
80fun cert_const ctxt const =
81  let
82    val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then ()
83      else error ("No such constant: " ^ quote const);
84  in const end;
85
86fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
87
88fun cert_tyco ctxt tyco =
89  let
90    val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
91      else error ("No such type constructor: " ^ quote tyco);
92  in tyco end;
93
94fun read_tyco ctxt =
95  #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt;
96
97fun cert_class ctxt class =
98  let
99    val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
100  in class end;
101
102val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
103
104fun cert_inst ctxt (class, tyco) =
105  (cert_class ctxt class, cert_tyco ctxt tyco);
106
107fun read_inst ctxt (raw_tyco, raw_class) =
108  (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
109
110val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class;
111
112fun cert_syms ctxt =
113  Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
114    (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
115
116fun read_syms ctxt =
117  Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
118    (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
119
120fun check_name is_module s =
121  let
122    val _ = if s = "" then error "Bad empty code name" else ();
123    val xs = Long_Name.explode s;
124    val xs' = if is_module
125        then map (Name.desymbolize NONE) xs
126      else if length xs < 2
127        then error ("Bad code name without module component: " ^ quote s)
128      else
129        let
130          val (ys, y) = split_last xs;
131          val ys' = map (Name.desymbolize NONE) ys;
132          val y' = Name.desymbolize NONE y;
133        in ys' @ [y'] end;
134  in if xs' = xs
135    then if is_module then (xs, "") else split_last xs
136    else error ("Invalid code name: " ^ quote s ^ "\n"
137      ^ "better try " ^ quote (Long_Name.implode xs'))
138  end;
139
140
141(** serializations and serializer **)
142
143(* serialization: abstract nonsense to cover different destinies for generated code *)
144
145datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
146type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
147
148fun serialization output _ content width (Export some_path) =
149      (output width some_path content; NONE)
150  | serialization _ string content width Produce =
151      string [] width content |> SOME
152  | serialization _ string content width (Present syms) =
153     string syms width content
154     |> (apfst o map o apsnd) Output.output
155     |> SOME;
156
157fun export some_path f = (f (Export some_path); ());
158fun produce f = the (f Produce);
159fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
160
161
162(* serializers: functions producing serializations *)
163
164type serializer = Token.T list
165  -> Proof.context
166  -> {
167    module_name: string,
168    reserved_syms: string list,
169    identifiers: Code_Printer.identifiers,
170    includes: (string * Pretty.T) list,
171    class_syntax: string -> string option,
172    tyco_syntax: string -> Code_Printer.tyco_syntax option,
173    const_syntax: string -> Code_Printer.const_syntax option }
174  -> Code_Symbol.T list
175  -> Code_Thingol.program
176  -> serialization;
177
178  
179(** theory data **)
180
181type language = {serializer: serializer, literals: literals,
182  check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
183  evaluation_args: Token.T list}; 
184
185type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
186
187val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
188
189type target = {serial: serial, language: language, ancestry: ancestry};
190
191structure Targets = Theory_Data
192(
193  type T = (target * Code_Printer.data) Symtab.table;
194  val empty = Symtab.empty;
195  val extend = I;
196  fun merge (targets1, targets2) : T =
197    Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
198      if #serial target1 = #serial target2 then
199      ({serial = #serial target1, language = #language target1,
200        ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
201        Code_Printer.merge_data (data1, data2))
202      else error ("Incompatible targets: " ^ quote target_name) 
203    ) (targets1, targets2)
204);
205
206fun exists_target thy = Symtab.defined (Targets.get thy);
207fun lookup_target_data thy = Symtab.lookup (Targets.get thy);
208fun assert_target thy target_name =
209  if exists_target thy target_name
210  then target_name
211  else error ("Unknown code target language: " ^ quote target_name);
212
213fun fold1 f xs = fold f (tl xs) (hd xs);
214
215fun join_ancestry thy target_name =
216  let
217    val _ = assert_target thy target_name; 
218    val the_target_data = the o lookup_target_data thy;
219    val (target, this_data) = the_target_data target_name;
220    val ancestry = #ancestry target;
221    val modifies = rev (map snd ancestry);
222    val modify = fold (curry (op o)) modifies I;
223    val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
224    val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
225  in (modify, (target, data)) end;
226
227  fun allocate_target target_name target thy =
228  let
229    val _ = if exists_target thy target_name
230      then error ("Attempt to overwrite existing target " ^ quote target_name)
231      else ();
232  in
233    thy
234    |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
235  end;
236
237fun add_language (target_name, language) =
238  allocate_target target_name {serial = serial (), language = language,
239    ancestry = []};
240
241fun add_derived_target (target_name, initial_ancestry) thy =
242  let
243    val _ = if null initial_ancestry
244      then error "Must derive from existing target(s)" else ();
245    fun the_target_data target_name' = case lookup_target_data thy target_name' of
246      NONE => error ("Unknown code target language: " ^ quote target_name')
247    | SOME target_data' => target_data';
248    val targets = rev (map (fst o the_target_data o fst) initial_ancestry);
249    val supremum = fold1 (fn target' => fn target =>
250      if #serial target = #serial target'
251      then target else error "Incompatible targets") targets;
252    val ancestries = map #ancestry targets @ [initial_ancestry];
253    val ancestry = fold1 (fn ancestry' => fn ancestry =>
254      merge_ancestry (ancestry, ancestry')) ancestries;
255  in
256    allocate_target target_name {serial = #serial supremum, language = #language supremum,
257      ancestry = ancestry} thy 
258  end;
259  
260fun map_data target_name f thy =
261  let
262    val _ = assert_target thy target_name;
263  in
264    thy
265    |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
266  end;
267
268fun map_reserved target_name =
269  map_data target_name o @{apply 3 (1)};
270fun map_identifiers target_name =
271  map_data target_name o @{apply 3 (2)};
272fun map_printings target_name =
273  map_data target_name o @{apply 3 (3)};
274
275
276(** serializer usage **)
277
278(* technical aside: pretty printing width *)
279
280val default_code_width = Attrib.setup_config_int @{binding "default_code_width"} (K 80);
281
282
283(* montage *)
284
285fun the_language ctxt =
286  #language o fst o the o lookup_target_data (Proof_Context.theory_of ctxt);
287
288fun the_literals ctxt = #literals o the_language ctxt;
289
290fun the_evaluation_args ctxt = #evaluation_args o the_language ctxt;
291
292local
293
294fun activate_target ctxt target_name =
295  let
296    val thy = Proof_Context.theory_of ctxt;
297    val (modify, target_data) = join_ancestry thy target_name;
298  in (target_data, modify) end;
299
300fun project_program ctxt syms_hidden syms1 program2 =
301  let
302    val syms2 = subtract (op =) syms_hidden syms1;
303    val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
304    val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
305    val unimplemented = Code_Thingol.unimplemented program3;
306    val _ =
307      if null unimplemented then ()
308      else error ("No code equations for " ^
309        commas (map (Proof_Context.markup_const ctxt) unimplemented));
310    val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
311  in (syms4, program4) end;
312
313fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
314    printings module_name args proto_program syms =
315  let
316    val syms_hidden = Code_Symbol.symbols_of printings;
317    val (syms_all, program) = project_program ctxt syms_hidden syms proto_program;
318    fun select_include (name, (content, cs)) =
319      if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
320      then SOME (name, content) else NONE;
321    val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
322  in
323    (serializer args ctxt {
324      module_name = module_name,
325      reserved_syms = reserved,
326      identifiers = identifiers,
327      includes = includes,
328      const_syntax = Code_Symbol.lookup_constant_data printings,
329      tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
330      class_syntax = Code_Symbol.lookup_type_class_data printings },
331      (subtract (op =) syms_hidden syms, program))
332  end;
333
334fun mount_serializer ctxt target_name some_width module_name args program syms =
335  let
336    val default_width = Config.get ctxt default_code_width;
337    val ((target, data), modify) = activate_target ctxt target_name;
338    val serializer = (#serializer o #language) target;
339    val (prepared_serializer, (prepared_syms, prepared_program)) =
340      prepare_serializer ctxt serializer
341        (Code_Printer.the_reserved data) (Code_Printer.the_identifiers data)
342        (Code_Printer.the_printings data)
343        module_name args (modify program) syms
344    val width = the_default default_width some_width;
345  in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
346
347fun invoke_serializer ctxt target_name some_width raw_module_name args program all_public syms =
348  let
349    val module_name = if raw_module_name = "" then ""
350      else (check_name true raw_module_name; raw_module_name)
351    val (mounted_serializer, (prepared_syms, prepared_program)) =
352      mount_serializer ctxt target_name some_width module_name args program syms;
353  in
354    Code_Preproc.timed_exec "serializing"
355      (fn () => mounted_serializer prepared_program (if all_public then [] else prepared_syms)) ctxt
356  end;
357
358fun assert_module_name "" = error "Empty module name not allowed here"
359  | assert_module_name module_name = module_name;
360
361val using_master_directory =
362  Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
363
364in
365
366val generatedN = "Generated_Code";
367
368fun export_code_for ctxt some_path target_name some_width module_name args =
369  export (using_master_directory ctxt some_path)
370  ooo invoke_serializer ctxt target_name some_width module_name args;
371
372fun produce_code_for ctxt target_name some_width module_name args =
373  let
374    val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
375  in fn program => fn all_public => fn syms =>
376    produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
377  end;
378
379fun present_code_for ctxt target_name some_width module_name args =
380  let
381    val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
382  in fn program => fn (syms, selects) =>
383    present selects (serializer program false syms)
384  end;
385
386fun check_code_for ctxt target_name strict args program all_public syms =
387  let
388    val { env_var, make_destination, make_command } =
389      (#check o the_language ctxt) target_name;
390    fun ext_check p =
391      let
392        val destination = make_destination p;
393        val _ = export (SOME destination) (invoke_serializer ctxt target_name (SOME 80)
394          generatedN args program all_public syms);
395        val cmd = make_command generatedN;
396      in
397        if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
398        then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
399        else ()
400      end;
401  in
402    if not (env_var = "") andalso getenv env_var = ""
403    then if strict
404      then error (env_var ^ " not set; cannot check code for " ^ target_name)
405      else warning (env_var ^ " not set; skipped checking code for " ^ target_name)
406    else Isabelle_System.with_tmp_dir "Code_Test" ext_check
407  end;
408
409fun dynamic_compilation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
410  let
411    val _ = if Code_Thingol.contains_dict_var t then
412      error "Term to be evaluated contains free dictionaries" else ();
413    val v' = singleton (Name.variant_list (map fst vs)) "a";
414    val vs' = (v', []) :: vs;
415    val ty' = ITyVar v' `-> ty;
416    val program = prepared_program
417      |> Code_Symbol.Graph.new_node (Code_Symbol.value,
418          Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE))
419      |> fold (curry (perhaps o try o
420          Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
421    val (program_code, deresolve) =
422      produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
423    val value_name = the (deresolve Code_Symbol.value);
424  in ((program_code, value_name), deresolve) end;
425
426fun compilation_text' ctxt target_name some_module_name program syms =
427  let
428    val evaluation_args = the_evaluation_args ctxt target_name;
429    val (mounted_serializer, (_, prepared_program)) =
430      mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) evaluation_args program syms;
431  in
432    Code_Preproc.timed_exec "serializing"
433    (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt
434  end;
435
436fun compilation_text ctxt target_name program syms =
437  fst oo compilation_text' ctxt target_name NONE program syms
438  
439end; (* local *)
440
441
442(* code generation *)
443
444fun prep_destination (s, pos) =
445  if s = "" then NONE
446  else
447    let
448      val _ = Position.report pos Markup.language_path;
449      val path = Path.explode s;
450      val _ = Position.report pos (Markup.path (Path.smart_implode path));
451    in SOME path end;
452
453fun export_code ctxt all_public cs seris =
454  let
455    val program = Code_Thingol.consts_program ctxt cs;
456    val _ = map (fn (((target_name, module_name), some_path), args) =>
457      export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
458  in () end;
459
460fun export_code_cmd all_public raw_cs seris ctxt =
461  export_code ctxt all_public
462    (Code_Thingol.read_const_exprs ctxt raw_cs)
463    ((map o apfst o apsnd) prep_destination seris);
464
465fun produce_code ctxt all_public cs target_name some_width some_module_name args =
466  let
467    val program = Code_Thingol.consts_program ctxt cs;
468  in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end;
469
470fun present_code ctxt cs syms target_name some_width some_module_name args =
471  let
472    val program = Code_Thingol.consts_program ctxt cs;
473  in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end;
474
475fun check_code ctxt all_public cs seris =
476  let
477    val program = Code_Thingol.consts_program ctxt cs;
478    val _ = map (fn ((target_name, strict), args) =>
479      check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris;
480  in () end;
481
482fun check_code_cmd all_public raw_cs seris ctxt =
483  check_code ctxt all_public
484    (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
485
486local
487
488val parse_const_terms = Scan.repeat1 Args.term
489  >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
490
491fun parse_names category parse internalize mark_symbol =
492  Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
493  >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
494
495val parse_consts = parse_names "consts" Args.term
496  (Code.check_const o Proof_Context.theory_of) Constant;
497
498val parse_types = parse_names "types" (Scan.lift Args.name)
499  (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
500
501val parse_classes = parse_names "classes" (Scan.lift Args.name)
502  (Sign.intern_class o Proof_Context.theory_of) Type_Class;
503
504val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
505  (fn ctxt => fn (raw_tyco, raw_class) =>
506    let
507      val thy = Proof_Context.theory_of ctxt;
508    in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
509
510in
511
512val _ = Theory.setup
513  (Thy_Output.antiquotation_raw @{binding code_stmts}
514    (parse_const_terms --
515      Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
516      -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
517    (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
518      Latex.string
519        (present_code ctxt (mk_cs ctxt)
520          (maps (fn f => f ctxt) mk_stmtss)
521          target_name some_width "Example" [])));
522
523end;
524
525
526(** serializer configuration **)
527
528(* reserved symbol names *)
529
530fun add_reserved target_name sym thy =
531  let
532    val (_, (_, data)) = join_ancestry thy target_name;
533    val _ = if member (op =) (Code_Printer.the_reserved data) sym
534      then error ("Reserved symbol " ^ quote sym ^ " already declared")
535      else ();
536  in
537    thy
538    |> map_reserved target_name (insert (op =) sym)
539  end;
540
541
542(* checking of syntax *)
543
544fun check_const_syntax ctxt target_name c syn =
545  if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c
546  then error ("Too many arguments in syntax for constant " ^ quote c)
547  else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target_name) c syn;
548
549fun check_tyco_syntax ctxt target_name tyco syn =
550  if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco
551  then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
552  else syn;
553
554
555(* custom symbol names *)
556
557fun arrange_name_decls x =
558  let
559    fun arrange is_module (sym, target_names) = map (fn (target, some_name) =>
560      (target, (sym, Option.map (check_name is_module) some_name))) target_names;
561  in
562    Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false)
563      (arrange false) (arrange false) (arrange true) x
564  end;
565
566fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls;
567
568fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls;
569
570fun set_identifier (target_name, sym_name) = map_identifiers target_name (Code_Symbol.set_data sym_name);
571
572fun gen_set_identifiers prep_name_decl raw_name_decls thy =
573  fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy;
574
575val set_identifiers = gen_set_identifiers cert_name_decls;
576val set_identifiers_cmd = gen_set_identifiers read_name_decls;
577
578
579(* custom printings *)
580
581fun arrange_printings prep_const ctxt =
582  let
583    fun arrange check (sym, target_syns) =
584      map (fn (target_name, some_syn) =>
585        (target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns;
586  in
587    Code_Symbol.maps_attr'
588      (arrange check_const_syntax) (arrange check_tyco_syntax)
589        (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
590        (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
591          (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
592            map (prep_const ctxt) raw_cs)))
593  end;
594
595fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;
596
597fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt;
598
599fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn);
600
601fun gen_set_printings prep_print_decl raw_print_decls thy =
602  fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
603
604val set_printings = gen_set_printings cert_printings;
605val set_printings_cmd = gen_set_printings read_printings;
606
607
608(* concrete syntax *)
609
610fun parse_args f args =
611  case Scan.read Token.stopper f args
612   of SOME x => x
613    | NONE => error "Bad serializer arguments";
614
615
616(** Isar setup **)
617
618fun parse_single_symbol_pragma parse_keyword parse_isa parse_target =
619  parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
620    -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target)));
621
622fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
623  parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
624    >> Constant
625  || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
626    >> Type_Constructor
627  || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
628    >> Type_Class
629  || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
630    >> Class_Relation
631  || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
632    >> Class_Instance
633  || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
634    >> Code_Symbol.Module;
635
636fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
637  Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
638    (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
639
640val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [];
641
642fun code_expr_inP all_public raw_cs =
643  Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
644    -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
645    -- Scan.optional (@{keyword "file"} |-- Parse.position Parse.path) ("", Position.none)
646    -- code_expr_argsP))
647      >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
648
649fun code_expr_checkingP all_public raw_cs =
650  (@{keyword "checking"} |-- Parse.!!!
651    (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true)
652    -- code_expr_argsP)))
653      >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
654
655val code_exprP = (Scan.optional (@{keyword "open"} |-- Scan.succeed true) false
656  -- Scan.repeat1 Parse.term)
657  :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
658
659val _ =
660  Outer_Syntax.command @{command_keyword code_reserved}
661    "declare words as reserved for target language"
662    (Parse.name -- Scan.repeat1 Parse.name
663      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
664
665val _ =
666  Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
667    (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
668      >> (Toplevel.theory o fold set_identifiers_cmd));
669
670val _ =
671  Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
672    (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
673      Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
674      (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
675      >> (Toplevel.theory o fold set_printings_cmd));
676
677val _ =
678  Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
679    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
680
681end; (*struct*)
682