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