<> <> <> SF: CEDAR DEFINITIONS ~ BEGIN <> Vec: TYPE ~ RECORD [s, f: INTEGER]; minVec: Vec ~ [s: INTEGER.FIRST, f: INTEGER.FIRST]; maxVec: Vec ~ [s: INTEGER.LAST, f: INTEGER.LAST]; zeroVec: Vec ~ [s: 0, f: 0]; NonNegative: PROC [v: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: NAT[v.s], f: NAT[v.f]]]; }; Add: PROC [v1, v2: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: v1.s+v2.s, f: v1.f+v2.f]]; }; Sub: PROC [v1, v2: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: v1.s-v2.s, f: v1.f-v2.f]]; }; Min: PROC [v1, v2: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: IF v1.s<=v2.s THEN v1.s ELSE v2.s, f: IF v1.f<=v2.f THEN v1.f ELSE v2.f]]; }; Min3: PROC [v1, v2, v3: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: MIN[v1.s, v2.s, v3.s], f: MIN[v1.f, v2.f, v3.f]]]; }; Max: PROC [v1, v2: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: IF v2.s>=v1.s THEN v2.s ELSE v1.s, f: IF v2.f>=v1.f THEN v2.f ELSE v1.f]]; }; Max3: PROC [v1, v2, v3: Vec] RETURNS [Vec] ~ INLINE { RETURN[[s: MAX[v1.s, v2.s, v3.s], f: MAX[v1.f, v2.f, v3.f]]]; }; Eq: PROC [v1, v2: Vec] RETURNS [BOOL] ~ INLINE { RETURN[v1.s=v2.s AND v1.f=v2.f]; }; Lt: PROC [v1, v2: Vec] RETURNS [BOOL] ~ INLINE { RETURN[v1.sv2.s OR v1.f>v2.f]; }; Ge: PROC [v1, v2: Vec] RETURNS [BOOL] ~ INLINE { RETURN[v1.s>=v2.s OR v1.f>=v2.f]; }; <> Box: TYPE ~ RECORD [min, max: Vec]; <> <<>> maxBox: Box ~ [min: minVec, max: maxVec]; BoxAction: TYPE ~ PROC [box: Box]; BoxGenerator: TYPE ~ PROC [boxAction: BoxAction]; <<>> Nonempty: PROC [box: Box] RETURNS [BOOL] ~ INLINE { RETURN[Lt[box.min, box.max]]; }; Empty: PROC [box: Box] RETURNS [BOOL] ~ INLINE { RETURN[Ge[box.min, box.max]]; }; Intersect: PROC [box1, box2: Box] RETURNS [Box] ~ INLINE { RETURN[[min: Max[box2.min, box1.min], max: Min[box1.max, box2.max]]]; }; Disjoint: PROC [box1, box2: Box] RETURNS [BOOL] ~ INLINE { RETURN[Le[box1.max, box2.min] OR Le[box2.max, box1.min]]; }; SizeF: PROC [box: Box] RETURNS [CARDINAL] ~ INLINE { RETURN[IF box.min.f