src/Pure/ML/ml_thms.ML
author wenzelm
Sat, 11 Aug 2012 22:17:46 +0200
changeset 48776 37cd53e69840
parent 47815 43f677b3ae91
child 48782 e955964d89cb
permissions -rw-r--r--
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
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
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    10
  val the_thms: Proof.context -> int -> thm list
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    11
  val the_thm: Proof.context -> int -> thm
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    12
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    13
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    14
structure ML_Thms: ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    15
struct
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    16
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    17
(* auxiliary data *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    18
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    19
structure Data = Proof_Data
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    20
(
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    21
  type T = Args.src list Inttab.table * thm list Inttab.table;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    22
  fun init _ = (Inttab.empty, Inttab.empty);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    23
);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    24
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    25
val put_attributes = Data.map o apfst o Inttab.update;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    26
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    27
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    28
val put_thms = Data.map o apsnd o Inttab.update;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    29
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    30
fun the_thms ctxt name = the (Inttab.lookup (snd (Data.get ctxt)) name);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    31
fun the_thm ctxt name = the_single (the_thms ctxt name);
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
(* attribute source *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    35
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    36
val _ =
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    37
  Context.>> (Context.map_theory
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    38
    (ML_Context.add_antiq (Binding.name "attributes")
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    39
      (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background =>
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    40
        let
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    41
          val thy = Proof_Context.theory_of background;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    42
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    43
          val i = serial ();
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    44
          val srcs = map (Attrib.intern_src thy) raw_srcs;
47815
43f677b3ae91 clarified signature;
wenzelm
parents: 45592
diff changeset
    45
          val _ = map (Attrib.attribute background) srcs;
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    46
          val (a, background') = background
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    47
            |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    48
          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
    49
            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    50
              string_of_int i ^ ";\n", "Isabelle." ^ a);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    51
        in (K ml, background') end))));
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    52
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    53
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    54
(* fact references *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    55
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    56
fun thm_bind kind a i =
48776
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 47815
diff changeset
    57
  "val " ^ a ^ " = ML_Thms.the_" ^ kind ^ " ML_context " ^ string_of_int i ^ ";\n";
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    58
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    59
fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
35019
1ec0a3ff229e simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents: 33700
diff changeset
    60
  (fn _ => scan >> (fn ths => fn background =>
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    61
    let
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    62
      val i = serial ();
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    63
      val (a, background') = background
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    64
        |> ML_Antiquote.variant kind ||> put_thms (i, ths);
41486
82c1e348bc18 reverted 08240feb69c7 -- breaks positions of reports;
wenzelm
parents: 41376
diff changeset
    65
      val ml = (thm_bind kind a i, "Isabelle." ^ a);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    66
    in (K ml, background') end));
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    67
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    68
val _ =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    69
  Context.>> (Context.map_theory
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    70
   (thm_antiq "thm" (Attrib.thm >> single) #>
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    71
    thm_antiq "thms" Attrib.thms));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    72
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    73
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    74
(* ad-hoc goals *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    75
30266
970bf4f594c9 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents: 29606
diff changeset
    76
val and_ = Args.$$$ "and";
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27521
diff changeset
    77
val by = Args.$$$ "by";
45198
f579dab96734 proper source positions for @{lemma};
wenzelm
parents: 43560
diff changeset
    78
val goal = Scan.unless (by || and_) Args.name_source;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    79
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    80
val _ =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    81
  Context.>> (Context.map_theory
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    82
   (ML_Context.add_antiq (Binding.name "lemma")
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    83
    (fn _ => Args.context -- Args.mode "open" --
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    84
        Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    85
          (by |-- Method.parse -- Scan.option Method.parse)) >>
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    86
      (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    87
        let
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    88
          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    89
          val i = serial ();
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    90
          val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    91
          fun after_qed res goal_ctxt =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    92
            put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    93
          val ctxt' = ctxt
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    94
            |> Proof.theorem NONE after_qed propss
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    95
            |> Proof.global_terminal_proof methods;
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    96
          val (a, background') = background
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    97
            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    98
          val ml =
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
    99
            (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42360
diff changeset
   100
        in (K ml, background') end))));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   101
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   102
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   103