private processListTypeDecl()

in impl/src/tooling/verifier/smtdecls_emitter.ts [575:704]
97 lines of code
15 McCabe index (conditional complexity)

    private processListTypeDecl(ldecl: MIRPrimitiveListEntityTypeDecl) {
        const mtype = this.temitter.getMIRType(ldecl.tkey);
        const ltype = this.temitter.getSMTTypeFor(mtype);
        const ctype = this.temitter.getMIRType(ldecl.oftype);
        const nattype = this.temitter.getSMTTypeFor(this.temitter.getMIRType("NSCore::Nat"));
        
        const linfo = this.bemitter.lopsManager.ops.get(ldecl.tkey);
        const constructors: { cname: string, cargs: { fname: string, ftype: SMTType }[] }[] = [];

        ////
        //cons ops

        if(this.bemitter.lopsManager.rangenat && ctype.typeID == this.temitter.getMIRType("NSCore::Nat").typeID) {
            const crange = this.bemitter.lopsManager.emitConstructorRange(mtype, ltype, ctype);
            this.processConstructorGenInfo(crange, constructors);
        }

        if(this.bemitter.lopsManager.rangeint && ctype.typeID == this.temitter.getMIRType("NSCore::Int").typeID) {
            const crange = this.bemitter.lopsManager.emitConstructorRange(mtype, ltype, ctype);
            this.processConstructorGenInfo(crange, constructors);
        }

        const cempty = this.bemitter.lopsManager.emitConstructorEmpty(mtype, ltype);
        this.processConstructorGenInfo(cempty, constructors);

        const cslice = this.bemitter.lopsManager.emitConstructorSlice(mtype, ltype);
        this.processConstructorGenInfo(cslice, constructors);

        const cconcat2 = this.bemitter.lopsManager.emitConstructorConcat2(mtype, ltype);
        this.processConstructorGenInfo(cconcat2, constructors);

        for (let i = 1; i <= 3; ++i) {
            const ck = this.bemitter.lopsManager.emitConstructorLiteralK(mtype, ltype, ctype, i);
            this.processConstructorGenInfo(ck, constructors);
        }

        if(linfo !== undefined) {
            //large consops

            if(linfo.consops.fill) {
                const cfill = this.bemitter.lopsManager.emitConstructorFill(mtype, ltype, ctype);
                this.processConstructorGenInfo(cfill, constructors);
            }
    
            if(linfo.consops.havoc) {
                const chavoc = this.bemitter.lopsManager.emitConstructorHavoc(mtype, ltype, ctype);
                this.processConstructorGenInfo(chavoc, constructors);
            }

            if(linfo.consops.filter) {
                const cfilter = this.bemitter.lopsManager.emitConstructorFilter(ltype, mtype);
                this.processConstructorGenInfo(cfilter, constructors);
            }
    
            linfo.consops.map.forEach((minfo, code) => {
                const cmap = this.bemitter.lopsManager.emitConstructorMap(this.temitter.getSMTTypeFor(minfo.totype), minfo.totype, minfo.fromtype, minfo.isidx, code, minfo.code);
                this.processConstructorGenInfo(cmap, constructors);
            });
        }
            
        ////
        //des ops

        const dget = this.bemitter.lopsManager.emitDestructorGet(ltype, ctype, linfo !== undefined ? linfo.consops : undefined);
        this.processDestructorGenInfo(dget);

        if (linfo !== undefined) {
            linfo.dops.safecheckpred.forEach((pcode, code) => {
                const dsafe = this.bemitter.lopsManager.emitSafeCheckPred(ltype, mtype, pcode.isidx, code, pcode.code);
                this.processDestructorGenInfo(dsafe);
            });

            linfo.dops.safecheckfn.forEach((cinfo, code) => {
                const dsafe = this.bemitter.lopsManager.emitSafeCheckFn(ltype, mtype, cinfo.rtype, cinfo.isidx, code, cinfo.code);
                this.processDestructorGenInfo(dsafe);
            });

            linfo.dops.isequence.forEach((pcode, code) => {
                const disq = this.bemitter.lopsManager.emitDestructorISequence(ltype, pcode.isidx, code, pcode.code);
                this.processDestructorGenInfo(disq);
            });

            linfo.dops.haspredcheck.forEach((pcode, code) => {
                const disq = this.bemitter.lopsManager.emitDestructorHasPredCheck(ltype, pcode.isidx, code, pcode.code);
                this.processDestructorGenInfo(disq);
            });

            linfo.dops.findIndexOf.forEach((pcode, code) => {
                const disq = this.bemitter.lopsManager.emitDestructorFindIndexOf(ltype, pcode.isidx, code, pcode.code);
                this.processDestructorGenInfo(disq);
            });

            linfo.dops.findLastIndexOf.forEach((pcode, code) => {
                const disq = this.bemitter.lopsManager.emitDestructorFindIndexOfLast(ltype, pcode.isidx, code, pcode.code);
                this.processDestructorGenInfo(disq);
            });

            if (linfo.dops.sum) {
                const disq = this.bemitter.lopsManager.emitDestructorSum(ltype, ctype);
                this.processDestructorGenInfo(disq);
            }

            if (linfo.dops.strconcat) {
                const disq = this.bemitter.lopsManager.emitDestructorStrConcat(ltype);
                this.processDestructorGenInfo(disq);
            }

            if (linfo.dops.strjoin) {
                const disq = this.bemitter.lopsManager.emitDestructorStrJoin(ltype);
                this.processDestructorGenInfo(disq);
            }
        }

        const ttag = `TypeTag_${ltype.name}`;
        const iskey = this.temitter.assembly.subtypeOf(mtype, this.temitter.getMIRType("NSCore::KeyType"));

        const consfuncs = this.temitter.getSMTConstructorName(mtype);
        const consdecl = {
            cname: consfuncs.cons, 
            cargs: [
                { fname: `${ltype.name}@size`, ftype: nattype },
                { fname: `${ltype.name}@uli`, ftype: this.bemitter.lopsManager.generateULITypeFor(ltype) }
            ]
        };

        const emptyconst = `(declare-const ${this.temitter.lookupTypeName(ldecl.tkey)}@empty_const ${ltype.name}) (assert (= ${this.temitter.lookupTypeName(ldecl.tkey)}@empty_const (${consfuncs.cons} BNat@zero ${this.bemitter.lopsManager.generateConsCallName_Direct(ltype, "empty")})))`;

        const smtdecl = new SMTListDecl(iskey, this.bemitter.lopsManager.generateULITypeFor(ltype).name, constructors, emptyconst, ltype.name, ttag, consdecl, consfuncs.box, consfuncs.bfield);
        this.assembly.listDecls.push(smtdecl);
    }