diff options
| author |  leino <unknown> | 2014-08-02 01:05:17 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-02 01:05:17 -0700 |
| commit | ae578ae92040975fed005d045110679e4e858c31 (patch) | |
| tree | 79f2a3a67c8c9059a89d9771e933c8a0b6b601bf | |
| parent | 54b670417f5974c43ef2fd55d37ba3806ad5c72d (diff) | |
Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator
| -rw-r--r-- | Source/Dafny/Cloner.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 56 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 84 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 127 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 268 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyRuntime.cs | 7 | ||||
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 3 | ||||
| -rw-r--r-- | Test/dafny0/TypeSynonyms.dfy | 7 | ||||
| -rw-r--r-- | Test/dafny0/TypeSynonyms.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy.expect | 4 |
13 files changed, 356 insertions, 225 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index bb644825..8ef8f0ee 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -142,6 +142,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();
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index c665026c..c8af05f4 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1543,8 +1543,6 @@ namespace Microsoft.Dafny { // ...
// }
if (s.Cases.Count != 0) {
- var sourceType = (UserDefinedType)s.Source.Type;
-
SpillLetVariableDecls(s.Source, indent);
string source = "_source" + tmpVarCount;
tmpVarCount++;
@@ -1554,6 +1552,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);
@@ -1820,7 +1819,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));
@@ -2002,24 +2001,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);
@@ -2074,11 +2073,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();
@@ -2198,7 +2198,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)");
@@ -2214,11 +2214,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)");
@@ -2243,10 +2243,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.
@@ -2257,11 +2256,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.
@@ -2287,7 +2285,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(", ");
@@ -2298,7 +2296,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(", ");
@@ -2453,7 +2451,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 ");
@@ -2536,7 +2534,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;
@@ -2605,8 +2603,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 21227dd6..7f86e078 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) {
@@ -4278,6 +4305,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);
@@ -4295,7 +4329,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
@@ -4327,7 +4361,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
@@ -4341,7 +4375,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
@@ -4354,7 +4388,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) {
@@ -4369,7 +4403,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) {
@@ -4406,7 +4440,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;
@@ -4418,7 +4452,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
@@ -4432,7 +4466,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
@@ -4466,7 +4500,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;
@@ -4486,7 +4520,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;
@@ -4505,7 +4539,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/Resolver.cs b/Source/Dafny/Resolver.cs index 5e7381d9..02af6e12 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -474,16 +474,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
@@ -496,7 +497,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);
}
}
@@ -2014,7 +2015,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;
@@ -2884,11 +2885,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);
@@ -2981,6 +2983,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
@@ -3213,8 +3216,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);
@@ -3756,6 +3760,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) {
@@ -3989,7 +3997,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
@@ -4032,7 +4040,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;
@@ -4099,7 +4107,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 {
@@ -4181,6 +4189,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>
@@ -4367,7 +4389,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'");
}
@@ -4761,7 +4783,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);
}
@@ -4875,7 +4897,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);
@@ -5318,7 +5340,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) {
@@ -5621,8 +5643,6 @@ namespace Microsoft.Dafny }
}
-
-
Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {
Contract.Requires(rr != null);
Contract.Requires(stmt != null);
@@ -5639,9 +5659,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);
@@ -5650,7 +5667,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) {
@@ -5690,8 +5707,8 @@ namespace Microsoft.Dafny // ---------- new C
Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null);
}
- if (!callsConstructor && rr.EType is UserDefinedType) {
- var udt = (UserDefinedType)rr.EType;
+ if (!callsConstructor && 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) {
Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name);
@@ -5823,6 +5840,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);
@@ -5841,7 +5872,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
@@ -5887,6 +5918,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);
@@ -5928,7 +5970,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 {
@@ -6079,7 +6121,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;
@@ -6134,8 +6176,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");
@@ -6203,7 +6245,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;
@@ -6227,10 +6269,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
@@ -6252,11 +6294,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 {
@@ -6322,14 +6364,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 {
@@ -6359,14 +6401,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 {
@@ -6684,7 +6726,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);
}
@@ -6779,7 +6821,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
@@ -6870,6 +6912,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);
@@ -7494,12 +7538,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;
}
@@ -7983,6 +8027,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 a936200e..330afd8a 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);
}
@@ -2447,7 +2460,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);
@@ -2951,8 +2964,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);
@@ -2974,12 +2987,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));
@@ -3235,7 +3249,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;
@@ -3571,20 +3584,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 {
@@ -3598,14 +3612,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));
@@ -3645,20 +3659,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);
@@ -3834,7 +3842,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));
}
@@ -5725,7 +5733,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;
@@ -5733,13 +5742,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;
}
@@ -5747,28 +5756,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;
@@ -6580,12 +6589,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);
@@ -6616,12 +6625,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);
@@ -7034,8 +7043,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));
}
@@ -7056,6 +7065,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)
@@ -7157,6 +7167,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);
@@ -7169,8 +7182,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) {
@@ -7442,7 +7453,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;
@@ -7871,7 +7882,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));
}
@@ -7883,7 +7895,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;
@@ -8597,20 +8609,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);
@@ -8620,23 +8633,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);
@@ -8665,24 +8678,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);
@@ -8757,10 +8771,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();
}
@@ -8774,29 +8789,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));
@@ -8808,9 +8825,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]
@@ -8837,7 +8854,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
@@ -8883,16 +8900,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;
@@ -8952,11 +8973,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);
@@ -8981,11 +9002,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);
@@ -9002,7 +9023,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)));
@@ -9047,9 +9068,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 {
@@ -10063,7 +10086,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);
@@ -10139,7 +10162,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);
@@ -10149,7 +10174,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);
@@ -10158,7 +10183,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));
}
@@ -10306,7 +10331,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);
@@ -10736,6 +10761,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;
@@ -10806,7 +10832,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) {
@@ -11863,6 +11889,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;
@@ -11870,6 +11898,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));
@@ -11879,6 +11909,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/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..aaf1291c 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)
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 49cfe650..d5d12eb9 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,4 @@ 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
+174 resolution/type errors detected in ResolutionErrors.dfy
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
|