LichenSetTheory:
CEDAR
DEFINITIONS =
BEGIN
NotMutable: ERROR;
HashParms: TYPE ~ RECORD [hash: RefTab.HashProc ← NIL, equal: RefTab.EqualProc ← NIL];
Set: TYPE = REF SetPrivate;
SetPrivate:
TYPE =
RECORD [
class: SetClass ← NIL,
mutable: BOOL ← TRUE,
data: REF ANY ← NIL];
SetClass: TYPE = REF SetClassPrivate;
SetClassPrivate:
TYPE =
RECORD [
TestMembership: PROC [set: Set, elt: REF ANY] RETURNS [BOOL],
UnionSingleton: PROC [set: Set, elt: REF ANY] RETURNS [new: BOOL],
UnionSet: PROC [self, other: Set],
RemoveElt: PROC [set: Set, elt: REF ANY] RETURNS [had: BOOL],
Enumerate: PROC [set: Set, Consumer: PROC [ra: REF ANY]],
Erase: PROC [set: Set],
Size: PROC [set: Set] RETURNS [INT]
];
DontUnionSingleton: PROC [set: Set, elt: REF ANY] RETURNS [new: BOOL];
DontUnionSet: PROC [self, other: Set];
DontRemoveElt: PROC [set: Set, elt: REF ANY] RETURNS [had: BOOL];
DontErase: PROC [set: Set];
HasMember:
PROC [set: Set, elt:
REF
ANY]
RETURNS [
BOOL]
= INLINE {RETURN[set.class.TestMembership[set, elt]]};
PickOne: PROC [set: Set] RETURNS [REF ANY];
TheElt:
PROC [set: Set]
RETURNS [
REF
ANY]
~ INLINE {IF set.Size[]#1 THEN ERROR ELSE RETURN [PickOne[set]]};
UnionSingleton:
PROC [set: Set, elt:
REF
ANY]
RETURNS [new:
BOOL]
= INLINE {IF NOT set.mutable THEN NotMutable[] ELSE new ← set.class.UnionSingleton[set, elt]};
UnionSet:
PROC [self, other: Set]
= INLINE {IF NOT self.mutable THEN NotMutable[] ELSE self.class.UnionSet[self, other]};
RemoveElt:
PROC [set: Set, elt:
REF
ANY]
RETURNS [had:
BOOL]
= INLINE {IF NOT set.mutable THEN NotMutable[] ELSE RETURN [set.class.RemoveElt[set, elt]]};
Enumerate:
PROC [set: Set,
Consumer:
PROC [
REF
ANY]]
= INLINE {set.class.Enumerate[set, Consumer]};
Erase:
PROC [set: Set]
= INLINE {IF NOT set.mutable THEN NotMutable[] ELSE set.class.Erase[set]};
Size:
PROC [set: Set]
RETURNS [
INT]
= INLINE {RETURN[set.class.Size[set]]};
FreezeSet:
PROC [set: Set]
= INLINE {set.mutable ← FALSE};
DestroySet:
PROC [set: Set]
= INLINE {set.class ← NIL; set.data ← NIL};
CreateSingleton: PROC [elt: REF ANY] RETURNS [set: Set];
CreateHashSet: PROC [HashParms ← []] RETURNS [set: Set];
SetList: TYPE = LIST OF Set;
CreateUnion:
PROC [sets: SetList, eltsImmutable:
BOOL ←
TRUE]
RETURNS [Set];
If eltsImmutable, the sets cannot change their contents.
emptySet: READONLY Set;
Mapper: TYPE = REF MapperPrivate;
MapperPrivate:
TYPE =
RECORD [
class: MapperClass,
mutable: BOOL ← TRUE,
data: REF ANY];
MapperClass: TYPE = REF MapperClassPrivate;
MapperClassPrivate:
TYPE =
RECORD [
Map: PROC [m: Mapper, domain: REF ANY] RETURNS [range: REF ANY],
PutMapping: PROC [m: Mapper, domain, range: REF ANY] RETURNS [newDomain: BOOL],
Enumerate: PROC [m: Mapper, Consume: PROC [domain, range: REF ANY]],
DomainEqual: PROC [m: Mapper, r1, r2: REF ANY] RETURNS [BOOL],
Size: PROC [m: Mapper] RETURNS [INT]
];
DontPutMapping: PROC [m: Mapper, domain, range: REF ANY] RETURNS [newDomain: BOOL];
DontEnumerateMapper: PROC [m: Mapper, Consume: PROC [domain, range: REF ANY]];
DomainCompareByRef: PROC [m: Mapper, r1, r2: REF ANY] RETURNS [BOOL];
DontAskMapperSize: PROC [m: Mapper] RETURNS [INT];
Map:
PROC [mapper: Mapper, arg:
REF
ANY]
RETURNS [result:
REF
ANY]
= INLINE {result ← mapper.class.Map[mapper, arg]};
PutMapping:
PROC [mapper: Mapper, domain, range:
REF
ANY]
RETURNS [newDomain:
BOOL]
= INLINE {IF NOT mapper.mutable THEN NotMutable[] ELSE newDomain ← mapper.class.PutMapping[mapper, domain, range]};
EnumerateMap:
PROC [mapper: Mapper,
Consume:
PROC [domain, range:
REF
ANY]]
= INLINE {mapper.class.Enumerate[mapper, Consume]};
DomainEqual:
PROC [m: Mapper, r1, r2:
REF
ANY]
RETURNS [
BOOL]
~ INLINE {RETURN [m.class.DomainEqual[m, r1, r2]]};
MapSize:
PROC [mapper: Mapper]
RETURNS [size:
INT]
= INLINE {size ← mapper.class.Size[mapper]};
FreezeMapper:
PROC [mapper: Mapper]
= INLINE {mapper.mutable ← FALSE};
CreateHashMapper: PROC [HashParms ← []] RETURNS [m: Mapper];
CreateHashDictionary: PROC [caseSensitive: BOOL] RETURNS [m: Mapper];
OneToOne: TYPE ~ REF OneToOnePrivate;
OneToOnePrivate:
TYPE ~
RECORD [
class: OneToOneClass,
mutable: BOOL ← TRUE,
data: REF ANY
];
OneToOneClass: TYPE ~ REF OneToOneClassPrivate;
OneToOneClassPrivate:
TYPE ~
RECORD [
Map: PROC [oto: OneToOne, from: REF ANY, dir: Direction] RETURNS [to: REF ANY],
PutMapping: PROC [oto: OneToOne, pair: Pair] RETURNS [new: LRBits],
Enumerate: PROC [oto: OneToOne, Consume: PROC [Pair]],
Size: PROC [oto: OneToOne] RETURNS [INT]
];
Pair: TYPE ~ ARRAY Side OF REF ANY;
Direction: TYPE ~ {leftToRight, rightToLeft};
Side: TYPE ~ {left, right};
OtherDirection: ARRAY Direction OF Direction ~ [rightToLeft, leftToRight];
OtherSide: ARRAY Side OF Side ~ [right, left];
Source: ARRAY Direction OF Side ~ [left, right];
Dest: ARRAY Direction OF Side ~ [right, left];
From: ARRAY Side OF Direction ~ [leftToRight, rightToLeft];
To: ARRAY Side OF Direction ~ [rightToLeft, leftToRight];
LRBits: TYPE ~ ARRAY Side OF BOOL;
OTOMap:
PROC [oto: OneToOne, from:
REF
ANY, dir: Direction]
RETURNS [
REF
ANY]
~ INLINE {RETURN [oto.class.Map[oto, from, dir]]};
PutOTOMapping:
PROC [oto: OneToOne, pair: Pair]
RETURNS [new: LRBits]
~ INLINE {IF NOT oto.mutable THEN NotMutable[] ELSE new ← oto.class.PutMapping[oto, pair]};
EnumerateOTO:
PROC [oto: OneToOne,
Consume:
PROC [Pair]]
~ INLINE {oto.class.Enumerate[oto, Consume]};
OTOSize:
PROC [oto: OneToOne]
RETURNS [size:
INT]
= INLINE {size ← oto.class.Size[oto]};
FreezeOTO:
PROC [oto: OneToOne]
= INLINE {oto.mutable ← FALSE};
CreateHashOTO: PROC [HashParmsPair ← [[], []]] RETURNS [OneToOne];
HashParmsPair: TYPE ~ ARRAY Side OF HashParms;
CreateOTOFromMappers: PROC [ARRAY Direction OF Mapper] RETURNS [OneToOne];
ReverseOTO: PROC [OneToOne] RETURNS [OneToOne];
ComposeOTOs: PROC [a, b: OneToOne] RETURNS [OneToOne];
Half: PROC [oto: OneToOne, dir: Direction] RETURNS [Mapper];
BiRel: TYPE ~ REF BiRelPrivate;
BiRelPrivate:
TYPE ~
RECORD [
class: BiRelClass,
mutable: BOOL ← TRUE,
data: REF ANY
];
BiRelClass: TYPE ~ REF BiRelClassPrivate;
BiRelClassPrivate:
TYPE ~
RECORD [
Map: PROC [reln: BiRel, x: REF ANY, dir: Direction] RETURNS [Set],
EnumerateMapping: PROC [reln: BiRel, x: REF ANY, dir: Direction, Consume: PROC [REF ANY]],
Enumerate: PROC [reln: BiRel, Consume: PROC [Pair]],
AddPair: PROC [reln: BiRel, pair: Pair] RETURNS [news: BOOL],
RemPair: PROC [reln: BiRel, pair: Pair] RETURNS [had: BOOL],
MappingSize: PROC [reln: BiRel, x: REF ANY, dir: Direction, limit: INT ← 1] RETURNS [size: INT],
Size: PROC [reln: BiRel] RETURNS [INT]
];
BiRelMap:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction]
RETURNS [Set]
~ INLINE {RETURN [reln.class.Map[reln, x, dir]]};
EnumerateMapping:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction,
Consume:
PROC [
REF
ANY]]
~ INLINE {reln.class.EnumerateMapping[reln, x, dir, Consume]};
EnumerateBiRel:
PROC [reln: BiRel,
Consume:
PROC [Pair]]
~ INLINE {reln.class.Enumerate[reln, Consume]};
AddPair:
PROC [reln: BiRel, pair: Pair]
RETURNS [news:
BOOL]
~ INLINE {RETURN [reln.class.AddPair[reln, pair]]};
RemPair:
PROC [reln: BiRel, pair: Pair]
RETURNS [had:
BOOL]
~ INLINE {RETURN [reln.class.RemPair[reln, pair]]};
MappingSize:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction, limit:
INT ← 1]
RETURNS [size:
INT
--size in [limit..actual size] OR size=actual size--]
~ INLINE {RETURN [reln.class.MappingSize[reln, x, dir, limit]]};
HasMapping:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction]
RETURNS [
BOOL]
~ INLINE {RETURN [reln.class.MappingSize[reln, x, dir, 1]>=1]};
BiRelSize:
PROC [reln: BiRel]
RETURNS [
INT]
~ INLINE {RETURN [reln.class.Size[reln]]};
CreateHashBiRel: PROC [HashParmsPair ← [[], []]] RETURNS [BiRel];
ReverseBiRel: PROC [BiRel] RETURNS [BiRel];
ComposeBiRels: PROC [a, b: BiRel] RETURNS [BiRel];
refAnyParms: READONLY HashParms;
caselessRopeParms: READONLY HashParms;
casefulRopeParms: READONLY HashParms;
HashIntI:
PROC [
INT]
RETURNS [
CARDINAL]
~ TRUSTED MACHINE CODE { PrincOps.zXOR };
HashRefI:
PROC [
REF
ANY]
RETURNS [
CARDINAL]
~ TRUSTED MACHINE CODE { PrincOps.zXOR };
END.