From b20306de5978493dd2096bcc884ea0ec2de6f9c2 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Fri, 15 Jul 2011 14:52:19 -0700 Subject: Added compilation support for multisets and sequences from arrays. --- Binaries/DafnyRuntime.cs | 148 ++++++++++++++++++++++++++++++++++++++++++++++- Source/Dafny/Compiler.cs | 66 +++++++++++++++++---- 2 files changed, 203 insertions(+), 11 deletions(-) diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index c03ac643..82de380d 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -132,11 +132,154 @@ namespace Dafny return default(T); } } + public class MultiSet + { + Dictionary dict; + public MultiSet() { } + MultiSet(Dictionary d) { + dict = d; + } + public static MultiSet Empty { + get { + return new MultiSet(new Dictionary(0)); + } + } + public static MultiSet FromElements(params T[] values) { + Dictionary d = new Dictionary(values.Length); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d); + } + public static MultiSet FromCollection(ICollection values) { + Dictionary d = new Dictionary(); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d); + } + public static MultiSet FromSeq(Sequence values) { + Dictionary d = new Dictionary(); + foreach (T t in values.Elements) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d); + } + public static MultiSet FromSet(Set values) { + Dictionary d = new Dictionary(); + foreach (T t in values.Elements) { + d[t] = 1; + } + return new MultiSet(d); + } + + public bool Equals(MultiSet other) { + return other.IsSubsetOf(this) && this.IsSubsetOf(other); + } + public override bool Equals(object other) { + return other is MultiSet && Equals((MultiSet)other); + } + public override int GetHashCode() { + return dict.GetHashCode(); + } + public bool IsProperSubsetOf(MultiSet other) { + return !Equals(other) && IsSubsetOf(other); + } + public bool IsSubsetOf(MultiSet other) { + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) + return false; + } + return true; + } + public bool IsSupersetOf(MultiSet other) { + return other.IsSubsetOf(this); + } + public bool IsProperSupersetOf(MultiSet other) { + return other.IsProperSubsetOf(this); + } + public bool IsDisjointFrom(MultiSet other) { + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) + return false; + } + foreach (T t in other.dict.Keys) { + if (dict.ContainsKey(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return dict.ContainsKey(t); + } + public MultiSet Union(MultiSet other) { + if (dict.Count == 0) + return other; + else if (other.dict.Count == 0) + return this; + var r = new Dictionary(); + foreach (T t in dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + dict[t]; + } + foreach (T t in other.dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + other.dict[t]; + } + return new MultiSet(r); + } + public MultiSet Intersect(MultiSet other) { + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return other; + var r = new Dictionary(); + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) { + r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]); + } + } + return new MultiSet(r); + } + public MultiSet Difference(MultiSet other) { // \result == this - other + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return this; + var r = new Dictionary(); + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t)) { + r.Add(t, dict[t]); + } else if (other.dict[t] < dict[t]) { + r.Add(t, dict[t] - other.dict[t]); + } + } + return new MultiSet(r); + } + } public class Sequence { T[] elmts; public Sequence() { } - Sequence(T[] ee) { + public Sequence(T[] ee) { elmts = ee; } public static Sequence Empty { @@ -303,5 +446,8 @@ namespace Dafny return c.IsZero ? c : BigInteger.Subtract(bp, c); } } + public static Sequence SeqFromArray(T[] array) { + return new Sequence(array); + } } } diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index d61d653d..6fa9440a 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -483,8 +483,9 @@ namespace Microsoft.Dafny { } // ----- Type --------------------------------------------------------------------------------- - + readonly string DafnySetClass = "Dafny.Set"; + readonly string DafnyMultiSetClass = "Dafny.MultiSet"; readonly string DafnySeqClass = "Dafny.Sequence"; string TypeName(Type type) @@ -541,6 +542,12 @@ namespace Microsoft.Dafny { Error("compilation of seq is not supported; consider introducing a ghost"); } return DafnySeqClass + "<" + TypeName(argType) + ">"; + } else if (type is MultiSetType) { + Type argType = ((MultiSetType)type).Arg; + if (argType is ObjectType) { + Error("compilation of seq is not supported; consider introducing a ghost"); + } + return DafnyMultiSetClass + "<" + TypeName(argType) + ">"; } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } @@ -607,6 +614,8 @@ namespace Microsoft.Dafny { return "default(@" + udt.Name + ")"; } else if (type is SetType) { return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty"; + } else if (type is MultiSetType) { + return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)type).Arg) + ">.Empty"; } else if (type is SeqType) { return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty"; } else { @@ -1186,12 +1195,18 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) { IdentifierExpr e = (IdentifierExpr)expr; wr.Write("@" + e.Var.Name); - + } else if (expr is SetDisplayExpr) { SetDisplayExpr e = (SetDisplayExpr)expr; Type elType = cce.NonNull((SetType)e.Type).Arg; wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType)); TrExprList(e.Elements); + + } else if (expr is MultiSetDisplayExpr) { + MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr; + Type elType = cce.NonNull((MultiSetType)e.Type).Arg; + wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType)); + TrExprList(e.Elements); } else if (expr is SeqDisplayExpr) { SeqDisplayExpr e = (SeqDisplayExpr)expr; @@ -1214,18 +1229,29 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - TrParenExpr(e.Seq); Contract.Assert(e.Seq.Type != null); if (e.Seq.Type.IsArrayType) { - Contract.Assert(e.SelectOne); - Contract.Assert(e.E0 != null && e.E1 == null); - wr.Write("[(int)"); - TrParenExpr(e.E0); - wr.Write("]"); + if (e.SelectOne) { + Contract.Assert(e.E0 != null && e.E1 == null); + TrParenExpr(e.Seq); + wr.Write("[(int)"); + TrParenExpr(e.E0); + wr.Write("]"); + } else { + TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq); + if (e.E1 != null) { + TrParenExpr(".Take", e.E1); + } + if (e.E0 != null) { + TrParenExpr(".Drop", e.E0); + } + } } else if (e.SelectOne) { Contract.Assert(e.E0 != null && e.E1 == null); + TrParenExpr(e.Seq); TrParenExpr(".Select", e.E0); } else { + TrParenExpr(e.Seq); if (e.E1 != null) { TrParenExpr(".Take", e.E1); } @@ -1233,7 +1259,16 @@ namespace Microsoft.Dafny { TrParenExpr(".Drop", e.E0); } } - + } else if (expr is MultiSetFormingExpr) { + MultiSetFormingExpr e = (MultiSetFormingExpr)expr; + wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(((CollectionType)e.E.Type).Arg)); + if (e.E.Type is SeqType) { + TrParenExpr(".FromSeq", e.E); + } else if (e.E.Type is SetType) { + TrParenExpr(".FromSet", e.E); + } else { + Contract.Assert(false); throw new cce.UnreachableException(); + } } else if (expr is MultiSelectExpr) { MultiSelectExpr e = (MultiSelectExpr)expr; TrParenExpr(e.Array); @@ -1389,29 +1424,37 @@ namespace Microsoft.Dafny { wr.Write(")"); break; case BinaryExpr.ResolvedOpcode.SetEq: + case BinaryExpr.ResolvedOpcode.MultiSetEq: case BinaryExpr.ResolvedOpcode.SeqEq: callString = "Equals"; break; case BinaryExpr.ResolvedOpcode.SetNeq: + case BinaryExpr.ResolvedOpcode.MultiSetNeq: case BinaryExpr.ResolvedOpcode.SeqNeq: preOpString = "!"; callString = "Equals"; break; - case BinaryExpr.ResolvedOpcode.ProperSubset: + case BinaryExpr.ResolvedOpcode.ProperMultiSubset: callString = "IsProperSubsetOf"; break; case BinaryExpr.ResolvedOpcode.Subset: + case BinaryExpr.ResolvedOpcode.MultiSubset: callString = "IsSubsetOf"; break; case BinaryExpr.ResolvedOpcode.Superset: + case BinaryExpr.ResolvedOpcode.MultiSuperset: callString = "IsSupersetOf"; break; case BinaryExpr.ResolvedOpcode.ProperSuperset: + case BinaryExpr.ResolvedOpcode.ProperMultiSuperset: callString = "IsProperSupersetOf"; break; case BinaryExpr.ResolvedOpcode.Disjoint: + case BinaryExpr.ResolvedOpcode.MultiSetDisjoint: callString = "IsDisjointFrom"; break; case BinaryExpr.ResolvedOpcode.InSet: + case BinaryExpr.ResolvedOpcode.InMultiSet: TrParenExpr(e.E1); wr.Write(".Contains("); TrExpr(e.E0); wr.Write(")"); break; case BinaryExpr.ResolvedOpcode.NotInSet: + case BinaryExpr.ResolvedOpcode.NotInMultiSet: wr.Write("!"); TrParenExpr(e.E1); wr.Write(".Contains("); @@ -1419,10 +1462,13 @@ namespace Microsoft.Dafny { wr.Write(")"); break; case BinaryExpr.ResolvedOpcode.Union: + case BinaryExpr.ResolvedOpcode.MultiSetUnion: callString = "Union"; break; case BinaryExpr.ResolvedOpcode.Intersection: + case BinaryExpr.ResolvedOpcode.MultiSetIntersection: callString = "Intersect"; break; case BinaryExpr.ResolvedOpcode.SetDifference: + case BinaryExpr.ResolvedOpcode.MultiSetDifference: callString = "Difference"; break; case BinaryExpr.ResolvedOpcode.ProperPrefix: -- cgit v1.2.3