summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs22
-rw-r--r--Source/Dafny/DafnyAst.cs62
-rw-r--r--Source/Dafny/Resolver.cs165
-rw-r--r--Source/Dafny/Translator.cs69
-rw-r--r--Test/dafny0/CoResolution.dfy.expect4
-rw-r--r--Test/dafny0/DerivedTypes.dfy38
-rw-r--r--Test/dafny0/DerivedTypes.dfy.expect3
-rw-r--r--Test/dafny0/DerivedTypesResolution.dfy38
-rw-r--r--Test/dafny0/DerivedTypesResolution.dfy.expect10
-rw-r--r--Test/dafny0/OpaqueFunctionsFail.dfy.expect8
-rw-r--r--Test/dafny0/ResolutionErrors.dfy6
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect9
-rw-r--r--Test/hofs/Underspecified.dfy.expect8
13 files changed, 339 insertions, 103 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index bba99355..6c35fc45 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2298,14 +2298,22 @@ namespace Microsoft.Dafny {
} else if (expr is ConversionExpr) {
var e = (ConversionExpr)expr;
if (e.ToType is IntType) {
- Contract.Assert(e.E.Type.IsRealType);
- TrParenExpr(e.E);
- wr.Write(".ToBigInteger()");
+ if (e.E.Type.IsNumericBased(Type.NumericPersuation.Int)) {
+ TrParenExpr(e.E);
+ } else {
+ Contract.Assert(e.E.Type.IsRealType);
+ TrParenExpr(e.E);
+ wr.Write(".ToBigInteger()");
+ }
} else if (e.ToType is RealType) {
- Contract.Assert(e.E.Type.IsIntegerType);
- wr.Write("new Dafny.BigRational(");
- TrExpr(e.E);
- wr.Write(", BigInteger.One)");
+ if (e.E.Type.IsNumericBased(Type.NumericPersuation.Real)) {
+ TrParenExpr(e.E);
+ } else {
+ Contract.Assert(e.E.Type.IsIntegerType);
+ wr.Write("new Dafny.BigRational(");
+ TrExpr(e.E);
+ wr.Write(", BigInteger.One)");
+ }
} else {
Contract.Assert(false); // unexpected ConversionExpr to-type
}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 35a70869..6fec41e4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -364,10 +364,33 @@ namespace Microsoft.Dafny {
public bool IsSubrangeType {
get { return NormalizeExpand() is NatType; }
}
- public bool IsNumericBased {
- get {
- var t = NormalizeExpand();
- return t.IsIntegerType || t.IsRealType || t.AsDerivedType != null;
+ public bool IsNumericBased() {
+ var t = NormalizeExpand();
+ return t.IsIntegerType || t.IsRealType || t.AsDerivedType != null;
+ }
+ public enum NumericPersuation { Int, Real }
+ public bool IsNumericBased(NumericPersuation p) {
+ Type t = this;
+ while (true) {
+ t = t.NormalizeExpand();
+ if (t.IsIntegerType) {
+ return p == NumericPersuation.Int;
+ } else if (t.IsRealType) {
+ return p == NumericPersuation.Real;
+ }
+ var proxy = t as OperationTypeProxy;
+ if (proxy != null) {
+ if (proxy.JustInts) {
+ return p == NumericPersuation.Int;
+ } else if (proxy.JustReals) {
+ return p == NumericPersuation.Real;
+ }
+ }
+ var d = t.AsDerivedType;
+ if (d == null) {
+ return false;
+ }
+ t = d.BaseType;
}
}
@@ -1141,9 +1164,20 @@ namespace Microsoft.Dafny {
/// In addition, if AllowSetVarieties, it can stand for a set or multiset.
/// </summary>
public class OperationTypeProxy : RestrictedTypeProxy {
+ public readonly bool AllowInts;
+ public readonly bool AllowReals;
public readonly bool AllowSeq;
public readonly bool AllowSetVarieties;
- public OperationTypeProxy(bool allowSeq, bool allowSetVarieties) {
+ public bool JustInts {
+ get { return AllowInts && !AllowReals && !AllowSeq && !AllowSetVarieties; }
+ }
+ public bool JustReals {
+ get { return !AllowInts && AllowReals && !AllowSeq && !AllowSetVarieties; }
+ }
+ public OperationTypeProxy(bool allowInts, bool allowReals, bool allowSeq, bool allowSetVarieties) {
+ Contract.Requires(allowInts || allowReals || allowSeq || allowSetVarieties); // don't allow unsatisfiable constraint
+ AllowInts = allowInts;
+ AllowReals = allowReals;
AllowSeq = allowSeq;
AllowSetVarieties = allowSetVarieties;
}
@@ -1152,6 +1186,19 @@ namespace Microsoft.Dafny {
return 3;
}
}
+ [Pure]
+ public override string TypeName(ModuleDefinition context) {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ if (T == null) {
+ if (JustInts) {
+ return "int";
+ } else if (JustReals) {
+ return "real";
+ }
+ }
+ return base.TypeName(context);
+ }
}
/// <summary>
@@ -1162,11 +1209,13 @@ namespace Microsoft.Dafny {
/// This proxy stands for one of:
/// seq(T) Domain,Range,Arg := int,T,T
/// multiset(T) Domain,Range,Arg := T,int,T
+ /// if AllowMap, may also be:
/// map(T,U) Domain,Range,Arg := T,U,T
/// if AllowArray, may also be:
/// array(T) Domain,Range,Arg := int,T,T
/// </summary>
public class IndexableTypeProxy : RestrictedTypeProxy {
+ public readonly bool AllowMap;
public readonly bool AllowArray;
public readonly Type Domain, Range, Arg;
[ContractInvariantMethod]
@@ -1176,13 +1225,14 @@ namespace Microsoft.Dafny {
Contract.Invariant(Arg != null);
}
- public IndexableTypeProxy(Type domain, Type range, Type arg, bool allowArray) {
+ public IndexableTypeProxy(Type domain, Type range, Type arg, bool allowMap, bool allowArray) {
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Requires(arg != null);
Domain = domain;
Range = range;
Arg = arg;
+ AllowMap = allowMap;
AllowArray = allowArray;
}
public override int OrderID {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 320a096a..dd600e18 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1545,7 +1545,7 @@ namespace Microsoft.Dafny
} else if (d is DerivedTypeDecl) {
var dd = (DerivedTypeDecl)d;
// this check can be done only after it has been determined that the redirected types do not involve cycles
- if (!dd.BaseType.IsNumericBased) {
+ if (!dd.BaseType.IsNumericBased()) {
Error(dd.tok, "derived types must be based on some numeric type (got {0})", dd.BaseType);
}
}
@@ -2030,8 +2030,8 @@ namespace Microsoft.Dafny
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
foreach (var p in s.TypeArgumentSubstitutions) {
- if (p.Value.Normalize() is TypeProxy) {
- Error(stmt.Tok, "type variable '{0}' in the method call to '{1}' could not determined", p.Key.Name, s.MethodName);
+ if (!IsDetermined(p.Value.Normalize())) {
+ Error(stmt.Tok, "type variable '{0}' in the method call to '{1}' could not be determined", p.Key.Name, s.MethodName);
}
}
}
@@ -2041,8 +2041,8 @@ namespace Microsoft.Dafny
var e = (ComprehensionExpr)expr;
if (e != null) {
foreach (var bv in e.BoundVars) {
- if (bv.Type.Normalize() is TypeProxy) {
- Error(bv.tok, "type of bound variable '{0}' could not determined; please specify the type explicitly",
+ if (!IsDetermined(bv.Type.Normalize())) {
+ Error(bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly",
bv.Name);
}
}
@@ -2051,7 +2051,7 @@ namespace Microsoft.Dafny
var e = (MemberSelectExpr)expr;
if (e.Member is Function) {
foreach (var p in e.TypeApplication) {
- if (p.Normalize() is TypeProxy) {
+ if (!IsDetermined(p.Normalize())) {
Error(e.tok, "type '{0}' to the function '{1}' is not determined", p, e.Member.Name);
}
}
@@ -2059,8 +2059,8 @@ namespace Microsoft.Dafny
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
foreach (var p in e.TypeArgumentSubstitutions) {
- if (p.Value.Normalize() is TypeProxy) {
- Error(e.tok, "type variable '{0}' in the function call to '{1}' could not determined{2}", p.Key.Name, e.Name,
+ if (!IsDetermined(p.Value.Normalize())) {
+ Error(e.tok, "type variable '{0}' in the function call to '{1}' could not be determined{2}", p.Key.Name, e.Name,
(e.Name.Contains("reveal_") || e.Name.Contains("_FULL"))
? ". If you are making an opaque function, make sure that the function can be called."
: ""
@@ -2071,7 +2071,7 @@ namespace Microsoft.Dafny
var e = (LetExpr)expr;
foreach (var p in e.LHSs) {
foreach (var x in p.Vars) {
- if (x.Type.Normalize() is TypeProxy) {
+ if (!IsDetermined(x.Type.Normalize())) {
Error(e.tok, "the type of the bound variable '{0}' could not be determined", x.Name);
}
}
@@ -2087,11 +2087,43 @@ namespace Microsoft.Dafny
}
}
}
+ /// <summary>
+ /// This method checks to see if 'tp' has been determined and returns the result.
+ /// However, if tp denotes an int-based or real-based type, then tp is set to int or real,
+ /// respectively, here.
+ /// </summary>
+ bool IsDetermined(Type t) {
+ Contract.Requires(t != null);
+ // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively
+ if (t is OperationTypeProxy) {
+ var proxy = (OperationTypeProxy)t;
+ if (proxy.JustInts) {
+ proxy.T = Type.Int;
+ return true;
+ } else if (proxy.JustReals) {
+ proxy.T = Type.Real;
+ return true;
+ }
+ }
+ return !(t is TypeProxy); // all other proxies indicate the type has not yet been determined
+ }
bool CheckTypeIsDetermined(IToken tok, Type t, string what, bool aggressive = false) {
Contract.Requires(tok != null);
Contract.Requires(t != null);
Contract.Requires(what != null);
t = t.NormalizeExpand();
+ // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively
+ if (t is OperationTypeProxy) {
+ var proxy = (OperationTypeProxy)t;
+ if (proxy.JustInts) {
+ proxy.T = Type.Int;
+ return true;
+ } else if (proxy.JustReals) {
+ proxy.T = Type.Real;
+ return true;
+ }
+ }
+
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;
@@ -4280,8 +4312,14 @@ namespace Microsoft.Dafny
} else if (proxy is OperationTypeProxy) {
var opProxy = (OperationTypeProxy)proxy;
- if (t.IsNumericBased || (opProxy.AllowSetVarieties && (t is SetType || t is MultiSetType)) || (opProxy.AllowSeq && t is SeqType)) {
- // this is the expected case
+ if (opProxy.AllowInts && t.IsNumericBased(Type.NumericPersuation.Int)) {
+ // fine
+ } else if (opProxy.AllowReals && t.IsNumericBased(Type.NumericPersuation.Real)) {
+ // fine
+ } else if (opProxy.AllowSetVarieties && (t is SetType || t is MultiSetType)) {
+ // fine
+ } else if (opProxy.AllowSeq && t is SeqType) {
+ // fine
} else {
return false;
}
@@ -4305,7 +4343,7 @@ namespace Microsoft.Dafny
} else if (!UnifyTypes(iProxy.Arg, iProxy.Range)) {
return false;
}
- } else if (t is MapType) {
+ } else if (iProxy.AllowMap && t is MapType) {
if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) {
return false;
} else if (!UnifyTypes(iProxy.Range, ((MapType)t).Range)) {
@@ -4385,16 +4423,18 @@ namespace Microsoft.Dafny
}
return true;
} else if (b is IndexableTypeProxy) {
- CollectionTypeProxy pa = (CollectionTypeProxy)a;
+ var pa = (CollectionTypeProxy)a;
var ib = (IndexableTypeProxy)b;
// pa is:
// set(Arg) or multiset(Arg) or seq(Arg) or map(Arg, anyRange)
- // pb is:
- // seq(Arg) or multiset(Arg) or map(Domain, Arg), or
+ // ib is:
+ // multiset(Arg) or
+ // seq(Arg) or
+ // if AllowMap, map(Domain, Arg), or
// if AllowArray, array(Arg)
// Their intersection is:
if (ib.AllowArray) {
- var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, false);
+ var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, ib.AllowMap, false);
ib.T = c;
ib = c;
}
@@ -4407,36 +4447,67 @@ namespace Microsoft.Dafny
} else if (a is OperationTypeProxy) {
var pa = (OperationTypeProxy)a;
if (b is OperationTypeProxy) {
- if (pa.AllowSeq) {
- a.T = b; // a has the weaker requirement
- } else {
+ var pb = (OperationTypeProxy)b;
+ var i = pa.AllowInts && pb.AllowInts;
+ var r = pa.AllowReals && pb.AllowReals;
+ var q = pa.AllowSeq && pb.AllowSeq;
+ var s = pa.AllowSetVarieties && pb.AllowSetVarieties;
+ if (!i && !r && !q && !s) {
+ // over-constrained
+ return false;
+ } else if (i == pa.AllowInts && r == pa.AllowReals && q == pa.AllowSeq && s == pa.AllowSetVarieties) {
b.T = a; // a has the stronger requirement
+ } else if (i == pb.AllowInts && r == pb.AllowReals && q == pb.AllowSeq && s == pb.AllowSetVarieties) {
+ a.T = b; // b has the stronger requirement
+ } else {
+ var c = new OperationTypeProxy(i, r, q, s);
+ a.T = c;
+ b.T = c;
}
return true;
} else {
- var pb = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type
- // a is: int or set or multiset or seq
- // b is: seq, multiset, map, or possibly array
- if (!pa.AllowSeq) {
+ var ib = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type
+ // a is: possibly numeric, possibly seq, possibly set or multiset
+ // b is: seq, multiset, possibly map, possibly array -- with some constraints about the type parameterization
+ // So, the intersection could include multiset and seq.
+ if (pa.AllowSetVarieties && !pa.AllowSeq) {
// strengthen a and b to a multiset type
- b.T = new MultiSetType(pb.Arg);
+ b.T = new MultiSetType(ib.Arg);
a.T = b.T;
return true;
- } else {
+ } else if (pa.AllowSeq && !pa.AllowSetVarieties) {
// strengthen a and b to a sequence type
- b.T = new SeqType(pb.Arg); // TODO: the type is really *either* a seq or a multiset
+ b.T = new SeqType(ib.Arg); // TODO: the type is really *either* a seq or a multiset
a.T = b.T;
return true;
+ } else if (!pa.AllowSeq && !pa.AllowSetVarieties) {
+ // over-constrained
+ return false;
+ } else {
+ Contract.Assert(pa.AllowSeq && pa.AllowSetVarieties); // the only case left
+ if (ib.AllowMap || ib.AllowArray) {
+ var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, false, false);
+ b.T = c;
+ b = c;
+ }
+ a.T = b;
+ return true;
}
}
} else if (a is IndexableTypeProxy) {
var ia = (IndexableTypeProxy)a;
var ib = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type
- if (ia.AllowArray) {
- a.T = b; // a has the weaker requirement
+ var am = ia.AllowMap && ib.AllowMap;
+ var ar = ia.AllowArray && ib.AllowArray;
+ if (am == ia.AllowMap && ar == ia.AllowArray) {
+ b.T = a; // a has the stronger requirement
+ } else if (am == ib.AllowMap && ar == ib.AllowArray) {
+ a.T = b; // b has the stronger requirement
} else {
- b.T = a; // a has the strong requirement
+ var c = new IndexableTypeProxy(ia.Domain, ia.Range, ia.Arg, am, ar);
+ a.T = c;
+ b.T = c;
}
return UnifyTypes(ia.Domain, ib.Domain) && UnifyTypes(ia.Range, ib.Range) && UnifyTypes(ia.Arg, ib.Arg);
@@ -5162,8 +5233,8 @@ namespace Microsoft.Dafny
guess = Expression.CreateSubtract(bin.E0, bin.E1);
break;
case BinaryExpr.ResolvedOpcode.NeqCommon:
- 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)
+ if (bin.E0.Type.IsNumericBased()) {
+ // for A != B where A and B are numeric, 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);
var test = Expression.CreateAtMost(bin.E0, bin.E1);
@@ -6274,11 +6345,11 @@ namespace Microsoft.Dafny
e.ResolvedExpression = e.E;
} else {
Expression zero;
- if (e.E.Type.IsRealType) {
- // we know for sure that this is a real-unary-minus
+ if (e.E.Type.IsNumericBased(Type.NumericPersuation.Real)) {
+ // we know for sure that this is a real-based unary minus
zero = new LiteralExpr(e.tok, Basetypes.BigDec.ZERO);
} else {
- // it's may be an integer operand or it may be that we don't know yet; we'll treat
+ // it may be an int-based operand or it may be that we don't know yet; we'll treat
// two cases the same way
zero = new LiteralExpr(e.tok, 0);
}
@@ -6301,9 +6372,9 @@ namespace Microsoft.Dafny
if (e.Value == null) {
e.Type = new ObjectTypeProxy();
} else if (e.Value is BigInteger) {
- e.Type = Type.Int;
+ e.Type = new OperationTypeProxy(true, false, false, false);
} else if (e.Value is Basetypes.BigDec) {
- e.Type = Type.Real;
+ e.Type = new OperationTypeProxy(false, true, false, false);
} else if (e.Value is bool) {
e.Type = Type.Bool;
} else {
@@ -6632,12 +6703,12 @@ namespace Microsoft.Dafny
ResolveType(e.tok, e.ToType, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);
ResolveExpression(e.E, opts);
if (e.ToType is IntType) {
- if (!(e.E.Type.IsRealType)) {
- Error(expr, "type conversion to int is allowed only from real (got {0})", e.E.Type);
+ if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false))) {
+ Error(expr, "type conversion to int is allowed only from numeric types (got {0})", e.E.Type);
}
} else if (e.ToType is RealType) {
- if (!(e.E.Type.IsIntegerType)) {
- Error(expr, "type conversion to real is allowed only from int (got {0})", e.E.Type);
+ if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false))) {
+ Error(expr, "type conversion to real is allowed only from numeric types(got {0})", e.E.Type);
}
} else {
Error(expr, "type conversions are not supported to this type (got {0})", e.ToType);
@@ -6718,7 +6789,7 @@ namespace Microsoft.Dafny
expr.Type = Type.Bool;
} else {
bool err = false;
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true))) {
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, true, true))) {
Error(expr, "arguments to {0} must be of a numeric type or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
err = true;
}
@@ -6755,7 +6826,7 @@ namespace Microsoft.Dafny
expr.Type = Type.Bool;
} else {
bool err = false;
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false, true))) {
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, true))) {
Error(expr, "arguments to {0} must be of a numeric type or set type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
err = true;
}
@@ -6781,7 +6852,7 @@ namespace Microsoft.Dafny
break;
case BinaryExpr.Opcode.Div:
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false, false))) {
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false))) {
Error(expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
}
if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
@@ -6791,13 +6862,13 @@ namespace Microsoft.Dafny
break;
case BinaryExpr.Opcode.Mod:
- if (!UnifyTypes(e.E0.Type, Type.Int)) {
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false))) {
Error(expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
}
- if (!UnifyTypes(e.E1.Type, Type.Int)) {
+ if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
Error(expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
}
- expr.Type = Type.Int;
+ expr.Type = e.E0.Type;
break;
default:
@@ -8395,7 +8466,7 @@ namespace Microsoft.Dafny
Type domainType = new InferredTypeProxy();
Type argType = new InferredTypeProxy();
- IndexableTypeProxy expectedType = new IndexableTypeProxy(domainType, elementType, argType, true);
+ IndexableTypeProxy expectedType = new IndexableTypeProxy(domainType, elementType, argType, true, true);
if (!UnifyTypes(e.Seq.Type, expectedType)) {
Error(e, "sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got {0})", e.Seq.Type);
seqErr = true;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4f834793..1036d539 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4676,7 +4676,7 @@ namespace Microsoft.Dafny {
break;
case BinaryExpr.ResolvedOpcode.Div:
case BinaryExpr.ResolvedOpcode.Mod: {
- Bpl.Expr zero = (e.E1.Type.IsRealType) ? Bpl.Expr.Literal(Basetypes.BigDec.ZERO) : Bpl.Expr.Literal(0);
+ Bpl.Expr zero = e.E1.Type.IsNumericBased(Type.NumericPersuation.Real) ? 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));
}
@@ -6228,10 +6228,18 @@ namespace Microsoft.Dafny {
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Type>() != null);
- type = type.NormalizeExpand();
- if (type is TypeProxy) {
- // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
- return predef.RefType;
+ while (true) {
+ type = type.NormalizeExpand();
+ if (type is TypeProxy) {
+ // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
+ return predef.RefType;
+ }
+ var d = type.AsDerivedType;
+ if (d == null) {
+ break;
+ } else {
+ type = d.BaseType; // the Boogie type to be used for the derived type is the same as for the base type
+ }
}
if (type is BoolType) {
@@ -7103,15 +7111,14 @@ namespace Microsoft.Dafny {
var empty = new SeqDisplayExpr(x.tok, new List<Expression>());
empty.Type = xType;
yield return empty;
- } else if (xType is IntType) {
+ } else if (xType.IsNumericBased(Type.NumericPersuation.Int)) {
var lit = new LiteralExpr(x.tok, 0);
- lit.Type = Type.Int; // resolve here
+ lit.Type = xType; // resolve here
yield return lit;
- } else if (xType is RealType) {
+ } else if (xType.IsNumericBased(Type.NumericPersuation.Real)) {
var lit = new LiteralExpr(x.tok, Basetypes.BigDec.ZERO);
- lit.Type = Type.Real; // resolve here
+ lit.Type = xType; // resolve here
yield return lit;
-
}
var missingBounds = new List<BoundVar>();
@@ -8436,16 +8443,24 @@ namespace Microsoft.Dafny {
Bpl.Expr prefixIsLess = Bpl.Expr.False;
for (int i = 0; i < k; i++) {
prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);
+ };
+
+ Bpl.Expr zero = null;
+ string zeroStr = null;
+ if (types0[k].IsNumericBased(Type.NumericPersuation.Int)) {
+ zero = Bpl.Expr.Literal(0);
+ zeroStr = "0";
+ } else if (types0[k].IsNumericBased(Type.NumericPersuation.Real)) {
+ zero = Bpl.Expr.Literal(Basetypes.BigDec.ZERO);
+ zeroStr = "0.0";
}
- if (types0[k] is IntType || types0[k] is RealType) {
- var zero = types0[k] is IntType ? Bpl.Expr.Literal(0) : Bpl.Expr.Literal(Basetypes.BigDec.ZERO);
+ if (zero != null) {
Bpl.Expr bounded = Bpl.Expr.Le(zero, ee1[k]);
for (int i = 0; i < k; i++) {
bounded = Bpl.Expr.Or(bounded, Less[i]);
}
string component = N == 1 ? "" : " (component " + k + ")";
- string zerostr = types0[k] is IntType ? "0" : "0.0";
- Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by " + zerostr + suffixMsg);
+ Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by " + zeroStr + suffixMsg);
builder.Add(cmd);
}
}
@@ -8473,10 +8488,12 @@ namespace Microsoft.Dafny {
u = u.NormalizeExpand();
if (t is BoolType) {
return u is BoolType;
- } else if (t is IntType) {
- return u is IntType;
- } else if (t is RealType) {
- return u is RealType;
+ } else if (t.IsNumericBased(Type.NumericPersuation.Int)) {
+ // we can allow different kinds of int-based types
+ return u.IsNumericBased(Type.NumericPersuation.Int);
+ } else if (t.IsNumericBased(Type.NumericPersuation.Real)) {
+ // we can allow different kinds of real-based types
+ return u.IsNumericBased(Type.NumericPersuation.Real);
} else if (t is SetType) {
return u is SetType;
} else if (t is SeqType) {
@@ -8532,9 +8549,9 @@ namespace Microsoft.Dafny {
eq = Bpl.Expr.Iff(e0, e1);
less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
atmost = Bpl.Expr.Imp(e0, e1);
- } else if (ty0 is IntType || ty0 is SeqType || ty0.IsDatatype) {
+ } else if (ty0.IsNumericBased(Type.NumericPersuation.Int) || ty0 is SeqType || ty0.IsDatatype) {
Bpl.Expr b0, b1;
- if (ty0 is IntType) {
+ if (ty0.IsNumericBased(Type.NumericPersuation.Int)) {
b0 = e0;
b1 = e1;
} else if (ty0 is SeqType) {
@@ -8549,12 +8566,12 @@ namespace Microsoft.Dafny {
eq = Bpl.Expr.Eq(b0, b1);
less = Bpl.Expr.Lt(b0, b1);
atmost = Bpl.Expr.Le(b0, b1);
- if (ty0 is IntType && includeLowerBound) {
+ if (ty0.IsNumericBased(Type.NumericPersuation.Int) && includeLowerBound) {
less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);
atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);
}
- } else if (ty0 is RealType) {
+ } else if (ty0.IsNumericBased(Type.NumericPersuation.Real)) {
eq = Bpl.Expr.Eq(e0, e1);
less = Bpl.Expr.Le(e0, Bpl.Expr.Sub(e1, Bpl.Expr.Literal(Basetypes.BigDec.FromInt(1))));
atmost = Bpl.Expr.Le(e0, e1);
@@ -10265,8 +10282,14 @@ namespace Microsoft.Dafny {
var e = (ConversionExpr)expr;
Bpl.ArithmeticCoercion.CoercionType ct;
if (e.ToType is IntType) {
+ if (e.E.Type.IsNumericBased(Type.NumericPersuation.Int)) {
+ return TrExpr(e.E);
+ }
ct = Bpl.ArithmeticCoercion.CoercionType.ToInt;
} else if (e.ToType is RealType) {
+ if (e.E.Type.IsNumericBased(Type.NumericPersuation.Real)) {
+ return TrExpr(e.E);
+ }
ct = Bpl.ArithmeticCoercion.CoercionType.ToReal;
} else {
Contract.Assert(false); // unexpected ConversionExpr to-type
@@ -10276,7 +10299,7 @@ namespace Microsoft.Dafny {
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
- bool isReal = e.E0.Type.IsRealType;
+ bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real);
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
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect
index 140aa890..196b3faa 100644
--- a/Test/dafny0/CoResolution.dfy.expect
+++ b/Test/dafny0/CoResolution.dfy.expect
@@ -19,6 +19,6 @@ CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only
CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not determined
-CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not determined
+CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined
+CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined
23 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
new file mode 100644
index 00000000..7a2249da
--- /dev/null
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -0,0 +1,38 @@
+// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type int32 = new int
+type posReal = new real
+type int8 = new int32
+
+method M()
+{
+ var k8 := new int8[100];
+ var s: set<int32>;
+ var x: posReal;
+ var y: posReal;
+ var z: int32;
+ x := 5.3;
+ z := 12;
+ s := {};
+ s := {40,20};
+ x := x + y;
+ var r0 := real(x);
+ var r1: real := 2.0 * r0;
+ var i0 := int(z);
+ var i1: nat := 2 * i0;
+ assert i1 == 24;
+ assert y == 0.0 ==> r1 == 10.6;
+
+ assert real(x) == r0;
+ assert 2.0 * real(x) == real(2.0 * x);
+
+ assert real(int(z)) == real(i0);
+ assert 2 * int(z) == int(2 * z);
+
+ var di: int32 := z / 2 + 24 / z;
+ assert di == 8;
+ y := 60.0;
+ var dr: posReal := y / 2.0 + 120.0 / y;
+ assert dr == 32.0;
+}
diff --git a/Test/dafny0/DerivedTypes.dfy.expect b/Test/dafny0/DerivedTypes.dfy.expect
new file mode 100644
index 00000000..33214760
--- /dev/null
+++ b/Test/dafny0/DerivedTypes.dfy.expect
@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled assembly into DerivedTypes.dll
diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
index 0c242db9..336a087a 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -23,5 +23,43 @@ module Goodies {
var s: set<int32>;
var x: posReal;
var y: posReal;
+ var z: int32;
+ x := 5.3;
+ z := 12;
+ s := {};
+ s := {40,20};
+ x := x + y;
+ var r0 := real(x);
+ var r1: real := 2.0 * r0;
+ var i0 := int(z);
+ var i1: nat := 2 * i0;
+ assert i1 == 24;
+ assert r1 == 10.6;
+ if x == r0 { // error: cannot compare posReal and real
+ } else if real(x) == r0 {
+ } else if i0 == int(x) {
+ } else if i0 == int(real(x)) {
+ } else if real(i0) == real(x) {
+ }
+ if z == i0 { // error: cannot compare int32 and int
+ } else if int(z) == i0 {
+ } else if r0 == real(z) {
+ } else if r0 == real(int(z)) {
+ } else if int(r0) == int(z) {
+ }
+ assert x == z; // error: cannot compare posReal and int32
+ assert x <= z; // error: cannot compare posReal and int32
+ assert z < i0; // error: cannot compare int32 and int
+ assert x > r1; // error: cannot compare posReal and real
+
+ var di := z % 2 - z / 2 + if z == 0 then 3 else 100 / z + 100 % z;
+ var dr := x / 2.0 + if x == 0.0 then 3.0 else 100.0 / x;
+ dr := dr % 3.0 + 3.0 % dr; // error: mod not supported for real-based types
+ z, x := di, dr;
+
+ var sq := [23, 50];
+ assert forall ii :: 0 <= ii < |sq| ==> sq[ii] == sq[ii];
+ var ms := multiset{23.0, 50.0};
+ assert forall rr :: 0.0 <= rr < 100.0 ==> ms[rr] == ms[rr];
}
}
diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
index 09b41101..4f86c813 100644
--- a/Test/dafny0/DerivedTypesResolution.dfy.expect
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -1,3 +1,11 @@
DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (derived types, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym
DerivedTypesResolution.dfy(12,7): Error: derived types must be based on some numeric type (got List<int>)
-2 resolution/type errors detected in DerivedTypesResolution.dfy
+DerivedTypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)
+DerivedTypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)
+DerivedTypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)
+DerivedTypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)
+DerivedTypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)
+DerivedTypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)
+DerivedTypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)
+DerivedTypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)
+10 resolution/type errors detected in DerivedTypesResolution.dfy
diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy.expect b/Test/dafny0/OpaqueFunctionsFail.dfy.expect
index 8c2638c3..a893c35e 100644
--- a/Test/dafny0/OpaqueFunctionsFail.dfy.expect
+++ b/Test/dafny0/OpaqueFunctionsFail.dfy.expect
@@ -1,4 +1,4 @@
-OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called.
-OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not determined
-OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called.
-3 resolution/type errors detected in OpaqueFunctionsFail.dfy
+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not be determined. If you are making an opaque function, make sure that the function can be called.
+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not be determined
+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not be determined. If you are making an opaque function, make sure that the function can be called.
+3 resolution/type errors detected in OpaqueFunctionsFail.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 3c9156dd..38f2f9c2 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -957,9 +957,9 @@ method TypeConversions(m: nat, i: int, r: real) returns (n: nat, j: int, s: real
s := (2.0 / 1.7) + (r / s) - (--r) * -12.3;
- s := real(s); // error: cannot convert real->real
- j := int(j); // error: cannot convert int->int
- j := int(n); // error: cannot convert nat->int
+ s := real(s); // fine (identity transform)
+ j := int(j); // fine (identity transform)
+ j := int(n); // fine (identity transform)
}
// --- filling in type arguments and checking that there aren't too many ---
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 4827dc07..cf1810e6 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -2,8 +2,8 @@ ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS
ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
-ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not determined
-ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not determined
+ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be determined
ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements
@@ -171,11 +171,8 @@ ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#
ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
-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)
ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-180 resolution/type errors detected in ResolutionErrors.dfy
+177 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect
index dfb4e978..04394d78 100644
--- a/Test/hofs/Underspecified.dfy.expect
+++ b/Test/hofs/Underspecified.dfy.expect
@@ -1,5 +1,5 @@
-Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not determined; please specify the type explicitly
-Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not determined; please specify the type explicitly
-Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not determined; please specify the type explicitly
-Underspecified.dfy(8,11): Error: type of bound variable 'a' could not determined; please specify the type explicitly
+Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not be determined; please specify the type explicitly
+Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not be determined; please specify the type explicitly
+Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not be determined; please specify the type explicitly
+Underspecified.dfy(8,11): Error: type of bound variable 'a' could not be determined; please specify the type explicitly
4 resolution/type errors detected in Underspecified.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 04:17:02 +0000