src/Pure/Isar/net_rules.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/Isar/net_rules.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Efficient storage of rules: preserves order, prefers later entries.
     5 *)
     6 
     7 signature NET_RULES =
     8 sig
     9   type 'a T
    10   val rules: 'a T -> 'a list
    11   val retrieve: 'a T -> term -> 'a list
    12   val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    13   val merge: 'a T * 'a T -> 'a T
    14   val delete: 'a -> 'a T -> 'a T
    15   val insert: 'a -> 'a T -> 'a T
    16   val intro: thm T
    17   val elim: thm T
    18 end;
    19 
    20 structure NetRules: NET_RULES =
    21 struct
    22 
    23 (* datatype rules *)
    24 
    25 datatype 'a T =
    26   Rules of {
    27     eq: 'a * 'a -> bool,
    28     index: 'a -> term,
    29     rules: 'a list,
    30     next: int,
    31     net: (int * 'a) Net.net};
    32 
    33 fun mk_rules eq index rules next net =
    34   Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    35 
    36 fun rules (Rules {rules = rs, ...}) = rs;
    37 
    38 fun retrieve (Rules {rules, net, ...}) tm =
    39   Tactic.untaglist 
    40      ((Library.sort (int_ord o pairself #1) (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 (K false) (index rule, (next, rule)) net);
    50 
    51 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    52   let val rules = Library.merge eq (rules1, rules2)
    53   in fold_rev add rules (init eq index) end;
    54 
    55 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    56   if not (member eq rules rule) then rs
    57   else mk_rules eq index (remove eq rule rules) next
    58     (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
    59 
    60 fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
    61 
    62 
    63 (* intro/elim rules *)
    64 
    65 val intro = init Thm.eq_thm_prop Thm.concl_of;
    66 val elim = init Thm.eq_thm_prop Thm.major_prem_of;
    67 
    68 
    69 end;