diff options
Diffstat (limited to 'Source/Core/TypeAmbiguitySeeker.cs')
-rw-r--r-- | Source/Core/TypeAmbiguitySeeker.cs | 244 |
1 files changed, 122 insertions, 122 deletions
diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs index 753385a1..6f57ad43 100644 --- a/Source/Core/TypeAmbiguitySeeker.cs +++ b/Source/Core/TypeAmbiguitySeeker.cs @@ -1,123 +1,123 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Diagnostics.Contracts;
-using System.Collections.Generic;
-
-// Visitor to search for types proxies that could not completely be
-// determined by type inference. If this happens, a warning is
-// generated and the proxies are instantiated in a more or less arbitrary
-// fashion.
-
-namespace Microsoft.Boogie {
-
- public class TypeAmbiguitySeeker : ReadOnlyVisitor {
-
- private readonly InTypeSeeker/*!*/ inTypeSeeker = new InTypeSeeker();
- private readonly TypecheckingContext/*!*/ TC;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(inTypeSeeker != null);
- Contract.Invariant(TC != null);
- }
-
-
- public TypeAmbiguitySeeker(TypecheckingContext tc) {
- Contract.Requires(tc != null);
- TC = tc;
- }
-
- private void CheckTypeParams(Absy node, TypeParamInstantiation insts) {
- Contract.Requires(insts != null);
- Contract.Requires(node != null);
- foreach (TypeVariable/*!*/ var in insts.FormalTypeParams) {
- Contract.Assert(var != null);
- Type/*!*/ inst = insts[var];
- Contract.Assert(inst != null);
-
- inTypeSeeker.FoundAmbiguity = false;
- inTypeSeeker.Visit(inst);
- if (inTypeSeeker.FoundAmbiguity)
- TC.Warning(node,
- "type parameter {0} is ambiguous, instantiating to {1}",
- var, inst);
- }
- }
-
- public override Expr VisitNAryExpr(NAryExpr node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- CheckTypeParams(node, cce.NonNull(node.TypeParameters));
- return base.VisitNAryExpr(node);
- }
-
- public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<AssignLhs>() != null);
- CheckTypeParams(node, cce.NonNull(node.TypeParameters));
- return base.VisitMapAssignLhs(node);
- }
- }
-
- internal class InTypeSeeker : ReadOnlyVisitor {
-
- internal bool FoundAmbiguity = false;
-
- // called when an uninstantiated proxy was found
- private Type Instantiate(Type node, Type inst) {
- Contract.Requires(inst != null);
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Type>() == node);
- FoundAmbiguity = true;
- bool success = node.Unify(inst);
- Contract.Assert(success);
- return node;
- }
-
- public override Type VisitTypeProxy(TypeProxy node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- if (node.ProxyFor != null)
- return base.VisitTypeProxy(node);
-
- return Instantiate(node, Type.Int);
- }
-
- public override Type VisitMapTypeProxy(MapTypeProxy node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- if (node.ProxyFor != null)
- return base.VisitMapTypeProxy(node);
-
- List<TypeVariable>/*!*/ typeParams = new List<TypeVariable>();
- List<Type>/*!*/ arguments = new List<Type>();
- for (int i = 0; i < node.Arity; ++i) {
- TypeVariable/*!*/ param = new TypeVariable(Token.NoToken, "arg" + i);
- Contract.Assert(param != null);
- typeParams.Add(param);
- arguments.Add(param);
- }
- TypeVariable/*!*/ result = new TypeVariable(Token.NoToken, "res");
- Contract.Assert(result != null);
- typeParams.Add(result);
-
- Type/*!*/ instantiation = new MapType(Token.NoToken, typeParams, arguments, result);
- Contract.Assert(instantiation != null);
-
- return Instantiate(node, instantiation);
- }
-
- public override Type VisitBvTypeProxy(BvTypeProxy node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- if (node.ProxyFor != null)
- return base.VisitBvTypeProxy(node);
-
- return Instantiate(node, new BvType(node.MinBits));
- }
- }
-
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Diagnostics.Contracts; +using System.Collections.Generic; + +// Visitor to search for types proxies that could not completely be +// determined by type inference. If this happens, a warning is +// generated and the proxies are instantiated in a more or less arbitrary +// fashion. + +namespace Microsoft.Boogie { + + public class TypeAmbiguitySeeker : ReadOnlyVisitor { + + private readonly InTypeSeeker/*!*/ inTypeSeeker = new InTypeSeeker(); + private readonly TypecheckingContext/*!*/ TC; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(inTypeSeeker != null); + Contract.Invariant(TC != null); + } + + + public TypeAmbiguitySeeker(TypecheckingContext tc) { + Contract.Requires(tc != null); + TC = tc; + } + + private void CheckTypeParams(Absy node, TypeParamInstantiation insts) { + Contract.Requires(insts != null); + Contract.Requires(node != null); + foreach (TypeVariable/*!*/ var in insts.FormalTypeParams) { + Contract.Assert(var != null); + Type/*!*/ inst = insts[var]; + Contract.Assert(inst != null); + + inTypeSeeker.FoundAmbiguity = false; + inTypeSeeker.Visit(inst); + if (inTypeSeeker.FoundAmbiguity) + TC.Warning(node, + "type parameter {0} is ambiguous, instantiating to {1}", + var, inst); + } + } + + public override Expr VisitNAryExpr(NAryExpr node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Expr>() != null); + CheckTypeParams(node, cce.NonNull(node.TypeParameters)); + return base.VisitNAryExpr(node); + } + + public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result<AssignLhs>() != null); + CheckTypeParams(node, cce.NonNull(node.TypeParameters)); + return base.VisitMapAssignLhs(node); + } + } + + internal class InTypeSeeker : ReadOnlyVisitor { + + internal bool FoundAmbiguity = false; + + // called when an uninstantiated proxy was found + private Type Instantiate(Type node, Type inst) { + Contract.Requires(inst != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Type>() == node); + FoundAmbiguity = true; + bool success = node.Unify(inst); + Contract.Assert(success); + return node; + } + + public override Type VisitTypeProxy(TypeProxy node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Type>() != null); + if (node.ProxyFor != null) + return base.VisitTypeProxy(node); + + return Instantiate(node, Type.Int); + } + + public override Type VisitMapTypeProxy(MapTypeProxy node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Type>() != null); + if (node.ProxyFor != null) + return base.VisitMapTypeProxy(node); + + List<TypeVariable>/*!*/ typeParams = new List<TypeVariable>(); + List<Type>/*!*/ arguments = new List<Type>(); + for (int i = 0; i < node.Arity; ++i) { + TypeVariable/*!*/ param = new TypeVariable(Token.NoToken, "arg" + i); + Contract.Assert(param != null); + typeParams.Add(param); + arguments.Add(param); + } + TypeVariable/*!*/ result = new TypeVariable(Token.NoToken, "res"); + Contract.Assert(result != null); + typeParams.Add(result); + + Type/*!*/ instantiation = new MapType(Token.NoToken, typeParams, arguments, result); + Contract.Assert(instantiation != null); + + return Instantiate(node, instantiation); + } + + public override Type VisitBvTypeProxy(BvTypeProxy node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Type>() != null); + if (node.ProxyFor != null) + return base.VisitBvTypeProxy(node); + + return Instantiate(node, new BvType(node.MinBits)); + } + } + }
\ No newline at end of file |