src/Pure/Isar/net_rules.ML
author wenzelm
Mon Oct 15 20:33:05 2001 +0200 (2001-10-15 ago)
changeset 11776 d4f9de0bde28
parent 11693 63b0b2ec5830
child 12290 29b1a4ef4d9f
permissions -rw-r--r--
support weight;
wenzelm@8298
     1
(*  Title:      Pure/Isar/net_rules.ML
wenzelm@8298
     2
    ID:         $Id$
wenzelm@8298
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@8298
     5
wenzelm@8298
     6
Efficient storage of rules: preserves order, prefers later entries.
wenzelm@8298
     7
*)
wenzelm@8298
     8
wenzelm@8298
     9
signature NET_RULES =
wenzelm@8298
    10
sig
wenzelm@8298
    11
  type 'a T
wenzelm@8298
    12
  val rules: 'a T -> 'a list
wenzelm@11776
    13
  val retrieve: 'a T -> term -> 'a list
wenzelm@11776
    14
  val retrieve_weighted: 'a T -> term -> 'a list
wenzelm@11776
    15
  val init: ('a * 'a -> bool) -> ('a -> int) -> ('a -> term) -> 'a T
wenzelm@8298
    16
  val merge: 'a T * 'a T -> 'a T
wenzelm@8298
    17
  val delete: 'a -> 'a T -> 'a T
wenzelm@8298
    18
  val insert: 'a -> 'a T -> 'a T
wenzelm@8298
    19
  val deletes: 'a list -> 'a T -> 'a T
wenzelm@8298
    20
  val inserts: 'a list -> 'a T -> 'a T
wenzelm@11776
    21
  val intro: thm T
wenzelm@11776
    22
  val elim: thm T
wenzelm@8298
    23
end;
wenzelm@8298
    24
wenzelm@8298
    25
structure NetRules: NET_RULES =
wenzelm@8298
    26
struct
wenzelm@8298
    27
wenzelm@8298
    28
(* datatype rules *)
wenzelm@8298
    29
wenzelm@8298
    30
datatype 'a T =
wenzelm@8298
    31
  Rules of {
wenzelm@8298
    32
    eq: 'a * 'a -> bool,
wenzelm@11776
    33
    weight: 'a -> int,
wenzelm@8298
    34
    index: 'a -> term,
wenzelm@8298
    35
    rules: 'a list,
wenzelm@8298
    36
    next: int,
wenzelm@11776
    37
    net: ((int * int) * 'a) Net.net};
wenzelm@8298
    38
wenzelm@11776
    39
fun mk_rules eq weight index rules next net =
wenzelm@11776
    40
  Rules {eq = eq, weight = weight, index = index, rules = rules, next = next, net = net};
wenzelm@8298
    41
wenzelm@8298
    42
fun rules (Rules {rules = rs, ...}) = rs;
wenzelm@11776
    43
wenzelm@11776
    44
wenzelm@11776
    45
(* retrieve rules *)
wenzelm@11776
    46
wenzelm@11776
    47
fun gen_retrieve order (Rules {rules, net, ...}) tm =
wenzelm@11776
    48
  Tactic.untaglist (map (fn ((_, k), x) => (k, x))
wenzelm@11776
    49
    (sort (order o pairself #1) (Net.unify_term net tm)));
wenzelm@11776
    50
wenzelm@11776
    51
fun retrieve x = gen_retrieve (int_ord o pairself snd) x;
wenzelm@11776
    52
fun retrieve_weighted x = gen_retrieve (prod_ord int_ord int_ord) x;
wenzelm@8298
    53
wenzelm@8298
    54
wenzelm@8298
    55
(* build rules *)
wenzelm@8298
    56
wenzelm@11776
    57
fun init eq weight index = mk_rules eq weight index [] ~1 Net.empty;
wenzelm@8298
    58
wenzelm@11776
    59
fun add rule (Rules {eq, weight, index, rules, next, net}) =
wenzelm@11776
    60
  mk_rules eq weight index (rule :: rules) (next - 1)
wenzelm@11776
    61
    (Net.insert_term ((index rule, ((weight rule, next), rule)), net, K false));
wenzelm@8298
    62
wenzelm@11776
    63
fun make eq weight index rules = foldr (uncurry add) (rules, init eq weight index);
wenzelm@8298
    64
wenzelm@8298
    65
wenzelm@11776
    66
fun merge (Rules {eq, weight, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
wenzelm@11776
    67
  make eq weight index (Library.generic_merge eq I I rules1 rules2);
wenzelm@8298
    68
wenzelm@11776
    69
fun delete rule (rs as Rules {eq, weight, index, rules, next, net}) =
wenzelm@8298
    70
  if not (Library.gen_mem eq (rule, rules)) then rs
wenzelm@11776
    71
  else mk_rules eq weight index (Library.gen_rem eq (rules, rule)) next
wenzelm@11776
    72
    (Net.delete_term ((index rule, ((0, 0), rule)), net, eq o pairself #2));
wenzelm@8298
    73
wenzelm@8298
    74
fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
wenzelm@8298
    75
wenzelm@8298
    76
fun deletes rules rs = foldr (uncurry delete) (rules, rs);
wenzelm@8298
    77
fun inserts rules rs = foldr (uncurry insert) (rules, rs);
wenzelm@8298
    78
wenzelm@8298
    79
wenzelm@8298
    80
(* intro/elim rules *)
wenzelm@8298
    81
wenzelm@11776
    82
val intro = init Thm.eq_thm Thm.nprems_of Thm.concl_of;
wenzelm@11776
    83
val elim = init Thm.eq_thm Thm.nprems_of Thm.major_prem_of;
wenzelm@8298
    84
wenzelm@8298
    85
wenzelm@8298
    86
end;