src/Pure/fact_index.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 21648 c8a0370c9b93
child 25389 3e58c7cb5a73
permissions -rw-r--r--
Name.uu, Name.aT;
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@13270
    11
  type T
wenzelm@16020
    12
  val facts: T -> (string * thm list) list
wenzelm@20010
    13
  val props: T -> thm list
wenzelm@18026
    14
  val could_unify: T -> term -> thm list
wenzelm@13270
    15
  val empty: T
wenzelm@21648
    16
  val add_local: bool -> bool -> (string * thm list) -> T -> T
wenzelm@18026
    17
  val add_global: (string * thm list) -> T -> T
wenzelm@16020
    18
  val find: T -> spec -> (string * thm list) list
wenzelm@13270
    19
end;
wenzelm@13270
    20
wenzelm@13270
    21
structure FactIndex: FACT_INDEX =
wenzelm@13270
    22
struct
wenzelm@13270
    23
wenzelm@16020
    24
wenzelm@13270
    25
(* indexing items *)
wenzelm@13270
    26
wenzelm@18026
    27
type spec = string list * string list;
wenzelm@18026
    28
wenzelm@16874
    29
val add_consts = fold_aterms
wenzelm@16874
    30
  (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
wenzelm@13270
    31
wenzelm@20156
    32
val add_frees = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
wenzelm@16874
    33
wenzelm@20156
    34
fun index_term t (cs, xs) = (add_consts t cs, add_frees t xs);
wenzelm@13270
    35
wenzelm@20156
    36
fun index_thm th =
wenzelm@16020
    37
  let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
wenzelm@20156
    38
    index_term prop
wenzelm@20156
    39
    #> fold index_term hyps
wenzelm@20156
    40
    #> fold (fn (t, u) => index_term t #> index_term u) tpairs
wenzelm@16020
    41
  end;
wenzelm@13270
    42
wenzelm@13270
    43
wenzelm@13270
    44
(* build index *)
wenzelm@13270
    45
wenzelm@18026
    46
type fact = string * thm list;
wenzelm@18026
    47
wenzelm@18026
    48
datatype T = Index of
wenzelm@18026
    49
 {facts: fact list,
wenzelm@18026
    50
  consts: (serial * fact) list Symtab.table,
wenzelm@18026
    51
  frees: (serial * fact) list Symtab.table,
wenzelm@18026
    52
  props: thm Net.net};
wenzelm@13270
    53
wenzelm@16020
    54
fun facts (Index {facts, ...}) = facts;
wenzelm@20010
    55
fun props (Index {props, ...}) =
wenzelm@20010
    56
  sort_distinct (Term.term_ord o pairself Thm.full_prop_of) (Net.content props);
wenzelm@18026
    57
fun could_unify (Index {props, ...}) = Net.unify_term props;
wenzelm@16020
    58
wenzelm@13270
    59
val empty =
wenzelm@18026
    60
  Index {facts = [], consts = Symtab.empty, frees = Symtab.empty, props = Net.empty};
wenzelm@13270
    61
wenzelm@21648
    62
fun add_local do_props do_index (fact as (_, ths)) (Index {facts, consts, frees, props}) =
wenzelm@13270
    63
  let
wenzelm@18026
    64
    val entry = (serial (), fact);
wenzelm@20156
    65
    val (cs, xs) = fold index_thm ths ([], []);
wenzelm@18026
    66
wenzelm@19141
    67
    val (facts', consts', frees') =
wenzelm@19141
    68
      if do_index then
wenzelm@19141
    69
       (fact :: facts,
wenzelm@19141
    70
        consts |> fold (fn c => Symtab.update_list (c, entry)) cs,
wenzelm@19141
    71
        frees |> fold (fn x => Symtab.update_list (x, entry)) xs)
wenzelm@19141
    72
      else (facts, consts, frees);
wenzelm@19141
    73
    val props' =
wenzelm@19141
    74
      if do_props then props |> fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths
wenzelm@19141
    75
      else props;
wenzelm@18026
    76
  in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
wenzelm@18026
    77
wenzelm@21648
    78
val add_global = add_local false true;
wenzelm@13270
    79
wenzelm@13270
    80
wenzelm@18026
    81
(* find by consts/frees *)
wenzelm@18026
    82
wenzelm@18026
    83
local
wenzelm@13270
    84
wenzelm@16491
    85
fun fact_ord ((i, _), (j, _)) = int_ord (j, i);
wenzelm@13270
    86
wenzelm@13270
    87
fun intersects [xs] = xs
wenzelm@16491
    88
  | intersects xss =
wenzelm@16491
    89
      if exists null xss then []
wenzelm@16491
    90
      else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
wenzelm@13270
    91
wenzelm@18026
    92
in
wenzelm@18026
    93
wenzelm@16020
    94
fun find idx ([], []) = facts idx
wenzelm@16020
    95
  | find (Index {consts, frees, ...}) (cs, xs) =
wenzelm@18931
    96
      (map (Symtab.lookup_list consts) cs @
wenzelm@18931
    97
        map (Symtab.lookup_list frees) xs) |> intersects |> map #2;
wenzelm@13270
    98
wenzelm@18026
    99
end
wenzelm@18026
   100
wenzelm@13270
   101
end;