From c7caa77a6ad5244ed213c9a838a4b8ba9f20e4ba Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 14 Aug 2025 10:58:44 +0200 Subject: [PATCH 01/12] Remove bad [SyntaxConstructor] --- .../Expressions/Datatypes/DatatypeValue.cs | 1 - .../AST/SyntaxDeserializer/Generated.cs | 198 ++++++++---------- Source/Scripts/Syntax.cs-schema | 73 +++---- 3 files changed, 120 insertions(+), 152 deletions(-) diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs index 01ccbb6c6cc..f360b0a3c3c 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs @@ -44,7 +44,6 @@ public DatatypeValue(IOrigin origin, string datatypeName, string memberName, [Ca : this(origin, datatypeName, memberName, new ActualBindings(arguments)) { } - [SyntaxConstructor] public DatatypeValue(IOrigin origin, string datatypeName, string memberName, ActualBindings bindings) : base(origin) { DatatypeName = datatypeName; diff --git a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs index 7c6d7d5e673..e8d17984a48 100644 --- a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs +++ b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs @@ -360,92 +360,6 @@ public OldExpr ReadOldExprOption() return ReadOldExpr(); } - public DatatypeValue ReadDatatypeValue() - { - var parameter0 = ReadAbstract(); - var parameter1 = ReadString(); - var parameter2 = ReadString(); - var parameter3 = ReadActualBindings(); - return new DatatypeValue(parameter0, parameter1, parameter2, parameter3); - } - - public DatatypeValue ReadDatatypeValueOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadDatatypeValue(); - } - - public ModuleQualifiedId ReadModuleQualifiedId() - { - var parameter0 = ReadList(() => ReadName()); - return new ModuleQualifiedId(parameter0); - } - - public ModuleQualifiedId ReadModuleQualifiedIdOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadModuleQualifiedId(); - } - - public Name ReadName() - { - var parameter0 = ReadAbstract(); - var parameter1 = ReadString(); - return new Name(parameter0, parameter1); - } - - public Name ReadNameOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadName(); - } - - public ActualBinding ReadActualBinding() - { - var parameter0 = ReadAbstractOption(); - var parameter1 = ReadAbstract(); - var parameter2 = ReadBoolean(); - return new ActualBinding(parameter0, parameter1, parameter2); - } - - public ActualBinding ReadActualBindingOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadActualBinding(); - } - - public ActualBindings ReadActualBindings() - { - var parameter0 = ReadList(() => ReadActualBinding()); - return new ActualBindings(parameter0); - } - - public ActualBindings ReadActualBindingsOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadActualBindings(); - } - public TernaryExpr ReadTernaryExpr() { var parameter0 = ReadAbstract(); @@ -684,6 +598,73 @@ public AllocateClass ReadAllocateClassOption() return ReadAllocateClass(); } + public ModuleQualifiedId ReadModuleQualifiedId() + { + var parameter0 = ReadList(() => ReadName()); + return new ModuleQualifiedId(parameter0); + } + + public ModuleQualifiedId ReadModuleQualifiedIdOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadModuleQualifiedId(); + } + + public Name ReadName() + { + var parameter0 = ReadAbstract(); + var parameter1 = ReadString(); + return new Name(parameter0, parameter1); + } + + public Name ReadNameOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadName(); + } + + public ActualBinding ReadActualBinding() + { + var parameter0 = ReadAbstractOption(); + var parameter1 = ReadAbstract(); + var parameter2 = ReadBoolean(); + return new ActualBinding(parameter0, parameter1, parameter2); + } + + public ActualBinding ReadActualBindingOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadActualBinding(); + } + + public ActualBindings ReadActualBindings() + { + var parameter0 = ReadList(() => ReadActualBinding()); + return new ActualBindings(parameter0); + } + + public ActualBindings ReadActualBindingsOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadActualBindings(); + } + public ExprRhs ReadExprRhs() { var parameter0 = ReadAbstract(); @@ -2334,31 +2315,6 @@ private object ReadObject(System.Type actualType) return ReadOldExpr(); } - if (actualType == typeof(DatatypeValue)) - { - return ReadDatatypeValue(); - } - - if (actualType == typeof(ModuleQualifiedId)) - { - return ReadModuleQualifiedId(); - } - - if (actualType == typeof(Name)) - { - return ReadName(); - } - - if (actualType == typeof(ActualBinding)) - { - return ReadActualBinding(); - } - - if (actualType == typeof(ActualBindings)) - { - return ReadActualBindings(); - } - if (actualType == typeof(TernaryExpr)) { return ReadTernaryExpr(); @@ -2419,6 +2375,26 @@ private object ReadObject(System.Type actualType) return ReadAllocateClass(); } + if (actualType == typeof(ModuleQualifiedId)) + { + return ReadModuleQualifiedId(); + } + + if (actualType == typeof(Name)) + { + return ReadName(); + } + + if (actualType == typeof(ActualBinding)) + { + return ReadActualBinding(); + } + + if (actualType == typeof(ActualBindings)) + { + return ReadActualBindings(); + } + if (actualType == typeof(ExprRhs)) { return ReadExprRhs(); diff --git a/Source/Scripts/Syntax.cs-schema b/Source/Scripts/Syntax.cs-schema index 901831c7c67..a1e380e6497 100644 --- a/Source/Scripts/Syntax.cs-schema +++ b/Source/Scripts/Syntax.cs-schema @@ -202,46 +202,6 @@ class OldExpr : Expression String? at; } -class DatatypeValue : Expression -{ - String datatypeName; - String memberName; - ActualBindings bindings; -} - -abstract class NodeWithoutOrigin : Node -{ -} - -class ModuleQualifiedId : NodeWithoutOrigin -{ - List path; -} - -class Name : Node -{ - IOrigin origin; - String value; -} - -class Specification : NodeWithoutOrigin where T : Node -{ - List? expressions; - Attributes? attributes; -} - -class ActualBinding : NodeWithoutOrigin -{ - IOrigin? formalParameterName; - Expression actual; - Boolean isGhost; -} - -class ActualBindings : NodeWithoutOrigin -{ - List argumentBindings; -} - class TernaryExpr : Expression { TernaryExprOpcode op; @@ -360,6 +320,39 @@ class AllocateClass : TypeRhs ActualBindings? bindings; } +abstract class NodeWithoutOrigin : Node +{ +} + +class ModuleQualifiedId : NodeWithoutOrigin +{ + List path; +} + +class Name : Node +{ + IOrigin origin; + String value; +} + +class Specification : NodeWithoutOrigin where T : Node +{ + List? expressions; + Attributes? attributes; +} + +class ActualBinding : NodeWithoutOrigin +{ + IOrigin? formalParameterName; + Expression actual; + Boolean isGhost; +} + +class ActualBindings : NodeWithoutOrigin +{ + List argumentBindings; +} + class AllocateArray : TypeRhs { Type? explicitType; From 9a397128faa56caeb05668e443edd46f65fc616f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 14 Aug 2025 10:59:01 +0200 Subject: [PATCH 02/12] Turn off 'recursive constraint dependency' message --- .../NameResolutionAndTypeInference.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 61f5309c597..453e05b820d 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4230,7 +4230,7 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); } else { // detect self-loops here, since they don't show up in the graph's SCC methods - reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name); + // reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name); } } t.ResolvedClass = d; From a2b5d1fa50e435a24860d4c48bc57a4d97c66567 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 15 Aug 2025 15:32:28 +0200 Subject: [PATCH 03/12] Updates --- .../Expressions/Datatypes/DatatypeValue.cs | 1 - .../AST/Expressions/Heap/WildcardExpr.cs | 1 + .../AST/SyntaxDeserializer/Generated.cs | 219 +++++++++--------- .../NameResolutionAndTypeInference.cs | 2 +- Source/Scripts/Syntax.cs-schema | 77 +++--- 5 files changed, 147 insertions(+), 153 deletions(-) diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs index 01ccbb6c6cc..f360b0a3c3c 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs @@ -44,7 +44,6 @@ public DatatypeValue(IOrigin origin, string datatypeName, string memberName, [Ca : this(origin, datatypeName, memberName, new ActualBindings(arguments)) { } - [SyntaxConstructor] public DatatypeValue(IOrigin origin, string datatypeName, string memberName, ActualBindings bindings) : base(origin) { DatatypeName = datatypeName; diff --git a/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs b/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs index 831ef5bc0ad..5b958f4a9c5 100644 --- a/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs @@ -7,6 +7,7 @@ public class WildcardExpr : Expression, ICloneable { // a Wildcar public WildcardExpr(Cloner cloner, WildcardExpr original) : base(cloner, original) { } + [SyntaxConstructor] public WildcardExpr(IOrigin origin) : base(origin) { Contract.Requires(origin != null); diff --git a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs index 7c6d7d5e673..ba253063227 100644 --- a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs +++ b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs @@ -306,6 +306,22 @@ public CharLiteralExpr ReadCharLiteralExprOption() return ReadCharLiteralExpr(); } + public WildcardExpr ReadWildcardExpr() + { + var parameter0 = ReadAbstract(); + return new WildcardExpr(parameter0); + } + + public WildcardExpr ReadWildcardExprOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadWildcardExpr(); + } + public UnchangedExpr ReadUnchangedExpr() { var parameter0 = ReadAbstract(); @@ -360,92 +376,6 @@ public OldExpr ReadOldExprOption() return ReadOldExpr(); } - public DatatypeValue ReadDatatypeValue() - { - var parameter0 = ReadAbstract(); - var parameter1 = ReadString(); - var parameter2 = ReadString(); - var parameter3 = ReadActualBindings(); - return new DatatypeValue(parameter0, parameter1, parameter2, parameter3); - } - - public DatatypeValue ReadDatatypeValueOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadDatatypeValue(); - } - - public ModuleQualifiedId ReadModuleQualifiedId() - { - var parameter0 = ReadList(() => ReadName()); - return new ModuleQualifiedId(parameter0); - } - - public ModuleQualifiedId ReadModuleQualifiedIdOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadModuleQualifiedId(); - } - - public Name ReadName() - { - var parameter0 = ReadAbstract(); - var parameter1 = ReadString(); - return new Name(parameter0, parameter1); - } - - public Name ReadNameOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadName(); - } - - public ActualBinding ReadActualBinding() - { - var parameter0 = ReadAbstractOption(); - var parameter1 = ReadAbstract(); - var parameter2 = ReadBoolean(); - return new ActualBinding(parameter0, parameter1, parameter2); - } - - public ActualBinding ReadActualBindingOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadActualBinding(); - } - - public ActualBindings ReadActualBindings() - { - var parameter0 = ReadList(() => ReadActualBinding()); - return new ActualBindings(parameter0); - } - - public ActualBindings ReadActualBindingsOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadActualBindings(); - } - public TernaryExpr ReadTernaryExpr() { var parameter0 = ReadAbstract(); @@ -684,6 +614,73 @@ public AllocateClass ReadAllocateClassOption() return ReadAllocateClass(); } + public ModuleQualifiedId ReadModuleQualifiedId() + { + var parameter0 = ReadList(() => ReadName()); + return new ModuleQualifiedId(parameter0); + } + + public ModuleQualifiedId ReadModuleQualifiedIdOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadModuleQualifiedId(); + } + + public Name ReadName() + { + var parameter0 = ReadAbstract(); + var parameter1 = ReadString(); + return new Name(parameter0, parameter1); + } + + public Name ReadNameOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadName(); + } + + public ActualBinding ReadActualBinding() + { + var parameter0 = ReadAbstractOption(); + var parameter1 = ReadAbstract(); + var parameter2 = ReadBoolean(); + return new ActualBinding(parameter0, parameter1, parameter2); + } + + public ActualBinding ReadActualBindingOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadActualBinding(); + } + + public ActualBindings ReadActualBindings() + { + var parameter0 = ReadList(() => ReadActualBinding()); + return new ActualBindings(parameter0); + } + + public ActualBindings ReadActualBindingsOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadActualBindings(); + } + public ExprRhs ReadExprRhs() { var parameter0 = ReadAbstract(); @@ -2319,6 +2316,11 @@ private object ReadObject(System.Type actualType) return ReadCharLiteralExpr(); } + if (actualType == typeof(WildcardExpr)) + { + return ReadWildcardExpr(); + } + if (actualType == typeof(UnchangedExpr)) { return ReadUnchangedExpr(); @@ -2334,31 +2336,6 @@ private object ReadObject(System.Type actualType) return ReadOldExpr(); } - if (actualType == typeof(DatatypeValue)) - { - return ReadDatatypeValue(); - } - - if (actualType == typeof(ModuleQualifiedId)) - { - return ReadModuleQualifiedId(); - } - - if (actualType == typeof(Name)) - { - return ReadName(); - } - - if (actualType == typeof(ActualBinding)) - { - return ReadActualBinding(); - } - - if (actualType == typeof(ActualBindings)) - { - return ReadActualBindings(); - } - if (actualType == typeof(TernaryExpr)) { return ReadTernaryExpr(); @@ -2419,6 +2396,26 @@ private object ReadObject(System.Type actualType) return ReadAllocateClass(); } + if (actualType == typeof(ModuleQualifiedId)) + { + return ReadModuleQualifiedId(); + } + + if (actualType == typeof(Name)) + { + return ReadName(); + } + + if (actualType == typeof(ActualBinding)) + { + return ReadActualBinding(); + } + + if (actualType == typeof(ActualBindings)) + { + return ReadActualBindings(); + } + if (actualType == typeof(ExprRhs)) { return ReadExprRhs(); diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 61f5309c597..453e05b820d 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4230,7 +4230,7 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); } else { // detect self-loops here, since they don't show up in the graph's SCC methods - reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name); + // reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name); } } t.ResolvedClass = d; diff --git a/Source/Scripts/Syntax.cs-schema b/Source/Scripts/Syntax.cs-schema index 901831c7c67..f9470d3e3bf 100644 --- a/Source/Scripts/Syntax.cs-schema +++ b/Source/Scripts/Syntax.cs-schema @@ -184,6 +184,10 @@ class CharLiteralExpr : LiteralExpr { } +class WildcardExpr : Expression +{ +} + class UnchangedExpr : Expression { List frame; @@ -202,46 +206,6 @@ class OldExpr : Expression String? at; } -class DatatypeValue : Expression -{ - String datatypeName; - String memberName; - ActualBindings bindings; -} - -abstract class NodeWithoutOrigin : Node -{ -} - -class ModuleQualifiedId : NodeWithoutOrigin -{ - List path; -} - -class Name : Node -{ - IOrigin origin; - String value; -} - -class Specification : NodeWithoutOrigin where T : Node -{ - List? expressions; - Attributes? attributes; -} - -class ActualBinding : NodeWithoutOrigin -{ - IOrigin? formalParameterName; - Expression actual; - Boolean isGhost; -} - -class ActualBindings : NodeWithoutOrigin -{ - List argumentBindings; -} - class TernaryExpr : Expression { TernaryExprOpcode op; @@ -360,6 +324,39 @@ class AllocateClass : TypeRhs ActualBindings? bindings; } +abstract class NodeWithoutOrigin : Node +{ +} + +class ModuleQualifiedId : NodeWithoutOrigin +{ + List path; +} + +class Name : Node +{ + IOrigin origin; + String value; +} + +class Specification : NodeWithoutOrigin where T : Node +{ + List? expressions; + Attributes? attributes; +} + +class ActualBinding : NodeWithoutOrigin +{ + IOrigin? formalParameterName; + Expression actual; + Boolean isGhost; +} + +class ActualBindings : NodeWithoutOrigin +{ + List argumentBindings; +} + class AllocateArray : TypeRhs { Type? explicitType; From d135d519cafe5f24c8d206b6a7e78181fef9e70f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Aug 2025 13:39:32 +0200 Subject: [PATCH 04/12] Add AssumeStmt --- Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs index cbe324e58e6..594e97007af 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs @@ -12,6 +12,7 @@ public AssumeStmt Clone(Cloner cloner) { public AssumeStmt(Cloner cloner, AssumeStmt original) : base(cloner, original) { } + [SyntaxConstructor] public AssumeStmt(IOrigin origin, Expression expr, Attributes attributes) : base(origin, expr, attributes) { Contract.Requires(origin != null); From e636935c9cd9c38653c856ba41b04a60618e6055 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Aug 2025 13:40:30 +0200 Subject: [PATCH 05/12] update schema --- .../AST/SyntaxDeserializer/Generated.cs | 23 +++++++++++++++++++ Source/Scripts/Syntax.cs-schema | 4 ++++ 2 files changed, 27 insertions(+) diff --git a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs index ba253063227..87d93ff5080 100644 --- a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs +++ b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs @@ -517,6 +517,24 @@ public ExpectStmt ReadExpectStmtOption() return ReadExpectStmt(); } + public AssumeStmt ReadAssumeStmt() + { + var parameter0 = ReadAbstract(); + var parameter2 = ReadAttributes(); + var parameter1 = ReadAbstract(); + return new AssumeStmt(parameter0, parameter1, parameter2); + } + + public AssumeStmt ReadAssumeStmtOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadAssumeStmt(); + } + public AssertStmt ReadAssertStmt() { var parameter0 = ReadAbstract(); @@ -2371,6 +2389,11 @@ private object ReadObject(System.Type actualType) return ReadExpectStmt(); } + if (actualType == typeof(AssumeStmt)) + { + return ReadAssumeStmt(); + } + if (actualType == typeof(AssertStmt)) { return ReadAssertStmt(); diff --git a/Source/Scripts/Syntax.cs-schema b/Source/Scripts/Syntax.cs-schema index f9470d3e3bf..c2128af9367 100644 --- a/Source/Scripts/Syntax.cs-schema +++ b/Source/Scripts/Syntax.cs-schema @@ -277,6 +277,10 @@ class ExpectStmt : PredicateStmt Expression? message; } +class AssumeStmt : PredicateStmt +{ +} + class AssertStmt : PredicateStmt { AssertLabel? label; From 33c802a8d39457c6b6e520e9656f335c199716eb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Aug 2025 15:30:04 +0200 Subject: [PATCH 06/12] Add AssumeStmt --- Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs | 5 +++-- Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs index 594e97007af..0d218410012 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs @@ -1,3 +1,4 @@ +#nullable enable using System.Collections.Generic; using System.Diagnostics.Contracts; using Microsoft.Dafny.Auditor; @@ -13,7 +14,7 @@ public AssumeStmt(Cloner cloner, AssumeStmt original) : base(cloner, original) { } [SyntaxConstructor] - public AssumeStmt(IOrigin origin, Expression expr, Attributes attributes) + public AssumeStmt(IOrigin origin, Expression expr, Attributes? attributes) : base(origin, expr, attributes) { Contract.Requires(origin != null); Contract.Requires(expr != null); @@ -44,7 +45,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co public override void ResolveGhostness(ModuleResolver resolver, ErrorReporter reporter, bool mustBeErasable, ICodeContext codeContext, - string proofContext, bool allowAssumptionVariables, bool inConstructorInitializationPhase) { + string? proofContext, bool allowAssumptionVariables, bool inConstructorInitializationPhase) { IsGhost = true; } } diff --git a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs index 87d93ff5080..bf960e949e8 100644 --- a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs +++ b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs @@ -520,7 +520,7 @@ public ExpectStmt ReadExpectStmtOption() public AssumeStmt ReadAssumeStmt() { var parameter0 = ReadAbstract(); - var parameter2 = ReadAttributes(); + var parameter2 = ReadAttributesOption(); var parameter1 = ReadAbstract(); return new AssumeStmt(parameter0, parameter1, parameter2); } From 296febe8813686b2009b1f313bf967b4f4fa39fa Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Sep 2025 17:17:03 +0200 Subject: [PATCH 07/12] Add tests --- .../TestFiles/LitTests/LitTest/ast/constResolution.dfy | 8 ++++++++ .../LitTests/LitTest/ast/constResolution.dfy.expect | 3 +++ .../LitTest/ast/{const.dfy => constVerification.dfy} | 0 .../{const.dfy.expect => constVerification.dfy.expect} | 0 .../LitTests/LitTest/ast/subsetTypes/cycles.dfy | 10 ++++++++++ .../LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect | 0 6 files changed, 21 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect rename Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/{const.dfy => constVerification.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/{const.dfy.expect => constVerification.dfy.expect} (100%) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy new file mode 100644 index 00000000000..5dcd66096bf --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy @@ -0,0 +1,8 @@ +// RUN: %testDafnyForEachResolver "%s" -- --allow-axioms=false + +type Even = x: int | x % 2 == 0 +opaque const ten: Even := 10 + +const twoHundred: LessThanHundredNinetyNine := 200 +const hundredNinetyNine: int := twoHundred as int - 1 +type LessThanHundredNinetyNine = k | 0 <= k < hundredNinetyNine \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect new file mode 100644 index 00000000000..9295799d21f --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect @@ -0,0 +1,3 @@ +constResolution.dfy(4,5): Error: recursive constraint dependency involving a subset type: LessThanTwoHundred -> twoHundred_2 -> LessThanTwoHundred +constResolution.dfy(8,5): Error: recursive constraint dependency involving a subset type: LessThanHundredNinetyNine -> hundredNinetyNine -> twoHundred -> LessThanHundredNinetyNine +2 resolution/type errors detected in constResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy new file mode 100644 index 00000000000..e06dc315078 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy @@ -0,0 +1,10 @@ +// RUN: ! %verify %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +datatype Stmt = + | Skip + | Block(stmts: seq) + | If(b: bool, thn: BlockStmt, els: BlockStmt) + +type BlockStmt = s: Stmt | s.Block? witness Block([]) +// ^^^^^^^^^ error: recursive constraint dependency involving a subset type: BlockStmt -> Stmt -> BlockStmt \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect new file mode 100644 index 00000000000..e69de29bb2d From 21c4e283f6e00279eb8bf2a061a955e24a38ee9e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Sep 2025 17:30:55 +0200 Subject: [PATCH 08/12] Update cycles test --- .../LitTests/LitTest/ast/subsetTypes/cycles.dfy | 9 +++++++-- .../LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect | 2 ++ 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy index e06dc315078..da50e9bc750 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy @@ -1,4 +1,4 @@ -// RUN: ! %verify %s &> "%t" +// RUN: ! %verify --type-system-refresh --general-traits=datatype %s &> "%t" // RUN: %diff "%s.expect" "%t" datatype Stmt = @@ -7,4 +7,9 @@ datatype Stmt = | If(b: bool, thn: BlockStmt, els: BlockStmt) type BlockStmt = s: Stmt | s.Block? witness Block([]) -// ^^^^^^^^^ error: recursive constraint dependency involving a subset type: BlockStmt -> Stmt -> BlockStmt \ No newline at end of file + +trait SelfConstraintDep> {} +trait SelfConstraintDep2> extends object {} + +datatype D extends SelfConstraintDep = D {} +class C extends SelfConstraintDep2 {} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect index e69de29bb2d..7e54a5efe76 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect @@ -0,0 +1,2 @@ +cycles.dfy(9,5): Error: recursive constraint dependency involving a subset type: BlockStmt -> Stmt -> BlockStmt +1 resolution/type errors detected in cycles.dfy From 7e9c3a93b93a7a2c3e3fca8697e367317261866c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Sep 2025 18:08:08 +0200 Subject: [PATCH 09/12] Add tests and update code --- .../NameResolutionAndTypeInference.cs | 3 --- .../TestFiles/LitTests/LitTest/ast/constResolution.dfy | 9 ++++++--- .../LitTests/LitTest/ast/constResolution.dfy.expect | 4 ++-- .../LitTests/LitTest/ast/subsetTypes/cycles.dfy | 6 ------ .../TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy | 8 ++++++++ .../LitTests/LitTest/ast/typeBounds/cycles.dfy.expect | 2 ++ 6 files changed, 18 insertions(+), 14 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 8645e2b671f..91ca77576a7 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4228,9 +4228,6 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo } else if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) { // detect self-loops here, since they don't show up in the graph's SCC methods reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); - } else { - // detect self-loops here, since they don't show up in the graph's SCC methods - // reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name); } } t.ResolvedClass = d; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy index 5dcd66096bf..9b9532f445c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy @@ -1,8 +1,11 @@ -// RUN: %testDafnyForEachResolver "%s" -- --allow-axioms=false +// RUN: ! %testDafnyForEachResolver "%s" -- --allow-axioms=false type Even = x: int | x % 2 == 0 opaque const ten: Even := 10 -const twoHundred: LessThanHundredNinetyNine := 200 -const hundredNinetyNine: int := twoHundred as int - 1 +const twoHundred: LessThanTwoHundred := 200 +type LessThanTwoHundred = k | 0 <= k < twoHundred + +const twoHundred_2: LessThanHundredNinetyNine := 200 +const hundredNinetyNine: int := twoHundred_2 as int - 1 type LessThanHundredNinetyNine = k | 0 <= k < hundredNinetyNine \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect index 9295799d21f..90fb86cfac9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect @@ -1,3 +1,3 @@ -constResolution.dfy(4,5): Error: recursive constraint dependency involving a subset type: LessThanTwoHundred -> twoHundred_2 -> LessThanTwoHundred -constResolution.dfy(8,5): Error: recursive constraint dependency involving a subset type: LessThanHundredNinetyNine -> hundredNinetyNine -> twoHundred -> LessThanHundredNinetyNine +constResolution.dfy(7,5): Error: recursive constraint dependency involving a subset type: LessThanTwoHundred -> twoHundred -> LessThanTwoHundred +constResolution.dfy(11,5): Error: recursive constraint dependency involving a subset type: LessThanHundredNinetyNine -> hundredNinetyNine -> twoHundred_2 -> LessThanHundredNinetyNine 2 resolution/type errors detected in constResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy index da50e9bc750..16ab37ec0c8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy @@ -7,9 +7,3 @@ datatype Stmt = | If(b: bool, thn: BlockStmt, els: BlockStmt) type BlockStmt = s: Stmt | s.Block? witness Block([]) - -trait SelfConstraintDep> {} -trait SelfConstraintDep2> extends object {} - -datatype D extends SelfConstraintDep = D {} -class C extends SelfConstraintDep2 {} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy new file mode 100644 index 00000000000..903850941fb --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy @@ -0,0 +1,8 @@ +// RUN: %verify --type-system-refresh --general-traits=datatype %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +trait SelfConstraintDep> {} +trait SelfConstraintDep2> extends object {} + +datatype D extends SelfConstraintDep = D {} +class C extends SelfConstraintDep2 {} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect new file mode 100644 index 00000000000..012f5b99379 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors From 1d5679619ce6205fdc8613d1dd2cc2dd10a90363 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Sep 2025 23:16:01 +0200 Subject: [PATCH 10/12] Updates --- Source/DafnyCore/Resolver/ModuleResolver.cs | 3 ++- .../dafny0/GeneralNewtypeResolution.dfy.expect | 16 +++++++++------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 206bf2cf53b..4dac5be115b 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1696,7 +1696,8 @@ private void ComputeGhostInterestAndMisc(List declarations) { private void CheckForCyclesAmongRedirectingTypes(RedirectingTypeDecl dd, HashSet cycleErrorHasBeenReported) { var enclosingModule = dd.EnclosingModule; - if (enclosingModule.CallGraph.GetSCCSize(dd) != 1) { + if (enclosingModule.CallGraph.GetSCCSize(dd) != 1 || + enclosingModule.CallGraph.FindVertex(dd).Successors.Any(v => v.N == dd)) { var r = enclosingModule.CallGraph.GetSCCRepresentative(dd); if (cycleErrorHasBeenReported.Contains(r)) { // An error has already been reported for this cycle, so don't report another. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect index f6399331691..c2f6cfe5065 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect @@ -191,11 +191,13 @@ GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed t GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') -GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A -GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(939,10): Error: a newtype ('W') must be based on some numeric type (got X) +GeneralNewtypeResolution.dfy(940,10): Error: Cyclic dependency among declarations: A -> A +GeneralNewtypeResolution.dfy(944,10): Error: a newtype ('W') must be based on some numeric type (got X) +GeneralNewtypeResolution.dfy(945,10): Error: Cyclic dependency among declarations: A -> A GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A -GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A -197 resolution/type errors detected in GeneralNewtypeResolution.dfy +GeneralNewtypeResolution.dfy(955,10): Error: Cyclic dependency among declarations: A -> A +199 resolution/type errors detected in GeneralNewtypeResolution.dfy GeneralNewtypeResolution.dfy(34,10): Error: a newtype ('MyOrdinal') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got ORDINAL) GeneralNewtypeResolution.dfy(40,10): Error: a newtype ('MyObject') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got object) GeneralNewtypeResolution.dfy(41,10): Error: a newtype ('MyTrait') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got Trait) @@ -355,8 +357,8 @@ GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed t GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') -GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A -GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(940,10): Error: Cyclic dependency among declarations: A -> A +GeneralNewtypeResolution.dfy(945,10): Error: Cyclic dependency among declarations: A -> A GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A -GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(955,10): Error: Cyclic dependency among declarations: A -> A 162 resolution/type errors detected in GeneralNewtypeResolution.dfy From 63a36b22ed1df7583ff514f6bc3e14880ad781bd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 2 Sep 2025 11:41:55 +0200 Subject: [PATCH 11/12] Fixes --- .../Expressions/Datatypes/DatatypeValue.cs | 1 + .../AST/SyntaxDeserializer/Generated.cs | 198 ++++++++++-------- Source/DafnyCore/Resolver/ModuleResolver.cs | 2 +- Source/Scripts/Syntax.cs-schema | 73 ++++--- 4 files changed, 153 insertions(+), 121 deletions(-) diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs index f360b0a3c3c..01ccbb6c6cc 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs @@ -44,6 +44,7 @@ public DatatypeValue(IOrigin origin, string datatypeName, string memberName, [Ca : this(origin, datatypeName, memberName, new ActualBindings(arguments)) { } + [SyntaxConstructor] public DatatypeValue(IOrigin origin, string datatypeName, string memberName, ActualBindings bindings) : base(origin) { DatatypeName = datatypeName; diff --git a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs index bf960e949e8..4fb16dc9998 100644 --- a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs +++ b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs @@ -376,6 +376,92 @@ public OldExpr ReadOldExprOption() return ReadOldExpr(); } + public DatatypeValue ReadDatatypeValue() + { + var parameter0 = ReadAbstract(); + var parameter1 = ReadString(); + var parameter2 = ReadString(); + var parameter3 = ReadActualBindings(); + return new DatatypeValue(parameter0, parameter1, parameter2, parameter3); + } + + public DatatypeValue ReadDatatypeValueOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadDatatypeValue(); + } + + public ModuleQualifiedId ReadModuleQualifiedId() + { + var parameter0 = ReadList(() => ReadName()); + return new ModuleQualifiedId(parameter0); + } + + public ModuleQualifiedId ReadModuleQualifiedIdOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadModuleQualifiedId(); + } + + public Name ReadName() + { + var parameter0 = ReadAbstract(); + var parameter1 = ReadString(); + return new Name(parameter0, parameter1); + } + + public Name ReadNameOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadName(); + } + + public ActualBinding ReadActualBinding() + { + var parameter0 = ReadAbstractOption(); + var parameter1 = ReadAbstract(); + var parameter2 = ReadBoolean(); + return new ActualBinding(parameter0, parameter1, parameter2); + } + + public ActualBinding ReadActualBindingOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadActualBinding(); + } + + public ActualBindings ReadActualBindings() + { + var parameter0 = ReadList(() => ReadActualBinding()); + return new ActualBindings(parameter0); + } + + public ActualBindings ReadActualBindingsOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadActualBindings(); + } + public TernaryExpr ReadTernaryExpr() { var parameter0 = ReadAbstract(); @@ -632,73 +718,6 @@ public AllocateClass ReadAllocateClassOption() return ReadAllocateClass(); } - public ModuleQualifiedId ReadModuleQualifiedId() - { - var parameter0 = ReadList(() => ReadName()); - return new ModuleQualifiedId(parameter0); - } - - public ModuleQualifiedId ReadModuleQualifiedIdOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadModuleQualifiedId(); - } - - public Name ReadName() - { - var parameter0 = ReadAbstract(); - var parameter1 = ReadString(); - return new Name(parameter0, parameter1); - } - - public Name ReadNameOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadName(); - } - - public ActualBinding ReadActualBinding() - { - var parameter0 = ReadAbstractOption(); - var parameter1 = ReadAbstract(); - var parameter2 = ReadBoolean(); - return new ActualBinding(parameter0, parameter1, parameter2); - } - - public ActualBinding ReadActualBindingOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadActualBinding(); - } - - public ActualBindings ReadActualBindings() - { - var parameter0 = ReadList(() => ReadActualBinding()); - return new ActualBindings(parameter0); - } - - public ActualBindings ReadActualBindingsOption() - { - if (ReadIsNull()) - { - return default; - } - - return ReadActualBindings(); - } - public ExprRhs ReadExprRhs() { var parameter0 = ReadAbstract(); @@ -2354,6 +2373,31 @@ private object ReadObject(System.Type actualType) return ReadOldExpr(); } + if (actualType == typeof(DatatypeValue)) + { + return ReadDatatypeValue(); + } + + if (actualType == typeof(ModuleQualifiedId)) + { + return ReadModuleQualifiedId(); + } + + if (actualType == typeof(Name)) + { + return ReadName(); + } + + if (actualType == typeof(ActualBinding)) + { + return ReadActualBinding(); + } + + if (actualType == typeof(ActualBindings)) + { + return ReadActualBindings(); + } + if (actualType == typeof(TernaryExpr)) { return ReadTernaryExpr(); @@ -2419,26 +2463,6 @@ private object ReadObject(System.Type actualType) return ReadAllocateClass(); } - if (actualType == typeof(ModuleQualifiedId)) - { - return ReadModuleQualifiedId(); - } - - if (actualType == typeof(Name)) - { - return ReadName(); - } - - if (actualType == typeof(ActualBinding)) - { - return ReadActualBinding(); - } - - if (actualType == typeof(ActualBindings)) - { - return ReadActualBindings(); - } - if (actualType == typeof(ExprRhs)) { return ReadExprRhs(); diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 4dac5be115b..36e321d48f8 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1696,7 +1696,7 @@ private void ComputeGhostInterestAndMisc(List declarations) { private void CheckForCyclesAmongRedirectingTypes(RedirectingTypeDecl dd, HashSet cycleErrorHasBeenReported) { var enclosingModule = dd.EnclosingModule; - if (enclosingModule.CallGraph.GetSCCSize(dd) != 1 || + if (enclosingModule.CallGraph.GetSCCSize(dd) != 1 || enclosingModule.CallGraph.FindVertex(dd).Successors.Any(v => v.N == dd)) { var r = enclosingModule.CallGraph.GetSCCRepresentative(dd); if (cycleErrorHasBeenReported.Contains(r)) { diff --git a/Source/Scripts/Syntax.cs-schema b/Source/Scripts/Syntax.cs-schema index c2128af9367..5899a4d1e5c 100644 --- a/Source/Scripts/Syntax.cs-schema +++ b/Source/Scripts/Syntax.cs-schema @@ -206,6 +206,46 @@ class OldExpr : Expression String? at; } +class DatatypeValue : Expression +{ + String datatypeName; + String memberName; + ActualBindings bindings; +} + +abstract class NodeWithoutOrigin : Node +{ +} + +class ModuleQualifiedId : NodeWithoutOrigin +{ + List path; +} + +class Name : Node +{ + IOrigin origin; + String value; +} + +class Specification : NodeWithoutOrigin where T : Node +{ + List? expressions; + Attributes? attributes; +} + +class ActualBinding : NodeWithoutOrigin +{ + IOrigin? formalParameterName; + Expression actual; + Boolean isGhost; +} + +class ActualBindings : NodeWithoutOrigin +{ + List argumentBindings; +} + class TernaryExpr : Expression { TernaryExprOpcode op; @@ -328,39 +368,6 @@ class AllocateClass : TypeRhs ActualBindings? bindings; } -abstract class NodeWithoutOrigin : Node -{ -} - -class ModuleQualifiedId : NodeWithoutOrigin -{ - List path; -} - -class Name : Node -{ - IOrigin origin; - String value; -} - -class Specification : NodeWithoutOrigin where T : Node -{ - List? expressions; - Attributes? attributes; -} - -class ActualBinding : NodeWithoutOrigin -{ - IOrigin? formalParameterName; - Expression actual; - Boolean isGhost; -} - -class ActualBindings : NodeWithoutOrigin -{ - List argumentBindings; -} - class AllocateArray : TypeRhs { Type? explicitType; From 0b87be38cec8f9ac6a18ef0faba40cdba8251fa7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 2 Sep 2025 11:52:36 +0200 Subject: [PATCH 12/12] Refactor --- .../NameResolutionAndTypeInference.cs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 91ca77576a7..7a5c2aa900e 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4222,12 +4222,14 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo t.ResolvedClass = d; // Store the decl, so the compiler will generate the fully qualified name } else if (d is RedirectingTypeDecl) { var dd = (RedirectingTypeDecl)d; - var caller = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) as ICallable; - if (caller != null && !(d is SubsetTypeDecl && caller is SpecialFunction)) { - if (caller != d) { - } else if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) { - // detect self-loops here, since they don't show up in the graph's SCC methods - reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); + var parent = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) as ICallable; + if (parent != null && !(d is SubsetTypeDecl && parent is SpecialFunction)) { + var cycleFound = parent == d; + if (cycleFound) { + if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) { + // detect self-loops here, since they don't show up in the graph's SCC methods + reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); + } } } t.ResolvedClass = d;