src/Pure/fact_index.ML
changeset 16020 ace2c610b5be
parent 15570 8d8c70b41bab
child 16491 7310d0a36599
     1.1 --- a/src/Pure/fact_index.ML	Sun May 22 16:51:07 2005 +0200
     1.2 +++ b/src/Pure/fact_index.ML	Sun May 22 16:51:08 2005 +0200
     1.3 @@ -2,24 +2,27 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Facts indexed by consts or (some) frees.
     1.8 +Facts indexed by consts or frees.
     1.9  *)
    1.10  
    1.11  signature FACT_INDEX =
    1.12  sig
    1.13 -  val index_term: (string -> bool) -> (string list * string list) * term
    1.14 -    -> string list * string list
    1.15 -  val index_thm: (string -> bool) -> (string list * string list) * thm
    1.16 -    -> string list * string list
    1.17 +  type spec
    1.18 +  val index_term: (string -> bool) -> term -> spec -> spec
    1.19 +  val index_thm: (string -> bool) -> thm -> spec -> spec
    1.20    type T
    1.21 +  val facts: T -> (string * thm list) list
    1.22    val empty: T
    1.23 -  val add: (string -> bool) -> T * (string * thm list) -> T
    1.24 -  val find: string list * string list -> T -> (string * thm list) list
    1.25 +  val add: (string -> bool) -> (string * thm list) -> T -> T
    1.26 +  val find: T -> spec -> (string * thm list) list
    1.27  end;
    1.28  
    1.29  structure FactIndex: FACT_INDEX =
    1.30  struct
    1.31  
    1.32 +type spec = string list * string list;
    1.33 +
    1.34 +
    1.35  (* indexing items *)
    1.36  
    1.37  fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
    1.38 @@ -27,12 +30,16 @@
    1.39    | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
    1.40    | add_frees _ (_, xs) = xs;
    1.41  
    1.42 -fun index_term pred ((cs, xs), t) =
    1.43 +fun index_term pred t (cs, xs) =
    1.44    (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
    1.45  
    1.46 -fun index_thm pred (idx, th) =
    1.47 -  let val {hyps, prop, ...} = Thm.rep_thm th
    1.48 -  in Library.foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
    1.49 +fun index_thm pred th idx =
    1.50 +  let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
    1.51 +    idx
    1.52 +    |> index_term pred prop
    1.53 +    |> fold (index_term pred) hyps
    1.54 +    |> fold (index_term pred) (Thm.terms_of_tpairs tpairs)
    1.55 +  end;
    1.56  
    1.57  
    1.58  (* build index *)
    1.59 @@ -41,16 +48,18 @@
    1.60    consts: (int * (string * thm list)) list Symtab.table,
    1.61    frees: (int * (string * thm list)) list Symtab.table};
    1.62  
    1.63 +fun facts (Index {facts, ...}) = facts;
    1.64 +
    1.65  val empty =
    1.66    Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
    1.67  
    1.68 -fun add pred (Index {next, facts, consts, frees}, (name, ths)) =
    1.69 +fun add pred (name, ths) (Index {next, facts, consts, frees}) =
    1.70    let
    1.71 -    fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
    1.72 -    val (cs, xs) = Library.foldl (index_thm pred) (([], []), ths);
    1.73 +    fun upd a tab = Symtab.update_multi ((a, (next, (name, ths))), tab);
    1.74 +    val (cs, xs) = fold (index_thm pred) ths ([], []);
    1.75    in
    1.76      Index {next = next + 1, facts = (name, ths) :: facts,
    1.77 -      consts = Library.foldl upd (consts, cs), frees = Library.foldl upd (frees, xs)}
    1.78 +      consts = fold upd cs consts, frees = fold upd xs frees}
    1.79    end;
    1.80  
    1.81  
    1.82 @@ -64,10 +73,10 @@
    1.83        else intersect (xxs, ys);
    1.84  
    1.85  fun intersects [xs] = xs
    1.86 -  | intersects xss = if exists null xss then [] else Library.foldl intersect (hd xss, tl xss);
    1.87 +  | intersects xss = if exists null xss then [] else foldr1 intersect xss;
    1.88  
    1.89 -fun find ([], []) (Index {facts, ...}) = facts
    1.90 -  | find (cs, xs) (Index {consts, frees, ...}) =
    1.91 +fun find idx ([], []) = facts idx
    1.92 +  | find (Index {consts, frees, ...}) (cs, xs) =
    1.93        (map (curry Symtab.lookup_multi consts) cs @
    1.94          map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
    1.95