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