src/Pure/Isar/net_rules.ML
changeset 12385 389d11fb62c8
parent 12290 29b1a4ef4d9f
child 13105 3d1e7a199bdc
     1.1 --- a/src/Pure/Isar/net_rules.ML	Wed Dec 05 03:17:34 2001 +0100
     1.2 +++ b/src/Pure/Isar/net_rules.ML	Wed Dec 05 03:18:03 2001 +0100
     1.3 @@ -11,13 +11,10 @@
     1.4    type 'a T
     1.5    val rules: 'a T -> 'a list
     1.6    val retrieve: 'a T -> term -> 'a list
     1.7 -  val retrieve_weighted: 'a T -> term -> 'a list
     1.8 -  val init: ('a * 'a -> bool) -> ('a -> int) -> ('a -> term) -> 'a T
     1.9 +  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    1.10    val merge: 'a T * 'a T -> 'a T
    1.11    val delete: 'a -> 'a T -> 'a T
    1.12    val insert: 'a -> 'a T -> 'a T
    1.13 -  val deletes: 'a list -> 'a T -> 'a T
    1.14 -  val inserts: 'a list -> 'a T -> 'a T
    1.15    val intro: thm T
    1.16    val elim: thm T
    1.17  end;
    1.18 @@ -30,57 +27,44 @@
    1.19  datatype 'a T =
    1.20    Rules of {
    1.21      eq: 'a * 'a -> bool,
    1.22 -    weight: 'a -> int,
    1.23      index: 'a -> term,
    1.24      rules: 'a list,
    1.25      next: int,
    1.26 -    net: ((int * int) * 'a) Net.net};
    1.27 +    net: (int * 'a) Net.net};
    1.28  
    1.29 -fun mk_rules eq weight index rules next net =
    1.30 -  Rules {eq = eq, weight = weight, index = index, rules = rules, next = next, net = net};
    1.31 +fun mk_rules eq index rules next net =
    1.32 +  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    1.33  
    1.34  fun rules (Rules {rules = rs, ...}) = rs;
    1.35  
    1.36 -
    1.37 -(* retrieve rules *)
    1.38 -
    1.39 -fun gen_retrieve order (Rules {rules, net, ...}) tm =
    1.40 -  Tactic.untaglist (map (fn ((_, k), x) => (k, x))
    1.41 -    (sort (order o pairself #1) (Net.unify_term net tm)));
    1.42 -
    1.43 -fun retrieve x = gen_retrieve (int_ord o pairself snd) x;
    1.44 -fun retrieve_weighted x = gen_retrieve (prod_ord int_ord int_ord) x;
    1.45 +fun retrieve (Rules {rules, net, ...}) tm =
    1.46 +  Tactic.untaglist ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
    1.47  
    1.48  
    1.49  (* build rules *)
    1.50  
    1.51 -fun init eq weight index = mk_rules eq weight index [] ~1 Net.empty;
    1.52 +fun init eq index = mk_rules eq index [] ~1 Net.empty;
    1.53  
    1.54 -fun add rule (Rules {eq, weight, index, rules, next, net}) =
    1.55 -  mk_rules eq weight index (rule :: rules) (next - 1)
    1.56 -    (Net.insert_term ((index rule, ((weight rule, next), rule)), net, K false));
    1.57 -
    1.58 -fun make eq weight index rules = foldr (uncurry add) (rules, init eq weight index);
    1.59 -
    1.60 +fun add rule (Rules {eq, index, rules, next, net}) =
    1.61 +  mk_rules eq index (rule :: rules) (next - 1)
    1.62 +    (Net.insert_term ((index rule, (next, rule)), net, K false));
    1.63  
    1.64 -fun merge (Rules {eq, weight, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    1.65 -  make eq weight index (Library.gen_merge_lists' eq rules1 rules2);
    1.66 +fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    1.67 +  let val rules = Library.gen_merge_lists' eq rules1 rules2
    1.68 +  in foldr (uncurry add) (rules, init eq index) end;
    1.69  
    1.70 -fun delete rule (rs as Rules {eq, weight, index, rules, next, net}) =
    1.71 +fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    1.72    if not (Library.gen_mem eq (rule, rules)) then rs
    1.73 -  else mk_rules eq weight index (Library.gen_rem eq (rules, rule)) next
    1.74 -    (Net.delete_term ((index rule, ((0, 0), rule)), net, eq o pairself #2));
    1.75 +  else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
    1.76 +    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
    1.77  
    1.78 -fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
    1.79 -
    1.80 -fun deletes rules rs = foldr (uncurry delete) (rules, rs);
    1.81 -fun inserts rules rs = foldr (uncurry insert) (rules, rs);
    1.82 +fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
    1.83  
    1.84  
    1.85  (* intro/elim rules *)
    1.86  
    1.87 -val intro = init Thm.eq_thm Thm.nprems_of Thm.concl_of;
    1.88 -val elim = init Thm.eq_thm Thm.nprems_of Thm.major_prem_of;
    1.89 +val intro = init Thm.eq_thm Thm.concl_of;
    1.90 +val elim = init Thm.eq_thm Thm.major_prem_of;
    1.91  
    1.92  
    1.93  end;