src/Pure/Thy/thm_database.ML
author wenzelm
Mon Mar 24 23:34:30 2008 +0100 (2008-03-24)
changeset 26386 9c806de22a6a
parent 25699 891fe6b71d3b
permissions -rw-r--r--
ML runtime compilation: pass position, tuned signature;
removed obsolete (use_)legacy_bindings;
clasohm@1132
     1
(*  Title:      Pure/Thy/thm_database.ML
clasohm@1132
     2
    ID:         $Id$
wenzelm@11895
     3
    Author:     Markus Wenzel, TU Muenchen
clasohm@1132
     4
wenzelm@17170
     5
ML toplevel interface to the theorem database.
wenzelm@4023
     6
*)
clasohm@1262
     7
wenzelm@6204
     8
signature BASIC_THM_DATABASE =
wenzelm@4023
     9
sig
wenzelm@4023
    10
  val store_thm: string * thm -> thm
wenzelm@7410
    11
  val store_thms: string * thm list -> thm list
wenzelm@4023
    12
end;
clasohm@1132
    13
wenzelm@6204
    14
signature THM_DATABASE =
wenzelm@6204
    15
sig
wenzelm@6204
    16
  include BASIC_THM_DATABASE
wenzelm@7410
    17
  val qed_thms: thm list ref
wenzelm@6204
    18
  val ml_store_thm: string * thm -> unit
wenzelm@7410
    19
  val ml_store_thms: string * thm list -> unit
wenzelm@6204
    20
end;
wenzelm@6204
    21
wenzelm@3627
    22
structure ThmDatabase: THM_DATABASE =
nipkow@1221
    23
struct
clasohm@1132
    24
wenzelm@4023
    25
(** store theorems **)
clasohm@1132
    26
wenzelm@13279
    27
(* store in theory and perform presentation *)
clasohm@1136
    28
wenzelm@4023
    29
fun store_thm (name, thm) =
wenzelm@7410
    30
  let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
wenzelm@6327
    31
  in Present.theorem name thm'; thm' end;
clasohm@1132
    32
wenzelm@7410
    33
fun store_thms (name, thms) =
wenzelm@7410
    34
  let val thms' = PureThy.smart_store_thms (name, thms)
wenzelm@7410
    35
  in Present.theorems name thms'; thms' end;
wenzelm@7410
    36
clasohm@1262
    37
wenzelm@4023
    38
(* store on ML toplevel *)
wenzelm@4023
    39
wenzelm@7410
    40
val qed_thms: thm list ref = ref [];
clasohm@1262
    41
wenzelm@7410
    42
fun warn_ml name =
wenzelm@21482
    43
  if ML_Syntax.is_identifier name then false
wenzelm@7573
    44
  else if name = "" then true
wenzelm@7410
    45
  else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
wenzelm@7410
    46
wenzelm@26386
    47
val use_text_verbose = use_text (0, "") Output.ml_output true;
wenzelm@7854
    48
wenzelm@4023
    49
fun ml_store_thm (name, thm) =
wenzelm@4023
    50
  let val thm' = store_thm (name, thm) in
wenzelm@7410
    51
    if warn_ml name then ()
wenzelm@25699
    52
    else NAMED_CRITICAL "ML" (fn () => (qed_thms := [thm'];
wenzelm@23921
    53
      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
wenzelm@7410
    54
  end;
wenzelm@7410
    55
wenzelm@7410
    56
fun ml_store_thms (name, thms) =
wenzelm@7410
    57
  let val thms' = store_thms (name, thms) in
wenzelm@7410
    58
    if warn_ml name then ()
wenzelm@25699
    59
    else NAMED_CRITICAL "ML" (fn () => (qed_thms := thms';
wenzelm@23921
    60
      use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
clasohm@1262
    61
  end;
clasohm@1262
    62
clasohm@1132
    63
end;
wenzelm@6204
    64
wenzelm@6204
    65
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
wenzelm@6204
    66
open BasicThmDatabase;