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