16464

1 
(* Title: Pure/General/ord_list.ML


2 
ID: $Id$


3 
Author: Makarius


4 


5 
Ordered lists without duplicates  a lightweight representation of

16497

6 
finite sets, all operations take linear time and economize heap usage.

16464

7 
*)


8 


9 
signature ORD_LIST =


10 
sig


11 
val member: ('b * 'a > order) > 'a list > 'b > bool


12 
val insert: ('a * 'a > order) > 'a > 'a list > 'a list


13 
val remove: ('b * 'a > order) > 'b > 'a list > 'a list

16511

14 
val subset: ('b * 'a > order) > 'b list * 'a list > bool

16464

15 
val union: ('a * 'a > order) > 'a list > 'a list > 'a list

16497

16 
val inter: ('b * 'a > order) > 'b list > 'a list > 'a list


17 
val subtract: ('b * 'a > order) > 'b list > 'a list > 'a list

16464

18 
end;


19 


20 
structure OrdList: ORD_LIST =


21 
struct


22 

16511

23 


24 
(* single elements *)


25 


26 
fun find_index ord list x =


27 
let

16811

28 
fun find i [] = ~ i

16511

29 
 find i (y :: ys) =


30 
(case ord (x, y) of

16811

31 
LESS => ~ i

16511

32 
 EQUAL => i


33 
 GREATER => find (i + 1) ys);

16811

34 
in find 1 list end;

16497

35 

16811

36 
fun member ord list x = find_index ord list x > 0;

16464

37 


38 
fun insert ord x list =


39 
let

16811

40 
fun insrt 1 ys = x :: ys

16511

41 
 insrt i (y :: ys) = y :: insrt (i  1) ys;

16811

42 
val idx = find_index ord list x;


43 
in if idx > 0 then list else insrt (~ idx) list end;

16464

44 


45 
fun remove ord x list =


46 
let

16811

47 
fun rmove 1 (_ :: ys) = ys

16511

48 
 rmove i (y :: ys) = y :: rmove (i  1) ys;

16811

49 
val idx = find_index ord list x;


50 
in if idx > 0 then rmove idx list else list end;

16511

51 


52 


53 
(* lists as sets *)


54 


55 
nonfix subset;


56 
fun subset ord (list1, list2) =


57 
let


58 
fun sub [] _ = true


59 
 sub _ [] = false


60 
 sub (lst1 as x :: xs) (y :: ys) =

16464

61 
(case ord (x, y) of

16511

62 
LESS => false


63 
 EQUAL => sub xs ys


64 
 GREATER => sub lst1 ys);


65 
in sub list1 list2 end;


66 


67 


68 
(* algebraic operations *)


69 


70 
exception SAME;


71 
fun handle_same f x = f x handle SAME => x;

16464

72 

16497

73 
(*union: insert elements of first list into second list*)

16464

74 
nonfix union;

16497

75 
fun union ord list1 list2 =


76 
let


77 
fun unio [] _ = raise SAME


78 
 unio xs [] = xs


79 
 unio (lst1 as x :: xs) (lst2 as y :: ys) =


80 
(case ord (x, y) of


81 
LESS => x :: handle_same (unio xs) lst2


82 
 EQUAL => y :: unio xs ys


83 
 GREATER => y :: unio lst1 ys);

16886

84 
in handle_same (unio list1) list2 end;

16464

85 

16497

86 
(*intersection: filter second list for elements present in first list*)

16464

87 
nonfix inter;

16497

88 
fun inter ord list1 list2 =


89 
let


90 
fun intr _ [] = raise SAME


91 
 intr [] _ = []


92 
 intr (lst1 as x :: xs) (lst2 as y :: ys) =


93 
(case ord (x, y) of


94 
LESS => intr xs lst2


95 
 EQUAL => y :: intr xs ys


96 
 GREATER => handle_same (intr lst1) ys);


97 
in handle_same (intr list1) list2 end;


98 


99 
(*subtraction: filter second list for elements NOT present in first list*)


100 
fun subtract ord list1 list2 =


101 
let


102 
fun subtr [] _ = raise SAME


103 
 subtr _ [] = raise SAME


104 
 subtr (lst1 as x :: xs) (lst2 as y :: ys) =


105 
(case ord (x, y) of


106 
LESS => subtr xs lst2


107 
 EQUAL => handle_same (subtr xs) ys


108 
 GREATER => y :: subtr lst1 ys);


109 
in handle_same (subtr list1) list2 end;

16464

110 


111 
end;
