diff options
| author |  leino <unknown> | 2014-07-02 13:24:34 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-07-02 13:24:34 -0700 |
| commit | c040550119028f43c8f6f6aead1844f88f2049a4 (patch) | |
| tree | dd39e03ceb86d1db023983d30ecd85803b941bf2 /Test/dafny0/TypeParameters.dfy | |
| parent | 0bcef90b3cadb13d7cebd4394ff8bf51e95015e7 (diff) | |
Allow array-type parameters to be filled in automatically.
Enhanced filling in of datatype parameters: allow places that need only a prefix of the parameters of the datatype
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 963916f0..900b6110 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -321,3 +321,35 @@ method IdentityMap(s: set<Pair>) returns (m: map) m, s := m[p.0 := p.1], s - {p};
}
}
+
+// -------------- auto filled-in type arguments for array types ------
+
+module ArrayTypeMagic {
+ method M(a: array2)
+ {
+ }
+
+ method F(b: array) returns (s: seq)
+ requires b != null;
+ {
+ return b[..];
+ }
+
+ datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)
+ datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)
+ datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)
+
+ function G(t: ArrayCubeTree): array3
+ {
+ match t
+ case Leaf(d) => d
+ case Node(l, _) => G(l)
+ }
+
+ datatype Nat = Zero | Succ(Nat)
+
+ datatype List<T> = Nil | Cons(T, List)
+
+ datatype Cell<T> = Mk(T)
+ datatype DList<T,U> = Nil(Cell) | Cons(T, U, DList)
+}
|