summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Binaries/DafnyRuntime.cs7
-rw-r--r--Source/Dafny/Cloner.cs14
-rw-r--r--Source/Dafny/Compiler.cs56
-rw-r--r--Source/Dafny/DafnyAst.cs84
-rw-r--r--Source/Dafny/Printer.cs3
-rw-r--r--Source/Dafny/Resolver.cs448
-rw-r--r--Source/Dafny/Rewriter.cs6
-rw-r--r--Source/Dafny/Translator.cs268
-rw-r--r--Source/DafnyExtension/DafnyRuntime.cs7
-rw-r--r--Test/dafny0/AutoReq.dfy226
-rw-r--r--Test/dafny0/AutoReq.dfy.expect4
-rw-r--r--Test/dafny0/EqualityTypes.dfy.expect2
-rw-r--r--Test/dafny0/ResolutionErrors.dfy18
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect4
-rw-r--r--Test/dafny0/Trait/TraitBasix.dfy.expect4
-rw-r--r--Test/dafny0/Trait/TraitMultiModule.dfy.expect2
-rw-r--r--Test/dafny0/Trait/TraitOverride0.dfy.expect2
-rw-r--r--Test/dafny0/Trait/TraitOverride1.dfy.expect2
-rw-r--r--Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect2
-rw-r--r--Test/dafny0/TypeSynonyms.dfy7
-rw-r--r--Test/dafny0/TypeSynonyms.dfy.expect2
-rw-r--r--Test/dafny0/TypeTests.dfy.expect4
22 files changed, 651 insertions, 521 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 6f0cab13..d6bd895a 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -656,6 +656,13 @@ namespace Dafny
num = n;
den = d;
}
+ public BigInteger ToBigInteger() {
+ if (0 <= num) {
+ return num / den;
+ } else {
+ return (num - den + 1) / den;
+ }
+ }
/// <summary>
/// Returns values such that aa/dd == a and bb/dd == b.
/// </summary>
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index b462f983..203dbef4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -136,19 +136,14 @@ namespace Microsoft.Dafny
Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?)
var f = (Field)member;
Field field = new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
- field.Inherited = member.Inherited; //we do need this information in ResolveClassMemberTypes method
return field;
} else if (member is Function) {
var f = (Function)member;
- f.Inherited = member.Inherited;
Function func = CloneFunction(f);
- func.Inherited = member.Inherited;
return func;
} else {
var m = (Method)member;
- m.Inherited = member.Inherited;
Method method = CloneMethod(m);
- method.Inherited = member.Inherited;
return method;
}
}
@@ -170,6 +165,13 @@ namespace Microsoft.Dafny
return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
} else if (t is UserDefinedType) {
var tt = (UserDefinedType)t;
+#if TEST_TYPE_SYNONYM_TRANSPARENCY
+ if (tt.Name == "type#synonym#transparency#test") {
+ // time to drop the synonym wrapper
+ var syn = (TypeSynonymDecl)tt.ResolvedClass;
+ return CloneType(syn.Rhs);
+ }
+#endif
return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(Tok));
} else if (t is InferredTypeProxy) {
return new InferredTypeProxy();
@@ -183,8 +185,6 @@ namespace Microsoft.Dafny
public Formal CloneFormal(Formal formal) {
Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
- if (f.Type is UserDefinedType && formal.Type is UserDefinedType)
- ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass;
return f;
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 220b5561..fcd6e637 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1672,8 +1672,6 @@ namespace Microsoft.Dafny {
// ...
// }
if (s.Cases.Count != 0) {
- var sourceType = (UserDefinedType)s.Source.Type;
-
SpillLetVariableDecls(s.Source, indent);
string source = "_source" + tmpVarCount;
tmpVarCount++;
@@ -1683,6 +1681,7 @@ namespace Microsoft.Dafny {
wr.WriteLine(";");
int i = 0;
+ var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();
foreach (MatchCaseStmt mc in s.Cases) {
MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);
TrStmtList(mc.Body, indent);
@@ -1956,7 +1955,7 @@ namespace Microsoft.Dafny {
if (tp.ArrayDimensions == null) {
wr.Write("new {0}()", TypeName(tp.EType));
} else {
- if (tp.EType is IntType || tp.EType.IsTypeParameter) {
+ if (tp.EType.IsIntegerType || tp.EType.IsTypeParameter) {
// Because the default constructor for BigInteger does not generate a valid BigInteger, we have
// to excplicitly initialize the elements of an integer array. This is all done in a helper routine.
wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));
@@ -2138,24 +2137,24 @@ namespace Microsoft.Dafny {
wr.Write(enclosingMethod != null && enclosingMethod.IsTailRecursive ? "_this" : "this");
} else if (expr is IdentifierExpr) {
- IdentifierExpr e = (IdentifierExpr)expr;
+ var e = (IdentifierExpr)expr;
wr.Write("@" + e.Var.CompileName);
} else if (expr is SetDisplayExpr) {
- SetDisplayExpr e = (SetDisplayExpr)expr;
- Type elType = cce.NonNull((SetType)e.Type).Arg;
+ var e = (SetDisplayExpr)expr;
+ var elType = e.Type.AsSetType.Arg;
wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));
TrExprList(e.Elements);
} else if (expr is MultiSetDisplayExpr) {
- MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
- Type elType = cce.NonNull((MultiSetType)e.Type).Arg;
+ var e = (MultiSetDisplayExpr)expr;
+ var elType = e.Type.AsMultiSetType.Arg;
wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));
TrExprList(e.Elements);
} else if (expr is SeqDisplayExpr) {
- SeqDisplayExpr e = (SeqDisplayExpr)expr;
- Type elType = cce.NonNull((SeqType)e.Type).Arg;
+ var e = (SeqDisplayExpr)expr;
+ var elType = e.Type.AsSeqType.Arg;
wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
TrExprList(e.Elements);
@@ -2210,11 +2209,12 @@ namespace Microsoft.Dafny {
}
}
} else if (expr is MultiSetFormingExpr) {
- MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
- wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(((CollectionType)e.E.Type).Arg));
- if (e.E.Type is SeqType) {
+ var e = (MultiSetFormingExpr)expr;
+ wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg));
+ var eeType = e.E.Type.NormalizeExpand();
+ if (eeType is SeqType) {
TrParenExpr(".FromSeq", e.E);
- } else if (e.E.Type is SetType) {
+ } else if (eeType is SetType) {
TrParenExpr(".FromSet", e.E);
} else {
Contract.Assert(false); throw new cce.UnreachableException();
@@ -2334,7 +2334,7 @@ namespace Microsoft.Dafny {
TrParenExpr(e.E);
break;
case UnaryOpExpr.Opcode.Cardinality:
- if (cce.NonNull(e.E.Type).IsArrayType) {
+ if (e.E.Type.IsArrayType) {
wr.Write("new BigInteger(");
TrParenExpr(e.E);
wr.Write(".Length)");
@@ -2350,11 +2350,11 @@ namespace Microsoft.Dafny {
} else if (expr is ConversionExpr) {
var e = (ConversionExpr)expr;
if (e.ToType is IntType) {
- Contract.Assert(e.E.Type is RealType);
+ Contract.Assert(e.E.Type.IsRealType);
TrParenExpr(e.E);
wr.Write(".ToBigInteger()");
} else if (e.ToType is RealType) {
- Contract.Assert(e.E.Type is IntType);
+ Contract.Assert(e.E.Type.IsIntegerType);
wr.Write("new Dafny.BigRational(");
TrExpr(e.E);
wr.Write(", BigInteger.One)");
@@ -2379,10 +2379,9 @@ namespace Microsoft.Dafny {
opString = "&&"; break;
case BinaryExpr.ResolvedOpcode.EqCommon: {
- Type t = cce.NonNull(e.E0.Type);
- if (t.IsDatatype || t.IsTypeParameter) {
+ if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) {
callString = "Equals";
- } else if (t.IsRefType) {
+ } else if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
@@ -2393,11 +2392,10 @@ namespace Microsoft.Dafny {
break;
}
case BinaryExpr.ResolvedOpcode.NeqCommon: {
- Type t = cce.NonNull(e.E0.Type);
- if (t.IsDatatype || t.IsTypeParameter) {
+ if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) {
preOpString = "!";
callString = "Equals";
- } else if (t.IsRefType) {
+ } else if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
@@ -2423,7 +2421,7 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.Mul:
opString = "*"; break;
case BinaryExpr.ResolvedOpcode.Div:
- if (expr.Type is IntType) {
+ if (expr.Type.IsIntegerType) {
wr.Write("Dafny.Helpers.EuclideanDivision(");
TrParenExpr(e.E0);
wr.Write(", ");
@@ -2434,7 +2432,7 @@ namespace Microsoft.Dafny {
}
break;
case BinaryExpr.ResolvedOpcode.Mod:
- if (expr.Type is IntType) {
+ if (expr.Type.IsIntegerType) {
wr.Write("Dafny.Helpers.EuclideanModulus(");
TrParenExpr(e.E0);
wr.Write(", ");
@@ -2589,7 +2587,7 @@ namespace Microsoft.Dafny {
wr.Write("throw new System.Exception();");
} else {
int i = 0;
- var sourceType = (UserDefinedType)e.Source.Type;
+ var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();
foreach (MatchCaseExpr mc in e.Cases) {
MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0);
wr.Write("return ");
@@ -2672,7 +2670,7 @@ namespace Microsoft.Dafny {
// return Dafny.Set<G>.FromCollection(_coll);
// })()
Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
- var typeName = TypeName(((SetType)e.Type).Arg);
+ var typeName = TypeName(e.Type.AsSetType.Arg);
wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);
wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);
var n = e.BoundVars.Count;
@@ -2741,8 +2739,8 @@ namespace Microsoft.Dafny {
// return Dafny.Map<U, V>.FromElements(_coll);
// })()
Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
- var domtypeName = TypeName(((MapType)e.Type).Domain);
- var rantypeName = TypeName(((MapType)e.Type).Range);
+ var domtypeName = TypeName(e.Type.AsMapType.Domain);
+ var rantypeName = TypeName(e.Type.AsMapType.Range);
wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);
wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);
var n = e.BoundVars.Count;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e757257c..a0912f19 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -130,7 +130,6 @@ namespace Microsoft.Dafny {
arrayTypeDecls.Add(dims, arrayClass);
SystemModule.TopLevelDecls.Add(arrayClass);
}
- udt.ResolvedClass = arrayTypeDecls[dims];
return udt;
}
@@ -331,6 +330,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// Return the type that "this" stands for, getting to the bottom of proxies and following type synonyms.
/// </summary>
+ [Pure]
public Type NormalizeExpand() {
Contract.Ensures(Contract.Result<Type>() != null);
Contract.Ensures(!(Contract.Result<Type>() is TypeProxy) || ((TypeProxy)Contract.Result<Type>()).T == null); // return a proxy only if .T == null
@@ -357,19 +357,32 @@ namespace Microsoft.Dafny {
}
}
+ /// <summary>
+ /// Returns whether or not "this" and "that" denote the same type, module proxies and type synonyms.
+ /// </summary>
[Pure]
public abstract bool Equals(Type that);
+ public bool IsBoolType { get { return NormalizeExpand() is BoolType; } }
+ public bool IsIntegerType { get { return NormalizeExpand() is IntType; } }
+ public bool IsRealType { get { return NormalizeExpand() is RealType; } }
public bool IsSubrangeType {
- get { return this is NatType; }
+ get { return NormalizeExpand() is NatType; }
}
+ public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }
+ public SetType AsSetType { get { return NormalizeExpand() as SetType; } }
+ public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } }
+ public SeqType AsSeqType { get { return NormalizeExpand() as SeqType; } }
+ public MapType AsMapType { get { return NormalizeExpand() as MapType; } }
+
public bool IsRefType {
get {
- if (this is ObjectType) {
+ var t = NormalizeExpand();
+ if (t is ObjectType) {
return true;
} else {
- UserDefinedType udt = this as UserDefinedType;
+ var udt = t as UserDefinedType;
return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl;
}
}
@@ -381,13 +394,14 @@ namespace Microsoft.Dafny {
}
public ArrayClassDecl/*?*/ AsArrayType {
get {
- UserDefinedType udt = UserDefinedType.DenotesClass(this);
+ var t = NormalizeExpand();
+ var udt = UserDefinedType.DenotesClass(t);
return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;
}
}
public TypeSynonymDecl AsTypeSynonym {
get {
- var udt = this as UserDefinedType;
+ var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()'
if (udt == null) {
return null;
} else {
@@ -402,7 +416,7 @@ namespace Microsoft.Dafny {
}
public DatatypeDecl AsDatatype {
get {
- UserDefinedType udt = this as UserDefinedType;
+ var udt = NormalizeExpand() as UserDefinedType;
if (udt == null) {
return null;
} else {
@@ -417,7 +431,7 @@ namespace Microsoft.Dafny {
}
public IndDatatypeDecl AsIndDatatype {
get {
- UserDefinedType udt = this as UserDefinedType;
+ var udt = NormalizeExpand() as UserDefinedType;
if (udt == null) {
return null;
} else {
@@ -432,7 +446,7 @@ namespace Microsoft.Dafny {
}
public CoDatatypeDecl AsCoDatatype {
get {
- UserDefinedType udt = this as UserDefinedType;
+ var udt = NormalizeExpand() as UserDefinedType;
if (udt == null) {
return null;
} else {
@@ -452,7 +466,7 @@ namespace Microsoft.Dafny {
}
public TypeParameter AsTypeParameter {
get {
- UserDefinedType ct = this as UserDefinedType;
+ var ct = NormalizeExpand() as UserDefinedType;
return ct == null ? null : ct.ResolvedParam;
}
}
@@ -466,7 +480,9 @@ namespace Microsoft.Dafny {
/// Returns true if it is known how to meaningfully compare the type's inhabitants.
/// </summary>
public bool IsOrdered {
- get { return !IsTypeParameter && !IsCoDatatype; }
+ get {
+ return !IsTypeParameter && !IsCoDatatype;
+ }
}
public void ForeachTypeComponent(Action<Type> action) {
@@ -492,7 +508,7 @@ namespace Microsoft.Dafny {
return "bool";
}
public override bool Equals(Type that) {
- return that.NormalizeExpand() is BoolType;
+ return that.IsBoolType;
}
}
@@ -762,8 +778,14 @@ namespace Microsoft.Dafny {
}
public override bool Equals(Type that) {
- var t = that.NormalizeExpand() as UserDefinedType;
- return t != null && ResolvedClass == t.ResolvedClass && ResolvedParam == t.ResolvedParam;
+ var i = NormalizeExpand();
+ if (i is UserDefinedType) {
+ var ii = (UserDefinedType)i;
+ var t = that.NormalizeExpand() as UserDefinedType;
+ return t != null && ii.ResolvedClass == t.ResolvedClass && ii.ResolvedParam == t.ResolvedParam;
+ } else {
+ return i.Equals(that);
+ }
}
/// <summary>
@@ -800,6 +822,11 @@ namespace Microsoft.Dafny {
if (BuiltIns.IsTupleTypeName(Name)) {
return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")";
} else {
+#if TEST_TYPE_SYNONYM_TRANSPARENCY
+ if (Name == "type#synonym#transparency#test" && ResolvedClass is TypeSynonymDecl) {
+ return ((TypeSynonymDecl)ResolvedClass).Rhs.TypeName(context);
+ }
+#endif
string s = "";
foreach (var t in Path) {
if (context != null && t == context.tok) {
@@ -4292,6 +4319,13 @@ namespace Microsoft.Dafny {
type = value.Normalize();
}
}
+#if TEST_TYPE_SYNONYM_TRANSPARENCY
+ public void DebugTest_ChangeType(Type ty) {
+ Contract.Requires(WasResolved()); // we're here to set it again
+ Contract.Requires(ty != null);
+ type = ty;
+ }
+#endif
public Expression(IToken tok) {
Contract.Requires(tok != null);
@@ -4309,7 +4343,7 @@ namespace Microsoft.Dafny {
public static IEnumerable<Expression> Conjuncts(Expression expr) {
Contract.Requires(expr != null);
- Contract.Requires(expr.Type is BoolType);
+ Contract.Requires(expr.Type.IsBoolType);
Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
// strip off parens
@@ -4341,7 +4375,7 @@ namespace Microsoft.Dafny {
public static Expression CreateAdd(Expression e0, Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType));
+ Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));
Contract.Ensures(Contract.Result<Expression>() != null);
var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1);
s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add; // resolve here
@@ -4355,7 +4389,7 @@ namespace Microsoft.Dafny {
public static Expression CreateSubtract(Expression e0, Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType));
+ Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));
Contract.Ensures(Contract.Result<Expression>() != null);
var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1);
s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; // resolve here
@@ -4368,7 +4402,7 @@ namespace Microsoft.Dafny {
/// </summary>
public static Expression CreateIncrement(Expression e, int n) {
Contract.Requires(e != null);
- Contract.Requires(e.Type is IntType);
+ Contract.Requires(e.Type.NormalizeExpand() is IntType);
Contract.Requires(0 <= n);
Contract.Ensures(Contract.Result<Expression>() != null);
if (n == 0) {
@@ -4383,7 +4417,7 @@ namespace Microsoft.Dafny {
/// </summary>
public static Expression CreateDecrement(Expression e, int n) {
Contract.Requires(e != null);
- Contract.Requires(e.Type is IntType);
+ Contract.Requires(e.Type.NormalizeExpand() is IntType);
Contract.Requires(0 <= n);
Contract.Ensures(Contract.Result<Expression>() != null);
if (n == 0) {
@@ -4420,7 +4454,7 @@ namespace Microsoft.Dafny {
public static Expression CreateNot(IToken tok, Expression e) {
Contract.Requires(tok != null);
- Contract.Requires(e.Type is BoolType);
+ Contract.Requires(e.Type.IsBoolType);
var un = new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Not, e);
un.Type = Type.Bool; // resolve here
return un;
@@ -4432,7 +4466,7 @@ namespace Microsoft.Dafny {
public static Expression CreateLess(Expression e0, Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- Contract.Requires(e0.Type is IntType && e1.Type is IntType);
+ Contract.Requires(e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType);
Contract.Ensures(Contract.Result<Expression>() != null);
var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1);
s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt; // resolve here
@@ -4446,7 +4480,7 @@ namespace Microsoft.Dafny {
public static Expression CreateAtMost(Expression e0, Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType));
+ Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));
Contract.Ensures(Contract.Result<Expression>() != null);
var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1);
s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le; // resolve here
@@ -4480,7 +4514,7 @@ namespace Microsoft.Dafny {
public static Expression CreateAnd(Expression a, Expression b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
- Contract.Requires(a.Type is BoolType && b.Type is BoolType);
+ Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
Contract.Ensures(Contract.Result<Expression>() != null);
if (LiteralExpr.IsTrue(a)) {
return b;
@@ -4500,7 +4534,7 @@ namespace Microsoft.Dafny {
public static Expression CreateImplies(Expression a, Expression b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
- Contract.Requires(a.Type is BoolType && b.Type is BoolType);
+ Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
Contract.Ensures(Contract.Result<Expression>() != null);
if (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b)) {
return b;
@@ -4519,7 +4553,7 @@ namespace Microsoft.Dafny {
Contract.Requires(test != null);
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- Contract.Requires(test.Type is BoolType && e0.Type.Equals(e1.Type));
+ Contract.Requires(test.Type.IsBoolType && e0.Type.Equals(e1.Type));
Contract.Ensures(Contract.Result<Expression>() != null);
var ite = new ITEExpr(test.tok, test, e0, e1);
ite.Type = e0.type; // resolve here
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6e10e7a1..a96efb8b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -265,6 +265,9 @@ namespace Microsoft.Dafny {
Contract.Requires(c != null);
Indent(indent);
PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
+ if (c.TraitId != null) {
+ wr.Write(" extends {0}", c.TraitId.val);
+ }
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
} else {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 9798e79f..d391ab4e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -136,12 +136,12 @@ namespace Microsoft.Dafny
return nm;
}
}
- //Dictionary<string/*!*/, Tuple<DatatypeCtor, bool>> allDatatypeCtors;
+ //Dictionary<string, Tuple<DatatypeCtor, bool>> allDatatypeCtors;
- readonly Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ classMembers = new Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
- readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
- readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();
- readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
+ readonly Dictionary<ClassDecl, Dictionary<string, MemberDecl>> classMembers = new Dictionary<ClassDecl, Dictionary<string, MemberDecl>>();
+ readonly Dictionary<DatatypeDecl, Dictionary<string, MemberDecl>> datatypeMembers = new Dictionary<DatatypeDecl, Dictionary<string, MemberDecl>>();
+ readonly Dictionary<DatatypeDecl, Dictionary<string, DatatypeCtor>> datatypeCtors = new Dictionary<DatatypeDecl, Dictionary<string, DatatypeCtor>>();
+ readonly Graph<ModuleDecl> dependencies = new Graph<ModuleDecl>();
private ModuleSignature systemNameInfo = null;
private bool useCompileSignatures = false;
private RefinementTransformer refinementTransformer = null;
@@ -475,16 +475,17 @@ namespace Microsoft.Dafny
} else {
Expression e = fe.E; // keep only fe.E, drop any fe.Field designation
Contract.Assert(e.Type != null); // should have been resolved already
- if (e.Type.IsRefType) {
+ var eType = e.Type.NormalizeExpand();
+ if (eType.IsRefType) {
// e represents a singleton set
if (singletons == null) {
singletons = new List<Expression>();
}
singletons.Add(e);
- } else if (e.Type is SeqType) {
+ } else if (eType is SeqType) {
// e represents a sequence
// Add: set x :: x in e
- var bv = new BoundVar(e.tok, "_s2s_" + tmpVarCount, ((SeqType)e.Type).Arg);
+ var bv = new BoundVar(e.tok, "_s2s_" + tmpVarCount, ((SeqType)eType).Arg);
tmpVarCount++;
var bvIE = new IdentifierExpr(e.tok, bv.Name);
bvIE.Var = bv; // resolve here
@@ -497,7 +498,7 @@ namespace Microsoft.Dafny
sets.Add(s);
} else {
// e is already a set
- Contract.Assert(e.Type is SetType);
+ Contract.Assert(eType is SetType);
sets.Add(e);
}
}
@@ -1456,6 +1457,14 @@ namespace Microsoft.Dafny
allTypeParameters.PopMarker();
}
+ // Now that all traits have been resolved, let classes inherit the trait members
+ foreach (var d in declarations) {
+ var cl = d as ClassDecl;
+ if (cl != null) {
+ InheritTraitMembers(cl);
+ }
+ }
+
// perform acyclicity test on type synonyms
var cycle = typeSynonymDependencies.TryFindCycle();
if (cycle != null) {
@@ -1477,7 +1486,7 @@ namespace Microsoft.Dafny
Contract.Assert(d != null);
if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0)
{
- Error(d, "a trait can not declare type parameters");
+ Error(d, "a trait cannot declare type parameters");
}
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, false, d);
@@ -2024,7 +2033,7 @@ namespace Microsoft.Dafny
Contract.Requires(tok != null);
Contract.Requires(t != null);
Contract.Requires(what != null);
- t = t.Normalize();
+ t = t.NormalizeExpand();
if (t is TypeProxy && (aggressive || !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy))) {
Error(tok, "the type of this {0} is underspecified, but it cannot be an opaque type.", what);
return false;
@@ -2762,13 +2771,33 @@ namespace Microsoft.Dafny
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
- void ResolveClassMemberTypes(ClassDecl/*!*/ cl) {
+ void ResolveClassMemberTypes(ClassDecl cl) {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
currentClass = cl;
- RefinementCloner cloner = new RefinementCloner(cl.Module);
+
+ // Resolve names of traits extended
+ if (cl.TraitId != null) {
+ var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);
+ if (trait == null) {
+ Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val);
+ } else if (!(trait is TraitDecl)) {
+ Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val);
+ } else {
+ //disallowing inheritance in multi module case
+ string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty);
+ string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty);
+ if (clModName != traitModName) {
+ Error(cl.TraitId, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",
+ cl.FullName, trait.FullName));
+ } else {
+ cl.Trait = (TraitDecl)trait;
+ }
+ }
+ }
+
foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
@@ -2813,165 +2842,126 @@ namespace Microsoft.Dafny
}
}
+ currentClass = null;
+ }
+
+ void InheritTraitMembers(ClassDecl cl) {
+ Contract.Requires(cl != null);
+
//merging class members with parent members if any
- if (cl.TraitId != null)
- {
- //resolving trait: making sure if the given qualifed name is a Trait
- var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);
- if (trait != null && trait is TraitDecl)
- {
- //disallowing inheritance in multi module case
- string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty);
- string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty);
- if (clModName != traitModName)
- {
- Error(cl, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",
- cl.FullName, trait.FullName));
+ if (cl.Trait != null) {
+ var clMembers = classMembers[cl];
+ var traitMembers = classMembers[cl.Trait];
+ //merging current class members with the inheriting trait
+ foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers) {
+ MemberDecl clMember;
+ if (clMembers.TryGetValue(traitMem.Key, out clMember)) {
+ //check if the signature of the members are equal and the member is body-less
+ if (traitMem.Value is Method) {
+ Method traitMethod = (Method)traitMem.Value;
+ // TODO: should check that the class member is also a method, and the same kind of method
+ Method classMethod = (Method)clMember;
+ //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod);
+ if (traitMethod.Body != null && !clMembers[classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent
+ Error(classMethod, "a class cannot override implemented methods");
+ else {
+ classMethod.OverriddenMethod = traitMethod;
+ //adding a call graph edge from the trait method to that of class
+ cl.Module.CallGraph.AddEdge(traitMethod, classMethod);
+
+ //checking specifications
+ //class method must provide its own specifications in case the overriden method has provided any
+ if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
+ {
+ Error(classMethod, "Method must provide its own Requires clauses anew");
+ }
+ if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
+ {
+ Error(classMethod, "Method must provide its own Ensures clauses anew");
+ }
+ if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
+ {
+ Error(classMethod, "Method must provide its own Modifies clauses anew");
+ }
+ if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
+ {
+ Error(classMethod, "Method must provide its own Decreases clauses anew");
+ }
}
- else
- {
- cl.Trait = (TraitDecl)trait;
- var traitMembers = classMembers[trait];
- //merging current class members with the inheriting trait
- foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers)
- {
- object clMember = cl.Members.FirstOrDefault(clMem => clMem.CompileName == traitMem.Key);
- if (clMember != null)
- {
- //check if the signature of the members are equal and the member is body-less
- if (traitMem.Value is Method)
- {
- Method traitMethod = (Method)traitMem.Value;
- Method classMethod = (Method)clMember;
- //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod);
- if (traitMethod.Body != null && !classMembers[cl][classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent
- Error(classMethod, "a class can not override implemented methods");
- else
- {
- classMethod.OverriddenMethod = traitMethod;
- //adding a call graph edge from the trait method to that of class
- cl.Module.CallGraph.AddEdge(traitMethod, classMethod);
-
- //checking specifications
- //class method must provide its own specifications in case the overriden method has provided any
- if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
- {
- Error(classMethod, "Method must provide its own Requires clauses anew");
- }
- if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
- {
- Error(classMethod, "Method must provide its own Ensures clauses anew");
- }
- if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
- {
- Error(classMethod, "Method must provide its own Modifies clauses anew");
- }
- if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
- {
- Error(classMethod, "Method must provide its own Decreases clauses anew");
- }
- }
- }
- else if (traitMem.Value is Function)
- {
- Function traitFunction = (Function)traitMem.Value;
- Function classFunction = (Function)clMember;
- //refinementTransformer.CheckFunctionsAreRefinements(classFunction, traitFunction);
- if (traitFunction.Body != null && !classMembers[cl][classFunction.CompileName].Inherited)
- Error(classFunction, "a class can not override implemented functions");
- else
- {
- classFunction.OverriddenFunction = traitFunction;
- //adding a call graph edge from the trait method to that of class
- cl.Module.CallGraph.AddEdge(traitFunction, classFunction);
-
- //checking specifications
- //class function must provide its own specifications in case the overriden function has provided any
- if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
- {
- Error(classFunction, "Function must provide its own Requires clauses anew");
- }
- if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
- {
- Error(classFunction, "Function must provide its own Ensures clauses anew");
- }
- if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
- {
- Error(classFunction, "Function must provide its own Reads clauses anew");
- }
- if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
- {
- Error(classFunction, "Function must provide its own Decreases clauses anew");
- }
- }
- }
- else if (traitMem.Value is Field)
- {
- Field traitField = (Field)traitMem.Value;
- Field classField = (Field)clMember;
- if (!classMembers[cl][classField.CompileName].Inherited)
- Error(classField, "member in the class has been already inherited from its parent trait");
- }
- }
- else //the member is not already in the class
- {
- MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);
- if (classNewMember is Field)
- {
- Field f = (Field)classNewMember;
- if (f.Type is UserDefinedType)
- ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass;
- }
- classNewMember.EnclosingClass = cl;
- classNewMember.Inherited = true;
- classMembers[cl].Add(traitMem.Key, classNewMember);
- cl.Members.Add(classNewMember);
- }
- }//foreach
-
- //checking to make sure all body-less methods/functions have been implemented in the child class
- if (refinementTransformer == null)
- refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);
- foreach (MemberDecl traitMember in trait.Members.Where(mem => mem is Function || mem is Method))
- {
- if (traitMember is Function)
- {
- Function traitFunc = (Function)traitMember;
- if (traitFunc.Body == null) //we do this check only if trait function body is null
+ } else if (traitMem.Value is Function) {
+ Function traitFunction = (Function)traitMem.Value;
+ Function classFunction = (Function)clMember;
+ //refinementTransformer.CheckFunctionsAreRefinements(classFunction, traitFunction);
+ if (traitFunction.Body != null && !classMembers[cl][classFunction.CompileName].Inherited)
+ Error(classFunction, "a class cannot override implemented functions");
+ else {
+ classFunction.OverriddenFunction = traitFunction;
+ //adding a call graph edge from the trait method to that of class
+ cl.Module.CallGraph.AddEdge(traitFunction, classFunction);
+
+ //checking specifications
+ //class function must provide its own specifications in case the overriden function has provided any
+ if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
+ {
+ Error(classFunction, "Function must provide its own Requires clauses anew");
+ }
+ if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
+ {
+ Error(classFunction, "Function must provide its own Ensures clauses anew");
+ }
+ if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
+ {
+ Error(classFunction, "Function must provide its own Reads clauses anew");
+ }
+ if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
+ {
+ Error(classFunction, "Function must provide its own Decreases clauses anew");
+ }
+ }
+ } else if (traitMem.Value is Field) {
+ Field traitField = (Field)traitMem.Value;
+ Field classField = (Field)clMember;
+ if (!clMembers[classField.CompileName].Inherited)
+ Error(classField, "member in the class has been already inherited from its parent trait");
+ }
+ } else {
+ //the member is not already in the class
+ // enter the trait member in the symbol table for the class
+ clMembers.Add(traitMem.Key, traitMem.Value);
+ }
+ }//foreach
+
+ //checking to make sure all body-less methods/functions have been implemented in the child class
+ if (refinementTransformer == null)
+ refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);
+ foreach (MemberDecl traitMember in cl.Trait.Members.Where(mem => mem is Function || mem is Method)) {
+ if (traitMember is Function) {
+ Function traitFunc = (Function)traitMember;
+ if (traitFunc.Body == null) //we do this check only if trait function body is null
{
- var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
- if (classMem != null)
- {
- Function classFunc = (Function)classMem;
- refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
- }
- else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)
- Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);
- }
- }
- if (traitMember is Method)
- {
- Method traitMethod = (Method)traitMember;
- if (traitMethod.Body == null) //we do this check only if trait method body is null
+ var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null) {
+ Function classFunc = (Function)classMem;
+ refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
+ } else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);
+ }
+ }
+ if (traitMember is Method) {
+ Method traitMethod = (Method)traitMember;
+ if (traitMethod.Body == null) //we do this check only if trait method body is null
{
- var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
- if (classMem != null)
- {
- Method classMethod = (Method)classMem;
- refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
- }
- if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
- Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
- }
- }
- }
+ var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null) {
+ Method classMethod = (Method)classMem;
+ refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
}
+ if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
+ }
}
- else
- Error(cl, string.Format("unresolved identifier: {0}", cl.TraitId.val));
+ }
}
-
- currentClass = null;
}
/// <summary>
@@ -3054,11 +3044,12 @@ namespace Microsoft.Dafny
}
}
- void AddDatatypeDependencyEdge(IndDatatypeDecl/*!*/ dt, Type/*!*/ tp, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
+ void AddDatatypeDependencyEdge(IndDatatypeDecl dt, Type tp, Graph<IndDatatypeDecl> dependencies) {
Contract.Requires(dt != null);
Contract.Requires(tp != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+ tp = tp.NormalizeExpand();
var dependee = tp.AsIndDatatype;
if (dependee != null && dt.Module == dependee.Module) {
dependencies.AddEdge(dt, dependee);
@@ -3151,6 +3142,7 @@ namespace Microsoft.Dafny
}
bool CheckCanBeConstructed(Type tp, List<TypeParameter> typeParametersUsed) {
+ tp = tp.NormalizeExpand();
var dependee = tp.AsIndDatatype;
if (dependee == null) {
// the type is not an inductive datatype, which means it is always possible to construct it
@@ -3383,8 +3375,9 @@ namespace Microsoft.Dafny
ResolveExpression(fe.E, false, codeContext);
Type t = fe.E.Type;
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
- if (t is CollectionType) {
- t = ((CollectionType)t).Arg;
+ var collType = t.AsCollectionType;
+ if (collType != null) {
+ t = collType.Arg;
}
if (!UnifyTypes(t, new ObjectType())) {
Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);
@@ -3926,6 +3919,10 @@ namespace Microsoft.Dafny
}
} else if (type is UserDefinedType) {
var t = (UserDefinedType)type;
+ 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);
if (tt.IsSubrangeType) {
@@ -4168,7 +4165,7 @@ namespace Microsoft.Dafny
// In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
var dtp = (DatatypeProxy)proxy;
- if (!dtp.Co && t.IsIndDatatype) {
+ if (!dtp.Co && t.NormalizeExpand().IsIndDatatype) {
// all is fine, proxy can be redirected to t
} else if (dtp.Co && t.IsCoDatatype) {
// all is fine, proxy can be redirected to t
@@ -4211,7 +4208,7 @@ namespace Microsoft.Dafny
} else if (!UnifyTypes(iProxy.Arg, iProxy.Range)) {
return false;
}
- } else if (iProxy.AllowArray && t.IsArrayType && (t.AsArrayType).Dims == 1) {
+ } else if (iProxy.AllowArray && t.IsArrayType && t.AsArrayType.Dims == 1) {
Type elType = UserDefinedType.ArrayElementType(t);
if (!UnifyTypes(iProxy.Domain, Type.Int)) {
return false;
@@ -4278,7 +4275,7 @@ 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 = builtIns.ArrayType(1, ib.Arg);
+ a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg);
b.T = a.T;
return UnifyTypes(ib.Arg, ib.Range);
} else {
@@ -4360,6 +4357,20 @@ namespace Microsoft.Dafny
}
/// <summary>
+ /// Returns a resolved type denoting an array type with dimension "dims" and element type "arg".
+ /// 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) {
+ 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);
+ return at;
+ }
+
+ /// <summary>
/// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
/// at run time. That means it must not have any side effects on non-ghost variables, for example.
/// </summary>
@@ -4546,7 +4557,7 @@ namespace Microsoft.Dafny
{
Error(local.Tok, "assumption variable must be ghost");
}
- if (!(local.Type is BoolType))
+ if (!(local.Type.IsBoolType))
{
Error(s, "assumption variable must be of type 'bool'");
}
@@ -4940,7 +4951,7 @@ namespace Microsoft.Dafny
}
UserDefinedType sourceType = null;
DatatypeDecl dtd = null;
- if (s.Source.Type.NormalizeExpand().IsDatatype) {
+ if (s.Source.Type.IsDatatype) {
sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();
dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
}
@@ -5054,7 +5065,7 @@ namespace Microsoft.Dafny
guess = Expression.CreateSubtract(bin.E0, bin.E1);
break;
case BinaryExpr.ResolvedOpcode.NeqCommon:
- if (bin.E0.Type is IntType || bin.E0.Type is RealType) {
+ if (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType) {
// for A != B where A and B are integers, use the absolute difference between A and B (that is: if A <= B then B-A else A-B)
var AminusB = Expression.CreateSubtract(bin.E0, bin.E1);
var BminusA = Expression.CreateSubtract(bin.E1, bin.E0);
@@ -5497,7 +5508,7 @@ namespace Microsoft.Dafny
}
} else if (lhs is SeqSelectExpr) {
var ll = (SeqSelectExpr)lhs;
- if (!UnifyTypes(ll.Seq.Type, builtIns.ArrayType(1, new InferredTypeProxy()))) {
+ if (!UnifyTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy()))) {
Error(ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
}
if (!ll.SelectOne) {
@@ -5800,8 +5811,6 @@ namespace Microsoft.Dafny
}
}
-
-
Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {
Contract.Requires(rr != null);
Contract.Requires(stmt != null);
@@ -5818,9 +5827,6 @@ namespace Microsoft.Dafny
Contract.Assert(rr.Arguments == null && rr.OptionalNameComponent == null && rr.InitCall == null);
ResolveType(stmt.Tok, rr.EType, ResolveTypeOptionEnum.InferTypeProxies, null);
int i = 0;
- if (rr.EType.IsSubrangeType) {
- Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type");
- }
foreach (Expression dim in rr.ArrayDimensions) {
Contract.Assert(dim != null);
ResolveExpression(dim, true, codeContext);
@@ -5829,7 +5835,7 @@ namespace Microsoft.Dafny
}
i++;
}
- rr.Type = builtIns.ArrayType(rr.ArrayDimensions.Count, rr.EType);
+ rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType);
} else {
var initCallTok = rr.Tok;
if (rr.OptionalNameComponent == null && rr.Arguments != null) {
@@ -5869,17 +5875,13 @@ namespace Microsoft.Dafny
// ---------- new C
Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null);
}
- if (rr.EType is UserDefinedType)
- {
- if (((UserDefinedType)rr.EType).ResolvedClass is TraitDecl)
- {
- Error(stmt, "new can not be applied to a trait");
- }
- }
- if (!callsConstructor && rr.EType is UserDefinedType) {
- var udt = (UserDefinedType)rr.EType;
+ if (rr.EType.NormalizeExpand() is UserDefinedType) {
+ var udt = (UserDefinedType)rr.EType.NormalizeExpand();
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.HasConstructor) {
+ if (cl is TraitDecl) {
+ Error(stmt, "new cannot be applied to a trait");
+ }
+ if (!callsConstructor && cl.HasConstructor) {
Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name);
}
}
@@ -6009,6 +6011,20 @@ namespace Microsoft.Dafny
}
} else if (t.ResolvedClass != null) {
List<Type> newArgs = null; // allocate it lazily
+ var resolvedClass = t.ResolvedClass;
+#if TEST_TYPE_SYNONYM_TRANSPARENCY
+ if (resolvedClass is TypeSynonymDecl && resolvedClass.Name == "type#synonym#transparency#test") {
+ // Usually, all type parameters mentioned in the definition of a type synonym are also type parameters
+ // to the type synonym itself, but in this instrumented testing, that is not so, so we also do a substitution
+ // in the .Rhs of the synonym.
+ var syn = (TypeSynonymDecl)resolvedClass;
+ var r = SubstType(syn.Rhs, subst);
+ if (r != syn.Rhs) {
+ resolvedClass = new TypeSynonymDecl(syn.tok, syn.Name, syn.TypeArgs, syn.Module, r, null);
+ newArgs = new List<Type>();
+ }
+ }
+#endif
for (int i = 0; i < t.TypeArgs.Count; i++) {
Type p = t.TypeArgs[i];
Type s = SubstType(p, subst);
@@ -6027,7 +6043,7 @@ namespace Microsoft.Dafny
// there were no substitutions
return type;
} else {
- return new UserDefinedType(t.tok, t.Name, t.ResolvedClass, newArgs, t.Path);
+ return new UserDefinedType(t.tok, t.Name, resolvedClass, newArgs, t.Path);
}
} else {
// there's neither a resolved param nor a resolved class, which means the UserDefinedType wasn't
@@ -6073,6 +6089,17 @@ namespace Microsoft.Dafny
/// "twoState" implies that "old" and "fresh" expressions are allowed.
/// </summary>
public void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext) {
+#if TEST_TYPE_SYNONYM_TRANSPARENCY
+ ResolveExpressionX(expr, twoState, codeContext);
+ // For testing purposes, change the type of "expr" to a type synonym (mwo-ha-ha-ha!)
+ var t = expr.Type;
+ Contract.Assert(t != null);
+ var sd = new TypeSynonymDecl(expr.tok, "type#synonym#transparency#test", new List<TypeParameter>(), codeContext.EnclosingModule, t, null);
+ var ts = new UserDefinedType(expr.tok, "type#synonym#transparency#test", sd, new List<Type>(), null);
+ expr.DebugTest_ChangeType(ts);
+ }
+ public void ResolveExpressionX(Expression expr, bool twoState, ICodeContext codeContext) {
+#endif
Contract.Requires(expr != null);
Contract.Requires(codeContext != null);
Contract.Ensures(expr.Type != null);
@@ -6114,7 +6141,7 @@ namespace Microsoft.Dafny
e.ResolvedExpression = e.E;
} else {
Expression zero;
- if (e.E.Type is RealType) {
+ if (e.E.Type.IsRealType) {
// we know for sure that this is a real-unary-minus
zero = new LiteralExpr(e.tok, Basetypes.BigDec.ZERO);
} else {
@@ -6265,7 +6292,7 @@ namespace Microsoft.Dafny
ResolveExpression(e.Array, twoState, codeContext);
Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(e.Array.Type, builtIns.ArrayType(e.Indices.Count, elementType))) {
+ if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType))) {
Error(e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
}
int i = 0;
@@ -6320,8 +6347,8 @@ namespace Microsoft.Dafny
}
expr.Type = e.Seq.Type;
- } else if (e.Seq.Type is UserDefinedType && ((UserDefinedType)e.Seq.Type).IsDatatype) {
- DatatypeDecl dt = ((UserDefinedType)e.Seq.Type).AsDatatype;
+ } else if (e.Seq.Type.IsDatatype) {
+ var dt = e.Seq.Type.AsDatatype;
if (!(e.Index is IdentifierSequence || (e.Index is LiteralExpr && ((LiteralExpr)e.Index).Value is BigInteger))) {
Error(expr, "datatype updates must be to datatype destructors");
@@ -6389,7 +6416,7 @@ namespace Microsoft.Dafny
if (!UnifyTypes(e.E.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
Error(e.tok, "can only form a multiset from a seq or set.");
}
- expr.Type = new MultiSetType(((CollectionType)e.E.Type).Arg);
+ expr.Type = new MultiSetType(e.E.Type.AsCollectionType.Arg);
} else if (expr is UnaryOpExpr) {
var e = (UnaryOpExpr)expr;
@@ -6413,10 +6440,10 @@ namespace Microsoft.Dafny
Error(expr, "fresh expressions are not allowed in this context");
}
// the type of e.E must be either an object or a collection of objects
- Type t = e.E.Type;
+ Type t = e.E.Type.NormalizeExpand();
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
if (t is CollectionType) {
- t = ((CollectionType)t).Arg;
+ t = ((CollectionType)t).Arg.NormalizeExpand();
}
if (t is ObjectType) {
// fine
@@ -6438,11 +6465,11 @@ namespace Microsoft.Dafny
ResolveType(e.tok, e.ToType, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);
ResolveExpression(e.E, twoState, codeContext);
if (e.ToType is IntType) {
- if (!(e.E.Type is RealType)) {
+ if (!(e.E.Type.IsRealType)) {
Error(expr, "type conversion to int is allowed only from real (got {0})", e.E.Type);
}
} else if (e.ToType is RealType) {
- if (!(e.E.Type is IntType)) {
+ if (!(e.E.Type.IsIntegerType)) {
Error(expr, "type conversion to real is allowed only from int (got {0})", e.E.Type);
}
} else {
@@ -6508,14 +6535,14 @@ namespace Microsoft.Dafny
case BinaryExpr.Opcode.Lt:
case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add: {
- if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
+ if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.NormalizeExpand().IsIndDatatype) {
if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
} else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
- } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {
+ } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.NormalizeExpand().IsIndDatatype) {
if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
} else {
@@ -6545,14 +6572,14 @@ namespace Microsoft.Dafny
case BinaryExpr.Opcode.Mul:
case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge: {
- if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
+ if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.NormalizeExpand().IsIndDatatype) {
if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
} else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
- } else if (e.Op == BinaryExpr.Opcode.Gt && e.E1.Type.IsIndDatatype) {
+ } else if (e.Op == BinaryExpr.Opcode.Gt && e.E1.Type.NormalizeExpand().IsIndDatatype) {
if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
} else {
@@ -6870,7 +6897,7 @@ namespace Microsoft.Dafny
Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression
UserDefinedType sourceType = null;
DatatypeDecl dtd = null;
- if (me.Source.Type.NormalizeExpand().IsDatatype) {
+ if (me.Source.Type.IsDatatype) {
sourceType = (UserDefinedType)me.Source.Type.NormalizeExpand();
dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
}
@@ -6965,7 +6992,7 @@ namespace Microsoft.Dafny
DatatypeDecl dtd = null;
UserDefinedType udt = null;
if (sourceType.IsDatatype) {
- udt = (UserDefinedType)sourceType;
+ udt = (UserDefinedType)sourceType.NormalizeExpand();
dtd = (DatatypeDecl)udt.ResolvedClass;
}
// Find the constructor in the given datatype
@@ -7056,6 +7083,8 @@ 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);
@@ -7680,12 +7709,12 @@ namespace Microsoft.Dafny
for (int j = 0; j < bvars.Count; j++) {
var bv = bvars[j];
var bounds = new List<ComprehensionExpr.BoundedPool>();
- if (bv.Type is BoolType) {
+ if (bv.Type.IsBoolType) {
// easy
bounds.Add(new ComprehensionExpr.BoolBoundedPool());
} else {
bool foundBoundsForBv = false;
- if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {
+ if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {
bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
foundBoundsForBv = true;
}
@@ -8169,6 +8198,7 @@ namespace Microsoft.Dafny
/// </summary>
public static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type operandType) {
Contract.Requires(operandType != null);
+ operandType = operandType.NormalizeExpand();
switch (op) {
case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff;
case BinaryExpr.Opcode.Imp: return BinaryExpr.ResolvedOpcode.Imp;
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index ca3c105d..63bb2dcc 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -174,7 +174,7 @@ namespace Microsoft.Dafny
}
} else if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var fn = (Function)member;
- if (fn.Formals.Count == 0 && fn.ResultType is BoolType) {
+ if (fn.Formals.Count == 0 && fn.ResultType.IsBoolType) {
Valid = fn;
}
}
@@ -201,7 +201,7 @@ namespace Microsoft.Dafny
Boogie.IToken tok = new AutoGeneratedToken(member.tok);
if (member is Function && member.Name == "Valid" && !member.IsStatic) {
var valid = (Function)member;
- if (valid.IsGhost && valid.ResultType is BoolType) {
+ if (valid.IsGhost && valid.ResultType.IsBoolType) {
Expression c;
if (valid.RefinementBase == null) {
var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr); // this in Repr
@@ -265,7 +265,7 @@ namespace Microsoft.Dafny
var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());
valid.Function = Valid;
valid.Type = Type.Bool;
- // Add the identity substitution to this call
+ // Add the identity substitution to this call
valid.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
foreach (var p in cl.TypeArgs) {
valid.TypeArgumentSubstitutions.Add(p, new UserDefinedType(p));
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 585ebf85..a703df3b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -598,17 +598,18 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Constructor injectivity"));
if (dt is IndDatatypeDecl) {
- if (arg.Type.IsDatatype || arg.Type.IsTypeParameter) {
+ var argType = arg.Type.NormalizeExpand();
+ if (argType.IsDatatype || argType.IsTypeParameter) {
// for datatype: axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params)));
// for type-parameter type: axiom (forall params :: DtRank(Unbox(params_i)) < DtRank(#dt.ctor(params)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,
- arg.Type.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i]));
+ argType.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i]));
Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Inductive rank"));
- } else if (arg.Type is SeqType) {
+ } else if (argType is SeqType) {
// axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(arg[i]) < DtRank(#dt.ctor(params)));
// that is:
// axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(Unbox(Seq#Index(arg,i))) < DtRank(#dt.ctor(params)));
@@ -633,7 +634,7 @@ namespace Microsoft.Dafny {
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Inductive seq rank"));
- } else if (arg.Type is SetType) {
+ } else if (argType is SetType) {
// axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
// that is:
// axiom (forall params, d: Datatype :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
@@ -647,7 +648,7 @@ namespace Microsoft.Dafny {
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Inductive set rank"));
- } else if (arg.Type is MultiSetType) {
+ } else if (argType is MultiSetType) {
// axiom (forall params, d: Datatype :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
// that is:
// axiom (forall params, d: Datatype :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
@@ -946,6 +947,12 @@ namespace Microsoft.Dafny {
// Makes a call to equality, if k is null, or otherwise prefix equality. For codatatypes.
Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List<Bpl.Expr> largs, List<Bpl.Expr> rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) {
+ Contract.Requires(codecl != null);
+ Contract.Requires(largs != null);
+ Contract.Requires(rargs != null);
+ Contract.Requires(l != null);
+ Contract.Requires(A != null);
+ Contract.Requires(B != null);
if (tok == null) {
tok = A.tok;
}
@@ -960,6 +967,12 @@ namespace Microsoft.Dafny {
// Same as above, but with Dafny-typed type-argument lists
Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List<Type> largs, List<Type> rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) {
+ Contract.Requires(codecl != null);
+ Contract.Requires(largs != null);
+ Contract.Requires(rargs != null);
+ Contract.Requires(l != null);
+ Contract.Requires(A != null);
+ Contract.Requires(B != null);
return CoEqualCall(codecl, Map(largs, TypeToTy), Map(rargs, TypeToTy), k, l, A, B, tok);
}
@@ -2493,7 +2506,7 @@ namespace Microsoft.Dafny {
var decrCaller = new List<Expr>();
foreach (var ee in m.Decreases.Expressions) {
decrToks.Add(ee.tok);
- decrTypes.Add(ee.Type);
+ decrTypes.Add(ee.Type.NormalizeExpand());
decrCaller.Add(exprTran.TrExpr(ee));
Expression es = Substitute(ee, receiverReplacement, substMap);
es = Substitute(es, null, decrSubstMap);
@@ -3543,8 +3556,8 @@ namespace Microsoft.Dafny {
#endif
}
- Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List<FrameExpression/*!*/>/*!*/ rw, ExpressionTranslator/*!*/ etran,
- Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap) {
+ Bpl.Expr/*!*/ InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List<FrameExpression> rw, ExpressionTranslator etran,
+ Expression receiverReplacement, Dictionary<IVariable,Expression> substMap) {
Contract.Requires(tok != null);
Contract.Requires(o != null);
Contract.Requires(f != null);
@@ -3566,12 +3579,13 @@ namespace Microsoft.Dafny {
e = Substitute(e, receiverReplacement, substMap);
}
Bpl.Expr disjunct;
+ var eType = e.Type.NormalizeExpand();
if (e is WildcardExpr) {
disjunct = Bpl.Expr.True;
- } else if (e.Type is SetType) {
+ } else if (eType is SetType) {
// old(e)[Box(o)]
- disjunct = etran.TrInSet(tok, o, e, ((SetType)e.Type).Arg);
- } else if (e.Type is SeqType) {
+ disjunct = etran.TrInSet(tok, o, e, ((SetType)eType).Arg);
+ } else if (eType is SeqType) {
// (exists i: int :: 0 <= i && i < Seq#Length(old(e)) && Seq#Index(old(e),i) == Box(o))
Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o);
Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
@@ -3827,7 +3841,6 @@ namespace Microsoft.Dafny {
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- //bool isSequence = e.Seq.Type is SeqType;
Bpl.Expr total = CanCallAssumption(e.Seq, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
@@ -4163,20 +4176,21 @@ namespace Microsoft.Dafny {
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- bool isSequence = e.Seq.Type is SeqType;
+ var eSeqType = e.Seq.Type.NormalizeExpand();
+ bool isSequence = eSeqType is SeqType;
CheckWellformed(e.Seq, options, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
- if (e.Seq.Type.IsArrayType) {
+ if (eSeqType.IsArrayType) {
builder.Add(Assert(e.Seq.tok, Bpl.Expr.Neq(seq, predef.Null), "array may be null"));
}
Bpl.Expr e0 = null;
- if (e.Seq.Type is MapType) {
+ if (eSeqType is MapType) {
e0 = etran.TrExpr(e.E0);
CheckWellformed(e.E0, options, locals, builder, etran);
Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq);
inDomain = Bpl.Expr.Select(inDomain, BoxIfNecessary(e.tok, e0, e.E0.Type));
builder.Add(Assert(expr.tok, inDomain, "element may not be in domain", options.AssertKv));
- } else if (e.Seq.Type is MultiSetType) {
+ } else if (eSeqType is MultiSetType) {
// cool
} else {
@@ -4190,14 +4204,14 @@ namespace Microsoft.Dafny {
builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "upper bound " + (e.E0 == null ? "" : "below lower bound or ") + "above length of " + (isSequence ? "sequence" : "array"), options.AssertKv));
}
}
- if (options.DoReadsChecks && e.Seq.Type.IsArrayType) {
+ if (options.DoReadsChecks && eSeqType.IsArrayType) {
if (e.SelectOne) {
Contract.Assert(e.E0 != null);
Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));
builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv));
} else {
Bpl.Expr lowerBound = e.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(e.E0);
- Contract.Assert((e.Seq.Type).AsArrayType.Dims == 1);
+ Contract.Assert(eSeqType.AsArrayType.Dims == 1);
Bpl.Expr upperBound = e.E1 == null ? ArrayLength(e.tok, seq, 1, 0) : etran.TrExpr(e.E1);
// check that, for all i in lowerBound..upperBound, a[i] is in the frame
Bpl.BoundVariable iVar = new Bpl.BoundVariable(e.tok, new Bpl.TypedIdent(e.tok, "$i", Bpl.Type.Int));
@@ -4237,20 +4251,14 @@ namespace Microsoft.Dafny {
Bpl.Expr index = etran.TrExpr(e.Index);
Bpl.Expr value = etran.TrExpr(e.Value);
CheckWellformed(e.Index, options, locals, builder, etran);
- if (e.Seq.Type is SeqType)
- {
+ var eSeqType = e.Seq.Type.NormalizeExpand();
+ if (eSeqType is SeqType) {
builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv));
- }
- else if (e.Seq.Type is MapType)
- {
+ } else if (eSeqType is MapType) {
// updates to maps are always valid if the values are well formed
- }
- else if (e.Seq.Type is MultiSetType)
- {
+ } else if (eSeqType is MultiSetType) {
builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), value), "new number of occurrences might be negative", options.AssertKv));
- }
- else
- {
+ } else {
Contract.Assert(false);
}
CheckWellformed(e.Value, options, locals, builder, etran);
@@ -4426,7 +4434,7 @@ namespace Microsoft.Dafny {
break;
case BinaryExpr.ResolvedOpcode.Div:
case BinaryExpr.ResolvedOpcode.Mod: {
- Bpl.Expr zero = (e.E1.Type is RealType) ? Bpl.Expr.Literal(Basetypes.BigDec.ZERO) : Bpl.Expr.Literal(0);
+ Bpl.Expr zero = (e.E1.Type.IsRealType) ? Bpl.Expr.Literal(Basetypes.BigDec.ZERO) : Bpl.Expr.Literal(0);
CheckWellformed(e.E1, options, locals, builder, etran);
builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), zero), "possible division by zero", options.AssertKv));
}
@@ -6320,7 +6328,8 @@ namespace Microsoft.Dafny {
IEnumerable<Expression> GuessWitnesses(BoundVar x, Expression expr) {
Contract.Requires(x != null);
Contract.Requires(expr != null);
- if (x.Type is BoolType) {
+ var xType = x.Type.NormalizeExpand();
+ if (xType is BoolType) {
var lit = new LiteralExpr(x.tok, false);
lit.Type = Type.Bool; // resolve here
yield return lit;
@@ -6328,13 +6337,13 @@ namespace Microsoft.Dafny {
lit.Type = Type.Bool; // resolve here
yield return lit;
yield break; // there are no more possible witnesses for booleans
- } else if (x.Type.IsRefType) {
+ } else if (xType.IsRefType) {
var lit = new LiteralExpr(x.tok); // null
- lit.Type = x.Type;
+ lit.Type = xType;
yield return lit;
- } else if (x.Type.IsDatatype) {
- var dt = x.Type.AsDatatype;
- Expression zero = Zero(x.tok, x.Type);
+ } else if (xType.IsDatatype) {
+ var dt = xType.AsDatatype;
+ Expression zero = Zero(x.tok, xType);
if (zero != null) {
yield return zero;
}
@@ -6342,28 +6351,28 @@ namespace Microsoft.Dafny {
if (ctor.Formals.Count == 0) {
var v = new DatatypeValue(x.tok, dt.Name, ctor.Name, new List<Expression>());
v.Ctor = ctor; // resolve here
- v.InferredTypeArgs = x.Type.TypeArgs; // resolved here.
+ v.InferredTypeArgs = xType.TypeArgs; // resolved here.
v.Type = new UserDefinedType(x.tok, dt.Name, dt, new List<Type>()); // resolve here
yield return v;
}
}
- } else if (x.Type is SetType) {
+ } else if (xType is SetType) {
var empty = new SetDisplayExpr(x.tok, new List<Expression>());
- empty.Type = x.Type;
+ empty.Type = xType;
yield return empty;
- } else if (x.Type is MultiSetType) {
+ } else if (xType is MultiSetType) {
var empty = new MultiSetDisplayExpr(x.tok, new List<Expression>());
- empty.Type = x.Type;
+ empty.Type = xType;
yield return empty;
- } else if (x.Type is SeqType) {
+ } else if (xType is SeqType) {
var empty = new SeqDisplayExpr(x.tok, new List<Expression>());
- empty.Type = x.Type;
+ empty.Type = xType;
yield return empty;
- } else if (x.Type is IntType) {
+ } else if (xType is IntType) {
var lit = new LiteralExpr(x.tok, 0);
lit.Type = Type.Int; // resolve here
yield return lit;
- } else if (x.Type is RealType) {
+ } else if (xType is RealType) {
var lit = new LiteralExpr(x.tok, Basetypes.BigDec.ZERO);
lit.Type = Type.Real; // resolve here
yield return lit;
@@ -7175,12 +7184,12 @@ namespace Microsoft.Dafny {
// include a free invariant that says that all completed iterations so far have only decreased the termination metric
if (initDecr != null) {
- List<IToken> toks = new List<IToken>();
- List<Type> types = new List<Type>();
- List<Expr> decrs = new List<Expr>();
+ var toks = new List<IToken>();
+ var types = new List<Type>();
+ var decrs = new List<Expr>();
foreach (Expression e in theDecreases) {
toks.Add(e.tok);
- types.Add(cce.NonNull(e.Type));
+ types.Add(e.Type.NormalizeExpand());
decrs.Add(etran.TrExpr(e));
}
Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, initDecr, null, null, true, false);
@@ -7211,12 +7220,12 @@ namespace Microsoft.Dafny {
// time for the actual loop body
bodyTr(loopBodyBuilder, updatedFrameEtran);
// check definedness of decreases expressions
- List<IToken> toks = new List<IToken>();
- List<Type> types = new List<Type>();
- List<Expr> decrs = new List<Expr>();
+ var toks = new List<IToken>();
+ var types = new List<Type>();
+ var decrs = new List<Expr>();
foreach (Expression e in theDecreases) {
toks.Add(e.tok);
- types.Add(cce.NonNull(e.Type));
+ types.Add(e.Type.NormalizeExpand());
decrs.Add(etran.TrExpr(e));
}
Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false);
@@ -7629,8 +7638,8 @@ namespace Microsoft.Dafny {
break;
}
toks.Add(tok);
- types0.Add(e0.Type);
- types1.Add(e1.Type);
+ types0.Add(e0.Type.NormalizeExpand());
+ types1.Add(e1.Type.NormalizeExpand());
callee.Add(etranCurrent.TrExpr(e0));
caller.Add(etranInitial.TrExpr(e1));
}
@@ -7651,6 +7660,7 @@ namespace Microsoft.Dafny {
/// or has gone down or stayed the same (if allowNoChange).
/// ee0 represents the new values and ee1 represents old values.
/// If builder is non-null, then the check '0 ATMOST decr' is generated to builder.
+ /// Requires all types in types0 and types1 to be non-proxy non-synonym types (that is, callers should invoke NormalizeExpand)
/// </summary>
Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1, List<Bpl.Expr> ee0, List<Bpl.Expr> ee1,
Bpl.StmtListBuilder builder, string suffixMsg, bool allowNoChange, bool includeLowerBound)
@@ -7752,6 +7762,9 @@ namespace Microsoft.Dafny {
else return null;
}
+ /// <summary>
+ /// Requires ty0 and ty1 to be non-proxy non-synonym types (that is, caller is expected have have invoked NormalizeExpand)
+ /// </summary>
void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out Bpl.Expr less, out Bpl.Expr atmost, out Bpl.Expr eq, bool includeLowerBound)
{
Contract.Requires(tok != null);
@@ -7764,8 +7777,6 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.ValueAtReturn(out atmost)!=null);
Contract.Ensures(Contract.ValueAtReturn(out eq)!=null);
- ty0 = ty0.NormalizeExpand();
- ty1 = ty1.NormalizeExpand();
var rk0 = RankFunction(ty0);
var rk1 = RankFunction(ty1);
if (rk0 != null && rk1 != null && rk0 != rk1) {
@@ -8037,7 +8048,7 @@ namespace Microsoft.Dafny {
Contract.Requires(type != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
- if (type.NormalizeExpand() is BoolType) {
+ if (type.IsBoolType) {
return FunctionCall(box.tok, BuiltinFunction.IsCanonicalBoolBox, null, box);
} else {
return Bpl.Expr.True;
@@ -8466,7 +8477,8 @@ namespace Microsoft.Dafny {
Contract.Requires(builder != null);
var cre = CheckSubrange_Expr(tok, bRhs, tp);
- var msg = (tp is NatType) ? "value assigned to a nat must be non-negative" :
+ var msg = (tp.NormalizeExpand() is NatType) ?
+ "value assigned to a nat must be non-negative" :
"value does not satisfy the subrange criteria";
builder.Add(Assert(tok, cre, msg));
}
@@ -8478,7 +8490,7 @@ namespace Microsoft.Dafny {
// Only need to check this for natural numbers for now.
// We should always be able to use Is, but this is an optimisation.
- if (tp is NatType) {
+ if (tp.NormalizeExpand() is NatType) {
return MkIs(bRhs, tp);
} else {
return Bpl.Expr.True;
@@ -9192,20 +9204,21 @@ namespace Microsoft.Dafny {
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
+ var seqType = e.Seq.Type.NormalizeExpand();
Type elmtType = null;
Type domainType = null;
- Contract.Assert(e.Seq.Type != null); // the expression has been successfully resolved
- if (e.Seq.Type.IsArrayType) {
+ Contract.Assert(seqType != null); // the expression has been successfully resolved
+ if (seqType.IsArrayType) {
domainType = Type.Int;
- elmtType = UserDefinedType.ArrayElementType(e.Seq.Type);
- } else if (e.Seq.Type is SeqType) {
+ elmtType = UserDefinedType.ArrayElementType(seqType);
+ } else if (seqType is SeqType) {
domainType = Type.Int;
- elmtType = ((SeqType)e.Seq.Type).Arg;
- } else if (e.Seq.Type is MapType) {
- domainType = ((MapType)e.Seq.Type).Domain;
- elmtType = ((MapType)e.Seq.Type).Range;
- } else if (e.Seq.Type is MultiSetType) {
- domainType = ((MultiSetType)e.Seq.Type).Arg;
+ elmtType = ((SeqType)seqType).Arg;
+ } else if (seqType is MapType) {
+ domainType = ((MapType)seqType).Domain;
+ elmtType = ((MapType)seqType).Range;
+ } else if (seqType is MultiSetType) {
+ domainType = ((MultiSetType)seqType).Arg;
elmtType = Type.Int;
} else { Contract.Assert(false); }
Bpl.Type elType = translator.TrType(elmtType);
@@ -9215,23 +9228,23 @@ namespace Microsoft.Dafny {
if (e.SelectOne) {
Contract.Assert(e1 == null);
Bpl.Expr x;
- if (e.Seq.Type.IsArrayType) {
+ if (seqType.IsArrayType) {
Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0);
x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName);
- } else if(e.Seq.Type is SeqType) {
+ } else if (seqType is SeqType) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
- } else if (e.Seq.Type is MapType) {
+ } else if (seqType is MapType) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq);
x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType));
- } else if (e.Seq.Type is MultiSetType) {
+ } else if (seqType is MultiSetType) {
x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType));
} else { Contract.Assert(false); x = null; }
- if (!ModeledAsBoxType(elmtType) && !(e.Seq.Type is MultiSetType)) {
+ if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
}
return x;
} else {
- if (e.Seq.Type.IsArrayType) {
+ if (seqType.IsArrayType) {
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqFromArray, elType, HeapExpr, seq);
}
var isLit = translator.IsLit(seq);
@@ -9260,24 +9273,25 @@ namespace Microsoft.Dafny {
else
{
Bpl.Expr seq = TrExpr(e.Seq);
- if (e.Seq.Type is SeqType)
+ var seqType = e.Seq.Type.NormalizeExpand();
+ if (seqType is SeqType)
{
- Type elmtType = cce.NonNull((SeqType)e.Seq.Type).Arg;
+ Type elmtType = cce.NonNull((SeqType)seqType).Arg;
Bpl.Expr index = TrExpr(e.Index);
Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);
}
- else if (e.Seq.Type is MapType)
+ else if (seqType is MapType)
{
- MapType mt = (MapType)e.Seq.Type;
+ MapType mt = (MapType)seqType;
Bpl.Type maptype = predef.MapType(expr.tok, predef.BoxType, predef.BoxType);
Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain);
Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range);
return translator.FunctionCall(expr.tok, "Map#Build", maptype, seq, index, val);
}
- else if (e.Seq.Type is MultiSetType)
+ else if (seqType is MultiSetType)
{
- Type elmtType = cce.NonNull((MultiSetType)e.Seq.Type).Arg;
+ Type elmtType = cce.NonNull((MultiSetType)seqType).Arg;
Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType);
Bpl.Expr val = TrExpr(e.Value);
return Bpl.Expr.StoreTok(expr.tok, seq, index, val);
@@ -9352,10 +9366,11 @@ namespace Microsoft.Dafny {
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
- if (e.E.Type is SetType) {
- return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSet, translator.TrType(cce.NonNull((SetType)e.E.Type).Arg), TrExpr(e.E));
- } else if (e.E.Type is SeqType) {
- return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSeq, translator.TrType(cce.NonNull((SeqType)e.E.Type).Arg), TrExpr(e.E));
+ var eType = e.E.Type.NormalizeExpand();
+ if (eType is SetType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSet, translator.TrType(cce.NonNull((SetType)eType).Arg), TrExpr(e.E));
+ } else if (eType is SeqType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSeq, translator.TrType(cce.NonNull((SeqType)eType).Arg), TrExpr(e.E));
} else {
Contract.Assert(false); throw new cce.UnreachableException();
}
@@ -9369,29 +9384,31 @@ namespace Microsoft.Dafny {
case UnaryOpExpr.Opcode.Not:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
case UnaryOpExpr.Opcode.Cardinality:
- if (e.E.Type is SeqType) {
+ var eType = e.E.Type.NormalizeExpand();
+ if (eType is SeqType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
- } else if (e.E.Type is SetType) {
+ } else if (eType is SetType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SetCard, null, arg);
- } else if (e.E.Type is MultiSetType) {
+ } else if (eType is MultiSetType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetCard, null, arg);
- } else if (e.E.Type is MapType) {
+ } else if (eType is MapType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.MapCard, null, arg);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected sized type
}
case UnaryOpExpr.Opcode.Fresh:
- if (e.E.Type is SetType) {
+ var eeType = e.E.Type.NormalizeExpand();
+ if (eeType is SetType) {
// generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])
// TODO: trigger?
Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
- Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);
+ Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)eeType).Arg);
Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o));
Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);
return new Bpl.ForallExpr(expr.tok, new List<Variable> { oVar }, body);
- } else if (e.E.Type is SeqType) {
+ } else if (eeType is SeqType) {
// generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc])
// TODO: trigger?
Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
@@ -9403,9 +9420,9 @@ namespace Microsoft.Dafny {
Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(XsubI, predef.Null);
Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);
return new Bpl.ForallExpr(expr.tok, new List<Variable> { iVar }, body);
- } else if (e.E.Type.IsDatatype) {
- // translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);
- Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), e.E.Type, Old.HeapExpr);
+ } else if (eeType.IsDatatype) {
+ // translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);
+ Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), eeType, Old.HeapExpr);
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc);
} else {
// generate: x != null && !old($Heap)[x]
@@ -9432,7 +9449,7 @@ namespace Microsoft.Dafny {
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
- bool isReal = e.E0.Type is RealType;
+ bool isReal = e.E0.Type.IsRealType;
Bpl.Expr e0 = TrExpr(e.E0);
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {
return TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1
@@ -9478,16 +9495,20 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.EqCommon:
keepLits = true;
- if (e.E0.Type.IsCoDatatype) {
- var cot = e.E0.Type.AsCoDatatype;
- return translator.CoEqualCall(cot, e.E0.Type.TypeArgs, e.E1.Type.TypeArgs, null, LayerN(2), e0, e1, expr.tok);
+ var cot = e.E0.Type.AsCoDatatype;
+ if (cot != null) {
+ var e0args = e.E0.Type.NormalizeExpand().TypeArgs;
+ var e1args = e.E1.Type.NormalizeExpand().TypeArgs;
+ return translator.CoEqualCall(cot, e0args, e1args, null, LayerN(2), e0, e1, expr.tok);
}
typ = Bpl.Type.Bool;
bOpcode = BinaryOperator.Opcode.Eq; break;
case BinaryExpr.ResolvedOpcode.NeqCommon:
- if (e.E0.Type.IsCoDatatype) {
- var cot = e.E0.Type.AsCoDatatype;
- var x = translator.CoEqualCall(cot, e.E0.Type.TypeArgs, e.E1.Type.TypeArgs, null, LayerN(2), e0, e1, expr.tok);
+ var cotx = e.E0.Type.AsCoDatatype;
+ if (cotx != null) {
+ var e0args = e.E0.Type.NormalizeExpand().TypeArgs;
+ var e1args = e.E1.Type.NormalizeExpand().TypeArgs;
+ var x = translator.CoEqualCall(cotx, e0args, e1args, null, LayerN(2), e0, e1, expr.tok);
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, x);
}
typ = Bpl.Type.Bool;
@@ -9547,11 +9568,11 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.NotInSet:
Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
case BinaryExpr.ResolvedOpcode.Union:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(expr.Type.AsSetType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.Intersection:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(expr.Type.AsSetType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.SetDifference:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(expr.Type.AsSetType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.MultiSetEq:
return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1);
@@ -9576,11 +9597,11 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.NotInMultiSet:
Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
case BinaryExpr.ResolvedOpcode.MultiSetUnion:
- return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnion, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnion, translator.TrType(expr.Type.AsMultiSetType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.MultiSetIntersection:
- return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetIntersection, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetIntersection, translator.TrType(expr.Type.AsMultiSetType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.MultiSetDifference:
- return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDifference, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDifference, translator.TrType(expr.Type.AsMultiSetType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.SeqEq:
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEqual, null, e0, e1);
@@ -9597,7 +9618,7 @@ namespace Microsoft.Dafny {
translator.FunctionCall(expr.tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
}
case BinaryExpr.ResolvedOpcode.Concat:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(cce.NonNull((SeqType)expr.Type).Arg), e0, e1);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(expr.Type.AsSeqType.Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.InSeq:
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1,
BoxIfNecessary(expr.tok, e0, cce.NonNull(e.E0.Type)));
@@ -9642,9 +9663,11 @@ namespace Microsoft.Dafny {
switch (e.Op) {
case TernaryExpr.Opcode.PrefixEqOp:
case TernaryExpr.Opcode.PrefixNeqOp:
- var cot = e.E1.Type.AsCoDatatype;
+ var e1type = e.E1.Type.NormalizeExpand();
+ var e2type = e.E2.Type.NormalizeExpand();
+ var cot = e1type.AsCoDatatype;
Contract.Assert(cot != null); // the argument types of prefix equality (and prefix disequality) are codatatypes
- var r = translator.CoEqualCall(cot, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, e0, LayerN(2), e1, e2);
+ var r = translator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, LayerN(2), e1, e2);
if (e.Op == TernaryExpr.Opcode.PrefixEqOp) {
return r;
} else {
@@ -10658,7 +10681,7 @@ namespace Microsoft.Dafny {
/// </summary>
bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, bool apply_induction, ExpressionTranslator etran) {
Contract.Requires(expr != null);
- Contract.Requires(expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType));
+ Contract.Requires(expr.Type.IsBoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type.IsBoolType));
Contract.Requires(splits != null);
Contract.Requires(etran != null);
@@ -10734,7 +10757,9 @@ namespace Microsoft.Dafny {
} else if (expr is TernaryExpr) {
var e = (TernaryExpr)expr;
if ((e.Op == TernaryExpr.Opcode.PrefixEqOp && position) || (e.Op == TernaryExpr.Opcode.PrefixNeqOp && !position)) {
- var codecl = e.E1.Type.AsCoDatatype;
+ var e1type = e.E1.Type.NormalizeExpand();
+ var e2type = e.E2.Type.NormalizeExpand();
+ var codecl = e1type.AsCoDatatype;
Contract.Assert(codecl != null);
var k = etran.TrExpr(e.E0);
var A = etran.TrExpr(e.E1);
@@ -10744,7 +10769,7 @@ namespace Microsoft.Dafny {
// checked $PrefixEqual#Dt(k, A, B) || (0 < k ==> A.Cons? ==> B.Cons? && A.head == B.head && $PrefixEqual#2#Dt(k - 1, A.tail, B.tail)) // note the #2 in the recursive call, just like for user-defined predicates that are inlined by TrSplitExpr
// free $PrefixEqual#Dt(k, A, B);
var kPos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);
- var prefixEqK = CoEqualCall(codecl, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, k, etran.LayerN(2), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);
+ var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, k, etran.LayerN(2), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);
var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));
// for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions)
var etran2 = etran.LayerOffset(1);
@@ -10753,7 +10778,7 @@ namespace Microsoft.Dafny {
var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr);
// Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+
Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2);
- foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, kMinusOne, layer, A2, B2, true)) {
+ foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) {
var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c));
splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));
}
@@ -10901,7 +10926,7 @@ namespace Microsoft.Dafny {
var substMap = new Dictionary<IVariable, Expression>();
foreach (var n in inductionVariables) {
toks.Add(n.tok);
- types.Add(n.Type);
+ types.Add(n.Type.NormalizeExpand());
BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + otherTmpVarCount, n.Type);
otherTmpVarCount++;
kvars.Add(k);
@@ -11331,6 +11356,7 @@ namespace Microsoft.Dafny {
}
IEnumerable<Bpl.Expr> InductionCases(Type ty, Bpl.Expr expr, ExpressionTranslator etran) {
+ ty = ty.NormalizeExpand();
IndDatatypeDecl dt = ty.AsIndDatatype;
if (dt == null) {
yield return Bpl.Expr.True;
@@ -11401,7 +11427,7 @@ namespace Microsoft.Dafny {
if (ty.IsTypeParameter && ! ty.AsTypeParameter.IsAbstractTypeDeclaration) {
fvs.Add(ty.AsTypeParameter);
}
- ty.TypeArgs.Iter(tt => ComputeFreeTypeVariables(tt, fvs));
+ ty.NormalizeExpand().TypeArgs.Iter(tt => ComputeFreeTypeVariables(tt, fvs));
}
static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, ref bool usesOldHeap, ref Type usesThis, bool inOldContext) {
@@ -12458,6 +12484,8 @@ namespace Microsoft.Dafny {
}
static List<A> Concat<A>(List<A> xs, List<A> ys) {
+ Contract.Requires(xs != null);
+ Contract.Requires(ys != null);
List<A> cpy = new List<A>(xs);
cpy.AddRange(ys);
return cpy;
@@ -12465,6 +12493,8 @@ namespace Microsoft.Dafny {
public static List<B> Map<A,B>(IEnumerable<A> xs, Func<A,B> f)
{
+ Contract.Requires(xs != null);
+ Contract.Requires(f != null);
List<B> ys = new List<B>();
foreach (A x in xs) {
ys.Add(f(x));
@@ -12474,6 +12504,8 @@ namespace Microsoft.Dafny {
public static void MapM<A>(IEnumerable<A> xs, Action<A> K)
{
+ Contract.Requires(xs != null);
+ Contract.Requires(K != null);
foreach (A x in xs) {
K(x);
}
diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs
index 6f0cab13..d6bd895a 100644
--- a/Source/DafnyExtension/DafnyRuntime.cs
+++ b/Source/DafnyExtension/DafnyRuntime.cs
@@ -656,6 +656,13 @@ namespace Dafny
num = n;
den = d;
}
+ public BigInteger ToBigInteger() {
+ if (0 <= num) {
+ return num / den;
+ } else {
+ return (num - den + 1) / den;
+ }
+ }
/// <summary>
/// Returns values such that aa/dd == a and bb/dd == b.
/// </summary>
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy
index efe88446..9e0d3b63 100644
--- a/Test/dafny0/AutoReq.dfy
+++ b/Test/dafny0/AutoReq.dfy
@@ -146,170 +146,170 @@ module {:autoReq} QuantifierTestsHard {
function n(x:int) : bool
function f1(x:int) : bool
- requires x > 3;
- requires x < 16;
+ requires x > 3;
+ requires x < 16;
function variable_uniqueness_test(x:int) : bool
{
(forall y:int :: m(y))
- &&
- f1(x)
+ &&
+ f1(x)
}
}
module CorrectReqOrdering {
- function f1(x:int) : bool
- requires x > 3;
+ function f1(x:int) : bool
+ requires x > 3;
- function f2(b:bool) : bool
- requires b;
+ function f2(b:bool) : bool
+ requires b;
- // Should pass if done correctly.
- // However, if Dafny incorrectly put the requires for f2 first,
- // then the requires for f1 won't be satisfied
- function {:autoReq} f3(z:int) : bool
- {
- f2(f1(z))
- }
+ // Should pass if done correctly.
+ // However, if Dafny incorrectly put the requires for f2 first,
+ // then the requires for f1 won't be satisfied
+ function {:autoReq} f3(z:int) : bool
+ {
+ f2(f1(z))
+ }
}
-module ShortCircuiting {
- function f1(x:int) : bool
- requires x > 3;
+module ShortCircuiting {
+ function f1(x:int) : bool
+ requires x > 3;
- function f2(y:int) : bool
- requires y < 10;
+ function f2(y:int) : bool
+ requires y < 10;
- function {:autoReq} test1(x':int, y':int) : bool
- {
- f1(x') && f2(y')
- }
+ function {:autoReq} test1(x':int, y':int) : bool
+ {
+ f1(x') && f2(y')
+ }
- function {:autoReq} test2(x':int, y':int) : bool
- {
- f1(x') ==> f2(y')
- }
+ function {:autoReq} test2(x':int, y':int) : bool
+ {
+ f1(x') ==> f2(y')
+ }
- function {:autoReq} test3(x':int, y':int) : bool
- {
- f1(x') || f2(y')
- }
+ function {:autoReq} test3(x':int, y':int) : bool
+ {
+ f1(x') || f2(y')
+ }
}
module Lets {
- function f1(x:int) : bool
- requires x > 3;
+ function f1(x:int) : bool
+ requires x > 3;
- function {:autoReq} test1(x':int) : bool
- {
- var y' := 3*x'; f1(y')
- }
+ function {:autoReq} test1(x':int) : bool
+ {
+ var y' := 3*x'; f1(y')
+ }
}
// Test nested module specification of :autoReq attribute
module {:autoReq} M1 {
- module M2 {
- function f(x:int) : bool
- requires x > 3;
- {
- x > 7
- }
-
- // Should succeed thanks to auto-generation based on f's requirements
- function {:autoReq} h(y:int) : bool
- {
- f(y)
- }
+ module M2 {
+ function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
}
+
+ // Should succeed thanks to auto-generation based on f's requirements
+ function {:autoReq} h(y:int) : bool
+ {
+ f(y)
+ }
+ }
}
module Datatypes {
- datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
+ datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
- function f1(t:TheType):bool
- requires t.TheType_builder? && t.x > 3;
+ function f1(t:TheType):bool
+ requires t.TheType_builder? && t.x > 3;
- function {:autoReq} test(t:TheType) : bool
- {
- f1(t)
- }
+ function {:autoReq} test(t:TheType) : bool
+ {
+ f1(t)
+ }
- function f2(x:int) : bool
- requires forall t:TheType :: t.TheType_builder? && t.x > x;
- {
- true
- }
+ function f2(x:int) : bool
+ requires forall t:TheType :: t.TheType_builder? && t.x > x;
+ {
+ true
+ }
- // Should cause a function-requirement violation without autoReq
- function f3(y:int) : bool
- {
- f2(y)
- }
+ // Should cause a function-requirement violation without autoReq
+ function f3(y:int) : bool
+ {
+ f2(y)
+ }
- function {:autoReq} test2(z:int) : bool
- {
- f2(z)
- }
+ function {:autoReq} test2(z:int) : bool
+ {
+ f2(z)
+ }
}
module Matches {
- datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
+ datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
- function f1(x:int):bool
- requires x > 3;
+ function f1(x:int):bool
+ requires x > 3;
- function {:autoReq} basic_test(t:TheType) : bool
- {
- match t
- case TheType_builder(x) => f1(x)
- case TheType_copier(t) => true
- }
+ function {:autoReq} basic_test(t:TheType) : bool
+ {
+ match t
+ case TheType_builder(x) => f1(x)
+ case TheType_copier(t) => true
+ }
}
// Make sure :autoReq works with static functions
module StaticTest {
- static function f(x:int) : bool
- requires x > 3;
- {
- x > 7
- }
+ static function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
+ }
- static function {:autoReq} g(z:int) : bool
- requires f(z);
- {
- true
- }
-
- // Should succeed thanks to auto-generation based on f's requirements
- static function {:autoReq} h(y:int) : bool
- {
- g(y)
- }
+ static function {:autoReq} g(z:int) : bool
+ requires f(z);
+ {
+ true
+ }
- static predicate IsEven(x:int)
+ // Should succeed thanks to auto-generation based on f's requirements
+ static function {:autoReq} h(y:int) : bool
+ {
+ g(y)
+ }
- static function EvenDoubler(x:int) : int
- requires IsEven(x);
+ static predicate IsEven(x:int)
- // Should succeed thanks to auto-generated requirement of IsEven
- static function {:autoReq} test(y:int) : int
- {
- EvenDoubler(y)
- }
+ static function EvenDoubler(x:int) : int
+ requires IsEven(x);
+
+ // Should succeed thanks to auto-generated requirement of IsEven
+ static function {:autoReq} test(y:int) : int
+ {
+ EvenDoubler(y)
+ }
}
module OpaqueTest {
- static function bar(x:int) : int
- requires x>7;
- {
- x-2
- }
+ static function bar(x:int) : int
+ requires x>7;
+ {
+ x-2
+ }
- static function {:autoReq} {:opaque} foo(x:int) : int
- {
- bar(x)
- }
+ static function {:autoReq} {:opaque} foo(x:int) : int
+ {
+ bar(x)
+ }
}
diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect
index 617e6003..547b676d 100644
--- a/Test/dafny0/AutoReq.dfy.expect
+++ b/Test/dafny0/AutoReq.dfy.expect
@@ -1,5 +1,5 @@
-AutoReq.dfy(247,3): Error: possible violation of function precondition
-AutoReq.dfy(239,12): Related location
+AutoReq.dfy(247,5): Error: possible violation of function precondition
+AutoReq.dfy(239,14): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Else
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 410e4507..70e46ff0 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by
EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality
EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
-EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
+EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)
EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 520b2e38..9f6c948a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1007,20 +1007,20 @@ module CycleError2 {
type A = B // error: cycle: A -> B -> A
type B = set<A>
}
-module Good0 {
+module CycleErrors3 {
type A = (B, D<bool>)
type B = C
class C {
var a: A; // this is fine
}
- datatype D<X> = Make(A, B, C) // this is fine, too
+ datatype D<X> = Make(A, B, C) // error: cannot construct a D<X>
}
-module CycleError3 {
+module CycleError4 {
type A = B // error: cycle: A -> B -> A
type B = C<A>
class C<T> { }
}
-module CycleError4 {
+module CycleError5 {
type A = B // error: cycle: A -> B -> A
type B = Dt<A>
datatype Dt<T> = Make(T)
@@ -1090,3 +1090,13 @@ module OpaqueTypes1 {
assert p != q; // error: types must be the same in order to do compare
}
}
+
+// ----- new trait -------------------------------------------
+
+
+trait J { }
+type JJ = J
+method TraitSynonym()
+{
+ var x := new JJ; // error: new cannot be applied to a trait
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 49cfe650..b11fa9f8 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -63,6 +63,7 @@ ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter
ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A
ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
@@ -171,4 +172,5 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i
ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)
ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)
ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
-173 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
+175 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
index 1d44d0f6..4a908ee7 100644
--- a/Test/dafny0/Trait/TraitBasix.dfy.expect
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -1,7 +1,7 @@
+TraitBasix.dfy(91,23): Error: unresolved identifier: IX
TraitBasix.dfy(77,13): Error: member in the class has been already inherited from its parent trait
TraitBasix.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable
TraitBasix.dfy(80,7): Error: class: I0Child2 does not implement trait member: F
-TraitBasix.dfy(91,7): Error: unresolved identifier: IX
TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor
-TraitBasix.dfy(117,10): Error: new can not be applied to a trait
+TraitBasix.dfy(117,10): Error: new cannot be applied to a trait
6 resolution/type errors detected in TraitBasix.dfy
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect
index 589fba07..b9031dac 100644
--- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect
+++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect
@@ -1,2 +1,2 @@
-TraitMultiModule.dfy(21,9): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
+TraitMultiModule.dfy(21,20): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
1 resolution/type errors detected in TraitMultiModule.dfy
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect
index 4020b880..1e7bface 100644
--- a/Test/dafny0/Trait/TraitOverride0.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect
@@ -1,4 +1,4 @@
-TraitOverride0.dfy(53,20): Error: a class can not override implemented functions
+TraitOverride0.dfy(53,20): Error: a class cannot override implemented functions
TraitOverride0.dfy(48,20): Error: function 'BodyLess1' is declared with a different number of parameter (1 instead of 0) than the corresponding function in the module it overrides
TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess1
TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess2
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect
index 0f7b49e3..c90560b0 100644
--- a/Test/dafny0/Trait/TraitOverride1.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect
@@ -1,2 +1,2 @@
-Dafny program verifier finished with 62 verified, 0 errors
+Dafny program verifier finished with 52 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
index 6849499c..b59d7b80 100644
--- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
@@ -5,4 +5,4 @@ Execution trace:
(0,0): anon2
(0,0): anon6_Then
-Dafny program verifier finished with 9 verified, 1 error
+Dafny program verifier finished with 7 verified, 1 error
diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy
index 4bec5253..85beb340 100644
--- a/Test/dafny0/TypeSynonyms.dfy
+++ b/Test/dafny0/TypeSynonyms.dfy
@@ -44,3 +44,10 @@ function Skip(s: Synonym3): Synonym0
case Nil => Nil
case Cons(_, tail) => tail
}
+
+type MyMap = map<int, map<real, bool>>
+
+predicate MyMapProperty(m: MyMap, x: int)
+{
+ x in m && real(x) in m[x] && m[x][real(x)]
+}
diff --git a/Test/dafny0/TypeSynonyms.dfy.expect b/Test/dafny0/TypeSynonyms.dfy.expect
index 4ef2de53..76f19e0d 100644
--- a/Test/dafny0/TypeSynonyms.dfy.expect
+++ b/Test/dafny0/TypeSynonyms.dfy.expect
@@ -1,2 +1,2 @@
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 62e41019..5d78fe16 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -25,8 +25,8 @@ TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the
TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts
TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context