-
Notifications
You must be signed in to change notification settings - Fork 18
Description
Add a range datatype and structure. Its goal is to represent ranges like 'x > 0 andalso x < 10' and 'x = 5', and also sets of ranges.
It is based on Guava's Range and RangeSet types.
datatype 'a range =
POINT of 'a (*) POINT 5: x = 5
| AT_LEAST of 'a (*) AT_LEAST 5: x >= 5
| GREATER_THAN of 'a (*) GREATER_THAN 5: x > 5
| AT_MOST of 'a (*) AT_MOST 5: x <= 5
| LESS_THAN 'a (*) LESS_THAN 5: x < 5
| CLOSED of 'a * a (*) CLOSED (5, 10): x > 5 andalso x < 10
| OPEN of 'a * 'a (*) OPEN (5, 10): x >= 5 andalso x <= 10
| CLOSED_OPEN of 'a * 'a (*) CLOSED_OPEN (5, 10): x > 5 andalso x <= 10
| OPEN_CLOSED of 'a * 'a; (*) OPEN_CLOSED (5, 10): x >= 5 andalso x < 10The type 'a' may be any ordered type, including sum types (datatype), records, string, listandbag`.
There should be a method to normalize a list of ranges (sort, and merge adjacent ranges). If the type is discrete adjacent points can be merged into a range, and closed bounds can be converted into open bounds.
There should also be a to_list method to convert a list of ranges to a list of values. It fails if type 'a is not discrete or the range is infinite. For these purposes int that is not bounded above or below is infinite, but boolean, char, unit and sum types over finite types are finite.
We should replace uses of List.tabulate and Bag.tabulate in generated code Range.to_list. For example, List.tabulate (6, fn i => i + 5) generates [5,6,7,8,9,10] : int list. We should instead use Range.to_list [OPEN (5, 10)].