src/Pure/fact_index.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15570 8d8c70b41bab
child 16020 ace2c610b5be
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
wenzelm@13270
     1
(*  Title:      Pure/fact_index.ML
wenzelm@13270
     2
    ID:         $Id$
wenzelm@13270
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@13270
     4
wenzelm@13270
     5
Facts indexed by consts or (some) frees.
wenzelm@13270
     6
*)
wenzelm@13270
     7
wenzelm@13270
     8
signature FACT_INDEX =
wenzelm@13270
     9
sig
wenzelm@13270
    10
  val index_term: (string -> bool) -> (string list * string list) * term
wenzelm@13270
    11
    -> string list * string list
wenzelm@13270
    12
  val index_thm: (string -> bool) -> (string list * string list) * thm
wenzelm@13270
    13
    -> string list * string list
wenzelm@13270
    14
  type T
wenzelm@13270
    15
  val empty: T
wenzelm@13270
    16
  val add: (string -> bool) -> T * (string * thm list) -> T
wenzelm@13270
    17
  val find: string list * string list -> T -> (string * thm list) list
wenzelm@13270
    18
end;
wenzelm@13270
    19
wenzelm@13270
    20
structure FactIndex: FACT_INDEX =
wenzelm@13270
    21
struct
wenzelm@13270
    22
wenzelm@13270
    23
(* indexing items *)
wenzelm@13270
    24
wenzelm@13270
    25
fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
wenzelm@13270
    26
  | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
wenzelm@13270
    27
  | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
wenzelm@13270
    28
  | add_frees _ (_, xs) = xs;
wenzelm@13270
    29
wenzelm@13270
    30
fun index_term pred ((cs, xs), t) =
wenzelm@13542
    31
  (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
wenzelm@13270
    32
wenzelm@13270
    33
fun index_thm pred (idx, th) =
wenzelm@13270
    34
  let val {hyps, prop, ...} = Thm.rep_thm th
skalberg@15570
    35
  in Library.foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
wenzelm@13270
    36
wenzelm@13270
    37
wenzelm@13270
    38
(* build index *)
wenzelm@13270
    39
wenzelm@13283
    40
datatype T = Index of {next: int, facts: (string * thm list) list,
wenzelm@13270
    41
  consts: (int * (string * thm list)) list Symtab.table,
wenzelm@13270
    42
  frees: (int * (string * thm list)) list Symtab.table};
wenzelm@13270
    43
wenzelm@13270
    44
val empty =
wenzelm@13283
    45
  Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
wenzelm@13270
    46
wenzelm@13283
    47
fun add pred (Index {next, facts, consts, frees}, (name, ths)) =
wenzelm@13270
    48
  let
wenzelm@13270
    49
    fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
skalberg@15570
    50
    val (cs, xs) = Library.foldl (index_thm pred) (([], []), ths);
wenzelm@13283
    51
  in
wenzelm@13283
    52
    Index {next = next + 1, facts = (name, ths) :: facts,
skalberg@15570
    53
      consts = Library.foldl upd (consts, cs), frees = Library.foldl upd (frees, xs)}
wenzelm@13283
    54
  end;
wenzelm@13270
    55
wenzelm@13270
    56
wenzelm@13270
    57
(* find facts *)
wenzelm@13270
    58
wenzelm@13270
    59
fun intersect ([], _) = []
wenzelm@13270
    60
  | intersect (_, []) = []
wenzelm@13270
    61
  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
wenzelm@13270
    62
      if i = j then x :: intersect (xs, ys)
wenzelm@13270
    63
      else if i > j then intersect (xs, yys)
wenzelm@13270
    64
      else intersect (xxs, ys);
wenzelm@13270
    65
wenzelm@13270
    66
fun intersects [xs] = xs
skalberg@15570
    67
  | intersects xss = if exists null xss then [] else Library.foldl intersect (hd xss, tl xss);
wenzelm@13270
    68
wenzelm@13283
    69
fun find ([], []) (Index {facts, ...}) = facts
wenzelm@13283
    70
  | find (cs, xs) (Index {consts, frees, ...}) =
wenzelm@13283
    71
      (map (curry Symtab.lookup_multi consts) cs @
wenzelm@13283
    72
        map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
wenzelm@13270
    73
wenzelm@13270
    74
end;