public static void Resolve()

in ironclad-apps/tools/DafnySpec/ParseMain.cs [334:441]
108 lines of code
24 McCabe index (conditional complexity)

    public static void Resolve(Resolver resolver, Program program)
    {
        try
        {
            foreach (ModuleDefinition module in program.Modules)
            {
                foreach (TopLevelDecl decl in module.TopLevelDecls)
                {
                    DatatypeDecl data = decl as DatatypeDecl;
                    if (data != null)
                    {
                        foreach (var ctor in data.Ctors)
                        {
                            resolver.PushGhost();
                            data.TypeArgs.ForEach(p => resolver.PushTypeParam(p));
                            ctor.Formals.ForEach(f => f.Resolve(resolver));
                            data.TypeArgs.ForEach(p => resolver.PopTypeParam(p));
                            resolver.PopGhost();
                        }
                    }
                }
            }
            foreach (MemberDecl member in ClassDecl.TheClass.Members)
            {
                Field field = member as Field;
                Function fun = member as Function;
                Method method = member as Method;
                if (field != null)
                {
                    if (field.IsGhost) { resolver.PushGhost(); }
                    field.Type.Resolve(resolver);
                    if (field.IsGhost) { resolver.PopGhost(); }
                }
                if (fun != null)
                {
                    resolver.currentFunction = fun;
                    resolver.PushGhost();
                    fun.TypeArgs.ForEach(p => resolver.PushTypeParam(p));
                    fun.Formals.ForEach(x => { x.Resolve(resolver); });
                    fun.ResultType.Resolve(resolver);
                    fun.TypeArgs.ForEach(p => resolver.PopTypeParam(p));
                    resolver.PopGhost();
                    resolver.currentFunction = null;
                }
                if (method != null)
                {
                    resolver.currentMethod = method;
                    if (method.IsGhost) { resolver.PushGhost(); }
                    method.TypeArgs.ForEach(p => resolver.PushTypeParam(p));
                    method.Formals.ForEach(x => { x.Resolve(resolver); });
                    method.Outs.ForEach(x => { x.Resolve(resolver); });
                    method.TypeArgs.ForEach(p => resolver.PopTypeParam(p));
                    if (method.IsGhost) { resolver.PopGhost(); }
                    resolver.currentMethod = null;
                }
            }
            foreach (MemberDecl member in ClassDecl.TheClass.Members)
            {
                Function fun = member as Function;
                Method method = member as Method;
                if (fun != null)
                {
                    resolver.currentFunction = fun;
                    resolver.PushGhost();
                    fun.TypeArgs.ForEach(p => resolver.PushTypeParam(p));
                    fun.Formals.ForEach(x => { resolver.PushVar(x.Name, x.Type, true); });
                    fun.ResultType.Resolve(resolver);
                    fun.Req = fun.Req.ConvertAll(e => e.Resolve(resolver, Type.Bool));
                    fun.Ens = fun.Ens.ConvertAll(e => e.Resolve(resolver, Type.Bool));
                    fun.Decreases.Resolve(resolver);
                    if (fun.Body != null) { fun.Body = fun.Body.Resolve(resolver, fun.ResultType); }
                    if (fun.IsRecursive && fun.Decreases.Expressions.Count == 0)
                    {
                        fun.Decreases.Expressions.Add(new IdentifierExpr(Token.NoToken, fun.Formals[0].Name));
                        fun.Decreases.Resolve(resolver);
                    }
                    fun.Formals.ForEach(x => resolver.PopVar(x.Name));
                    fun.TypeArgs.ForEach(p => resolver.PopTypeParam(p));
                    resolver.PopGhost();
                    resolver.currentFunction = null;
                }
                if (method != null)
                {
                    resolver.currentMethod = method;
                    if (method.IsGhost) { resolver.PushGhost(); }
                    method.TypeArgs.ForEach(p => resolver.PushTypeParam(p));
                    method.Formals.ForEach(x => { resolver.PushVar(x.Name, x.Type, true); });
                    method.Req.ForEach(e => e.Resolve(resolver));
                    method.Outs.ForEach(x => { resolver.PushVar(x.Name, x.Type, true); });
                    method.Ens.ForEach(e => e.Resolve(resolver));
                    method.Decreases.Resolve(resolver);
                    method.Outs.ForEach(x => resolver.PopVar(x.Name));
                    method.Formals.ForEach(x => resolver.PopVar(x.Name));
                    method.TypeArgs.ForEach(p => resolver.PopTypeParam(p));
                    if (method.IsGhost) { resolver.PopGhost(); }
                    resolver.currentMethod = null;
                }
            }
        }
        catch (Exception e)
        {
            string ctxt =
                (resolver.currentMethod != null) ? "in method " + resolver.currentMethod.Name + ": ":
                (resolver.currentFunction != null) ? "in function " + resolver.currentFunction.Name + ": ":
                "";
            throw new Exception(ctxt, e);
        }
    }