summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl36
-rw-r--r--Source/Dafny/DafnyAst.cs4
-rw-r--r--Source/Dafny/Resolver.cs7
-rw-r--r--Source/Dafny/Translator.cs35
4 files changed, 70 insertions, 12 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 561a29a1..7c8a9db8 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -20,12 +20,17 @@ const null: ref;
type Set T = [T]bool;
+function Set#Card<T>(Set T): int;
+axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
+
function Set#Empty<T>(): Set T;
axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
+axiom (forall<T> s: Set T :: { Set#Card(s) } Set#Card(s) == 0 <==> s == Set#Empty());
function Set#Singleton<T>(T): Set T;
axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
+axiom (forall<T> r: T :: { Set#Card(Set#Singleton(r)) } Set#Card(Set#Singleton(r)) == 1);
function Set#UnionOne<T>(Set T, T): Set T;
axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
@@ -34,6 +39,10 @@ axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
Set#UnionOne(a, x)[x]);
axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
a[y] ==> Set#UnionOne(a, x)[y]);
+axiom (forall<T> a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) }
+ a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
+axiom (forall<T> a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) }
+ !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
function Set#Union<T>(Set T, Set T): Set T;
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
@@ -46,6 +55,9 @@ axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
Set#Disjoint(a, b) ==>
Set#Difference(Set#Union(a, b), a) == b &&
Set#Difference(Set#Union(a, b), b) == a);
+axiom (forall<T> a, b: Set T :: { Set#Card(Set#Union(a, b)) }
+ Set#Disjoint(a, b) ==>
+ Set#Card(Set#Union(a, b)) == Set#Card(a) + Set#Card(b));
function Set#Intersection<T>(Set T, Set T): Set T;
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
@@ -104,9 +116,15 @@ function $IsGoodMultiSet<T>(ms: MultiSet T): bool;
// ints are non-negative, used after havocing, and for conversion from sequences to multisets.
axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) }
$IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));
+
+function MultiSet#Card<T>(MultiSet T): int;
+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
+axiom (forall<T> s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }
+ 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n);
function MultiSet#Empty<T>(): MultiSet T;
axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } MultiSet#Card(s) == 0 <==> s == MultiSet#Empty());
function MultiSet#Singleton<T>(T): MultiSet T;
axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&
@@ -126,12 +144,17 @@ axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
// other elements unchanged
axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);
+axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#Card(MultiSet#UnionOne(a, x)) }
+ MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
+
function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;
// union-ing is the sum of the contents
axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] }
MultiSet#Union(a,b)[o] == a[o] + b[o]);
-
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Card(MultiSet#Union(a,b)) }
+ MultiSet#Card(MultiSet#Union(a,b)) == MultiSet#Card(a) + MultiSet#Card(b));
+
// two containment axioms
axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }
0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);
@@ -181,6 +204,8 @@ function MultiSet#FromSet<T>(Set T): MultiSet T;
axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }
(MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&
(MultiSet#FromSet(s)[a] == 1 <==> s[a]));
+axiom (forall<T> s: Set T :: { MultiSet#Card(MultiSet#FromSet(s)) }
+ MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));
// conversion to a multiset, from a sequence.
function MultiSet#FromSeq<T>(Seq T): MultiSet T;
@@ -370,10 +395,14 @@ type Map U V;
function Map#Domain<U, V>(Map U V): [U] bool;
function Map#Elements<U, V>(Map U V): [U]V;
+function Map#Card<U, V>(Map U V): int;
+axiom (forall<U, V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
+
function Map#Empty<U, V>(): Map U V;
axiom (forall<U, V> u: U ::
{ Map#Domain(Map#Empty(): Map U V)[u] }
!Map#Domain(Map#Empty(): Map U V)[u]);
+axiom (forall<U, V> m: Map U V :: { Map#Card(m) } Map#Card(m) == 0 <==> m == Map#Empty());
function Map#Glue<U, V>([U] bool, [U]V): Map U V;
axiom (forall<U, V> a: [U] bool, b:[U]V ::
@@ -396,6 +425,11 @@ axiom (forall<U, V> m: Map U V, u: U, u': U, v: V ::
Map#Elements(Map#Build(m, u, v))[u'] == v) &&
(u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] &&
Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));
+axiom (forall<U, V> m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }
+ Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
+axiom (forall<U, V> m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }
+ !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
+
//equality for maps
function Map#Equal<U, V>(Map U V, Map U V): bool;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 678c200e..6feaae60 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -724,7 +724,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// This proxy stands for:
- /// set(Arg) or seq(Arg) or map(Arg, Range)
+ /// set(Arg) or multiset(Arg) or seq(Arg) or map(Arg, Range)
/// </summary>
public class CollectionTypeProxy : RestrictedTypeProxy {
public readonly Type Arg;
@@ -765,7 +765,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// This proxy stands for:
- /// seq(Arg) or array(Arg) or map(Arg, Range)
+ /// seq(Arg) or array(Arg) or multiset(Arg) map(Arg, Range)
/// </summary>
public class IndexableTypeProxy : RestrictedTypeProxy {
public readonly Type Arg, Domain;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5219be3f..fcc74eda 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5198,8 +5198,9 @@ namespace Microsoft.Dafny
expr.Type = elType;
break;
case UnaryExpr.Opcode.SeqLength:
- if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
- Error(expr, "length operator expects a sequence argument (instead got {0})", e.E.Type);
+
+ if (!UnifyTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy()))) {
+ Error(expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
}
expr.Type = Type.Int;
break;
@@ -5314,7 +5315,7 @@ namespace Microsoft.Dafny
case BinaryExpr.Opcode.In:
case BinaryExpr.Opcode.NotIn:
if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type))) {
- Error(expr, "second argument to \"{0}\" must be a set or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
+ Error(expr, "second argument to \"{0}\" must be a set, multiset or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
}
expr.Type = Type.Bool;
break;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3d4e8a98..e3f38aa9 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3164,8 +3164,9 @@ namespace Microsoft.Dafny {
if (e.Op == UnaryExpr.Opcode.SetChoose) {
Bpl.Expr emptySet = FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E), emptySet), "choose is defined only on nonempty sets"));
- } else if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
- CheckNonNull(expr.tok, e.E, builder, etran, options.AssertKv);
+ // Nadia: why was this here? Is it supposed to work for arrays?
+ //} else if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ // CheckNonNull(expr.tok, e.E, builder, etran, options.AssertKv);
}
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
@@ -7680,8 +7681,16 @@ namespace Microsoft.Dafny {
case UnaryExpr.Opcode.SeqLength:
if (e.E.Type is SeqType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
+ } else if (e.E.Type is SetType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SetCard, null, arg);
+ } else if (e.E.Type is MultiSetType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetCard, null, arg);
+ } else if (e.E.Type is MapType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MapCard, null, arg);
} else {
- return translator.ArrayLength(expr.tok, arg, 1, 0);
+ // Nadia: why was this here? Is it supposed to work for arrays?
+ //return translator.ArrayLength(expr.tok, arg, 1, 0);
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected sized type
}
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
@@ -8392,6 +8401,7 @@ namespace Microsoft.Dafny {
enum BuiltinFunction
{
+ SetCard,
SetEmpty,
SetUnionOne,
SetUnion,
@@ -8400,8 +8410,9 @@ namespace Microsoft.Dafny {
SetEqual,
SetSubset,
SetDisjoint,
- SetChoose,
+ SetChoose,
+ MultiSetCard,
MultiSetEmpty,
MultiSetUnionOne,
MultiSetUnion,
@@ -8411,7 +8422,7 @@ namespace Microsoft.Dafny {
MultiSetSubset,
MultiSetDisjoint,
MultiSetFromSet,
- MultiSetFromSeq,
+ MultiSetFromSeq,
IsGoodMultiSet,
SeqLength,
@@ -8427,6 +8438,7 @@ namespace Microsoft.Dafny {
SeqSameUntil,
SeqFromArray,
+ MapCard,
MapDomain,
MapElements,
MapEqual,
@@ -8472,6 +8484,10 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
switch (f) {
+ case BuiltinFunction.SetCard:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "Set#Card", Bpl.Type.Int, args);
case BuiltinFunction.SetEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
@@ -8511,7 +8527,10 @@ namespace Microsoft.Dafny {
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Choose", typeInstantiation, args);
-
+ case BuiltinFunction.MultiSetCard:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Card", Bpl.Type.Int, args);
case BuiltinFunction.MultiSetEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
@@ -8615,6 +8634,10 @@ namespace Microsoft.Dafny {
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);
+ case BuiltinFunction.MapCard:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "Map#Card", Bpl.Type.Int, args);
case BuiltinFunction.MapDomain:
Contract.Assert(args.Length == 1);
return FunctionCall(tok, "Map#Domain", typeInstantiation, args);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 19:26:05 +0000