Maybes
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];
Being Had
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]];
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.
IfHad: TYPE ~ PACKED ARRAY --had=none--BOOL OF --add:--BOOL;
IfHadPair:
TYPE ~
ARRAY Direction
OF IfHad;
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.
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]]]};
Other Interesting 2-tuples
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]]]};
Relative Orders
RelOrder: TYPE ~ RECORD [sub: SubOrderPair ← ALL[no], first: Side ← left];
SubOrderPair:
TYPE ~
PACKED
ARRAY Side
OF Sets.RelOrder;
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.
TotalRelOrder:
TYPE ~ RelOrder;
Just what it says: a RelOrder that is total. Another way to say it is: neither of sub's elements is `no'.
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[result.first]=no => result.sub = ALL[no]
functional[From[ro.first]] => 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]
True iff (forall a, b: a <coarse= b implies a <fine= b)
~
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];
result=fwd implies Coarser[num, den]; result=bwd implies Coarser[num, den.Reverse]; result=no implies NOT (Coarser[num, den] OR Coarser[num, den.Reverse]).
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]<equal THEN p2 ELSE p1]};
ROCompair:
PROC [ro: RelOrder, cp: ComPair]
RETURNS [PartialComparison]
~
INLINE {
IF cp[ro.first]#equal THEN RETURN ro.sub[ro.first].RelativizeComparison[cp[ro.first]];
{second: Side ~ OtherSide[ro.first];
RETURN ro.sub[second].RelativizeComparison[cp[second]]}};
LexizeComPair:
PROC [cp: ComPair, first: Side]
RETURNS [Comparison]
~ INLINE {RETURN [IF cp[first]#equal THEN cp[first] ELSE cp[OtherSide[first]]]};
RelativizeComPair:
PROC [sop: SubOrderPair, cp: ComPair]
RETURNS [PComPair]
~
INLINE {
RETURN [[
sop[left].RelativizeComparison[cp[left]],
sop[right].RelativizeComparison[cp[right]] ]]};
LexizePComPair:
PROC [cp: PComPair, first: Side]
RETURNS [PartialComparison]
~ INLINE {RETURN [IF cp[first]#equal THEN cp[first] ELSE cp[OtherSide[first]]]};
Pair Spaces
PairSpace:
TYPE ~
RECORD [sp: SpacePair, tro: TotalRelOrder];
A space of REF Pair, where [left] is in sp[left] and [right] is in sp[right]. Ordered according to ro.
WidenPairSpace: PROC [PairSpace] RETURNS [s: Space];
IsPairSpace:
PROC [s: Space]
RETURNS [
BOOL]
Is s the result of WidenPairSpace?
~ INLINE {RETURN [QuaPairSpace[s].found]};
AsPairSpace:
PROC [s: Space]
RETURNS [PairSpace]
Please apply only if IsPairSpace[s].
~ INLINE {RETURN [QuaPairSpace[s].it]};
QuaPairSpace: PROC [s: Space] RETURNS [MaybePairSpace];