support weight;
authorwenzelm
Mon Oct 15 20:33:05 2001 +0200 (2001-10-15)
changeset 11776d4f9de0bde28
parent 11775 e7eeca372b7c
child 11777 b03c8a3fcc6d
support weight;
src/Pure/Isar/net_rules.ML
     1.1 --- a/src/Pure/Isar/net_rules.ML	Mon Oct 15 20:32:13 2001 +0200
     1.2 +++ b/src/Pure/Isar/net_rules.ML	Mon Oct 15 20:33:05 2001 +0200
     1.3 @@ -10,15 +10,16 @@
     1.4  sig
     1.5    type 'a T
     1.6    val rules: 'a T -> 'a list
     1.7 -  val may_unify: 'a T -> term -> 'a list
     1.8 -  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
     1.9 +  val retrieve: 'a T -> term -> 'a list
    1.10 +  val retrieve_weighted: 'a T -> term -> 'a list
    1.11 +  val init: ('a * 'a -> bool) -> ('a -> int) -> ('a -> term) -> 'a T
    1.12    val merge: 'a T * 'a T -> 'a T
    1.13    val delete: 'a -> 'a T -> 'a T
    1.14    val insert: 'a -> 'a T -> 'a T
    1.15    val deletes: 'a list -> 'a T -> 'a T
    1.16    val inserts: 'a list -> 'a T -> 'a T
    1.17 -  val init_intro: thm T
    1.18 -  val init_elim: thm T
    1.19 +  val intro: thm T
    1.20 +  val elim: thm T
    1.21  end;
    1.22  
    1.23  structure NetRules: NET_RULES =
    1.24 @@ -29,36 +30,46 @@
    1.25  datatype 'a T =
    1.26    Rules of {
    1.27      eq: 'a * 'a -> bool,
    1.28 +    weight: 'a -> int,
    1.29      index: 'a -> term,
    1.30      rules: 'a list,
    1.31      next: int,
    1.32 -    net: (int * 'a) Net.net};
    1.33 +    net: ((int * int) * 'a) Net.net};
    1.34  
    1.35 -fun mk_rules eq index rules next net =
    1.36 -  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    1.37 +fun mk_rules eq weight index rules next net =
    1.38 +  Rules {eq = eq, weight = weight, index = index, rules = rules, next = next, net = net};
    1.39  
    1.40  fun rules (Rules {rules = rs, ...}) = rs;
    1.41 -fun may_unify (Rules {rules, net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
    1.42 +
    1.43 +
    1.44 +(* retrieve rules *)
    1.45 +
    1.46 +fun gen_retrieve order (Rules {rules, net, ...}) tm =
    1.47 +  Tactic.untaglist (map (fn ((_, k), x) => (k, x))
    1.48 +    (sort (order o pairself #1) (Net.unify_term net tm)));
    1.49 +
    1.50 +fun retrieve x = gen_retrieve (int_ord o pairself snd) x;
    1.51 +fun retrieve_weighted x = gen_retrieve (prod_ord int_ord int_ord) x;
    1.52  
    1.53  
    1.54  (* build rules *)
    1.55  
    1.56 -fun init eq index = mk_rules eq index [] ~1 Net.empty;
    1.57 +fun init eq weight index = mk_rules eq weight index [] ~1 Net.empty;
    1.58  
    1.59 -fun add rule (Rules {eq, index, rules, next, net}) =
    1.60 -  mk_rules eq index (rule :: rules) (next - 1)
    1.61 -    (Net.insert_term ((index rule, (next, rule)), net, K false));
    1.62 +fun add rule (Rules {eq, weight, index, rules, next, net}) =
    1.63 +  mk_rules eq weight index (rule :: rules) (next - 1)
    1.64 +    (Net.insert_term ((index rule, ((weight rule, next), rule)), net, K false));
    1.65  
    1.66 -fun make eq index rules = foldr (uncurry add) (rules, init eq index);
    1.67 +fun make eq weight index rules = foldr (uncurry add) (rules, init eq weight index);
    1.68  
    1.69  
    1.70 -fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    1.71 -  make eq index (Library.generic_merge eq I I rules1 rules2);
    1.72 +fun merge (Rules {eq, weight, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    1.73 +  make eq weight index (Library.generic_merge eq I I rules1 rules2);
    1.74  
    1.75 -fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    1.76 +fun delete rule (rs as Rules {eq, weight, index, rules, next, net}) =
    1.77    if not (Library.gen_mem eq (rule, rules)) then rs
    1.78 -  else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
    1.79 -    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
    1.80 +  else mk_rules eq weight index (Library.gen_rem eq (rules, rule)) next
    1.81 +    (Net.delete_term ((index rule, ((0, 0), rule)), net, eq o pairself #2));
    1.82  
    1.83  fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
    1.84  
    1.85 @@ -68,8 +79,8 @@
    1.86  
    1.87  (* intro/elim rules *)
    1.88  
    1.89 -val init_intro = init Thm.eq_thm Thm.concl_of;
    1.90 -val init_elim = init Thm.eq_thm Thm.major_prem_of;
    1.91 +val intro = init Thm.eq_thm Thm.nprems_of Thm.concl_of;
    1.92 +val elim = init Thm.eq_thm Thm.nprems_of Thm.major_prem_of;
    1.93  
    1.94  
    1.95  end;