src/Pure/Thy/thm_database.ML
author wenzelm
Mon Oct 22 18:04:26 2001 +0200 (2001-10-22)
changeset 11895 73b2c277974f
parent 11769 1fcf1eb51608
child 13279 8a722689a1c9
permissions -rw-r--r--
moved goal related stuff to goals.ML;
clasohm@1132
     1
(*  Title:      Pure/Thy/thm_database.ML
clasohm@1132
     2
    ID:         $Id$
wenzelm@11895
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@11895
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
clasohm@1132
     5
wenzelm@11895
     6
Interface to thm database (see also Pure/pure_thy.ML).
wenzelm@4023
     7
*)
clasohm@1262
     8
wenzelm@6204
     9
signature BASIC_THM_DATABASE =
wenzelm@4023
    10
sig
wenzelm@4023
    11
  val store_thm: string * thm -> thm
wenzelm@7410
    12
  val store_thms: string * thm list -> thm list
wenzelm@4023
    13
end;
clasohm@1132
    14
wenzelm@6204
    15
signature THM_DATABASE =
wenzelm@6204
    16
sig
wenzelm@6204
    17
  include BASIC_THM_DATABASE
wenzelm@7410
    18
  val qed_thms: thm list ref
wenzelm@6204
    19
  val ml_store_thm: string * thm -> unit
wenzelm@7410
    20
  val ml_store_thms: string * thm list -> unit
wenzelm@6204
    21
  val is_ml_identifier: string -> bool
berghofe@11529
    22
  val ml_reserved: string list
wenzelm@11895
    23
  val thms_containing: theory -> string list -> (string * thm) list
wenzelm@11017
    24
  val print_thms_containing: theory -> term list -> unit
wenzelm@6204
    25
end;
wenzelm@6204
    26
wenzelm@3627
    27
structure ThmDatabase: THM_DATABASE =
nipkow@1221
    28
struct
clasohm@1132
    29
wenzelm@4023
    30
(** store theorems **)
clasohm@1132
    31
wenzelm@4023
    32
(* store in theory and generate HTML *)
clasohm@1136
    33
wenzelm@4023
    34
fun store_thm (name, thm) =
wenzelm@7410
    35
  let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
wenzelm@6327
    36
  in Present.theorem name thm'; thm' end;
clasohm@1132
    37
wenzelm@7410
    38
fun store_thms (name, thms) =
wenzelm@7410
    39
  let val thms' = PureThy.smart_store_thms (name, thms)
wenzelm@7410
    40
  in Present.theorems name thms'; thms' end;
wenzelm@7410
    41
clasohm@1262
    42
wenzelm@4023
    43
(* store on ML toplevel *)
wenzelm@4023
    44
wenzelm@7410
    45
val qed_thms: thm list ref = ref [];
clasohm@1262
    46
wenzelm@4023
    47
val ml_reserved =
wenzelm@4023
    48
 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
wenzelm@4023
    49
  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
wenzelm@4023
    50
  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
wenzelm@4023
    51
  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
wenzelm@4023
    52
  "eqtype", "functor", "include", "sharing", "sig", "signature",
wenzelm@4023
    53
  "struct", "structure", "where"];
clasohm@1262
    54
wenzelm@4023
    55
fun is_ml_identifier name =
wenzelm@4023
    56
  Syntax.is_identifier name andalso not (name mem ml_reserved);
clasohm@1262
    57
wenzelm@7410
    58
fun warn_ml name =
wenzelm@7410
    59
  if is_ml_identifier name then false
wenzelm@7573
    60
  else if name = "" then true
wenzelm@7410
    61
  else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
wenzelm@7410
    62
wenzelm@10914
    63
val use_text_verbose = use_text Context.ml_output true;
wenzelm@7854
    64
wenzelm@4023
    65
fun ml_store_thm (name, thm) =
wenzelm@4023
    66
  let val thm' = store_thm (name, thm) in
wenzelm@7410
    67
    if warn_ml name then ()
wenzelm@7854
    68
    else (qed_thms := [thm']; use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
wenzelm@7410
    69
  end;
wenzelm@7410
    70
wenzelm@7410
    71
fun ml_store_thms (name, thms) =
wenzelm@7410
    72
  let val thms' = store_thms (name, thms) in
wenzelm@7410
    73
    if warn_ml name then ()
wenzelm@7854
    74
    else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
clasohm@1262
    75
  end;
clasohm@1262
    76
wenzelm@4023
    77
wenzelm@4023
    78
wenzelm@4037
    79
(** retrieve theorems **)
clasohm@1132
    80
wenzelm@11895
    81
fun thms_containing thy consts = PureThy.thms_containing thy consts
wenzelm@11017
    82
  handle THEORY (msg, _) => error msg | THM (msg, _, _) => error msg;
wenzelm@11017
    83
wenzelm@11017
    84
fun print_thms_containing thy ts =
wenzelm@11017
    85
  let
wenzelm@11017
    86
    val prt_const =
wenzelm@11017
    87
      Pretty.quote o Pretty.str o Sign.cond_extern (Theory.sign_of thy) Sign.constK;
wenzelm@11017
    88
    fun prt_thm (a, th) = Pretty.block [Pretty.str (a ^ ":"),
wenzelm@11017
    89
      Pretty.brk 1, Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
wenzelm@7609
    90
wenzelm@11017
    91
    val cs = foldr Term.add_term_consts (ts, []);
wenzelm@11017
    92
    val header =
wenzelm@11017
    93
      if Library.null cs then []
wenzelm@11017
    94
      else [Pretty.block (Pretty.breaks (Pretty.str "theorems containing constants:" ::
wenzelm@11017
    95
          map prt_const cs)), Pretty.str ""];
wenzelm@11017
    96
  in
wenzelm@11017
    97
    if Library.null cs andalso not (Library.null ts) then
wenzelm@11017
    98
      warning "thms_containing: no constants in specification"
wenzelm@11895
    99
    else (header @ map prt_thm (thms_containing thy cs)) |> Pretty.chunks |> Pretty.writeln
wenzelm@11017
   100
  end;
clasohm@1132
   101
berghofe@3601
   102
clasohm@1132
   103
end;
wenzelm@6204
   104
wenzelm@6204
   105
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
wenzelm@6204
   106
open BasicThmDatabase;