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