Skip to content

Commit

Permalink
Merge branch 'master' into fix-predicate-parens
Browse files Browse the repository at this point in the history
  • Loading branch information
@RustanLeino
RustanLeino committed Feb 9, 2024
2 parents 217e7a2 + 693baaf commit 5f365fa
Show file tree
Hide file tree
Showing 51 changed files with 1,758 additions and 1,817 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/jekyll.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ jobs:
- name: Checkout
uses: actions/checkout@v4
- name: Setup Ruby
uses: ruby/setup-ruby@1
uses: ruby/setup-ruby@v1
with:
ruby-version: '3.1' # Not needed with a .ruby-version file
bundler-cache: true # runs 'bundle install' and caches installed gems automatically
Expand Down
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 5f365fa

Please sign in to comment.