DIRECTORY AbSets, IntStuff, SetBasics; BiRelBasics: CEDAR DEFINITIONS IMPORTS AbSets, SetBasics = {OPEN IntStuff, SetBasics, Sets:AbSets, Sets; Pair: TYPE ~ ARRAY Side OF Value; noPair: Pair ~ [noValue, noValue]; Cons: PROC [s1: Side, v1, v2: Value] RETURNS [Pair] ~ TRUSTED 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: 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 NoingPair; NoingPair: TYPE ~ Pair _ noPair; 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]; 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] b, OPPOSITE => NOT b, FALSE => FALSE, TRUE => TRUE, ENDCASE => ERROR]}; ConstRel: ARRAY BOOL OF RelBool ~ [FALSE: FALSE, TRUE: TRUE]; }. ͺBiRelBasics.Mesa Last tweaked by Mike Spreitzer on December 14, 1987 12:18:39 pm PST Pairs (general 2-tuples) Swap [left] and [right]. Maybes Being Had When adding a pair to, or removing a pair from, a variable BiRel that is Functional[dir], the resultant HadPair[dir] tells about the previous state of that variable: none means there was previously no pair with equivalent [Source[dir]]; different means there was a pair with equivalent [Source[dir]] and non-equivalent [Dest[dir]]; same means there was previously an equivalent pair. If the BiRel is not Functional[dir], the resultant HadPair[dir] can be anything. The procedures that add to variable BiRels can be conditional on the previous state: if the BiRel is Functional[dir], if[dir][had[dir]=none] must be TRUE in order for the addition to happen. Other Interesting 2-tuples PairIntervals Relative Orders An RelOrder specifies a partial ordering among pairs, relative to the orderings of a SpacePair. It's a lexicographic composition of the relative orders on components given by sub, with the indicated first side being more significant. Note that when one of the Sets.RelOrders is no, first is irrelevant. Note also that for a BiRel that is Functional[][From[first]], sub[OtherSide[first]] is irrelevant. Just what it says: a RelOrder that is total. Another way to say it is: neither of sub's elements is `no'. result.sub[result.first]=no => result.sub = ALL[no] functional[From[ro.first]] => result.sub[OtherSide[ro.first]]=no True iff (forall a, b: a ˜N—K˜šž œœœ ˜2Kšœœœ%˜5—K˜šžœœœ ˜;Kšœœœ%˜5—K˜šžœœœ ˜8Kšœœœ%˜5——™Kš œ œœœ œœ˜0K˜šžœœœ ˜5Kšœœœ%˜5—K˜Kšœ œœœ˜&K˜šžœœœœ˜9Kšœœœ&œ*˜c—K˜šžœœœ ˜8Kšœœœ˜(—K˜Kšœœ˜K˜Kšœ œœœ ˜)Kšœ œœœ˜1K˜šžœœœ ˜=šœœœ˜Kšœ&˜&Kšœ-˜-——K˜šœ œœœ ˜)Kšœ œ˜ —K˜šžœœ)œ ˜HKšœœœœ˜B—K˜šžœœœ ˜9Kšœœœ8˜H—K˜šž œœœ ˜2Kšœœœ˜(——™ šœœœœ ˜,Kšœ œ˜ —K˜šžœœ œ ˜>Kšœœœ-˜=—K˜šžœœœ˜5Kšœœœ!˜1——™Kšœ œœœ˜Jš œœœœœ˜8Kš œ°ŸœŸœKŸœŸœ4ŸœŸœ™”—K˜šœœ ˜Kšœj™j—K˜Kšœ&˜&Kšœ&˜&Kšœ(˜(Kšœ(˜(K˜šž œœ-œ ˜QKšœœœ$œ˜N—K˜šž œœ-œ˜VKšœœœœ˜H—K˜šžœœ&œ ˜OK™3K™@—K˜Kšž œœœ ˜2K˜šžœœœ ˜6Kšœœœ9˜I—K˜šž œœ1œ˜]šœœ˜ Kšœb˜bKšœ œœ˜K˜ K˜7Kšœ˜ ——K˜šž œœ1œ ˜Ušœœ˜ KšœZ˜ZKšœ œœ˜K˜ K˜6Kšœ˜ ——K˜šžœœœœ˜5K™7šœœ˜ Kšœœœœ˜2Kš œœ1œœœ˜bK˜(Kšœ&œ˜H——K˜šžœœœ˜