
    <<LichenChecking.Mesa>>
        <<Mike Spreitzer January 27, 1987 12:32:44 pm PST>>
        <<Last tweaked by Mike Spreitzer on April 7, 1987 3:11:26 pm PDT>>

    DIRECTORY Asserting, GList, LichenArrayStuff, LichenDataOps, LichenDataStructure, LichenSetTheory, Rope;

    LichenChecking: CEDAR PROGRAM
        IMPORTS Asserting, LichenArrayStuff, LichenDataOps, LichenDataStructure, LichenSetTheory, Rope
        EXPORTS LichenDataOps =

        BEGIN OPEN LichenSetTheory, LichenDataOps, LichenArrayStuff, LichenDataStructure;

    <<When in rep-normal form:>>
    <<ANHighestBindingRepd: The binding between ports and wires is represented as `highly' as possible.>>
    <<>>
    <<(>>
    <<(>>
    <<When in circuit-normal form:>>
    <<ANNetUsed: Each net has a part attached to at least one thing.>>
    <<>>
    <<(note that we allow a ci to be >>
    <<ANPortUsedI: Each port is internally attached to something.>>
    <<>>
    <<ANPortsMergedI: Each net is connected to at most one port.>>
    <<>>
    <<Implies nets merged.>>
    <<The following duals are NOT required to be true:>>
    <<ANPortUsedO: Each port is used for something interesting at least once.>>
    <<>>
    <<ANPortsMergedO: Each port distinction is used at least once.>>
    <<>>
    <<For a design to be comparable, we must also have:>>
    <<ACCellTypeEquivd: The structural equivalence class of a cell type is clear.>>
    <<ct.equivClass # implicitClass COR |ct.names.designed| = 1 OR |ct.names.designed| = 0 CAND (|ct.names.unknown| = 1 OR 
    |ct.names.unknown| = 0 CAND |ct.names.progged| = 1)>>
    <<ACPortEquivd: The structural equivalence class of a port is clear.>>
    <<p.equivClass # implicitClass COR |p.names.designed| = 1 OR |p.names.designed| = 0 CAND (|p.names.unknown| = 1 OR 
    |p.names.unknown| = 0 CAND |p.names.progged| = 1)>>

        PortList: TYPE = LIST OF Port;

        debugging: BOOL _ TRUE;
        OutersToo: BOOL = FALSE;

        CheckDesign: PUBLIC PROC [design: Design, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp] = {
            PerCellType: PROC [ct: CellType] = {
                CheckCellType[ct, rep, norm, comparable];
                };
            SELECT norm FROM
                ignore => NULL;
                report, check, establish => EnsureAllIn[design];
                ENDCASE => ERROR;
            EnumerateCellTypes[design, PerCellType];
            };

        PortData: TYPE = RefTable--port 
        PortDatum: TYPE = REF PortDatumPrivate;
        PortDatumPrivate: TYPE = RECORD [
            used, seen, deleted: BOOL _ FALSE,
            assoc: PortList _ NIL,
            newPort: Port _ NIL];

        CheckCellType: PUBLIC PROC [ct: CellType, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, interface, internals, 
        instances: BOOL _ TRUE] = {
            portData: PortData;
            consequences: RefTable = SELECT norm FROM
                establish => CreateRefTable[],
                ignore, report, check => NIL,
                ENDCASE => ERROR;
            altered: BOOL _ FALSE;
            SELECT norm FROM
                ignore, report, check => NULL;
                establish => IF NOT (interface AND internals AND instances) THEN ERROR;
                ENDCASE => ERROR;
            IF ct.privateKnown AND NOT ct.publicKnown THEN ERROR Error["Broken: private parts known but not the public"];
            IF internals THEN EnsurePrivate[ct];
            EnsurePublic[ct];
            IF ct.privateKnown AND NOT ct.publicKnown THEN ERROR Error["Broken: private parts known but not the public"];
            IF interface THEN {
                CheckPort: PROC [port: Port] = {
                    WITH port.parent SELECT FROM
                        pp: Port => {
                            IF (IF port.prev # NIL THEN port.prev.next ELSE pp.firstChild) # port THEN ERROR Error["Broken"];
                            IF (IF port.next # NIL THEN port.next.prev ELSE pp.lastChild) # port THEN ERROR Error["Broken"];
                            };
                        ct: CellType => {
                            IF port.next # NIL OR port.prev # NIL THEN ERROR Error["Broken"];
                            IF ct.port # port THEN ERROR Error["Broken"];
                            };
                        ENDCASE => ERROR;
                    IF (port.firstChild # NIL) # (port.lastChild # NIL) THEN ERROR Error["Broken"];
                    };
                EnumeratePorts[ct, CheckPort];
                };
            IF instances THEN {
                SELECT norm FROM
                    ignore => NULL;
                    report, check, establish => {
                        ct.wasntNormalized _ FALSE;
                        portData _ CreatePortData[ct];
                        };
                    ENDCASE => ERROR;
                IF (ct.firstInstance # NIL AND ct.firstInstance.prevInstance # NIL) OR (ct.lastInstance # NIL AND ct.lastInstance.nextInstance # 
                NIL) THEN ERROR Error["Broken: cell type - instance linkage"];
                {useCount: INT _ 0;
                PerInstance: PROC [v: CellInstance] = {
                    IF v.type # ct THEN ERROR Error["Broken"];
                    IF IsMirror[v] THEN ERROR Error["Broken"];    --AM2
                    CheckInstance[v, portData, rep, norm];
                    useCount _ useCount + 1;
                    };
                PerArray: PROC [act: CellType] = {
                    a: Array = act.asArray;
                    IF a=NIL OR a.eltType # ct THEN ERROR Error["Broken"];
                    useCount _ useCount + 1;
                    };
                EnumerateInstances[ct, PerInstance];
                EnumerateArrays[ct, PerArray];
                IF useCount # ct.useCount THEN ERROR Error["Broken"];
                };
                SELECT norm FROM
                    ignore => NULL;
                    report, check => IF OutersToo THEN {
                        PerPortDatum: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
                            port: Port =  NARROW[key];
                            pd: PortDatum = NARROW[val];
                            IF NOT pd.used THEN Fail[normal, norm, "%g fails ANPortUsedO", port];
                            IF pd.assoc # NIL THEN Fail[normal, norm, "%g fails ANPortsMergedO", port];
                                <<Note that we depend on ANPortsMergedO being true for some other cellTypes, and ANPortsMergedI being true for this and some other 
                                cellTypes, in making this test.>>
                            };
                        [] _ portData.Pairs[PerPortDatum];
                        };
                    establish => IF OutersToo THEN {
                        PerPort: PROC [port: Port] = {
                            pd: PortDatum = NARROW[portData.Fetch[port].val];
                            IF (NOT pd.used) AND (pd.assoc # NIL) THEN ERROR;
                            IF NOT pd.used THEN {
                                IF debugging THEN Log["Deleting port %g.\n", port];
                                DeletePort[ct, port, consequences];
                                ct.wasntNormalized _ TRUE;
                                CheckCellType[ct, ignore, ignore, comparable]}
                            ELSE IF pd.assoc # NIL THEN {
                                IF debugging THEN Log["On Type %g, merging ports %g.\n", ct, pd.assoc];
                                MergePorts[ct, CONS[port, pd.assoc], portData, consequences];
                                ct.wasntNormalized _ TRUE;
                                CheckCellType[ct, ignore, ignore, comparable]};
                            };
                        EnumeratePorts[ct, PerPort];
                        };
                    ENDCASE => ERROR;
                };
            IF internals AND ct.asUnorganized # NIL THEN {
                PerInstance: PROC [elt: REF ANY] = {
                    ci: CellInstance = NARROW[elt];
                    IF ci.containingCT # ct THEN ERROR Error["Broken"];
                    IF IsMirror[ci] THEN ERROR Error["Broken"]--AM1--;
                    CheckComponent[ci, rep];
                    };
                IF ct.asUnorganized.mirror = NIL THEN ERROR Error["Broken"];
                IF ct.asUnorganized.mirror.type # ct THEN ERROR Error["Broken"]; --AM3
                IF ct.asUnorganized.mirror.containingCT # ct THEN ERROR Error["Broken"];
                IF CheckNet[ct.asUnorganized.internalWire, norm, comparable, consequences] THEN altered _ TRUE;
                ct.asUnorganized.containedInstances.Enumerate[PerInstance];
                CheckComponent[ct.asUnorganized.mirror, rep];
                };
            IF internals AND ct.asArray # NIL THEN CheckArray[ct];
            IF instances THEN SELECT norm FROM
                ignore => NULL;
                report, check => IF ct.wasntNormalized THEN ERROR Error["Broken"];
                establish => {
                    SELECT consequences.Fetch[ct].val FROM
                        $T => {
                            [] _ consequences.Delete[ct];
                            CheckCellType[ct, ignore, establish, comparable];
                            };
                        ENDCASE => IF ct.wasntNormalized THEN CheckCellType[ct, ignore, check, comparable];
                    [] _ consequences.Pairs[FixAffectedType];
                    };
                ENDCASE => ERROR;
            };

        CheckArray: PROC [ct: CellType] = {
            a: Array = ct.asArray;
            FOR d: Dim IN Dim DO
                gp: GroupingParms = a.groupingParmses[d];
                hasMiddle: BOOL = gp.middle.maxPlusOne > gp.middle.min;
                peculiar: INT = gp.middle.min + a.size[d] - gp.middle.maxPlusOne;
                nMid: NAT = IF hasMiddle THEN a.jointsPeriod[d] ELSE 0;
                firstHigh: INT = gp.middle.min + nMid;
                IF
                    gp.middle.min < 0 OR
                    gp.middle.maxPlusOne > a.size[d] OR
                    gp.middle.maxPlusOne < gp.middle.min OR
                    gp.firstHigh # firstHigh OR
                    gp.sum # peculiar + nMid OR
                    gp.d # firstHigh - gp.middle.maxPlusOne
                    THEN ERROR Error["Broken"];
                IF a.nextRP[d] # a.roles[d].length THEN ERROR Error["Broken"];
                FOR index: NAT IN [0 .. a.roles[d].length) DO
                    rpd: SidedPortData = NARROW[a.roles[d].refs[index]];
                    IF rpd # NIL AND (
                        rpd.index # index OR
                        a.toRole[d][rpd.side].Fetch[rpd.port].val # rpd OR
                        (index#0 AND rpd.links = NIL AND RPDNeedsLinks[a, d, rpd]))
                    THEN ERROR Error["Broken"];
                    ENDLOOP;
                FOR side: End IN End DO
                    CheckToRole: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
                        port: Port = NARROW[key];
                        rpd: SidedPortData = NARROW[val];
                        IF rpd.side # side OR rpd.port # port OR rpd.index >= a.nextRP[d] THEN ERROR Error["Broken"];
                        };
                    IF a.toRole[d][side].Pairs[CheckToRole] THEN ERROR;
                    ENDLOOP;
                FOR 
                    phase: Nat2 = [
                    j: Joint = GetArrayJoint[a, d, phase];
                    rawLair: Range2 = IF d = Foo
                        THEN [[0, a.size[Foo]-1], [0, a.size[Bar]-0]]
                        ELSE [[0, a.size[Foo]-0], [0, a.size[Bar]-1]];
                    jiir: Range2 = Range2Div[r: rawLair, 
                    size2: Size2 = RangeShape[jiir];
                    middle: Range2 = Range2Div[r: [a.groupingParmses[Foo].middle, a.groupingParmses[Bar].middle], 
                    IF jiir[Foo].min # 0 OR jiir[Bar].min # 0 THEN ERROR;
                    IF
                        j = NIL OR
                        j.size # j.size2[Foo]*j.size2[Bar] OR
                        j.size2 # size2
                        THEN ERROR Error["Broken"];
                    FOR dc: Dim IN Dim DO
                        IF
                            j.groupingParmses[dc].middle # middle[dc]
                            THEN ERROR Error["Broken"];
                        ENDLOOP;
                    ENDLOOP ENDLOOP;
                ENDLOOP;
            };

        CheckWireAgainstPort: PROC [wire: Wire, port: Port, andInsertIn: Set] = {
            subWire: Wire _ wire.firstChild;
            subPort: Port _ port.firstChild;
            [] _ andInsertIn.UnionSingleton[port];
            WHILE subWire # NIL AND subPort # NIL DO
                CheckWireAgainstPort[subWire, subPort, andInsertIn];
                subWire _ subWire.next;
                subPort _ subPort.next;
                ENDLOOP;
            IF subWire # NIL OR subPort # NIL THEN ERROR Error["Broken: Wire %g doesn't match port %g", wire, port];
            };

        CheckInstance: PROC [v: CellInstance, portData: PortData, rep, norm: AssertionOp] = {
            CheckComponent[v, rep];
            SELECT norm FROM
                ignore => NULL;
                report, check, establish => {
                    PerConnection: PROC [port: Port, net: Vertex] = {
                        pd: PortDatum = NARROW[portData.Fetch[port].val];
                        ClearSeen: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
                            pd: PortDatum = NARROW[val];
                            pd.seen_ FALSE;
                            };
                        PerNetConnection: PROC [port2: Port, u: Vertex] = {
                            pd2: PortDatum = NARROW[portData.Fetch[port2].val];
                            IF u = v THEN pd2.seen _ TRUE;
                            IF u # v OR port2 # port THEN pd.used _ TRUE;
                            };
                        [] _ portData.Pairs[ClearSeen];
                        EnumerateImmediateConnections[net, PerNetConnection];
                        IF NOT pd.seen THEN ERROR Error["Broken: Port %g half connected to", port];
                        IF v = v.type.firstInstance THEN {
                            StartAssoc: PROC [port2: Port] = {
                                pd2: PortDatum = NARROW[portData.Fetch[port2].val];
                                IF pd2.seen AND port # port2 THEN pd.assoc _ CONS[port2, pd.assoc];
                                };
                            pd.assoc _ NIL;
                            EnumeratePorts[v.type, StartAssoc];
                            }
                        ELSE {
                            lastAssoc: PortList _ NIL;
                            FOR la: PortList _ pd.assoc, la.rest WHILE la # NIL DO
                                pd2: PortDatum = NARROW[portData.Fetch[la.first].val];
                                IF NOT pd2.seen THEN {
                                    IF lastAssoc = NIL THEN pd.assoc _ la.rest ELSE lastAssoc.rest _ la.rest
                                    }
                                ELSE lastAssoc _ la;
                                ENDLOOP;
                            };
                        };
                    EnumerateImmediateConnections[v, PerConnection];
                    };
                ENDCASE => ERROR;
            };

        CheckIntermediate: PROC [im: Intermediary] = {
            NULL --er, nothing to do here, since the intermediates are checked as part of the cell instance checking, uh, right?--;
            };

        CheckNet: PROC [v: Wire, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, noteIn: RefTable] RETURNS [altered: BOOL] = {
            Work: PROC [v: Wire] RETURNS [portSeen, otherSeen, portUsed: BOOL _ FALSE] = {
                portCount, otherCount: NAT _ 0;
                ports: PortList _ NIL;
                iAmPorted, anNetUsed, anPortUsedI: BOOL;
                SeekPortage: PROC [port: Port, w: Vertex] = {
                    ci: CellInstance = NARROW[w];
                    IF IsMirror[ci] THEN {
                        portCount _ portCount + 1;
                        ports _ CONS[port, ports];
                        portSeen _ TRUE;
                        }
                    ELSE {otherCount _ otherCount + 1; otherSeen _ TRUE};
                    };
                EnumerateTransitiveConnections[v, SeekPortage];
                iAmPorted _ portSeen;
                portUsed _ iAmPorted AND portCount + otherCount > 1;
                IF portCount > 1 THEN SELECT norm FROM
                    ignore => ERROR;
                    report, check => Fail[normal, norm, "%g fails ANPortsMergedI", v];
                    establish => {
                        IF debugging THEN Log["Merging ports %g.\n", ports];
                        altered _ TRUE;
                        [] _ noteIn.Store[v.containingCT, $T];
                        [] _ MergePorts[v.containingCT, ports, NIL, noteIn];
                        v.containingCT.wasntNormalized _ TRUE;
                        CheckCellType[v.containingCT, ignore, ignore, comparable];
                        };
                    ENDCASE => ERROR;
                FOR subWire: Wire _ v.FirstChildWire[], subWire.NextChildWire[] WHILE subWire # NIL DO
                    subPortSeen, subOtherSeen, subPortUsed: BOOL;
                    [subPortSeen, subOtherSeen, subPortUsed] _ Work[subWire];
                    portSeen _ portSeen OR subPortSeen;
                    otherSeen _ otherSeen OR subOtherSeen;
                    portUsed _ portUsed OR subPortUsed;
                    ENDLOOP;
                anNetUsed _ portSeen OR otherSeen;
                anPortUsedI _ portCount = 0 OR portUsed;
                SELECT norm FROM
                    ignore => ERROR;
                    report, check => {
                        IF NOT anNetUsed THEN Fail[normal, norm, "%g fails ANNetUsed", v];
                        IF NOT anPortUsedI THEN Fail[normal, norm, "%g fails ANPortUsedI", ports.first];
                        };
                    establish => {
                        IF NOT anNetUsed THEN {
                            IF debugging THEN Log["Deleting net %g.\n", v];
                            altered _ TRUE;
                            [] _ noteIn.Store[v.containingCT, $T];
                            DeleteVertex[v];
                            v.containingCT.wasntNormalized _ TRUE;
                            CheckCellType[v.containingCT, ignore, ignore, comparable]};
                        IF NOT anPortUsedI THEN {
                            IF debugging THEN Log["Deleting port %g.\n", ports.first];
                            altered _ TRUE;
                            [] _ noteIn.Store[v.containingCT, $T];
                            [] _ DeletePort[v.containingCT, ports.first, noteIn];
                            v.containingCT.wasntNormalized _ TRUE;
                            CheckCellType[v.containingCT, ignore, ignore, comparable]};
                        };
                    ENDCASE => ERROR;
                };
            altered _ FALSE;
            IF norm = ignore THEN RETURN;
            [] _ Work[v];
            };

        CheckComponent: PROC [v: CellInstance, rep: AssertionOp] = {
            portsConnected: Set = CreateHashSet[];
            altered: BOOL _ FALSE;
            CheckConnections: PROC [port: Port, cellward, v: Vertex] = {
                containingWire, subWire: Wire _ NIL;
                first, match: BOOL _ TRUE;
                PerConnection: PROC [port: Port, w: Vertex] = {
                    IF NOT portsConnected.UnionSingleton[port] THEN ERROR Error["Broken: Port %g multiply connected on cell instance %g", port, v];
                    WITH w SELECT FROM
                        wire: Wire => {
                            IF first THEN {subWire _ wire; first _ FALSE} ELSE IF match AND wire # (subWire _ NextChildWire[subWire]) THEN match _ FALSE;
                            CheckWireAgainstPort[wire, port, portsConnected];
                            };
                        im: Intermediary => {
                            match _ first _ FALSE;
                            CheckConnections[port, v, im];
                            };
                        ci: CellInstance => {
                            ERROR Error["Broken: Found cell instance %g on wireward end of an edge from cell instance %g", ci, v];
                            };
                        ENDCASE => ERROR;
                    };
                EnumerateImmediateConnections[v, PerConnection, [cellward: FALSE, wireward: TRUE], forward];
                IF first THEN ERROR Error["Broken"];
                IF match AND NextChildWire[subWire] # NIL THEN match _ FALSE;
                IF match AND cellward # NIL THEN {
                    containingWire _ subWire.containingWire;
                    SELECT rep FROM
                        ignore => NULL;
                        report, check => Fail[rep, rep, "Effective connection between port %g and wire %g not represented", port, containingWire];
                        establish => {
                            Unlinkem: PROC [port: Port, w: Vertex, e: Edge] = {RemoveEdge[e]};
                            IF debugging THEN Log["Making connection between port %g and wire %g.\n", port, containingWire];
                            EnumerateImmediateEdges[v, Unlinkem, [cellward: FALSE, wireward: TRUE]];
                            AddEdge[[cellward: cellward, wireward: containingWire], port];
                            altered _ TRUE;
                            };
                        ENDCASE => ERROR;
                    };
                };
            PerPort: PROC [port: Port] = {
                IF portsConnected.HasMember[port] # (port # v.type.port) THEN ERROR Error["Broken: Port %g not properly covered by connections to 
                cell instance %g", port, v];
                };
            SELECT IsMirror[v] FROM
                FALSE => {
                    IF (IF v.prevInstance # NIL THEN v.prevInstance.nextInstance ELSE v.type.firstInstance) # v THEN ERROR Error["Broken: Cell type - 
                    instance linkage"];
                    IF (IF v.nextInstance # NIL THEN v.nextInstance.prevInstance ELSE v.type.lastInstance) # v THEN ERROR Error["Broken: Cell type - 
                    instance linkage"];
                    };
                TRUE => {
                    IF v.prevInstance # NIL OR v.nextInstance # NIL OR v.type.firstInstance = v OR v.type.lastInstance = v THEN ERROR Error["Broken: 
                    Mirror %g linked among instances of cell type %g", v, v.type];
                    };
                ENDCASE => ERROR;
            EnsurePublic[v.type];
            CheckConnections[v.type.port, NIL, v];
            EnumeratePorts[v.type, PerPort];
            portsConnected.DestroySet[];
            IF altered THEN CheckComponent[v, check];
            };

        MergeNets: PUBLIC PROC [net1, net2: Wire] RETURNS [merged, doomed: Wire] =
            BEGIN
            MoveToMerged: PROC [port: Port, w: Vertex, e: Edge] = {
                e.sides[wireward].v _ merged;
                };
            PerName: PROC [assertion: Asserting.Assertion] = {
                name: ROPE = NARROW[Asserting.TermsOf[assertion].first];
                KnowVertexName[merged, name];
                };
            IF net1.containingCT # net2.containingCT THEN ERROR;
            IF net1 = net2 THEN RETURN [net1, NIL];
            merged _ net1;
            doomed _ net2;
            EnumerateImmediateEdges[doomed, MoveToMerged];
            IF doomed.firstEdge # NIL THEN {
                IF merged.lastEdge # NIL THEN merged.lastEdge.sides[wireward].next _ doomed.firstEdge ELSE merged.firstEdge _ doomed.firstEdge;
                merged.lastEdge _ doomed.lastEdge;
                doomed.firstEdge.sides[wireward].prev _ merged.lastEdge;
                doomed.firstEdge _ NIL;
                doomed.lastEdge _ NIL;
                };
            DeleteVertex[doomed];
            Asserting.EnumerateAssertionsAbout[nameReln, doomed.other, PerName];
            END;

        MergePorts: PROC [ct: CellType, ports: PortList, portData: PortData, noteIn: RefTable] = {
            Length: PROC [ln: PortList] RETURNS [len: NAT _ 0] =
                {FOR ln _ ln, ln.rest WHILE ln # NIL DO len _ len+1 ENDLOOP};
            numIndices: NAT = Length[ports];
            oldPorts: Port = ct.port;
            newPorts: Port = oldPorts;
            updatePortData: BOOL = portData # NIL;
            surviver: Port = ports.first;
            siNet: Wire;
            designed, unked, progged, recent, old: LIST OF NAT _ NIL;
            oldest: INTEGER _ 0;
            newPI: NAT _ 0;
            ClearSeen: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ FALSE] --HashTable.EachPairAction-- = {
                pd: PortDatum = NARROW[val];
                pd.seen_ FALSE;
                };
            IF numIndices < 2 THEN ERROR;
            IF numIndices >= 2 AND portData # NIL THEN ERROR--code below might exhibit bugs--;
            IF portData = NIL THEN portData _ CreatePortData[ct];
            [] _ portData.Pairs[ClearSeen];
            FOR pil: PortList _ ports, pil.rest WHILE pil # NIL DO
                pd: PortDatum = NARROW[portData.Fetch[pil.first].val];
                IF pd.seen THEN ERROR Error["Broken"];
                pd.seen _ TRUE;
                ENDLOOP;
            IF surviver = NIL THEN ERROR Error["Broken"];
            [] _ portData.Pairs[ClearSeen];
            FOR pil: PortList _ ports, pil.rest WHILE pil # NIL DO
                pd: PortDatum = NARROW[portData.Fetch[pil.first].val];
                IF pil.first # surviver THEN {
                    pd.seen _ TRUE;
                    };
                ENDLOOP;
            {InitPortDatum: PROC [port: Port] = {
                pd: PortDatum = NARROW[portData.Fetch[port].val];
                IF port = surviver OR NOT pd.seen THEN pd.newPort _ port
                ELSE pd.newPort _ NIL;
                };
            EnumeratePorts[ct, InitPortDatum]};
            IF ExpansionKnown[ct] THEN {
                InnerCleanup: PROC [ip: Port, w: Vertex, e: Edge] = {
                    iNet: Wire = NARROW[w];
                    pd: PortDatum = NARROW[portData.Fetch[ip].val];
                    IF pd.seen AND iNet # siNet THEN {
                        RemoveEdge[e];
                        [] _ MergeNets[siNet, iNet]}
                    };
                siNet _ NARROW[FindImmediateConnection[ct.asUnorganized.mirror, surviver]];
                EnumerateImmediateEdges[ct.asUnorganized.mirror, InnerCleanup];
                };
            {FixInstance: PROC [v: CellInstance] = {
                soNet: Wire = NARROW[FindImmediateConnection[v, surviver]];
                OuterCleanup: PROC [op: Port, w: Vertex, e: Edge] = {
                    oNet: Wire = NARROW[w];
                    pd: PortDatum = NARROW[portData.Fetch[op].val];
                    IF pd.seen AND oNet # soNet THEN {
                        RemoveEdge[e];
                        [] _ MergeNets[soNet, oNet]}
                    };
                EnumerateImmediateEdges[v, OuterCleanup];
                [] _ noteIn.Store[v.containingCT, $T];
                };
            EnumerateInstances[ct, FixInstance]};
            IF updatePortData THEN {
                FixPortDatum: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ FALSE] -- HashTable.EachPairAction-- = {
                    port: Port = NARROW[key];
                    pd: PortDatum = NARROW[val];
                    IF NOT pd.seen THEN {
                        oldAssoc: PortList _ pd.assoc;
                        pd.assoc _ NIL;
                        FOR oldAssoc _ oldAssoc, oldAssoc.rest WHILE oldAssoc # NIL DO
                            pd2: PortDatum = NARROW[portData.Fetch[oldAssoc.first].val];
                            SELECT TRUE FROM
                                oldAssoc.first = port => ERROR Error["Broken"];
                                pd2.newPort = NIL => NULL;
                                pd2.newPort # NIL => pd.assoc _ CONS[pd2.newPort, pd.assoc];
                                ENDCASE => ERROR Error["Broken"];
                            ENDLOOP;
                        };
                    };
                [] _ portData.Pairs[FixPortDatum];
                };
            };

        DeletePort: PROC [ct: CellType, port: Port, noteIn: RefTable] = {
            FixInstance: PROC [v: CellInstance] = {
                UnlinkPort[v, port];
                [] _ noteIn.Store[v.containingCT, $T];
                };
            IF ExpansionKnown[ct] THEN UnlinkPort[ct.asUnorganized.mirror, port];
            EnumerateInstances[ct, FixInstance];
            };

        FixAffectedType: PROC [key, val: REF ANY] RETURNS [quit: BOOL _ TRUE] = {
            parent: CellType = NARROW[key];
            CheckCellType[parent, ignore, establish, ignore]};

        CheckCellTypes: PUBLIC PROC [cts: Set--of CellType--, rep, norm: AssertionOp, comparable: MerelyCheckableAssertionOp, interface, 
        internals, instances: BOOL _ TRUE] = {
            Checkit: PROC [ra: REF ANY] = {
                ct: CellType = NARROW[ra];
                CheckCellType[ct, rep, norm, comparable, interface, internals, instances];
                };
            cts.Enumerate[Checkit];
            };

        ToAO: PROC [ra: REF ANY] RETURNS [ao: AssertionOp] = {
            ao _ SELECT ra FROM
                $ignore => ignore,
                $report => report,
                $check => check,
                $establish => establish,
                ENDCASE => ERROR};

        ToBOOL: PROC [ra: REF ANY] RETURNS [b: BOOL] = {
            b _ SELECT ra FROM
                $FALSE => FALSE,
                $TRUE => TRUE,
                ENDCASE => ERROR};

        AssertionFamily: TYPE = {rep, normal, comparable};
        AssertionFamilyComplaints: ARRAY AssertionFamily OF ROPE = [
            rep: "RepNotNormal: ",
            normal: "NotNormal: ",
            comparable: "NotComparable: "];

        Fail: PROC [af: AssertionFamily, ao: FailableAssertionOp, msg: ROPE, v1, v2, v3, v4, v5: REF ANY _ NIL] = {
            msg _ AssertionFamilyComplaints[af].Concat[msg];
            SELECT ao FROM
                report => SIGNAL Warning[msg, v1, v2, v3, v4, v5];
                check => ERROR Error[msg, v1, v2, v3, v4, v5];
                ENDCASE => ERROR;
            };

        CreatePortData: PROC [ct: CellType] RETURNS [portData: PortData] = {
            InitPortDatum: PROC [port: Port] = {
                pd: PortDatum = NEW [PortDatumPrivate _ []];
                [] _ portData.Insert[port, pd]};
            portData _ CreateRefTable[];
            EnumeratePorts[ct, InitPortDatum];
            };

        END.