diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-05-01 14:49:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-05-01 14:49:41 -0700 |
| commit | 9266a3c8da8825816bfd2b31aca9cec8aae0c455 (patch) | |
| tree | e87903cb141450e57b976c4dfca7057c2dbefb9a /Test/dafny0/Compilation.dfy | |
| parent | bdf8ac6927bac67364dbc16422aa4d197c7f6e25 (diff) | |
Dafny: added support for co-recursive calls
Diffstat (limited to 'Test/dafny0/Compilation.dfy')
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 62 |
1 files changed, 54 insertions, 8 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 301a4e94..bf21432f 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -1,13 +1,59 @@ // The tests in this file are designed to run through the compiler. They contain
// program snippets that are tricky to compile or whose compilation once was buggy.
-datatype MyDt<T> = Nil | Cons(T, MyDt<T>);
-
-method M<U>(x: MyDt<int>)
-{
- match (x) {
- case Cons(head, tail) =>
- var y: int := head;
- case Nil =>
+module OnceBuggy {
+ datatype MyDt<T> = Nil | Cons(T, MyDt<T>);
+
+ method M<U>(x: MyDt<int>)
+ {
+ match (x) {
+ case Cons(head, tail) =>
+ var y: int := head;
+ case Nil =>
+ }
+ }
+}
+
+// --------------------------------------------------
+
+module CoRecursion {
+ codatatype Stream<T> = More(head: T, rest: Stream);
+
+ function method AscendingChain(n: int): Stream<int>
+ {
+ More(n, AscendingChain(n+1))
+ }
+
+ datatype List<T> = Nil | Cons(car: T, cdr: List);
+
+ function method Prefix(n: nat, s: Stream): List
+ {
+ if n == 0 then Nil else
+ Cons(s.head, Prefix(n-1, s.rest))
+ }
+
+ class Cell { var data: int; }
+
+ // When run, the following method should print
+ // 400
+ // 320
+ // 40
+ // 41
+ // 42
+ method Main() {
+ var m := 17;
+ var cell := new Cell;
+ cell.data := 40;
+ var mr := More(400, More(320, AscendingChain(cell.data)));
+ m := 30;
+ cell.data := 60;
+ var l := Prefix(5, mr);
+ while (l != Nil)
+ decreases l;
+ {
+ match (l) { case Cons(x,y) => }
+ print l.car, "\n";
+ l := l.cdr;
+ }
}
}
|