summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl9
-rw-r--r--Binaries/DafnyRuntime.cs36
-rw-r--r--Source/Dafny/Compiler.cs74
-rw-r--r--Source/Dafny/Dafny.atg22
-rw-r--r--Source/Dafny/DafnyAst.cs18
-rw-r--r--Source/Dafny/Parser.cs50
-rw-r--r--Source/Dafny/Printer.cs18
-rw-r--r--Source/Dafny/RefinementTransformer.cs2
-rw-r--r--Source/Dafny/Resolver.cs39
-rw-r--r--Source/Dafny/Translator.cs76
-rw-r--r--Test/dafny0/Answer2
-rw-r--r--Test/dafny0/Maps.dfy81
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, V> u: U ::
{ Map#Domain(Map#Empty(): Map U V)[u] }
!Map#Domain(Map#Empty(): Map U V)[u]);
+function Map#Glue<U, V>([U] bool, [U]V): Map U V;
+axiom (forall<U, V> a: [U] bool, b:[U]V ::
+ { Map#Domain(Map#Glue(a, b)) }
+ Map#Domain(Map#Glue(a, b)) == a);
+axiom (forall<U, V> 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<U, V>(Map U V, U, V): Map U V;
/*axiom (forall<U, V> 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<T>(r);
}
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ 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<U, V>
@@ -288,9 +301,16 @@ namespace Dafny
return new Map<U, V>(new Dictionary<U,V>());
}
}
- public static Map<U, V> FromElements(params Pair<U,V>[] values) {
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
- foreach (Pair<U,V> p in values) {
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
d[p.Car] = p.Cdr;
}
return new Map<U, V>(d);
@@ -343,6 +363,11 @@ namespace Dafny
d[index] = val;
return new Map<U, V>(d);
}
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
}
public class Sequence<T>
{
@@ -471,6 +496,12 @@ namespace Dafny
}
return frall;
}
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> 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<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
public static IEnumerable<bool> 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<U, V>)delegate() {
+ // var _coll = new List<Pair<U,V>>();
+ // 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<U, V>.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<Dafny.Pair<{0},{1}>>(); ", 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<out Expression e>
.
MapExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = null; List<ExpressionPair/*!*/>/*!*/ elements;
+ IToken/*!*/ x = Token.NoToken;
+ List<ExpressionPair/*!*/>/*!*/ elements;
e = dummyExpr;
.)
"map" (. x = t; .)
- ( "{" (. elements = new List<ExpressionPair/*!*/>(); .)
+ ( "[" (. elements = new List<ExpressionPair/*!*/>(); .)
[ MapLiteralExpressions<out elements> ] (. e = new MapDisplayExpr(x, elements);.)
- "}"
- | (. SemErr("map must be followed by braces."); .)
+ "]"
+ | (
+ (.
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression/*!*/ range;
+ Expression body = null;
+ .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
+ "|" Expression<out range>
+ QSep
+ Expression<out body>
+ (. e = new MapComprehension(x, bvars, range, body); .)
+ )
+ | (. SemErr("map must be followed by literal in brackets or comprehension."); .)
)
.
MapLiteralExpressions<.out List<ExpressionPair> 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 {
/// <summary>
/// This proxy stands for:
- /// set(Arg) or seq(Arg)
+ /// set(Arg) or seq(Arg) or map(Arg, Range)
/// </summary>
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<BoundVar/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void MapExpr(out Expression e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = null; List<ExpressionPair/*!*/>/*!*/ elements;
+ IToken/*!*/ x = Token.NoToken;
+ List<ExpressionPair/*!*/>/*!*/ elements;
e = dummyExpr;
Expect(42);
x = t;
- if (la.kind == 6) {
+ if (la.kind == 55) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(9)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(7);
+ Expect(56);
+ } else if (la.kind == 1) {
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ 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<Expression/*!*/>/*!*/ 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<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
@@ -2454,7 +2476,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<BoundVar>();
+ 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<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();
+ 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<U, V> 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<int, bool>, b: map<int, bool>)
@@ -72,7 +72,7 @@ method m3(a: map<int, int>)
}
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<int, int>)
}
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<U, V>(a: map<U, V>, b: map<U, V>)
@@ -139,3 +139,44 @@ method m11<U, V>(a: map<U, V>, b: map<U, V>)
{
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<U, V>(m: map<U,V>): set<U>
+ 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<U, V>(m: map<U,V>, m': map<U,V>): map<U,V>
+ 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};
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 12:48:30 +0000