src/Pure/fact_index.ML
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 13542 bb3e8a86d610
child 15570 8d8c70b41bab
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/fact_index.ML
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     4
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     5
Facts indexed by consts or (some) frees.
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     6
*)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     7
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     8
signature FACT_INDEX =
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
     9
sig
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    10
  val index_term: (string -> bool) -> (string list * string list) * term
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    11
    -> string list * string list
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    12
  val index_thm: (string -> bool) -> (string list * string list) * thm
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    13
    -> string list * string list
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    14
  type T
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    15
  val empty: T
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    16
  val add: (string -> bool) -> T * (string * thm list) -> T
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    17
  val find: string list * string list -> T -> (string * thm list) list
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    18
end;
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    19
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    20
structure FactIndex: FACT_INDEX =
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    21
struct
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    22
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    23
(* indexing items *)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    24
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    25
fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    26
  | add_frees pred (t $ u, xs) = add_frees pred (t, add_frees pred (u, xs))
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    27
  | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    28
  | add_frees _ (_, xs) = xs;
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    29
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    30
fun index_term pred ((cs, xs), t) =
13542
bb3e8a86d610 thms_containing: allow "_" in specification;
wenzelm
parents: 13283
diff changeset
    31
  (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    32
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    33
fun index_thm pred (idx, th) =
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    34
  let val {hyps, prop, ...} = Thm.rep_thm th
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    35
  in foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    36
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    37
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    38
(* build index *)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    39
13283
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    40
datatype T = Index of {next: int, facts: (string * thm list) list,
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    41
  consts: (int * (string * thm list)) list Symtab.table,
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    42
  frees: (int * (string * thm list)) list Symtab.table};
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    43
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    44
val empty =
13283
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    45
  Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    46
13283
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    47
fun add pred (Index {next, facts, consts, frees}, (name, ths)) =
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    48
  let
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    49
    fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    50
    val (cs, xs) = foldl (index_thm pred) (([], []), ths);
13283
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    51
  in
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    52
    Index {next = next + 1, facts = (name, ths) :: facts,
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    53
      consts = foldl upd (consts, cs), frees = foldl upd (frees, xs)}
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    54
  end;
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    55
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    56
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    57
(* find facts *)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    58
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    59
fun intersect ([], _) = []
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    60
  | intersect (_, []) = []
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    61
  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    62
      if i = j then x :: intersect (xs, ys)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    63
      else if i > j then intersect (xs, yys)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    64
      else intersect (xxs, ys);
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    65
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    66
fun intersects [xs] = xs
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    67
  | intersects xss = if exists null xss then [] else foldl intersect (hd xss, tl xss);
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    68
13283
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    69
fun find ([], []) (Index {facts, ...}) = facts
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    70
  | find (cs, xs) (Index {consts, frees, ...}) =
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    71
      (map (curry Symtab.lookup_multi consts) cs @
1051aa66cbf3 proper treatment of border cases;
wenzelm
parents: 13270
diff changeset
    72
        map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    73
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    74
end;