From 57a7fa3aa01ced1943dde6fe3270c62f1b6923c3 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 31 May 2012 17:13:35 -0700 Subject: Dafny: Added map comprehensions and updated display syntax --- Binaries/DafnyPrelude.bpl | 9 ++++ Binaries/DafnyRuntime.cs | 36 +++++++++++++++- Source/Dafny/Compiler.cs | 74 ++++++++++++++++++++++++++++++++ Source/Dafny/Dafny.atg | 22 ++++++++-- Source/Dafny/DafnyAst.cs | 18 +++++++- Source/Dafny/Parser.cs | 50 +++++++++++++-------- Source/Dafny/Printer.cs | 18 ++++++++ Source/Dafny/RefinementTransformer.cs | 2 + Source/Dafny/Resolver.cs | 39 +++++++++++++++++ Source/Dafny/Translator.cs | 76 ++++++++++++++++++++++++++------ Test/dafny0/Answer | 2 +- Test/dafny0/Maps.dfy | 81 ++++++++++++++++++++++++++--------- 12 files changed, 367 insertions(+), 60 deletions(-) diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 09b6efcf..742fd4e4 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -371,6 +371,15 @@ axiom (forall u: U :: { Map#Domain(Map#Empty(): Map U V)[u] } !Map#Domain(Map#Empty(): Map U V)[u]); +function Map#Glue([U] bool, [U]V): Map U V; +axiom (forall a: [U] bool, b:[U]V :: + { Map#Domain(Map#Glue(a, b)) } + Map#Domain(Map#Glue(a, b)) == a); +axiom (forall a: [U] bool, b:[U]V :: + { Map#Elements(Map#Glue(a, b)) } + Map#Elements(Map#Glue(a, b)) == b); + + //Build is used in displays, and for map updates function Map#Build(Map U V, U, V): Map U V; /*axiom (forall m: Map U V, u: U, v: V :: diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 67669245..f7eecfc5 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -274,6 +274,19 @@ namespace Dafny } return new MultiSet(r); } + public IEnumerable Elements { + get { + List l = new List(); + foreach (T t in dict.Keys) { + int n; + dict.TryGetValue(t, out n); + for (int i = 0; i < n; i ++) { + l.Add(t); + } + } + return l; + } + } } public class Map @@ -288,9 +301,16 @@ namespace Dafny return new Map(new Dictionary()); } } - public static Map FromElements(params Pair[] values) { + public static Map FromElements(params Pair[] values) { Dictionary d = new Dictionary(values.Length); - foreach (Pair p in values) { + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d); + } + public static Map FromCollection(List> values) { + Dictionary d = new Dictionary(values.Count); + foreach (Pair p in values) { d[p.Car] = p.Cdr; } return new Map(d); @@ -343,6 +363,11 @@ namespace Dafny d[index] = val; return new Map(d); } + public IEnumerable Domain { + get { + return dict.Keys; + } + } } public class Sequence { @@ -471,6 +496,12 @@ namespace Dafny } return frall; } + public static bool QuantMap(Dafny.Map map, bool frall, System.Predicate pred) { + foreach (var u in map.Domain) { + if (pred(u) != frall) { return !frall; } + } + return frall; + } public static bool QuantSeq(Dafny.Sequence seq, bool frall, System.Predicate pred) { foreach (var u in seq.Elements) { if (pred(u) != frall) { return !frall; } @@ -479,6 +510,7 @@ namespace Dafny } // Enumerating other collections public delegate Dafny.Set ComprehensionDelegate(); + public delegate Dafny.Map MapComprehensionDelegate(); public static IEnumerable AllBooleans { get { yield return false; diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 232224b0..fad4e7fa 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1990,6 +1990,11 @@ namespace Microsoft.Dafny { wr.Write("Dafny.Helpers.QuantSet("); TrExpr(b.Set); wr.Write(", "); + } else if (bound is QuantifierExpr.MapBoundedPool) { + var b = (QuantifierExpr.MapBoundedPool)bound; + wr.Write("Dafny.Helpers.QuantMap("); + TrExpr(b.Map); + wr.Write(", "); } else if (bound is QuantifierExpr.SeqBoundedPool) { var b = (QuantifierExpr.SeqBoundedPool)bound; wr.Write("Dafny.Helpers.QuantSeq("); @@ -2047,6 +2052,11 @@ namespace Microsoft.Dafny { wr.Write("foreach (var @{0} in (", bv.Name); TrExpr(b.Set); wr.Write(").Elements) { "); + } else if (bound is QuantifierExpr.MapBoundedPool) { + var b = (QuantifierExpr.MapBoundedPool)bound; + wr.Write("foreach (var @{0} in (", bv.Name); + TrExpr(b.Map); + wr.Write(").Domain) { "); } else if (bound is QuantifierExpr.SeqBoundedPool) { var b = (QuantifierExpr.SeqBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.Name); @@ -2067,6 +2077,70 @@ namespace Microsoft.Dafny { wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName); wr.Write("})()"); + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + // For "map i | R(i) :: Term(i)" where the term has type "V" and i has type "U", emit something like: + // ((MapComprehensionDelegate)delegate() { + // var _coll = new List>(); + // foreach (L l in sq.Elements) { + // foreach (K k in st.Elements) { + // for (BigInteger j = Lo; j < Hi; j++) { + // for (bool i in Helper.AllBooleans) { + // if (R(i,j,k,l)) { + // _coll.Add(new Pair(i, Term(i)); + // } + // } + // } + // } + // } + // return Dafny.Map.FromElements(_coll); + // })() + Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds + var domtypeName = TypeName(((MapType)e.Type).Domain); + var rantypeName = TypeName(((MapType)e.Type).Range); + wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName); + wr.Write("var _coll = new System.Collections.Generic.List>(); ", domtypeName, rantypeName); + var n = e.BoundVars.Count; + Contract.Assert(e.Bounds.Count == n && n == 1); + var bound = e.Bounds[0]; + var bv = e.BoundVars[0]; + if (bound is QuantifierExpr.BoolBoundedPool) { + wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.Name); + } else if (bound is QuantifierExpr.IntBoundedPool) { + var b = (QuantifierExpr.IntBoundedPool)bound; + wr.Write("for (var @{0} = ", bv.Name); + TrExpr(b.LowerBound); + wr.Write("; @{0} < ", bv.Name); + TrExpr(b.UpperBound); + wr.Write("; @{0}++) {{ ", bv.Name); + } else if (bound is QuantifierExpr.SetBoundedPool) { + var b = (QuantifierExpr.SetBoundedPool)bound; + wr.Write("foreach (var @{0} in (", bv.Name); + TrExpr(b.Set); + wr.Write(").Elements) { "); + } else if (bound is QuantifierExpr.MapBoundedPool) { + var b = (QuantifierExpr.MapBoundedPool)bound; + wr.Write("foreach (var @{0} in (", bv.Name); + TrExpr(b.Map); + wr.Write(").Domain) { "); + } else if (bound is QuantifierExpr.SeqBoundedPool) { + var b = (QuantifierExpr.SeqBoundedPool)bound; + wr.Write("foreach (var @{0} in (", bv.Name); + TrExpr(b.Seq); + wr.Write(").Elements) { "); + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type + } + wr.Write("if ("); + TrExpr(e.Range); + wr.Write(") { "); + wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.Name); + TrExpr(e.Term); + wr.Write(")); }"); + wr.Write("}"); + wr.Write("return Dafny.Map<{0},{1}>.FromCollection(_coll); ", domtypeName, rantypeName); + wr.Write("})()"); + } else if (expr is PredicateExpr) { var e = (PredicateExpr)expr; TrExpr(e.Body); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 103cb5c7..97da97e3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1342,14 +1342,28 @@ MultiSetExpr . MapExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); - IToken/*!*/ x = null; List/*!*/ elements; + IToken/*!*/ x = Token.NoToken; + List/*!*/ elements; e = dummyExpr; .) "map" (. x = t; .) - ( "{" (. elements = new List(); .) + ( "[" (. elements = new List(); .) [ MapLiteralExpressions ] (. e = new MapDisplayExpr(x, elements);.) - "}" - | (. SemErr("map must be followed by braces."); .) + "]" + | ( + (. + BoundVar/*!*/ bv; + List bvars = new List(); + Expression/*!*/ range; + Expression body = null; + .) + IdentTypeOptional (. bvars.Add(bv); .) + "|" Expression + QSep + Expression + (. e = new MapComprehension(x, bvars, range, body); .) + ) + | (. SemErr("map must be followed by literal in brackets or comprehension."); .) ) . MapLiteralExpressions<.out List elements.> diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index b42fcb5a..5fd34e65 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -577,7 +577,7 @@ namespace Microsoft.Dafny { /// /// This proxy stands for: - /// set(Arg) or seq(Arg) + /// set(Arg) or seq(Arg) or map(Arg, Range) /// public class CollectionTypeProxy : RestrictedTypeProxy { public readonly Type Arg; @@ -3068,6 +3068,11 @@ namespace Microsoft.Dafny { public readonly Expression Set; public SetBoundedPool(Expression set) { Set = set; } } + public class MapBoundedPool : BoundedPool + { + public readonly Expression Map; + public MapBoundedPool(Expression map) { Map = map; } + } public class SeqBoundedPool : BoundedPool { public readonly Expression Seq; @@ -3162,6 +3167,17 @@ namespace Microsoft.Dafny { TermIsImplicit = term == null; } } + public class MapComprehension : ComprehensionExpr + { + public MapComprehension(IToken/*!*/ tok, List/*!*/ bvars, Expression/*!*/ range, Expression term) + : base(tok, bvars, range, term, null) { + Contract.Requires(tok != null); + Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(1 <= bvars.Count); + Contract.Requires(range != null); + Contract.Requires(term != null); + } + } public class WildcardExpr : Expression { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings) diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 817df12b..fe4d58a9 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2303,21 +2303,35 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void MapExpr(out Expression e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); - IToken/*!*/ x = null; List/*!*/ elements; + IToken/*!*/ x = Token.NoToken; + List/*!*/ elements; e = dummyExpr; Expect(42); x = t; - if (la.kind == 6) { + if (la.kind == 55) { Get(); elements = new List(); if (StartOf(9)) { MapLiteralExpressions(out elements); } e = new MapDisplayExpr(x, elements); - Expect(7); + Expect(56); + } else if (la.kind == 1) { + BoundVar/*!*/ bv; + List bvars = new List(); + Expression/*!*/ range; + Expression body = null; + + IdentTypeOptional(out bv); + bvars.Add(bv); + Expect(18); + Expression(out range); + QSep(); + Expression(out body); + e = new MapComprehension(x, bvars, range, body); } else if (StartOf(19)) { - SemErr("map must be followed by braces."); + SemErr("map must be followed by literal in brackets or comprehension."); } else SynErr(177); } @@ -2426,6 +2440,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } + void QSep() { + if (la.kind == 106) { + Get(); + } else if (la.kind == 107) { + Get(); + } else SynErr(179); + } + void MatchExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); @@ -2454,7 +2476,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 104 || la.kind == 105) { Exists(); x = t; - } else SynErr(179); + } else SynErr(180); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2524,7 +2546,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 103) { Get(); - } else SynErr(180); + } else SynErr(181); } void Exists() { @@ -2532,14 +2554,6 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 105) { Get(); - } else SynErr(181); - } - - void QSep() { - if (la.kind == 106) { - Get(); - } else if (la.kind == 107) { - Get(); } else SynErr(182); } @@ -2800,10 +2814,10 @@ public class Errors { case 176: s = "invalid MultiSetExpr"; break; case 177: s = "invalid MapExpr"; break; case 178: s = "invalid ConstAtomExpression"; break; - case 179: s = "invalid QuantifierGuts"; break; - case 180: s = "invalid Forall"; break; - case 181: s = "invalid Exists"; break; - case 182: s = "invalid QSep"; break; + case 179: s = "invalid QSep"; break; + case 180: s = "invalid QuantifierGuts"; break; + case 181: s = "invalid Forall"; break; + case 182: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 38ec17fc..6cf71fa1 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1190,6 +1190,24 @@ namespace Microsoft.Dafny { } if (parensNeeded) { wr.Write(")"); } + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + bool parensNeeded = !isRightmost; + if (parensNeeded) { wr.Write("("); } + wr.Write("map "); + string sep = ""; + foreach (BoundVar bv in e.BoundVars) { + wr.Write("{0}{1}", sep, bv.Name); + sep = ", "; + PrintType(": ", bv.Type); + } + PrintAttributes(e.Attributes); + wr.Write(" | "); + PrintExpression(e.Range); + wr.Write(" :: "); + PrintExpression(e.Term); + if (parensNeeded) { wr.Write(")"); } + } else if (expr is WildcardExpr) { wr.Write("*"); diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 29a4943a..d966a76f 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -353,6 +353,8 @@ namespace Microsoft.Dafny { return new ForallExpr(tk, bvs, range, term, null); } else if (e is ExistsExpr) { return new ExistsExpr(tk, bvs, range, term, null); + } else if (e is MapComprehension) { + return new MapComprehension(tk, bvs, range, term); } else { Contract.Assert(e is SetComprehension); return new SetComprehension(tk, bvs, range, term); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 4402e5b1..7be3fca2 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3067,6 +3067,42 @@ namespace Microsoft.Dafny { } } + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + int prevErrorCount = ErrorCount; + scope.PushMarker(); + if (e.BoundVars.Count != 1) { + Error(e.tok, "a map comprehension must have exactly one bound variable."); + } + foreach (BoundVar v in e.BoundVars) { + if (!scope.Push(v.Name, v)) { + Error(v, "Duplicate bound-variable name: {0}", v.Name); + } + ResolveType(v.tok, v.Type, null, true); + } + ResolveExpression(e.Range, twoState); + Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.Range.Type, Type.Bool)) { + Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type); + } + ResolveExpression(e.Term, twoState); + Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression + + ResolveAttributes(e.Attributes, twoState); + scope.PopMarker(); + expr.Type = new MapType(e.BoundVars[0].Type,e.Term.Type); + + if (prevErrorCount == ErrorCount) { + var missingBounds = new List(); + e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds); + if (missingBounds.Count != 0) { + e.MissingBounds = missingBounds; + foreach (var bv in e.MissingBounds) { + Error(expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); + } + } + } + } else if (expr is WildcardExpr) { expr.Type = new SetType(new ObjectType()); @@ -4251,6 +4287,9 @@ namespace Microsoft.Dafny { } else if (expr is SetComprehension) { var e = (SetComprehension)expr; return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term)); } else if (expr is WildcardExpr) { return false; } else if (expr is PredicateExpr) { diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 3f3d89f1..0189c11b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1730,19 +1730,29 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; bool isSequence = e.Seq.Type is SeqType; - Bpl.Expr total = IsTotal(e.Seq, etran); - Bpl.Expr seq = etran.TrExpr(e.Seq); - Bpl.Expr e0 = null; - if (e.E0 != null) { - e0 = etran.TrExpr(e.E0); - total = BplAnd(total, IsTotal(e.E0, etran)); - total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne)); - } - if (e.E1 != null) { - total = BplAnd(total, IsTotal(e.E1, etran)); - total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true)); + if (e.Seq.Type is MapType) { + Bpl.Expr total = IsTotal(e.Seq, etran); + Bpl.Expr map = etran.TrExpr(e.Seq); + var e0 = etran.TrExpr(e.E0); + Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), map); + inDomain = Bpl.Expr.Select(inDomain, etran.BoxIfNecessary(e.tok, e0, e.E0.Type)); + total = BplAnd(total, inDomain); + return total; + } else { + Bpl.Expr total = IsTotal(e.Seq, etran); + Bpl.Expr seq = etran.TrExpr(e.Seq); + Bpl.Expr e0 = null; + if (e.E0 != null) { + e0 = etran.TrExpr(e.E0); + total = BplAnd(total, IsTotal(e.E0, etran)); + total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne)); + } + if (e.E1 != null) { + total = BplAnd(total, IsTotal(e.E1, etran)); + total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true)); + } + return total; } - return total; } else if (expr is MultiSelectExpr) { MultiSelectExpr e = (MultiSelectExpr)expr; Bpl.Expr total = IsTotal(e.Array, etran); @@ -5475,7 +5485,7 @@ namespace Microsoft.Dafny { x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0); } else if (e.Seq.Type is MapType) { x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq); - x = Bpl.Expr.Select(x, translator.FunctionCall(e.tok, BuiltinFunction.Box, null, e0)); + x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType)); } else { Contract.Assert(false); x = null; } if (!ModeledAsBoxType(elmtType)) { x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x); @@ -5839,6 +5849,36 @@ namespace Microsoft.Dafny { return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst); + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + // Translate "map x | R :: T" into + // Map#Glue(lambda y: BoxType :: [unbox(y)/x]R, + // lambda y: BoxType :: [unbox(y)/x]T)". + Bpl.VariableSeq bvars = new Bpl.VariableSeq(); + var bv = e.BoundVars[0]; + TrBoundVariables(e.BoundVars, bvars); + + Bpl.QKeyValue kv = TrAttributes(e.Attributes, null); + + var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType)); + translator.otherTmpVarCount++; + + Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, yVar), bv.Type, this); + Bpl.Expr unboxy = !ModeledAsBoxType(bv.Type) ? translator.FunctionCall(e.tok, BuiltinFunction.Unbox, translator.TrType(bv.Type), new Bpl.IdentifierExpr(expr.tok, yVar)) + : (Bpl.Expr)(new Bpl.IdentifierExpr(expr.tok, yVar)); + + + Dictionary subst = new Dictionary(); + subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type)); + + var ebody = translator.BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(Substitute(e.Range, null, subst))); + Bpl.Expr l1 = new Bpl.LambdaExpr(e.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, ebody); + ebody = TrExpr(Substitute(e.Term, null, subst)); + Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type)); + + + return translator.FunctionCall(e.tok, BuiltinFunction.MapGlue, null, l1, l2); + } else if (expr is PredicateExpr) { var e = (PredicateExpr)expr; return TrExpr(e.Body); @@ -6301,6 +6341,7 @@ namespace Microsoft.Dafny { MapBuild, MapDisjoint, MapUnion, + MapGlue, IndexField, MultiIndexField, @@ -6485,6 +6526,9 @@ namespace Microsoft.Dafny { case BuiltinFunction.MapElements: Contract.Assert(args.Length == 1); return FunctionCall(tok, "Map#Elements", typeInstantiation, args); + case BuiltinFunction.MapGlue: + Contract.Assert(args.Length == 2); + return FunctionCall(tok, "Map#Glue", predef.MapType(tok, predef.BoxType, predef.BoxType), args); case BuiltinFunction.MapEqual: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); @@ -7427,6 +7471,10 @@ namespace Microsoft.Dafny { if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) { newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm); } + } else if (e is MapComprehension) { + if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) { + newExpr = new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm); + } } else if (e is QuantifierExpr) { var q = (QuantifierExpr)e; if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) { @@ -7437,7 +7485,7 @@ namespace Microsoft.Dafny { } } } else { - Contract.Assume(false); // unexpected ComprehensionExpr + Contract.Assert(false); // unexpected ComprehensionExpr } } else if (expr is PredicateExpr) { diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 35a5017b..c451cc62 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1565,7 +1565,7 @@ Maps.dfy(126,13): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 22 verified, 2 errors +Dafny program verifier finished with 30 verified, 2 errors -------------------- SmallTests.dfy -------------------- SmallTests.dfy(30,11): Error: index out of range diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index eb543283..a49ac3c1 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -2,7 +2,7 @@ // This method can be used to test compilation. method Main() { - var m:= map{2:=3}; + var m := map[2:=3]; // test "in" if(2 in m) { @@ -25,28 +25,28 @@ method Main() else { assert false; } // test disjoint operator - if(m !! map{3 := 3}) + if(m !! map[3 := 3]) { print "m3\n"; } else { assert false; } // updates should replace values that already exist - if(m[2 := 4] == map{2 := 4}) + if(m[2 := 4] == map[2 := 4]) { print "m4\n"; } else { assert false; } // add something to the map - if(m[7 := 1] == map{2 := 3,7 := 1}) + if(m[7 := 1] == map[2 := 3,7 := 1]) { print "m5\n"; } else { assert false; } // test applicative nature of Map in C# - if(m == map{2 := 3}) + if(m == map[2 := 3]) { print "m6\n"; } @@ -57,7 +57,7 @@ method Main() method m() { - var a := map{2:=3}; var b := map{3:=2}; + var a := map[2:=3]; var b := map[3:=2]; assert a[b[3]] == 3; } method m2(a: map, b: map) @@ -72,7 +72,7 @@ method m3(a: map) } method m4() { - var a := map{3 := 9}; + var a := map[3 := 9]; if(a[4] == 4) // UNSAFE, 4 not in the domain { m(); @@ -86,14 +86,14 @@ method m5(a: map) } method m6() { - var a := map{3 := 9}; - assert a[3:=5] == map{3:=5}; - assert a[2:=5] == map{2:=5, 3:=9}; - assert a[2:=5] == map{2:=6, 3:=9, 2:=5}; // test the ordering of assignments in the map literal + var a := map[3 := 9]; + assert a[3:=5] == map[3:=5]; + assert a[2:=5] == map[2:=5, 3:=9]; + assert a[2:=5] == map[2:=6, 3:=9, 2:=5]; // test the ordering of assignments in the map literal } method m7() { - var a := map{1:=1, 2:=4, 3:=9}; + var a := map[1:=1, 2:=4, 3:=9]; assert forall i | i in a :: a[i] == i * i; assert 0 !in a; assert 1 in a; @@ -103,7 +103,7 @@ method m7() } method m8() { - var a := map{}; + var a := map[]; assert forall i :: i !in a; // check emptiness var i,n := 0, 100; while(i < n) @@ -114,24 +114,24 @@ method m8() a := a[i := i * i]; i := i + 1; } - assert a !! map{-1:=2}; + assert a !! map[-1:=2]; m3(a); } method m9() { - var a, b := map{}, map{}; + var a, b := map[], map[]; assert a !! b; - b := map{2:=3,4:=2,5:=-6,6:=7}; + b := map[2:=3,4:=2,5:=-6,6:=7]; assert a !! b; - assert b !! map{6:=3}; // ERROR, both share 6 in the domain. + assert b !! map[6:=3]; // ERROR, both share 6 in the domain. } method m10() { - var a, b := map{}, map{}; + var a, b := map[], map[]; assert a !! b; - b := map{2:=3,4:=2,5:=-6,6:=7}; + b := map[2:=3,4:=2,5:=-6,6:=7]; assert a !! b; - a := map{3:=3,1:=2,9:=-6,8:=7}; + a := map[3:=3,1:=2,9:=-6,8:=7]; assert a !! b; } method m11(a: map, b: map) @@ -139,3 +139,44 @@ method m11(a: map, b: map) { assert a !! b; } + +method m12() +{ + var x := map i | 0 <= i < 10 :: i * 2; + assert 0 in x; + assert 1 in x; + assert 10 !in x; + assert x[0] == 0 && x[2] == 4; +} + +function domain(m: map): set + ensures forall i :: i in domain(m) <==> i in m; +{ + set s | s in m +} + +method m13() +{ + var s := {0, 1, 3, 4}; + var x := map i | i in s :: i; + assert forall i | i in x :: x[i] == i; + assert domain(x) == s; +} + +function union(m: map, m': map): map + requires m !! m'; + ensures forall i :: i in union(m, m') <==> i in m || i in m'; + ensures forall i :: i in m ==> union(m, m')[i] == m[i]; + ensures forall i :: i in m' ==> union(m, m')[i] == m'[i]; +{ + map i | i in (domain(m) + domain(m')) :: if i in m then m[i] else m'[i] +} + +method m14() +{ + var s, t := {0, 1}, {3, 4}; + var x,y := map i | i in s :: i, map i | i in t :: 1+i; + ghost var u := union(x,y); + assert u[1] == 1 && u[3] == 4; + assert domain(u) == {0, 1, 3, 4}; +} -- cgit v1.2.3