summaryrefslogtreecommitdiff
path: root/Test/dafny0/Coinductive.dfy
blob: 431d6bb19ad44106fab62a5550272e88d47334b3 (plain)
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
// --------------------------------------------------

module TestInductiveDatatypes
{
  // The following types test for cycles that go via instantiated type arguments

  datatype Record<T> = Ctor(T);

  datatype RecInt = Ctor(Record<int>);  // this is fine
  datatype Rec_Forever = Ctor(Record<Rec_Forever>);  // error
  datatype Rec_Stops = Cons(Record<Rec_Stops>, Rec_Stops) | Nil;  // this is okay

  datatype D<T> = Ctor(E<D<T>>);  // error: illegal cycle
  datatype E<T> = Ctor(T);

  // the following is okay
  datatype MD<T> = Ctor(ME<T>);
  datatype ME<T> = Ctor(T);
  method M()
  {
    var d: MD<MD<int>>;
  }

  datatype A = Ctor(B);  // superficially looks like a cycle, but can still be constructed
  datatype B = Ctor(List<A>);
  datatype List<T> = Nil | Cons(T, List);
}

module MoreInductive {
  datatype Tree<G> = Node(G, List<Tree<G>>);
  datatype List<T> = Nil | Cons(T, List<T>);

  datatype M = All(List<M>);
  datatype H<'a> = HH('a, Tree<'a>);
  datatype K<'a> = KK('a, Tree<K<'a>>);  // error
  datatype L<'a> = LL('a, Tree<List<L<'a>>>);
}

// --------------------------------------------------

module TestCoinductiveDatatypes
{
  codatatype InfList<T> = Done | Continue(T, InfList);

  codatatype Stream<T> = More(T, Stream<T>);

  codatatype BinaryTreeForever<T> = BNode(val: T, left: BinaryTreeForever<T>, right: BinaryTreeForever<T>);

  datatype List<T> = Nil | Cons(T, List);

  codatatype BestBushEver<T> = Node(value: T, branches: List<BestBushEver<T>>);

  codatatype LazyRecord<T> = Lazy(contents: T);
  class MyClass<T> { }
  datatype GenericDt<T> = Blue | Green(T);
  datatype GenericRecord<T> = Rec(T);

  datatype FiniteEnough_Class = Ctor(MyClass<FiniteEnough_Class>);
  datatype FiniteEnough_Co = Ctor(LazyRecord<FiniteEnough_Co>);
  datatype FiniteEnough_Dt = Ctor(GenericDt<FiniteEnough_Dt>);  // fine
  datatype NotFiniteEnough_Dt = Ctor(GenericRecord<NotFiniteEnough_Dt>);  // error

}

// --------------- CoPredicates --------------------------

module CoPredicateResolutionErrors {

  codatatype Stream<T> = StreamCons(head: T, tail: Stream);

  function Upward(n: int): Stream<int>
  {
    StreamCons(n, Upward(n + 1))
  }

  function Doubles(n: int): Stream<int>
  {
    StreamCons(2*n, Doubles(n + 1))
  }

  copredicate Pos(s: Stream<int>)
  {
    0 < s.head && Pos(s.tail) && Even(s)
  }

  copredicate Even(s: Stream<int>)
  {
    s.head % 2 == 0 && Even(s.tail)
    && (s.head == 17 ==> Pos(s))
    && (Pos(s) ==> s.head == 17)  // error: cannot make recursive copredicate call in negative position
    && !Even(s)  // error: cannot make recursive copredicate call in negative position
    && (Even(s) <==> Even(s))  // error (x2): recursive copredicate calls allowed only in positive positions
  }

  copredicate Another(s: Stream<int>)
  {
    !Even(s)  // here, negation is fine
  }

  ghost method Lemma(n: int)
    ensures Even(Doubles(n));
  {
  }
}

// --------------------------------------------------