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