List GenerateAutoReqs()

in ironclad-apps/tools/DafnySpec/ParseMain.cs [174:329]
156 lines of code
36 McCabe index (conditional complexity)

    List<Expression> GenerateAutoReqs(Expression expr, Function parent)
    {
        List<Expression> reqs = new List<Expression>();
        Func<Expression,List<Expression>> generateAutoReqs = e => GenerateAutoReqs(e, parent);
        if (expr is LiteralExpr)
        {
        }
        else if (expr is ThisExpr)
        {
        }
        else if (expr is IdentifierExpr)
        {
        }
        else if (expr is SeqDisplayExpr)
        {
            SeqDisplayExpr e = (SeqDisplayExpr)expr;
            foreach (var elt in e.Elements)
            {
                reqs.AddRange(generateAutoReqs(elt));
            }
        }
        else if (expr is MemberSelectExpr && ((MemberSelectExpr)expr).Member is Field)
        {
            MemberSelectExpr e = (MemberSelectExpr)expr;
            reqs.AddRange(generateAutoReqs(e.Obj));
        }
        else if (expr is SeqSelectExpr)
        {
            SeqSelectExpr e = (SeqSelectExpr)expr;
            reqs.AddRange(generateAutoReqs(e.Seq));
            if (e.E0 != null)
            {
                reqs.AddRange(generateAutoReqs(e.E0));
            }
            if (e.E1 != null)
            {
                reqs.AddRange(generateAutoReqs(e.E1));
            }
        }
        else if (expr is SeqUpdateExpr)
        {
            SeqUpdateExpr e = (SeqUpdateExpr)expr;
            reqs.AddRange(generateAutoReqs(e.Seq));
            reqs.AddRange(generateAutoReqs(e.Index));
            reqs.AddRange(generateAutoReqs(e.Value));
        }
        else if (expr is FunctionCallExpr)
        {
            FunctionCallExpr e = (FunctionCallExpr)expr;
            foreach (var arg in e.Args)
            {
                reqs.AddRange(generateAutoReqs(arg));
            }
            if (parent == null || parent.Name != e.name)
            {
                ReqFunction(e.Function);
                reqs.AddRange(GatherReqs(e.Function, e.Args));
            }
        }
        else if (expr is DatatypeValue)
        {         
            DatatypeValue dtv = (DatatypeValue)expr;
            for (int i = 0; i < dtv.Arguments.Count; i++)
            {
                Expression arg = dtv.Arguments[i];
                reqs.AddRange(generateAutoReqs(arg));
            }
        }
        else if (expr is OldExpr)
        {
        }
        else if (expr is MatchExpr)
        {
            MatchExpr e = (MatchExpr)expr;
            reqs.AddRange(generateAutoReqs(e.Source));
            List<MatchCaseExpr> newMatches = new List<MatchCaseExpr>();
            foreach (MatchCaseExpr caseExpr in e.Cases)
            {
                MatchCaseExpr c = new MatchCaseExpr(caseExpr.name, caseExpr.Arguments, Andify(generateAutoReqs(caseExpr.Body)));
                newMatches.Add(c);
            }
            reqs.Add(new MatchExpr(e.Source, newMatches));
        }
        else if (expr is UnaryOpExpr)
        {
            UnaryOpExpr e = (UnaryOpExpr)expr;
            Expression arg = e.E;            
            reqs.AddRange(generateAutoReqs(arg));
        }
        else if (expr is BinaryExpr)
        {
            BinaryExpr e = (BinaryExpr)expr;
            switch (e.Op)
            {
                case BinaryExpr.Opcode.Imp:
                case BinaryExpr.Opcode.And:
                    reqs.AddRange(generateAutoReqs(e.E0));
                    foreach (var req in generateAutoReqs(e.E1))
                    {
                        reqs.Add(new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp, e.E0, req));
                    }
                    break;
                case BinaryExpr.Opcode.Or:
                    reqs.AddRange(generateAutoReqs(e.E0));
                    foreach (var req in generateAutoReqs(e.E1))
                    {
                        reqs.Add(new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Imp,
                            new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Not, e.E0), req));
                    }
                    break;
                default:
                    reqs.AddRange(generateAutoReqs(e.E0));
                    reqs.AddRange(generateAutoReqs(e.E1));
                    break;
            }
        }
        else if (expr is LetExpr)
        {
            var e = (LetExpr)expr;
            if (e.Exact)
            {
                foreach (var rhs in e.RHSs)
                {
                    reqs.AddRange(generateAutoReqs(rhs));
                }
                var new_reqs = generateAutoReqs(e.Body);
                if (new_reqs.Count > 0)
                {
                    reqs.Add(new LetExpr(e.Exact, e.LHSs, e.RHSs, Andify(new_reqs)));
                }
            }
        }
        else if (expr is QuantifierExpr)
        {
            QuantifierExpr e = (QuantifierExpr)expr;
            var auto_reqs = generateAutoReqs(e.Term);
            if (auto_reqs.Count > 0)
            {
                Expression allReqsSatisfied = Andify(auto_reqs);
                Expression allReqsSatisfiedAndTerm = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, allReqsSatisfied, e.Term);
                e.Term = allReqsSatisfiedAndTerm;
            }
        }
        else if (expr is StmtExpr)
        {
            var e = (StmtExpr)expr;
            reqs.AddRange(generateAutoReqs(e.E));
        }
        else if (expr is ITEExpr)
        {
            ITEExpr e = (ITEExpr)expr;
            reqs.AddRange(generateAutoReqs(e.Test));
            reqs.Add(new ITEExpr(e.Test, Andify(generateAutoReqs(e.Thn)), Andify(generateAutoReqs(e.Els))));
        }
        return reqs;
    }