src/Pure/fact_index.ML
author haftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 17271 2756a73f63a5
parent 17221 6cd180204582
child 17412 e26cb20ef0cc
permissions -rw-r--r--
introduced some new-style AList operations
     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 val add_consts = fold_aterms
    29   (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
    30 
    31 fun add_frees pred = fold_aterms
    32   (fn Free (x, _) => if pred x then insert (op =) x else I | _ => I);
    33 
    34 fun index_term pred t (cs, xs) = (add_consts t cs, 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 (fn (t, u) => index_term pred t #> index_term pred u) 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 = Symtab.curried_update_multi (a, (next, (name, ths)));
    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 fact_ord ((i, _), (j, _)) = int_ord (j, i);
    69 
    70 fun intersects [xs] = xs
    71   | intersects xss =
    72       if exists null xss then []
    73       else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
    74 
    75 fun find idx ([], []) = facts idx
    76   | find (Index {consts, frees, ...}) (cs, xs) =
    77       (map (Symtab.curried_lookup_multi consts) cs @
    78         map (Symtab.curried_lookup_multi frees) xs) |> intersects |> map #2;
    79 
    80 end;