src/Pure/Isar/net_rules.ML
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 8635 2f699cd7b8d7
child 8807 0046be1769f9
permissions -rw-r--r--
apply etc.: comments;
     1 (*  Title:      Pure/Isar/net_rules.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Efficient storage of rules: preserves order, prefers later entries.
     6 *)
     7 
     8 signature NET_RULES =
     9 sig
    10   type 'a T
    11   val rules: 'a T -> 'a list
    12   val may_unify: 'a T -> term -> 'a list
    13   val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    14   val merge: 'a T * 'a T -> 'a T
    15   val delete: 'a -> 'a T -> 'a T
    16   val insert: 'a -> 'a T -> 'a T
    17   val deletes: 'a list -> 'a T -> 'a T
    18   val inserts: 'a list -> 'a T -> 'a T
    19   val init_intro: thm T
    20   val init_elim: thm T
    21 end;
    22 
    23 structure NetRules: NET_RULES =
    24 struct
    25 
    26 (* datatype rules *)
    27 
    28 datatype 'a T =
    29   Rules of {
    30     eq: 'a * 'a -> bool,
    31     index: 'a -> term,
    32     rules: 'a list,
    33     next: int,
    34     net: (int * 'a) Net.net};
    35 
    36 fun mk_rules eq index rules next net =
    37   Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    38 
    39 fun rules (Rules {rules = rs, ...}) = rs;
    40 fun may_unify (Rules {rules, net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
    41 
    42 
    43 (* build rules *)
    44 
    45 fun init eq index = mk_rules eq index [] ~1 Net.empty;
    46 
    47 fun add rule (Rules {eq, index, rules, next, net}) =
    48   mk_rules eq index (rule :: rules) (next - 1)
    49     (Net.insert_term ((index rule, (next, rule)), net, K false));
    50 
    51 fun make eq index rules = foldr (uncurry add) (rules, init eq index);
    52 
    53 
    54 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    55   make eq index (Library.generic_merge eq I I rules1 rules2);
    56 
    57 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    58   if not (Library.gen_mem eq (rule, rules)) then rs
    59   else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
    60     (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
    61 
    62 fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
    63 
    64 fun deletes rules rs = foldr (uncurry delete) (rules, rs);
    65 fun inserts rules rs = foldr (uncurry insert) (rules, rs);
    66 
    67 
    68 (* intro/elim rules *)
    69 
    70 val init_intro = init Thm.eq_thm Thm.concl_of;
    71 val init_elim = init Thm.eq_thm (Logic.strip_assums_concl o Thm.major_prem_of);
    72 
    73 
    74 end;