Add imap display/update expressions

10 files changed, 103 insertions, 23 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index b88a0bdc..f4feacdc 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -35,6 +35,10 @@ function Inv0_TMap(Ty) : Ty;
 function Inv1_TMap(Ty) : Ty;

 axiom (forall t, u: Ty :: { TMap(t,u) } Inv0_TMap(TMap(t,u)) == t);

 axiom (forall t, u: Ty :: { TMap(t,u) } Inv1_TMap(TMap(t,u)) == u);

+function Inv0_TIMap(Ty) : Ty;

+function Inv1_TIMap(Ty) : Ty;

+axiom (forall t, u: Ty :: { TIMap(t,u) } Inv0_TIMap(TIMap(t,u)) == t);

+axiom (forall t, u: Ty :: { TIMap(t,u) } Inv1_TIMap(TIMap(t,u)) == u);

 

 // -- Classes and Datatypes --

 

@@ -51,6 +55,7 @@ const unique TagSet      : TyTag;
 const unique TagMultiSet : TyTag;

 const unique TagSeq      : TyTag;

 const unique TagMap      : TyTag;

+const unique TagIMap     : TyTag;

 const unique TagClass    : TyTag;

 

 axiom Tag(TBool) == TagBool;

@@ -62,6 +67,7 @@ axiom (forall t: Ty    :: { TSet(t) }      Tag(TSet(t))      == TagSet);
 axiom (forall t: Ty    :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);

 axiom (forall t: Ty    :: { TSeq(t) }      Tag(TSeq(t))      == TagSeq);

 axiom (forall t, u: Ty :: { TMap(t,u) }    Tag(TMap(t,u))    == TagMap);

+axiom (forall t, u: Ty :: { TIMap(t,u) }   Tag(TIMap(t,u))   == TagIMap);

 

 // ---------------------------------------------------------------

 // -- Literals ---------------------------------------------------

@@ -133,6 +139,9 @@ axiom (forall bx : Box, t : Ty ::
 axiom (forall bx : Box, s : Ty, t : Ty ::

     { $IsBox(bx, TMap(s, t)) }

     ( $IsBox(bx, TMap(s, t)) ==> $Box($Unbox(bx) : Map Box Box) == bx && $Is($Unbox(bx) : Map Box Box, TMap(s, t))));

+axiom (forall bx : Box, s : Ty, t : Ty ::

+    { $IsBox(bx, TIMap(s, t)) }

+    ( $IsBox(bx, TIMap(s, t)) ==> $Box($Unbox(bx) : IMap Box Box) == bx && $Is($Unbox(bx) : IMap Box Box, TIMap(s, t))));

 

 axiom (forall<T> v : T, t : Ty ::

     { $IsBox($Box(v), t) }

@@ -229,6 +238,23 @@ axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap ::
         $IsAllocBox(Map#Elements(v)[bx], t1, h) &&

         $IsAllocBox(bx, t0, h)));

 

+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::

+  { $Is(v, TIMap(t0, t1)) }

+  $Is(v, TIMap(t0, t1))

+     <==> (forall bx: Box ::

+      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }

+      IMap#Domain(v)[bx] ==>

+        $IsBox(IMap#Elements(v)[bx], t1) &&

+        $IsBox(bx, t0)));

+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap ::

+  { $IsAlloc(v, TIMap(t0, t1), h) }

+  $IsAlloc(v, TIMap(t0, t1), h)

+     <==> (forall bx: Box ::

+      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }

+      IMap#Domain(v)[bx] ==>

+        $IsAllocBox(IMap#Elements(v)[bx], t1, h) &&

+        $IsAllocBox(bx, t0, h)));

+

 // ---------------------------------------------------------------

 // -- Encoding of type names -------------------------------------

 // ---------------------------------------------------------------

@@ -934,6 +960,11 @@ type IMap U V;
 function IMap#Domain<U, V>(IMap U V): [U] bool;

 function IMap#Elements<U, V>(IMap U V): [U]V;

 

+function IMap#Empty<U, V>(): IMap U V;

+axiom (forall<U, V> u: U ::

+        { IMap#Domain(IMap#Empty(): IMap U V)[u] }

+        !IMap#Domain(IMap#Empty(): IMap U V)[u]);

+

 function IMap#Glue<U, V>([U] bool, [U]V, Ty): IMap U V;

 axiom (forall<U, V> a: [U] bool, b:[U]V, t:Ty ::

         { IMap#Domain(IMap#Glue(a, b, t)) }

@@ -945,6 +976,19 @@ axiom (forall<U, V> a: [U] bool, b:[U]V, t:Ty ::
         { $Is(IMap#Glue(a, b, t), t) }

         $Is(IMap#Glue(a, b, t), t));

 

+//Build is used in displays

+function IMap#Build<U, V>(IMap U V, U, V): IMap U V;

+/*axiom (forall<U, V> m: IMap U V, u: U, v: V ::

+  { IMap#Domain(IMap#Build(m, u, v))[u] } { IMap#Elements(IMap#Build(m, u, v))[u] }

+  IMap#Domain(IMap#Build(m, u, v))[u] && IMap#Elements(IMap#Build(m, u, v))[u] == v);*/

+

+axiom (forall<U, V> m: IMap U V, u: U, u': U, v: V ::

+  { IMap#Domain(IMap#Build(m, u, v))[u'] } { IMap#Elements(IMap#Build(m, u, v))[u'] }

+  (u' == u ==> IMap#Domain(IMap#Build(m, u, v))[u'] &&

+               IMap#Elements(IMap#Build(m, u, v))[u'] == v) &&

+  (u' != u ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u'] &&

+               IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u']));

+

 //equality for imaps

 function IMap#Equal<U, V>(IMap U V, IMap U V): bool;

 axiom (forall<U, V> m: IMap U V, m': IMap U V::

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 4aaecbde..1c2ab305 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -297,7 +297,7 @@ namespace Microsoft.Dafny
         foreach (ExpressionPair p in e.Elements) {

           pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));

         }

-        return new MapDisplayExpr(Tok(expr.tok), pp);

+        return new MapDisplayExpr(Tok(expr.tok), e.Finite, pp);

 

       } else if (expr is NameSegment) {

         var e = (NameSegment)expr;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9d0ad3b0..f78def79 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -158,6 +158,9 @@ bool IsNonFinalColon() {
 bool IsMapDisplay() {

   return la.kind == _map && scanner.Peek().kind == _lbracket;

 }

+bool IsIMapDisplay() {

+  return la.kind == _imap && scanner.Peek().kind == _lbracket;

+}

 

 bool IsSuffix() {

   return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen;

@@ -320,6 +323,7 @@ bool IsType(ref IToken pt) {
     case _multiset:

     case _seq:

     case _map:

+    case _imap:

       pt = scanner.Peek();

       return IsTypeList(ref pt);

     case _ident:

@@ -2258,7 +2262,11 @@ UnaryExpression<out Expression e, bool allowSemi, bool allowLambda>
 

   | IF(IsMapDisplay())  /* this alternative must be checked before going into EndlessExpression, where there is another "map" */

     "map"                                           (. x = t; .)

-    MapDisplayExpr<x, out e>

+    MapDisplayExpr<x, true, out e>

+    { IF(IsSuffix()) Suffix<ref e> }

+  | IF(IsIMapDisplay())  /* this alternative must be checked before going into EndlessExpression, where there is another "imap" */

+    "imap"                                          (. x = t; .)

+    MapDisplayExpr<x, false, out e>

     { IF(IsSuffix()) Suffix<ref e> }

   | IF(IsLambda(allowLambda))

     LambdaExpression<out e, allowSemi>  /* this is an endless expression */

@@ -2395,13 +2403,13 @@ MultiSetExpr<out Expression e>
     ")"

   )

   .

-MapDisplayExpr<IToken/*!*/ mapToken, out Expression e>

+MapDisplayExpr<IToken/*!*/ mapToken, bool finite, out Expression e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

      List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;

      e = dummyExpr;

   .)

   "["

-    [ MapLiteralExpressions<out elements> ]  (. e = new MapDisplayExpr(mapToken, elements);.)

+    [ MapLiteralExpressions<out elements> ]  (. e = new MapDisplayExpr(mapToken, finite, elements);.)

   "]"

   .

 MapLiteralExpressions<.out List<ExpressionPair> elements.>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index a4f078bc..d97de354 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5561,11 +5561,13 @@ namespace Microsoft.Dafny {
   }

 

   public class MapDisplayExpr : Expression {

+    public bool Finite;

     public List<ExpressionPair> Elements;

-    public MapDisplayExpr(IToken tok, List<ExpressionPair> elements)

+    public MapDisplayExpr(IToken tok, bool finite, List<ExpressionPair> elements)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(elements));

+      Finite = finite;

       Elements = elements;

     }

     public override IEnumerable<Expression> SubExpressions {

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index b8f71d20..840627bb 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -223,6 +223,9 @@ bool IsNonFinalColon() {
 bool IsMapDisplay() {

   return la.kind == _map && scanner.Peek().kind == _lbracket;

 }

+bool IsIMapDisplay() {

+  return la.kind == _imap && scanner.Peek().kind == _lbracket;

+}

 

 bool IsSuffix() {

   return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen;

@@ -385,6 +388,7 @@ bool IsType(ref IToken pt) {
     case _multiset:

     case _seq:

     case _map:

+    case _imap:

       pt = scanner.Peek();

       return IsTypeList(ref pt);

     case _ident:

@@ -3321,7 +3325,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (IsMapDisplay()) {

 			Expect(16);

 			x = t; 

-			MapDisplayExpr(x, out e);

+			MapDisplayExpr(x, true, out e);

+			while (IsSuffix()) {

+				Suffix(ref e);

+			}

+		} else if (IsIMapDisplay()) {

+			Expect(17);

+			x = t; 

+			MapDisplayExpr(x, false, out e);

 			while (IsSuffix()) {

 				Suffix(ref e);

 			}

@@ -3366,7 +3377,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(216);

 	}

 

-	void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {

+	void MapDisplayExpr(IToken/*!*/ mapToken, bool finite, out Expression e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

 		List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;

 		e = dummyExpr;

@@ -3375,7 +3386,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (StartOf(7)) {

 			MapLiteralExpressions(out elements);

 		}

-		e = new MapDisplayExpr(mapToken, elements);

+		e = new MapDisplayExpr(mapToken, finite, elements);

 		Expect(42);

 	}

 

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 41b40bfc..bf483528 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1340,7 +1340,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is MapDisplayExpr) {

         MapDisplayExpr e = (MapDisplayExpr)expr;

-        wr.Write("map");

+        wr.Write(e.Finite ? "map" : "imap");

         wr.Write("[");

         PrintExpressionPairList(e.Elements);

         wr.Write("]");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 88b896c9..e1d8c95f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -6480,7 +6480,7 @@ namespace Microsoft.Dafny
             Error(p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);

           }

         }

-        expr.Type = new MapType(true, domainType, rangeType);

+        expr.Type = new MapType(e.Finite, domainType, rangeType);

       } else if (expr is NameSegment) {

         var e = (NameSegment)expr;

         ResolveNameSegment(e, true, null, opts, false);

@@ -6605,6 +6605,16 @@ namespace Microsoft.Dafny
             Error(e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);

           }

           expr.Type = e.Seq.Type;

+        } else if (UnifyTypes(e.Seq.Type, new MapType(false, domainType, rangeType))) {

+          ResolveExpression(e.Index, opts);

+          if (!UnifyTypes(e.Index.Type, domainType)) {

+            Error(e.Index, "imap update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);

+          }

+          ResolveExpression(e.Value, opts);

+          if (!UnifyTypes(e.Value.Type, rangeType)) {

+            Error(e.Value, "imap update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);

+          }

+          expr.Type = e.Seq.Type;

         } else if (UnifyTypes(e.Seq.Type, new MultiSetType(elementType))) {

           ResolveExpression(e.Index, opts);

           if (!UnifyTypes(e.Index.Type, elementType)) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b10294b7..cdc40e2f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -10438,12 +10438,12 @@ namespace Microsoft.Dafny {
 

         } else if (expr is MapDisplayExpr) {

           MapDisplayExpr e = (MapDisplayExpr)expr;

-          Bpl.Type maptype = predef.MapType(expr.tok, true, predef.BoxType, predef.BoxType);

-          Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MapEmpty, predef.BoxType);

+          Bpl.Type maptype = predef.MapType(expr.tok, e.Finite, predef.BoxType, predef.BoxType);

+          Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.MapEmpty : BuiltinFunction.IMapEmpty, predef.BoxType);

           foreach (ExpressionPair p in e.Elements) {

             Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A), cce.NonNull(p.A.Type));

             Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B), cce.NonNull(p.B.Type));

-            s = translator.FunctionCall(expr.tok, "Map#Build", maptype, s, elt, elt2);

+            s = translator.FunctionCall(expr.tok, e.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2);

           }

           return s;

 

@@ -10558,13 +10558,13 @@ namespace Microsoft.Dafny {
               Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);

               return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);

             }

-            else if (seqType is MapType && ((MapType)seqType).Finite)

+            else if (seqType is MapType)

             {

               MapType mt = (MapType)seqType;

-              Bpl.Type maptype = predef.MapType(expr.tok, true, predef.BoxType, predef.BoxType);

+              Bpl.Type maptype = predef.MapType(expr.tok, mt.Finite, predef.BoxType, predef.BoxType);

               Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain);

               Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range);

-              return translator.FunctionCall(expr.tok, "Map#Build", maptype, seq, index, val);

+              return translator.FunctionCall(expr.tok, mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val);

             }

             else if (seqType is MultiSetType)

             {

@@ -11668,6 +11668,7 @@ namespace Microsoft.Dafny {
       MapUnion,

       MapGlue,

 

+      IMapEmpty,

       IMapDomain,

       IMapElements,

       IMapEqual,

@@ -11982,6 +11983,12 @@ namespace Microsoft.Dafny {
           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "Map#Disjoint", typeInstantiation, args);

 

+        case BuiltinFunction.IMapEmpty: {

+            Contract.Assert(args.Length == 0);

+            Contract.Assert(typeInstantiation != null);

+            Bpl.Type resultType = predef.MapType(tok, false, typeInstantiation, typeInstantiation);  // use 'typeInstantiation' (which is really always just BoxType anyway) as both type arguments

+            return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "IMap#Empty", resultType, args), resultType);

+          }

         case BuiltinFunction.IMapDomain:

           Contract.Assert(args.Length == 1);

           return FunctionCall(tok, "IMap#Domain", typeInstantiation, args);

@@ -13173,7 +13180,7 @@ namespace Microsoft.Dafny {
             }

           }

           if (anyChanges) {

-            newExpr = new MapDisplayExpr(expr.tok, elmts);

+            newExpr = new MapDisplayExpr(expr.tok, e.Finite, elmts);

           }

         } else if (expr is MemberSelectExpr) {

           MemberSelectExpr fse = (MemberSelectExpr)expr;

diff --git a/Test/dafny0/IMaps.dfy b/Test/dafny0/IMaps.dfy
index 19edd4fb..0ec8fba4 100644
--- a/Test/dafny0/IMaps.dfy
+++ b/Test/dafny0/IMaps.dfy
@@ -4,8 +4,7 @@
 // This method can be used to test compilation.

 ghost method M()

 {

-   var m := map[2:=3];

-   ghost var im := imap i | i in m :: m[i];

+   ghost var im := imap[2:=3];

    // test "in"

    if(2 in im)

    {

@@ -25,7 +24,7 @@ ghost method M()
    else

    { assert false; }

    // test applicative nature of Map<U, V> in C#

-   if(im == (imap i | i == 2 :: 3))

+   if(im == imap[2 := 3])

    {

    }

    else

@@ -63,8 +62,7 @@ lemma m5(a: imap<int, int>)
 }

 lemma m7()

 {

-   var m := map[1:=1, 2:=4, 3:=9];

-   var a := imap i | i in m :: m[i];

+   var a := imap[1:=1, 2:=4, 3:=9];

    assert forall i | i in a :: a[i] == i * i;

    assert 0 !in a;

    assert 1 in a;

diff --git a/Test/dafny0/IMaps.dfy.expect b/Test/dafny0/IMaps.dfy.expect
index 344d7abf..c2da9505 100644
--- a/Test/dafny0/IMaps.dfy.expect
+++ b/Test/dafny0/IMaps.dfy.expect
@@ -1,4 +1,4 @@
-IMaps.dfy(53,8): Error: element may not be in domain

+IMaps.dfy(52,8): Error: element may not be in domain

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then