diff options
| author |  tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
| commit | b617dda87871573b826dada4af73fc48dce94f15 (patch) | |
| tree | 453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/TypeAmbiguitySeeker.cs | |
| parent | 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff) | |
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/TypeAmbiguitySeeker.cs')
| -rw-r--r-- | Source/Core/TypeAmbiguitySeeker.cs | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs new file mode 100644 index 00000000..fc7cf071 --- /dev/null +++ b/Source/Core/TypeAmbiguitySeeker.cs @@ -0,0 +1,95 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+
+// 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 : StandardVisitor {
+
+ private readonly InTypeSeeker! inTypeSeeker = new InTypeSeeker ();
+ private readonly TypecheckingContext! TC;
+
+ public TypeAmbiguitySeeker(TypecheckingContext! tc) {
+ TC = tc;
+ }
+
+ private void CheckTypeParams(Absy! node, TypeParamInstantiation! insts) {
+ foreach (TypeVariable! var in insts.FormalTypeParams) {
+ Type! inst = insts[var];
+ 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)
+ {
+ CheckTypeParams(node, (!)node.TypeParameters);
+ return base.VisitNAryExpr(node);
+ }
+
+ public override AssignLhs! VisitMapAssignLhs(MapAssignLhs! node) {
+ CheckTypeParams(node, (!)node.TypeParameters);
+ return base.VisitMapAssignLhs(node); + }
+ }
+
+ internal class InTypeSeeker : StandardVisitor {
+
+ internal bool FoundAmbiguity = false;
+
+ // called when an uninstantiated proxy was found
+ private Type! Instantiate(Type! node, Type! inst) {
+ FoundAmbiguity = true;
+ bool success = node.Unify(inst);
+ assert success;
+ return node;
+ }
+
+ public override Type! VisitTypeProxy(TypeProxy! node) {
+ if (node.ProxyFor != null)
+ return base.VisitTypeProxy(node);
+
+ return Instantiate(node, Type.Int);
+ }
+
+ public override Type! VisitMapTypeProxy(MapTypeProxy! node) {
+ if (node.ProxyFor != null)
+ return base.VisitMapTypeProxy(node);
+
+ TypeVariableSeq! typeParams = new TypeVariableSeq ();
+ TypeSeq! arguments = new TypeSeq ();
+ for (int i = 0; i < node.Arity; ++i) {
+ TypeVariable! param = new TypeVariable (Token.NoToken, "arg" + i);
+ typeParams.Add(param);
+ arguments.Add(param);
+ }
+ TypeVariable! result = new TypeVariable (Token.NoToken, "res");
+ typeParams.Add(result);
+
+ Type! instantiation = new MapType (Token.NoToken, typeParams, arguments, result);
+
+ return Instantiate(node, instantiation);
+ }
+
+ public override Type! VisitBvTypeProxy(BvTypeProxy! node) {
+ if (node.ProxyFor != null)
+ return base.VisitBvTypeProxy(node);
+
+ return Instantiate(node, new BvType (node.MinBits));
+ }
+ }
+
+}
\ No newline at end of file |