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
|
// --------------------------------------------------
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
}
// --------------------------------------------------
|
