1(* Title: Tools/Code/code_runtime.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Runtime services building on code generation into implementation language SML. 5*) 6 7signature CODE_RUNTIME = 8sig 9 val target: string 10 val value: Proof.context -> 11 (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> 12 string * string -> 'a 13 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string 14 val dynamic_value: 'a cookie -> Proof.context -> string option 15 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option 16 val dynamic_value_strict: 'a cookie -> Proof.context -> string option 17 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a 18 val dynamic_value_exn: 'a cookie -> Proof.context -> string option 19 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result 20 val dynamic_holds_conv: Proof.context -> conv 21 val code_reflect: (string * string list option) list -> string list -> string 22 -> string option -> theory -> theory 23 datatype truth = Holds 24 val put_truth: (unit -> truth) -> Proof.context -> Proof.context 25 val mount_computation: Proof.context -> (string * typ) list -> typ 26 -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a 27 val mount_computation_conv: Proof.context -> (string * typ) list -> typ 28 -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv 29 val mount_computation_check: Proof.context -> (string * typ) list 30 -> (term -> truth) -> Proof.context -> conv 31 val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory 32 val trace: bool Config.T 33end; 34 35structure Code_Runtime : CODE_RUNTIME = 36struct 37 38open Basic_Code_Symbol; 39 40(** ML compiler as evaluation environment **) 41 42(* technical prerequisites *) 43 44val thisN = "Code_Runtime"; 45val prefix_this = Long_Name.append thisN; 46val truthN = prefix_this "truth"; 47val HoldsN = prefix_this "Holds"; 48 49val target = "Eval"; 50 51datatype truth = Holds; 52 53val _ = Theory.setup 54 (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)]) 55 #> Code_Target.set_printings (Type_Constructor (@{type_name prop}, 56 [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))])) 57 #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds}, 58 [(target, SOME (Code_Printer.plain_const_syntax HoldsN))])) 59 #> Code_Target.add_reserved target thisN 60 #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]); 61 (*avoid further pervasive infix names*) 62 63val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false); 64 65fun compile_ML verbose code context = 66 (if Config.get_generic context trace then tracing code else (); 67 Code_Preproc.timed "compiling ML" Context.proof_of 68 (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context 69 {line = 0, file = "generated code", verbose = verbose, 70 debug = false} code)) context); 71 72fun value ctxt (get, put, put_ml) (prelude, value) = 73 let 74 val code = 75 prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ 76 put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))"; 77 val ctxt' = ctxt 78 |> put (fn () => error ("Bad compilation for " ^ quote put_ml)) 79 |> Context.proof_map (compile_ML false code); 80 val computator = get ctxt'; 81 in Code_Preproc.timed_exec "running ML" computator ctxt' end; 82 83 84(* evaluation into ML language values *) 85 86type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; 87 88fun reject_vars ctxt t = 89 ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t); 90 91fun build_compilation_text ctxt some_target program consts = 92 Code_Target.compilation_text ctxt (the_default target some_target) program consts false 93 #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); 94 95fun run_compilation_text cookie ctxt comp vs_t args = 96 let 97 val (program_code, value_name) = comp vs_t; 98 val value_code = space_implode " " 99 (value_name :: "()" :: map (enclose "(" ")") args); 100 in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; 101 102fun partiality_as_none e = SOME (Exn.release e) 103 handle General.Match => NONE 104 | General.Bind => NONE 105 | General.Fail _ => NONE; 106 107fun dynamic_value_exn cookie ctxt some_target postproc t args = 108 let 109 val _ = reject_vars ctxt t; 110 val _ = if Config.get ctxt trace 111 then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t)) 112 else () 113 fun comp program _ vs_ty_t deps = 114 run_compilation_text cookie ctxt (build_compilation_text ctxt some_target program deps) vs_ty_t args; 115 in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end; 116 117fun dynamic_value_strict cookie ctxt some_target postproc t args = 118 Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args); 119 120fun dynamic_value cookie ctxt some_target postproc t args = 121 partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); 122 123 124(* evaluation for truth or nothing *) 125 126structure Truth_Result = Proof_Data 127( 128 type T = unit -> truth; 129 val empty: T = fn () => raise Fail "Truth_Result"; 130 fun init _ = empty; 131); 132val put_truth = Truth_Result.put; 133val truth_cookie = (Truth_Result.get, put_truth, prefix_this "put_truth"); 134 135local 136 137val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of); 138 139fun check_holds ctxt evaluator vs_t ct = 140 let 141 val t = Thm.term_of ct; 142 val _ = if fastype_of t <> propT 143 then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t) 144 else (); 145 val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT)); 146 val result = case partiality_as_none (run_compilation_text truth_cookie ctxt evaluator vs_t []) 147 of SOME Holds => true 148 | _ => false; 149 in 150 Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) 151 end; 152 153val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result 154 (Thm.add_oracle (@{binding holds_by_evaluation}, 155 fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct))); 156 157fun check_holds_oracle ctxt evaluator vs_ty_t ct = 158 raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); 159 160in 161 162fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt 163 (fn program => fn vs_t => fn deps => 164 check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t) 165 o reject_vars ctxt; 166 167end; (*local*) 168 169 170(** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **) 171 172(* auxiliary *) 173 174val generated_computationN = "Generated_Computation"; 175 176 177(* possible type signatures of constants *) 178 179fun typ_signatures' T = 180 let 181 val (Ts, T') = strip_type T; 182 in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end; 183 184fun typ_signatures cTs = 185 let 186 fun add (c, T) = 187 fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts))) 188 (typ_signatures' T); 189 in 190 Typtab.empty 191 |> fold add cTs 192 |> Typtab.lookup_list 193 end; 194 195 196(* name mangling *) 197 198local 199 200fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco] 201 | tycos_of _ = []; 202 203val ml_name_of = Name.desymbolize NONE o Long_Name.base_name; 204 205in 206 207val covered_constsN = "covered_consts"; 208 209fun of_term_for_typ Ts = 210 let 211 val names = Ts 212 |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) 213 |> Name.variant_list []; 214 in the o AList.lookup (op =) (Ts ~~ names) end; 215 216fun eval_for_const ctxt cTs = 217 let 218 fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T)) 219 val names = cTs 220 |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list) 221 |> Name.variant_list []; 222 in the o AList.lookup (op =) (cTs ~~ names) end; 223 224end; 225 226 227(* checks for input terms *) 228 229fun monomorphic T = fold_atyps ((K o K) false) T true; 230 231fun check_typ ctxt T t = 232 Syntax.check_term ctxt (Type.constraint T t); 233 234fun check_computation_input ctxt cTs t = 235 let 236 fun check t = check_comb (strip_comb t) 237 and check_comb (t as Abs _, _) = 238 error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t) 239 | check_comb (t as Const (cT as (c, T)), ts) = 240 let 241 val _ = if not (member (op =) cTs cT) 242 then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t) 243 else (); 244 val _ = if not (monomorphic T) 245 then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t) 246 else (); 247 val _ = map check ts; 248 in () end; 249 val _ = check t; 250 in t end; 251 252 253(* code generation for of the universal morphism *) 254 255val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ; 256 257fun print_of_term_funs { typ_signatures_for, eval_for_const, of_term_for_typ } Ts = 258 let 259 val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); 260 fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" 261 |> fold (fn x => fn s => s ^ " $ " ^ x) xs 262 |> enclose "(" ")"; 263 fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T) 264 |> fold2 (fn T' => fn x => fn s => 265 s ^ (" (" ^ of_term_for_typ T' ^ " " ^ x ^ ")")) Ts xs 266 fun print_eq T (c, Ts) = 267 let 268 val xs = var_names (length Ts); 269 in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end; 270 fun print_eqs T = 271 let 272 val typ_signs = typ_signatures_for T; 273 val name = of_term_for_typ T; 274 in 275 map (print_eq T) typ_signs 276 |> map (prefix (name ^ " ")) 277 |> space_implode "\n | " 278 end; 279 in 280 map print_eqs Ts 281 |> space_implode "\nand " 282 |> prefix "fun " 283 end; 284 285fun print_computation_code ctxt compiled_value [] requested_Ts = 286 if null requested_Ts then ("", []) 287 else error ("No equation available for requested type " 288 ^ Syntax.string_of_typ ctxt (hd requested_Ts)) 289 | print_computation_code ctxt compiled_value cTs requested_Ts = 290 let 291 val proper_cTs = map_filter I cTs; 292 val typ_signatures_for = typ_signatures proper_cTs; 293 fun add_typ T Ts = 294 if member (op =) Ts T 295 then Ts 296 else case typ_signatures_for T of 297 [] => error ("No equation available for requested type " 298 ^ Syntax.string_of_typ ctxt T) 299 | typ_signs => 300 Ts 301 |> cons T 302 |> fold (fold add_typ o snd) typ_signs; 303 val required_Ts = fold add_typ requested_Ts []; 304 val of_term_for_typ' = of_term_for_typ required_Ts; 305 val eval_for_const' = eval_for_const ctxt proper_cTs; 306 val eval_for_const'' = the_default "_" o Option.map eval_for_const'; 307 val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs)); 308 fun mk_abs s = "fn " ^ s ^ " => "; 309 val eval_abs = space_implode "" 310 (map (mk_abs o eval_for_const'') cTs); 311 val of_term_code = print_of_term_funs { 312 typ_signatures_for = typ_signatures_for, 313 eval_for_const = eval_for_const', 314 of_term_for_typ = of_term_for_typ' } required_Ts; 315 val of_term_names = map (Long_Name.append generated_computationN 316 o of_term_for_typ') requested_Ts; 317 in 318 cat_lines [ 319 "structure " ^ generated_computationN ^ " =", 320 "struct", 321 "", 322 "val " ^ covered_constsN ^ " = " ^ ML_Syntax.print_list print_const proper_cTs ^ ";", 323 "", 324 "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()", 325 " (" ^ eval_abs, 326 " " ^ eval_tuple ^ ");", 327 "", 328 of_term_code, 329 "", 330 "end" 331 ] |> rpair of_term_names 332 end; 333 334 335(* dedicated preprocessor for computations *) 336 337structure Computation_Preproc_Data = Theory_Data 338( 339 type T = thm list; 340 val empty = []; 341 val extend = I; 342 val merge = Library.merge Thm.eq_thm_prop; 343); 344 345local 346 347fun add thm thy = 348 let 349 val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm; 350 in 351 thy 352 |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms) 353 end; 354 355fun get ctxt = 356 Computation_Preproc_Data.get (Proof_Context.theory_of ctxt) 357 |> map (Thm.transfer' ctxt) 358 359in 360 361fun preprocess_conv { ctxt } = 362 let 363 val rules = get ctxt; 364 in fn ctxt' => Raw_Simplifier.rewrite ctxt' false rules end; 365 366fun preprocess_term { ctxt } = 367 let 368 val rules = map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt); 369 in fn ctxt' => Pattern.rewrite_term (Proof_Context.theory_of ctxt') rules [] end; 370 371val _ = Theory.setup 372 (Attrib.setup @{binding code_computation_unfold} 373 (Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add thm) I))) 374 "preprocessing equations for computation"); 375 376end; 377 378 379(* mounting computations *) 380 381fun prechecked_computation T raw_computation ctxt = 382 check_typ ctxt T 383 #> reject_vars ctxt 384 #> raw_computation ctxt; 385 386fun prechecked_conv T raw_conv ctxt = 387 tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of) 388 #> raw_conv ctxt; 389 390fun checked_computation cTs raw_computation ctxt = 391 check_computation_input ctxt cTs 392 #> Exn.interruptible_capture raw_computation 393 #> partiality_as_none; 394 395fun mount_computation ctxt cTs T raw_computation lift_postproc = 396 let 397 val preprocess = preprocess_term { ctxt = ctxt }; 398 val computation = prechecked_computation T (Code_Preproc.static_value 399 { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] } 400 (K (checked_computation cTs raw_computation))); 401 in fn ctxt' => preprocess ctxt' #> computation ctxt' end; 402 403fun mount_computation_conv ctxt cTs T raw_computation conv = 404 let 405 val preprocess = preprocess_conv { ctxt = ctxt }; 406 val computation_conv = prechecked_conv T (Code_Preproc.static_conv 407 { ctxt = ctxt, consts = [] } 408 (K (fn ctxt' => fn t => 409 case checked_computation cTs raw_computation ctxt' t of 410 SOME x => conv ctxt' x 411 | NONE => Conv.all_conv))); 412 in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end; 413 414local 415 416fun holds ct = Thm.mk_binop @{cterm "Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop"} 417 ct @{cprop "PROP Code_Generator.holds"}; 418 419val (_, holds_oracle) = Context.>>> (Context.map_theory_result 420 (Thm.add_oracle (@{binding holds}, holds))); 421 422in 423 424fun mount_computation_check ctxt cTs raw_computation = 425 mount_computation_conv ctxt cTs @{typ prop} raw_computation 426 ((K o K) holds_oracle); 427 428end; 429 430 431(** variants of universal runtime code generation **) 432 433(*FIXME consolidate variants*) 434 435fun runtime_code'' ctxt module_name program tycos consts = 436 let 437 val thy = Proof_Context.theory_of ctxt; 438 val (ml_modules, target_names) = 439 Code_Target.produce_code_for ctxt 440 target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos); 441 val ml_code = space_implode "\n\n" (map snd ml_modules); 442 val (consts', tycos') = chop (length consts) target_names; 443 val consts_map = map2 (fn const => 444 fn NONE => 445 error ("Constant " ^ (quote o Code.string_of_const thy) const ^ 446 "\nhas a user-defined serialization") 447 | SOME const' => (const, const')) consts consts' 448 val tycos_map = map2 (fn tyco => 449 fn NONE => 450 error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ 451 "\nhas a user-defined serialization") 452 | SOME tyco' => (tyco, tyco')) tycos tycos'; 453 in (ml_code, (tycos_map, consts_map)) end; 454 455fun runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps = 456 let 457 val thy = Proof_Context.theory_of ctxt; 458 fun the_const (Const cT) = cT 459 | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t) 460 val raw_computation_cTs = case evals of 461 Abs (_, _, t) => (map the_const o snd o strip_comb) t 462 | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals); 463 val computation_cTs = fold_rev (fn cT => fn cTs => 464 (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs []; 465 val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c) 466 computation_cTs named_consts; 467 val program' = Code_Thingol.consts_program ctxt consts'; 468 (*FIXME insufficient interfaces require double invocation of code generator*) 469 val program'' = Code_Symbol.Graph.merge (K true) (program, program'); 470 val ((ml_modules, compiled_value), deresolve) = 471 Code_Target.compilation_text' ctxt target some_module_name program'' 472 (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals; 473 (*FIXME constrain signature*) 474 fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of 475 NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ 476 "\nhas a user-defined serialization") 477 | SOME c' => c'; 478 fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of 479 NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^ 480 "\nhas a user-defined serialization") 481 | SOME c' => c'; 482 val tyco_names = map deresolve_tyco named_tycos; 483 val const_names = map deresolve_const named_consts; 484 val generated_code = space_implode "\n\n" (map snd ml_modules); 485 val (of_term_code, of_term_names) = 486 print_computation_code ctxt compiled_value computation_cTs computation_Ts; 487 val compiled_computation = generated_code ^ "\n" ^ of_term_code; 488 in 489 compiled_computation 490 |> rpair { tyco_map = named_tycos ~~ tyco_names, 491 const_map = named_consts ~~ const_names, 492 of_term_map = computation_Ts ~~ of_term_names } 493 end; 494 495fun funs_of_maps { tyco_map, const_map, of_term_map } = 496 { name_for_tyco = the o AList.lookup (op =) tyco_map, 497 name_for_const = the o AList.lookup (op =) const_map, 498 of_term_for_typ = the o AList.lookup (op =) of_term_map }; 499 500fun runtime_code ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps = 501 runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps 502 ||> funs_of_maps; 503 504 505(** code and computation antiquotations **) 506 507local 508 509val mount_computationN = prefix_this "mount_computation"; 510val mount_computation_convN = prefix_this "mount_computation_conv"; 511val mount_computation_checkN = prefix_this "mount_computation_check"; 512 513structure Code_Antiq_Data = Proof_Data 514( 515 type T = { named_consts: string list, 516 computation_Ts: typ list, computation_cTs: (string * typ) list, 517 position_index: int, 518 generated_code: (string * { 519 name_for_tyco: string -> string, 520 name_for_const: string -> string, 521 of_term_for_typ: typ -> string 522 }) lazy 523 }; 524 val empty: T = { named_consts = [], 525 computation_Ts = [], computation_cTs = [], 526 position_index = 0, 527 generated_code = Lazy.lazy (fn () => raise Fail "empty") 528 }; 529 fun init _ = empty; 530); 531 532val current_position_index = #position_index o Code_Antiq_Data.get; 533 534fun register { named_consts, computation_Ts, computation_cTs } ctxt = 535 let 536 val data = Code_Antiq_Data.get ctxt; 537 val named_consts' = union (op =) named_consts (#named_consts data); 538 val computation_Ts' = union (op =) computation_Ts (#computation_Ts data); 539 val computation_cTs' = union (op =) computation_cTs (#computation_cTs data); 540 val position_index' = #position_index data + 1; 541 fun generated_code' () = 542 let 543 val evals = Abs ("eval", map snd computation_cTs' ---> 544 TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs')) 545 |> preprocess_term { ctxt = ctxt } ctxt 546 in Code_Thingol.dynamic_value ctxt 547 (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals 548 end; 549 in 550 ctxt 551 |> Code_Antiq_Data.put { 552 named_consts = named_consts', 553 computation_Ts = computation_Ts', 554 computation_cTs = computation_cTs', 555 position_index = position_index', 556 generated_code = Lazy.lazy generated_code' 557 } 558 end; 559 560fun register_const const = 561 register { named_consts = [const], 562 computation_Ts = [], 563 computation_cTs = [] }; 564 565fun register_computation cTs T = 566 register { named_consts = [], 567 computation_Ts = [T], 568 computation_cTs = cTs }; 569 570fun print body_code_for ctxt ctxt' = 571 let 572 val position_index = current_position_index ctxt; 573 val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt'; 574 val context_code = if position_index = 0 then code else ""; 575 val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt'); 576 in (context_code, body_code) end; 577 578fun print_code ctxt const = 579 print (fn { name_for_const, ... } => fn prfx => 580 Long_Name.append prfx (name_for_const const)) ctxt; 581 582fun print_computation kind ctxt T = 583 print (fn { of_term_for_typ, ... } => fn prfx => 584 enclose "(" ")" (space_implode " " [ 585 kind, 586 "(Context.proof_of (Context.the_generic_context ()))", 587 Long_Name.implode [prfx, generated_computationN, covered_constsN], 588 (ML_Syntax.atomic o ML_Syntax.print_typ) T, 589 Long_Name.append prfx (of_term_for_typ T) 590 ])) ctxt; 591 592fun print_computation_check ctxt = 593 print (fn { of_term_for_typ, ... } => fn prfx => 594 space_implode " " [ 595 mount_computation_checkN, 596 "(Context.proof_of (Context.the_generic_context ()))", 597 Long_Name.implode [prfx, generated_computationN, covered_constsN], 598 Long_Name.append prfx (of_term_for_typ @{typ prop}) 599 ]) ctxt; 600 601 602fun add_all_constrs ctxt (dT as Type (tyco, Ts)) = 603 case Code.get_type (Proof_Context.theory_of ctxt) tyco of 604 ((vs, constrs), false) => 605 let 606 val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts); 607 val cs = map (fn (c, (_, Ts')) => 608 (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts' 609 ---> dT)) constrs; 610 in 611 union (op =) cs 612 #> fold (add_all_constrs ctxt) Ts 613 end 614 | (_, true) => I; 615 616fun prep_spec ctxt (raw_ts, raw_dTs) = 617 let 618 val ts = map (Syntax.check_term ctxt) raw_ts; 619 val dTs = map (Syntax.check_typ ctxt) raw_dTs; 620 in 621 [] 622 |> (fold o fold_aterms) 623 (fn (t as Const (cT as (_, T))) => 624 if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t) 625 else insert (op =) cT | _ => I) ts 626 |> fold (fn dT => 627 if not (monomorphic dT) then error ("Polymorphic datatype: " ^ Syntax.string_of_typ ctxt dT) 628 else add_all_constrs ctxt dT) dTs 629 end; 630 631in 632 633fun ml_code_antiq raw_const ctxt = 634 let 635 val thy = Proof_Context.theory_of ctxt; 636 val const = Code.check_const thy raw_const; 637 in (print_code ctxt const, register_const const ctxt) end; 638 639fun gen_ml_computation_antiq kind (raw_T, raw_spec) ctxt = 640 let 641 val cTs = prep_spec ctxt raw_spec; 642 val T = Syntax.check_typ ctxt raw_T; 643 val _ = if not (monomorphic T) 644 then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T) 645 else (); 646 in (print_computation kind ctxt T, register_computation cTs T ctxt) end; 647 648val ml_computation_antiq = gen_ml_computation_antiq mount_computationN; 649 650val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN; 651 652fun ml_computation_check_antiq raw_spec ctxt = 653 let 654 val cTs = insert (op =) (dest_Const @{const holds}) (prep_spec ctxt raw_spec); 655 in (print_computation_check ctxt, register_computation cTs @{typ prop} ctxt) end; 656 657end; (*local*) 658 659 660(** reflection support **) 661 662fun check_datatype thy tyco some_consts = 663 let 664 val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco; 665 val constrs = case some_consts 666 of SOME [] => [] 667 | SOME consts => 668 let 669 val missing_constrs = subtract (op =) consts declared_constrs; 670 val _ = if null missing_constrs then [] 671 else error ("Missing constructor(s) " ^ commas_quote missing_constrs 672 ^ " for datatype " ^ quote tyco); 673 val false_constrs = subtract (op =) declared_constrs consts; 674 val _ = if null false_constrs then [] 675 else error ("Non-constructor(s) " ^ commas_quote false_constrs 676 ^ " for datatype " ^ quote tyco) 677 in consts end 678 | NONE => declared_constrs; 679 in (tyco, constrs) end; 680 681fun add_eval_tyco (tyco, tyco') thy = 682 let 683 val k = Sign.arity_number thy tyco; 684 fun pr pr' _ [] = tyco' 685 | pr pr' _ [ty] = 686 Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] 687 | pr pr' _ tys = 688 Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] 689 in 690 thy 691 |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))])) 692 end; 693 694fun add_eval_constr (const, const') thy = 695 let 696 val k = Code.args_number thy const; 697 fun pr pr' fxy ts = Code_Printer.brackify fxy 698 (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); 699 in 700 thy 701 |> Code_Target.set_printings (Constant (const, 702 [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))])) 703 end; 704 705fun add_eval_const (const, const') = Code_Target.set_printings (Constant 706 (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))])); 707 708fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy = 709 thy 710 |> Code_Target.add_reserved target module_name 711 |> Context.theory_map (compile_ML true code) 712 |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map 713 |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map 714 |> fold (add_eval_const o apsnd Code_Printer.str) const_map 715 | process_reflection (code, _) _ (SOME file_name) thy = 716 let 717 val preamble = 718 "(* Generated from " ^ 719 Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ 720 "; DO NOT EDIT! *)"; 721 val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); 722 in 723 thy 724 end; 725 726fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = 727 let 728 val ctxt = Proof_Context.init_global thy; 729 val datatypes = map (fn (raw_tyco, raw_cos) => 730 (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes; 731 val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes 732 |> apsnd flat; 733 val functions = map (prep_const thy) raw_functions; 734 val consts = constrs @ functions; 735 val program = Code_Thingol.consts_program ctxt consts; 736 val result = runtime_code'' ctxt module_name program tycos consts 737 |> (apsnd o apsnd) (chop (length constrs)); 738 in 739 thy 740 |> process_reflection result module_name some_file 741 end; 742 743val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); 744val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; 745 746 747(** Isar setup **) 748 749local 750 751val parse_consts_spec = 752 Scan.optional (Scan.lift (Args.$$$ "terms" -- Args.colon) |-- Scan.repeat1 Args.term) [] 753 -- Scan.optional (Scan.lift (Args.$$$ "datatypes" -- Args.colon) |-- Scan.repeat1 Args.typ) []; 754 755in 756 757val _ = Theory.setup 758 (ML_Antiquotation.declaration @{binding code} 759 Args.term (K ml_code_antiq) 760 #> ML_Antiquotation.declaration @{binding computation} 761 (Args.typ -- parse_consts_spec) (K ml_computation_antiq) 762 #> ML_Antiquotation.declaration @{binding computation_conv} 763 (Args.typ -- parse_consts_spec) (K ml_computation_conv_antiq) 764 #> ML_Antiquotation.declaration @{binding computation_check} 765 parse_consts_spec (K ml_computation_check_antiq)); 766 767end; 768 769local 770 771val parse_datatype = 772 Parse.name -- Scan.optional (@{keyword "="} |-- 773 (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ())) 774 || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []); 775 776in 777 778val _ = 779 Outer_Syntax.command @{command_keyword code_reflect} 780 "enrich runtime environment with generated code" 781 (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype 782 ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) [] 783 -- Scan.optional (@{keyword "functions"} |-- Parse.!!! (Scan.repeat1 Parse.name)) [] 784 -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name) 785 >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory 786 (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); 787 788end; (*local*) 789 790 791(** using external SML files as substitute for proper definitions -- only for polyml! **) 792 793local 794 795structure Loaded_Values = Theory_Data 796( 797 type T = string list 798 val empty = [] 799 val extend = I 800 fun merge data : T = Library.merge (op =) data 801); 802 803fun notify_val (string, value) = 804 let 805 val _ = #enterVal ML_Env.name_space (string, value); 806 val _ = Theory.setup (Loaded_Values.map (insert (op =) string)); 807 in () end; 808 809fun abort _ = error "Only value bindings allowed."; 810 811val notifying_context : ML_Compiler0.context = 812 {name_space = 813 {lookupVal = #lookupVal ML_Env.name_space, 814 lookupType = #lookupType ML_Env.name_space, 815 lookupFix = #lookupFix ML_Env.name_space, 816 lookupStruct = #lookupStruct ML_Env.name_space, 817 lookupSig = #lookupSig ML_Env.name_space, 818 lookupFunct = #lookupFunct ML_Env.name_space, 819 enterVal = notify_val, 820 enterType = abort, 821 enterFix = abort, 822 enterStruct = abort, 823 enterSig = abort, 824 enterFunct = abort, 825 allVal = #allVal ML_Env.name_space, 826 allType = #allType ML_Env.name_space, 827 allFix = #allFix ML_Env.name_space, 828 allStruct = #allStruct ML_Env.name_space, 829 allSig = #allSig ML_Env.name_space, 830 allFunct = #allFunct ML_Env.name_space}, 831 print_depth = NONE, 832 here = #here ML_Env.context, 833 print = #print ML_Env.context, 834 error = #error ML_Env.context}; 835 836in 837 838fun use_file filepath thy = 839 let 840 val thy' = Loaded_Values.put [] thy; 841 val _ = Context.put_generic_context ((SOME o Context.Theory) thy'); 842 val _ = 843 ML_Compiler0.ML notifying_context 844 {line = 0, file = Path.implode filepath, verbose = false, debug = false} 845 (File.read filepath); 846 val thy'' = Context.the_global_context (); 847 val names = Loaded_Values.get thy''; 848 in (names, thy'') end; 849 850end; 851 852fun add_definiendum (ml_name, (b, T)) thy = 853 thy 854 |> Code_Target.add_reserved target ml_name 855 |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] [] 856 |-> (fn ([Const (const, _)], _) => 857 Code_Target.set_printings (Constant (const, 858 [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) 859 #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN [])); 860 861fun process_file filepath (definienda, thy) = 862 let 863 val (ml_names, thy') = use_file filepath thy; 864 val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names; 865 val _ = if null superfluous then () 866 else error ("Value binding(s) " ^ commas_quote superfluous 867 ^ " found in external file " ^ Path.print filepath 868 ^ " not present among the given contants binding(s)."); 869 val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names; 870 val thy'' = fold add_definiendum these_definienda thy'; 871 val definienda' = fold (AList.delete (op =)) ml_names definienda; 872 in (definienda', thy'') end; 873 874fun polyml_as_definition bTs filepaths thy = 875 let 876 val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs; 877 val (remaining, thy') = fold process_file filepaths (definienda, thy); 878 val _ = if null remaining then () 879 else error ("Constant binding(s) " ^ commas_quote (map fst remaining) 880 ^ " not present in external file(s)."); 881 in thy' end; 882 883end; (*struct*) 884