optimize special case according to Library.merge (see also 8fbc355100f2);
authorwenzelm
Tue Feb 25 12:53:08 2014 +0100 (2014-02-25)
changeset 55741b969263fcf02
parent 55740 11dd48f84441
child 55742 a989bdaf8121
optimize special case according to Library.merge (see also 8fbc355100f2);
no treatment for Net.merge, due to non-standard merge order;
src/Pure/item_net.ML
src/Pure/net.ML
     1.1 --- a/src/Pure/item_net.ML	Tue Feb 25 11:36:04 2014 +0100
     1.2 +++ b/src/Pure/item_net.ML	Tue Feb 25 12:53:08 2014 +0100
     1.3 @@ -54,8 +54,12 @@
     1.4    mk_items eq index (x :: content) (next - 1)
     1.5      (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
     1.6  
     1.7 -fun merge (items1, Items {content = content2, ...}) =
     1.8 -  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
     1.9 +fun merge
    1.10 +    (items1 as Items {net = net1, ...},
    1.11 +     items2 as Items {net = net2, content = content2, ...}) =
    1.12 +  if pointer_eq (net1, net2) then items1
    1.13 +  else if Net.is_empty net1 then items2
    1.14 +  else fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    1.15  
    1.16  fun remove x (items as Items {eq, index, content, next, net}) =
    1.17    if member items x then
     2.1 --- a/src/Pure/net.ML	Tue Feb 25 11:36:04 2014 +0100
     2.2 +++ b/src/Pure/net.ML	Tue Feb 25 12:53:08 2014 +0100
     2.3 @@ -20,6 +20,7 @@
     2.4    val encode_type: typ -> term
     2.5    type 'a net
     2.6    val empty: 'a net
     2.7 +  val is_empty: 'a net -> bool
     2.8    exception INSERT
     2.9    val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
    2.10    val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
    2.11 @@ -251,7 +252,8 @@
    2.12        map (cons_fst VarK) (dest var) @
    2.13        maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
    2.14  
    2.15 -fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
    2.16 +fun merge eq (net1, net2) =
    2.17 +  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-standard merge order!?! *)
    2.18  
    2.19  fun content net = map #2 (dest net);
    2.20