src/Pure/Thy/thm_database.ML
author wenzelm
Sun, 28 Aug 2005 16:04:54 +0200
changeset 17170 cbe14eb12729
parent 15836 b805d85909c7
child 17221 6cd180204582
permissions -rw-r--r--
added (use_)legacy_bindings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thm_database.ML
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     2
    ID:         $Id$
11895
73b2c277974f moved goal related stuff to goals.ML;
wenzelm
parents: 11769
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
     4
17170
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
     5
ML toplevel interface to the theorem database.
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
     6
*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
     7
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
     8
signature BASIC_THM_DATABASE =
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
     9
sig
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    10
  val store_thm: string * thm -> thm
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    11
  val store_thms: string * thm list -> thm list
17170
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    12
  val legacy_bindings: theory -> string
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    13
  val use_legacy_bindings: theory -> unit
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    14
end;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    15
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    16
signature THM_DATABASE =
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    17
sig
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    18
  include BASIC_THM_DATABASE
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    19
  val qed_thms: thm list ref
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    20
  val ml_store_thm: string * thm -> unit
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    21
  val ml_store_thms: string * thm list -> unit
14680
6029e76841fd use Syntax.is_ascii_identifier;
wenzelm
parents: 13279
diff changeset
    22
  val ml_reserved: string list
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    23
  val is_ml_identifier: string -> bool
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    24
end;
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
    25
3627
3d0d5f2a2e33 tuned names;
wenzelm
parents: 3601
diff changeset
    26
structure ThmDatabase: THM_DATABASE =
1221
19dde7bfcd07 Added findI, findEs, and findE.
nipkow
parents: 1141
diff changeset
    27
struct
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    28
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    29
(** store theorems **)
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    30
13279
8a722689a1c9 removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents: 11895
diff changeset
    31
(* store in theory and perform presentation *)
1136
3910c96551d1 fixed bug in thms_containing; changed error/warning messages;
clasohm
parents: 1134
diff changeset
    32
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    33
fun store_thm (name, thm) =
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    34
  let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
6327
c6abb5884fed Present.theorem;
wenzelm
parents: 6204
diff changeset
    35
  in Present.theorem name thm'; thm' end;
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
    36
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    37
fun store_thms (name, thms) =
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    38
  let val thms' = PureThy.smart_store_thms (name, thms)
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    39
  in Present.theorems name thms'; thms' end;
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    40
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    41
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    42
(* store on ML toplevel *)
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    43
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    44
val qed_thms: thm list ref = ref [];
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    45
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    46
val ml_reserved =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    47
 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    48
  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    49
  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    50
  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    51
  "eqtype", "functor", "include", "sharing", "sig", "signature",
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    52
  "struct", "structure", "where"];
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    53
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    54
fun is_ml_identifier name =
14680
6029e76841fd use Syntax.is_ascii_identifier;
wenzelm
parents: 13279
diff changeset
    55
  not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    56
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    57
fun warn_ml name =
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    58
  if is_ml_identifier name then false
7573
aa87cf5a15f5 ml_store_thm: no warning for "";
wenzelm
parents: 7446
diff changeset
    59
  else if name = "" then true
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    60
  else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    61
10914
aded4ba99b88 use_text etc.: proper output of error messages;
wenzelm
parents: 10894
diff changeset
    62
val use_text_verbose = use_text Context.ml_output true;
7854
fe7b7e3c3ddc use_text_verbose;
wenzelm
parents: 7738
diff changeset
    63
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    64
fun ml_store_thm (name, thm) =
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    65
  let val thm' = store_thm (name, thm) in
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    66
    if warn_ml name then ()
13279
8a722689a1c9 removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents: 11895
diff changeset
    67
    else (qed_thms := [thm'];
8a722689a1c9 removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents: 11895
diff changeset
    68
      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
7410
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    69
  end;
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    70
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    71
fun ml_store_thms (name, thms) =
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    72
  let val thms' = store_thms (name, thms) in
7369a35fb3c2 added store/bind_thms;
wenzelm
parents: 7182
diff changeset
    73
    if warn_ml name then ()
7854
fe7b7e3c3ddc use_text_verbose;
wenzelm
parents: 7738
diff changeset
    74
    else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    75
  end;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1245
diff changeset
    76
4023
a9dc0484c903 restructured -- uses PureThy storage facilities;
wenzelm
parents: 3999
diff changeset
    77
17170
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    78
(* legacy bindings *)
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    79
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    80
fun legacy_bindings thy =
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    81
  let
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    82
    val thy_name = Context.theory_name thy;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    83
    val (space, thms) = PureThy.theorems_of thy;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    84
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    85
    fun prune name =
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    86
      let
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    87
        val xname = NameSpace.extern space name;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    88
        fun result prfx bname =
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    89
          if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    90
              NameSpace.intern space xname = name then
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    91
            SOME (prfx, (bname, xname, length (the (Symtab.lookup (thms, name))) = 1))
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    92
          else NONE;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    93
        val names = NameSpace.unpack name;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    94
      in
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    95
        (case #2 (splitAt (length names - 2, names)) of
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    96
          [bname] => result "" bname
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    97
        | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    98
        | _ => NONE)
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
    99
      end;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   100
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   101
    fun mk_struct "" = I
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   102
      | mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n";
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   103
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   104
    fun mk_thm (bname, xname, singleton) =
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   105
      "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   106
  in
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   107
    Symtab.keys thms |> List.mapPartial prune
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   108
    |> Symtab.make_multi |> Symtab.dest |> sort_wrt #1
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   109
    |> map (fn (prfx, entries) =>
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   110
      entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   111
    |> cat_lines
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   112
  end;
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   113
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   114
fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy);
cbe14eb12729 added (use_)legacy_bindings;
wenzelm
parents: 15836
diff changeset
   115
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff changeset
   116
end;
6204
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   117
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   118
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
c7ad5b27894f open BasicThmDatabase;
wenzelm
parents: 5744
diff changeset
   119
open BasicThmDatabase;