src/Pure/ML/ml_thms.ML
author wenzelm
Wed, 10 Dec 2014 19:24:54 +0100
changeset 59127 723b11f8ffbf
parent 59112 e670969f34df
child 61814 1ca1142e1711
permissions -rw-r--r--
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_thms.ML
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     3
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
     4
Attribute source and theorem values within ML.
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     5
*)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     6
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     7
signature ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     8
sig
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 56304
diff changeset
     9
  val the_attributes: Proof.context -> int -> Token.src list
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    10
  val the_thmss: Proof.context -> thm list list
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    11
  val get_stored_thms: unit -> thm list
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    12
  val get_stored_thm: unit -> thm
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    13
  val store_thms: string * thm list -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    14
  val store_thm: string * thm -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    15
  val bind_thm: string * thm -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    16
  val bind_thms: string * thm list -> unit
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    17
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    18
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    19
structure ML_Thms: ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    20
struct
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    21
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    22
(* auxiliary data *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    23
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    24
type thms = (string * bool) * thm list;  (*name, single, value*)
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    25
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    26
structure Data = Proof_Data
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    27
(
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 56304
diff changeset
    28
  type T = Token.src list Inttab.table * thms list;
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    29
  fun init _ = (Inttab.empty, []);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    30
);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    31
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    32
val put_attributes = Data.map o apfst o Inttab.update;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    33
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    34
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    35
val get_thmss = snd o Data.get;
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    36
val the_thmss = map snd o get_thmss;
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    37
val cons_thms = Data.map o apsnd o cons;
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    38
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    39
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    40
(* attribute source *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    41
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    42
val _ = Theory.setup
58028
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
    43
  (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs)
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    44
    (fn _ => fn raw_srcs => fn ctxt =>
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    45
      let val i = serial () in
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    46
        ctxt
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    47
        |> put_attributes (i, Attrib.check_attribs ctxt raw_srcs)
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    48
        |> ML_Context.value_decl "attributes"
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    49
            ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    50
      end));
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    51
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    52
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    53
(* fact references *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    54
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    55
fun thm_binding kind is_single thms ctxt =
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    56
  let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    57
    val initial = null (get_thmss ctxt);
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 58866
diff changeset
    58
    val (name, ctxt') = ML_Context.variant kind ctxt;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    59
    val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    60
59127
723b11f8ffbf more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents: 59112
diff changeset
    61
    val ml_body = ML_Context.struct_name ctxt ^ "." ^ name;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    62
    fun decl final_ctxt =
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    63
      if initial then
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    64
        let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    65
          val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    66
          val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    67
        in (ml_env, ml_body) end
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    68
      else ("", ml_body);
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    69
  in (decl, ctxt'') end;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    70
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    71
val _ = Theory.setup
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56199
diff changeset
    72
  (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
ceb8a93460b7 clarified modules;
wenzelm
parents: 56199
diff changeset
    73
   ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    74
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    75
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    76
(* ad-hoc goals *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    77
30266
970bf4f594c9 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents: 29606
diff changeset
    78
val and_ = Args.$$$ "and";
58866
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    79
val by = Parse.reserved "by";
55111
5792f5106c40 tuned signature;
wenzelm
parents: 54883
diff changeset
    80
val goal = Scan.unless (by || and_) Args.name_inner_syntax;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    81
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    82
val _ = Theory.setup
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56199
diff changeset
    83
  (ML_Antiquotation.declaration @{binding lemma}
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    84
    (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
58866
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    85
      (Parse.position by -- Method.parse -- Scan.option Method.parse)))
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    86
    (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    87
      let
58866
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    88
        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
f81e11391562 clarified syntax -- avoid overlap with command category;
wenzelm
parents: 58045
diff changeset
    89
        val _ = Context_Position.reports ctxt reports;
55515
0e161deca64d more markup;
wenzelm
parents: 55111
diff changeset
    90
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    91
        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    92
        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    93
        fun after_qed res goal_ctxt =
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    94
          Proof_Context.put_thms false (Auto_Bind.thisN,
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    95
            SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    96
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    97
        val ctxt' = ctxt
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    98
          |> Proof.theorem NONE after_qed propss
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    99
          |> Proof.global_terminal_proof (m1, m2);
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   100
        val thms =
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   101
          Proof_Context.get_fact ctxt'
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   102
            (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   103
      in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   104
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   105
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   106
(* old-style theorem bindings *)
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   107
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   108
structure Stored_Thms = Theory_Data
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   109
(
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   110
  type T = thm list;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   111
  val empty = [];
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   112
  fun extend _ = [];
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   113
  fun merge _ = [];
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   114
);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   115
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   116
fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   117
val get_stored_thm = hd o get_stored_thms;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   118
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   119
fun ml_store get (name, ths) =
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   120
  let
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   121
    val ths' = Context.>>> (Context.map_theory_result
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   122
      (Global_Theory.store_thms (Binding.name name, ths)));
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   123
    val _ = Theory.setup (Stored_Thms.put ths');
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   124
    val _ =
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   125
      if name = "" then ()
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   126
      else if not (ML_Syntax.is_identifier name) then
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   127
        error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   128
      else
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56275
diff changeset
   129
        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   130
          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   131
    val _ = Theory.setup (Stored_Thms.put []);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   132
  in () end;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   133
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   134
val store_thms = ml_store "ML_Thms.get_stored_thms";
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   135
fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   136
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   137
fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   138
fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   139
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   140
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   141