src/Pure/fact_index.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15570 8d8c70b41bab
child 16020 ace2c610b5be
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     1 (*  Title:      Pure/fact_index.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Facts indexed by consts or (some) frees.
     6 *)
     7 
     8 signature FACT_INDEX =
     9 sig
    10   val index_term: (string -> bool) -> (string list * string list) * term
    11     -> string list * string list
    12   val index_thm: (string -> bool) -> (string list * string list) * thm
    13     -> string list * string list
    14   type T
    15   val empty: T
    16   val add: (string -> bool) -> T * (string * thm list) -> T
    17   val find: string list * string list -> T -> (string * thm list) list
    18 end;
    19 
    20 structure FactIndex: FACT_INDEX =
    21 struct
    22 
    23 (* indexing items *)
    24 
    25 fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
    26   | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
    27   | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
    28   | add_frees _ (_, xs) = xs;
    29 
    30 fun index_term pred ((cs, xs), t) =
    31   (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
    32 
    33 fun index_thm pred (idx, th) =
    34   let val {hyps, prop, ...} = Thm.rep_thm th
    35   in Library.foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
    36 
    37 
    38 (* build index *)
    39 
    40 datatype T = Index of {next: int, facts: (string * thm list) list,
    41   consts: (int * (string * thm list)) list Symtab.table,
    42   frees: (int * (string * thm list)) list Symtab.table};
    43 
    44 val empty =
    45   Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
    46 
    47 fun add pred (Index {next, facts, consts, frees}, (name, ths)) =
    48   let
    49     fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
    50     val (cs, xs) = Library.foldl (index_thm pred) (([], []), ths);
    51   in
    52     Index {next = next + 1, facts = (name, ths) :: facts,
    53       consts = Library.foldl upd (consts, cs), frees = Library.foldl upd (frees, xs)}
    54   end;
    55 
    56 
    57 (* find facts *)
    58 
    59 fun intersect ([], _) = []
    60   | intersect (_, []) = []
    61   | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
    62       if i = j then x :: intersect (xs, ys)
    63       else if i > j then intersect (xs, yys)
    64       else intersect (xxs, ys);
    65 
    66 fun intersects [xs] = xs
    67   | intersects xss = if exists null xss then [] else Library.foldl intersect (hd xss, tl xss);
    68 
    69 fun find ([], []) (Index {facts, ...}) = facts
    70   | find (cs, xs) (Index {consts, frees, ...}) =
    71       (map (curry Symtab.lookup_multi consts) cs @
    72         map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
    73 
    74 end;