diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-19 10:30:44 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-19 10:30:44 -0700 |
| commit | 78e74bf9fa5ad7175cafd171427f58f556256e4a (patch) | |
| tree | b3f22b3584fccb470d14da61a8aa001562310455 | |
| parent | 5e7d03fba113642aa1d6b181a854c684c740979e (diff) | |
Fix type inference bug in data rank comparison when one side can be a TypeVar
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 10 | ||||
| -rw-r--r-- | Test/hofs/Fold.dfy | 2 |
3 files changed, 10 insertions, 6 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index abfc7835..08d05fab 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1068,8 +1068,10 @@ namespace Microsoft.Dafny { /// </summary>
public class DatatypeProxy : RestrictedTypeProxy {
public readonly bool Co; // false means only inductive datatypes; true means only co-inductive datatypes
- public DatatypeProxy(bool co) {
+ public readonly bool TypeVariableOK;
+ public DatatypeProxy(bool co, bool typeVariableOk = false) {
Co = co;
+ TypeVariableOK = typeVariableOk;
}
public override int OrderID {
get {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 60f40784..172f63ad 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4239,6 +4239,8 @@ namespace Microsoft.Dafny // all is fine, proxy can be redirected to t
} else if (dtp.Co && t.IsCoDatatype) {
// all is fine, proxy can be redirected to t
+ } else if (dtp.TypeVariableOK && t.IsTypeParameter) {
+ // looking good
} else {
return false;
}
@@ -6675,14 +6677,14 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add: {
if (e.Op == BinaryExpr.Opcode.Lt && (e.E0.Type.NormalizeExpand().IsIndDatatype || e.E0.Type.IsTypeParameter)) {
- if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
+ if (UnifyTypes(e.E1.Type, new DatatypeProxy(false, 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.NormalizeExpand().IsIndDatatype) {
- if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
+ if (UnifyTypes(e.E0.Type, new DatatypeProxy(false, true))) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
} else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
@@ -6712,14 +6714,14 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge: {
if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.NormalizeExpand().IsIndDatatype) {
- if (UnifyTypes(e.E1.Type, new DatatypeProxy(false)) || e.E1.Type.IsTypeParameter) {
+ if (UnifyTypes(e.E1.Type, new DatatypeProxy(false, true))) {
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.NormalizeExpand().IsIndDatatype || e.E1.Type.IsTypeParameter)) {
- if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
+ if (UnifyTypes(e.E0.Type, new DatatypeProxy(false, false))) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
} else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy index df7d0126..7ce99e56 100644 --- a/Test/hofs/Fold.dfy +++ b/Test/hofs/Fold.dfy @@ -15,7 +15,7 @@ function method Eval(e : Expr): int function method Fold(xs : List<A>, unit : B, f : (A,B) -> B): B reads f.reads; - requires forall x : A, y: B :: x < xs ==> f.requires(x,y); + requires forall x, y :: x < xs ==> f.requires(x,y); { match xs case Nil => unit |