src/Pure/Isar/net_rules.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 18921 f47c46d7d654
child 22360 26ead7ed4f4b
permissions -rw-r--r--
Attrib.internal: morphism;
wenzelm@8298
     1
(*  Title:      Pure/Isar/net_rules.ML
wenzelm@8298
     2
    ID:         $Id$
wenzelm@8298
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8298
     4
wenzelm@8298
     5
Efficient storage of rules: preserves order, prefers later entries.
wenzelm@8298
     6
*)
wenzelm@8298
     7
wenzelm@8298
     8
signature NET_RULES =
wenzelm@8298
     9
sig
wenzelm@8298
    10
  type 'a T
wenzelm@8298
    11
  val rules: 'a T -> 'a list
wenzelm@11776
    12
  val retrieve: 'a T -> term -> 'a list
wenzelm@12385
    13
  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
wenzelm@8298
    14
  val merge: 'a T * 'a T -> 'a T
wenzelm@8298
    15
  val delete: 'a -> 'a T -> 'a T
wenzelm@8298
    16
  val insert: 'a -> 'a T -> 'a T
wenzelm@11776
    17
  val intro: thm T
wenzelm@11776
    18
  val elim: thm T
wenzelm@8298
    19
end;
wenzelm@8298
    20
wenzelm@8298
    21
structure NetRules: NET_RULES =
wenzelm@8298
    22
struct
wenzelm@8298
    23
wenzelm@8298
    24
(* datatype rules *)
wenzelm@8298
    25
wenzelm@8298
    26
datatype 'a T =
wenzelm@8298
    27
  Rules of {
wenzelm@8298
    28
    eq: 'a * 'a -> bool,
wenzelm@8298
    29
    index: 'a -> term,
wenzelm@8298
    30
    rules: 'a list,
wenzelm@8298
    31
    next: int,
wenzelm@12385
    32
    net: (int * 'a) Net.net};
wenzelm@8298
    33
wenzelm@12385
    34
fun mk_rules eq index rules next net =
wenzelm@12385
    35
  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
wenzelm@8298
    36
wenzelm@8298
    37
fun rules (Rules {rules = rs, ...}) = rs;
wenzelm@11776
    38
wenzelm@12385
    39
fun retrieve (Rules {rules, net, ...}) tm =
paulson@14472
    40
  Tactic.untaglist 
wenzelm@16512
    41
     ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
wenzelm@8298
    42
wenzelm@8298
    43
wenzelm@8298
    44
(* build rules *)
wenzelm@8298
    45
wenzelm@12385
    46
fun init eq index = mk_rules eq index [] ~1 Net.empty;
wenzelm@8298
    47
wenzelm@12385
    48
fun add rule (Rules {eq, index, rules, next, net}) =
wenzelm@12385
    49
  mk_rules eq index (rule :: rules) (next - 1)
wenzelm@16800
    50
    (Net.insert_term (K false) (index rule, (next, rule)) net);
wenzelm@8298
    51
wenzelm@12385
    52
fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
wenzelm@18921
    53
  let val rules = Library.merge eq (rules1, rules2)
wenzelm@17351
    54
  in fold_rev add rules (init eq index) end;
wenzelm@8298
    55
wenzelm@12385
    56
fun delete rule (rs as Rules {eq, index, rules, next, net}) =
wenzelm@18646
    57
  if not (member eq rules rule) then rs
wenzelm@18646
    58
  else mk_rules eq index (remove eq rule rules) next
wenzelm@16800
    59
    (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
wenzelm@8298
    60
wenzelm@12385
    61
fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
wenzelm@8298
    62
wenzelm@8298
    63
wenzelm@8298
    64
(* intro/elim rules *)
wenzelm@8298
    65
wenzelm@13105
    66
val intro = init Drule.eq_thm_prop Thm.concl_of;
wenzelm@13105
    67
val elim = init Drule.eq_thm_prop Thm.major_prem_of;
wenzelm@8298
    68
wenzelm@8298
    69
wenzelm@8298
    70
end;