src/Pure/Thy/thm_database.ML
author wenzelm
Thu Apr 27 15:06:35 2006 +0200 (2006-04-27)
changeset 19482 9f11af8f7ef9
parent 19012 2577ac76cdc6
child 20676 21e096f30c5d
permissions -rw-r--r--
tuned basic list operators (flat, maps, map_filter);
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@17170
    12
  val legacy_bindings: theory -> string
wenzelm@17170
    13
  val use_legacy_bindings: theory -> unit
wenzelm@4023
    14
end;
clasohm@1132
    15
wenzelm@6204
    16
signature THM_DATABASE =
wenzelm@6204
    17
sig
wenzelm@6204
    18
  include BASIC_THM_DATABASE
wenzelm@7410
    19
  val qed_thms: thm list ref
wenzelm@6204
    20
  val ml_store_thm: string * thm -> unit
wenzelm@7410
    21
  val ml_store_thms: string * thm list -> unit
wenzelm@14680
    22
  val ml_reserved: string list
wenzelm@6204
    23
  val is_ml_identifier: string -> bool
wenzelm@6204
    24
end;
wenzelm@6204
    25
wenzelm@3627
    26
structure ThmDatabase: THM_DATABASE =
nipkow@1221
    27
struct
clasohm@1132
    28
wenzelm@4023
    29
(** store theorems **)
clasohm@1132
    30
wenzelm@13279
    31
(* store in theory and perform presentation *)
clasohm@1136
    32
wenzelm@4023
    33
fun store_thm (name, thm) =
wenzelm@7410
    34
  let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
wenzelm@6327
    35
  in Present.theorem name thm'; thm' end;
clasohm@1132
    36
wenzelm@7410
    37
fun store_thms (name, thms) =
wenzelm@7410
    38
  let val thms' = PureThy.smart_store_thms (name, thms)
wenzelm@7410
    39
  in Present.theorems name thms'; thms' end;
wenzelm@7410
    40
clasohm@1262
    41
wenzelm@4023
    42
(* store on ML toplevel *)
wenzelm@4023
    43
wenzelm@7410
    44
val qed_thms: thm list ref = ref [];
clasohm@1262
    45
wenzelm@4023
    46
val ml_reserved =
wenzelm@4023
    47
 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
wenzelm@4023
    48
  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
wenzelm@4023
    49
  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
wenzelm@4023
    50
  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
wenzelm@4023
    51
  "eqtype", "functor", "include", "sharing", "sig", "signature",
wenzelm@4023
    52
  "struct", "structure", "where"];
clasohm@1262
    53
wenzelm@4023
    54
fun is_ml_identifier name =
wenzelm@14680
    55
  not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name;
clasohm@1262
    56
wenzelm@7410
    57
fun warn_ml name =
wenzelm@7410
    58
  if is_ml_identifier name then false
wenzelm@7573
    59
  else if name = "" then true
wenzelm@7410
    60
  else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
wenzelm@7410
    61
wenzelm@10914
    62
val use_text_verbose = use_text Context.ml_output true;
wenzelm@7854
    63
wenzelm@4023
    64
fun ml_store_thm (name, thm) =
wenzelm@4023
    65
  let val thm' = store_thm (name, thm) in
wenzelm@7410
    66
    if warn_ml name then ()
wenzelm@13279
    67
    else (qed_thms := [thm'];
wenzelm@13279
    68
      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@17170
    78
(* legacy bindings *)
wenzelm@17170
    79
wenzelm@17170
    80
fun legacy_bindings thy =
wenzelm@17170
    81
  let
wenzelm@17170
    82
    val thy_name = Context.theory_name thy;
wenzelm@17170
    83
    val (space, thms) = PureThy.theorems_of thy;
wenzelm@17170
    84
wenzelm@17170
    85
    fun prune name =
wenzelm@17170
    86
      let
wenzelm@17170
    87
        val xname = NameSpace.extern space name;
wenzelm@17170
    88
        fun result prfx bname =
wenzelm@17170
    89
          if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
wenzelm@17170
    90
              NameSpace.intern space xname = name then
wenzelm@17412
    91
            SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
wenzelm@17170
    92
          else NONE;
wenzelm@17170
    93
        val names = NameSpace.unpack name;
wenzelm@17170
    94
      in
wenzelm@19012
    95
        (case #2 (chop (length names - 2) names) of
wenzelm@17170
    96
          [bname] => result "" bname
wenzelm@17170
    97
        | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
wenzelm@17170
    98
        | _ => NONE)
wenzelm@17170
    99
      end;
wenzelm@17170
   100
wenzelm@17170
   101
    fun mk_struct "" = I
wenzelm@17170
   102
      | mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n";
wenzelm@17170
   103
wenzelm@17170
   104
    fun mk_thm (bname, xname, singleton) =
wenzelm@17170
   105
      "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
wenzelm@17170
   106
  in
wenzelm@19482
   107
    Symtab.keys thms |> map_filter prune
wenzelm@18931
   108
    |> Symtab.make_list |> Symtab.dest |> sort_wrt #1
wenzelm@17170
   109
    |> map (fn (prfx, entries) =>
wenzelm@17170
   110
      entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
wenzelm@17170
   111
    |> cat_lines
wenzelm@17170
   112
  end;
wenzelm@17170
   113
wenzelm@17170
   114
fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy);
wenzelm@17170
   115
clasohm@1132
   116
end;
wenzelm@6204
   117
wenzelm@6204
   118
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
wenzelm@6204
   119
open BasicThmDatabase;