1(* Title: Pure/ML/ml_thms.ML 2 Author: Makarius 3 4Attribute source and theorem values within ML. 5*) 6 7signature ML_THMS = 8sig 9 val the_attributes: Proof.context -> int -> Token.src list 10 val the_thmss: Proof.context -> thm list list 11 val get_stored_thms: unit -> thm list 12 val get_stored_thm: unit -> thm 13 val store_thms: string * thm list -> unit 14 val store_thm: string * thm -> unit 15 val bind_thm: string * thm -> unit 16 val bind_thms: string * thm list -> unit 17end; 18 19structure ML_Thms: ML_THMS = 20struct 21 22(* auxiliary data *) 23 24type thms = (string * bool) * thm list; (*name, single, value*) 25 26structure Data = Proof_Data 27( 28 type T = Token.src list Inttab.table * thms list; 29 fun init _ = (Inttab.empty, []); 30); 31 32val put_attributes = Data.map o apfst o Inttab.update; 33fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); 34 35val get_thmss = snd o Data.get; 36val the_thmss = map snd o get_thmss; 37val cons_thms = Data.map o apsnd o cons; 38 39 40(* attribute source *) 41 42val _ = Theory.setup 43 (ML_Antiquotation.declaration \<^binding>\<open>attributes\<close> Attrib.attribs 44 (fn _ => fn srcs => fn ctxt => 45 let val i = serial () in 46 ctxt 47 |> put_attributes (i, srcs) 48 |> ML_Context.value_decl "attributes" 49 ("ML_Thms.the_attributes ML_context " ^ string_of_int i) 50 end)); 51 52 53(* fact references *) 54 55fun thm_binding kind is_single thms ctxt = 56 let 57 val initial = null (get_thmss ctxt); 58 val (name, ctxt') = ML_Context.variant kind ctxt; 59 val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; 60 61 val ml_body = ML_Context.struct_name ctxt ^ "." ^ name; 62 fun decl final_ctxt = 63 if initial then 64 let 65 val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); 66 val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n"; 67 in (ml_env, ml_body) end 68 else ("", ml_body); 69 in (decl, ctxt'') end; 70 71val _ = Theory.setup 72 (ML_Antiquotation.declaration \<^binding>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #> 73 ML_Antiquotation.declaration \<^binding>\<open>thms\<close> Attrib.thms (K (thm_binding "thms" false))); 74 75 76(* ad-hoc goals *) 77 78val and_ = Args.$$$ "and"; 79val by = Parse.reserved "by"; 80val goal = Scan.unless (by || and_) Args.embedded_inner_syntax; 81 82val _ = Theory.setup 83 (ML_Antiquotation.declaration \<^binding>\<open>lemma\<close> 84 (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- 85 (Parse.position by -- Method.parse -- Scan.option Method.parse))) 86 (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt => 87 let 88 val reports = 89 (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: 90 maps Method.reports_of (m1 :: the_list m2); 91 val _ = Context_Position.reports ctxt reports; 92 93 val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; 94 val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation; 95 fun after_qed res goal_ctxt = 96 Proof_Context.put_thms false (Auto_Bind.thisN, 97 SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; 98 99 val ctxt' = ctxt 100 |> Proof.theorem NONE after_qed propss 101 |> Proof.global_terminal_proof (m1, m2); 102 val thms = 103 Proof_Context.get_fact ctxt' 104 (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); 105 in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end)); 106 107 108(* old-style theorem bindings *) 109 110structure Stored_Thms = Theory_Data 111( 112 type T = thm list; 113 val empty = []; 114 fun extend _ = []; 115 fun merge _ = []; 116); 117 118fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ()); 119val get_stored_thm = hd o get_stored_thms; 120 121fun ml_store get (name, ths) = 122 let 123 val (_, ths') = 124 Context.>>> (Context.map_theory_result 125 (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); 126 val _ = Theory.setup (Stored_Thms.put ths'); 127 val _ = 128 if name = "" then () 129 else if not (ML_Syntax.is_identifier name) then 130 error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") 131 else 132 ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none 133 (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); 134 val _ = Theory.setup (Stored_Thms.put []); 135 in () end; 136 137val store_thms = ml_store "ML_Thms.get_stored_thms"; 138fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]); 139 140fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm); 141fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms); 142 143end; 144