src/Pure/fact_index.ML
author wenzelm
Tue Jul 02 15:36:12 2002 +0200 (2002-07-02)
changeset 13270 d7f35250cbad
child 13283 1051aa66cbf3
permissions -rw-r--r--
Facts indexed by consts or (some) frees.
     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), 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,
    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, consts = Symtab.empty, frees = Symtab.empty};
    47 
    48 fun add pred (Index {next, 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 Index {next = next + 1, consts = foldl upd (consts, cs), frees = foldl upd (frees, xs)} end;
    53 
    54 
    55 (* find facts *)
    56 
    57 fun intersect ([], _) = []
    58   | intersect (_, []) = []
    59   | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
    60       if i = j then x :: intersect (xs, ys)
    61       else if i > j then intersect (xs, yys)
    62       else intersect (xxs, ys);
    63 
    64 fun intersects [xs] = xs
    65   | intersects xss = if exists null xss then [] else foldl intersect (hd xss, tl xss);
    66 
    67 fun find (cs, xs) (Index {consts, frees, ...}) =
    68   let
    69     val raw =
    70       map (curry Symtab.lookup_multi consts) cs @
    71       map (curry Symtab.lookup_multi frees) xs;
    72     val res =
    73       if null raw then map #2 (Symtab.dest consts @ Symtab.dest frees) else raw;
    74   in map #2 (intersects res) end;
    75 
    76 end;