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