equal
deleted
inserted
replaced
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
9 val last2: 'a list -> 'a * 'a |
9 val last2: 'a list -> 'a * 'a |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
12 val partitions: 'a list -> int list -> 'a list list |
12 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
13 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
13 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
|
14 |
14 |
15 |
15 val is_true: term -> bool |
16 val is_true: term -> bool |
16 |
17 |
17 val dest_listT: typ -> typ |
18 val dest_listT: typ -> typ |
18 val dest_fsetT: typ -> typ |
19 val dest_fsetT: typ -> typ |
136 fun last2 [] = raise Empty |
137 fun last2 [] = raise Empty |
137 | last2 [_] = raise Empty |
138 | last2 [_] = raise Empty |
138 | last2 [x, y] = (x, y) |
139 | last2 [x, y] = (x, y) |
139 | last2 (_ :: xs) = last2 xs |
140 | last2 (_ :: xs) = last2 xs |
140 |
141 |
141 (* partitions a set according to the numbers in the int list *) |
142 fun map4 _ [] [] [] [] = [] |
142 fun partitions [] [] = [] |
143 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
143 | partitions xs (i :: js) = |
|
144 let |
|
145 val (head, tail) = chop i xs |
|
146 in |
|
147 head :: partitions tail js |
|
148 end |
|
149 |
144 |
150 fun split_filter f [] = ([], []) |
145 fun split_filter f [] = ([], []) |
151 | split_filter f (x :: xs) = |
146 | split_filter f (x :: xs) = |
152 let |
147 let |
153 val (r, l) = split_filter f xs |
148 val (r, l) = split_filter f xs |