-
Notifications
You must be signed in to change notification settings - Fork 256
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Keep type synonyms in some special cases (#1086)
Co-authored-by: David Cok <[email protected]>
- Loading branch information
1 parent
27297d8
commit 5ed8716
Showing
4 changed files
with
122 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,107 @@ | ||
// RUN: %dafny /compile:0 "%s" > "%t" | ||
// RUN: %diff "%s.expect" "%t" | ||
|
||
// ----- example reported in Issue 623 | ||
|
||
module M1 { | ||
export Abs | ||
provides M, T | ||
export Conc | ||
provides M, MyClass | ||
reveals T | ||
|
||
class MyClass { | ||
} | ||
|
||
type T = MyClass | ||
|
||
lemma M(f: T ~> bool) | ||
requires forall t :: f.requires(t) ==> f(t) // regression test: this once crashed during checking of M2 | ||
{ } | ||
} | ||
|
||
module M2 { | ||
import M1`Abs | ||
|
||
method K(t: M1.T) { | ||
} | ||
} | ||
|
||
module M3 { | ||
import M1`Conc | ||
|
||
method K(t: M1.T) { | ||
} | ||
} | ||
|
||
// ----- example reported in Issue 150 | ||
|
||
module N1 { | ||
export | ||
provides T, Equal, Foo | ||
|
||
type T(==) = seq<real> | ||
|
||
predicate Equal(u: T, v: T) | ||
{ | ||
u == v | ||
} | ||
|
||
lemma Foo() | ||
ensures forall u, v :: Equal(u, v) ==> u == v // regression test: this once crashed during checking of N2 | ||
{ } | ||
} | ||
|
||
module N2 { | ||
import N1 | ||
|
||
lemma Bar(u: N1.T, v: N1.T) | ||
requires N1.Equal(u, v) | ||
{ | ||
N1.Foo(); | ||
assert u == v; | ||
} | ||
} | ||
|
||
|
||
// ------------------- additional examples | ||
|
||
module Library { | ||
export | ||
provides W, P, X, Q | ||
provides M0, M1 | ||
|
||
type W = MyTrait | ||
trait MyTrait { | ||
} | ||
predicate P(u: W) | ||
|
||
type X = MyClass | ||
class MyClass extends MyTrait { | ||
} | ||
predicate Q(x: X) | ||
|
||
lemma M0() | ||
requires forall t :: P(t) | ||
{ } | ||
lemma M1() | ||
requires forall t :: Q(t) | ||
{ } | ||
|
||
lemma Private0() | ||
requires forall t :: P(t) && Q(t) // error: t is inferred as MyTrait, so can't prove that Q(t) is well-formed | ||
{ } | ||
lemma Private1() | ||
requires forall t :: Q(t) && P(t) // error: t is inferred as MyTrait, so can't prove that Q(t) is well-formed | ||
{ } | ||
} | ||
|
||
module Client { | ||
import Library | ||
|
||
method K() | ||
requires forall t :: Library.P(t) | ||
requires forall t :: Library.Q(t) | ||
{ | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
git-issue-623.dfy(92,35): Error: the RHS value (a MyTrait) is not known to be an instance of the LHS type (MyClass) | ||
Execution trace: | ||
(0,0): anon0 | ||
git-issue-623.dfy(95,27): Error: the RHS value (a MyTrait) is not known to be an instance of the LHS type (MyClass) | ||
Execution trace: | ||
(0,0): anon0 | ||
|
||
Dafny program verifier finished with 3 verified, 2 errors |