src/Pure/Isar/net_rules.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 12290 29b1a4ef4d9f
child 13105 3d1e7a199bdc
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/net_rules.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Efficient storage of rules: preserves order, prefers later entries.
     7 *)
     8 
     9 signature NET_RULES =
    10 sig
    11   type 'a T
    12   val rules: 'a T -> 'a list
    13   val retrieve: 'a T -> term -> 'a list
    14   val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    15   val merge: 'a T * 'a T -> 'a T
    16   val delete: 'a -> 'a T -> 'a T
    17   val insert: 'a -> 'a T -> 'a T
    18   val intro: thm T
    19   val elim: thm T
    20 end;
    21 
    22 structure NetRules: NET_RULES =
    23 struct
    24 
    25 (* datatype rules *)
    26 
    27 datatype 'a T =
    28   Rules of {
    29     eq: 'a * 'a -> bool,
    30     index: 'a -> term,
    31     rules: 'a list,
    32     next: int,
    33     net: (int * 'a) Net.net};
    34 
    35 fun mk_rules eq index rules next net =
    36   Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    37 
    38 fun rules (Rules {rules = rs, ...}) = rs;
    39 
    40 fun retrieve (Rules {rules, net, ...}) tm =
    41   Tactic.untaglist ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
    42 
    43 
    44 (* build rules *)
    45 
    46 fun init eq index = mk_rules eq index [] ~1 Net.empty;
    47 
    48 fun add rule (Rules {eq, index, rules, next, net}) =
    49   mk_rules eq index (rule :: rules) (next - 1)
    50     (Net.insert_term ((index rule, (next, rule)), net, K false));
    51 
    52 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    53   let val rules = Library.gen_merge_lists' eq rules1 rules2
    54   in foldr (uncurry add) (rules, init eq index) end;
    55 
    56 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    57   if not (Library.gen_mem eq (rule, rules)) then rs
    58   else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
    59     (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
    60 
    61 fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
    62 
    63 
    64 (* intro/elim rules *)
    65 
    66 val intro = init Thm.eq_thm Thm.concl_of;
    67 val elim = init Thm.eq_thm Thm.major_prem_of;
    68 
    69 
    70 end;