public override Expression Resolve()

in ironclad-apps/tools/DafnySpec/DafnySpecAst/DafnySpecAst.cs [514:575]
59 lines of code
42 McCabe index (conditional complexity)

    public override Expression Resolve(Resolver resolver, Type t)
    {
        Type t0 = null;
        Type t1 = null;
        switch (Op)
        {
            case Opcode.Iff: case Opcode.Imp: case Opcode.Exp: case Opcode.And: case Opcode.Or:
                t0 = Type.Bool;
                t1 = Type.Bool;
                Type = Type.Bool;
                break;
            case Opcode.Eq: case Opcode.Neq: Type = Type.Bool; break;
            case Opcode.Le: case Opcode.Lt: case Opcode.Ge: case Opcode.Gt:
                t0 = Type.Int;
                t1 = Type.Int;
                Type = Type.Bool;
                break;
            case Opcode.Sub: case Opcode.Mul: case Opcode.Div: case Opcode.Mod:
                t0 = Type.Int;
                t1 = Type.Int;
                Type = Type.Int;
                break;
        }
        switch (Op)
        {
            case Opcode.Eq: case Opcode.Neq: case Opcode.Le: case Opcode.Lt: case Opcode.Ge: case Opcode.Gt:
                //- ((a < b) < c) < d
                //- -->
                //- ((a < b) < c) && c < d
                BinaryExpr B0 = E0 as BinaryExpr;
                if (B0 != null)
                {
                    switch (B0.Op)
                    {
                        case Opcode.Eq: case Opcode.Neq: case Opcode.Le: case Opcode.Lt: case Opcode.Ge: case Opcode.Gt:
                            Expression _e0 = B0;
                            Expression _e1 = new BinaryExpr(tok, Op, B0.E1, E1);
                            Expression _e = new BinaryExpr(tok, Opcode.And, _e0, _e1);
                            return _e.Resolve(resolver, Type.Bool);
                    }
                }
                break;
        }
        E0 = E0.Resolve(resolver, t0);
        E1 = E1.Resolve(resolver, t1);
        if (E0.Type == null) { E0 = E0.Resolve(resolver, E1.Type); } // HACK
        if (E1.Type == null) { E1 = E1.Resolve(resolver, E0.Type); } // HACK
        switch (Op)
        {
            case Opcode.Add:
                if (E0.Type is SeqType) { ResolvedOp = ResolvedOpcode.Concat; Type = E0.Type; }
                else if (E0.Type is RealType) { Type = E0.Type; }
                else { Type = Type.Int; }
                break;
            case Opcode.Sub: case Opcode.Mul: case Opcode.Div:
                if (E0.Type is RealType) { Type = E0.Type; }
                break;
            case Opcode.Eq: if (E0.Type is SeqType) { ResolvedOp = ResolvedOpcode.SeqEq; } break;
            case Opcode.Neq: if (E0.Type is SeqType) { ResolvedOp = ResolvedOpcode.SeqNeq; } break;
        }
        return this;
    }