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