<> <> DIRECTORY AbSets, IntStuff, SetBasics; BiRelBasics: CEDAR DEFINITIONS IMPORTS AbSets, SetBasics = {OPEN IntStuff, SetBasics, Sets:AbSets, Sets; <> Pair: TYPE ~ ARRAY Side OF Value; noPair: READONLY Pair -- = [noValue, noValue]--; Cons: PROC [s1: Side, v1, v2: Value] RETURNS [Pair] ~ INLINE {p: Pair _ ALL[v2]; p[s1] _ v1; RETURN [p]}; InvertPair: PROC [x: Pair] RETURNS [Pair] <> ~ INLINE {RETURN [[x[right], x[left]]]}; <> MaybePair: TYPE ~ RECORD [found: BOOL, it: Pair]; noMaybePair: READONLY MaybePair -- = [FALSE, noPair]--; KeepHalf: PROC [mp: MaybePair, side: Side] RETURNS [MaybeValue] ~ INLINE {RETURN [[mp.found, mp.it[side]]]}; P: PROC [mp: MaybePair] RETURNS [Pair] ~ INLINE {IF mp.found THEN RETURN [mp.it] ELSE Error[notFound, NIL]}; DP: PROC [mp: MaybePair, ifNotFound: Pair] RETURNS [Pair] ~ INLINE {RETURN [IF mp.found THEN mp.it ELSE ifNotFound]}; InvertMaybe: PROC [mp: MaybePair] RETURNS [MaybePair] ~ INLINE {RETURN [[mp.found, InvertPair[mp.it]]]}; TripleMaybePair: TYPE ~ RECORD [prev, same, next: MaybePair]; MaybePairInterval: TYPE ~ RECORD [found: BOOL, it: PairInterval]; MPISide: PROC [mpi: MaybePairInterval, side: Side] RETURNS [MaybeInterval] ~ INLINE {RETURN [[mpi.found, PISide[mpi.it, side]]]}; RevMPI: PROC [mpi: MaybePairInterval] RETURNS [MaybePairInterval] ~ INLINE {RETURN [[mpi.found, [min: mpi.it[max], max: mpi.it[min]]]]}; MaybePairSpace: TYPE ~ RECORD [found: BOOL, it: PairSpace]; <> Had: TYPE ~ {same, different, none}; HadPair: TYPE ~ PACKED ARRAY Direction OF Had; HadSet: TYPE ~ PACKED ARRAY Had OF BOOL _ ALL[FALSE]; HadSetPair: TYPE ~ ARRAY Direction OF HadSet _ ALL[ALL[FALSE]]; <> IfHad: TYPE ~ PACKED ARRAY --had=none--BOOL OF --add:--BOOL; IfHadPair: TYPE ~ ARRAY Direction OF IfHad; <> alwaysAdd: IfHadPair ~ ALL[ALL[TRUE]]; addIfNew: IfHadPair ~ ALL[[FALSE, TRUE]]; addIfOld: IfHadPair ~ ALL[[TRUE, FALSE]]; UnSetHad: PROC [hs: HadSet] RETURNS [Had] ~ INLINE {RETURN [SELECT TRUE FROM hs[none] => none, hs[different] => different, ENDCASE => same]}; UnSetHads: PROC [hsp: HadSetPair] RETURNS [HadPair] ~ INLINE {RETURN [[UnSetHad[hsp[leftToRight]], UnSetHad[hsp[rightToLeft]] ]]}; InvertHadPair: PROC [x: HadPair] RETURNS [HadPair] ~ INLINE {RETURN [[x[rightToLeft], x[leftToRight]]]}; InvertHadSetPair: PROC [x: HadSetPair] RETURNS [HadSetPair] ~ INLINE {RETURN [[x[rightToLeft], x[leftToRight]]]}; InvertIfHadPair: PROC [x: IfHadPair] RETURNS [IfHadPair] ~ INLINE {RETURN [[x[rightToLeft], x[leftToRight]]]}; <> BoolPair: TYPE ~ PACKED ARRAY Direction OF BOOL; InvertBoolPair: PROC [x: BoolPair] RETURNS [BoolPair] ~ INLINE {RETURN [[x[rightToLeft], x[leftToRight]]]}; SpacePair: TYPE ~ ARRAY Side OF Space; PEqual: PROC [sp: SpacePair, p1, p2: Pair] RETURNS [BOOL] ~ INLINE {RETURN [sp[left].SEqual[p1[left], p2[left]] AND sp[right].SEqual[p1[right], p2[right]]]}; InvertSpacePair: PROC [x: SpacePair] RETURNS [SpacePair] ~ INLINE {RETURN [[x[right], x[left]]]}; refSpacePairs: READONLY Space; ComPair: TYPE ~ ARRAY Side OF Comparison; PComPair: TYPE ~ ARRAY Side OF PartialComparison; Compair: PROC [sp: SpacePair, p1, p2: Pair] RETURNS [ComPair] ~ INLINE {RETURN [[ sp[left].SCompare[p1[left], p2[left]], sp[right].SCompare[p1[right], p2[right]] ]]}; SetPair: TYPE ~ ARRAY Side OF NillingSet; NillingSet: TYPE ~ Set _ nilSet; ConsSets: PROC [side1: Side, set1, set2: Set _ nilSet] RETURNS [SetPair] ~ INLINE {sp: SetPair _ ALL[set2]; sp[side1] _ set1; RETURN [sp]}; CreateFullSetPair: PROC [sp: SpacePair] RETURNS [SetPair] ~ INLINE {RETURN [[CreateFullSet[sp[left]], CreateFullSet[sp[right]]]]}; InvertSetPair: PROC [x: SetPair] RETURNS [SetPair] ~ INLINE {RETURN [[x[right], x[left]]]}; <> PairInterval: TYPE ~ ARRAY End OF Pair; PISide: PROC [pi: PairInterval, side: Side] RETURNS [Interval] ~ INLINE {RETURN [[min: pi[min][side], max: pi[max][side]]]}; RevPI: PROC [pi: PairInterval] RETURNS [PairInterval] ~ INLINE {RETURN [[min: pi[max], max: pi[min]]]}; <> RelOrder: TYPE ~ RECORD [sub: SubOrderPair _ ALL[no], first: Side _ left]; SubOrderPair: TYPE ~ PACKED ARRAY Side OF Sets.RelOrder; <> TotalRelOrder: TYPE ~ RelOrder; <> leftFwd: RelOrder ~ [[fwd, no], left]; leftBwd: RelOrder ~ [[bwd, no], left]; rightFwd: RelOrder ~ [[no, fwd], right]; rightBwd: RelOrder ~ [[no, bwd], right]; ConsRelOrder: PROC [side1: Side, ro1, ro2: Sets.RelOrder _ no] RETURNS [RelOrder] ~ INLINE {ro: RelOrder _ [ALL[ro2], side1]; ro.sub[side1] _ ro1; RETURN [ro]}; ConsRelOrders: PROC [side1: Side, ro1, ro2: Sets.RelOrder _ no] RETURNS [SubOrderPair] ~ INLINE {sop: SubOrderPair _ ALL[ro2]; sop[side1] _ ro1; RETURN [sop]}; CanonizeRelOrder: PROC [ro: RelOrder, functional: BoolPair] RETURNS [RelOrder]; < result.sub = ALL[no]>> < result.sub[OtherSide[ro.first]]=no>> ReverseRO: PROC [ro: RelOrder] RETURNS [RelOrder]; InvertRelOrder: PROC [ro: RelOrder] RETURNS [RelOrder] ~ INLINE {RETURN [[[ro.sub[right], ro.sub[left]], OtherSide[ro.first]]]}; RelPCompare: PROC [ro: RelOrder, spaces: SpacePair, p1, p2: Pair] RETURNS [PartialComparison] ~ INLINE { c: PartialComparison _ ro.sub[ro.first].RelPCompare[spaces[ro.first], p1[ro.first], p2[ro.first]]; IF c # equal THEN RETURN [c]; {ss: Side ~ OtherSide[ro.first]; c _ ro.sub[ss].RelPCompare[spaces[ss], p1[ss], p2[ss]]; RETURN [c]}}; RelCompare: PROC [ro: RelOrder, spaces: SpacePair, p1, p2: Pair] RETURNS [Comparison] ~ INLINE { c: Comparison _ ro.sub[ro.first].RelCompare[spaces[ro.first], p1[ro.first], p2[ro.first]]; IF c # equal THEN RETURN [c]; {ss: Side ~ OtherSide[ro.first]; c _ ro.sub[ss].RelCompare[spaces[ss], p1[ss], p2[ss]]; RETURN [c]}}; Coarser: PROC [coarse, fine: RelOrder] RETURNS [BOOL] <> ~ INLINE { IF coarse.sub[coarse.first]=no THEN RETURN [TRUE]; IF coarse.first#fine.first OR coarse.sub[coarse.first]#fine.sub[coarse.first] THEN RETURN [FALSE]; {second: Side ~ OtherSide[coarse.first]; RETURN [coarse.sub[second]=fine.sub[second] OR coarse.sub[second]=no]}}; RODivide: PROC [num, den: RelOrder] RETURNS [Sets.RelOrder]; <> RMin: PROC [ro: RelOrder, spaces: SpacePair, p1, p2: Pair] RETURNS [Pair] ~ INLINE {RETURN [IF RelCompare[ro, spaces, p1, p2]>equal THEN p2 ELSE p1]}; RMax: PROC [ro: RelOrder, spaces: SpacePair, p1, p2: Pair] RETURNS [Pair] ~ INLINE {RETURN [IF RelCompare[ro, spaces, p1, p2]> PairSpace: TYPE ~ RECORD [sp: SpacePair, tro: TotalRelOrder]; <> WidenPairSpace: PROC [PairSpace] RETURNS [s: Space]; IsPairSpace: PROC [s: Space] RETURNS [BOOL] <> ~ INLINE {RETURN [QuaPairSpace[s].found]}; AsPairSpace: PROC [s: Space] RETURNS [PairSpace] <> ~ INLINE {RETURN [QuaPairSpace[s].it]}; QuaPairSpace: PROC [s: Space] RETURNS [MaybePairSpace]; <> RelBool: TYPE ~ {SAME, OPPOSITE, FALSE, TRUE}; <> RelativizeBool: PROC [rb: RelBool, b: BOOL] RETURNS [BOOL] ~ INLINE {RETURN [SELECT rb FROM SAME => b, OPPOSITE => NOT b, FALSE => FALSE, TRUE => TRUE, ENDCASE => ERROR]}; ConstRel: ARRAY BOOL OF RelBool ~ [FALSE: FALSE, TRUE: TRUE]; }.