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