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