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