src/Pure/facts.ML
author Timothy Bourke
Mon Feb 09 17:25:07 2009 +1100 (2009-02-09)
changeset 29848 a7c164e228e1
parent 29581 b3b33e0298eb
child 33093 d010f61d3702
permissions -rw-r--r--
Nicer names in FindTheorems.
* Patch NameSpace.get_accesses, contributed by Timothy Bourke:

NameSpace.get_accesses has been patched to fix the following
bug:
theory OverHOL imports Main begin
lemma conjI: "a & b --> b"
by blast

ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of;
val x1 = NameSpace.get_accesses ns "HOL.conjI";
val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *}
end

where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"],
but x1 should be just ["HOL.conjI"].

NameSpace.get_accesses is only used within the NameSpace
structure itself. The two uses have been modified to retain
their original behaviour.

Note that NameSpace.valid_accesses gives different results:
get_accesses ns "HOL.eq_class.eq"
gives ["eq", "eq_class.eq", "HOL.eq_class.eq"]
but,
valid_accesses ns "HOL.eq_class.eq"
gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"]

* Patch FindTheorems:
Prefer names that are shorter to type in the current context.

* Re-export space_of.
wenzelm@26281
     1
(*  Title:      Pure/facts.ML
wenzelm@26281
     2
    Author:     Makarius
wenzelm@26281
     3
wenzelm@26307
     4
Environment of named facts, optionally indexed by proposition.
wenzelm@26281
     5
*)
wenzelm@26281
     6
wenzelm@26281
     7
signature FACTS =
wenzelm@26281
     8
sig
wenzelm@26336
     9
  val the_single: string -> thm list -> thm
wenzelm@26336
    10
  datatype interval = FromTo of int * int | From of int | Single of int
wenzelm@26336
    11
  datatype ref =
wenzelm@26361
    12
    Named of (string * Position.T) * interval list option |
wenzelm@26336
    13
    Fact of string
wenzelm@26361
    14
  val named: string -> ref
wenzelm@26336
    15
  val string_of_ref: ref -> string
wenzelm@26336
    16
  val name_of_ref: ref -> string
wenzelm@26366
    17
  val pos_of_ref: ref -> Position.T
wenzelm@26336
    18
  val map_name_of_ref: (string -> string) -> ref -> ref
wenzelm@26336
    19
  val select: ref -> thm list -> thm list
wenzelm@26336
    20
  val selections: string * thm list -> (ref * thm) list
wenzelm@26281
    21
  type T
wenzelm@26393
    22
  val empty: T
Timothy@29848
    23
  val space_of: T -> NameSpace.T
wenzelm@26664
    24
  val intern: T -> xstring -> string
wenzelm@26664
    25
  val extern: T -> string -> xstring
wenzelm@27738
    26
  val lookup: Context.generic -> T -> string -> (bool * thm list) option
wenzelm@26692
    27
  val defined: T -> string -> bool
wenzelm@26692
    28
  val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
wenzelm@27175
    29
  val dest_static: T list -> T -> (string * thm list) list
wenzelm@27175
    30
  val extern_static: T list -> T -> (xstring * thm list) list
wenzelm@26281
    31
  val props: T -> thm list
wenzelm@26281
    32
  val could_unify: T -> term -> thm list
wenzelm@26281
    33
  val merge: T * T -> T
haftmann@29581
    34
  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
haftmann@29581
    35
  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
haftmann@29581
    36
  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
wenzelm@26654
    37
  val del: string -> T -> T
wenzelm@26654
    38
  val hide: bool -> string -> T -> T
wenzelm@26281
    39
end;
wenzelm@26281
    40
wenzelm@26281
    41
structure Facts: FACTS =
wenzelm@26281
    42
struct
wenzelm@26281
    43
wenzelm@26336
    44
(** fact references **)
wenzelm@26336
    45
wenzelm@26336
    46
fun the_single _ [th] : thm = th
wenzelm@26336
    47
  | the_single name _ = error ("Single theorem expected " ^ quote name);
wenzelm@26336
    48
wenzelm@26336
    49
wenzelm@26336
    50
(* datatype interval *)
wenzelm@26336
    51
wenzelm@26336
    52
datatype interval =
wenzelm@26336
    53
  FromTo of int * int |
wenzelm@26336
    54
  From of int |
wenzelm@26336
    55
  Single of int;
wenzelm@26336
    56
wenzelm@26336
    57
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
wenzelm@26336
    58
  | string_of_interval (From i) = string_of_int i ^ "-"
wenzelm@26336
    59
  | string_of_interval (Single i) = string_of_int i;
wenzelm@26336
    60
wenzelm@26336
    61
fun interval n iv =
wenzelm@26336
    62
  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
wenzelm@26336
    63
    (case iv of
wenzelm@26336
    64
      FromTo (i, j) => if i <= j then i upto j else err ()
wenzelm@26336
    65
    | From i => if i <= n then i upto n else err ()
wenzelm@26336
    66
    | Single i => [i])
wenzelm@26336
    67
  end;
wenzelm@26336
    68
wenzelm@26336
    69
wenzelm@26336
    70
(* datatype ref *)
wenzelm@26336
    71
wenzelm@26336
    72
datatype ref =
wenzelm@26361
    73
  Named of (string * Position.T) * interval list option |
wenzelm@26336
    74
  Fact of string;
wenzelm@26336
    75
wenzelm@26361
    76
fun named name = Named ((name, Position.none), NONE);
wenzelm@26361
    77
wenzelm@26366
    78
fun name_pos_of_ref (Named (name_pos, _)) = name_pos
wenzelm@26366
    79
  | name_pos_of_ref (Fact _) = error "Illegal literal fact";
wenzelm@26366
    80
wenzelm@26366
    81
val name_of_ref = #1 o name_pos_of_ref;
wenzelm@26366
    82
val pos_of_ref = #2 o name_pos_of_ref;
wenzelm@26336
    83
wenzelm@26361
    84
fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
wenzelm@26336
    85
  | map_name_of_ref _ r = r;
wenzelm@26336
    86
wenzelm@26361
    87
fun string_of_ref (Named ((name, _), NONE)) = name
wenzelm@26361
    88
  | string_of_ref (Named ((name, _), SOME is)) =
wenzelm@26336
    89
      name ^ enclose "(" ")" (commas (map string_of_interval is))
wenzelm@26336
    90
  | string_of_ref (Fact _) = error "Illegal literal fact";
wenzelm@26336
    91
wenzelm@26336
    92
wenzelm@26336
    93
(* select *)
wenzelm@26336
    94
wenzelm@26336
    95
fun select (Fact _) ths = ths
wenzelm@26336
    96
  | select (Named (_, NONE)) ths = ths
wenzelm@26361
    97
  | select (Named ((name, pos), SOME ivs)) ths =
wenzelm@26336
    98
      let
wenzelm@26336
    99
        val n = length ths;
wenzelm@26361
   100
        fun err msg =
wenzelm@26361
   101
          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
wenzelm@26361
   102
            Position.str_of pos);
wenzelm@26336
   103
        fun sel i =
wenzelm@26336
   104
          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
wenzelm@26336
   105
          else nth ths (i - 1);
wenzelm@26336
   106
        val is = maps (interval n) ivs handle Fail msg => err msg;
wenzelm@26336
   107
      in map sel is end;
wenzelm@26336
   108
wenzelm@26336
   109
wenzelm@26336
   110
(* selections *)
wenzelm@26336
   111
wenzelm@26361
   112
fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
wenzelm@26361
   113
  | selections (name, ths) = map2 (fn i => fn th =>
wenzelm@26361
   114
      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
wenzelm@26336
   115
wenzelm@26336
   116
wenzelm@26336
   117
wenzelm@26336
   118
(** fact environment **)
wenzelm@26336
   119
wenzelm@26393
   120
(* datatypes *)
wenzelm@26393
   121
wenzelm@26393
   122
datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
wenzelm@26281
   123
wenzelm@26281
   124
datatype T = Facts of
wenzelm@26393
   125
 {facts: (fact * serial) NameSpace.table,
wenzelm@26281
   126
  props: thm Net.net};
wenzelm@26281
   127
wenzelm@26281
   128
fun make_facts facts props = Facts {facts = facts, props = props};
wenzelm@26393
   129
val empty = make_facts NameSpace.empty_table Net.empty;
wenzelm@26281
   130
wenzelm@26281
   131
wenzelm@26281
   132
(* named facts *)
wenzelm@26281
   133
wenzelm@26281
   134
fun facts_of (Facts {facts, ...}) = facts;
wenzelm@26281
   135
wenzelm@26281
   136
val space_of = #1 o facts_of;
wenzelm@26393
   137
val table_of = #2 o facts_of;
wenzelm@26393
   138
wenzelm@26664
   139
val intern = NameSpace.intern o space_of;
wenzelm@26664
   140
val extern = NameSpace.extern o space_of;
wenzelm@26664
   141
wenzelm@26692
   142
val defined = Symtab.defined o table_of;
wenzelm@26692
   143
wenzelm@26393
   144
fun lookup context facts name =
wenzelm@26393
   145
  (case Symtab.lookup (table_of facts) name of
wenzelm@26393
   146
    NONE => NONE
wenzelm@27738
   147
  | SOME (Static ths, _) => SOME (true, ths)
wenzelm@27738
   148
  | SOME (Dynamic f, _) => SOME (false, f context));
wenzelm@26393
   149
wenzelm@26692
   150
fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
wenzelm@26393
   151
wenzelm@27175
   152
wenzelm@27175
   153
(* content difference *)
wenzelm@27175
   154
wenzelm@27175
   155
fun diff_table prev_facts facts =
wenzelm@27175
   156
  fold_static (fn (name, ths) =>
wenzelm@27175
   157
    if exists (fn prev => defined prev name) prev_facts then I
wenzelm@27175
   158
    else cons (name, ths)) facts [];
wenzelm@27175
   159
wenzelm@27175
   160
fun dest_static prev_facts facts =
wenzelm@27175
   161
  sort_wrt #1 (diff_table prev_facts facts);
wenzelm@27175
   162
wenzelm@27175
   163
fun extern_static prev_facts facts =
wenzelm@27175
   164
  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
wenzelm@26281
   165
wenzelm@26281
   166
wenzelm@26281
   167
(* indexed props *)
wenzelm@26281
   168
wenzelm@29269
   169
val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of;
wenzelm@26281
   170
wenzelm@26281
   171
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
wenzelm@26281
   172
fun could_unify (Facts {props, ...}) = Net.unify_term props;
wenzelm@26281
   173
wenzelm@26281
   174
wenzelm@26393
   175
(* merge facts *)
wenzelm@26281
   176
wenzelm@26393
   177
fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
wenzelm@26281
   178
wenzelm@27175
   179
(* FIXME stamp identity! *)
wenzelm@26654
   180
fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
wenzelm@26654
   181
  | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
wenzelm@26654
   182
wenzelm@26281
   183
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
wenzelm@26281
   184
  let
wenzelm@26654
   185
    val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
wenzelm@26654
   186
      handle Symtab.DUP dup => err_dup_fact dup;
wenzelm@26281
   187
    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
wenzelm@26281
   188
  in make_facts facts' props' end;
wenzelm@26281
   189
wenzelm@26393
   190
wenzelm@26654
   191
(* add static entries *)
wenzelm@26393
   192
haftmann@28864
   193
fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
wenzelm@26281
   194
  let
haftmann@28965
   195
    val (name, facts') = if Binding.is_empty b then ("", facts)
haftmann@28864
   196
      else let
haftmann@28864
   197
        val (space, tab) = facts;
haftmann@28965
   198
        val (name, space') = NameSpace.declare naming b space;
haftmann@28864
   199
        val entry = (name, (Static ths, serial ()));
haftmann@28864
   200
        val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
haftmann@28864
   201
          handle Symtab.DUP dup => err_dup_fact dup;
haftmann@28864
   202
      in (name, (space', tab')) end;
wenzelm@26281
   203
    val props' =
wenzelm@26281
   204
      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
wenzelm@26281
   205
      else props;
haftmann@28864
   206
  in (name, make_facts facts' props') end;
wenzelm@26281
   207
wenzelm@26307
   208
val add_global = add false false;
wenzelm@26307
   209
val add_local = add true;
wenzelm@26307
   210
wenzelm@26393
   211
wenzelm@26654
   212
(* add dynamic entries *)
wenzelm@26393
   213
haftmann@28864
   214
fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
wenzelm@26290
   215
  let
haftmann@28965
   216
    val (name, space') = NameSpace.declare naming b space;
wenzelm@26393
   217
    val entry = (name, (Dynamic f, serial ()));
wenzelm@26393
   218
    val tab' = Symtab.update_new entry tab
wenzelm@26393
   219
      handle Symtab.DUP dup => err_dup_fact dup;
haftmann@28864
   220
  in (name, make_facts (space', tab') props) end;
wenzelm@26281
   221
wenzelm@26654
   222
wenzelm@26654
   223
(* remove entries *)
wenzelm@26654
   224
wenzelm@26654
   225
fun del name (Facts {facts = (space, tab), props}) =
wenzelm@26654
   226
  let
wenzelm@26654
   227
    val space' = NameSpace.hide true name space handle ERROR _ => space;
wenzelm@26654
   228
    val tab' = Symtab.delete_safe name tab;
wenzelm@26654
   229
  in make_facts (space', tab') props end;
wenzelm@26654
   230
wenzelm@26654
   231
fun hide fully name (Facts {facts = (space, tab), props}) =
wenzelm@26654
   232
  make_facts (NameSpace.hide fully name space, tab) props;
wenzelm@26654
   233
wenzelm@26281
   234
end;