src/Pure/fact_index.ML
author wenzelm
Sun May 22 16:51:08 2005 +0200 (2005-05-22)
changeset 16020 ace2c610b5be
parent 15570 8d8c70b41bab
child 16491 7310d0a36599
permissions -rw-r--r--
major tuning;
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@16020
     5
Facts indexed by consts or frees.
wenzelm@13270
     6
*)
wenzelm@13270
     7
wenzelm@13270
     8
signature FACT_INDEX =
wenzelm@13270
     9
sig
wenzelm@16020
    10
  type spec
wenzelm@16020
    11
  val index_term: (string -> bool) -> term -> spec -> spec
wenzelm@16020
    12
  val index_thm: (string -> bool) -> thm -> spec -> spec
wenzelm@13270
    13
  type T
wenzelm@16020
    14
  val facts: T -> (string * thm list) list
wenzelm@13270
    15
  val empty: T
wenzelm@16020
    16
  val add: (string -> bool) -> (string * thm list) -> T -> T
wenzelm@16020
    17
  val find: T -> spec -> (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@16020
    23
type spec = string list * string list;
wenzelm@16020
    24
wenzelm@16020
    25
wenzelm@13270
    26
(* indexing items *)
wenzelm@13270
    27
wenzelm@13270
    28
fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
wenzelm@13270
    29
  | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
wenzelm@13270
    30
  | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
wenzelm@13270
    31
  | add_frees _ (_, xs) = xs;
wenzelm@13270
    32
wenzelm@16020
    33
fun index_term pred t (cs, xs) =
wenzelm@13542
    34
  (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
wenzelm@13270
    35
wenzelm@16020
    36
fun index_thm pred th idx =
wenzelm@16020
    37
  let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
wenzelm@16020
    38
    idx
wenzelm@16020
    39
    |> index_term pred prop
wenzelm@16020
    40
    |> fold (index_term pred) hyps
wenzelm@16020
    41
    |> fold (index_term pred) (Thm.terms_of_tpairs tpairs)
wenzelm@16020
    42
  end;
wenzelm@13270
    43
wenzelm@13270
    44
wenzelm@13270
    45
(* build index *)
wenzelm@13270
    46
wenzelm@13283
    47
datatype T = Index of {next: int, facts: (string * thm list) list,
wenzelm@13270
    48
  consts: (int * (string * thm list)) list Symtab.table,
wenzelm@13270
    49
  frees: (int * (string * thm list)) list Symtab.table};
wenzelm@13270
    50
wenzelm@16020
    51
fun facts (Index {facts, ...}) = facts;
wenzelm@16020
    52
wenzelm@13270
    53
val empty =
wenzelm@13283
    54
  Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
wenzelm@13270
    55
wenzelm@16020
    56
fun add pred (name, ths) (Index {next, facts, consts, frees}) =
wenzelm@13270
    57
  let
wenzelm@16020
    58
    fun upd a tab = Symtab.update_multi ((a, (next, (name, ths))), tab);
wenzelm@16020
    59
    val (cs, xs) = fold (index_thm pred) ths ([], []);
wenzelm@13283
    60
  in
wenzelm@13283
    61
    Index {next = next + 1, facts = (name, ths) :: facts,
wenzelm@16020
    62
      consts = fold upd cs consts, frees = fold upd xs frees}
wenzelm@13283
    63
  end;
wenzelm@13270
    64
wenzelm@13270
    65
wenzelm@13270
    66
(* find facts *)
wenzelm@13270
    67
wenzelm@13270
    68
fun intersect ([], _) = []
wenzelm@13270
    69
  | intersect (_, []) = []
wenzelm@13270
    70
  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
wenzelm@13270
    71
      if i = j then x :: intersect (xs, ys)
wenzelm@13270
    72
      else if i > j then intersect (xs, yys)
wenzelm@13270
    73
      else intersect (xxs, ys);
wenzelm@13270
    74
wenzelm@13270
    75
fun intersects [xs] = xs
wenzelm@16020
    76
  | intersects xss = if exists null xss then [] else foldr1 intersect xss;
wenzelm@13270
    77
wenzelm@16020
    78
fun find idx ([], []) = facts idx
wenzelm@16020
    79
  | find (Index {consts, frees, ...}) (cs, xs) =
wenzelm@13283
    80
      (map (curry Symtab.lookup_multi consts) cs @
wenzelm@13283
    81
        map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
wenzelm@13270
    82
wenzelm@13270
    83
end;