forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
git-issue-4939.dfy
148 lines (120 loc) · 3.17 KB
/
git-issue-4939.dfy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
// RUN: %exits-with 2 %verify --type-system-refresh --general-traits=datatype "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module FromIssue0 {
trait Program {
method Compute() returns (r: Result)
}
datatype Result =
| Bounce(next: Program)
| Done()
datatype Trivial extends Program =
Trivial()
{
method Compute() returns (r: Result) {
return Done();
}
}
datatype Seq extends Program =
Seq(left: Program, right: Program) // this once gave an error, saying Seq is empty because of cyclic dependencies
{
method Compute() returns (r: Result) {
var result := left.Compute();
match result
case Done() => r := right.Compute();
case Bounce(next) =>
var next' := Seq(next, right);
assert next' is Program;
return Bounce(next');
}
}
}
module FromIssue1 {
trait Program {
}
datatype Trivial extends Program =
Trivial()
datatype Seq extends Program =
Seq(left: Program, right: Program) // this once gave an error, saying Seq is empty because of cyclic dependencies
}
module FromIssue2 {
// NoInstances has no instances
class NoInstances {
constructor ()
requires false
{
}
}
// ... and therefore, neither does D. However, this is not detected syntactically, so there are no complaints.
datatype D = D(n: NoInstances)
}
module FromIssue3 {
trait Interface {
function getString(i: int): string
}
datatype Wrapper extends Interface = Wrapper(inner: Interface) // this once gave the cyclic-dependency error
{
function getString(i: int): string {
inner.getString(i+1)
}
}
datatype DetectZero extends Interface = DetectZero
{
function getString(i: int): string {
if i == 0
then "zero"
else "I don't know"
}
}
function getWrappedDetectZero(): Interface {
Wrapper(DetectZero)
}
}
module FromIssue4 {
trait Interface {
function GetString(i: int): string
}
class {:extern} Store {
var interface: Interface
constructor (interface: Interface) {
this.interface := interface;
}
function GetInterface(): (res: Interface)
ensures res == interface
}
datatype Wrapper extends Interface = Wrapper(inner: Store)
{
function GetString(i: int): string {
inner.GetInterface().GetString(i + 1)
}
}
}
module SimpleExample0 {
trait GeneralTrait {
function F(): int { 5 }
}
datatype Wrapper = Wrapper(g: GeneralTrait) // this once gave the cyclic-dependency error
}
module SimpleExample1 {
trait GeneralTrait extends object {
function F(): int { 5 }
}
datatype Wrapper = Wrapper(g: GeneralTrait) // this was always fine
}
module Standard {
datatype List<X> = Nil | Cons(X, List<X>)
datatype Op = Plus | Times
datatype Expr = Value(int) | Node(operator: Op, arguments: List<Expr>)
}
module Good0 {
datatype Mutual = M0(Nutual) | M1(Mutual)
datatype Nutual = N0(Mutual) | Easy
}
module Good1 {
datatype Nutual = N0(Mutual) | Easy
datatype Mutual = M0(Nutual) | M1(Mutual)
}
module Bad {
datatype T = Make(T, T) // error: obviously empty
datatype Mutual = M0(Nutual) | M1(Mutual) // error: empty
datatype Nutual = N0(Mutual) // error: empty
}