src/Pure/ML/ml_thms.ML
author wenzelm
Fri, 23 Aug 2013 19:53:27 +0200
changeset 53169 e2d31807cbf6
parent 53168 d998de7f0efc
child 53171 a5e54d4d9081
permissions -rw-r--r--
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
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
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
     9
  val the_attributes: Proof.context -> int -> Args.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
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    11
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    12
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    13
structure ML_Thms: ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    14
struct
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    15
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    16
(* auxiliary data *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    17
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
    18
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
    19
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    20
structure Data = Proof_Data
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    21
(
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
    22
  type T = Args.src list Inttab.table * thms list;
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
    23
  fun init _ = (Inttab.empty, []);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    24
);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    25
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    26
val put_attributes = Data.map o apfst o Inttab.update;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    27
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    28
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
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
    30
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
    31
val cons_thms = Data.map o apsnd o cons;
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    32
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    33
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    34
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    35
(* attribute source *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    36
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    37
val _ =
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    38
  Context.>> (Context.map_theory
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    39
    (ML_Context.add_antiq (Binding.name "attributes")
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    40
      (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    41
        let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    42
          val ctxt = Context.the_proof context;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    43
          val thy = Proof_Context.theory_of ctxt;
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    44
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    45
          val i = serial ();
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    46
          val srcs = map (Attrib.intern_src thy) raw_srcs;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    47
          val _ = map (Attrib.attribute ctxt) srcs;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    48
          val (a, ctxt') = ctxt
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    49
            |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    50
          val ml =
48776
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 47815
diff changeset
    51
            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    52
              string_of_int i ^ ";\n", "Isabelle." ^ a);
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    53
        in (Context.Proof ctxt', K ml) end)))));
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    54
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    55
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    56
(* fact references *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    57
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    58
fun thm_binding kind is_single context thms =
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
    59
  let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    60
    val ctxt = Context.the_proof context;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    61
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    62
    val initial = null (get_thmss ctxt);
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    63
    val (name, ctxt') = ML_Antiquote.variant kind ctxt;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    64
    val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    65
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_body = "Isabelle." ^ name;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    67
    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
    68
      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
    69
        let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    70
          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
    71
          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
    72
        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
    73
      else ("", ml_body);
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    74
  in (Context.Proof ctxt'', decl) end;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    75
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    76
val _ =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    77
  Context.>> (Context.map_theory
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    78
    (ML_Context.add_antiq (Binding.name "thm")
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    79
      (Scan.depend (fn context =>
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    80
        Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    81
     ML_Context.add_antiq (Binding.name "thms")
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    82
      (Scan.depend (fn context =>
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    83
        Scan.pass context Attrib.thms >> thm_binding "thms" false context))));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    84
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    85
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    86
(* ad-hoc goals *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    87
30266
970bf4f594c9 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents: 29606
diff changeset
    88
val and_ = Args.$$$ "and";
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27521
diff changeset
    89
val by = Args.$$$ "by";
45198
f579dab96734 proper source positions for @{lemma};
wenzelm
parents: 43560
diff changeset
    90
val goal = Scan.unless (by || and_) Args.name_source;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    91
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    92
val _ =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    93
  Context.>> (Context.map_theory
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    94
   (ML_Context.add_antiq (Binding.name "lemma")
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    95
    (Scan.depend (fn context =>
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    96
      Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    97
      (by |-- Method.parse -- Scan.option Method.parse) >>
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    98
        (fn ((is_open, raw_propss), methods) =>
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    99
          let
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   100
            val ctxt = Context.proof_of context;
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
   101
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   102
            val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   103
            val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   104
            fun after_qed res goal_ctxt =
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   105
              Proof_Context.put_thms false (Auto_Bind.thisN,
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   106
                SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   107
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   108
            val ctxt' = ctxt
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   109
              |> Proof.theorem NONE after_qed propss
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   110
              |> Proof.global_terminal_proof methods;
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   111
            val thms =
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   112
              Proof_Context.get_fact ctxt'
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   113
                (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   114
          in thm_binding "lemma" (length (flat propss) = 1) context thms end)))));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   115
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   116
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   117