src/Pure/Isar/net_rules.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 18921 f47c46d7d654
child 22360 26ead7ed4f4b
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     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 retrieve: '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 intro: thm T
    18   val elim: thm T
    19 end;
    20 
    21 structure NetRules: NET_RULES =
    22 struct
    23 
    24 (* datatype rules *)
    25 
    26 datatype 'a T =
    27   Rules of {
    28     eq: 'a * 'a -> bool,
    29     index: 'a -> term,
    30     rules: 'a list,
    31     next: int,
    32     net: (int * 'a) Net.net};
    33 
    34 fun mk_rules eq index rules next net =
    35   Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    36 
    37 fun rules (Rules {rules = rs, ...}) = rs;
    38 
    39 fun retrieve (Rules {rules, net, ...}) tm =
    40   Tactic.untaglist 
    41      ((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 (K false) (index rule, (next, rule)) net);
    51 
    52 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    53   let val rules = Library.merge eq (rules1, rules2)
    54   in fold_rev add rules (init eq index) end;
    55 
    56 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    57   if not (member eq rules rule) then rs
    58   else mk_rules eq index (remove eq rule rules) next
    59     (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
    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 Drule.eq_thm_prop Thm.concl_of;
    67 val elim = init Drule.eq_thm_prop Thm.major_prem_of;
    68 
    69 
    70 end;