CompareDataStructure:
CEDAR
DEFINITIONS =
BEGIN
LORA: TYPE = LIST OF REF ANY;
LOLORA: TYPE = LIST OF LORA;
ROPE: TYPE = Rope.ROPE;
RopeList: TYPE = LIST OF ROPE;
SymbolTable: TYPE = OrderedSymbolTableRef.Table;
SymbolTableHolder: TYPE = REF SymbolTable;
Assertions: TYPE = Asserting.Assertions;
GraphID: TYPE = {A, B, Unspecified};
RealGraphID: TYPE = GraphID[A .. B];
Color: TYPE = HashTableIndex;
noColor: Color = LAST[Color];
HashTableIndex: TYPE = CARDINAL;
NullIndex: HashTableIndex = LAST[HashTableIndex];
VertexClass: TYPE = {net, cell};
OtherClass: ARRAY VertexClass OF VertexClass = [net: cell, cell: net];
EquivClass: TYPE = ROPE;
implicitClass: EquivClass = NIL;
NamesList: TYPE = LIST OF Names;
Names: TYPE = RECORD [designed, unknown, progged: RopeList ← NIL];
Design: TYPE = REF DesignRep;
DesignRep:
TYPE =
RECORD [
name: ROPE,
cellTypesByName: SymbolTable,
cellTypesByAddress: SymbolTable,
other: Assertions ← NIL,
allKnown, allKept: BOOL ← FALSE
];
CellType: TYPE = REF CellTypeRep;
CellTypeRep:
TYPE =
RECORD [
design: Design,
names: Names,
file: ROPE,
equivClass: EquivClass ← implicitClass,
color: Color ← noColor,
inittedFor: NAT ← 0,
publicKnown, privateKnown, wasntNormalized: BOOL ← FALSE,
ports: PortS ← NIL,
At most one of these two should be present:
Fully general description:
parts: SymbolTable ← NIL,
mirror: Vertex ←
NIL,
--the outside world, as seen from the inside
AM1: A mirror is not entered in its parent's parts table.
AM2: A mirror is not linked in as an instance of its type.
asArray: Array ← NIL,
netCount, cellCount:
NAT ← 0,
Counts are redundant with parts and asArray.
firstInstance, lastInstance: Vertex ← NIL,
otherPublic, otherPrivate: Assertions ← NIL];
PortS: TYPE = REF PortSeq;
PortSeq: TYPE = RECORD [ports: SEQUENCE length: PortIndex OF Port];
PortIndex: TYPE = NAT;
NullPortIndex: PortIndex = LAST[PortIndex];
Port: TYPE = RECORD [names: Names ← [NIL, NIL, NIL], equivClass: EquivClass ← implicitClass, netNames: RopeList ← NIL, other: Assertions ← NIL, color: Color ← noColor];
AliasList: TYPE = LIST OF Alias;
Alias: TYPE = REF AliasRep;
AliasRep:
TYPE =
RECORD [
name: ROPE,
thing: REF ANY];
VertexList: TYPE = LIST OF Vertex;
Vertex: TYPE = REF VertexRep;
VertexRep:
TYPE =
RECORD [
names: Names,
QNext: Vertex ← notInQ,
colorNext, equiv: Vertex ← NIL,
firstEdge, lastEdge: Edge ← NIL,
nextInstance, prevInstance: Vertex ← NIL,
type, parent: CellType ← NIL,
extraConnections: SymbolTable ← NIL,
other: Assertions ← NIL,
oldColor, curColor: Color ← noColor,
graph: GraphID ← Unspecified,
class: VertexClass,
unique, suspect: BOOL ← FALSE];
Edge: TYPE = REF EdgeRep;
EdgeRep:
TYPE =
RECORD [
sides: ARRAY VertexClass OF RECORD [v: Vertex, next, prev: Edge],
color: Color, portIndex: CARDINAL];
ExtraConnection: TYPE = REF ExtraConnectionRep;
ExtraConnectionRep: TYPE = RECORD [parentNet, subCell, childNet: Vertex];
Array assertions:
AA1: Each connection between adjacent elements involves exactly one port of each element.
AA2: Each port of an array connects to no more than one port of each element.
AA3: For any port of an array, all of the element ports it connects to are connected by array elements.
Array: TYPE = REF ArrayRep;
ArrayRep:
TYPE =
RECORD [
eltType: CellType,
shape: ARRAY Dim OF Range,
joints: ARRAY Dim--perp to joint-- OF ARRAY EO--perp to dim-- OF ARRAY EO--along dim-- OF Joint ← ALL[ALL[ALL[NIL]]],
portConnections: ArrayPortConnections,
redundant with porting.
porting:
SEQUENCE eltPorts: PortIndex
OF Porting
porting[p] gives port connections for e[f, b].p, for all f, b on edge of array.
];
Dim--ension--: TYPE = {Foo, Bar};
OtherDim: ARRAY Dim OF Dim = [Foo: Bar, Bar: Foo];
Range: TYPE = RECORD [min, maxPlusOne: INT];
EO: TYPE = {Even, Odd};
OtherEO: ARRAY EO OF EO = [Even: Odd, Odd: Even];
Joint: TYPE = REF JointSeq;
JointSeq:
TYPE =
RECORD [joints:
SEQUENCE eltPorts: PortIndex
OF
RECORD [low, high: PortIndex]];
e[i].pl é e[i+1].ph { j[pl].high = ph & j[ph].low = pl
e[i].pl not connected to any e[i+1].ph { j[pl].high = NullPortIndex
Porting: TYPE = REF ANY --actually UNION [{notPorted, unknownPorting}, DetailedPorting]--;
notPorted: Porting;
unknownPorting: Porting;
DetailedPorting: TYPE = REF DetailedPortingRep;
DetailedPortingRep:
TYPE =
RECORD [
corners:
ARRAY End
--Foo--
OF
ARRAY End
--Bar--
OF PortIndex,
e[Foo.LAST, Bar.LAST].p é a.q { porting[p].corners[high][high] = q
NullPortIndex means elt port not connected to any array port.
sideIndices:
ARRAY End
OF
ARRAY Dim
OF SideIndex,
sideIndices[low][Foo] covers [f, b] f = FIRST[Foo] & b (FIRST[BAR] .. LAST[BAR])
slots: SEQUENCE length: NAT OF PortIndex];
End: TYPE = {low, high};
OtherEnd: ARRAY End OF End = [low: high, high: low];
SideIndex: TYPE = RECORD [same: BOOL, firstSlot: NAT];
ArrayPortConnections: TYPE = REF ArrayPortConnectionSeq;
ArrayPortConnectionSeq: TYPE = RECORD [SEQUENCE arrayPorts: PortIndex OF ARRAY End OF ARRAY Dim OF SideConnection];
SideConnection: TYPE = RECORD [range: Range, sockets: ArraySocketList];
ArraySocketList: TYPE = LIST OF ArraySocket;
ArraySocket: TYPE = RECORD [ai: ArrayIndex, pi: PortIndex];
ArrayIndex: TYPE = ARRAY Dim OF INT;
notInQ: Vertex --don't look:-- = NIL --you looked!--;
endOfQ: Vertex;
Socket: TYPE = REF SocketRep;
SocketRep: TYPE = RECORD [ct: CellType, portIndex: PortIndex];
HashTable: TYPE = REF HashTableRep;
HashTableRep:
TYPE =
RECORD [
firstNonEmpty: HashTableIndex ← NullIndex,
entries: SEQUENCE length: HashTableIndex OF HashTableEntry];
HashTableEntry:
TYPE =
RECORD [
v: Vertex ← NIL,
nextNonEmpty: HashTableIndex ← NullIndex,
count: ARRAY RealGraphID OF CARDINAL ← [0, 0],
newColor: Color ← noColor,
suspect, multicolored: BOOL ← FALSE
];
newColor and multicolored are indexed by oldColor; the rest by curColor.
graphIDToRope: ARRAY GraphID OF ROPE;
CompareRopes: OrderedSymbolTableRef.CompareProc;
CompareNames: OrderedSymbolTableRef.CompareProc;
CompareByAddress: OrderedSymbolTableRef.CompareProc;
CompareVertices: OrderedSymbolTableRef.CompareProc;
CompareECParentNet, CompareECSubCell, CompareECChildNet, CompareECSubCellThenChildNet: OrderedSymbolTableRef.CompareProc;
MirrorName: ROPE;
END.