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