Skip to content

Commit

Permalink
Merge branch 'master' into triggers-for-such-that
Browse files Browse the repository at this point in the history
  • Loading branch information
@RustanLeino
RustanLeino committed Feb 24, 2025
2 parents b43bf6b + cd5902f commit 8ef0bfa
Show file tree
Hide file tree
Showing 108 changed files with 7,150 additions and 3,730 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ public static void TestApply()
_3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("std"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("any"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
RAST._IType _4_Any;
_4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<RAST._IAttribute>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<RAST._IAttribute>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummy"), (_3_std__any__Any).AsType(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("doit"), Std.Wrappers.Option<RAST._IType>.create_Some((RAST.__default.RcType).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unknown")))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("something"))).ApplyType(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType((RAST.__default.std__default__Default).AsType())))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements(RAST.__default.std__default__Default__default, (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd!"))).AsExpr()).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString"))).AsType()), ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType"))).AsType()))))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.RcPath)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.std__default__Default)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummy"), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any")), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("doit"), Std.Wrappers.Option<RAST._IType>.create_Some((RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Rc"))).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unknown")))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("something"))).ApplyType(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Default")))))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Default"))).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("default"))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements()), (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd!"))).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString"))), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))))))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), Dafny.Sequence<RAST._IType>.FromElements(), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyIntern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing"))))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), Dafny.Sequence<RAST._IType>.FromElements(), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyIntern"), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))))));
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ public ForallStmt(Cloner cloner, ForallStmt original) : base(cloner, original) {
Attributes = cloner.CloneAttributes(original.Attributes);

if (cloner.CloneResolvedFields) {
Bounds = original.Bounds.ConvertAll(bp => bp.Clone(cloner));
Bounds = original.Bounds.ConvertAll(bp => bp?.Clone(cloner));
Kind = original.Kind;
EffectiveEnsuresClauses = original.EffectiveEnsuresClauses?.Select(cloner.CloneExpr).ToList();
}
Expand Down
27 changes: 26 additions & 1 deletion Source/DafnyCore/AST/TypeDeclarations/Declaration.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,17 +110,42 @@ public bool IsVisibleInScope(VisibilityScope scope) {
protected string? sanitizedName;
public virtual string SanitizedName => sanitizedName ??= NonglobalVariable.SanitizeName(Name);

protected string enclosingModuleName; // Computed at the same time as compileName

protected string? compileName;

public virtual string GetCompileName(DafnyOptions options) {
if (compileName == null) {
this.IsExtern(options, out _, out compileName);
this.IsExtern(options, out var possibleEnclosingModuleName, out compileName);
if (!IsCompiled) {
enclosingModuleName = possibleEnclosingModuleName;
}
if (this is TopLevelDecl topDecl) {
enclosingModuleName ??= topDecl.EnclosingModuleDefinition.GetCompileName(options);
}

compileName ??= SanitizedName;
}

return compileName;
}

public bool IsCompiled {
get {
var compile = true;
return !Attributes.ContainsBool(Attributes, "compile", ref compile) || compile;
}
}

public string GetQualificationName(DafnyOptions options) {
if (compileName == null) {
GetCompileName(options); // Sets the enclosing module name if defined by externs.
return enclosingModuleName;
}

return enclosingModuleName;
}

public Attributes? Attributes; // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict
Attributes? IAttributeBearingDeclaration.Attributes {
get => Attributes;
Expand Down
Loading

0 comments on commit 8ef0bfa

Please sign in to comment.