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