src/Pure/fact_index.ML
changeset 13270 d7f35250cbad
child 13283 1051aa66cbf3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/fact_index.ML	Tue Jul 02 15:36:12 2002 +0200
     1.3 @@ -0,0 +1,76 @@
     1.4 +(*  Title:      Pure/fact_index.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Facts indexed by consts or (some) frees.
    1.10 +*)
    1.11 +
    1.12 +signature FACT_INDEX =
    1.13 +sig
    1.14 +  val index_term: (string -> bool) -> (string list * string list) * term
    1.15 +    -> string list * string list
    1.16 +  val index_thm: (string -> bool) -> (string list * string list) * thm
    1.17 +    -> string list * string list
    1.18 +  type T
    1.19 +  val empty: T
    1.20 +  val add: (string -> bool) -> T * (string * thm list) -> T
    1.21 +  val find: string list * string list -> T -> (string * thm list) list
    1.22 +end;
    1.23 +
    1.24 +structure FactIndex: FACT_INDEX =
    1.25 +struct
    1.26 +
    1.27 +(* indexing items *)
    1.28 +
    1.29 +fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
    1.30 +  | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
    1.31 +  | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
    1.32 +  | add_frees _ (_, xs) = xs;
    1.33 +
    1.34 +fun index_term pred ((cs, xs), t) =
    1.35 +  (Term.add_term_consts (t, cs), add_frees pred (t, xs));
    1.36 +
    1.37 +fun index_thm pred (idx, th) =
    1.38 +  let val {hyps, prop, ...} = Thm.rep_thm th
    1.39 +  in foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
    1.40 +
    1.41 +
    1.42 +(* build index *)
    1.43 +
    1.44 +datatype T = Index of {next: int,
    1.45 +  consts: (int * (string * thm list)) list Symtab.table,
    1.46 +  frees: (int * (string * thm list)) list Symtab.table};
    1.47 +
    1.48 +val empty =
    1.49 +  Index {next = 0, consts = Symtab.empty, frees = Symtab.empty};
    1.50 +
    1.51 +fun add pred (Index {next, consts, frees}, (name, ths)) =
    1.52 +  let
    1.53 +    fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
    1.54 +    val (cs, xs) = foldl (index_thm pred) (([], []), ths);
    1.55 +  in Index {next = next + 1, consts = foldl upd (consts, cs), frees = foldl upd (frees, xs)} end;
    1.56 +
    1.57 +
    1.58 +(* find facts *)
    1.59 +
    1.60 +fun intersect ([], _) = []
    1.61 +  | intersect (_, []) = []
    1.62 +  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
    1.63 +      if i = j then x :: intersect (xs, ys)
    1.64 +      else if i > j then intersect (xs, yys)
    1.65 +      else intersect (xxs, ys);
    1.66 +
    1.67 +fun intersects [xs] = xs
    1.68 +  | intersects xss = if exists null xss then [] else foldl intersect (hd xss, tl xss);
    1.69 +
    1.70 +fun find (cs, xs) (Index {consts, frees, ...}) =
    1.71 +  let
    1.72 +    val raw =
    1.73 +      map (curry Symtab.lookup_multi consts) cs @
    1.74 +      map (curry Symtab.lookup_multi frees) xs;
    1.75 +    val res =
    1.76 +      if null raw then map #2 (Symtab.dest consts @ Symtab.dest frees) else raw;
    1.77 +  in map #2 (intersects res) end;
    1.78 +
    1.79 +end;