diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-25 16:37:12 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-25 16:37:12 -0700 |
| commit | a732a632287074e74a1dd394149b36e83526a0cf (patch) | |
| tree | 9770cb8127d4bf9d8348a5da54922d32f3d29fdb /Test/dafny0/Coinductive.dfy | |
| parent | 032662d0adb823376b1abd49a0c46ba3276f8721 (diff) | |
Dafny: fixed resolution bug for inductive datatypes (previous check did not handle generic datatypes correctly)
Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code)
Dafny: added "codatatype" declaration (syntax only for now)
Diffstat (limited to 'Test/dafny0/Coinductive.dfy')
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy new file mode 100644 index 00000000..fdb8c06b --- /dev/null +++ b/Test/dafny0/Coinductive.dfy @@ -0,0 +1,55 @@ +// --------------------------------------------------
+
+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 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
+
+}
+
+// --------------------------------------------------
|