src/Pure/Isar/net_rules.ML
changeset 11776 d4f9de0bde28
parent 11693 63b0b2ec5830
child 12290 29b1a4ef4d9f
equal deleted inserted replaced
11775:e7eeca372b7c 11776:d4f9de0bde28
     8 
     8 
     9 signature NET_RULES =
     9 signature NET_RULES =
    10 sig
    10 sig
    11   type 'a T
    11   type 'a T
    12   val rules: 'a T -> 'a list
    12   val rules: 'a T -> 'a list
    13   val may_unify: 'a T -> term -> 'a list
    13   val retrieve: 'a T -> term -> 'a list
    14   val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    14   val retrieve_weighted: 'a T -> term -> 'a list
       
    15   val init: ('a * 'a -> bool) -> ('a -> int) -> ('a -> term) -> 'a T
    15   val merge: 'a T * 'a T -> 'a T
    16   val merge: 'a T * 'a T -> 'a T
    16   val delete: 'a -> 'a T -> 'a T
    17   val delete: 'a -> 'a T -> 'a T
    17   val insert: 'a -> 'a T -> 'a T
    18   val insert: 'a -> 'a T -> 'a T
    18   val deletes: 'a list -> 'a T -> 'a T
    19   val deletes: 'a list -> 'a T -> 'a T
    19   val inserts: 'a list -> 'a T -> 'a T
    20   val inserts: 'a list -> 'a T -> 'a T
    20   val init_intro: thm T
    21   val intro: thm T
    21   val init_elim: thm T
    22   val elim: thm T
    22 end;
    23 end;
    23 
    24 
    24 structure NetRules: NET_RULES =
    25 structure NetRules: NET_RULES =
    25 struct
    26 struct
    26 
    27 
    27 (* datatype rules *)
    28 (* datatype rules *)
    28 
    29 
    29 datatype 'a T =
    30 datatype 'a T =
    30   Rules of {
    31   Rules of {
    31     eq: 'a * 'a -> bool,
    32     eq: 'a * 'a -> bool,
       
    33     weight: 'a -> int,
    32     index: 'a -> term,
    34     index: 'a -> term,
    33     rules: 'a list,
    35     rules: 'a list,
    34     next: int,
    36     next: int,
    35     net: (int * 'a) Net.net};
    37     net: ((int * int) * 'a) Net.net};
    36 
    38 
    37 fun mk_rules eq index rules next net =
    39 fun mk_rules eq weight index rules next net =
    38   Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    40   Rules {eq = eq, weight = weight, index = index, rules = rules, next = next, net = net};
    39 
    41 
    40 fun rules (Rules {rules = rs, ...}) = rs;
    42 fun rules (Rules {rules = rs, ...}) = rs;
    41 fun may_unify (Rules {rules, net, ...}) tm = Tactic.orderlist (Net.unify_term net tm);
    43 
       
    44 
       
    45 (* retrieve rules *)
       
    46 
       
    47 fun gen_retrieve order (Rules {rules, net, ...}) tm =
       
    48   Tactic.untaglist (map (fn ((_, k), x) => (k, x))
       
    49     (sort (order o pairself #1) (Net.unify_term net tm)));
       
    50 
       
    51 fun retrieve x = gen_retrieve (int_ord o pairself snd) x;
       
    52 fun retrieve_weighted x = gen_retrieve (prod_ord int_ord int_ord) x;
    42 
    53 
    43 
    54 
    44 (* build rules *)
    55 (* build rules *)
    45 
    56 
    46 fun init eq index = mk_rules eq index [] ~1 Net.empty;
    57 fun init eq weight index = mk_rules eq weight index [] ~1 Net.empty;
    47 
    58 
    48 fun add rule (Rules {eq, index, rules, next, net}) =
    59 fun add rule (Rules {eq, weight, index, rules, next, net}) =
    49   mk_rules eq index (rule :: rules) (next - 1)
    60   mk_rules eq weight index (rule :: rules) (next - 1)
    50     (Net.insert_term ((index rule, (next, rule)), net, K false));
    61     (Net.insert_term ((index rule, ((weight rule, next), rule)), net, K false));
    51 
    62 
    52 fun make eq index rules = foldr (uncurry add) (rules, init eq index);
    63 fun make eq weight index rules = foldr (uncurry add) (rules, init eq weight index);
    53 
    64 
    54 
    65 
    55 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    66 fun merge (Rules {eq, weight, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    56   make eq index (Library.generic_merge eq I I rules1 rules2);
    67   make eq weight index (Library.generic_merge eq I I rules1 rules2);
    57 
    68 
    58 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    69 fun delete rule (rs as Rules {eq, weight, index, rules, next, net}) =
    59   if not (Library.gen_mem eq (rule, rules)) then rs
    70   if not (Library.gen_mem eq (rule, rules)) then rs
    60   else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
    71   else mk_rules eq weight index (Library.gen_rem eq (rules, rule)) next
    61     (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
    72     (Net.delete_term ((index rule, ((0, 0), rule)), net, eq o pairself #2));
    62 
    73 
    63 fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
    74 fun insert rule rs = add rule (delete rule rs);    (*ensure new rule gets precedence*)
    64 
    75 
    65 fun deletes rules rs = foldr (uncurry delete) (rules, rs);
    76 fun deletes rules rs = foldr (uncurry delete) (rules, rs);
    66 fun inserts rules rs = foldr (uncurry insert) (rules, rs);
    77 fun inserts rules rs = foldr (uncurry insert) (rules, rs);
    67 
    78 
    68 
    79 
    69 (* intro/elim rules *)
    80 (* intro/elim rules *)
    70 
    81 
    71 val init_intro = init Thm.eq_thm Thm.concl_of;
    82 val intro = init Thm.eq_thm Thm.nprems_of Thm.concl_of;
    72 val init_elim = init Thm.eq_thm Thm.major_prem_of;
    83 val elim = init Thm.eq_thm Thm.nprems_of Thm.major_prem_of;
    73 
    84 
    74 
    85 
    75 end;
    86 end;