added gen_merge_lists(') and merge_lists(');
authorwenzelm
Sat Nov 24 16:55:56 2001 +0100 (2001-11-24)
changeset 12284131e743d168a
parent 12283 d42aa776889e
child 12285 6490fc7b3eed
added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Nov 24 16:55:00 2001 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Nov 24 16:55:56 2001 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/library.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Author:	Markus Wenzel, TU Munich
     1.8 +    Author:     Markus Wenzel, TU Munich
     1.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11  Basic library: functions, options, pairs, booleans, lists, integers,
    1.12 @@ -211,14 +211,12 @@
    1.13    val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    1.14    val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
    1.15  
    1.16 -  (*generic tables*)
    1.17 -  val generic_extend: ('a * 'a -> bool)
    1.18 -    -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'a list -> 'b
    1.19 -  val generic_merge: ('a * 'a -> bool) -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'b -> 'b
    1.20 -  val extend_list: ''a list -> ''a list -> ''a list
    1.21 +  (*lists as tables*)
    1.22 +  val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.23 +  val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.24    val merge_lists: ''a list -> ''a list -> ''a list
    1.25 +  val merge_lists': ''a list -> ''a list -> ''a list
    1.26    val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    1.27 -  val merge_rev_lists: ''a list -> ''a list -> ''a list
    1.28  
    1.29    (*balanced trees*)
    1.30    exception Balance
    1.31 @@ -880,9 +878,9 @@
    1.32  
    1.33  (*generalized intersection*)
    1.34  fun gen_inter eq ([], ys) = []
    1.35 -  | gen_inter eq (x::xs, ys) = 
    1.36 +  | gen_inter eq (x::xs, ys) =
    1.37        if gen_mem eq (x,ys) then x :: gen_inter eq (xs, ys)
    1.38 -	                   else      gen_inter eq (xs, ys);
    1.39 +                           else      gen_inter eq (xs, ys);
    1.40  
    1.41  
    1.42  (*subset*)
    1.43 @@ -1013,46 +1011,19 @@
    1.44    in over al end;
    1.45  
    1.46  
    1.47 -
    1.48 -(** generic tables **)
    1.49 -
    1.50 -(*Tables are supposed to be 'efficient' encodings of lists of elements distinct
    1.51 -  wrt. an equality "eq". The extend and merge operations below are optimized
    1.52 -  for long-term space efficiency.*)
    1.53 +(* lists as tables *)
    1.54  
    1.55 -(*append (new) elements to a table*)
    1.56 -fun generic_extend _ _ _ tab [] = tab
    1.57 -  | generic_extend eq dest_tab mk_tab tab1 lst2 =
    1.58 -      let
    1.59 -        val lst1 = dest_tab tab1;
    1.60 -        val new_lst2 = gen_rems eq (lst2, lst1);
    1.61 -      in
    1.62 -        if null new_lst2 then tab1
    1.63 -        else mk_tab (lst1 @ new_lst2)
    1.64 -      end;
    1.65 +fun gen_merge_lists _ xs [] = xs
    1.66 +  | gen_merge_lists _ [] ys = ys
    1.67 +  | gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
    1.68  
    1.69 -(*append (new) elements of 2nd table to 1st table*)
    1.70 -fun generic_merge eq dest_tab mk_tab tab1 tab2 =
    1.71 -  let
    1.72 -    val lst1 = dest_tab tab1;
    1.73 -    val lst2 = dest_tab tab2;
    1.74 -    val new_lst2 = gen_rems eq (lst2, lst1);
    1.75 -  in
    1.76 -    if null new_lst2 then tab1
    1.77 -    else if gen_subset eq (lst1, lst2) then tab2
    1.78 -    else mk_tab (lst1 @ new_lst2)
    1.79 -  end;
    1.80 +fun gen_merge_lists' _ xs [] = xs
    1.81 +  | gen_merge_lists' _ [] ys = ys
    1.82 +  | gen_merge_lists' eq xs ys = gen_rems eq (xs, ys) @ ys;
    1.83  
    1.84 -
    1.85 -(*lists as tables*)
    1.86 -fun extend_list tab = generic_extend (op =) I I tab;
    1.87 -fun merge_lists tab = generic_merge (op =) I I tab;
    1.88 -fun merge_alists tab = generic_merge eq_fst I I tab;
    1.89 -
    1.90 -fun merge_rev_lists xs [] = xs
    1.91 -  | merge_rev_lists [] ys = ys
    1.92 -  | merge_rev_lists xs (y :: ys) =
    1.93 -      (if y mem xs then I else cons y) (merge_rev_lists xs ys);
    1.94 +fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
    1.95 +fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;
    1.96 +fun merge_alists al = gen_merge_lists eq_fst al;
    1.97  
    1.98  
    1.99