Skip to content

Commit

Permalink
Monomorphic Field and collection types (#4597)
Browse files Browse the repository at this point in the history 
Removes the type argument from `Field`, and from all collection types.
All heap and collection elements are now always of type `Box`.

This has the effect of very slightly increasing brittleness on some
particularly brittle examples, though it has minimal effect on most
code. The benefits of the simplification (and the opportunities it opens
for future optimization) seem worth the tradeoff, however.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

---------

Co-authored-by: Aaron Tomb <[email protected]>
  • Loading branch information
@zafer-esen @atomb
zafer-esen and atomb authored Feb 9, 2024
1 parent 29c4525 commit fdc06b5
Show file tree
Hide file tree
Showing 44 changed files with 1,710 additions and 1,802 deletions.
678 changes: 340 additions & 338 deletions Source/DafnyCore/DafnyPrelude.bpl
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Source/DafnyCore/GeneratedFromDafny.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -921,7 +921,7 @@ public static Dafny.ISequence<__T> SetToSeq<__T>(Dafny.ISet<__T> s) {
goto after__ASSIGN_SUCH_THAT_0;
}
}
throw new System.Exception("assign-such-that search produced no value (line 7231)");
throw new System.Exception("assign-such-that search produced no value (line 7247)");
after__ASSIGN_SUCH_THAT_0:;
_105_left = Dafny.Set<__T>.Difference(_105_left, Dafny.Set<__T>.FromElements(_106_x));
xs = Dafny.Sequence<__T>.Concat(xs, Dafny.Sequence<__T>.FromElements(_106_x));
Expand Down
103 changes: 31 additions & 72 deletions Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -295,30 +295,24 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan

case BuiltinFunction.SetCard:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Card", Bpl.Type.Int, args);
case BuiltinFunction.SetEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.SetType(tok, true, typeInstantiation);
Bpl.Type resultType = predef.SetType;
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Set#Empty", resultType, args), resultType);
}
case BuiltinFunction.SetUnionOne:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#UnionOne", predef.SetType(tok, true, typeInstantiation), args);
return FunctionCall(tok, "Set#UnionOne", predef.SetType, args);
case BuiltinFunction.SetUnion:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Union", predef.SetType(tok, true, typeInstantiation), args);
return FunctionCall(tok, "Set#Union", predef.SetType, args);
case BuiltinFunction.SetIntersection:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Intersection", predef.SetType(tok, true, typeInstantiation), args);
return FunctionCall(tok, "Set#Intersection", predef.SetType, args);
case BuiltinFunction.SetDifference:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Difference", predef.SetType(tok, true, typeInstantiation), args);
return FunctionCall(tok, "Set#Difference", predef.SetType, args);
case BuiltinFunction.SetEqual:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
Expand All @@ -333,148 +327,114 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan
return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);
case BuiltinFunction.ISetEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.SetType(tok, false, typeInstantiation);
Bpl.Type resultType = predef.ISetType;
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "ISet#Empty", resultType, args), resultType);
}
case BuiltinFunction.ISetUnionOne:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "ISet#UnionOne", predef.SetType(tok, false, typeInstantiation), args);
return FunctionCall(tok, "ISet#UnionOne", predef.ISetType, args);
case BuiltinFunction.ISetUnion:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "ISet#Union", predef.SetType(tok, false, typeInstantiation), args);
return FunctionCall(tok, "ISet#Union", predef.ISetType, args);
case BuiltinFunction.ISetIntersection:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "ISet#Intersection", predef.SetType(tok, false, typeInstantiation), args);
return FunctionCall(tok, "ISet#Intersection", predef.ISetType, args);
case BuiltinFunction.ISetDifference:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "ISet#Difference", predef.SetType(tok, false, typeInstantiation), args);
return FunctionCall(tok, "ISet#Difference", predef.ISetType, args);
case BuiltinFunction.ISetEqual:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "ISet#Equal", Bpl.Type.Bool, args);
case BuiltinFunction.ISetSubset:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "ISet#Subset", Bpl.Type.Bool, args);
case BuiltinFunction.ISetDisjoint:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "ISet#Disjoint", Bpl.Type.Bool, args);
case BuiltinFunction.MultiSetCard:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "MultiSet#Card", Bpl.Type.Int, args);
case BuiltinFunction.MultiSetEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.MultiSetType(tok, typeInstantiation);
Bpl.Type resultType = predef.MultiSetType;
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "MultiSet#Empty", resultType, args), resultType);
}
case BuiltinFunction.MultiSetUnionOne:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "MultiSet#UnionOne", predef.MultiSetType(tok, typeInstantiation), args);
return FunctionCall(tok, "MultiSet#UnionOne", predef.MultiSetType, args);
case BuiltinFunction.MultiSetUnion:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "MultiSet#Union", predef.MultiSetType(tok, typeInstantiation), args);
return FunctionCall(tok, "MultiSet#Union", predef.MultiSetType, args);
case BuiltinFunction.MultiSetIntersection:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "MultiSet#Intersection", predef.MultiSetType(tok, typeInstantiation), args);
return FunctionCall(tok, "MultiSet#Intersection", predef.MultiSetType, args);
case BuiltinFunction.MultiSetDifference:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "MultiSet#Difference", predef.MultiSetType(tok, typeInstantiation), args);
return FunctionCall(tok, "MultiSet#Difference", predef.MultiSetType, args);
case BuiltinFunction.MultiSetEqual:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "MultiSet#Equal", Bpl.Type.Bool, args);
case BuiltinFunction.MultiSetSubset:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "MultiSet#Subset", Bpl.Type.Bool, args);
case BuiltinFunction.MultiSetDisjoint:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "MultiSet#Disjoint", Bpl.Type.Bool, args);
case BuiltinFunction.MultiSetFromSet:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "MultiSet#FromSet", predef.MultiSetType(tok, typeInstantiation), args);
return FunctionCall(tok, "MultiSet#FromSet", predef.MultiSetType, args);
case BuiltinFunction.MultiSetFromSeq:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "MultiSet#FromSeq", predef.MultiSetType(tok, typeInstantiation), args);
return FunctionCall(tok, "MultiSet#FromSeq", predef.MultiSetType, args);
case BuiltinFunction.IsGoodMultiSet:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args);

case BuiltinFunction.SeqLength:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Length", Bpl.Type.Int, args);
case BuiltinFunction.SeqEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.SeqType(tok, typeInstantiation);
Bpl.Type resultType = predef.SeqType;
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType);
}
case BuiltinFunction.SeqBuild:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Build", predef.SeqType(tok, typeInstantiation), args);
return FunctionCall(tok, "Seq#Build", predef.SeqType, args);
case BuiltinFunction.SeqAppend:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Append", predef.SeqType(tok, typeInstantiation), args);
return FunctionCall(tok, "Seq#Append", predef.SeqType, args);
case BuiltinFunction.SeqIndex:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Index", typeInstantiation, args);
return FunctionCall(tok, "Seq#Index", predef.BoxType, args);
case BuiltinFunction.SeqUpdate:
Contract.Assert(args.Length == 3);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Update", predef.SeqType(tok, typeInstantiation), args);
return FunctionCall(tok, "Seq#Update", predef.SeqType, args);
case BuiltinFunction.SeqContains:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Contains", Bpl.Type.Bool, args);
case BuiltinFunction.SeqDrop:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Drop", predef.SeqType(tok, typeInstantiation), args);
return FunctionCall(tok, "Seq#Drop", predef.SeqType, args);
case BuiltinFunction.SeqTake:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Take", predef.SeqType(tok, typeInstantiation), args);
return FunctionCall(tok, "Seq#Take", predef.SeqType, args);
case BuiltinFunction.SeqEqual:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Equal", Bpl.Type.Bool, args);
case BuiltinFunction.SeqSameUntil:
Contract.Assert(args.Length == 3);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
case BuiltinFunction.SeqFromArray:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);
case BuiltinFunction.SeqRank:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#Rank", Bpl.Type.Int, args);

case BuiltinFunction.MapEmpty: {
Contract.Assert(args.Length == 0);
Contract.Assert(typeInstantiation != null);
Bpl.Type resultType = predef.MapType(tok, true, typeInstantiation, typeInstantiation); // use 'typeInstantiation' (which is really always just BoxType anyway) as both type arguments
Bpl.Type resultType = predef.MapType;
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Map#Empty", resultType, args), resultType);
}
case BuiltinFunction.MapCard:
Expand All @@ -489,7 +449,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan
return FunctionCall(tok, "Map#Elements", typeInstantiation, args);
case BuiltinFunction.MapGlue:
Contract.Assert(args.Length == 3);
return FunctionCall(tok, "Map#Glue", predef.MapType(tok, true, predef.BoxType, predef.BoxType), args);
return FunctionCall(tok, "Map#Glue", predef.MapType, args);
case BuiltinFunction.MapEqual:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
Expand All @@ -505,8 +465,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan

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
Bpl.Type resultType = predef.IMapType;
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "IMap#Empty", resultType, args), resultType);
}
case BuiltinFunction.IMapDomain:
Expand All @@ -517,7 +476,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan
return FunctionCall(tok, "IMap#Elements", typeInstantiation, args);
case BuiltinFunction.IMapGlue:
Contract.Assert(args.Length == 3);
return FunctionCall(tok, "IMap#Glue", predef.MapType(tok, false, predef.BoxType, predef.BoxType), args);
return FunctionCall(tok, "IMap#Glue", predef.IMapType, args);
case BuiltinFunction.IMapEqual:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
Expand All @@ -526,11 +485,11 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan
case BuiltinFunction.IndexField:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "IndexField", predef.FieldName(tok, predef.BoxType), args);
return FunctionCall(tok, "IndexField", predef.FieldName(tok), args);
case BuiltinFunction.MultiIndexField:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "MultiIndexField", predef.FieldName(tok, predef.BoxType), args);
return FunctionCall(tok, "MultiIndexField", predef.FieldName(tok), args);

case BuiltinFunction.Box:
Contract.Assert(args.Length == 1);
Expand Down Expand Up @@ -582,7 +541,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan
case BuiltinFunction.FieldOfDecl:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok, typeInstantiation), args);
return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok), args);
case BuiltinFunction.FDim:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation != null);
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/Verifier/BoogieGenerator.DataTypes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -582,7 +582,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
bvs.Add(dVar);
var ie = new Bpl.IdentifierExpr(arg.tok, dVar);
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
var domain = FunctionCall(arg.tok, f, predef.MapType(arg.tok, finite, predef.BoxType, predef.BoxType),
var domain = FunctionCall(arg.tok, f, finite ? predef.MapType : predef.IMapType,
args[i]);
var inDomain = Bpl.Expr.SelectTok(arg.tok, domain, FunctionCall(arg.tok, BuiltinFunction.Box, null, ie));
var lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);
Expand All @@ -601,11 +601,11 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
bvs.Add(bxVar);
var ie = new Bpl.IdentifierExpr(arg.tok, bxVar);
var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;
var domain = FunctionCall(arg.tok, f, predef.MapType(arg.tok, finite, predef.BoxType, predef.BoxType),
var domain = FunctionCall(arg.tok, f, finite ? predef.MapType : predef.IMapType,
args[i]);
var inDomain = Bpl.Expr.SelectTok(arg.tok, domain, ie);
var ef = finite ? BuiltinFunction.MapElements : BuiltinFunction.IMapElements;
var element = FunctionCall(arg.tok, ef, predef.MapType(arg.tok, finite, predef.BoxType, predef.BoxType),
var element = FunctionCall(arg.tok, ef, finite ? predef.MapType : predef.IMapType,
args[i]);
var elmt = Bpl.Expr.SelectTok(arg.tok, element, ie);
var unboxElmt = FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType, elmt);
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -287,8 +287,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
b1 = e1;
} else {
// for maps, compare their domains as sets
b0 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType(tok, true, predef.BoxType, predef.BoxType), e0);
b1 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType(tok, true, predef.BoxType, predef.BoxType), e1);
b0 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType, e0);
b1 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType, e1);
}
eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, b0, b1);
less = ProperSubset(tok, b0, b1);
Expand All @@ -303,8 +303,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
} else {
Contract.Assert(!((MapType)ty0).Finite);
// for maps, compare their domains as sets
b0 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType(tok, false, predef.BoxType, predef.BoxType), e0);
b1 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType(tok, false, predef.BoxType, predef.BoxType), e1);
b0 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType, e0);
b1 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType, e1);
}
eq = FunctionCall(tok, BuiltinFunction.ISetEqual, null, b0, b1);
less = Bpl.Expr.False;
Expand Down
Loading

0 comments on commit fdc06b5

Please sign in to comment.