diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 405 |
1 files changed, 263 insertions, 142 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 640fa223..2cc6010a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -471,7 +471,7 @@ namespace Microsoft.Dafny }
public static Expression FrameArrowToObjectSet(Expression e, ref int tmpCounter) {
- var arrTy = e.Type as ArrowType;
+ var arrTy = e.Type.AsArrowType;
if (arrTy != null) {
var bvars = new List<BoundVar>();
var bexprs = new List<Expression>();
@@ -797,7 +797,7 @@ namespace Microsoft.Dafny // nothing more to register
} else if (d is TypeSynonymDecl) {
// nothing more to register
- } else if (d is DerivedTypeDecl) {
+ } else if (d is NewtypeDecl) {
// nothing more to register
} else if (d is IteratorDecl) {
@@ -1089,7 +1089,7 @@ namespace Microsoft.Dafny a.OriginalSignature = abs.OriginalSignature;
return a;
} else {
- return new Cloner(false).CloneDeclaration(d, m);
+ return new ClonerButDropMethodBodies().CloneDeclaration(d, m);
}
}
@@ -1124,16 +1124,16 @@ namespace Microsoft.Dafny // nothing to do
} else if (d is TypeSynonymDecl) {
var syn = (TypeSynonymDecl)d;
- ResolveType(syn.tok, syn.Rhs, ResolveTypeOptionEnum.AllowPrefix, syn.TypeArgs);
+ ResolveType(syn.tok, syn.Rhs, syn, ResolveTypeOptionEnum.AllowPrefix, syn.TypeArgs);
syn.Rhs.ForeachTypeComponent(ty => {
var s = ty.AsRedirectingType;
if (s != null) {
typeRedirectionDependencies.AddEdge(syn, s);
}
});
- } else if (d is DerivedTypeDecl) {
- var dd = (DerivedTypeDecl)d;
- ResolveType(dd.tok, dd.BaseType, ResolveTypeOptionEnum.DontInfer, null);
+ } else if (d is NewtypeDecl) {
+ var dd = (NewtypeDecl)d;
+ ResolveType(dd.tok, dd.BaseType, dd, ResolveTypeOptionEnum.DontInfer, null);
dd.BaseType.ForeachTypeComponent(ty => {
var s = ty.AsRedirectingType;
if (s != null) {
@@ -1177,7 +1177,7 @@ namespace Microsoft.Dafny if (cycle != null) {
Contract.Assert(cycle.Count != 0);
var erste = cycle[0];
- Error(erste.Tok, "Cycle among redirecting types (derived types, type synonyms): {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);
+ Error(erste.Tok, "Cycle among redirecting types (newtypes, type synonyms): {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);
}
}
@@ -1208,25 +1208,28 @@ namespace Microsoft.Dafny } else if (d is ClassDecl) {
var cl = (ClassDecl)d;
ResolveClassMemberBodies(cl);
- } else if (d is DerivedTypeDecl) {
- var dd = (DerivedTypeDecl)d;
+ } else if (d is NewtypeDecl) {
+ var dd = (NewtypeDecl)d;
// this check can be done only after it has been determined that the redirected types do not involve cycles
if (!dd.BaseType.IsNumericBased()) {
- Error(dd.tok, "derived types must be based on some numeric type (got {0})", dd.BaseType);
+ Error(dd.tok, "newtypes must be based on some numeric type (got {0})", dd.BaseType);
}
// type check the constraint, if any
if (dd.Var != null) {
- Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.BaseType)); // follows from DerivedTypeDecl invariant
- Contract.Assert(dd.Constraint != null); // follows from DerivedTypeDecl invariant
+ Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.BaseType)); // follows from NewtypeDecl invariant
+ Contract.Assert(dd.Constraint != null); // follows from NewtypeDecl invariant
scope.PushMarker();
var added = scope.Push(dd.Var.Name, dd.Var);
Contract.Assert(added);
- ResolveType(dd.Var.tok, dd.Var.Type, ResolveTypeOptionEnum.DontInfer, null);
- ResolveExpression(dd.Constraint, new ResolveOpts(new NoContext(d.Module), false, true));
+ ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null);
+ ResolveExpression(dd.Constraint, new ResolveOpts(dd, false, true));
Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(dd.Constraint.Type, Type.Bool)) {
Error(dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type);
}
+ if (!CheckTypeInference_Visitor.IsDetermined(dd.BaseType.NormalizeExpand())) {
+ Error(dd.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name);
+ }
scope.PopMarker();
}
}
@@ -1245,6 +1248,12 @@ namespace Microsoft.Dafny } else if (d is ClassDecl) {
var cl = (ClassDecl)d;
cl.Members.Iter(CheckTypeInference_Member);
+ } else if (d is NewtypeDecl) {
+ var dd = (NewtypeDecl)d;
+ if (dd.Var != null) {
+ Contract.Assert(dd.Constraint != null);
+ CheckTypeInference(dd.Constraint);
+ }
}
}
}
@@ -1523,6 +1532,7 @@ namespace Microsoft.Dafny }
// Check that copredicates are not recursive with non-copredicate functions, and
// check that colemmas are not recursive with non-colemma methods.
+ // Also, check that newtypes sit in their own SSC.
foreach (var d in declarations) {
if (d is ClassDecl) {
foreach (var member in ((ClassDecl)d).Members) {
@@ -1547,6 +1557,12 @@ namespace Microsoft.Dafny }
}
}
+ } else if (d is NewtypeDecl) {
+ var dd = (NewtypeDecl)d;
+ if (dd.Module.CallGraph.GetSCCSize(dd) != 1) {
+ var cycle = Util.Comma(" -> ", dd.Module.CallGraph.GetSCC(dd), clbl => clbl.NameRelativeToModule);
+ Error(dd.tok, "recursive dependency involving a newtype: " + cycle);
+ }
}
}
}
@@ -1773,7 +1789,7 @@ namespace Microsoft.Dafny /// However, if tp denotes an int-based or real-based type, then tp is set to int or real,
/// respectively, here.
/// </summary>
- bool IsDetermined(Type t) {
+ public static bool IsDetermined(Type t) {
Contract.Requires(t != null);
// If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively
if (t is OperationTypeProxy) {
@@ -2587,7 +2603,10 @@ namespace Microsoft.Dafny foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
- ResolveType(member.tok, ((Field)member).Type, ResolveTypeOptionEnum.DontInfer, null);
+ // In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to
+ // involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint
+ // to obtain a non-null object.
+ ResolveType(member.tok, ((Field)member).Type, new NoContext(cl.Module), ResolveTypeOptionEnum.DontInfer, null);
} else if (member is Function) {
var f = (Function)member;
@@ -3099,9 +3118,9 @@ namespace Microsoft.Dafny if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.tok, p.Type, option, f.TypeArgs);
+ ResolveType(p.tok, p.Type, f, option, f.TypeArgs);
}
- ResolveType(f.tok, f.ResultType, option, f.TypeArgs);
+ ResolveType(f.tok, f.ResultType, f, option, f.TypeArgs);
scope.PopMarker();
}
@@ -3161,7 +3180,7 @@ namespace Microsoft.Dafny ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */));
Type t = fe.E.Type;
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
- var arrTy = t.NormalizeExpand() as ArrowType;
+ var arrTy = t.AsArrowType;
if (arrTy != null) {
t = arrTy.Result;
}
@@ -3203,14 +3222,14 @@ namespace Microsoft.Dafny if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.tok, p.Type, option, m.TypeArgs);
+ ResolveType(p.tok, p.Type, m, option, m.TypeArgs);
}
// resolve out-parameters
foreach (Formal p in m.Outs) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.tok, p.Type, option, m.TypeArgs);
+ ResolveType(p.tok, p.Type, m, option, m.TypeArgs);
}
scope.PopMarker();
}
@@ -3309,10 +3328,14 @@ namespace Microsoft.Dafny void ResolveCtorSignature(DatatypeCtor ctor, List<TypeParameter> dtTypeArguments) {
Contract.Requires(ctor != null);
+ Contract.Requires(ctor.EnclosingDatatype != null);
Contract.Requires(dtTypeArguments != null);
ResolveTypeOption option = dtTypeArguments.Count == 0 ? new ResolveTypeOption(ctor) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix);
foreach (Formal p in ctor.Formals) {
- ResolveType(p.tok, p.Type, option, dtTypeArguments);
+ // In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to
+ // involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint
+ // to obtain a non-null object.
+ ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), option, dtTypeArguments);
}
}
@@ -3328,11 +3351,11 @@ namespace Microsoft.Dafny var option = iter.TypeArgs.Count == 0 ? new ResolveTypeOption(iter) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix);
// resolve the types of the parameters
foreach (var p in iter.Ins.Concat(iter.Outs)) {
- ResolveType(p.tok, p.Type, option, iter.TypeArgs);
+ ResolveType(p.tok, p.Type, iter, option, iter.TypeArgs);
}
// resolve the types of the added fields (in case some of these types would cause the addition of default type arguments)
foreach (var p in iter.OutsHistoryFields) {
- ResolveType(p.tok, p.Type, option, iter.TypeArgs);
+ ResolveType(p.tok, p.Type, iter, option, iter.TypeArgs);
}
scope.PopMarker();
}
@@ -3614,15 +3637,21 @@ namespace Microsoft.Dafny /// <summary>
/// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters.
/// </summary>
- public void ResolveType(IToken tok, Type type, ResolveTypeOptionEnum eopt, List<TypeParameter> defaultTypeArguments) {
+ public void ResolveType(IToken tok, Type type, ICodeContext context, ResolveTypeOptionEnum eopt, List<TypeParameter> defaultTypeArguments) {
+ Contract.Requires(tok != null);
+ Contract.Requires(type != null);
+ Contract.Requires(context != null);
Contract.Requires(eopt != ResolveTypeOptionEnum.AllowPrefixExtend);
- ResolveType(tok, type, new ResolveTypeOption(eopt), defaultTypeArguments);
+ ResolveType(tok, type, context, new ResolveTypeOption(eopt), defaultTypeArguments);
}
- public void ResolveType(IToken tok, Type type, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments) {
+ public void ResolveType(IToken tok, Type type, ICodeContext context, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments) {
+ Contract.Requires(tok != null);
+ Contract.Requires(type != null);
+ Contract.Requires(context != null);
Contract.Requires(option != null);
Contract.Requires((option.Opt == ResolveTypeOptionEnum.DontInfer || option.Opt == ResolveTypeOptionEnum.InferTypeProxies) == (defaultTypeArguments == null));
- var r = ResolveTypeLenient(tok, type, option, defaultTypeArguments, false);
+ var r = ResolveTypeLenient(tok, type, context, option, defaultTypeArguments, false);
Contract.Assert(r == null);
}
@@ -3647,9 +3676,10 @@ namespace Microsoft.Dafny /// 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, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments, bool allowShortenedPath) {
+ public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ICodeContext context, ResolveTypeOption option, List<TypeParameter> defaultTypeArguments, bool allowShortenedPath) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
+ Contract.Requires(context != null);
Contract.Requires((option.Opt == ResolveTypeOptionEnum.DontInfer || option.Opt == ResolveTypeOptionEnum.InferTypeProxies) == (defaultTypeArguments == null));
if (type is BasicType) {
// nothing to resolve
@@ -3657,8 +3687,8 @@ namespace Microsoft.Dafny var mt = (MapType)type;
int typeArgumentCount = 0;
if (mt.HasTypeArg()) {
- ResolveType(tok, mt.Domain, option, defaultTypeArguments);
- ResolveType(tok, mt.Range, option, defaultTypeArguments);
+ ResolveType(tok, mt.Domain, context, option, defaultTypeArguments);
+ ResolveType(tok, mt.Range, context, option, defaultTypeArguments);
typeArgumentCount = 2;
} else if (option.Opt != ResolveTypeOptionEnum.DontInfer) {
var inferredTypeArgs = new List<Type>();
@@ -3688,7 +3718,7 @@ namespace Microsoft.Dafny } else if (type is CollectionType) {
var t = (CollectionType)type;
if (t.HasTypeArg()) {
- ResolveType(tok, t.Arg, option, defaultTypeArguments);
+ ResolveType(tok, t.Arg, context, option, defaultTypeArguments);
} else if (option.Opt != ResolveTypeOptionEnum.DontInfer) {
var inferredTypeArgs = new List<Type>();
FillInTypeArguments(tok, 1, inferredTypeArgs, defaultTypeArguments, option);
@@ -3711,20 +3741,16 @@ namespace Microsoft.Dafny } else if (type is UserDefinedType) {
var t = (UserDefinedType)type;
var isArrow = t is ArrowType;
- if (!isArrow && (t.ResolvedClass != null || t.ResolvedParam != null)) {
+ 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, option, defaultTypeArguments);
+ ResolveType(t.tok, tt, context, option, defaultTypeArguments);
if (tt.IsSubrangeType && !isArrow) {
Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
}
}
- if (isArrow) {
- return null;
- // Done already, all arrow types are resolved at construction time
- }
TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null;
if (tp != null) {
if (t.TypeArgs.Count == 0) {
@@ -3785,6 +3811,18 @@ namespace Microsoft.Dafny 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;
+ var caller = context as ICallable;
+ if (caller != null) {
+ caller.EnclosingModule.CallGraph.AddEdge(caller, dd);
+ if (caller == dd) {
+ // detect self-loops here, since they don't show up in the graph's SSC methods
+ 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 = "class/datatype";
@@ -3805,7 +3843,7 @@ namespace Microsoft.Dafny } else if (type is TypeProxy) {
TypeProxy t = (TypeProxy)type;
if (t.T != null) {
- ResolveType(tok, t.T, option, defaultTypeArguments);
+ ResolveType(tok, t.T, context, option, defaultTypeArguments);
}
} else {
@@ -4082,7 +4120,10 @@ namespace Microsoft.Dafny } else if (b is IndexableTypeProxy && ((IndexableTypeProxy)b).AllowArray) {
var ib = (IndexableTypeProxy)b;
// the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
- a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg);
+ // Note, we're calling ResolvedArrayType here, which in turn calls ResolveType on ib.Arg. However, we
+ // don't need to worry about what ICodeContext we're passing in, because ib.Arg should already have been
+ // resolved.
+ a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg, new DontUseICallable());
b.T = a.T;
return UnifyTypes(ib.Arg, ib.Range);
} else {
@@ -4202,12 +4243,12 @@ namespace Microsoft.Dafny /// Callers are expected to provide "arg" as an already resolved type. (Note, a proxy type is resolved--
/// only types that contain identifiers stand the possibility of not being resolved.)
/// </summary>
- Type ResolvedArrayType(IToken tok, int dims, Type arg) {
+ Type ResolvedArrayType(IToken tok, int dims, Type arg, ICodeContext context) {
Contract.Requires(tok != null);
Contract.Requires(1 <= dims);
Contract.Requires(arg != null);
var at = builtIns.ArrayType(tok, dims, new List<Type> { arg }, false);
- ResolveType(tok, at, ResolveTypeOptionEnum.DontInfer, null);
+ ResolveType(tok, at, context, ResolveTypeOptionEnum.DontInfer, null);
return at;
}
@@ -4338,7 +4379,7 @@ namespace Microsoft.Dafny // Resolve the types of the locals
foreach (var local in s.Locals) {
- ResolveType(local.Tok, local.OptionalType, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(local.Tok, local.OptionalType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
local.type = local.OptionalType;
if (specContextOnly) {
// a local variable in a specification-only context might as well be ghost
@@ -4420,7 +4461,7 @@ namespace Microsoft.Dafny // the LHS didn't resolve correctly; some error would already have been reported
} else {
lvalueIsGhost = var.IsGhost || codeContext.IsGhost;
- CheckIsLvalue(lhs);
+ CheckIsLvalue(lhs, codeContext);
if (!lvalueIsGhost && specContextOnly) {
Error(stmt, "Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
@@ -4460,7 +4501,7 @@ namespace Microsoft.Dafny }
}
}
- CheckIsLvalue(fse);
+ CheckIsLvalue(fse, codeContext);
}
} else if (lhs is SeqSelectExpr) {
var slhs = (SeqSelectExpr)lhs;
@@ -4470,17 +4511,17 @@ namespace Microsoft.Dafny if (specContextOnly) {
Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
- CheckIsLvalue(slhs);
+ CheckIsLvalue(slhs, codeContext);
}
} else if (lhs is MultiSelectExpr) {
if (specContextOnly) {
Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
- CheckIsLvalue(lhs);
+ CheckIsLvalue(lhs, codeContext);
} else {
- CheckIsLvalue(lhs);
+ CheckIsLvalue(lhs, codeContext);
}
s.IsGhost = lvalueIsGhost;
@@ -4649,7 +4690,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
}
ResolveExpression(s.Range, new ResolveOpts(codeContext, true));
Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
@@ -4847,7 +4888,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate parameter name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
if (ctor != null && i < ctor.Formals.Count) {
Formal formal = ctor.Formals[i];
Type st = SubstType(formal.Type, subst);
@@ -5314,7 +5355,7 @@ namespace Microsoft.Dafny }
}
// LHS must denote a mutable field.
- CheckIsLvalue(resolvedLhs);
+ CheckIsLvalue(resolvedLhs, codeContext);
}
}
@@ -5346,8 +5387,9 @@ namespace Microsoft.Dafny /// that can be assigned to. In particular, this means that lhs denotes a mutable variable, field,
/// or array element. If a violation is detected, an error is reported.
/// </summary>
- void CheckIsLvalue(Expression lhs) {
+ void CheckIsLvalue(Expression lhs, ICodeContext codeContext) {
Contract.Requires(lhs != null);
+ Contract.Requires(codeContext != null);
if (lhs is IdentifierExpr) {
var ll = (IdentifierExpr)lhs;
if (!ll.Var.IsMutable) {
@@ -5361,7 +5403,7 @@ namespace Microsoft.Dafny }
} else if (lhs is SeqSelectExpr) {
var ll = (SeqSelectExpr)lhs;
- if (!UnifyTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy()))) {
+ if (!UnifyTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), codeContext))) {
Error(ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
}
if (!ll.SelectOne) {
@@ -5678,7 +5720,7 @@ namespace Microsoft.Dafny if (rr.ArrayDimensions != null) {
// ---------- new T[EE]
Contract.Assert(rr.Arguments == null && rr.OptionalNameComponent == null && rr.InitCall == null);
- ResolveType(stmt.Tok, rr.EType, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(stmt.Tok, rr.EType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
int i = 0;
foreach (Expression dim in rr.ArrayDimensions) {
Contract.Assert(dim != null);
@@ -5688,7 +5730,7 @@ namespace Microsoft.Dafny }
i++;
}
- rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType);
+ rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType, codeContext);
} else {
var initCallTok = rr.Tok;
if (rr.OptionalNameComponent == null && rr.Arguments != null) {
@@ -5696,21 +5738,21 @@ namespace Microsoft.Dafny // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the default constructor.
// * If the all-but-last components of rr.EType denote a type, then do EType,OptionalNameComponent := allButLast(EType),last(EType)
// * Otherwise, report an error
- var ret = ResolveTypeLenient(stmt.Tok, rr.EType, new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null, true);
+ var ret = ResolveTypeLenient(stmt.Tok, rr.EType, 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;
rr.EType = ret.ReplacementType;
initCallTok = ret.LastToken;
- ResolveType(stmt.Tok, rr.EType, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(stmt.Tok, rr.EType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
} 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, ResolveTypeOptionEnum.InferTypeProxies, 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);
@@ -5773,9 +5815,14 @@ namespace Microsoft.Dafny if (ctype != null) {
var cd = (ClassDecl)ctype.ResolvedClass; // correctness of cast follows from postcondition of DenotesClass
Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count); // follows from the fact that ctype was resolved
+#if TWO_SEARCHES
MemberDecl member = cd.Members.Find(md => md.Name == memberName);
if (member == null &&
(!classMembers.ContainsKey(cd) || !classMembers[cd].TryGetValue(memberName, out member))) {
+#else
+ MemberDecl member;
+ if (!classMembers[cd].TryGetValue(memberName, out member)) {
+#endif
var kind = cd is IteratorDecl ? "iterator" : "class";
if (memberName == "_ctor") {
Error(tok, "{0} {1} does not have a default constructor", kind, ctype.Name);
@@ -5883,7 +5930,9 @@ namespace Microsoft.Dafny }
} else if (type is ArrowType) {
var t = (ArrowType)type;
- return new ArrowType(t.Args.ConvertAll(u => SubstType(u, subst)), SubstType(t.Result, subst));
+ var at = new ArrowType(t.tok, t.Args.ConvertAll(u => SubstType(u, subst)), SubstType(t.Result, subst));
+ at.ResolvedClass = t.ResolvedClass;
+ return at;
} else if (type is UserDefinedType) {
var t = (UserDefinedType)type;
if (t.ResolvedParam != null) {
@@ -6078,7 +6127,7 @@ namespace Microsoft.Dafny if (e is StaticReceiverExpr) {
StaticReceiverExpr eStatic = (StaticReceiverExpr)e;
- this.ResolveType(eStatic.tok, eStatic.UnresolvedType, ResolveTypeOptionEnum.InferTypeProxies, null);
+ this.ResolveType(eStatic.tok, eStatic.UnresolvedType, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
eStatic.Type = eStatic.UnresolvedType;
} else {
if (e.Value == null) {
@@ -6203,7 +6252,7 @@ namespace Microsoft.Dafny subst[tp] = prox;
e.TypeApplication.Add(prox);
}
- e.Type = SubstType(fn.Type, subst);
+ e.Type = new ArrowType(fn.tok, fn.Formals.ConvertAll(f => SubstType(f.Type, subst)), SubstType(fn.ResultType, subst), builtIns.SystemModule);
AddCallGraphEdge(e, opts.codeContext, fn);
} else if (member is Field) {
var field = (Field)member;
@@ -6234,7 +6283,7 @@ namespace Microsoft.Dafny ResolveExpression(e.Array, opts);
Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType))) {
+ if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType, opts.codeContext))) {
Error(e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
}
int i = 0;
@@ -6345,19 +6394,24 @@ namespace Microsoft.Dafny ResolveFunctionCallExpr(e, opts, false);
} else if (expr is ApplyExpr) {
- ApplyExpr e = (ApplyExpr)expr;
+ var e = (ApplyExpr)expr;
ResolveExpression(e.Function, opts);
foreach (var arg in e.Args) {
ResolveExpression(arg, opts);
}
- Type tb = new InferredTypeProxy();
- var targs = e.Args.ConvertAll(arg => arg.Type);
- Type tc = new ArrowType(targs, tb);
- if (!UnifyTypes(e.Function.Type, tc)) {
- Error(e.OpenParen, "cannot apply arguments with types {0} to expression with type {1}",
- Util.Comma(targs, x => x.ToString()), e.Function.Type, ", ");
+ var fnType = e.Function.Type.AsArrowType;
+ if (fnType == null) {
+ Error(e.OpenParen, "apply expression requires a function (got {0})", e.Function.Type);
+ } else if (fnType.Arity != e.Args.Count) {
+ Error(e.OpenParen, "wrong number of arguments to function application (function type '{0}' expects {1}, got {2})", fnType, fnType.Arity, e.Args.Count);
+ } else {
+ for (var i = 0; i < fnType.Arity; i++) {
+ if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
+ Error(e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
+ }
+ }
}
- expr.Type = tb;
+ expr.Type = fnType == null ? new InferredTypeProxy() : fnType.Result;
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
@@ -6419,15 +6473,15 @@ namespace Microsoft.Dafny } else if (expr is ConversionExpr) {
var e = (ConversionExpr)expr;
- ResolveType(e.tok, e.ToType, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);
+ ResolveType(e.tok, e.ToType, opts.codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);
ResolveExpression(e.E, opts);
- if (e.ToType is IntType) {
+ if (e.ToType.IsNumericBased(Type.NumericPersuation.Int)) {
if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false))) {
- Error(expr, "type conversion to int is allowed only from numeric types (got {0})", e.E.Type);
+ Error(expr, "type conversion to an int-based type is allowed only from numeric types (got {0})", e.E.Type);
}
- } else if (e.ToType is RealType) {
+ } else if (e.ToType.IsNumericBased(Type.NumericPersuation.Real)) {
if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false))) {
- Error(expr, "type conversion to real is allowed only from numeric types(got {0})", e.E.Type);
+ Error(expr, "type conversion to a real-based type is allowed only from numeric types (got {0})", e.E.Type);
}
} else {
Error(expr, "type conversions are not supported to this type (got {0})", e.ToType);
@@ -6633,7 +6687,7 @@ namespace Microsoft.Dafny var i = 0;
foreach (var lhs in e.LHSs) {
var rhsType = i < e.RHSs.Count ? e.RHSs[i].Type : new InferredTypeProxy();
- ResolveCasePattern(lhs, rhsType);
+ ResolveCasePattern(lhs, rhsType, opts.codeContext);
// Check for duplicate names now, because not until after resolving the case pattern do we know if identifiers inside it refer to bound variables or nullary constructors
var c = 0;
foreach (var v in lhs.Vars) {
@@ -6661,7 +6715,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate let-variable name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
}
foreach (var rhs in e.RHSs) {
ResolveExpression(rhs, opts);
@@ -6692,7 +6746,7 @@ namespace Microsoft.Dafny Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer);
- ResolveType(v.tok, v.Type, option, typeQuantifier ? e.TypeArgs : null);
+ ResolveType(v.tok, v.Type, opts.codeContext, option, typeQuantifier ? e.TypeArgs : null);
}
if (e.TypeArgs.Count > 0 && !typeQuantifier) {
Error(expr, "a quantifier cannot quantify over types. Possible fix: use the experimental attribute :typeQuantifier");
@@ -6747,7 +6801,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
}
ResolveExpression(e.Range, opts);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
@@ -6788,7 +6842,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
}
ResolveExpression(e.Range, opts);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
@@ -6821,7 +6875,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
}
if (e.Range != null) {
@@ -6839,7 +6893,7 @@ namespace Microsoft.Dafny ResolveExpression(e.Term, opts);
Contract.Assert(e.Term.Type != null);
scope.PopMarker();
- expr.Type = new ArrowType(Util.Map(e.BoundVars, v => v.Type), e.Body.Type);
+ expr.Type = new ArrowType(e.tok, Util.Map(e.BoundVars, v => v.Type), e.Body.Type, builtIns.SystemModule);
} else if (expr is WildcardExpr) {
expr.Type = new SetType(new ObjectType());
} else if (expr is StmtExpr) {
@@ -6929,7 +6983,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate parameter name: {0}", v.Name);
}
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
if (ctor != null && i < ctor.Formals.Count) {
Formal formal = ctor.Formals[i];
Type st = SubstType(formal.Type, subst);
@@ -6970,9 +7024,10 @@ namespace Microsoft.Dafny }
}
- void ResolveCasePattern(CasePattern pat, Type sourceType) {
+ void ResolveCasePattern(CasePattern pat, Type sourceType, ICodeContext context) {
Contract.Requires(pat != null);
Contract.Requires(sourceType != null);
+ Contract.Requires(context != null);
DatatypeDecl dtd = null;
UserDefinedType udt = null;
@@ -6993,7 +7048,7 @@ namespace Microsoft.Dafny if (pat.Var != null) {
// this is a simple resolution
var v = pat.Var;
- ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);
+ ResolveType(v.tok, v.Type, context, ResolveTypeOptionEnum.InferTypeProxies, null);
if (!UnifyTypes(v.Type, sourceType)) {
Error(v.tok, "type of corresponding source/RHS ({0}) does not match type of bound variable ({1})", sourceType, v.Type);
}
@@ -7019,7 +7074,7 @@ namespace Microsoft.Dafny if (j < ctor.Formals.Count) {
var formal = ctor.Formals[j];
Type st = SubstType(formal.Type, subst);
- ResolveCasePattern(arg, st);
+ ResolveCasePattern(arg, st, context);
}
j++;
}
@@ -7040,7 +7095,7 @@ namespace Microsoft.Dafny subst.Add(dt.TypeArgs[i], t);
}
// Construct a resolved type directly, as we know the declaration is dt.
- dtv.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, dt, gt);
+ dtv.Type = new UserDefinedType(dtv.tok, dt.Name, dt, gt);
DatatypeCtor ctor;
if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
@@ -7265,11 +7320,29 @@ namespace Microsoft.Dafny /// If you are calling a field that could be a function, creates an ApplyExpr, otherwise an ordinary FunctionCallExpr.
/// </summary>
private Expression NewFunctionCallExpr(IToken tok, string fn, Expression receiver, IToken openParen, List<Expression> args) {
- NonProxyType nptype;
- MemberDecl member = ResolveMember(tok, receiver.Type, fn, out nptype);
+ Contract.Requires(tok != null);
+ Contract.Requires(fn != null);
+ Contract.Requires(receiver != null && receiver.Type != null);
+ // We're going to look for a field of a class or a destructor of a datatype, but rather than calling
+ // ResolveMember (which would report an error if the member is not found), we do it ourselves.
+ MemberDecl member;
+ UserDefinedType ctype = UserDefinedType.DenotesClass(receiver.Type);
+ if (ctype != null) {
+ var cd = (ClassDecl)ctype.ResolvedClass; // correctness of cast follows from postcondition of DenotesClass
+ if (!classMembers[cd].TryGetValue(fn, out member)) {
+ member = null;
+ }
+ } else if (receiver.Type.IsDatatype) {
+ var dtd = receiver.Type.AsDatatype;
+ if (!datatypeMembers[dtd].TryGetValue(fn, out member)) {
+ member = null;
+ }
+ } else {
+ member = null;
+ }
var field = member as Field;
if (field != null) {
- if (field.Type is ArrowType || field.Type.IsTypeParameter) {
+ if (field.Type.IsArrowType || field.Type.IsTypeParameter) {
return new ApplyExpr(tok, openParen, new ExprDotName(tok, receiver, fn), args);
}
}
@@ -7385,11 +7458,14 @@ namespace Microsoft.Dafny /// Otherwise, resolves all sub-parts of "e" and returns a (resolved) CallRhs expression representing the call.
/// </summary>
CallRhs ResolveIdentifierSequence(IdentifierSequence e, ResolveOpts opts, bool allowMethodCall) {
+ Contract.Requires(e != null);
+ Contract.Requires(opts != null);
// Look up "id" as follows:
// - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally)
+ // - if the length of the path is 1, unambiguous constructor name of a datatype (if two constructors have the same name, an error message is
+ // produced here)
// - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or opaque type)
// (if two imported types have the same name, an error message is produced here)
- // - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)
// - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")
// - iterator
// - static function or method in the enclosing module, or its imports.
@@ -7408,26 +7484,35 @@ namespace Microsoft.Dafny ResolveExpression(r, opts);
r = ResolveSuffix(r, e, 1, opts, allowMethodCall, out call);
+ } else if (e.Tokens.Count == 1 && moduleInfo.Ctors.TryGetValue(id.val, out pair)) {
+ // ----- root is a datatype constructor
+ if (pair.Item2) {
+ // there is more than one constructor with this name
+ Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);
+ } else {
+ var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args);
+ ResolveExpression(r, opts);
+ if (e.Tokens.Count != 1) {
+ r = ResolveSuffix(r, e, 1, opts, allowMethodCall, out call);
+ }
+ }
+
} else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {
if (decl is AmbiguousTopLevelDecl) {
Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
} else if (e.Tokens.Count == 1 && e.Arguments == null) {
Error(id, "name of type ('{0}') is used as a variable", id.val);
} else if (e.Tokens.Count == 1 && e.Arguments != null) {
- // in
- // datatype Id = Id
- // you cannot refer to the constructor, instead this error message is thrown:
- // (bug?)
- Error(id, "name of type ('{0}') is used as a function", id.val);
- // resolve the arguments nonetheless
- foreach (var arg in e.Arguments) {
- ResolveExpression(arg, opts);
+ if (ResolveAsTypeConversion(e, opts, decl, id, ref r)) {
+ // everything taken care of by ResolveAsTypeConversion
+ } else {
+ Error(id, "name of type ('{0}') is used as a function", id.val);
+ // resolve the arguments nonetheless
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, opts);
+ }
}
- } else if (decl is ClassDecl) {
- // ----- root is a class
- var cd = (ClassDecl)decl;
- r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, opts, allowMethodCall, out call);
-
} else if (decl is ModuleDecl) {
// ----- root is a submodule
if (!(1 < e.Tokens.Count)) {
@@ -7435,27 +7520,25 @@ namespace Microsoft.Dafny }
call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, opts, allowMethodCall);
} else {
- // ----- root is a datatype
- var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
- var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();
- r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);
- ResolveExpression(r, opts);
- if (e.Tokens.Count != 2) {
- r = ResolveSuffix(r, e, 2, opts, allowMethodCall, out call);
- }
- }
-
- } else if (moduleInfo.Ctors.TryGetValue(id.val, out pair)) {
- // ----- root is a datatype constructor
- if (pair.Item2) {
- // there is more than one constructor with this name
- Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);
- } else {
- var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List<Expression>();
- r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args);
- ResolveExpression(r, opts);
- if (e.Tokens.Count != 1) {
- r = ResolveSuffix(r, e, 1, opts, allowMethodCall, out call);
+ // expand any synonyms
+ var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());
+ var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs).NormalizeExpand();
+ if (ty.IsRefType) {
+ // ----- root is a class
+ var cd = (ClassDecl)((UserDefinedType)ty).ResolvedClass;
+ r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, opts, allowMethodCall, out call);
+ } else if (ty.IsDatatype) {
+ // ----- root is a datatype
+ var dt = ty.AsDatatype;
+ var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();
+ var dtv = new DatatypeValue(id, id.val, e.Tokens[1].val, args);
+ ResolveDatatypeValue(opts, dtv, dt);
+ r = dtv;
+ if (e.Tokens.Count != 2) {
+ r = ResolveSuffix(r, e, 2, opts, allowMethodCall, out call);
+ }
+ } else {
+ Error(id, "name of type ('{0}') is used as a variable", id.val);
}
}
@@ -7498,6 +7581,28 @@ namespace Microsoft.Dafny return call;
}
+ bool ResolveAsTypeConversion(IdentifierSequence e, ResolveOpts opts, TopLevelDecl decl, IToken id, ref Expression r) {
+ var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());
+ var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs);
+ if (ty.AsNewtype == null) {
+ return false;
+ } else {
+ if (e.Arguments.Count != 1) {
+ Error(id, "conversion operation to {0} got wrong number of arguments (expected 1, got {1})", id.val, e.Arguments.Count);
+ }
+ var conversionArg = 1 <= e.Arguments.Count ? e.Arguments[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.Arguments.Count; i++) {
+ ResolveExpression(e.Arguments[i], opts);
+ }
+ return true;
+ }
+ }
+
CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, ResolveOpts opts, bool allowMethodCall) {
// Look up "id" as follows:
// - unambiguous type/module name (class, datatype, sub-module (including submodules of imports) or opaque type)
@@ -7517,27 +7622,43 @@ namespace Microsoft.Dafny if (sig.TopLevels.TryGetValue(id.val, out decl)) {
if (decl is AmbiguousTopLevelDecl) {
Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else if (p == e.Tokens.Count - 1 && e.Arguments != null && ResolveAsTypeConversion(e, opts, decl, id, ref r)) {
+ // everything taken care of by ResolveAsTypeConversion
} else if (decl is ModuleDecl) {
// ----- root is a submodule
if (!(p + 1 < e.Tokens.Count)) {
Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);
}
call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, opts, allowMethodCall);
- } else if (decl is TypeSynonymDecl) {
- // ----- root apparently refers to a type synonym
- Error(e.tok, "type synonym {0} cannot be used here", id.val); // todo: this is a bit of a cop-out; perhaps something better could be done
- } else if (decl is ClassDecl) {
- // ----- root is a class
- var cd = (ClassDecl)decl;
- r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, opts, allowMethodCall, out call);
} else {
- // ----- root is a datatype
- var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
- var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();
- r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);
- ResolveDatatypeValue(opts, (DatatypeValue)r, dt);
- if (e.Tokens.Count != p + 2) {
- r = ResolveSuffix(r, e, p + 2, opts, allowMethodCall, out call);
+ // expand any synonyms
+ var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());
+ var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs).NormalizeExpand();
+ if (ty.IsRefType) {
+ // ----- root is a class
+ var cd = (ClassDecl)((UserDefinedType)ty).ResolvedClass;
+ r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, opts, allowMethodCall, out call);
+ } else if (ty.IsDatatype) {
+ // ----- root is a datatype
+ var dt = ty.AsDatatype;
+ var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);
+ ResolveDatatypeValue(opts, (DatatypeValue)r, dt);
+ if (e.Tokens.Count != p + 2) {
+ r = ResolveSuffix(r, e, p + 2, opts, allowMethodCall, out call);
+ }
+ } else {
+ if (p == e.Tokens.Count - 1 && e.Arguments != null) {
+ Error(id, "name of type ('{0}') is used as a function", id.val);
+ } else {
+ Error(id, "name of type ('{0}') is used as a variable", id.val);
+ }
+ // resolve arguments, if any
+ if (e.Arguments != null) {
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, opts);
+ }
+ }
}
}
} else if (sig.Ctors.TryGetValue(id.val, out pair)) {
@@ -7639,7 +7760,7 @@ namespace Microsoft.Dafny }
} else if (e.Arguments != null) {
Contract.Assert(p == e.Tokens.Count);
- if (r.Type is ArrowType || r.Type.IsTypeParameter) {
+ if (r.Type.IsArrowType || r.Type.IsTypeParameter) {
r = new ApplyExpr(e.tok, e.OpenParen, r, e.Arguments);
ResolveExpression(r, opts);
} else {
@@ -7671,7 +7792,7 @@ namespace Microsoft.Dafny // error has already been reported by ResolveMember
return null;
} else {
- // assume it's a field and let the resolution of the FieldSelectExpr check any further problems
+ // assume it's a field and let the resolution of the MemberSelectExpr check any further problems
return new MemberSelectExpr(tok, obj, suffixName);
}
}
|