diff options
| author |  leino <unknown> | 2015-01-23 16:17:23 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-01-23 16:17:23 -0800 |
| commit | 227fa997dd25a41c8bfc86d919635b6677df2c5f (patch) | |
| tree | 4ac05f6efa2a3d51ff46118c61567f3b1f52d120 | |
| parent | 97e7528b3cd3e9b9e21b75abf817d6e0ed3b9df7 (diff) | |
Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests
| -rw-r--r-- | Source/Dafny/Cloner.cs | 39 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 84 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 259 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 368 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 21 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 512 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/LiberalEquality.dfy | 80 | ||||
| -rw-r--r-- | Test/dafny0/LiberalEquality.dfy.expect | 20 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy.expect | 16 | ||||
| -rw-r--r-- | Test/dafny0/Modules2.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 10 | ||||
| -rw-r--r-- | Test/hofs/Consequence.dfy | 7 | ||||
| -rw-r--r-- | Test/hofs/Consequence.dfy.expect | 2 |
17 files changed, 878 insertions, 565 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index f95c05ed..3ec8ac59 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -188,7 +188,7 @@ namespace Microsoft.Dafny return CloneType(syn.Rhs);
}
#endif
- return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(Tok));
+ return new UserDefinedType(Tok(tt.tok), CloneExpr(tt.NamePath));
} else if (t is InferredTypeProxy) {
return new InferredTypeProxy();
} else if (t is OperationTypeProxy) {
@@ -209,8 +209,8 @@ namespace Microsoft.Dafny return f;
}
- public BoundVar CloneBoundVar(BoundVar bv) {
- var bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));
+ public virtual BoundVar CloneBoundVar(BoundVar bv) {
+ var bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.SyntacticType));
bvNew.IsGhost = bv.IsGhost;
return bvNew;
}
@@ -453,7 +453,7 @@ namespace Microsoft.Dafny } else if (r.Arguments == null) {
c = new TypeRhs(Tok(r.Tok), CloneType(r.EType));
} else {
- c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.OptionalNameComponent, r.Arguments.ConvertAll(CloneExpr));
+ c = new TypeRhs(Tok(r.Tok), CloneType(r.Path), r.Arguments.ConvertAll(CloneExpr), false);
}
}
c.Attributes = CloneAttributes(rhs.Attributes);
@@ -707,8 +707,10 @@ namespace Microsoft.Dafny public override Expression CloneExpr(Expression expr) {
if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
+ // Note, the CoLemmaPostconditionSubstituter is an unusual cloner in that it operates on
+ // resolved expressions. Hence, we bypass the syntactic parts here.
return CloneExpr(e.Resolved);
- } else if (expr is FunctionCallExpr) {
+ } else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
if (coConclusions.Contains(e)) {
var receiver = CloneExpr(e.Receiver);
@@ -735,6 +737,26 @@ namespace Microsoft.Dafny }
return base.CloneExpr(expr);
}
+ public override Type CloneType(Type t) {
+ if (t is UserDefinedType) {
+ var tt = (UserDefinedType)t;
+ // We want syntactic cloning of the Expression that is tt.NamePath, unlike the semantic (that is, post-resolved)
+ // cloning that CloneExpr is doing above.
+ return new UserDefinedType(Tok(tt.tok), CloneNamePathExpression(tt.NamePath));
+ } else {
+ return base.CloneType(t);
+ }
+ }
+ Expression CloneNamePathExpression(Expression expr) {
+ Contract.Requires(expr is NameSegment || expr is ExprDotName);
+ if (expr is NameSegment) {
+ var e = (NameSegment)expr;
+ return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
+ } else {
+ var e = (ExprDotName)expr;
+ return new ExprDotName(Tok(e.tok), CloneNamePathExpression(e.Lhs), e.SuffixName, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
+ }
+ }
}
/// <summary>
@@ -813,6 +835,13 @@ namespace Microsoft.Dafny return newPat;
}
}
+
+ public override BoundVar CloneBoundVar(BoundVar bv) {
+ // The difference here from the overridden method is that we do CloneType(bv.Type) instead of CloneType(bv.SyntacticType)
+ var bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));
+ bvNew.IsGhost = bv.IsGhost;
+ return bvNew;
+ }
}
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d6799290..45018cd3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1090,33 +1090,34 @@ Type<out Type ty> TypeAndToken<out IToken tok, out Type ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type> gt = null;
+ List<Type> gt; List<Type> tupleArgTypes = null;
.)
( "bool" (. tok = t; .)
| "char" (. tok = t; ty = new CharType(); .)
| "nat" (. tok = t; ty = new NatType(); .)
| "int" (. tok = t; ty = new IntType(); .)
| "real" (. tok = t; ty = new RealType(); .)
- | "set" (. tok = t; gt = new List<Type/*!*/>(); .)
+ | "object" (. tok = t; ty = new ObjectType(); .)
+ | "set" (. tok = t; gt = new List<Type>(); .)
[ GenericInstantiation<gt> ] (. if (gt.Count > 1) {
SemErr("set type expects only one type argument");
}
ty = new SetType(gt.Count == 1 ? gt[0] : null);
.)
- | "multiset" (. tok = t; gt = new List<Type/*!*/>(); .)
+ | "multiset" (. tok = t; gt = new List<Type>(); .)
[ GenericInstantiation<gt> ] (. if (gt.Count > 1) {
SemErr("multiset type expects only one type argument");
}
ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);
.)
- | "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
+ | "seq" (. tok = t; gt = new List<Type>(); .)
[ GenericInstantiation<gt> ] (. if (gt.Count > 1) {
SemErr("seq type expects only one type argument");
}
ty = new SeqType(gt.Count == 1 ? gt[0] : null);
.)
- | "string" (. tok = t; ty = new UserDefinedType(tok, tok.val, new List<Type>(), new List<IToken>()); .)
- | "map" (. tok = t; gt = new List<Type/*!*/>(); .)
+ | "string" (. tok = t; ty = new UserDefinedType(tok, tok.val, null); .)
+ | "map" (. tok = t; gt = new List<Type>(); .)
[ GenericInstantiation<gt> ] (. if (gt.Count == 0) {
ty = new MapType(null, null);
} else if (gt.Count != 2) {
@@ -1126,26 +1127,42 @@ TypeAndToken<out IToken tok, out Type ty> ty = new MapType(gt[0], gt[1]);
}
.)
- | "(" (. tok = t; gt = new List<Type>(); .)
- [ Type<out ty> (. gt.Add(ty); .)
- { "," Type<out ty> (. gt.Add(ty); .)
+ | arrayToken (. tok = t; gt = null; .)
+ [ (. gt = new List<Type>(); .)
+ GenericInstantiation<gt>
+ ]
+ (. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
+ ty = theBuiltIns.ArrayType(tok, dims, gt, true);
+ .)
+ | "(" (. tok = t; tupleArgTypes = new List<Type>(); .)
+ [ Type<out ty> (. tupleArgTypes.Add(ty); .)
+ { "," Type<out ty> (. tupleArgTypes.Add(ty); .)
}
]
- ")" (. if (gt.Count == 1) {
+ ")" (. if (tupleArgTypes.Count == 1) {
// just return the type 'ty'
} else {
- // make sure the nullary tuple type exists
- var dims = gt.Count;
- var tmp = theBuiltIns.TupleType(tok, dims, true);
- ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());
+ var dims = tupleArgTypes.Count;
+ var tmp = theBuiltIns.TupleType(tok, dims, true); // make sure the tuple type exists
+ ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), dims == 0 ? null : tupleArgTypes);
}
.)
- | ReferenceType<out tok, out ty>
+ | (. Expression e; .)
+ NameSegmentForTypeName<out e>
+ { "." ident (. tok = t; List<Type> typeArgs = null; .)
+ [ (. typeArgs = new List<Type>(); .)
+ GenericInstantiation<typeArgs>
+ ]
+ (. e = new ExprDotName(tok, e, tok.val, typeArgs); .)
+ }
+ (. ty = new UserDefinedType(e.tok, e); .)
)
[ (. Type t2; .)
"->" (. tok = t; .)
Type<out t2>
- (. if (gt == null) {
+ (. if (tupleArgTypes != null) {
+ gt = tupleArgTypes;
+ } else {
gt = new List<Type>{ ty };
}
ty = new ArrowType(tok, gt, t2);
@@ -1154,26 +1171,6 @@ TypeAndToken<out IToken tok, out Type ty> ]
.
-ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
-= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
- tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type> gt;
- List<IToken> path;
- .)
- ( "object" (. tok = t; ty = new ObjectType(); .)
- | arrayToken (. tok = t; gt = new List<Type>(); .)
- [ GenericInstantiation<gt> ] (. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
- ty = theBuiltIns.ArrayType(tok, dims, gt, true);
- .)
- | Ident<out tok> (. gt = new List<Type>();
- path = new List<IToken>(); .)
- { IF(la.kind == _dot) /* greedily parse as many identifiers as possible (if the next identifier really denotes a constructor in a "new" RHS, then it will be adjusted for later */
- (. path.Add(tok); .)
- "." Ident<out tok>
- }
- [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
- )
- .
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
"<"
@@ -1495,7 +1492,6 @@ Rhs<out AssignmentRhs r> var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
.)
| (. x = null; args = new List<Expression/*!*/>(); .)
- [ "." Ident<out x> ]
"("
[ Expressions<args> ]
")"
@@ -1503,7 +1499,7 @@ Rhs<out AssignmentRhs r> (. if (ee != null) {
r = new TypeRhs(newToken, ty, ee);
} else if (args != null) {
- r = new TypeRhs(newToken, ty, x == null ? null : x.val, args);
+ r = new TypeRhs(newToken, ty, args, false);
} else {
r = new TypeRhs(newToken, ty);
}
@@ -2575,6 +2571,18 @@ NameSegment<out Expression e> }
.)
.
+/* NameSegmentForTypeName is like the production NameSegment, except that it does not allow HashCall */
+NameSegmentForTypeName<out Expression e>
+= (. IToken id;
+ List<Type> typeArgs = null;
+ .)
+ Ident<out id>
+ [ (. typeArgs = new List<Type>(); .)
+ GenericInstantiation<typeArgs>
+ ]
+ (. e = new NameSegment(id, id.val, typeArgs);
+ .)
+ .
/* The HashCall production extends a given identifier with a hash sign followed by
* a list of argument expressions. That is, if what was just parsed was an identifier id,
* then the HashCall production will continue parsing into id#[arg](args).
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f1fbd7ff..734f328f 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -120,13 +120,13 @@ namespace Microsoft.Dafny { Contract.Requires(arg != null);
return ArrayType(Token.NoToken, dims, new List<Type>() { arg }, allowCreationOfNewClass);
}
- public UserDefinedType ArrayType(IToken tok, int dims, List<Type> typeArgs, bool allowCreationOfNewClass) {
+ public UserDefinedType ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass) {
Contract.Requires(tok != null);
Contract.Requires(1 <= dims);
- Contract.Requires(typeArgs != null);
+ Contract.Requires(optTypeArgs == null || optTypeArgs.Count > 0); // ideally, it is 1, but more will generate an error later, and null means it will be filled in automatically
Contract.Ensures(Contract.Result<UserDefinedType>() != null);
- UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);
+ UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), optTypeArgs);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());
for (int d = 0; d < dims; d++) {
@@ -430,6 +430,23 @@ namespace Microsoft.Dafny { /// </summary>
[Pure]
public abstract bool Equals(Type that);
+ /// <summary>
+ /// Returns whether or not "this" and "that" could denote the same type, module proxies and type synonyms, if
+ /// type parameters are treated as wildcards.
+ /// </summary>
+ public bool PossiblyEquals(Type that) {
+ Contract.Requires(that != null);
+ var a = NormalizeExpand();
+ var b = that.NormalizeExpand();
+ return a.AsTypeParameter != null || b.AsTypeParameter != null || a.PossiblyEquals_W(b);
+ }
+ /// <summary>
+ /// Overridable worker routine for PossiblyEquals. Implementations can assume "that" to be non-null,
+ /// and that NormalizeExpand() has been applied to both "this" and "that". Furthermore, neither "this"
+ /// nor "that" is a TypeParameter, because that case is handled by PossiblyEquals. Recursive calls
+ /// should go to PossiblyEquals, not directly to PossiblyEquals_W.
+ /// </summary>
+ public abstract bool PossiblyEquals_W(Type that);
public bool IsBoolType { get { return NormalizeExpand() is BoolType; } }
public bool IsCharType { get { return NormalizeExpand() is CharType; } }
@@ -629,6 +646,9 @@ namespace Microsoft.Dafny { public abstract class BasicType : NonProxyType
{
+ public override bool PossiblyEquals_W(Type that) {
+ return Equals(that);
+ }
}
public class BoolType : BasicType {
@@ -710,7 +730,7 @@ namespace Microsoft.Dafny { /// Constructs a(n unresolved) arrow type.
/// </summary>
public ArrowType(IToken tok, List<Type> args, Type result)
- : base(tok, ArrowTypeName(args.Count), Util.Snoc(args, result), null) {
+ : base(tok, ArrowTypeName(args.Count), Util.Snoc(args, result)) {
Contract.Requires(tok != null);
Contract.Requires(args != null);
Contract.Requires(result != null);
@@ -831,6 +851,10 @@ namespace Microsoft.Dafny { var t = that.NormalizeExpand() as SetType;
return t != null && Arg.Equals(t.Arg);
}
+ public override bool PossiblyEquals_W(Type that) {
+ var t = that as SetType;
+ return t != null && Arg.PossiblyEquals(t.Arg);
+ }
}
public class MultiSetType : CollectionType
@@ -842,6 +866,10 @@ namespace Microsoft.Dafny { var t = that.NormalizeExpand() as MultiSetType;
return t != null && Arg.Equals(t.Arg);
}
+ public override bool PossiblyEquals_W(Type that) {
+ var t = that as MultiSetType;
+ return t != null && Arg.PossiblyEquals(t.Arg);
+ }
}
public class SeqType : CollectionType {
@@ -852,6 +880,10 @@ namespace Microsoft.Dafny { var t = that.NormalizeExpand() as SeqType;
return t != null && Arg.Equals(t.Arg);
}
+ public override bool PossiblyEquals_W(Type that) {
+ var t = that as SeqType;
+ return t != null && Arg.PossiblyEquals(t.Arg);
+ }
}
public class MapType : CollectionType
{
@@ -890,6 +922,10 @@ namespace Microsoft.Dafny { var t = that.NormalizeExpand() as MapType;
return t != null && Arg.Equals(t.Arg) && Range.Equals(t.Range);
}
+ public override bool PossiblyEquals_W(Type that) {
+ var t = that as MapType;
+ return t != null && Arg.PossiblyEquals(t.Arg) && Range.PossiblyEquals(t.Range);
+ }
}
public class UserDefinedType : NonProxyType
@@ -899,11 +935,11 @@ namespace Microsoft.Dafny { Contract.Invariant(tok != null);
Contract.Invariant(Name != null);
Contract.Invariant(cce.NonNullElements(TypeArgs));
- Contract.Invariant(cce.NonNullElements(Path));
+ Contract.Invariant(NamePath is NameSegment || NamePath is ExprDotName);
Contract.Invariant(!ArrowType.IsArrowTypeName(Name) || this is ArrowType);
}
- public readonly List<IToken> Path;
+ public readonly Expression NamePath; // either NameSegment or ExprDotName (with the inner expression satisfying this same constraint)
public readonly IToken tok; // token of the Name
public readonly string Name;
[Rep]
@@ -940,70 +976,76 @@ namespace Microsoft.Dafny { public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype/iterator and TypeArgs match the type parameters of that class/datatype/iterator
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
- public UserDefinedType(IToken tok, string name, [Captured] List<Type> typeArgs, List<IToken> moduleName) {
+ public UserDefinedType(IToken tok, string name, List<Type> optTypeArgs)
+ : this(tok, new NameSegment(tok, name, optTypeArgs))
+ {
Contract.Requires(tok != null);
Contract.Requires(name != null);
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(moduleName == null || cce.NonNullElements(moduleName));
- if (moduleName != null) this.Path = moduleName;
- else this.Path = new List<IToken>();
- this.tok = tok;
- this.Name = name;
- this.TypeArgs = typeArgs;
+ Contract.Requires(optTypeArgs == null || optTypeArgs.Count > 0); // this is what it means to be syntactically optional
}
- /// <summary>
- /// This constructor constructs a resolved class/datatype/iterator type
- /// </summary>
- public UserDefinedType(IToken tok, string name, TopLevelDecl cd, [Captured] List<Type> typeArgs)
- : this(tok, name, cd, typeArgs, null)
- {
+ public UserDefinedType(IToken tok, Expression namePath) {
Contract.Requires(tok != null);
- Contract.Requires(name != null);
- Contract.Requires(cd != null);
- Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(namePath is NameSegment || namePath is ExprDotName);
+ this.tok = tok;
+ if (namePath is NameSegment) {
+ var n = (NameSegment)namePath;
+ this.Name = n.Name;
+ this.TypeArgs = n.OptTypeArguments;
+ } else {
+ var n = (ExprDotName)namePath;
+ this.Name = n.SuffixName;
+ this.TypeArgs = n.OptTypeArguments;
+ }
+ if (this.TypeArgs == null) {
+ this.TypeArgs = new List<Type>(); // TODO: is this really the thing to do?
+ }
+ this.NamePath = namePath;
}
/// <summary>
/// This constructor constructs a resolved class/datatype/iterator type
/// </summary>
- public UserDefinedType(IToken tok, string name, TopLevelDecl cd, [Captured] List<Type> typeArgs, List<IToken> moduleName) {
+ public UserDefinedType(IToken tok, string name, TopLevelDecl cd, [Captured] List<Type> typeArgs) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cd != null);
Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(moduleName == null || cce.NonNullElements(moduleName));
+ Contract.Requires(cd.TypeArgs.Count == typeArgs.Count);
this.tok = tok;
this.Name = name;
this.ResolvedClass = cd;
this.TypeArgs = typeArgs;
- if (moduleName != null)
- this.Path = moduleName;
- else
- this.Path = new List<IToken>();
+ var ns = new NameSegment(tok, name, typeArgs.Count == 0 ? null : typeArgs);
+ var r = new Resolver_IdentifierExpr(tok, cd, typeArgs);
+ ns.ResolvedExpression = r;
+ ns.Type = r.Type;
+ this.NamePath = ns;
}
/// <summary>
/// This constructor constructs a resolved type parameter
/// </summary>
- public UserDefinedType(IToken tok, string name, TypeParameter tp) {
- Contract.Requires(tok != null);
- Contract.Requires(name != null);
+ public UserDefinedType(TypeParameter tp)
+ : this(tp.tok, tp) {
Contract.Requires(tp != null);
- this.tok = tok;
- this.Name = name;
- this.TypeArgs = new List<Type>();
- this.ResolvedParam = tp;
- this.Path = new List<IToken>();
}
/// <summary>
/// This constructor constructs a resolved type parameter
/// </summary>
- public UserDefinedType(TypeParameter tp)
- : this(tp.tok, tp.Name, tp)
- {
+ public UserDefinedType(IToken tok, TypeParameter tp) {
+ Contract.Requires(tok != null);
Contract.Requires(tp != null);
+ this.tok = tok;
+ this.Name = tp.Name;
+ this.TypeArgs = new List<Type>();
+ this.ResolvedParam = tp;
+ var ns = new NameSegment(tok, tp.Name, null);
+ var r = new Resolver_IdentifierExpr(tok, tp);
+ ns.ResolvedExpression = r;
+ ns.Type = r.Type;
+ this.NamePath = ns;
}
public override bool Equals(Type that) {
@@ -1027,6 +1069,19 @@ namespace Microsoft.Dafny { return i.Equals(that);
}
}
+ public override bool PossiblyEquals_W(Type that) {
+ Contract.Assume(ResolvedParam == null); // we get this assumption from the caller, PossiblyEquals
+ var t = that as UserDefinedType;
+ if (t != null && ResolvedClass != null && ResolvedClass == t.ResolvedClass) {
+ for (int j = 0; j < TypeArgs.Count; j++) {
+ if (!TypeArgs[j].PossiblyEquals(t.TypeArgs[j])) {
+ return false;
+ }
+ }
+ return true;
+ }
+ return false;
+ }
/// <summary>
/// If type denotes a resolved class type, then return that class type.
@@ -1067,19 +1122,13 @@ namespace Microsoft.Dafny { return ((TypeSynonymDecl)ResolvedClass).Rhs.TypeName(context);
}
#endif
- string s = "";
- foreach (var t in Path) {
- if (context != null && t == context.tok) {
- // drop the prefix up to here
- s = "";
- } else {
- s += t.val + ".";
+ var s = Printer.ExprToString(NamePath);
+ if (ResolvedClass != null) {
+ var optionalTypeArgs = NamePath is NameSegment ? ((NameSegment)NamePath).OptTypeArguments : ((ExprDotName)NamePath).OptTypeArguments;
+ if (optionalTypeArgs == null && TypeArgs != null && TypeArgs.Count != 0) {
+ s += "<" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ">";
}
}
- s += Name;
- if (TypeArgs.Count != 0) {
- s += "<" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ">";
- }
return s;
}
}
@@ -1146,6 +1195,9 @@ namespace Microsoft.Dafny { return i.Equals(that);
}
}
+ public override bool PossiblyEquals_W(Type that) {
+ return false; // we don't consider unresolved proxies as worthy of "possibly equals" status
+ }
}
public abstract class UnrestrictedTypeProxy : TypeProxy {
@@ -1456,6 +1508,7 @@ namespace Microsoft.Dafny { // Represents a submodule declaration at module level scope
abstract public class ModuleDecl : TopLevelDecl
{
+ public override string WhatKind { get { return "module"; } }
public ModuleSignature Signature; // filled in by resolution, in topological order.
public int Height;
public readonly bool Opened;
@@ -1720,6 +1773,7 @@ namespace Microsoft.Dafny { }
public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {
+ public abstract string WhatKind { get; }
public readonly ModuleDefinition Module;
public readonly List<TypeParameter> TypeArgs;
[ContractInvariantMethod]
@@ -1762,13 +1816,15 @@ namespace Microsoft.Dafny { public class TraitDecl : ClassDecl
{
- public bool IsParent { set; get; }
- public TraitDecl(IToken tok, string name, ModuleDefinition module,
- List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes)
- : base(tok, name, module, typeArgs, members, attributes, null) { }
+ public override string WhatKind { get { return "trait"; } }
+ public bool IsParent { set; get; }
+ public TraitDecl(IToken tok, string name, ModuleDefinition module,
+ List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes)
+ : base(tok, name, module, typeArgs, members, attributes, null) { }
}
public class ClassDecl : TopLevelDecl {
+ public override string WhatKind { get { return "class"; } }
public readonly List<MemberDecl> Members;
public List<TraitDecl> TraitsObj;
public readonly List<Type> TraitsTyp;
@@ -1834,6 +1890,7 @@ namespace Microsoft.Dafny { }
public class ArrayClassDecl : ClassDecl {
+ public override string WhatKind { get { return "array type"; } }
public readonly int Dims;
public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)
: base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
@@ -1849,6 +1906,7 @@ namespace Microsoft.Dafny { public class ArrowTypeDecl : ClassDecl
{
+ public override string WhatKind { get { return "function type"; } }
public readonly int Arity;
public readonly Function Requires;
public readonly Function Reads;
@@ -1897,6 +1955,7 @@ namespace Microsoft.Dafny { public class IndDatatypeDecl : DatatypeDecl
{
+ public override string WhatKind { get { return "datatype"; } }
public DatatypeCtor DefaultCtor; // set during resolution
public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as the number of type arguments
@@ -1953,7 +2012,7 @@ namespace Microsoft.Dafny { var formals = new List<Formal>();
for (int i = 0; i < typeArgs.Count; i++) {
var tp = typeArgs[i];
- var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp.Name, tp), true, false);
+ var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp), true, false);
formals.Add(f);
}
var ctor = new DatatypeCtor(Token.NoToken, BuiltIns.TupleTypeCtorName, formals, null);
@@ -1963,6 +2022,7 @@ namespace Microsoft.Dafny { public class CoDatatypeDecl : DatatypeDecl
{
+ public override string WhatKind { get { return "codatatype"; } }
public CoDatatypeDecl SscRepr; // filled in during resolution
public CoDatatypeDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,
@@ -2102,6 +2162,7 @@ namespace Microsoft.Dafny { public class IteratorDecl : ClassDecl, IMethodCodeContext
{
+ public override string WhatKind { get { return "iterator"; } }
public readonly List<Formal> Ins;
public readonly List<Formal> Outs;
public readonly Specification<FrameExpression> Reads;
@@ -2207,6 +2268,7 @@ namespace Microsoft.Dafny { }
public abstract class MemberDecl : Declaration {
+ public abstract string WhatKind { get; }
public readonly bool HasStaticKeyword;
public bool IsStatic {
get {
@@ -2269,6 +2331,7 @@ namespace Microsoft.Dafny { }
public class Field : MemberDecl {
+ public override string WhatKind { get { return "field"; } }
public readonly bool IsMutable; // says whether or not the field can ever change values
public readonly bool IsUserMutable; // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable)
public readonly Type Type;
@@ -2341,6 +2404,7 @@ namespace Microsoft.Dafny { public class OpaqueTypeDecl : TopLevelDecl, TypeParameter.ParentType
{
+ public override string WhatKind { get { return "opaque type"; } }
public readonly TypeParameter TheType;
public TypeParameter.EqualitySupportValue EqualitySupport {
get { return TheType.EqualitySupport; }
@@ -2390,6 +2454,7 @@ namespace Microsoft.Dafny { public class NewtypeDecl : TopLevelDecl, RedirectingTypeDecl
{
+ public override string WhatKind { get { return "newtype"; } }
public readonly Type BaseType;
public readonly BoundVar Var; // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType))
public readonly Expression Constraint; // is null iff Var is
@@ -2438,6 +2503,7 @@ namespace Microsoft.Dafny { public class TypeSynonymDecl : TopLevelDecl, RedirectingTypeDecl
{
+ public override string WhatKind { get { return "type synonym"; } }
public readonly Type Rhs;
public TypeSynonymDecl(IToken tok, string name, List<TypeParameter> typeArgs, ModuleDefinition module, Type rhs, Attributes attributes)
: base(tok, name, module, typeArgs, attributes) {
@@ -2466,12 +2532,7 @@ namespace Microsoft.Dafny { string RedirectingTypeDecl.Name { get { return Name; } }
- bool ICodeContext.IsGhost {
- get {
- // A type synonym does not have any expressions or statements, so the the question of IsGhost should never arise.
- throw new cce.UnreachableException();
- }
- }
+ bool ICodeContext.IsGhost { get { return false; } }
List<TypeParameter> ICodeContext.TypeArgs { get { return TypeArgs; } }
List<Formal> ICodeContext.Ins { get { return new List<Formal>(); } }
ModuleDefinition ICodeContext.EnclosingModule { get { return Module; } }
@@ -2671,6 +2732,7 @@ namespace Microsoft.Dafny { }
}
Type type;
+ public Type SyntacticType { get { return type; } } // returns the non-normalized type
public Type Type {
get {
Contract.Ensures(Contract.Result<Type>() != null);
@@ -2780,6 +2842,7 @@ namespace Microsoft.Dafny { }
public class Function : MemberDecl, TypeParameter.ParentType, ICallable {
+ public override string WhatKind { get { return "function"; } }
public bool IsRecursive; // filled in during resolution
public readonly List<TypeParameter> TypeArgs;
public readonly List<Formal> Formals;
@@ -2878,6 +2941,7 @@ namespace Microsoft.Dafny { public class Predicate : Function
{
+ public override string WhatKind { get { return "predicate"; } }
public enum BodyOriginKind
{
OriginalOrInherited, // this predicate definition is new (and the predicate may or may not have a body), or the predicate's body (whether or not it exists) is being inherited unmodified (from the previous refinement--it may be that the inherited body was itself an extension, for example)
@@ -2900,6 +2964,7 @@ namespace Microsoft.Dafny { /// </summary>
public class PrefixPredicate : Function
{
+ public override string WhatKind { get { return "prefix predicate"; } }
public readonly Formal K;
public readonly CoPredicate Co;
public PrefixPredicate(IToken tok, string name, bool hasStaticKeyword,
@@ -2917,6 +2982,7 @@ namespace Microsoft.Dafny { public class CoPredicate : Function
{
+ public override string WhatKind { get { return "copredicate"; } }
public readonly List<FunctionCallExpr> Uses = new List<FunctionCallExpr>(); // filled in during resolution, used by verifier
public PrefixPredicate PrefixPredicate; // filled in during resolution (name registration)
@@ -2960,6 +3026,7 @@ namespace Microsoft.Dafny { public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext
{
+ public override string WhatKind { get { return "method"; } }
public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } }
public readonly IToken SignatureEllipsis;
public bool MustReverify;
@@ -3047,6 +3114,7 @@ namespace Microsoft.Dafny { public class Lemma : Method
{
+ public override string WhatKind { get { return "lemma"; } }
public Lemma(IToken tok, string name,
bool hasStaticKeyword,
[Captured] List<TypeParameter> typeArgs,
@@ -3062,6 +3130,7 @@ namespace Microsoft.Dafny { public class Constructor : Method
{
+ public override string WhatKind { get { return "constructor"; } }
public Constructor(IToken tok, string name,
[Captured] List<TypeParameter> typeArgs,
[Captured] List<Formal> ins,
@@ -3093,6 +3162,7 @@ namespace Microsoft.Dafny { /// </summary>
public class PrefixLemma : Method
{
+ public override string WhatKind { get { return "prefix lemma"; } }
public readonly Formal K;
public readonly CoLemma Co;
public PrefixLemma(IToken tok, string name, bool hasStaticKeyword,
@@ -3110,6 +3180,7 @@ namespace Microsoft.Dafny { public class CoLemma : Method
{
+ public override string WhatKind { get { return "colemma"; } }
public PrefixLemma PrefixLemma; // filled in during resolution (name registration)
public CoLemma(IToken tok, string name,
@@ -3462,45 +3533,42 @@ namespace Microsoft.Dafny { /// This allocates an object of type C
/// * new C.Init(EE)
/// This allocates an object of type C and then invokes the method/constructor Init on it
- /// There are four ways to construct a TypeRhs syntactically:
+ /// There are three ways to construct a TypeRhs syntactically:
/// * TypeRhs(T, EE)
/// -- represents new T[EE]
/// * TypeRhs(C)
/// -- represents new C
- /// * TypeRhs(Path, null, EE)
+ /// * TypeRhs(Path, EE)
/// Here, Path may either be of the form C.Init
/// -- represents new C.Init(EE)
/// or all of Path denotes a type
/// -- represents new C._ctor(EE), where _ctor is the anonymous constructor for class C
- /// * TypeRhs(Path, s, EE)
- /// Here, Path must denote a type and s is a string that denotes the method/constructor Init
- /// -- represents new Path.s(EE)
/// </summary>
public class TypeRhs : AssignmentRhs
{
/// <summary>
/// If ArrayDimensions != null, then the TypeRhs represents "new EType[ArrayDimensions]"
- /// and Arguments, OptionalNameComponent, and InitCall are all null.
- /// If Arguments == null, then the TypeRhs represents "new C"
- /// and ArrayDimensions, OptionalNameComponent, and InitCall are all null.
- /// If OptionalNameComponent != null, then the TypeRhs represents "new EType.OptionalNameComponents(Arguments)"
- /// and InitCall is filled in by resolution, and ArrayDimensions == null and Arguments != null.
+ /// and Arguments, Path, and InitCall are all null.
+ /// If ArrayDimentions == null && Arguments == null, then the TypeRhs represents "new EType"
+ /// and Path, and InitCall are all null.
+ /// If Arguments != null, then the TypeRhs represents "new Path(Arguments)"
+ /// and EType and InitCall is filled in by resolution, and ArrayDimensions == null.
/// If OptionalNameComponent == null and Arguments != null, then the TypeRHS has not been resolved yet;
/// resolution will either produce an error or will chop off the last part of "EType" and move it to
/// OptionalNameComponent, after which the case above applies.
/// </summary>
- public Type EType; // almost readonly, except that resolution can split a given EType into a new EType plus a non-null OptionalNameComponent
+ public Type EType; // in the case of Arguments != null, EType is filled in during resolution
public readonly List<Expression> ArrayDimensions;
public readonly List<Expression> Arguments;
- public string OptionalNameComponent;
+ public Type Path;
public CallStmt InitCall; // may be null (and is definitely null for arrays), may be filled in during resolution
public Type Type; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(EType != null);
- Contract.Invariant(ArrayDimensions == null || (Arguments == null && OptionalNameComponent == null && InitCall == null));
- Contract.Invariant(ArrayDimensions == null || 1 <= ArrayDimensions.Count);
- Contract.Invariant(OptionalNameComponent == null || (Arguments != null && ArrayDimensions == null));
+ Contract.Invariant(EType != null || Arguments != null);
+ Contract.Invariant(ArrayDimensions == null || (Arguments == null && Path == null && InitCall == null && 1 <= ArrayDimensions.Count));
+ Contract.Invariant(Arguments == null || (Path != null && ArrayDimensions == null));
+ Contract.Invariant(!(ArrayDimensions == null && Arguments == null) || (Path == null && InitCall == null));
}
public TypeRhs(IToken tok, Type type, List<Expression> arrayDimensions)
@@ -3518,14 +3586,13 @@ namespace Microsoft.Dafny { Contract.Requires(type != null);
EType = type;
}
- public TypeRhs(IToken tok, Type type, string optionalNameComponent, List<Expression> arguments)
+ public TypeRhs(IToken tok, Type path, List<Expression> arguments, bool disambiguatingDummy)
: base(tok)
{
Contract.Requires(tok != null);
- Contract.Requires(type != null);
+ Contract.Requires(path != null);
Contract.Requires(arguments != null);
- EType = type;
- OptionalNameComponent = optionalNameComponent; // may be null
+ Path = path;
Arguments = arguments;
}
public override bool CanAffectPreviouslyKnownExpressions {
@@ -5375,13 +5442,17 @@ namespace Microsoft.Dafny { /// </summary>
class Resolver_IdentifierExpr : Expression
{
+ // The Resolver_IdentifierExpr either uses Decl and TypeArgs:
public readonly TopLevelDecl Decl;
public readonly List<Type> TypeArgs;
+ // ... or it uses TypeParamDecl:
+ public readonly TypeParameter TypeParamDecl;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Decl != null);
- Contract.Invariant(Type == null || Type is ResolverType_Module || Type is ResolverType_Type);
- Contract.Invariant(TypeArgs != null && TypeArgs.Count == Decl.TypeArgs.Count);
+ Contract.Invariant((Decl != null) != (TypeParamDecl != null)); // The Decl / TypeParamDecl fields are exclusive
+ Contract.Invariant((Decl != null) == (TypeArgs != null)); // The Decl / TypeArgs fields are used together
+ Contract.Invariant(TypeArgs == null || TypeArgs.Count == Decl.TypeArgs.Count);
+ Contract.Invariant(Type == null || (Type is ResolverType_Module && TypeParamDecl == null) || Type is ResolverType_Type);
}
public class ResolverType_Module : Type
@@ -5391,7 +5462,10 @@ namespace Microsoft.Dafny { return "#module";
}
public override bool Equals(Type that) {
- return that is ResolverType_Module;
+ return that.NormalizeExpand() is ResolverType_Module;
+ }
+ public override bool PossiblyEquals_W(Type that) {
+ return false;
}
}
public class ResolverType_Type : Type {
@@ -5400,7 +5474,10 @@ namespace Microsoft.Dafny { return "#type";
}
public override bool Equals(Type that) {
- return that is ResolverType_Type;
+ return that.NormalizeExpand() is ResolverType_Type;
+ }
+ public override bool PossiblyEquals_W(Type that) {
+ return false;
}
}
@@ -5413,6 +5490,13 @@ namespace Microsoft.Dafny { TypeArgs = typeArgs;
Type = decl is ModuleDecl ? (Type)new ResolverType_Module() : new ResolverType_Type();
}
+ public Resolver_IdentifierExpr(IToken tok, TypeParameter tp)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(tp != null);
+ TypeParamDecl = tp;
+ Type = new ResolverType_Type();
+ }
}
public abstract class DisplayExpression : Expression {
@@ -7004,6 +7088,7 @@ namespace Microsoft.Dafny { : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
+ Contract.Requires(optTypeArguments == null || optTypeArguments.Count > 0);
Name = name;
OptTypeArguments = optTypeArguments;
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 12fc3c34..ffe3f7f2 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1479,7 +1479,7 @@ bool IsType(ref IToken pt) { void TypeAndToken(out IToken tok, out Type ty) {
Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type> gt = null;
+ List<Type> gt; List<Type> tupleArgTypes = null;
switch (la.kind) {
case 6: {
@@ -1507,9 +1507,14 @@ bool IsType(ref IToken pt) { tok = t; ty = new RealType();
break;
}
+ case 11: {
+ Get();
+ tok = t; ty = new ObjectType();
+ break;
+ }
case 13: {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type>();
if (la.kind == 44) {
GenericInstantiation(gt);
}
@@ -1522,7 +1527,7 @@ bool IsType(ref IToken pt) { }
case 14: {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type>();
if (la.kind == 44) {
GenericInstantiation(gt);
}
@@ -1535,7 +1540,7 @@ bool IsType(ref IToken pt) { }
case 15: {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type>();
if (la.kind == 44) {
GenericInstantiation(gt);
}
@@ -1548,12 +1553,12 @@ bool IsType(ref IToken pt) { }
case 12: {
Get();
- tok = t; ty = new UserDefinedType(tok, tok.val, new List<Type>(), new List<IToken>());
+ tok = t; ty = new UserDefinedType(tok, tok.val, null);
break;
}
case 16: {
Get();
- tok = t; gt = new List<Type/*!*/>();
+ tok = t; gt = new List<Type>();
if (la.kind == 44) {
GenericInstantiation(gt);
}
@@ -1568,32 +1573,55 @@ bool IsType(ref IToken pt) { break;
}
+ case 5: {
+ Get();
+ tok = t; gt = null;
+ if (la.kind == 44) {
+ gt = new List<Type>();
+ GenericInstantiation(gt);
+ }
+ int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
+ ty = theBuiltIns.ArrayType(tok, dims, gt, true);
+
+ break;
+ }
case 42: {
Get();
- tok = t; gt = new List<Type>();
+ tok = t; tupleArgTypes = new List<Type>();
if (StartOf(3)) {
Type(out ty);
- gt.Add(ty);
+ tupleArgTypes.Add(ty);
while (la.kind == 20) {
Get();
Type(out ty);
- gt.Add(ty);
+ tupleArgTypes.Add(ty);
}
}
Expect(43);
- if (gt.Count == 1) {
+ if (tupleArgTypes.Count == 1) {
// just return the type 'ty'
} else {
- // make sure the nullary tuple type exists
- var dims = gt.Count;
- var tmp = theBuiltIns.TupleType(tok, dims, true);
- ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());
+ var dims = tupleArgTypes.Count;
+ var tmp = theBuiltIns.TupleType(tok, dims, true); // make sure the tuple type exists
+ ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), dims == 0 ? null : tupleArgTypes);
}
break;
}
- case 1: case 5: case 11: {
- ReferenceType(out tok, out ty);
+ case 1: {
+ Expression e;
+ NameSegmentForTypeName(out e);
+ while (la.kind == 24) {
+ Get();
+ Expect(1);
+ tok = t; List<Type> typeArgs = null;
+ if (la.kind == 44) {
+ typeArgs = new List<Type>();
+ GenericInstantiation(typeArgs);
+ }
+ e = new ExprDotName(tok, e, tok.val, typeArgs);
+ }
+ ty = new UserDefinedType(e.tok, e);
break;
}
default: SynErr(158); break;
@@ -1603,7 +1631,9 @@ bool IsType(ref IToken pt) { Get();
tok = t;
Type(out t2);
- if (gt == null) {
+ if (tupleArgTypes != null) {
+ gt = tupleArgTypes;
+ } else {
gt = new List<Type>{ ty };
}
ty = new ArrowType(tok, gt, t2);
@@ -1827,38 +1857,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(45);
}
- void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
- Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
- tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type> gt;
- List<IToken> path;
+ void NameSegmentForTypeName(out Expression e) {
+ IToken id;
+ List<Type> typeArgs = null;
+
+ Ident(out id);
+ if (la.kind == 44) {
+ typeArgs = new List<Type>();
+ GenericInstantiation(typeArgs);
+ }
+ e = new NameSegment(id, id.val, typeArgs);
- if (la.kind == 11) {
- Get();
- tok = t; ty = new ObjectType();
- } else if (la.kind == 5) {
- Get();
- tok = t; gt = new List<Type>();
- if (la.kind == 44) {
- GenericInstantiation(gt);
- }
- int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
- ty = theBuiltIns.ArrayType(tok, dims, gt, true);
-
- } else if (la.kind == 1) {
- Ident(out tok);
- gt = new List<Type>();
- path = new List<IToken>();
- while (la.kind == _dot) {
- path.Add(tok);
- Expect(24);
- Ident(out tok);
- }
- if (la.kind == 44) {
- GenericInstantiation(gt);
- }
- ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(166);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1866,7 +1875,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- while (!(StartOf(17))) {SynErr(167); Get();}
+ while (!(StartOf(17))) {SynErr(166); Get();}
if (la.kind == 37) {
Get();
Expression(out e, false, false);
@@ -1896,7 +1905,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, false, false);
OldSemi();
- } else SynErr(168);
+ } else SynErr(167);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1915,7 +1924,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(18)) {
FrameExpression(out fe, allowSemi, false);
- } else SynErr(169);
+ } else SynErr(168);
}
void PossiblyWildExpression(out Expression e, bool allowLambda) {
@@ -1926,7 +1935,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t);
} else if (StartOf(7)) {
Expression(out e, false, allowLambda);
- } else SynErr(170);
+ } else SynErr(169);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1943,7 +1952,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(19))) {SynErr(171); Get();}
+ while (!(StartOf(19))) {SynErr(170); Get();}
switch (la.kind) {
case 38: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
@@ -2014,8 +2023,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
breakCount++;
}
- } else SynErr(172);
- while (!(la.kind == 0 || la.kind == 25)) {SynErr(173); Get();}
+ } else SynErr(171);
+ while (!(la.kind == 0 || la.kind == 25)) {SynErr(172); Get();}
Expect(25);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
@@ -2028,7 +2037,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo SkeletonStmt(out s);
break;
}
- default: SynErr(174); break;
+ default: SynErr(173); break;
}
}
@@ -2047,7 +2056,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 51) {
Get();
dotdotdot = t;
- } else SynErr(175);
+ } else SynErr(174);
Expect(25);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -2072,7 +2081,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 51) {
Get();
dotdotdot = t;
- } else SynErr(176);
+ } else SynErr(175);
Expect(25);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -2142,13 +2151,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo suchThatAssume = t;
}
Expression(out suchThat, false, true);
- } else SynErr(177);
+ } else SynErr(176);
Expect(25);
endTok = t;
} else if (la.kind == 19) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(178);
+ } else SynErr(177);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -2212,7 +2221,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out suchThat, false, true);
}
}
- while (!(la.kind == 0 || la.kind == 25)) {SynErr(179); Get();}
+ while (!(la.kind == 0 || la.kind == 25)) {SynErr(178); Get();}
Expect(25);
endTok = t;
ConcreteUpdateStatement update;
@@ -2268,7 +2277,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 38) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(180);
+ } else SynErr(179);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -2276,7 +2285,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(181);
+ } else SynErr(180);
}
void WhileStmt(out Statement stmt) {
@@ -2321,7 +2330,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(51);
bodyEllipsis = t; endTok = t; isDirtyLoop = false;
} else if (StartOf(23)) {
- } else SynErr(182);
+ } else SynErr(181);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -2339,7 +2348,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else SynErr(183);
+ } else SynErr(182);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -2364,7 +2373,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseStatement(out c);
cases.Add(c);
}
- } else SynErr(184);
+ } else SynErr(183);
s = new MatchStmt(x, t, e, cases, usesOptionalBrace);
}
@@ -2389,7 +2398,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
- } else SynErr(185);
+ } else SynErr(184);
if (la.kind == _openparen) {
Expect(42);
if (la.kind == 1) {
@@ -2400,7 +2409,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == _ident) {
QuantifierDomain(out bvars, out attrs, out range);
}
- } else SynErr(186);
+ } else SynErr(185);
if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
@@ -2486,7 +2495,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 29) {
CalcStmt(out subCalc);
hintEnd = subCalc.EndTok; subhints.Add(subCalc);
- } else SynErr(187);
+ } else SynErr(186);
}
var h = new BlockStmt(hintStart, hintEnd, subhints); // if the hint is empty, hintStart is the first token of the next line, but it doesn't matter because the block statement is just used as a container
hints.Add(h);
@@ -2528,14 +2537,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 51) {
Get();
ellipsisToken = t;
- } else SynErr(188);
+ } else SynErr(187);
if (la.kind == 38) {
BlockStmt(out body, out bodyStart, out endTok);
} else if (la.kind == 25) {
- while (!(la.kind == 0 || la.kind == 25)) {SynErr(189); Get();}
+ while (!(la.kind == 0 || la.kind == 25)) {SynErr(188); Get();}
Get();
endTok = t;
- } else SynErr(190);
+ } else SynErr(189);
s = new ModifyStmt(tok, endTok, mod, attrs, body);
if (ellipsisToken != null) {
s = new SkeletonStatement(s, ellipsisToken, null);
@@ -2555,7 +2564,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 81) {
Get();
returnTok = t; isYield = true;
- } else SynErr(191);
+ } else SynErr(190);
if (StartOf(26)) {
Rhs(out r);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -2622,7 +2631,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 24 || la.kind == 40 || la.kind == 42) {
+ if (la.kind == 40 || la.kind == 42) {
if (la.kind == 40) {
Get();
ee = new List<Expression>();
@@ -2632,11 +2641,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
x = null; args = new List<Expression/*!*/>();
- if (la.kind == 24) {
- Get();
- Ident(out x);
- }
- Expect(42);
+ Get();
if (StartOf(7)) {
Expressions(args);
}
@@ -2646,7 +2651,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (ee != null) {
r = new TypeRhs(newToken, ty, ee);
} else if (args != null) {
- r = new TypeRhs(newToken, ty, x == null ? null : x.val, args);
+ r = new TypeRhs(newToken, ty, args, false);
} else {
r = new TypeRhs(newToken, ty);
}
@@ -2657,7 +2662,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(7)) {
Expression(out e, false, true);
r = new ExprRhs(e);
- } else SynErr(192);
+ } else SynErr(191);
while (la.kind == 38) {
Attribute(ref attrs);
}
@@ -2678,7 +2683,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 24 || la.kind == 40 || la.kind == 42) {
Suffix(ref e);
}
- } else SynErr(193);
+ } else SynErr(192);
}
void Expressions(List<Expression> args) {
@@ -2727,7 +2732,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(7)) {
Expression(out ee, true, true);
e = ee;
- } else SynErr(194);
+ } else SynErr(193);
}
void LoopSpec(List<MaybeFreeExpression> invariants, List<Expression> decreases, ref List<FrameExpression> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2735,7 +2740,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo bool isFree = false; Attributes attrs = null;
if (la.kind == 34 || la.kind == 79) {
- while (!(la.kind == 0 || la.kind == 34 || la.kind == 79)) {SynErr(195); Get();}
+ while (!(la.kind == 0 || la.kind == 34 || la.kind == 79)) {SynErr(194); Get();}
if (la.kind == 79) {
Get();
isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated");
@@ -2748,7 +2753,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo invariants.Add(new MaybeFreeExpression(e, isFree, attrs));
OldSemi();
} else if (la.kind == 33) {
- while (!(la.kind == 0 || la.kind == 33)) {SynErr(196); Get();}
+ while (!(la.kind == 0 || la.kind == 33)) {SynErr(195); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
@@ -2756,7 +2761,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, true, true);
OldSemi();
} else if (la.kind == 35) {
- while (!(la.kind == 0 || la.kind == 35)) {SynErr(197); Get();}
+ while (!(la.kind == 0 || la.kind == 35)) {SynErr(196); Get();}
Get();
mod = mod ?? new List<FrameExpression>();
while (IsAttribute()) {
@@ -2770,7 +2775,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
OldSemi();
- } else SynErr(198);
+ } else SynErr(197);
}
void CaseStatement(out MatchCaseStmt/*!*/ c) {
@@ -2795,10 +2800,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(43);
}
Expect(26);
- while (!(StartOf(28))) {SynErr(199); Get();}
+ while (!(StartOf(28))) {SynErr(198); Get();}
while (IsNotEndOfCase()) {
Stmt(body);
- while (!(StartOf(28))) {SynErr(200); Get();}
+ while (!(StartOf(28))) {SynErr(199); Get();}
}
c = new MatchCaseStmt(x, id.val, arguments, body);
}
@@ -2897,7 +2902,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(201); break;
+ default: SynErr(200); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2912,7 +2917,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 107) {
Get();
- } else SynErr(202);
+ } else SynErr(201);
}
void ImpliesOp() {
@@ -2920,7 +2925,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 109) {
Get();
- } else SynErr(203);
+ } else SynErr(202);
}
void ExpliesOp() {
@@ -2928,7 +2933,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 111) {
Get();
- } else SynErr(204);
+ } else SynErr(203);
}
void AndOp() {
@@ -2936,7 +2941,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 113) {
Get();
- } else SynErr(205);
+ } else SynErr(204);
}
void OrOp() {
@@ -2944,7 +2949,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 115) {
Get();
- } else SynErr(206);
+ } else SynErr(205);
}
void NegOp() {
@@ -2952,7 +2957,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 117) {
Get();
- } else SynErr(207);
+ } else SynErr(206);
}
void Forall() {
@@ -2960,7 +2965,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 118) {
Get();
- } else SynErr(208);
+ } else SynErr(207);
}
void Exists() {
@@ -2968,7 +2973,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 120) {
Get();
- } else SynErr(209);
+ } else SynErr(208);
}
void QSep() {
@@ -2976,7 +2981,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 23) {
Get();
- } else SynErr(210);
+ } else SynErr(209);
}
void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) {
@@ -3010,7 +3015,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LogicalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
}
- } else SynErr(211);
+ } else SynErr(210);
}
}
@@ -3040,7 +3045,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo RelationalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
}
- } else SynErr(212);
+ } else SynErr(211);
}
}
@@ -3258,7 +3263,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(213); break;
+ default: SynErr(212); break;
}
}
@@ -3280,7 +3285,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 123) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(214);
+ } else SynErr(213);
}
void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3326,7 +3331,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsSuffix()) {
Suffix(ref e);
}
- } else SynErr(215);
+ } else SynErr(214);
}
void MulOp(out IToken x, out BinaryExpr.Opcode op) {
@@ -3340,7 +3345,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 125) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(216);
+ } else SynErr(215);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3378,7 +3383,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 101) {
HashCall(id, out openParen, out typeArgs, out args);
} else if (StartOf(30)) {
- } else SynErr(217);
+ } else SynErr(216);
e = new ExprDotName(id, e, id.val, typeArgs);
if (openParen != null) {
e = new ApplySuffix(openParen, e, args);
@@ -3431,7 +3436,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(218);
+ } else SynErr(217);
} else if (la.kind == 132) {
Get();
anyDots = true;
@@ -3439,7 +3444,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true, true);
e1 = ee;
}
- } else SynErr(219);
+ } else SynErr(218);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3483,7 +3488,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(43);
e = new ApplySuffix(openParen, e, args);
- } else SynErr(220);
+ } else SynErr(219);
}
void LambdaExpression(out Expression e, bool allowSemi) {
@@ -3512,7 +3517,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
Expect(43);
- } else SynErr(221);
+ } else SynErr(220);
while (la.kind == 36 || la.kind == 37) {
if (la.kind == 36) {
Get();
@@ -3581,7 +3586,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(222); break;
+ default: SynErr(221); break;
}
}
@@ -3596,7 +3601,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 101) {
HashCall(id, out openParen, out typeArgs, out args);
} else if (StartOf(30)) {
- } else SynErr(223);
+ } else SynErr(222);
e = new NameSegment(id, id.val, typeArgs);
if (openParen != null) {
e = new ApplySuffix(openParen, e, args);
@@ -3625,7 +3630,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SeqDisplayExpr(x, elements);
Expect(41);
- } else SynErr(224);
+ } else SynErr(223);
}
void MultiSetExpr(out Expression e) {
@@ -3649,7 +3654,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, true);
e = new MultiSetFormingExpr(x, e);
Expect(43);
- } else SynErr(225);
+ } else SynErr(224);
}
void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3745,7 +3750,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(226); break;
+ default: SynErr(225); break;
}
}
@@ -3774,7 +3779,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero;
}
- } else SynErr(227);
+ } else SynErr(226);
}
void Dec(out Basetypes.BigDec d) {
@@ -3818,7 +3823,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 27) {
Get();
oneShot = true;
- } else SynErr(228);
+ } else SynErr(227);
}
void MapLiteralExpressions(out List<ExpressionPair> elements) {
@@ -3877,7 +3882,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseExpression(out c, allowSemi, allowLambda);
cases.Add(c);
}
- } else SynErr(229);
+ } else SynErr(228);
e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
@@ -3895,7 +3900,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 119 || la.kind == 120) {
Exists();
x = t;
- } else SynErr(230);
+ } else SynErr(229);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi, allowLambda);
@@ -3943,7 +3948,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s);
} else if (la.kind == 29) {
CalcStmt(out s);
- } else SynErr(231);
+ } else SynErr(230);
}
void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3983,7 +3988,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else SynErr(232);
+ } else SynErr(231);
Expression(out e, false, true);
letRHSs.Add(e);
while (la.kind == 20) {
@@ -4034,7 +4039,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(233);
+ } else SynErr(232);
if (pat == null) {
pat = new CasePattern(t, "_ParseError", new List<CasePattern>());
}
@@ -4125,7 +4130,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 36) {
Get();
x = t;
- } else SynErr(234);
+ } else SynErr(233);
}
@@ -4363,75 +4368,74 @@ public class Errors { case 163: s = "invalid MethodSpec"; break;
case 164: s = "invalid MethodSpec"; break;
case 165: s = "invalid FrameExpression"; break;
- case 166: s = "invalid ReferenceType"; break;
- case 167: s = "this symbol not expected in FunctionSpec"; break;
- case 168: s = "invalid FunctionSpec"; break;
- case 169: s = "invalid PossiblyWildFrameExpression"; break;
- case 170: s = "invalid PossiblyWildExpression"; break;
- case 171: s = "this symbol not expected in OneStmt"; break;
- case 172: s = "invalid OneStmt"; break;
- case 173: s = "this symbol not expected in OneStmt"; break;
- case 174: s = "invalid OneStmt"; break;
- case 175: s = "invalid AssertStmt"; break;
- case 176: s = "invalid AssumeStmt"; break;
+ case 166: s = "this symbol not expected in FunctionSpec"; break;
+ case 167: s = "invalid FunctionSpec"; break;
+ case 168: s = "invalid PossiblyWildFrameExpression"; break;
+ case 169: s = "invalid PossiblyWildExpression"; break;
+ case 170: s = "this symbol not expected in OneStmt"; break;
+ case 171: s = "invalid OneStmt"; break;
+ case 172: s = "this symbol not expected in OneStmt"; break;
+ case 173: s = "invalid OneStmt"; break;
+ case 174: s = "invalid AssertStmt"; break;
+ case 175: s = "invalid AssumeStmt"; break;
+ case 176: s = "invalid UpdateStmt"; break;
case 177: s = "invalid UpdateStmt"; break;
- case 178: s = "invalid UpdateStmt"; break;
- case 179: s = "this symbol not expected in VarDeclStatement"; break;
+ case 178: s = "this symbol not expected in VarDeclStatement"; break;
+ case 179: s = "invalid IfStmt"; break;
case 180: s = "invalid IfStmt"; break;
- case 181: s = "invalid IfStmt"; break;
+ case 181: s = "invalid WhileStmt"; break;
case 182: s = "invalid WhileStmt"; break;
- case 183: s = "invalid WhileStmt"; break;
- case 184: s = "invalid MatchStmt"; break;
+ case 183: s = "invalid MatchStmt"; break;
+ case 184: s = "invalid ForallStmt"; break;
case 185: s = "invalid ForallStmt"; break;
- case 186: s = "invalid ForallStmt"; break;
- case 187: s = "invalid CalcStmt"; break;
- case 188: s = "invalid ModifyStmt"; break;
- case 189: s = "this symbol not expected in ModifyStmt"; break;
- case 190: s = "invalid ModifyStmt"; break;
- case 191: s = "invalid ReturnStmt"; break;
- case 192: s = "invalid Rhs"; break;
- case 193: s = "invalid Lhs"; break;
- case 194: s = "invalid Guard"; break;
+ case 186: s = "invalid CalcStmt"; break;
+ case 187: s = "invalid ModifyStmt"; break;
+ case 188: s = "this symbol not expected in ModifyStmt"; break;
+ case 189: s = "invalid ModifyStmt"; break;
+ case 190: s = "invalid ReturnStmt"; break;
+ case 191: s = "invalid Rhs"; break;
+ case 192: s = "invalid Lhs"; break;
+ case 193: s = "invalid Guard"; break;
+ case 194: s = "this symbol not expected in LoopSpec"; break;
case 195: s = "this symbol not expected in LoopSpec"; break;
case 196: s = "this symbol not expected in LoopSpec"; break;
- case 197: s = "this symbol not expected in LoopSpec"; break;
- case 198: s = "invalid LoopSpec"; break;
+ case 197: s = "invalid LoopSpec"; break;
+ case 198: s = "this symbol not expected in CaseStatement"; break;
case 199: s = "this symbol not expected in CaseStatement"; break;
- case 200: s = "this symbol not expected in CaseStatement"; break;
- case 201: s = "invalid CalcOp"; break;
- case 202: s = "invalid EquivOp"; break;
- case 203: s = "invalid ImpliesOp"; break;
- case 204: s = "invalid ExpliesOp"; break;
- case 205: s = "invalid AndOp"; break;
- case 206: s = "invalid OrOp"; break;
- case 207: s = "invalid NegOp"; break;
- case 208: s = "invalid Forall"; break;
- case 209: s = "invalid Exists"; break;
- case 210: s = "invalid QSep"; break;
- case 211: s = "invalid ImpliesExpliesExpression"; break;
- case 212: s = "invalid LogicalExpression"; break;
- case 213: s = "invalid RelOp"; break;
- case 214: s = "invalid AddOp"; break;
- case 215: s = "invalid UnaryExpression"; break;
- case 216: s = "invalid MulOp"; break;
+ case 200: s = "invalid CalcOp"; break;
+ case 201: s = "invalid EquivOp"; break;
+ case 202: s = "invalid ImpliesOp"; break;
+ case 203: s = "invalid ExpliesOp"; break;
+ case 204: s = "invalid AndOp"; break;
+ case 205: s = "invalid OrOp"; break;
+ case 206: s = "invalid NegOp"; break;
+ case 207: s = "invalid Forall"; break;
+ case 208: s = "invalid Exists"; break;
+ case 209: s = "invalid QSep"; break;
+ case 210: s = "invalid ImpliesExpliesExpression"; break;
+ case 211: s = "invalid LogicalExpression"; break;
+ case 212: s = "invalid RelOp"; break;
+ case 213: s = "invalid AddOp"; break;
+ case 214: s = "invalid UnaryExpression"; break;
+ case 215: s = "invalid MulOp"; break;
+ case 216: s = "invalid Suffix"; break;
case 217: s = "invalid Suffix"; break;
case 218: s = "invalid Suffix"; break;
case 219: s = "invalid Suffix"; break;
- case 220: s = "invalid Suffix"; break;
- case 221: s = "invalid LambdaExpression"; break;
- case 222: s = "invalid EndlessExpression"; break;
- case 223: s = "invalid NameSegment"; break;
- case 224: s = "invalid DisplayExpr"; break;
- case 225: s = "invalid MultiSetExpr"; break;
- case 226: s = "invalid ConstAtomExpression"; break;
- case 227: s = "invalid Nat"; break;
- case 228: s = "invalid LambdaArrow"; break;
- case 229: s = "invalid MatchExpression"; break;
- case 230: s = "invalid QuantifierGuts"; break;
- case 231: s = "invalid StmtInExpr"; break;
- case 232: s = "invalid LetExpr"; break;
- case 233: s = "invalid CasePattern"; break;
- case 234: s = "invalid DotSuffix"; break;
+ case 220: s = "invalid LambdaExpression"; break;
+ case 221: s = "invalid EndlessExpression"; break;
+ case 222: s = "invalid NameSegment"; break;
+ case 223: s = "invalid DisplayExpr"; break;
+ case 224: s = "invalid MultiSetExpr"; break;
+ case 225: s = "invalid ConstAtomExpression"; break;
+ case 226: s = "invalid Nat"; break;
+ case 227: s = "invalid LambdaArrow"; break;
+ case 228: s = "invalid MatchExpression"; break;
+ case 229: s = "invalid QuantifierGuts"; break;
+ case 230: s = "invalid StmtInExpr"; break;
+ case 231: s = "invalid LetExpr"; break;
+ case 232: s = "invalid CasePattern"; break;
+ case 233: s = "invalid DotSuffix"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 794dfe05..80fc1d1d 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -399,12 +399,7 @@ namespace Microsoft.Dafny { private void PrintTypeInstantiation(List<Type> typeArgs) {
Contract.Requires(typeArgs == null || typeArgs.Count != 0);
if (typeArgs != null) {
- var prefix = "<";
- foreach (var ty in typeArgs) {
- wr.Write("{0}{1}", prefix, ty);
- prefix = ", ";
- }
- wr.Write(">");
+ wr.Write("<{0}>", Util.Comma(",", typeArgs, ty => ty.ToString()));
}
}
@@ -904,6 +899,9 @@ namespace Microsoft.Dafny { string sep = "(";
foreach (BoundVar bv in mc.Arguments) {
wr.Write("{0}{1}", sep, bv.DisplayName);
+ if (bv.Type is NonProxyType) {
+ wr.Write(": {0}", bv.Type);
+ }
sep = ", ";
}
wr.Write(")");
@@ -1106,8 +1104,8 @@ namespace Microsoft.Dafny { } else if (rhs is TypeRhs) {
TypeRhs t = (TypeRhs)rhs;
wr.Write("new ");
- PrintType(t.EType);
if (t.ArrayDimensions != null) {
+ PrintType(t.EType);
string s = "[";
foreach (Expression dim in t.ArrayDimensions) {
Contract.Assume(dim != null);
@@ -1117,11 +1115,9 @@ namespace Microsoft.Dafny { }
wr.Write("]");
} else if (t.Arguments == null) {
- // nothing else to print
+ PrintType(t.EType);
} else {
- if (t.OptionalNameComponent != null) {
- wr.Write(".{0}", t.OptionalNameComponent);
- }
+ PrintType(t.Path);
wr.Write("(");
PrintExpressionList(t.Arguments, false);
wr.Write(")");
@@ -1201,6 +1197,9 @@ namespace Microsoft.Dafny { string sep = "(";
foreach (BoundVar bv in mc.Arguments) {
wr.Write("{0}{1}", sep, bv.DisplayName);
+ if (bv.Type is NonProxyType) {
+ wr.Write(": {0}", bv.Type);
+ }
sep = ", ";
}
wr.Write(")");
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 8234846e..6067ed50 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -332,10 +332,7 @@ namespace Microsoft.Dafny if (newMem is Function) {
CheckFunctionsAreRefinements((Function)newMem, (Function)m);
} else {
- bool isPredicate = m is Predicate;
- bool isCoPredicate = m is CoPredicate;
- string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";
- reporter.Error(newMem, "{0} must be refined by a {0}", s);
+ reporter.Error(newMem, "{0} must be refined by a {0}", m.WhatKind);
}
}
} else {
@@ -690,19 +687,18 @@ namespace Microsoft.Dafny var f = (Function)nwMember;
bool isPredicate = f is Predicate;
bool isCoPredicate = f is CoPredicate;
- string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";
if (!(member is Function) || (isPredicate && !(member is Predicate)) || (isCoPredicate && !(member is CoPredicate))) {
- reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", s, nwMember.Name);
+ reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", f.WhatKind, nwMember.Name);
} else {
var prevFunction = (Function)member;
if (f.Req.Count != 0) {
- reporter.Error(f.Req[0].tok, "a refining {0} is not allowed to add preconditions", s);
+ reporter.Error(f.Req[0].tok, "a refining {0} is not allowed to add preconditions", f.WhatKind);
}
if (f.Reads.Count != 0) {
- reporter.Error(f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", s);
+ reporter.Error(f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", f.WhatKind);
}
if (f.Decreases.Expressions.Count != 0) {
- reporter.Error(f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", s);
+ reporter.Error(f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", f.WhatKind);
}
if (prevFunction.HasStaticKeyword != f.HasStaticKeyword) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 887a387f..51121ea0 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -101,6 +101,7 @@ namespace Microsoft.Dafny }
class AmbiguousTopLevelDecl : TopLevelDecl, IAmbiguousThing<TopLevelDecl> // only used with "classes"
{
+ public override string WhatKind { get { return A.WhatKind; } }
readonly TopLevelDecl A;
readonly TopLevelDecl B;
public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b)
@@ -140,6 +141,7 @@ namespace Microsoft.Dafny class AmbiguousMemberDecl : MemberDecl, IAmbiguousThing<MemberDecl> // only used with "classes"
{
+ public override string WhatKind { get { return A.WhatKind; } }
readonly MemberDecl A;
readonly MemberDecl B;
public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)
@@ -1305,7 +1307,7 @@ namespace Microsoft.Dafny }
// Now, we're ready for the other declarations.
foreach (TopLevelDecl d in declarations) {
- if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0)
+ if (d is TraitDecl && d.TypeArgs.Count > 0)
{
Error(d, "a trait cannot declare type parameters");
}
@@ -1934,11 +1936,10 @@ namespace Microsoft.Dafny }
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
- var what = e.Member is Function ? "function" : e.Member is Method ? "method" : null;
- if (what != null) {
+ if (e.Member is Function || e.Member is Method) {
foreach (var p in e.TypeApplication) {
if (!IsDetermined(p.Normalize())) {
- Error(e.tok, "type '{0}' to the {2} '{1}' is not determined", p, e.Member.Name, what);
+ Error(e.tok, "type '{0}' to the {2} '{1}' is not determined", p, e.Member.Name, e.Member.WhatKind);
}
}
}
@@ -3921,25 +3922,22 @@ namespace Microsoft.Dafny public class ResolveTypeReturn
{
public readonly Type ReplacementType;
- public readonly string LastName;
- public readonly IToken LastToken;
- public ResolveTypeReturn(Type replacementType, string lastName, IToken lastToken) {
+ public readonly ExprDotName LastComponent;
+ public ResolveTypeReturn(Type replacementType, ExprDotName lastComponent) {
Contract.Requires(replacementType != null);
- Contract.Requires(lastName != null);
- Contract.Requires(lastToken != null);
+ Contract.Requires(lastComponent != null);
ReplacementType = replacementType;
- LastName = lastName;
- LastToken = lastToken;
+ LastComponent = lastComponent;
}
}
/// <summary>
/// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters.
- /// One more thing: if "allowShortenedPath" is true, then if the resolution would have produced
+ /// One more thing: if "allowDanglingDotName" is true, then if the resolution would have produced
/// an error message that could have been avoided if "type" denoted an identifier sequence one
/// shorter, then return an unresolved replacement type where the identifier sequence is one
/// shorter. (In all other cases, the method returns null.)
/// </summary>
- public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ICodeContext context, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments, bool allowShortenedPath) {
+ public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ICodeContext context, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments, bool allowDanglingDotName) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
Contract.Requires(context != null);
@@ -4005,76 +4003,29 @@ namespace Microsoft.Dafny } else if (type is UserDefinedType) {
var t = (UserDefinedType)type;
- var isArrow = t is ArrowType;
if (t.ResolvedClass != null || t.ResolvedParam != null) {
// Apparently, this type has already been resolved
return null;
}
- foreach (Type tt in t.TypeArgs) {
- ResolveType(t.tok, tt, context, option, defaultTypeArguments);
- if (tt.IsSubrangeType && !isArrow) {
- Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
- }
- }
- TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null;
- if (tp != null) {
- if (t.TypeArgs.Count == 0) {
- t.ResolvedParam = tp;
- } else {
- Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
+ var prevErrorCount = ErrorCount;
+ if (t.NamePath is ExprDotName) {
+ var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true), allowDanglingDotName, option, defaultTypeArguments);
+ if (ret != null) {
+ return ret;
}
} else {
- TopLevelDecl d = null;
-
- int j;
- var sig = moduleInfo;
- for (j = 0; j < t.Path.Count; j++) {
- ModuleSignature submodule;
- if (sig.FindSubmodule(t.Path[j].val, out submodule)) {
- sig = GetSignature(submodule);
- } else {
- // maybe the last component of t.Path is actually the type name
- if (allowShortenedPath && t.TypeArgs.Count == 0 && j == t.Path.Count - 1 && sig.TopLevels.TryGetValue(t.Path[j].val, out d)) {
- // move the last component of t.Path to t.tok/t.name, tell the caller about this, and continue
- var reducedPath = new List<IToken>();
- for (int i = 0; i < j; i++) {
- reducedPath.Add(t.Path[i]);
- }
- return new ResolveTypeReturn(new UserDefinedType(t.Path[j], t.Path[j].val, t.TypeArgs, reducedPath), t.Name, t.tok);
- } else {
- Error(t.Path[j], ModuleNotFoundErrorMessage(j, t.Path));
- }
- break;
- }
- }
- if (j == t.Path.Count) {
- if (!sig.TopLevels.TryGetValue(t.Name, out d)) {
- if (j == 0) {
- if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && t.TypeArgs.Count == 0) {
- tp = new TypeParameter(tok, t.Name, defaultTypeArguments.Count, option.Parent);
- defaultTypeArguments.Add(tp);
- t.ResolvedParam = tp;
- allTypeParameters.Push(t.Name, tp);
- } else {
- Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)",
- t.Name);
- }
- } else {
- Error(t.tok, "Undeclared type {0} in module {1}", t.Name, t.Path[t.Path.Count - 1].val);
- }
- }
- } else {
- // error has already been reported
- }
-
- if (d == null) {
- // error has been reported above
- } else if (ReallyAmbiguousTopLevelDecl(ref d)) {
- Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
- } else {
- string what;
+ var s = (NameSegment)t.NamePath;
+ ResolveNameSegment_Type(s, new ResolveOpts(context, true), option, defaultTypeArguments);
+ }
+ if (ErrorCount == prevErrorCount) {
+ var r = t.NamePath.Resolved as Resolver_IdentifierExpr;
+ if (r == null || !(r.Type is Resolver_IdentifierExpr.ResolverType_Type)) {
+ Error(t.tok, "expected type");
+ } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type && r.TypeParamDecl != null) {
+ t.ResolvedParam = r.TypeParamDecl;
+ } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+ var d = r.Decl;
if (d is OpaqueTypeDecl) {
- what = "opaque type";
t.ResolvedParam = ((OpaqueTypeDecl)d).TheType; // resolve like a type parameter, and it may have type parameters if it's an opaque type
} else if (d is NewtypeDecl) {
var dd = (NewtypeDecl)d;
@@ -4086,11 +4037,9 @@ namespace Microsoft.Dafny Error(dd.tok, "recursive dependency involving a newtype: {0} -> {0}", dd.Name);
}
}
- what = "newtype";
t.ResolvedClass = dd;
} else {
// d is a class or datatype, and it may have type parameters
- what = isArrow ? "function type" : "class/datatype";
t.ResolvedClass = d;
}
if (option.Opt == ResolveTypeOptionEnum.DontInfer) {
@@ -4100,8 +4049,9 @@ namespace Microsoft.Dafny }
// defaults and auto have been applied; check if we now have the right number of arguments
if (d.TypeArgs.Count != t.TypeArgs.Count) {
- Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", t.TypeArgs.Count, d.TypeArgs.Count, what, t.Name);
+ Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", t.TypeArgs.Count, d.TypeArgs.Count, d.WhatKind, t.Name);
}
+
}
}
@@ -4176,9 +4126,7 @@ namespace Microsoft.Dafny Contract.Assert(n <= defaultTypeArguments.Count);
// automatically supply a prefix of the arguments from defaultTypeArguments
for (int i = 0; i < n; i++) {
- var typeArg = new UserDefinedType(tok, defaultTypeArguments[i].Name, new List<Type>(), null);
- typeArg.ResolvedParam = defaultTypeArguments[i]; // resolve "typeArg" here
- typeArgs.Add(typeArg);
+ typeArgs.Add(new UserDefinedType(defaultTypeArguments[i]));
}
}
}
@@ -6009,7 +5957,7 @@ namespace Microsoft.Dafny if (rr.Type == null) {
if (rr.ArrayDimensions != null) {
// ---------- new T[EE]
- Contract.Assert(rr.Arguments == null && rr.OptionalNameComponent == null && rr.InitCall == null);
+ Contract.Assert(rr.Arguments == null && rr.Path == null && rr.InitCall == null);
ResolveType(stmt.Tok, rr.EType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
int i = 0;
foreach (Expression dim in rr.ArrayDimensions) {
@@ -6022,42 +5970,44 @@ namespace Microsoft.Dafny }
rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType, codeContext);
} else {
- var initCallTok = rr.Tok;
- if (rr.OptionalNameComponent == null && rr.Arguments != null) {
- // Resolve rr.EType and do one of three things:
- // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the anonymous constructor.
- // * If the all-but-last components of rr.EType denote a type, then do EType,OptionalNameComponent := allButLast(EType),last(EType)
+ bool callsConstructor = false;
+ if (rr.Arguments == null) {
+ ResolveType(stmt.Tok, rr.EType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
+ if (!rr.EType.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
+ }
+ } else {
+ string initCallName = null;
+ IToken initCallTok = null;
+ // Resolve rr.Path and do one of three things:
+ // * If rr.Path denotes a type, then set EType,initCallName to rr.Path,"_ctor", which sets up a call to the anonymous constructor.
+ // * If the all-but-last components of rr.Path denote a type, then do EType,initCallName := allButLast(EType),last(EType)
// * Otherwise, report an error
- var ret = ResolveTypeLenient(stmt.Tok, rr.EType, codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null, true);
+ var ret = ResolveTypeLenient(rr.Tok, rr.Path, codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null, true);
if (ret != null) {
- // While rr.EType does not denote a type, no error has been reported yet and the all-but-last components of rr.EType may
- // denote a type, so shift the last component to OptionalNameComponent and retry with the suggested type.
- rr.OptionalNameComponent = ret.LastName;
+ // The all-but-last components of rr.Path denote a type (namely, ret.ReplacementType).
rr.EType = ret.ReplacementType;
- initCallTok = ret.LastToken;
- ResolveType(stmt.Tok, rr.EType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
+ initCallName = ret.LastComponent.SuffixName;
+ initCallTok = ret.LastComponent.tok;
+ } else {
+ // Either rr.Path resolved correctly as a type or there was no way to drop a last component to make it into something that looked
+ // like a type. In either case, set EType,initCallName to Path,"_ctor" and continue.
+ rr.EType = rr.Path;
+ initCallName = "_ctor";
+ initCallTok = rr.Tok;
+ }
+ if (!rr.EType.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
} else {
- // Either rr.EType resolved correctly as a type or there was no way to drop a last component to make it into something that looked
- // like a type. In either case, set OptionalNameComponent to "_ctor" and continue.
- rr.OptionalNameComponent = "_ctor";
- }
- } else {
- ResolveType(stmt.Tok, rr.EType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
- }
- if (!rr.EType.IsRefType) {
- Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
- } else {
- bool callsConstructor = false;
- if (rr.Arguments != null) {
// ---------- new C.Init(EE)
- Contract.Assert(rr.OptionalNameComponent != null); // if it wasn't non-null from the beginning, the code above would have set it to a non-null value
+ Contract.Assert(initCallName != null);
var prevErrorCount = ErrorCount;
// We want to create a MemberSelectExpr for the initializing method. To do that, we create a throw-away receiver of the appropriate
// type, create an dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions.
var lhs = new ImplicitThisExpr(initCallTok) { Type = rr.EType };
- var callLhs = new ExprDotName(initCallTok, lhs, rr.OptionalNameComponent, null/*TODO: if the all-but-last components of the original EType above denote a type, then we should use any type arguments of the final EType component here*/);
- ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true, specContextOnly), true); // we use this call instead of the regular ResolveDotSuffix, since callLhs.Expr has already been resolved
+ var callLhs = new ExprDotName(initCallTok, lhs, initCallName, ret == null ? null : ret.LastComponent.OptTypeArguments);
+ ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true, specContextOnly), true);
if (prevErrorCount == ErrorCount) {
Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr); // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)
var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;
@@ -6068,15 +6018,14 @@ namespace Microsoft.Dafny callsConstructor = true;
}
} else {
- Error(initCallTok, "object initialization must denote an initializing method or constructor ({0})", rr.OptionalNameComponent);
+ Error(initCallTok, "object initialization must denote an initializing method or constructor ({0})", initCallName);
}
}
- } else {
- // ---------- new C
- Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null);
}
- if (rr.EType.NormalizeExpand() is UserDefinedType) {
- var udt = (UserDefinedType)rr.EType.NormalizeExpand();
+ }
+ if (rr.EType.IsRefType) {
+ var udt = rr.EType.NormalizeExpand() as UserDefinedType;
+ if (udt != null) {
var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
if (cl is TraitDecl) {
Error(stmt, "new cannot be applied to a trait");
@@ -6282,7 +6231,8 @@ namespace Microsoft.Dafny // there were no substitutions
return type;
} else {
- return new UserDefinedType(t.tok, t.Name, resolvedClass, newArgs, t.Path);
+ // Note, even if t.NamePath is non-null, we don't care to keep that syntactic part of the expression in what we return here
+ return new UserDefinedType(t.tok, t.Name, resolvedClass, newArgs);
}
} else {
// there's neither a resolved param nor a resolved class, which means the UserDefinedType wasn't
@@ -6308,7 +6258,7 @@ namespace Microsoft.Dafny List<Type> args = new List<Type>();
foreach (TypeParameter tp in cl.TypeArgs) {
- args.Add(new UserDefinedType(tok, tp.Name, tp));
+ args.Add(new UserDefinedType(tok, tp));
}
return new UserDefinedType(tok, cl.Name, cl, args);
}
@@ -6436,7 +6386,7 @@ namespace Microsoft.Dafny } else if (e is CharLiteralExpr) {
e.Type = Type.Char;
} else if (e is StringLiteralExpr) {
- e.Type = new UserDefinedType(e.tok, "string", new List<Type>(), new List<IToken>());
+ e.Type = new UserDefinedType(e.tok, "string", (List<Type>)null);
ResolveType(e.tok, e.Type, opts.codeContext, ResolveTypeOptionEnum.DontInfer, null);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type
@@ -6465,7 +6415,7 @@ namespace Microsoft.Dafny if (!moduleInfo.TopLevels.TryGetValue(dtv.DatatypeName, out d)) {
Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName);
} else if (ReallyAmbiguousTopLevelDecl(ref d)) {
- Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else if (!(d is DatatypeDecl)) {
Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);
} else {
@@ -7478,7 +7428,7 @@ namespace Microsoft.Dafny } else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {
// ----- 3. Member of the enclosing module
if (ReallyAmbiguousTopLevelDecl(ref decl)) {
- Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());
} else {
// We have found a module name or a type name, neither of which is an expression. However, the NameSegment we're
// looking at may be followed by a further suffix that makes this into an expresion. We postpone the rest of the
@@ -7491,7 +7441,7 @@ namespace Microsoft.Dafny // ----- 4. static member of the enclosing module
Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
if (ReallyAmbiguousThing(ref member)) {
- Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());
+ Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());
} else {
var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
@@ -7512,6 +7462,110 @@ namespace Microsoft.Dafny return rWithArgs;
}
+ /// <summary>
+ /// Look up expr.Name in the following order:
+ /// 0. Type parameter
+ /// 1. Member of enclosing class (an implicit "this" is inserted, if needed)
+ /// 2. Member of the enclosing module (type name or the name of a module)
+ /// 3. Static function or method in the enclosing module or its imports
+ ///
+ /// Note: 1 and 3 are not used now, but they will be of interest when async task types are supported.
+ /// </summary>
+ void ResolveNameSegment_Type(NameSegment expr, ResolveOpts opts, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments) {
+ Contract.Requires(expr != null);
+ Contract.Requires(!expr.WasResolved());
+ Contract.Requires(opts != null);
+ Contract.Requires((option.Opt == ResolveTypeOptionEnum.DontInfer || option.Opt == ResolveTypeOptionEnum.InferTypeProxies) == (defaultTypeArguments == null));
+
+ if (expr.OptTypeArguments != null) {
+ foreach (var ty in expr.OptTypeArguments) {
+ ResolveType(expr.tok, ty, opts.codeContext, option, defaultTypeArguments);
+ if (ty.IsSubrangeType) {
+ Error(expr.tok, "sorry, cannot instantiate type parameter with a subrange type");
+ }
+ }
+ }
+
+ Expression r = null; // the resolved expression, if successful
+
+ // For 0:
+ TypeParameter tp;
+#if ASYNC_TASK_TYPES
+ // For 1:
+ Dictionary<string, MemberDecl> members;
+ // For 1 and 3:
+ MemberDecl member = null;
+#endif
+ // For 2:
+ TopLevelDecl decl;
+
+ tp = allTypeParameters.Find(expr.Name);
+ if (tp != null) {
+ // ----- 0. type parameter
+ if (expr.OptTypeArguments == null) {
+ r = new Resolver_IdentifierExpr(expr.tok, tp);
+ } else {
+ Error(expr.tok, "Type parameter expects no type arguments: {0}", expr.Name);
+ }
+#if ASYNC_TASK_TYPES // At the moment, there is no way for a class member to part of a type name, but this changes with async task types
+ } else if (currentClass != null && classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(expr.Name, out member)) {
+ // ----- 1. member of the enclosing class
+ Expression receiver;
+ if (member.IsStatic) {
+ receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ } else {
+ if (!scope.AllowInstance) {
+ Error(expr.tok, "'this' is not allowed in a 'static' context");
+ // nevertheless, set "receiver" to a value so we can continue resolution
+ }
+ receiver = new ImplicitThisExpr(expr.tok);
+ receiver.Type = GetThisType(expr.tok, (ClassDecl)member.EnclosingClass); // resolve here
+ }
+ r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
+#endif
+ } else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {
+ // ----- 2. Member of the enclosing module
+ if (ReallyAmbiguousTopLevelDecl(ref decl)) {
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else {
+ // We have found a module name or a type name, neither of which is a type expression. However, the NameSegment we're
+ // looking at may be followed by a further suffix that makes this into a type expresion. We postpone the rest of the
+ // resolution to any such suffix. For now, we create a temporary expression that will never be seen by the compiler
+ // or verifier, just to have a placeholder where we can recorded what we have found.
+ r = CreateResolver_IdentifierExpr(expr.tok, expr.Name, expr.OptTypeArguments, decl);
+ }
+
+#if ASYNC_TASK_TYPES // At the moment, there is no way for a class member to part of a type name, but this changes with async task types
+ } else if (moduleInfo.StaticMembers.TryGetValue(expr.Name, out member)) {
+ // ----- 3. static member of the enclosing module
+ Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
+ if (ReallyAmbiguousThing(ref member)) {
+ Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());
+ } else {
+ var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
+ }
+#endif
+ } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && expr.OptTypeArguments == null) {
+ // it woulc plausibly be a type parameter, but isn't; we will declare it automatically
+ tp = new TypeParameter(expr.tok, expr.Name, defaultTypeArguments.Count, option.Parent);
+ defaultTypeArguments.Add(tp);
+ r = new Resolver_IdentifierExpr(expr.tok, tp);
+ allTypeParameters.Push(expr.Name, tp);
+ } else {
+ // ----- None of the above
+ Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", expr.Name);
+ }
+
+ if (r == null) {
+ // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type
+ expr.Type = new InferredTypeProxy();
+ } else {
+ expr.ResolvedExpression = r;
+ expr.Type = r.Type;
+ }
+ }
+
Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IToken tok, string name, List<Type> optTypeArguments, TopLevelDecl decl) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -7521,7 +7575,7 @@ namespace Microsoft.Dafny if (optTypeArguments != null) {
// type arguments were supplied; they must be equal in number to those expected
if (n != decl.TypeArgs.Count) {
- Error(tok, "wrong number of type arguments for '{0}' (got {1}, expected {2})", name, n, decl.TypeArgs.Count);
+ Error(tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", n, decl.TypeArgs.Count, decl.WhatKind, name);
}
}
List<Type> tpArgs = new List<Type>();
@@ -7610,7 +7664,7 @@ namespace Microsoft.Dafny } else if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {
// ----- 1. Member of the specified module
if (ReallyAmbiguousTopLevelDecl(ref decl)) {
- Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());
} else {
// We have found a module name or a type name, neither of which is an expression. However, the ExprDotName we're
// looking at may be followed by a further suffix that makes this into an expresion. We postpone the rest of the
@@ -7622,7 +7676,7 @@ namespace Microsoft.Dafny // ----- 2. static member of the specified module
Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
if (ReallyAmbiguousThing(ref member)) {
- Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());
+ Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());
} else {
var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
@@ -7633,10 +7687,14 @@ namespace Microsoft.Dafny } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
var ri = (Resolver_IdentifierExpr)lhs;
- var decl = ri.Decl;
// ----- 3. Look up name in type
- // expand any synonyms
- var ty = new UserDefinedType(expr.tok, decl.Name, decl, ri.TypeArgs).NormalizeExpand();
+ Type ty;
+ if (ri.TypeParamDecl != null) {
+ ty = new UserDefinedType(ri.TypeParamDecl);
+ } else {
+ // expand any synonyms
+ ty = new UserDefinedType(expr.tok, ri.Decl.Name, ri.Decl, ri.TypeArgs).NormalizeExpand();
+ }
if (ty.IsRefType) {
// ----- LHS is a class
var cd = (ClassDecl)((UserDefinedType)ty).ResolvedClass;
@@ -7670,7 +7728,7 @@ namespace Microsoft.Dafny }
}
if (r == null) {
- Error(expr.tok, "member '{0}' does not exist in type '{1}'", expr.SuffixName, ri.Decl.Name);
+ Error(expr.tok, "member '{0}' does not exist in type '{1}'", expr.SuffixName, ri.TypeParamDecl != null ? ri.TypeParamDecl.Name : ri.Decl.Name);
}
} else if (lhs != null) {
// ----- 4. Look up name in the type of the Lhs
@@ -7692,6 +7750,104 @@ namespace Microsoft.Dafny return rWithArgs;
}
+ /// <summary>
+ /// To resolve "id" in expression "E . id", do:
+ /// * If E denotes a module name M:
+ /// 0. Member of module M: sub-module (including submodules of imports), class, datatype, etc.
+ /// (if two imported types have the same name, an error message is produced here)
+ /// 1. Static member of M._default denoting an async task type
+ /// (Note that in contrast to ResolveNameSegment_Type, imported modules, etc. are ignored)
+ /// * If E denotes a type:
+ /// 2. a. Member of that type denoting an async task type, or:
+ /// b. If allowDanglingDotName:
+ /// Return the type "E" and the given "expr", letting the caller try to make sense of the final dot-name.
+ ///
+ /// Note: 1 and 2a are not used now, but they will be of interest when async task types are supported.
+ /// </summary>
+ ResolveTypeReturn ResolveDotSuffix_Type(ExprDotName expr, ResolveOpts opts, bool allowDanglingDotName, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments) {
+ Contract.Requires(expr != null);
+ Contract.Requires(!expr.WasResolved());
+ Contract.Requires(expr.Lhs is NameSegment || expr.Lhs is ExprDotName);
+ Contract.Requires(opts != null);
+ Contract.Ensures(Contract.Result<ResolveTypeReturn>() == null || allowDanglingDotName);
+
+ // resolve the LHS expression
+ if (expr.Lhs is NameSegment) {
+ ResolveNameSegment_Type((NameSegment)expr.Lhs, opts, option, defaultTypeArguments);
+ } else {
+ ResolveDotSuffix_Type((ExprDotName)expr.Lhs, opts, false, option, defaultTypeArguments);
+ }
+
+ if (expr.OptTypeArguments != null) {
+ foreach (var ty in expr.OptTypeArguments) {
+ ResolveType(expr.tok, ty, opts.codeContext, option, defaultTypeArguments);
+ if (ty.IsSubrangeType) {
+ Error(expr.tok, "sorry, cannot instantiate type parameter with a subrange type");
+ }
+ }
+ }
+
+ Expression r = null; // the resolved expression, if successful
+
+ var lhs = expr.Lhs.Resolved;
+ if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) {
+ var ri = (Resolver_IdentifierExpr)lhs;
+ var sig = ((ModuleDecl)ri.Decl).Signature;
+ sig = GetSignature(sig);
+ // For 0:
+ TopLevelDecl decl;
+
+ if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {
+ // ----- 0. Member of the specified module
+ if (ReallyAmbiguousTopLevelDecl(ref decl)) {
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else {
+ // We have found a module name or a type name. We create a temporary expression that will never be seen by the compiler
+ // or verifier, just to have a placeholder where we can recorded what we have found.
+ r = CreateResolver_IdentifierExpr(expr.tok, expr.SuffixName, expr.OptTypeArguments, decl);
+ }
+#if ASYNC_TASK_TYPES
+ } else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) {
+ // ----- 1. static member of the specified module
+ Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
+ if (ReallyAmbiguousThing(ref member)) {
+ Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());
+ } else {
+ var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
+ r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
+ }
+#endif
+ } else {
+ Error(expr.tok, "module '{0}' does not declare a type '{1}'", ri.Decl.Name, expr.SuffixName);
+ }
+
+ } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+ var ri = (Resolver_IdentifierExpr)lhs;
+ // ----- 2. Look up name in type
+ Type ty;
+ if (ri.TypeParamDecl != null) {
+ ty = new UserDefinedType(ri.TypeParamDecl);
+ } else {
+ ty = new UserDefinedType(expr.tok, ri.Decl.Name, ri.Decl, ri.TypeArgs);
+ }
+ if (allowDanglingDotName && ty.IsRefType) {
+ return new ResolveTypeReturn(ty, expr);
+ }
+ if (r == null) {
+ Error(expr.tok, "member '{0}' does not exist in type '{1}' or cannot be part of type name", expr.SuffixName, ri.TypeParamDecl != null ? ri.TypeParamDecl.Name : ri.Decl.Name);
+ }
+ }
+
+ if (r == null) {
+ // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type
+ expr.Type = new InferredTypeProxy();
+ } else {
+ expr.ResolvedExpression = r;
+ expr.Type = r.Type;
+ }
+ return null;
+ }
+
Expression ResolveExprDotCall(IToken tok, Expression receiver, MemberDecl member, List<Type> optTypeArguments, ICodeContext caller, bool allowMethodCall) {
Contract.Requires(tok != null);
Contract.Requires(receiver != null);
@@ -7811,23 +7967,27 @@ namespace Microsoft.Dafny } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
// It may be a conversion expression
var ri = (Resolver_IdentifierExpr)lhs;
- var decl = ri.Decl;
- var ty = new UserDefinedType(e.tok, decl.Name, decl, ri.TypeArgs);
- if (ty.AsNewtype != null) {
- if (e.Args.Count != 1) {
- Error(e.tok, "conversion operation to {0} got wrong number of arguments (expected 1, got {1})", decl.Name, e.Args.Count);
- }
- var conversionArg = 1 <= e.Args.Count ? e.Args[0] :
- ty.IsNumericBased(Type.NumericPersuation.Int) ? LiteralExpr.CreateIntLiteral(e.tok, 0) :
- LiteralExpr.CreateRealLiteral(e.tok, Basetypes.BigDec.ZERO);
- r = new ConversionExpr(e.tok, conversionArg, ty);
- ResolveExpression(r, opts);
- // resolve the rest of the arguments, if any
- for (int i = 1; i < e.Args.Count; i++) {
- ResolveExpression(e.Args[i], opts);
- }
+ if (ri.TypeParamDecl != null) {
+ Error(e.tok, "name of type parameter ({0}) is used as a function", ri.TypeParamDecl.Name);
} else {
- Error(e.tok, "name of type ({0}) is used as a function", decl.Name);
+ var decl = ri.Decl;
+ var ty = new UserDefinedType(e.tok, decl.Name, decl, ri.TypeArgs);
+ if (ty.AsNewtype != null) {
+ if (e.Args.Count != 1) {
+ Error(e.tok, "conversion operation to {0} got wrong number of arguments (expected 1, got {1})", decl.Name, e.Args.Count);
+ }
+ var conversionArg = 1 <= e.Args.Count ? e.Args[0] :
+ ty.IsNumericBased(Type.NumericPersuation.Int) ? LiteralExpr.CreateIntLiteral(e.tok, 0) :
+ LiteralExpr.CreateRealLiteral(e.tok, Basetypes.BigDec.ZERO);
+ r = new ConversionExpr(e.tok, conversionArg, ty);
+ ResolveExpression(r, opts);
+ // resolve the rest of the arguments, if any
+ for (int i = 1; i < e.Args.Count; i++) {
+ ResolveExpression(e.Args[i], opts);
+ }
+ } else {
+ Error(e.tok, "name of type ({0}) is used as a function", decl.Name);
+ }
}
} else {
if (lhs is MemberSelectExpr && ((MemberSelectExpr)lhs).Member is Method) {
@@ -7945,63 +8105,27 @@ namespace Microsoft.Dafny }
private bool ComparableTypes(Type A, Type B) {
- A = A.NormalizeExpand();
- B = B.NormalizeExpand();
- if (A.IsArrayType && B.IsArrayType) {
- Type a = UserDefinedType.ArrayElementType(A);
- Type b = UserDefinedType.ArrayElementType(B);
- return CouldPossiblyBeSameType(a, b);
- } else
- if (A is UserDefinedType && B is UserDefinedType) {
- UserDefinedType a = (UserDefinedType)A;
- UserDefinedType b = (UserDefinedType)B;
- if ((a is ArrowType) != (b is ArrowType)) {
- return false;
- }
- if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass.Name == b.ResolvedClass.Name) {
- if (a.TypeArgs.Count != b.TypeArgs.Count) {
- return false; // this probably doesn't happen if the classes are the same.
- }
- for (int i = 0; i < a.TypeArgs.Count; i++) {
- if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
- return false;
- }
- // all parameters could be the same
- return true;
- }
- // either we don't know what class it is yet, or the classes mismatch
+ // If we know that both A and B denote classes and they denote the same class,
+ // then we will say the types are comparable (for the purpose of the == and !=
+ // opeators) if it isn't blatantly impossible to instantiate the type parameters
+ // of the enclosing context so that A and B are exactly the same type.
+ var a = A.NormalizeExpand() as UserDefinedType;
+ var b = B.NormalizeExpand() as UserDefinedType;
+ if (a != null && b != null) {
+ if (a is ArrowType || b is ArrowType) {
return false;
}
- return false;
- }
- public bool CouldPossiblyBeSameType(Type A, Type B) {
- if ((A is ArrowType) != (B is ArrowType)) {
- return false;
- }
- if (A.IsTypeParameter || B.IsTypeParameter) {
- return true;
- }
- if (A.IsArrayType && B.IsArrayType) {
- Type a = UserDefinedType.ArrayElementType(A);
- Type b = UserDefinedType.ArrayElementType(B);
- return CouldPossiblyBeSameType(a, b);
- }
- if (A is UserDefinedType && B is UserDefinedType) {
- UserDefinedType a = (UserDefinedType)A;
- UserDefinedType b = (UserDefinedType)B;
- if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass == b.ResolvedClass) {
- if (a.TypeArgs.Count != b.TypeArgs.Count) {
- return false; // this probably doesn't happen if the classes are the same.
- }
- for (int i = 0; i < a.TypeArgs.Count; i++) {
- if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ var acl = a.ResolvedClass;
+ var bcl = b.ResolvedClass;
+ if (acl is ClassDecl && bcl is ClassDecl && acl == bcl) {
+ for (int i = 0; i < acl.TypeArgs.Count; i++) {
+ if (!a.TypeArgs[i].PossiblyEquals(b.TypeArgs[i])) {
return false;
+ }
}
// all parameters could be the same
return true;
}
- // either we don't know what class it is yet, or the classes mismatch
- return false;
}
return false;
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index eca1a353..f8f4b218 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -182,7 +182,7 @@ namespace Microsoft.Dafny Contract.Assert(ReprField != null); // we expect there to be a "Repr" field, since we added one in PreResolve
Boogie.IToken clTok = new AutoGeneratedToken(cl.tok);
- Type ty = new UserDefinedType(clTok, cl.Name, cl, new List<Type>());
+ Type ty = new UserDefinedType(clTok, cl.Name, cl, cl.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)));
var self = new ThisExpr(clTok);
self.Type = ty;
var implicitSelf = new ImplicitThisExpr(clTok);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9379fac7..d5b7020b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1797,7 +1797,7 @@ namespace Microsoft.Dafny { // create and resolve datatype value
var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);
r.Ctor = mc.Ctor;
- r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/, null);
+ r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);
Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
substMap.Add(formal, r);
@@ -7409,7 +7409,7 @@ namespace Microsoft.Dafny { var v = new DatatypeValue(x.tok, dt.Name, ctor.Name, new List<Expression>());
v.Ctor = ctor; // resolve here
v.InferredTypeArgs = xType.TypeArgs; // resolved here.
- v.Type = new UserDefinedType(x.tok, dt.Name, dt, new List<Type>()); // resolve here
+ v.Type = xType; // resolve here
yield return v;
}
}
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy index 1020df26..c286376c 100644 --- a/Test/dafny0/LiberalEquality.dfy +++ b/Test/dafny0/LiberalEquality.dfy @@ -12,46 +12,94 @@ class Test<T> { predicate valid()
reads this, a, b;
{
- a != null && b != null && a != b && a.Length == b.Length
+ a != null && b != null &&
+ a != b && // this is the kind of thing the liberal equalty rules are designed to support
+ a.Length == b.Length
}
}
-method m1<T, U>(t: T, u: U)
- requires t != u; // Cannot compare type parameters (can only compare reference types that could be the same)
+method m0<T, U>(t: T, u: U, x: int)
+ requires t != u; // error: Cannot compare type parameters (can only compare reference types that could be the same)
+ requires u != x; // error: the liberal equality rules apply only if the top-level type is a reference type
{
-
}
-method m2<T>(t: array<T>, a: array<int>)
- requires t != null && a != null && t != a && t.Length == a.Length;
+method m1<T>(t: array<T>, a: array<int>, b: array3<T>, c: array3<int>)
+ requires t != null && a != null && b != null && c != null;
+ requires t != a && t.Length == a.Length;
+ requires b != c && b.Length0 == c.Length0 && b.Length1 == c.Length1 && b.Length2 == c.Length2;
+ requires t != b; // error: these types are never the same
+ requires a != c; // error: these types are never the same
+ requires t != c; // error: these types are never the same
+ requires a != b; // error: these types are never the same
{
-
}
-class Weird<T, U, V>
-{
+class Weird<T, U, V> { }
+method m2<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)
+ requires a == b; // error: second parameter can't be both bool and int.
+{
}
+method m3<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)
+ requires a == b;
+{
+}
-method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)
- requires a == b; // Bad: second parameter can't be both bool and int.
+method m4<T>(a: Weird<T, T, bool>, b: Weird<T, bool, T>, c: Weird<T, int, T>)
+ requires b != c; // error: this is like in m2 above
+ requires a != b; // the types of a and b would be the same if T := bool
+ requires a != c; // this is allowed by the liberal equality rules, which are simple minded;
+ // but there isn't actually any way that the types of a and c could be the same
{
+}
+// Just to make sure nothing went wrong.
+method m5(a: array<int>, b: array<bool>)
+ requires a == b; // error: never equal
+{
}
+iterator Iter<T>() { }
-method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)
- requires a == b;
+method m6<T>(a: Iter<T>, b: Iter<int>)
+ requires a != b;
{
+}
+method m7<T>(a: T -> int, b: int -> T, c: int -> int)
+ requires a != c; // error: arrow types don't fall under the liberal equality rules
+ requires b != c; // error: ditto
+{
}
+type Syn<U> = Weird<U, U, int>
-// Just to make sure nothing went wrong.
-method m5(a: array<int>, b: array<bool>)
- requires a == b; // Bad: never equal
+method m8<T,U>(a: Weird<int,int,int>, b: Syn<int>, c: Weird<T, bool, U>, d: Syn<T>, e: Syn<bool>)
+ requires a != b; // no prob -- the types are always equal
+ requires b != d; // allowed
+ requires c != d; // allowed
+ requires b != e; // error: these can't be the same type, ever
{
+}
+datatype List<X> = Nil | Cons(X, List<X>)
+type ListSynonym<X,Y> = List<Y>
+type Wrapper<T> = T
+
+method m9<T>(a: array<List<int>>, b: array<List<bool>>,
+ c: array<ListSynonym<T,int>>, d: array<ListSynonym<bool,int>>,
+ e: array<ListSynonym<int,T>>, f: array<ListSynonym<real,Wrapper<int>>>)
+ requires a != b; // error
+ requires a != c;
+ requires b != c; // error
+ requires c != d;
+ requires a != e;
+ requires b != e;
+ requires d != e;
+ requires a != f;
+ requires b != f; // error
+{
}
diff --git a/Test/dafny0/LiberalEquality.dfy.expect b/Test/dafny0/LiberalEquality.dfy.expect index 0b2cbb74..e1d63481 100644 --- a/Test/dafny0/LiberalEquality.dfy.expect +++ b/Test/dafny0/LiberalEquality.dfy.expect @@ -1,4 +1,16 @@ -LiberalEquality.dfy(20,14): Error: arguments must have the same type (got T and U)
-LiberalEquality.dfy(39,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
-LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array<int> and array<bool>)
-3 resolution/type errors detected in LiberalEquality.dfy
+LiberalEquality.dfy(22,14): Error: arguments must have the same type (got T and U)
+LiberalEquality.dfy(23,14): Error: arguments must have the same type (got U and int)
+LiberalEquality.dfy(31,14): Error: arguments must have the same type (got array<T> and array3<T>)
+LiberalEquality.dfy(32,14): Error: arguments must have the same type (got array<int> and array3<int>)
+LiberalEquality.dfy(33,14): Error: arguments must have the same type (got array<T> and array3<int>)
+LiberalEquality.dfy(34,14): Error: arguments must have the same type (got array<int> and array3<T>)
+LiberalEquality.dfy(42,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
+LiberalEquality.dfy(52,13): Error: arguments must have the same type (got Weird<T,bool,T> and Weird<T,int,T>)
+LiberalEquality.dfy(61,14): Error: arguments must have the same type (got array<int> and array<bool>)
+LiberalEquality.dfy(73,13): Error: arguments must have the same type (got T -> int and int -> int)
+LiberalEquality.dfy(74,13): Error: arguments must have the same type (got int -> T and int -> int)
+LiberalEquality.dfy(84,13): Error: arguments must have the same type (got Syn<int> and Syn<bool>)
+LiberalEquality.dfy(95,13): Error: arguments must have the same type (got array<List<int>> and array<List<bool>>)
+LiberalEquality.dfy(97,13): Error: arguments must have the same type (got array<List<bool>> and array<ListSynonym<T,int>>)
+LiberalEquality.dfy(103,13): Error: arguments must have the same type (got array<List<bool>> and array<ListSynonym<real,Wrapper<int>>>)
+15 resolution/type errors detected in LiberalEquality.dfy
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 51e7fe29..b6ad5d6b 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -309,6 +309,7 @@ module Q_Imp { }
module Q_M {
+ import Q_Imp
method MyMethod(root: Q_Imp.Node, S: set<Node>)
requires root in S; // error: the element type of S does not agree with the type of root
{
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index 0d9d44de..5d11f9c9 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -1,5 +1,5 @@ -Modules0.dfy(332,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here
-Modules0.dfy(334,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+Modules0.dfy(333,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here
+Modules0.dfy(335,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA
@@ -18,7 +18,7 @@ Modules0.dfy(84,9): Error: expected method call, found expression Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)
-Modules0.dfy(235,13): Error: Undeclared type X in module B
+Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'
Modules0.dfy(245,13): Error: unresolved identifier: X
Modules0.dfy(246,15): Error: member DoesNotExist does not exist in class X
Modules0.dfy(285,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
@@ -28,7 +28,13 @@ Modules0.dfy(289,16): Error: type of the receiver is not fully determined at thi Modules0.dfy(289,17): Error: expected method call, found expression
Modules0.dfy(290,16): Error: type of the receiver is not fully determined at this program point
Modules0.dfy(290,17): Error: expected method call, found expression
-Modules0.dfy(312,24): Error: module Q_Imp does not exist
+Modules0.dfy(314,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
+Modules0.dfy(318,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
+Modules0.dfy(319,11): Error: Undeclared top-level type or type parameter: LongLostModule (did you forget to qualify a name?)
+Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup (did you forget to qualify a name?)
+Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
+Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
+Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
Modules0.dfy(102,6): Error: type MyClassY does not have a member M
Modules0.dfy(102,7): Error: expected method call, found expression
Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
@@ -36,4 +42,4 @@ Modules0.dfy(142,13): Error: old expressions are allowed only in specification a Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts
Modules0.dfy(144,13): Error: unresolved identifier: allocated
Modules0.dfy(147,21): Error: unresolved identifier: allocated
-36 resolution/type errors detected in Modules0.dfy
+42 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny0/Modules2.dfy.expect b/Test/dafny0/Modules2.dfy.expect index 3d37146d..ec2fce61 100644 --- a/Test/dafny0/Modules2.dfy.expect +++ b/Test/dafny0/Modules2.dfy.expect @@ -1,6 +1,6 @@ Modules2.dfy(46,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
Modules2.dfy(46,10): Error: new can be applied only to reference types (got C)
Modules2.dfy(49,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E')
-Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B
-Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B
+Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
+Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B (try qualifying the member name with the module name)
5 resolution/type errors detected in Modules2.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 89531a5c..8c6dcce2 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,7 +1,7 @@ ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
-ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
+ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
@@ -54,10 +54,10 @@ ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements ( ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
-ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
+ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
+ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
-ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
+ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
@@ -86,7 +86,7 @@ ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type paramete ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B
+ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
diff --git a/Test/hofs/Consequence.dfy b/Test/hofs/Consequence.dfy index 35934470..9c62a6ba 100644 --- a/Test/hofs/Consequence.dfy +++ b/Test/hofs/Consequence.dfy @@ -1,9 +1,10 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" +newtype Nat = x | 0 <= x + method Check() { - var f : nat -> nat; + var f : Nat -> Nat; assume f.requires(0); - var i : nat := f(0); + var i : Nat := f(0); } - diff --git a/Test/hofs/Consequence.dfy.expect b/Test/hofs/Consequence.dfy.expect index 069e7767..52595bf9 100644 --- a/Test/hofs/Consequence.dfy.expect +++ b/Test/hofs/Consequence.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 3 verified, 0 errors
|