src/Pure/fact_index.ML
author wenzelm
Tue Jul 02 17:00:05 2002 +0200 (2002-07-02)
changeset 13283 1051aa66cbf3
parent 13270 d7f35250cbad
child 13542 bb3e8a86d610
permissions -rw-r--r--
proper treatment of border cases;
wenzelm@13270
     1
(*  Title:      Pure/fact_index.ML
wenzelm@13270
     2
    ID:         $Id$
wenzelm@13270
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@13270
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@13270
     5
wenzelm@13270
     6
Facts indexed by consts or (some) frees.
wenzelm@13270
     7
*)
wenzelm@13270
     8
wenzelm@13270
     9
signature FACT_INDEX =
wenzelm@13270
    10
sig
wenzelm@13270
    11
  val index_term: (string -> bool) -> (string list * string list) * term
wenzelm@13270
    12
    -> string list * string list
wenzelm@13270
    13
  val index_thm: (string -> bool) -> (string list * string list) * thm
wenzelm@13270
    14
    -> string list * string list
wenzelm@13270
    15
  type T
wenzelm@13270
    16
  val empty: T
wenzelm@13270
    17
  val add: (string -> bool) -> T * (string * thm list) -> T
wenzelm@13270
    18
  val find: string list * string list -> T -> (string * thm list) list
wenzelm@13270
    19
end;
wenzelm@13270
    20
wenzelm@13270
    21
structure FactIndex: FACT_INDEX =
wenzelm@13270
    22
struct
wenzelm@13270
    23
wenzelm@13270
    24
(* indexing items *)
wenzelm@13270
    25
wenzelm@13270
    26
fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
wenzelm@13270
    27
  | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
wenzelm@13270
    28
  | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
wenzelm@13270
    29
  | add_frees _ (_, xs) = xs;
wenzelm@13270
    30
wenzelm@13270
    31
fun index_term pred ((cs, xs), t) =
wenzelm@13270
    32
  (Term.add_term_consts (t, cs), add_frees pred (t, xs));
wenzelm@13270
    33
wenzelm@13270
    34
fun index_thm pred (idx, th) =
wenzelm@13270
    35
  let val {hyps, prop, ...} = Thm.rep_thm th
wenzelm@13270
    36
  in foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
wenzelm@13270
    37
wenzelm@13270
    38
wenzelm@13270
    39
(* build index *)
wenzelm@13270
    40
wenzelm@13283
    41
datatype T = Index of {next: int, facts: (string * thm list) list,
wenzelm@13270
    42
  consts: (int * (string * thm list)) list Symtab.table,
wenzelm@13270
    43
  frees: (int * (string * thm list)) list Symtab.table};
wenzelm@13270
    44
wenzelm@13270
    45
val empty =
wenzelm@13283
    46
  Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
wenzelm@13270
    47
wenzelm@13283
    48
fun add pred (Index {next, facts, consts, frees}, (name, ths)) =
wenzelm@13270
    49
  let
wenzelm@13270
    50
    fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
wenzelm@13270
    51
    val (cs, xs) = foldl (index_thm pred) (([], []), ths);
wenzelm@13283
    52
  in
wenzelm@13283
    53
    Index {next = next + 1, facts = (name, ths) :: facts,
wenzelm@13283
    54
      consts = foldl upd (consts, cs), frees = foldl upd (frees, xs)}
wenzelm@13283
    55
  end;
wenzelm@13270
    56
wenzelm@13270
    57
wenzelm@13270
    58
(* find facts *)
wenzelm@13270
    59
wenzelm@13270
    60
fun intersect ([], _) = []
wenzelm@13270
    61
  | intersect (_, []) = []
wenzelm@13270
    62
  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
wenzelm@13270
    63
      if i = j then x :: intersect (xs, ys)
wenzelm@13270
    64
      else if i > j then intersect (xs, yys)
wenzelm@13270
    65
      else intersect (xxs, ys);
wenzelm@13270
    66
wenzelm@13270
    67
fun intersects [xs] = xs
wenzelm@13270
    68
  | intersects xss = if exists null xss then [] else foldl intersect (hd xss, tl xss);
wenzelm@13270
    69
wenzelm@13283
    70
fun find ([], []) (Index {facts, ...}) = facts
wenzelm@13283
    71
  | find (cs, xs) (Index {consts, frees, ...}) =
wenzelm@13283
    72
      (map (curry Symtab.lookup_multi consts) cs @
wenzelm@13283
    73
        map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
wenzelm@13270
    74
wenzelm@13270
    75
end;