src/Pure/fact_index.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18026 ccf2972f6f89
child 18931 427df66052a1
permissions -rw-r--r--
simplified type attribute;
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
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
     5
Facts indexed by consts or frees.
13270
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
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    10
  type spec
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    11
  type T
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    12
  val facts: T -> (string * thm list) list
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    13
  val could_unify: T -> term -> thm list
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    14
  val empty: T
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    15
  val add_global: (string * thm list) -> T -> T
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    16
  val add_local: (string -> bool) -> (string * thm list) -> T -> T
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    17
  val find: T -> spec -> (string * thm list) list
13270
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
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    23
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    24
(* indexing items *)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    25
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    26
type spec = string list * string list;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    27
16874
wenzelm
parents: 16491
diff changeset
    28
val add_consts = fold_aterms
wenzelm
parents: 16491
diff changeset
    29
  (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    30
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    31
fun add_frees known = fold_aterms
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    32
  (fn Free (x, _) => if known x then insert (op =) x else I | _ => I);
16874
wenzelm
parents: 16491
diff changeset
    33
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    34
fun index_term known t (cs, xs) = (add_consts t cs, add_frees known t xs);
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    35
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    36
fun index_thm known th idx =
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    37
  let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    38
    idx
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    39
    |> index_term known prop
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    40
    |> fold (index_term known) hyps
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    41
    |> fold (fn (t, u) => index_term known t #> index_term known u) tpairs
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    42
  end;
13270
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
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    45
(* build index *)
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    46
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    47
type fact = string * thm list;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    48
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    49
datatype T = Index of
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    50
 {facts: fact list,
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    51
  consts: (serial * fact) list Symtab.table,
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    52
  frees: (serial * fact) list Symtab.table,
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    53
  props: thm Net.net};
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    54
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    55
fun facts (Index {facts, ...}) = facts;
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    56
fun could_unify (Index {props, ...}) = Net.unify_term props;
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    57
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    58
val empty =
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    59
  Index {facts = [], consts = Symtab.empty, frees = Symtab.empty, props = Net.empty};
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    60
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    61
fun add do_props known (fact as (_, ths)) (Index {facts, consts, frees, props}) =
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    62
  let
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    63
    val entry = (serial (), fact);
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    64
    val (cs, xs) = fold (index_thm known) ths ([], []);
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    65
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    66
    val facts' = fact :: facts;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    67
    val consts' = consts |> fold (fn c => Symtab.update_multi (c, entry)) cs;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    68
    val frees' = frees |> fold (fn x => Symtab.update_multi (x, entry)) xs;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    69
    val props' = props |> K do_props ?
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    70
      fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    71
  in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    72
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    73
val add_global = add false (K false);
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    74
val add_local = add true;
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    75
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    76
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    77
(* find by consts/frees *)
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    78
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    79
local
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    80
16491
7310d0a36599 OrdList.inter;
wenzelm
parents: 16020
diff changeset
    81
fun fact_ord ((i, _), (j, _)) = int_ord (j, i);
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    82
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    83
fun intersects [xs] = xs
16491
7310d0a36599 OrdList.inter;
wenzelm
parents: 16020
diff changeset
    84
  | intersects xss =
7310d0a36599 OrdList.inter;
wenzelm
parents: 16020
diff changeset
    85
      if exists null xss then []
7310d0a36599 OrdList.inter;
wenzelm
parents: 16020
diff changeset
    86
      else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    87
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    88
in
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    89
16020
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    90
fun find idx ([], []) = facts idx
ace2c610b5be major tuning;
wenzelm
parents: 15570
diff changeset
    91
  | find (Index {consts, frees, ...}) (cs, xs) =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    92
      (map (Symtab.lookup_multi consts) cs @
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    93
        map (Symtab.lookup_multi frees) xs) |> intersects |> map #2;
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    94
18026
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    95
end
ccf2972f6f89 added add_local/add_global;
wenzelm
parents: 17412
diff changeset
    96
13270
d7f35250cbad Facts indexed by consts or (some) frees.
wenzelm
parents:
diff changeset
    97
end;