<> <> <> <> <> Intervals: CEDAR DEFINITIONS = BEGIN Interval: TYPE = RECORD [min, max: INT]; <> <> Table: TYPE = REF TableRec; TableRec: TYPE = MONITORED RECORD [ range: Interval, -- given at creation time, it retains the range of all intervals. Clients should not change this field. size: NAT, -- maintained by all operations. Clients should not change this field. valueInterval: ValueIntervalProc, -- user-given function to access the interval corresponding to a value. Should be fast to compute. Clients should not change this field. userData: REF, -- user field. effectiveRange: PRIVATE Interval, -- effective range of current values. Use EffectiveRange to read that field (that may not be correct) leafBuckets: PRIVATE NAT, -- private field to detect when ReHashing is necessary. data: PRIVATE REF TableData ]; TableData: PRIVATE TYPE = RECORD [c: SEQUENCE hashSize: NAT OF LIST OF Value]; Value: TYPE = REF; ValueIntervalProc: TYPE = PROC [Table, Value] RETURNS [Interval]; Create: PROC [range: Interval, valueInterval: ValueIntervalProc, userData: REF _ NIL, logHashSize: NAT _ 2] RETURNS [Table]; <> Insert: PROC [table: Table, value: Value]; <> <> <> <> Delete: PROC [table: Table, value: Value]; <> <> <> Enumerate: PROC [table: Table, action: PROC [Table, Value] RETURNS [BOOLEAN _ FALSE], interval: Interval _ universe] RETURNS [BOOLEAN]; <> <> <> <> <> universe: Interval = [FIRST[INT], LAST[INT]]; empty: Interval = [LAST[INT], FIRST[INT]]; EffectiveRange: PROC [table: Table] RETURNS [Interval]; <> <<>> Union: PROC [interval1, interval2: Interval] RETURNS [Interval]; <> Overlap: PROC [interval1, interval2: Interval] RETURNS [BOOL]; <> <<>> END.