LichenSetTheoryImpl:
CEDAR
PROGRAM
IMPORTS LichenSetTheory, RefTab, Rope, RopeHash
EXPORTS LichenSetTheory =
BEGIN OPEN LichenSetTheory;
NotMutable: PUBLIC ERROR = CODE;
Escape: ERROR ~ CODE;
CreateSingleton:
PUBLIC
PROC [elt:
REF
ANY]
RETURNS [set: Set] = {
set ← NEW [SetPrivate ← [singletonClass, FALSE, elt]];
};
singletonClass: SetClass =
NEW [SetClassPrivate ← [
TestSingletonMembership,
DontUnionSingleton,
DontUnionSet,
DontRemoveElt,
EnumerateSingleton,
DontErase,
SingletonSize]];
TestSingletonMembership:
PROC [set: Set, elt:
REF
ANY]
RETURNS [in:
BOOL] = {
in ← elt = set.data};
DontUnionSingleton: PUBLIC PROC [set: Set, elt: REF ANY] RETURNS [new: BOOL] = {ERROR};
DontUnionSet: PUBLIC PROC [self, other: Set] = {ERROR};
DontRemoveElt: PUBLIC PROC [set: Set, elt: REF ANY] RETURNS [had: BOOL] = {ERROR};
DontEnumerate: PUBLIC PROC [set: Set, Consumer: PROC [ra: REF ANY]] ~ {ERROR};
DontErase: PUBLIC PROC [set: Set] = {ERROR};
DontAskSetSize: PUBLIC PROC [set: Set] RETURNS [INT] ~ {ERROR};
PickOne:
PUBLIC
PROC [set: Set]
RETURNS [elt:
REF
ANY] ~ {
See: PROC [ra: REF ANY] ~ {elt ← ra; Escape};
set.Enumerate[See !Escape => CONTINUE];
};
EnumerateSingleton: PROC [set: Set, Consumer: PROC [REF ANY]] = {Consumer[set.data]};
SingletonSize: PROC [set: Set] RETURNS [INT] = {RETURN[1]};
CreateHashSet:
PUBLIC
PROC [parms: HashParms ← []]
RETURNS [set: Set] = {
set ← NEW [SetPrivate ← [class: hashSetClass, data: RefTab.Create[hash: parms.hash, equal: parms.equal]]]};
hashSetClass: SetClass =
NEW [SetClassPrivate ← [
TestHashSetMembership,
HashSetUnionSingleton,
HashSetUnionSet,
RemoveHashSetElt,
EnumerateHashSet,
EraseHashSet,
HashSetSize]];
TestHashSetMembership:
PROC [set: Set, elt:
REF
ANY]
RETURNS [b:
BOOL] = {
ht: RefTab.Ref = NARROW[set.data];
b ← ht.Fetch[elt].found};
HashSetUnionSingleton:
PROC [set: Set, elt:
REF
ANY]
RETURNS [new:
BOOL] = {
ht: RefTab.Ref = NARROW[set.data];
new ← ht.Store[elt, $T];
};
HashSetUnionSet:
PROC [self, other: Set] = {
ht: RefTab.Ref = NARROW[self.data];
Addit:
PROC [elt:
REF
ANY] = {
[] ← ht.Insert[elt, $T]};
other.class.Enumerate[other, Addit];
};
RemoveHashSetElt:
PROC [set: Set, elt:
REF
ANY]
RETURNS [had:
BOOL] = {
ht: RefTab.Ref = NARROW[set.data];
had ← ht.Delete[elt];
};
EnumerateHashSet:
PROC [set: Set,
Consumer:
PROC [
REF
ANY]] = {
ht: RefTab.Ref = NARROW[set.data];
PerPair:
PROC [key, val:
REF
ANY]
RETURNS [quit:
BOOL ←
FALSE]
--RefTab.EachPairAction-- = {
Consumer[key];
};
[] ← ht.Pairs[PerPair]};
EraseHashSet:
PROC [set: Set] = {
ht: RefTab.Ref = NARROW[set.data];
ht.Erase[]};
HashSetSize:
PROC [set: Set]
RETURNS [size:
INT] = {
ht: RefTab.Ref = NARROW[set.data];
size ← ht.GetSize[]};
CreateFilterClass:
PUBLIC
PROC [
TestMembership:
PROC [set: Set, elt:
REF
ANY]
RETURNS [
BOOL]]
RETURNS [class: SetClass] ~ {
class ← NEW [SetClassPrivate ← [TestMembership, DontUnionSingleton, DontUnionSet, DontRemoveElt, DontEnumerate, DontErase, DontAskSetSize]];
};
CreateFilter:
PUBLIC
PROC [
TestMembership:
PROC [set: Set, elt:
REF
ANY]
RETURNS [
BOOL]]
RETURNS [f: Filter] ~ {
class: SetClass ~ CreateFilterClass[TestMembership];
f ← NEW [SetPrivate ← [class, FALSE, NIL]];
};
passAll: PUBLIC Filter ~ CreateFilter[PassAll];
PassAll: PROC [set: Set, elt: REF ANY] RETURNS [BOOL] ~ {RETURN [TRUE]};
Unioned: TYPE = REF UnionedPrivate;
UnionedPrivate:
TYPE =
RECORD [
incr, decr: SetList, --ordered by increasing size, decreasing size
eltsImmutable: BOOL,
size: INT ← notComputed
];
notComputed: INT = FIRST[INT];
unionSetClass: SetClass =
NEW [SetClassPrivate ← [
TestUnionMembership,
DontUnionSingleton,
UnionUnionSet,
DontRemoveElt,
EnumerateUnion,
DontErase,
UnionSize]];
CreateUnion:
PUBLIC
PROC [sets: SetList, eltsImmutable:
BOOL ←
TRUE]
RETURNS [set: Set] = {
u: Unioned = NEW [UnionedPrivate ← [eltsImmutable: eltsImmutable]];
[u.incr, u.decr] ← SizeSort[sets];
set ←
NEW [SetPrivate ← [
class: unionSetClass,
data: u
]];
};
TestUnionMembership:
PROC [set: Set, elt:
REF
ANY]
RETURNS [in:
BOOL] = {
u: Unioned = NARROW[set.data];
FOR sets: SetList ← u.decr, sets.rest
WHILE sets #
NIL
DO
IF sets.first.class.TestMembership[sets.first, elt] THEN RETURN [TRUE];
ENDLOOP;
in ← FALSE;
};
UnionUnionSet:
PROC [self, other: Set] = {
u: Unioned = NARROW[self.data];
[u.incr, u.decr] ← SizeInsert[u.incr, u.decr, other];
u.size ← notComputed;
};
EnumerateUnion:
PROC [set: Set,
Consumer:
PROC [
REF
ANY]] = {
u: Unioned = NARROW[set.data];
IF u.incr = NIL THEN RETURN;
u.incr.first.class.Enumerate[u.incr.first, Consumer];
EnumerateSetlistRestUnion[u.incr, Consumer];
};
EnumerateSetlistRestUnion:
PROC [sets: SetList,
Consumer:
PROC [
REF
ANY]] = {
FOR i: SetList ← sets.rest, i.rest
WHILE i #
NIL
DO
Filter:
PROC [elt:
REF
ANY] = {
FOR j: SetList ← sets, j.rest
WHILE j # i
DO
IF j.first.class.TestMembership[j.first, elt] THEN RETURN;
ENDLOOP;
Consumer[elt];
};
i.first.class.Enumerate[i.first, Filter];
ENDLOOP;
};
UnionSize:
PROC [set: Set]
RETURNS [size:
INT] = {
u: Unioned = NARROW[set.data];
CountIt: PROC [REF ANY] = {size ← size + 1};
IF u.size # notComputed THEN RETURN [u.size];
IF u.decr = NIL THEN RETURN [u.size ← 0];
size ← u.decr.first.class.Size[u.decr.first];
EnumerateSetlistRestUnion[u.decr, CountIt];
IF u.eltsImmutable THEN u.size ← size;
};
SizeSort:
PROC [sets: SetList]
RETURNS [increasing, decreasing: SetList] = {
increasing ← decreasing ← NIL;
WHILE sets #
NIL
DO
next: SetList = sets.rest;
increasing ← IncrInsert[increasing, sets];
sets ← next;
ENDLOOP;
FOR sets ← increasing, sets.rest
WHILE sets #
NIL
DO
decreasing ← CONS[sets.first, decreasing];
ENDLOOP;
};
SizeInsert:
PROC [oIncr, oDecr: SetList, set: Set]
RETURNS [
nIncr,
nDecr: SetList] = {
nIncr ← IncrInsert[oIncr, LIST[set]];
nDecr ← DecrInsert[oDecr, LIST[set]];
};
IncrInsert:
PROC [old, this: SetList]
RETURNS [new: SetList] = {
thisSize: INT = this.first.class.Size[this.first];
prev: SetList ← NIL;
following: SetList ← new ← old;
WHILE following #
NIL
AND thisSize > following.first.class.Size[following.first]
DO
prev ← following;
following ← following.rest;
ENDLOOP;
this.rest ← following;
IF prev = NIL THEN new ← this ELSE prev.rest ← this;
};
DecrInsert:
PROC [old, this: SetList]
RETURNS [new: SetList] = {
thisSize: INT = this.first.class.Size[this.first];
prev: SetList ← NIL;
following: SetList ← new ← old;
WHILE following #
NIL
AND thisSize <= following.first.class.Size[following.first]
DO
prev ← following;
following ← following.rest;
ENDLOOP;
this.rest ← following;
IF prev = NIL THEN new ← this ELSE prev.rest ← this;
};
emptySetClass: SetClass ~
NEW [SetClassPrivate ← [
EmptySetMembership,
DontUnionSingleton,
DontUnionSet,
RemoveEmptySetElt,
EnumerateEmptySet,
EraseEmptySet,
EmptySetSize]];
emptySet: PUBLIC Set ~ NEW [SetPrivate ← [emptySetClass, FALSE, NIL]];
EmptySetMembership:
PROC [set: Set, elt:
REF
ANY]
RETURNS [
BOOL]
~ {RETURN [FALSE]};
RemoveEmptySetElt:
PROC [set: Set, elt:
REF
ANY]
RETURNS [had:
BOOL]
~ {RETURN [FALSE]};
EnumerateEmptySet: PROC [set: Set, Consumer: PROC [ra: REF ANY]] ~ {};
EraseEmptySet: PROC [set: Set] ~ {};
EmptySetSize: PROC [set: Set] RETURNS [INT] ~ {RETURN [0]};
DontPutMapping: PUBLIC PROC [m: Mapper, domain, range: REF ANY] RETURNS [newDomain: BOOL] ~ {ERROR};
DontEnumerateMapper: PUBLIC PROC [m: Mapper, Consume: PROC [domain, range: REF ANY]] ~ {ERROR};
DomainCompareByRef: PUBLIC PROC [m: Mapper, r1, r2: REF ANY] RETURNS [BOOL] ~ {RETURN [r1=r2]};
DontAskMapperSize: PUBLIC PROC [m: Mapper] RETURNS [INT] ~ {ERROR};
CreateHashMapper:
PUBLIC
PROC [parms: HashParms ← []]
RETURNS [m: Mapper] = {
hm: HashMapper ~ NEW [HashMapperPrivate ← [RefTab.Create[hash: parms.hash, equal: parms.equal], parms]];
m ← NEW [MapperPrivate ← [class: hashMapperClass, data: hm]]};
CreateHashDictionary:
PUBLIC
PROC [caseSensitive:
BOOL]
RETURNS [m: Mapper] = {
m ← CreateHashMapper[IF caseSensitive THEN casefulRopeParms ELSE caselessRopeParms];
};
HashMapper: TYPE ~ REF HashMapperPrivate;
HashMapperPrivate:
TYPE ~
RECORD [
ht: RefTab.Ref,
parms: HashParms
];
hashMapperClass: MapperClass =
NEW [MapperClassPrivate ← [
Map: MapByHash,
PutMapping: PutHashMapping,
Enumerate: EnumerateHashMapping,
DomainEqual: HashDomainEqual,
Size: HashMappingSize]];
MapByHash:
PROC [m: Mapper, domain:
REF
ANY]
RETURNS [range:
REF
ANY] = {
hm: HashMapper ~ NARROW[m.data];
range ← hm.ht.Fetch[domain].val};
PutHashMapping:
PROC [m: Mapper, domain, range:
REF
ANY]
RETURNS [newDomain:
BOOL] = {
hm: HashMapper ~ NARROW[m.data];
SELECT range
FROM
=NIL => newDomain ← NOT hm.ht.Delete[domain];
#NIL => newDomain ← hm.ht.Store[domain, range];
ENDCASE => ERROR;
};
EnumerateHashMapping:
PROC [m: Mapper,
Consume:
PROC [domain, range:
REF
ANY]] = {
hm: HashMapper ~ NARROW[m.data];
Pass: PROC [key, val: REF ANY] RETURNS [quit: BOOL ← FALSE] --RefTab.EachPairAction-- = {Consume[key, val]};
[] ← hm.ht.Pairs[Pass];
};
HashDomainEqual:
PROC [m: Mapper, r1, r2:
REF
ANY]
RETURNS [
BOOL] ~ {
hm: HashMapper ~ NARROW[m.data];
RETURN [IF hm.parms.equal=NIL THEN r1=r2 ELSE hm.parms.equal[r1, r2]];
};
HashMappingSize:
PROC [m: Mapper]
RETURNS [size:
INT] = {
hm: HashMapper ~ NARROW[m.data];
size ← hm.ht.GetSize[]};
CreateProceduralMapperClass:
PUBLIC
PROC [
Map:
PROC [m: Mapper, domain:
REF
ANY]
RETURNS [range:
REF
ANY]]
RETURNS [class: MapperClass] ~ {
class ← NEW [MapperClassPrivate ← [Map, DontPutMapping, DontEnumerateMapper, DomainCompareByRef, DontAskMapperSize]];
};
CreateProceduralMapper:
PUBLIC
PROC [
Map:
PROC [m: Mapper, domain:
REF
ANY]
RETURNS [range:
REF
ANY], data:
REF
ANY ←
NIL]
RETURNS [m: Mapper] ~ {
class: MapperClass ← CreateProceduralMapperClass[Map];
m ← NEW [MapperPrivate ← [class, FALSE, data]];
};
CreateHashOTO:
PUBLIC
PROC [hpp: HashParmsPair ← [[], []]]
RETURNS [OneToOne] ~ {
RETURN [CreateOTOFromMappers[[leftToRight: CreateHashMapper[hpp[left]], rightToLeft: CreateHashMapper[hpp[right]]]]];
};
CreateOTOFromMappers:
PUBLIC
PROC [maps:
ARRAY Direction
OF Mapper]
RETURNS [oto: OneToOne] ~ {
mo: MapperOTO ~ NEW [MapperOTOPrivate ← [maps]];
Checkout:
PROC [dir: Direction] ~ {
Check:
PROC [domain, range:
REF
ANY] ~ {
IF NOT maps[dir].DomainEqual[maps[OtherDirection[dir]].Map[range], domain] THEN ERROR;
};
maps[dir].EnumerateMap[Check];
};
Checkout[leftToRight];
Checkout[rightToLeft];
oto ← NEW [OneToOnePrivate ← [class: abstractOTOClass, data: mo]];
};
MapperOTO: TYPE ~ REF MapperOTOPrivate;
MapperOTOPrivate:
TYPE ~
RECORD [
maps: ARRAY Direction OF Mapper
];
abstractOTOClass: OneToOneClass ~
NEW [OneToOneClassPrivate ← [
Map: MOMap,
PutMapping: PutMOMapping,
Enumerate: EnumerateMO,
Size: MOSize]];
MOMap:
PROC [oto: OneToOne, from:
REF
ANY, dir: Direction]
RETURNS [to:
REF
ANY] ~ {
mo: MapperOTO ~ NARROW[oto.data];
to ← mo.maps[dir].Map[from];
};
PutMOMapping:
PROC [oto: OneToOne, pair: Pair]
RETURNS [new: LRBits] ~ {
mo: MapperOTO ~ NARROW[oto.data];
oldLeft: REF ANY ~ mo.maps[rightToLeft].Map[pair[right]];
oldRight: REF ANY ~ mo.maps[leftToRight].Map[pair[left]];
leftEq: BOOL ~ mo.maps[leftToRight].DomainEqual[pair[left], oldLeft];
rightEq: BOOL ~ mo.maps[rightToLeft].DomainEqual[pair[right], oldRight];
IF leftEq AND rightEq THEN RETURN [[FALSE, FALSE]];
IF oldLeft#NIL AND NOT leftEq THEN IF mo.maps[leftToRight].PutMapping[oldLeft, NIL] THEN ERROR;
IF oldRight#NIL AND NOT rightEq THEN IF mo.maps[rightToLeft].PutMapping[oldRight, NIL] THEN ERROR;
[] ← mo.maps[leftToRight].PutMapping[pair[left], pair[right]];
[] ← mo.maps[rightToLeft].PutMapping[pair[right], pair[left]];
new ← [oldRight=NIL, oldLeft=NIL];
};
EnumerateMO:
PROC [oto: OneToOne,
Consume:
PROC [Pair]] ~ {
mo: MapperOTO ~ NARROW[oto.data];
Pass: PROC [domain, range: REF ANY] ~ {Consume[[domain, range]]};
mo.maps[leftToRight].EnumerateMap[Pass];
};
MOSize:
PROC [oto: OneToOne]
RETURNS [size:
INT] ~ {
mo: MapperOTO ~ NARROW[oto.data];
size ← mo.maps[leftToRight].MapSize[];
IF mo.maps[rightToLeft].MapSize[] # size THEN ERROR;
};
CreateHashBiRel:
PUBLIC
PROC [hpp: HashParmsPair ← [[], []]]
RETURNS [BiRel] ~ {
hb: HashBiRel ~
NEW [HashBiRelPrivate ← [
parms: hpp,
maps: [CreateHashMapper[hpp[left]], CreateHashMapper[hpp[right]]]
]];
RETURN [NEW [BiRelPrivate ← [hashBiRelClass, TRUE, hb]]];
};
HashBiRel: TYPE ~ REF HashBiRelPrivate;
HashBiRelPrivate:
TYPE ~
RECORD [
parms: HashParmsPair,
maps: ARRAY Direction OF Mapper,
size: INT ← 0
];
hashBiRelClass: BiRelClass ~
NEW [BiRelClassPrivate ← [
Map: HBMap,
EnumerateMapping: EnumerateHBMapping,
Enumerate: EnumerateHB,
AddPair: AddHBPair,
RemPair: RemHBPair,
MappingSize: HBMappingSize,
Size: HBSize]];
HBMap:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction]
RETURNS [Set] ~ {
hb: HashBiRel ~ NARROW[reln.data];
set: Set ~ NARROW[hb.maps[dir].Map[x]];
RETURN [IF set#NIL THEN set ELSE emptySet];
};
EnumerateHBMapping:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction,
Consume:
PROC [
REF
ANY]] ~ {
hb: HashBiRel ~ NARROW[reln.data];
set: Set ~ NARROW[hb.maps[dir].Map[x]];
IF set#NIL THEN set.Enumerate[Consume];
};
EnumerateHB:
PROC [reln: BiRel,
Consume:
PROC [Pair]] ~ {
hb: HashBiRel ~ NARROW[reln.data];
PerLeft:
PROC [domain, range:
REF
ANY] ~ {
set: Set ~ NARROW[range];
PerRight: PROC [right: REF ANY] ~ {Consume[[domain, right]]};
set.Enumerate[PerRight];
};
hb.maps[leftToRight].EnumerateMap[PerLeft];
};
AddHBPair:
PROC [reln: BiRel, pair: Pair]
RETURNS [news:
BOOL] ~ {
hb: HashBiRel ~ NARROW[reln.data];
Add:
PROC [dir: Direction]
RETURNS [news:
BOOL] ~ {
x: REF ANY ~ pair[Source[dir]];
y: REF ANY ~ pair[Dest[dir]];
set: Set ← NARROW[hb.maps[dir].Map[x]];
IF set=NIL THEN IF NOT hb.maps[dir].PutMapping[x, set ← CreateHashSet[hb.parms[Dest[dir]]]] THEN ERROR;
news ← set.UnionSingleton[y];
};
new: ARRAY Direction OF BOOL ~ [Add[leftToRight], Add[rightToLeft]];
IF new[leftToRight] # new[rightToLeft] THEN ERROR;
IF new[leftToRight] THEN hb.size ← hb.size+1;
RETURN [new[leftToRight]];
};
RemHBPair:
PROC [reln: BiRel, pair: Pair]
RETURNS [had:
BOOL] ~ {
hb: HashBiRel ~ NARROW[reln.data];
Rem:
PROC [dir: Direction]
RETURNS [had:
BOOL] ~ {
x: REF ANY ~ pair[Source[dir]];
y: REF ANY ~ pair[Dest[dir]];
set: Set ~ NARROW[hb.maps[dir].Map[x]];
IF set=NIL THEN RETURN [FALSE];
had ← set.RemoveElt[y];
};
hads: ARRAY Direction OF BOOL ~ [Rem[leftToRight], Rem[rightToLeft]];
IF hads[leftToRight] # hads[rightToLeft] THEN ERROR;
IF hads[leftToRight] THEN hb.size ← hb.size-1;
RETURN [hads[leftToRight]];
};
HBMappingSize:
PROC [reln: BiRel, x:
REF
ANY, dir: Direction, limit:
INT ← 1]
RETURNS [size:
INT] ~ {
hb: HashBiRel ~ NARROW[reln.data];
set: Set ~ NARROW[hb.maps[dir].Map[x]];
RETURN [IF set=NIL THEN 0 ELSE set.Size[]];
};
HBSize:
PROC [reln: BiRel]
RETURNS [
INT] ~ {
hb: HashBiRel ~ NARROW[reln.data];
RETURN [hb.size];
};
refAnyParms: PUBLIC HashParms ~ [HashRef, RefEqual];
caselessRopeParms: PUBLIC HashParms ~ [HashRopeModCase, RopeEqualModCase];
casefulRopeParms: PUBLIC HashParms ~ [HashRope, RopeEqual];
HashInt:
PROC [key:
INT]
RETURNS [
CARDINAL]
~ {RETURN [HashIntI[key]]};
HashRef:
PROC [key:
REF
ANY]
RETURNS [
CARDINAL]
~ {RETURN [HashRefI[key]]};
RefEqual:
PROC [key1, key2:
REF
ANY]
RETURNS [
BOOL]
~ {RETURN [key1 = key2]};
HashRope:
PROC [k:
REF
ANY]
RETURNS [
CARDINAL]
~ {RETURN [RopeHash.FromRope[NARROW[k], TRUE]]};
RopeEqual:
PROC [key1, key2:
REF
ANY]
RETURNS [
BOOL]
~ {RETURN [Rope.Equal[NARROW[key1], NARROW[key2], TRUE]]};
HashRopeModCase:
PROC [k:
REF
ANY]
RETURNS [
CARDINAL]
~ {RETURN [RopeHash.FromRope[NARROW[k], FALSE]]};
RopeEqualModCase:
PROC [key1, key2:
REF
ANY]
RETURNS [
BOOL]
~ {RETURN [Rope.Equal[NARROW[key1], NARROW[key2], FALSE]]};
END.