diff options
| author |  Rustan Leino <unknown> | 2014-03-21 23:00:28 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-03-21 23:00:28 -0700 |
| commit | 49cd5fd19facf9acce19fc193e381feec8ff82e8 (patch) | |
| tree | c921eb12b1a44309649d2aefae3fb7f60339a41f /Test/dafny0/TypeParameters.dfy | |
| parent | b517eb9ade15aa3eed8362c30a202d1ccdc341a8 (diff) | |
Auto-set type arguments of built-in collection types, just like for user-defined types.
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 705961a0..f2f68a96 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -267,3 +267,54 @@ ghost method ammeLtsiL_int(xs: List<int>, ys: List<int>) {
assert forall x :: InList(x, xs) ==> InList(x, ys);
}
+
+// -------------- auto filled-in type arguments for collection types ------
+
+function length(xs: List): nat
+{
+ match xs
+ case Nil => 0
+ case Cons(_, tail) => 1 + length(tail)
+}
+
+function elems(xs: List): set
+{
+ match xs
+ case Nil => {}
+ case Cons(x, tail) => {x} + elems(tail)
+}
+
+function Card(s: set): nat
+{
+ |s|
+}
+
+function Identity(s: set): set
+{
+ s
+}
+
+function MultisetToSet(m: multiset): set
+{
+ if |m| == 0 then {} else
+ var x :| x in m; MultisetToSet(m - multiset{x}) + {x}
+}
+
+function SeqToSet(q: seq): set
+{
+ if q == [] then {} else {q[0]} + SeqToSet(q[1..])
+}
+
+datatype Pair<T(==),U(==)> = MkPair(0: T, 1: U)
+
+method IdentityMap(s: set<Pair>) returns (m: map)
+{
+ m := map[];
+ var s := s;
+ while s != {}
+ decreases s;
+ {
+ var p :| p in s;
+ m, s := m[p.0 := p.1], s - {p};
+ }
+}
|