equal
deleted
inserted
replaced
54 in if idx > 0 then rmove idx list else list end; |
54 in if idx > 0 then rmove idx list else list end; |
55 |
55 |
56 |
56 |
57 (* lists as sets *) |
57 (* lists as sets *) |
58 |
58 |
59 nonfix subset; |
|
60 fun subset ord (list1, list2) = |
59 fun subset ord (list1, list2) = |
61 let |
60 let |
62 fun sub [] _ = true |
61 fun sub [] _ = true |
63 | sub _ [] = false |
62 | sub _ [] = false |
64 | sub (lst1 as x :: xs) (y :: ys) = |
63 | sub (lst1 as x :: xs) (y :: ys) = |
73 |
72 |
74 exception SAME; |
73 exception SAME; |
75 fun handle_same f x = f x handle SAME => x; |
74 fun handle_same f x = f x handle SAME => x; |
76 |
75 |
77 (*union: insert elements of first list into second list*) |
76 (*union: insert elements of first list into second list*) |
78 nonfix union; |
|
79 fun union ord list1 list2 = |
77 fun union ord list1 list2 = |
80 let |
78 let |
81 fun unio [] _ = raise SAME |
79 fun unio [] _ = raise SAME |
82 | unio xs [] = xs |
80 | unio xs [] = xs |
83 | unio (lst1 as x :: xs) (lst2 as y :: ys) = |
81 | unio (lst1 as x :: xs) (lst2 as y :: ys) = |
86 | EQUAL => y :: unio xs ys |
84 | EQUAL => y :: unio xs ys |
87 | GREATER => y :: unio lst1 ys); |
85 | GREATER => y :: unio lst1 ys); |
88 in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end; |
86 in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end; |
89 |
87 |
90 (*intersection: filter second list for elements present in first list*) |
88 (*intersection: filter second list for elements present in first list*) |
91 nonfix inter; |
|
92 fun inter ord list1 list2 = |
89 fun inter ord list1 list2 = |
93 let |
90 let |
94 fun intr _ [] = raise SAME |
91 fun intr _ [] = raise SAME |
95 | intr [] _ = [] |
92 | intr [] _ = [] |
96 | intr (lst1 as x :: xs) (lst2 as y :: ys) = |
93 | intr (lst1 as x :: xs) (lst2 as y :: ys) = |