added dest and merge operations;
authorwenzelm
Tue Jul 22 17:47:20 1997 +0200 (1997-07-22)
changeset 3548108d09eb3454
parent 3547 977d58464d7f
child 3549 e8c8d76810a6
added dest and merge operations;
src/Pure/net.ML
     1.1 --- a/src/Pure/net.ML	Tue Jul 22 17:46:35 1997 +0200
     1.2 +++ b/src/Pure/net.ML	Tue Jul 22 17:47:20 1997 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4    val match_term: 'a net -> term -> 'a list
     1.5    val key_of_term: term -> key list
     1.6    val unify_term: 'a net -> term -> 'a list
     1.7 +  val dest: 'a net -> (key list * 'a) list
     1.8 +  val merge: 'a net * 'a net * ('a*'a -> bool) -> 'a net
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -215,4 +217,26 @@
    1.13  fun unify_term net t = 
    1.14      extract_leaves (matching true t (net,[]));
    1.15  
    1.16 +
    1.17 +(** dest **)
    1.18 +
    1.19 +fun cons_fst x (xs, y) = (x :: xs, y);
    1.20 +val cons_fsts = map o cons_fst;
    1.21 +
    1.22 +fun dest (Leaf xs) = map (pair []) xs
    1.23 +  | dest (Net {comb, var, alist}) =
    1.24 +      cons_fsts CombK (dest comb) @
    1.25 +      cons_fsts VarK (dest var) @
    1.26 +      flat (map (fn (a, net) => cons_fsts (AtomK a) (dest net)) alist);
    1.27 +
    1.28 +
    1.29 +(** merge **)
    1.30 +
    1.31 +fun add eq (net, keys_x) =
    1.32 +  insert (keys_x, net, eq) handle INSERT => net;
    1.33 +
    1.34 +fun merge (net1, net2, eq) =
    1.35 +  foldl (add eq) (net1, dest net2);
    1.36 +
    1.37 +
    1.38  end;