feat: Add newtype support for map and imap (#5175)

This PR adds support for newtypes based on `map` and `imap`. Note, members (including the built-in members `.Keys` and `.Values`) have not yet been tested. Support for them will be added in a separate PR. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <[email protected]>
dafny-lang · Apr 9, 2024 · 8e75fcb · 8e75fcb
1 parent 5df66fe
commit 8e75fcb
Show file tree

Hide file tree

Showing 6 changed files with 196 additions and 31 deletions.
diff --git a/.gitignore b/.gitignore
@@ -80,4 +80,4 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/log.smt2
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model
 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html
-Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs
@@ -51,8 +51,28 @@ public class PreTypeConstraints {
  }
  var proxy = (PreTypeProxy)preType;
 
+ var approximateReceiverType = ApproximateReceiverTypeViaBounds(proxy, memberName, out var subProxies);
+ if (approximateReceiverType != null) {
+ return approximateReceiverType;
+ }
+
+ // The bounds didn't give any results, but perhaps one of the proxies visited (in the sub direction) has
+ // associated default advice.
+ foreach (var subProxy in subProxies) {
+ TryApplyDefaultAdviceFor(subProxy);
+ if (proxy.Normalize() is DPreType defaultType) {
+ return defaultType;
+ }
+ }
+
+ // Try once more, in case the application of default advice changed the situation
+ return ApproximateReceiverTypeViaBounds(proxy, memberName, out _);
+ }
+
+ [CanBeNull]
+ private DPreType ApproximateReceiverTypeViaBounds(PreTypeProxy proxy, [CanBeNull] string memberName, out HashSet<PreTypeProxy> subProxies) {
  // If there is a subtype constraint "proxy :> sub<X>", then (if the program is legal at all, then) "sub" must have the member "memberName".
- var subProxies = new HashSet<PreTypeProxy>();
+ subProxies = new HashSet<PreTypeProxy>();
  foreach (var sub in AllSubBounds(proxy, subProxies)) {
  return sub;
  }
@@ -68,16 +88,7 @@ public class PreTypeConstraints {
  }
  }
 
- // The bounds didn't give any results, but perhaps one of the proxies visited (in the sub direction) has
- // associated default advice.
- foreach (var subProxy in subProxies) {
- TryApplyDefaultAdviceFor(subProxy);
- if (proxy.Normalize() is DPreType defaultType) {
- return defaultType;
- }
- }
-
- return null; // could not be determined
+ return null;
  }
 
  /// <summary>
@@ -536,10 +547,12 @@ public enum CommonConfirmationBag {
  InRealFamily,
  InBoolFamily,
  InCharFamily,
- InSeqFamily,
  InSetFamily,
  InIsetFamily,
  InMultisetFamily,
+ InSeqFamily,
+ InMapFamily,
+ InImapFamily,
  IsNullableRefType,
  IsBitvector,
  IntLikeOrBitvector,
@@ -590,6 +603,10 @@ public enum CommonConfirmationBag {
  return familyDeclName == PreType.TypeNameMultiset;
  case CommonConfirmationBag.InSeqFamily:
  return familyDeclName == PreType.TypeNameSeq;
+ case CommonConfirmationBag.InMapFamily:
+ return familyDeclName == PreType.TypeNameMap;
+ case CommonConfirmationBag.InImapFamily:
+ return familyDeclName == PreType.TypeNameImap;
  case CommonConfirmationBag.IsNullableRefType:
  return DPreType.IsReferenceTypeDecl(pt.Decl);
  case CommonConfirmationBag.IsBitvector:
@@ -695,7 +712,7 @@ public enum CommonConfirmationBag {
  case CommonConfirmationBag.IsNewtypeBaseTypeLegacy:
  return pt.Decl is NewtypeDecl || pt.Decl.Name is PreType.TypeNameInt or PreType.TypeNameReal;
  case CommonConfirmationBag.IsNewtypeBaseTypeGeneral:
- if (familyDeclName is PreType.TypeNameMap or PreType.TypeNameImap || pt.Decl is DatatypeDecl) {
+ if (pt.Decl is DatatypeDecl) {
  // These base types are not yet supported, but they will be soon.
  return false;
  }

diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
@@ -153,8 +153,8 @@ public partial class PreTypeResolver {
  AddSubtypeConstraint(rangePreType, p.B.PreType, p.B.tok,
  "All elements of display must have some common supertype (got {1}, but needed type or type of previous elements is {0})");
  }
- var argTypes = new List<PreType>() { domainPreType, rangePreType };
- expr.PreType = new DPreType(BuiltInTypeDecl(PreType.MapTypeName(e.Finite)), argTypes);
+
+ ResolveMapProducingExpr(e.Finite, "display", expr, domainPreType, rangePreType);
 
  } else if (expr is NameSegment) {
  var e = (NameSegment)expr;
@@ -664,9 +664,6 @@ public partial class PreTypeResolver {
  foreach (BoundVar v in e.BoundVars) {
  resolver.ResolveType(v.tok, v.Type, resolutionContext, ResolveTypeOptionEnum.InferTypeProxies, null);
  ScopePushAndReport(v, "bound-variable", true);
- if (v.Type is InferredTypeProxy inferredProxy) {
- Contract.Assert(!inferredProxy.KeepConstraints); // in general, this proxy is inferred to be a base type
- }
  }
  ResolveExpression(e.Range, resolutionContext);
  ConstrainTypeExprBool(e.Range, "range of comprehension must be of type bool (instead got {0})");
@@ -677,8 +674,8 @@ public partial class PreTypeResolver {
 
  ResolveAttributes(e, resolutionContext, false);
  scope.PopMarker();
- expr.PreType = new DPreType(BuiltInTypeDecl(PreType.MapTypeName(e.Finite)),
-  new List<PreType>() { e.TermLeft != null ? e.TermLeft.PreType : e.BoundVars[0].PreType, e.Term.PreType });
+
+ ResolveMapProducingExpr(e.Finite, "comprehension", expr, e.TermLeft?.PreType ?? e.BoundVars[0].PreType, e.Term.PreType);
 
  } else if (expr is LambdaExpr) {
  var e = (LambdaExpr)expr;
@@ -754,19 +751,35 @@ public partial class PreTypeResolver {
  AddConfirmation(confirmationFamily, expr.PreType, expr.tok, $"{exprKind} used as if it had type {{0}}");
  }
 
- private void SetupCollectionProducingExpr(string typeName, string exprKind, Expression expr, PreType elementPreType) {
+ private void ResolveMapProducingExpr(bool finite, string exprKindSuffix, Expression expr, PreType keyPreType, PreType valuePreType) {
+ var typeName = PreType.MapTypeName(finite);
+ PreTypeConstraints.CommonConfirmationBag confirmationFamily =
+ finite ? PreTypeConstraints.CommonConfirmationBag.InMapFamily : PreTypeConstraints.CommonConfirmationBag.InImapFamily;
+ var exprKind = $"{typeName} {exprKindSuffix}";
+
+ SetupCollectionProducingExpr(typeName, exprKind, expr, keyPreType, valuePreType);
+ AddConfirmation(confirmationFamily, expr.PreType, expr.tok, $"{exprKind} used as if it had type {{0}}");
+ }
+
+ private void SetupCollectionProducingExpr(string typeName, string exprKind, Expression expr, PreType elementPreType, PreType valuePreType = null) {
  expr.PreType = CreatePreTypeProxy($"{exprKind}");
 
- var defaultType = new DPreType(BuiltInTypeDecl(typeName), new List<PreType>() { elementPreType });
+ var arguments = valuePreType == null ? new List<PreType>() { elementPreType } : new List<PreType>() { elementPreType, valuePreType };
+ var defaultType = new DPreType(BuiltInTypeDecl(typeName), arguments);
  Constraints.AddDefaultAdvice(expr.PreType, defaultType);
 
  Constraints.AddGuardedConstraint(() => {
  if (expr.PreType.UrAncestor(this) is DPreType dPreType) {
- if (dPreType.Decl.Name == typeName) {
+ if (dPreType.Decl.Name != typeName) {
+ ReportError(expr, $"{exprKind} used as if it had type {{0}}", expr.PreType);
+ } else if (valuePreType == null) {
  AddSubtypeConstraint(dPreType.Arguments[0], elementPreType, expr.tok,
  $"element type of {exprKind} expected to be {{0}} (got {{1}})");
  } else {
- ReportError(expr, $"{exprKind} used as if it had type {{0}}", expr.PreType);
+ AddSubtypeConstraint(dPreType.Arguments[0], elementPreType, expr.tok,
+ $"key type of {exprKind} expected to be {{0}} (got {{1}})");
+ AddSubtypeConstraint(dPreType.Arguments[1], valuePreType, expr.tok,
+ $"value type of {exprKind} expected to be {{0}} (got {{1}})");
  }
  return true;
  }
@@ -893,21 +906,33 @@ public partial class PreTypeResolver {
  // that only the expected types are allowed.
  var a0 = e0.PreType;
  var a1 = e1.PreType;
- var left = a0.NormalizeWrtScope() as DPreType;
- var right = a1.NormalizeWrtScope() as DPreType;
  var familyDeclNameLeft = AncestorName(a0);
  var familyDeclNameRight = AncestorName(a1);
  if (familyDeclNameLeft is PreType.TypeNameMap or PreType.TypeNameImap) {
+ var left = (DPreType)a0.UrAncestor(this);
  Contract.Assert(left.Arguments.Count == 2);
  var st = new DPreType(BuiltInTypeDecl(PreType.TypeNameSet), new List<PreType>() { left.Arguments[0] });
  Constraints.DebugPrint($" DEBUG: guard applies: Minusable {a0} {a1}, converting to {st} :> {a1}");
- AddSubtypeConstraint(st, a1, tok,
- "map subtraction expects right-hand operand to have type {0} (instead got {1})");
+ Constraints.AddDefaultAdvice(a1, st);
+
+ var messageFormat = $"map subtraction expects right-hand operand to have type {st} (instead got {{0}})";
+ Constraints.AddGuardedConstraint(() => {
+ if (a1.UrAncestor(this) is DPreType dPreType) {
+ if (dPreType.Decl.Name != PreType.TypeNameSet) {
+ ReportError(e1, messageFormat, a1);
+ } else {
+ AddSubtypeConstraint(dPreType.Arguments[0], left.Arguments[0], e1.tok,
+ $"element type of {PreType.TypeNameSet} expected to be {{0}} (got {{1}})");
+ }
+ return true;
+ }
+ return false;
+ });
+ AddConfirmation(PreTypeConstraints.CommonConfirmationBag.InSetFamily, a1, e1.tok, messageFormat);
  return true;
  } else if (familyDeclNameLeft != null || (familyDeclNameRight != null && familyDeclNameRight != PreType.TypeNameSet)) {
  Constraints.DebugPrint($" DEBUG: guard applies: Minusable {a0} {a1}, converting to {a0} :> {a1}");
- AddSubtypeConstraint(a0, a1, tok,
- "type of right argument to - ({0}) must agree with the result type ({1})");
+ AddSubtypeConstraint(a0, a1, tok, "type of right argument to - ({0}) must agree with the result type ({1})");
  return true;
  }
  return false;

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollections.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollections.dfy
@@ -9,6 +9,8 @@ method Main() {
  Multiset.Test();
  Seq.Test();
  SeqToMultisetConversion.Test();
+ Map.Test();
+ Imap.Test();
 }
 
 module Set {
@@ -407,3 +409,105 @@ module SeqToMultisetConversion {
  print m0' == m1', " ", |m0'|, "\n"; // true 4
  }
 }
+
+module Map {
+ newtype IntMap = m: map<int, real> | true
+ newtype IntSet = s: set<int> | true
+
+ method Test() {
+ var m: IntMap;
+ m := map[];
+ print m, " "; // map[]
+ m := map[6 := 2.0, 19 := 2.1];
+ var n: IntMap := m;
+ print |m|, " "; // 2
+ print 7 in m, " ", 6 in m, "\n"; // false true
+ print m[6], " ", m[19], "\n"; // 2.0 2.1
+ m := m[17 := 3.0][1800 := 0.0][6 := 1.0];
+ print m[6], " ", m[19], " ", m[17], "\n"; // 1.0 2.1 3.0
+
+ m := m + n;
+ // m is now: map[6 := 2.0, 17 := 3.0, 19 := 2.1, 1800 := 0.0]
+ print |m|, " ", m[6], "\n"; // 4 2.0
+
+ var sf: set<int> := {3, 4, 5, 17, 20};
+ m := m - sf;
+ var nf: IntSet := {3, 1800, 4, 5};
+ m := m - nf;
+ // m is now: map[6 := 2.0, 19 := 2.1]
+ print |m|, " ", m[6] + m[19], "\n"; // 2 4.1
+
+ var u: map<int, real>;
+ u := m as map<int, real>;
+ m := u as IntMap;
+ var b0 := m is map<int, real>;
+ var b1 := u is IntMap;
+
+ print |m|, " ", |u|, " ", b0, " ", b1, "\n"; // 2 2 true true
+
+ b0 := m == n;
+ b1 := m != n;
+ print b0, " ", b1, "\n"; // true false
+
+ TestComprehensions();
+ }
+
+ method TestComprehensions() {
+ var m: IntMap := map x: int | 2 <= x < 5 :: (2 * x) as real;
+ var n: IntMap := map x: int | 2 <= x < 5 :: 2 * x := 10.0 - x as real;
+ expect |m| == |n| == 3;
+ print 2 in m, " ", 2 in n, " ", 4 in m, " ", 4 in n, "\n"; // true false true true
+ assert 2 * 3 in n;
+ print m[3], " ", n[6], "\n"; // 6.0 7.0
+ }
+}
+
+module Imap {
+ newtype IntImap = m: imap<int, real> | true
+ newtype IntSet = s: set<int> | true
+
+ method Test() {
+ var m: IntImap;
+ m := imap[];
+ print m, " "; // imap[]
+ m := imap[6 := 2.0, 19 := 2.1];
+ var n: IntImap := m;
+ print 7 in m, " ", 6 in m, "\n"; // false true
+ print m[6], " ", m[19], "\n"; // 2.0 2.1
+ m := m[17 := 3.0][1800 := 0.0][6 := 1.0];
+ print m[6], " ", m[19], " ", m[17], "\n"; // 1.0 2.1 3.0
+
+ m := m + n;
+ // m is now: imap[6 := 2.0, 17 := 3.0, 19 := 2.1, 1800 := 0.0]
+ print m[6], "\n"; // 2.0
+
+ var sf: set<int> := {3, 4, 5, 17, 20};
+ m := m - sf;
+ var nf: IntSet := {3, 1800, 4, 5};
+ m := m - nf;
+ // m is now: imap[6 := 2.0, 19 := 2.1]
+ print m[6] + m[19], "\n"; // 4.1
+
+ var u: imap<int, real>;
+ u := m as imap<int, real>;
+ m := u as IntImap;
+ var b0 := m is imap<int, real>;
+ var b1 := u is IntImap;
+
+ print b0, " ", b1, "\n"; // true true
+
+ b0 := m == n;
+ b1 := m != n;
+ print b0, " ", b1, "\n"; // true false
+
+ TestComprehensions();
+ }
+
+ method TestComprehensions() {
+ var m: IntImap := imap x: int | 2 <= x < 5 :: (2 * x) as real;
+ var n: IntImap := imap x: int | 2 <= x < 5 :: 2 * x := 10.0 - x as real;
+ print 2 in m, " ", 2 in n, " ", 4 in m, " ", 4 in n, "\n"; // true false true true
+ assert 2 * 3 in n;
+ print m[3], " ", n[6], "\n"; // 6.0 7.0
+ }
+}
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollections.dfy.expect b/...e/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollections.dfy.expect
@@ -32,3 +32,21 @@ true 3
 true 3
 true 4
 true 4
+map[] 2 false true
+2.0 2.1
+1.0 2.1 3.0
+4 2.0
+2 4.1
+2 2 true true
+true false
+true false true true
+6.0 7.0
+map[] false true
+2.0 2.1
+1.0 2.1 3.0
+2.0
+4.1
+true true
+true false
+true false true true
+6.0 7.0
diff --git a/docs/dev/news/5175.feat b/docs/dev/news/5175.feat
@@ -0,0 +1 @@
+Support newtypes based on map and imap