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; |
|