LichenDataImplArrays2.Mesa
Last tweaked by Mike Spreitzer on May 11, 1988 5:48:59 pm PDT
DIRECTORY AbSets, Basics, BasicTime, BiRels, IO, LichenArrayPrivate, LichenDataOps, LichenDataStructure, LichenIntBasics, Rope, SetBasics;
LichenDataImplArrays2:
CEDAR
PROGRAM
IMPORTS AbSets, BiRels, LichenArrayPrivate, LichenDataOps, LichenDataStructure, LichenIntBasics, SetBasics
EXPORTS LichenDataStructure, LichenDataOps
=
BEGIN OPEN IB:LichenIntBasics, IB, LichenDataStructure, LichenDataOps, LichenArrayPrivate, Sets:AbSets;
FinishedMakingArrayConnections:
PUBLIC
PROC [act: CellType] ~ {
a: Array ~ act.asArray;
dwSpace: Sets.Space ~
NEW [SetBasics.SpacePrivate ← [
Contains: DWContains,
Equal: SetBasics.refs.Equal,
AHash: SetBasics.refs.AHash,
ACompare: SetBasics.refs.ACompare,
Print: DWPrint,
name: "dumb wires",
data: act]];
dumrep: DumRep ~
NEW [DumRepPrivate ← [
dwSpace: dwSpace,
wires: Sets.CreateHashSet[dwSpace],
epToWire: BiRels.CreateHashTable[[act.d.eSpace, SetBasics.refs]],
apToWire: BiRels.CreateHashFn[spaces: [act.d.eSpace, dwSpace], invable: TRUE]
]];
PerStatEdge:
PROC [ra:
REF
ANY] ~
--AASEU and AAOTSE tell us we can just do this in any order-- {
se: StatEdge ~ NARROW[ra];
DumbifyStatEdge[act, se, FALSE];
RETURN};
PerPort:
PROC [pair: BiRels.Pair] ~ {
ap: Port ~ NARROW[pair[left].VA];
pai: PortAtIndex ~ VPai[pair[right]];
dw: DumbWire ~ GetDumbWireForPort[act, pai.port, pai.ai, TRUE];
IF dw=NIL THEN ERROR;
dumrep.apToWire.AddNewAA[ap, dw];
RETURN};
IF a.buildPhase#buildingStatrep THEN ERROR;
a.buildPhase ← statrepFixed;
a.dumrep ← dumrep;
a.statrep.edges.EnumA[PerStatEdge];
a.statrep.apToPAI.Enumerate[PerPort];
RETURN};
DumbifyStatEdge:
PROC [act: CellType, se: StatEdge, supering:
BOOL] ~
--relies heavily on AASEU, and makes an amortized check of it-- {
a: Array ~ act.asArray;
epA: Port ~ se.vs[FALSE].port;
epB: Port ~ se.vs[TRUE].port;
pepA: Port ~ act.d.PParent[epA];
pepB: Port ~ act.d.PParent[epB];
fullRangeA: Range2 ~ Range2Intersection[SizeRange[a.size2], Range2Off[SizeRange[a.size2], Neg[se.d]]];
iRangeA: Range2 ~ Range2Div[fullRangeA, a.basePeriod, se.vs[FALSE].phase];
dwsA: Seq--cai b DumbWire-- ~ GetDumbWires[a, epA, TRUE]^;
dwsB: Seq--cai b DumbWire-- ~ GetDumbWires[a, epB, TRUE]^;
atomic: BOOL ~ act.d.Atomic[epA];
width: LNAT ~ IF atomic THEN 0 ELSE act.d.Width[epA];
IF act.d.Atomic[epB] # atomic THEN ERROR;
IF NOT (atomic OR width = act.d.Width[epB]) THEN ERROR;
FOR i
f:
INT
IN [iRangeA[X].min .. iRangeA[X].maxPlusOne)
DO
FOR i
b:
INT
IN [iRangeA[Y].min .. iRangeA[Y].maxPlusOne)
DO
aiA: Int2 ~ [
if*a.basePeriod[X]+se.vs[FALSE].phase[X],
ib*a.basePeriod[Y]+se.vs[FALSE].phase[Y]];
aiB: Int2 ~ Add[se.d, aiA];
caiA: CompositeArrayIndex ~ ComposeAI[a, aiA];
caiB: CompositeArrayIndex ~ ComposeAI[a, aiB];
dwA: DumbWire ~ NARROW[dwsA.ApplyI[caiA].MDA];
dwB: DumbWire ~ NARROW[dwsB.ApplyI[caiB].MDA];
dw: DumbWire ← NIL;
IF (IF dwA=NIL THEN pepA#NIL AND GetDumbWire[act, pepA, aiA, TRUE]#NIL ELSE dwA.parent#NIL) OR (IF dwB=NIL THEN pepB#NIL AND GetDumbWire[act, pepB, aiB, TRUE]#NIL ELSE dwB.parent#NIL) THEN ERROR--AASEU violated here--;
IF dwA=dwB
THEN {
IF dwA#
NIL
THEN dw ← dwA
ELSE {
dw ← CreateDumbTop[act, epA];
AddDumbElt[a, dw, epA, aiA];
AddDumbElt[a, dw, epB, aiB]}}
ELSE IF dwA=NIL THEN AddDumbElt[a, dw ← dwB, epA, aiA]
ELSE IF dwB=NIL THEN AddDumbElt[a, dw ← dwA, epB, aiB]
ELSE dw ← JoinDumbWires[a, dwA, dwB].survivor;
IF supering
THEN {dw ← dw;
FOR i:
LNAT
IN [0 .. width)
DO
cepA: Port ~ NARROW[act.d.Sub[epA, i]];
cepB: Port ~ NARROW[act.d.Sub[epB, i]];
cdwA: DumbWire ~ GetDumbWire[act, cepA, aiA, FALSE];
cdwB: DumbWire ~ GetDumbWire[act, cepB, aiB, FALSE];
IF cdwA = NIL OR cdwA # cdwB THEN ERROR;
EnsureDumbChild[act, dw, i, cdwA];
ENDLOOP;
act ← act};
se ← se;
ENDLOOP ENDLOOP;
RETURN};
GetDumbWires:
PROC [a: Array, ep: Port, mayAdd:
BOOL]
RETURNS [dws: RefBiRel
--cai
b DumbWire--] ~ {
dws ← NARROW[a.dumrep.epToWire.ApplyA[ep].MDA];
IF dws=
NIL
AND mayAdd
THEN {
dws ← BiRels.CreateVector[bounds: [0, a.size-1], rightSpace: a.dumrep.dwSpace].Refify;
a.dumrep.epToWire.AddNewAA[ep, dws]};
RETURN};
CreateDumbTop:
PROC [act: CellType, rep: Port]
RETURNS [tdw: TopDumbWire] ~ {
a: Array ~ act.asArray;
tdw ← CreateDumbWire[act, rep, NIL, LNAT.LAST];
IF NOT a.dumrep.wires.AddA[tdw] THEN ERROR;
RETURN};
AddDumbElt:
PROC [a: Array, dw: TopDumbWire, ep: Port, ai: Int2] ~ {
cai: CompositeArrayIndex ~ ComposeAI[a, ai];
dws: RefBiRel--cai b DumbWire-- ~ GetDumbWires[a, ep, TRUE];
dws^.AddNewIA[cai, dw];
dw.eps.AddNewPair[[AV[ep], IV[cai]]];
RETURN};
JoinDumbWires:
PROC [a: Array, dwA, dwB: TopDumbWire]
RETURNS [survivor, deceased: TopDumbWire] ~ {
MoveIndex:
PROC [ra:
REF
ANY] ~ {
ep: Port ~ NARROW[ra];
dws: RefBiRel ~ GetDumbWires[a, ep, FALSE];
IF dws=NIL THEN ERROR;
dws^.SubstituteA[dwB, dwA, right];
RETURN};
IF dwB.children#nilBiRel AND NOT dwB.children.Empty THEN ERROR;
IF NOT a.dumrep.wires.RemA[dwB] THEN ERROR;
dwB.eps.SetOn[left].EnumA[MoveIndex];
[] ← dwA.eps.AddSet[dwB.eps];
a.dumrep.apToWire.SubstituteA[dwB, dwA, right];
RETURN [dwA, dwB]};
GetDumbWireForPort:
PROC [act: CellType, ep: Port, ai: Int2, mayAdd:
BOOL]
RETURNS [dw: DumbWire] ~ {
a: Array ~ act.asArray;
dw ← GetDumbWire[act, ep, ai, TRUE];
IF dw#NIL OR NOT mayAdd THEN RETURN;
AddDumbSubtree[act, ai, ep];
dw ← GetDumbWire[act, ep, ai, TRUE];
RETURN};
AddDumbSubtree:
PROC [act: CellType, ai: Int2, ep: Port] ~
--required by AASEU to not add ancestor dumb wires to any already in same tree-- {
a: Array ~ act.asArray;
Check:
PROC [ep, done: Port]
RETURNS [ok:
BOOL ←
TRUE] ~ {
ok ← GetDumbWire[act, ep, ai, TRUE] = NIL;
IF ok
AND
NOT act.d.Atomic[ep]
THEN
FOR i:
LNAT
IN [0 .. act.d.Width[ep])
WHILE ok
DO
cep: Port ~ NARROW[act.d.Sub[ep, i]];
ok ← cep=done OR Check[cep, NIL];
ENDLOOP;
RETURN};
IF NOT Check[ep, NIL] THEN RETURN;
{
WorkUp:
PROC [ep: Port] ~ {
parent: Port ~ act.d.PParent[ep];
IF parent#
NIL
THEN {
pdw: DumbWire ~ GetDumbWire[act, parent, ai, TRUE];
IF pdw#NIL THEN {WorkDown[pdw, parent]; RETURN};
IF Check[parent, ep] THEN {WorkUp[parent]; RETURN};
};
{tdw: TopDumbWire ~ CreateDumbTop[act, ep];
AddDumbElt[a, tdw, ep, ai];
WorkDown[tdw, ep];
RETURN}};
WorkDown:
PROC [dw: DumbWire, ep: Port] ~ {
IF
NOT act.d.Atomic[ep]
THEN
FOR i:
LNAT
IN [0 .. act.d.Width[ep])
DO
cep: Port ~ NARROW[act.d.Sub[ep, i]];
WorkDown[GetDumbChild[act, cep, dw, i], cep];
ENDLOOP;
RETURN};
WorkUp[ep];
RETURN}};
ArrayEltPortsConnected:
PUBLIC
PROC [act: CellType, ai1, ai2: Int2, ep1, ep2: Port]
RETURNS [
BOOL] ~ {
a: Array ~ act.asArray;
IF a.buildPhase#statrepFixed THEN ERROR;
{dw1: DumbWire ~ GetDumbWire[act, ep1, ai1, TRUE];
dw2: DumbWire ~ GetDumbWire[act, ep2, ai2, TRUE];
RETURN [dw1=dw2 AND dw1#NIL]}};
GetDumbWire:
PROC [act: CellType, ep: Port, ai: Int2, mayUp:
BOOL]
RETURNS [dw: DumbWire] ~ {
a: Array ~ act.asArray;
d: Design ~ act.d;
cai: CompositeArrayIndex ~ ComposeAI[a, ai];
Work:
PROC [ep: Port]
RETURNS [dw: DumbWire] ~ {
dws: RefBiRel--cai b DumbWire-- ~ GetDumbWires[a, ep, FALSE];
IF dws#NIL THEN dw ← NARROW[dws^.ApplyI[cai].MDA];
IF dw#NIL OR NOT mayUp THEN RETURN;
{parent: Port ~ d.PParent[ep];
IF parent#
NIL
THEN {
pdw: DumbWire ~ Work[parent];
IF pdw#NIL THEN RETURN [GetDumbChild[act, ep, pdw, d.PIndex[ep, parent]]];
};
RETURN}};
IF a.buildPhase#statrepFixed THEN ERROR;
RETURN Work[ep]};
GetDumbChild:
PROC [act: CellType, ep: Port, pdw: DumbWire, idx:
LNAT]
RETURNS [cdw: ChildDumbWire] ~ {
cdw ← NARROW[pdw.children.ApplyI[idx].MDA];
IF cdw#NIL THEN RETURN;
pdw.children.AddNewIA[idx, cdw ← CreateDumbWire[act, ep, pdw, idx] ];
RETURN};
EnsureDumbChild:
PROC [act: CellType, pdw: DumbWire, idx:
LNAT, cdw: DumbWire] ~ {
SELECT pdw.children.ApplyI[idx].
MDA
FROM
cdw => NULL;
NIL => {
IF cdw.parent#NIL THEN ERROR;
pdw.children.AddNewIA[idx, cdw];
cdw.parent ← pdw; cdw.index ← idx};
ENDCASE => ERROR};
CreateDumbWire:
PROC [act: CellType, ep: Port, parent: DumbWire, index:
LNAT]
RETURNS [dw: DumbWire] ~ {
a: Array ~ act.asArray;
atomic: BOOL ~ act.d.Atomic[ep];
kidMax: INT ~ IF atomic THEN -1 ELSE act.d.Width[ep]-1;
dw ←
NEW [DumbWirePrivate ← [
eps: BiRels.GenCreate[
spaces: [act.d.eSpace, SetBasics.ints],
mappable: [TRUE, FALSE],
hints: [
leftToRight: [
fn: [$Hash],
set: [$Vector,
LIST[
[$Bounds, NEW [SetBasics.IntInterval ← [0, a.size-1]] ]
]]],
rightToLeft: []]],
parent: parent, index: index
]];
IF
NOT atomic
THEN dw.children ← BiRels.CreateVector[
bounds: [0, kidMax],
rightSpace: a.dumrep.dwSpace];
RETURN};
NoteNewArrayPort:
PUBLIC
PROC [act: CellType, ap: Port] ~ {
d: Design ~ act.d;
a: Array ~ act.asArray;
portKids: Seq--of Port-- ~ d.SubSeq[ap];
dumKids: Seq--of DumbWire-- ~ portKids.Compose[a.dumrep.apToWire];
width: LNAT ~ portKids.Size.EN;
pdw: DumbWire;
IF a.buildPhase#statrepFixed THEN ERROR;
IF portKids=nilBiRel THEN ERROR;
IF width=0 THEN ERROR;
IF width # dumKids.Size.EN THEN RETURN;
FOR i:
LNAT
IN [0 .. width)
DO
WITH dumKids.ApplyI[i].
MA
SELECT
FROM
cdw: DumbWire => {
IF cdw.parent=NIL THEN RETURN;
IF i=0 THEN {IF (pdw ← cdw.parent).children.Size.EN # width THEN RETURN}
ELSE IF pdw#cdw.parent THEN RETURN;
IF cdw.index # i THEN RETURN};
ENDCASE => RETURN;
ENDLOOP;
{pai: PortAtIndex ~ act.SomePAI[pdw];
IF pai.port=NIL THEN ERROR;
a.statrep.apToPAI.AddNewPair[[AV[ap], pai.PaiV]];
a.dumrep.apToWire.AddNewAA[ap, pdw];
RETURN}};
GetArrayPortForPort:
PUBLIC
PROC [act: CellType, ai: Int2, ep: Port, mayAdd:
BOOL]
RETURNS [arrayPort: Port] ~ {
d: Design ~ act.d;
a: Array ~ act.asArray;
IF a.buildPhase#statrepFixed THEN ERROR;
{dw: DumbWire ~ GetDumbWireForPort[act, ep, ai, mayAdd];
IF dw=NIL THEN {IF mayAdd THEN --possible because of AASEU-- ERROR--trying to export a composite wire that doesn't really exist-- ELSE RETURN [NIL]};
{aPort: Port ~ NARROW[a.dumrep.apToWire.Lookup[goal: AV[dw], order: Sets.alleq].MDA];
IF aPort#NIL THEN RETURN [aPort];
IF NOT mayAdd THEN RETURN [NIL];
{ect: CellType ~ act.EltType[];
apKids: Seq--of array port-- ← nilBiRel;
IF
NOT d.Atomic[ep]
THEN {
epKids: Seq--of elt port-- ~ BiRels.DeRef[d.sub.ApplyA[ep].MA];
width: NATURAL ~ epKids.Size.EN;
apKids ← BiRels.CreateVector[bounds: [0, width-1], oneToOne: TRUE, dense: TRUE, rightSpace: d.eSpace];
FOR i:
NATURAL
IN [0 .. width)
DO
epKid: Port ~ NARROW[epKids.ApplyI[i].MA];
apKid: Port ~ GetArrayPortForPort[act, ai, epKid, mayAdd];
apKids.AddNewIA[i, apKid];
ENDLOOP;
};
arrayPort ← CreatePort[act, IF act.inheritNames THEN ActualNames[OneSteppy[AIName[act, ai]], ect.PNames[ep]] ELSE emptySteppySet, TRUE, FALSE--taken care of below--, TRUE, TRUE, TRUE, apKids];
a.statrep.apToPAI.AddNewPair[[AV[arrayPort], PaiV[[ep, ai]]]];
a.dumrep.apToWire.AddNewAA[arrayPort, dw];
RETURN}}}};
NoteNewEltPort:
PUBLIC
PROC [act: CellType, ep: Port] ~ {
IF act.d.Atomic[ep] THEN RETURN;
{d: Design ~ act.d; a: Array ~ act.asArray;
width: LNAT ~ d.Width[ep];
cp0: Port ~ NARROW[d.Sub[ep, 0]];
TryUpEdge:
PROC [se: StatEdge, ob:
BOOL]
RETURNS [
BOOL] ~ {
parentSEP: StatEdgePrivate ~ ParentSEP[d, se^];
sb: BOOL ~ NOT ob;
oep: Port ~ parentSEP.vs[ob].port;
IF parentSEP.vs[sb].port # ep THEN ERROR;
IF oep = NIL THEN RETURN [FALSE];
IF d.Width[oep] # width THEN RETURN [FALSE];
IF d.Sub[oep, 0] # se.vs[ob].port THEN RETURN [FALSE];
FOR i:
LNAT
IN [1 .. width)
DO
IF FindStatEdge[a.statrep, ChildSEP[d, parentSEP, i], FALSE].fse = NIL THEN RETURN [FALSE];
ENDLOOP;
{pse: StatEdge ~ AddStatEdgeAndClose[d, a.statrep, parentSEP];
IF pse=NIL OR FindStatEdge[a.statrep, parentSEP, FALSE].fse#pse THEN ERROR;
SELECT a.buildPhase
FROM
buildingStatrep => NULL;
statrepFixed => DumbifyStatEdge[act, pse, TRUE];
ENDCASE => ERROR;
RETURN [FALSE]}};
FOR
f
x:
LNAT
IN [0 .. a.basePeriod[X])
DO
FOR
f
y:
LNAT
IN [0 .. a.basePeriod[Y])
DO
IF ScanStatEdgesFrom[a.statrep, [cp0, [fx, fy]], ALL[TRUE], TryUpEdge].found THEN ERROR;
ENDLOOP ENDLOOP;
RETURN}};
MakeArrayNewConnection:
PUBLIC
PROC [act: CellType, rangeA: Range2, delta: Int2, epA, epB: Port] ~ {
a: Array ~ act.asArray;
IF delta[X]<0
OR delta[X]=0
AND delta[Y]<0
THEN {
epC: Port ~ epA; epA ← epB; epB ← epC;
rangeA ← Range2Off[rangeA, delta];
delta ← Neg[delta]};
{fullRangeA: Range2 ~ Range2Intersection[SizeRange[a.size2], Range2Off[SizeRange[a.size2], Neg[delta]]];
rangeB: Range2 ~ Range2Off[rangeA, delta];
IF a.buildPhase#buildingStatrep THEN ERROR;
IF ABS[delta[X]]>1 OR ABS[delta[Y]]>1 THEN ERROR;
IF epA=epB AND delta=[0, 0] THEN --this self-connection is always implicitly present, let's not make it explicit-- RETURN;
IF rangeA#fullRangeA THEN ERROR;
FOR
f
f:
NAT
IN [0 .. a.basePeriod[X])
DO
FOR
f
b:
NAT
IN [0 .. a.basePeriod[Y])
DO
fA: Int2 ~ [ff, fb];
fB: Int2 ~ AddMod[fA, delta, a.basePeriod];
svA: StatVertex ~ [epA, fA];
svB: StatVertex ~ [epB, fB];
--the use and/or implementation of these procs rely heavily on AASEU-- IF FindStatEdge[a.statrep, [vs: [svA, svB], d: delta], FALSE].fse=NIL THEN [] ← AddStatEdgeAndClose[act.d, a.statrep, [vs: [svA, svB], d: delta]];
act ← act;
ENDLOOP ENDLOOP;
RETURN}};
FindStatEdge:
PROC [sr: StatRep, sep: StatEdgePrivate, careAboutOthers:
BOOL]
RETURNS [fse: StatEdge ←
NIL, others:
BOOL ←
FALSE] ~ {
TestEdge:
PROC [se: StatEdge, ob:
BOOL]
RETURNS [
BOOL] ~ {
IF NOT (ob OR careAboutOthers) THEN ERROR;
IF ob AND se.vs[TRUE]=sep.vs[TRUE] AND sep.d=se.d THEN {fse ← se; RETURN [NOT careAboutOthers]};
others ← TRUE;
RETURN [FALSE]};
[] ← ScanStatEdgesFrom[sr, sep.vs[FALSE], [FALSE: TRUE, TRUE: careAboutOthers], TestEdge];
RETURN};
ScanStatEdgesFrom:
PROC [sr: StatRep, from: StatVertex, start:
ARRAY
BOOL
OF
BOOL,
Test:
PROC [se: StatEdge, ob:
BOOL]
RETURNS [
BOOL]]
RETURNS [found:
BOOL ←
FALSE, se: StatEdge ←
NIL, ob:
BOOL ←
FALSE] ~ {
FOR ob
IN
BOOL
DO
sb: BOOL ~ NOT ob;
TestEdge:
PROC [ra: Sets.Value]
RETURNS [pass:
BOOL] ~ {
se: StatEdge ~ NARROW[ra.VA];
pass ← se.vs[sb].phase = from.phase AND Test[se, ob];
RETURN};
IF start[sb]
THEN {
mp: BiRels.MaybePair ~ sr.portEdge[sb].ScanMapping[AV[from.port], TestEdge];
IF mp.found THEN RETURN [TRUE, NARROW[mp.it[right].VA], ob]};
ENDLOOP;
RETURN};
AddStatEdgeAndClose:
PROC [d: Design, sr: StatRep, sep: StatEdgePrivate]
RETURNS [se: StatEdge] ~ {
se ← NEW [StatEdgePrivate ← sep];
IF sr.edges.HasMemA[se] THEN ERROR;
sr.portEdge[FALSE].AddNewAA[se.vs[FALSE].port, se];
sr.portEdge[TRUE].AddNewAA[se.vs[TRUE].port, se];
IF NOT sr.edges.AddA[se] THEN ERROR;
IF (sep.vs[FALSE] ← ParentSV[d, sep.vs[FALSE]]).port = NIL THEN GOTO KillKids;
IF (sep.vs[TRUE] ← ParentSV[d, sep.vs[TRUE]]).port = NIL THEN GOTO KillKids;
{width: NATURAL ~ d.Width[sep.vs[FALSE].port];
IF width # d.Width[sep.vs[TRUE].port] THEN GOTO KillKids;
FOR i:
NATURAL
IN [0 .. width)
DO
IF FindStatEdge[sr, ChildSEP[d, sep, i], FALSE].fse=NIL THEN GOTO KillKids;
ENDLOOP;
{pse: StatEdge ~ AddStatEdgeAndClose[d, sr, sep];
RETURN;
}};
EXITS KillKids => RemLowerStateEdges[d, sr, se^];
};
RemLowerStateEdges:
PROC [d: Design, sr: StatRep, sep: StatEdgePrivate] ~ {
kidPortsA: Seq ~ d.SubSeq[sep.vs[FALSE].port];
IF kidPortsA=nilBiRel
THEN {
IF NOT d.Atomic[sep.vs[TRUE].port] THEN ERROR;
RETURN};
{width: LNAT ~ kidPortsA.Size.EN;
IF width # d.Width[sep.vs[TRUE].port] THEN ERROR;
FOR i:
LNAT
IN [0 .. width)
DO
csep: StatEdgePrivate ~ ChildSEP[d, sep, i];
RemStatEdge[d, sr, csep];
RemLowerStateEdges[d, sr, csep];
ENDLOOP;
RETURN}};
RemStatEdge:
PROC [d: Design, sr: StatRep, sep: StatEdgePrivate] ~ {
se: StatEdge ~ FindStatEdge[sr, sep, FALSE].fse;
IF se=NIL THEN ERROR;
IF NOT sr.edges.RemA[se] THEN ERROR;
IF NOT sr.portEdge[FALSE].DeleteA[se, right] THEN ERROR;
IF NOT sr.portEdge[TRUE].DeleteA[se, right] THEN ERROR;
RETURN};
ChildSEP:
PROC [d: Design, sep: StatEdgePrivate, i:
NATURAL]
RETURNS [StatEdgePrivate] ~ {
RETURN [[
vs: [
FALSE: ChildSV[d, sep.vs[FALSE], i],
TRUE: ChildSV[d, sep.vs[TRUE], i] ],
d: sep.d]]};
ChildSV:
PROC [d: Design, sv: StatVertex, i:
NATURAL]
RETURNS [StatVertex] ~ {
RETURN [[NARROW[d.Sub[sv.port, i]], sv.phase]]};
ParentSEP:
PROC [d: Design, sep: StatEdgePrivate]
RETURNS [StatEdgePrivate] ~ {
RETURN [[
vs: [
FALSE: ParentSV[d, sep.vs[FALSE]],
TRUE: ParentSV[d, sep.vs[TRUE]] ],
d: sep.d]]};
ParentSV:
PROC [d: Design, sv: StatVertex]
RETURNS [StatVertex] ~ {
RETURN [[d.PParent[sv.port], sv.phase]]};
END.