src/Pure/Isar/net_rules.ML
author wenzelm
Sun Feb 27 15:07:53 2000 +0100 (2000-02-27)
changeset 8298 9b089bc07f69
child 8635 2f699cd7b8d7
permissions -rw-r--r--
added Isar/net_rules.ML;
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@8298
    12
  val may_unify: 'a T -> term -> 'a list
wenzelm@8298
    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@8298
    17
  val deletes: 'a list -> 'a T -> 'a T
wenzelm@8298
    18
  val inserts: 'a list -> 'a T -> 'a T
wenzelm@8298
    19
  val init_intro: thm T
wenzelm@8298
    20
  val init_elim: thm T
wenzelm@8298
    21
end;
wenzelm@8298
    22
wenzelm@8298
    23
structure NetRules: NET_RULES =
wenzelm@8298
    24
struct
wenzelm@8298
    25
wenzelm@8298
    26
(* datatype rules *)
wenzelm@8298
    27
wenzelm@8298
    28
datatype 'a T =
wenzelm@8298
    29
  Rules of {
wenzelm@8298
    30
    eq: 'a * 'a -> bool,
wenzelm@8298
    31
    index: 'a -> term,
wenzelm@8298
    32
    rules: 'a list,
wenzelm@8298
    33
    next: int,
wenzelm@8298
    34
    net: (int * 'a) Net.net};
wenzelm@8298
    35
wenzelm@8298
    36
fun mk_rules eq index rules next net =
wenzelm@8298
    37
  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
wenzelm@8298
    38
wenzelm@8298
    39
fun rules (Rules {rules = rs, ...}) = rs;
wenzelm@8298
    40
fun may_unify (Rules {net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
wenzelm@8298
    41
wenzelm@8298
    42
wenzelm@8298
    43
(* build rules *)
wenzelm@8298
    44
wenzelm@8298
    45
fun init eq index = mk_rules eq index [] ~1 Net.empty;
wenzelm@8298
    46
wenzelm@8298
    47
fun add rule (Rules {eq, index, rules, next, net}) =
wenzelm@8298
    48
  mk_rules eq index (rule :: rules) (next - 1)
wenzelm@8298
    49
    (Net.insert_term ((index rule, (next, rule)), net, K false));
wenzelm@8298
    50
wenzelm@8298
    51
fun make eq index rules = foldr (uncurry add) (rules, init eq index);
wenzelm@8298
    52
wenzelm@8298
    53
wenzelm@8298
    54
fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
wenzelm@8298
    55
  make eq index (Library.generic_merge eq I I rules1 rules2);
wenzelm@8298
    56
wenzelm@8298
    57
fun delete rule (rs as Rules {eq, index, rules, next, net}) =
wenzelm@8298
    58
  if not (Library.gen_mem eq (rule, rules)) then rs
wenzelm@8298
    59
  else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
wenzelm@8298
    60
    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
wenzelm@8298
    61
wenzelm@8298
    62
fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
wenzelm@8298
    63
wenzelm@8298
    64
fun deletes rules rs = foldr (uncurry delete) (rules, rs);
wenzelm@8298
    65
fun inserts rules rs = foldr (uncurry insert) (rules, rs);
wenzelm@8298
    66
wenzelm@8298
    67
wenzelm@8298
    68
(* intro/elim rules *)
wenzelm@8298
    69
wenzelm@8298
    70
val init_intro = init Thm.eq_thm Thm.concl_of;
wenzelm@8298
    71
val init_elim = init Thm.eq_thm Thm.major_prem_of;
wenzelm@8298
    72
wenzelm@8298
    73
wenzelm@8298
    74
end;