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