From 3254d298b2fdb8b4aee4081fd2fb8d661cfd533f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 9 Jan 2024 19:20:39 +0100 Subject: [PATCH 1/2] Update documentation for Dafny server (#4945) Update documentation for Dafny server By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- docs/DafnyRef/VSCodeIDE.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/docs/DafnyRef/VSCodeIDE.md b/docs/DafnyRef/VSCodeIDE.md index 32ad90189a..c4b73f4229 100644 --- a/docs/DafnyRef/VSCodeIDE.md +++ b/docs/DafnyRef/VSCodeIDE.md @@ -73,7 +73,7 @@ the position of the parse or resolution error. ## 14.3. The Dafny Server {#sec-old-dafny-server} -Before Dafny [implemented](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer) the official [Language Server Protocol](https://microsoft.github.io/language-server-protocol/), it implemented its own protocol for [Emacs](https://github.com/boogie-org/boogie-friends), which resulted in a project called [DafnyServer](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyServer). +Before Dafny [implemented](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer) the official [Language Server Protocol](https://microsoft.github.io/language-server-protocol/), it implemented its own protocol for [Emacs](https://github.com/boogie-org/boogie-friends), which resulted in a project called [DafnyServer](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyServer). While the latest Dafny releases still contain a working DafnyServer binary, this component has been feature frozen since 2022, and it may not support features that were added to Dafny after that time. We do not recommend using it. The Dafny Server has [integration tests](https://github.com/dafny-lang/dafny/tree/master/Test/server) that serve as the basis of the documentation. @@ -156,5 +156,3 @@ btoa(JSON.stringify({ Thus to decode such output, you'd manually use `JSON.parse(atob(payload))`. -The Dafny Server is still supported, but we recommend using the [Language Server](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer) instead. It is supported in [VSCode](https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode) only. The Language Server also provides features such as ghost highlighting or symbol hovering. - From 4080fae8a6f5e98c89631eb276d6f33e6dadac21 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 9 Jan 2024 11:15:59 -0800 Subject: [PATCH 2/2] Introduce --general-newtypes option (#4932) This PR adds a CLI option to prepare for other PRs that will fill in what this CLI option will do. In the new resolver, the PR also adds checks that make sure the `newtype` base type is allowed. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/Options/CommonOptionBag.cs | 11 +++++++++++ Source/DafnyCore/Options/DafnyCommands.cs | 1 + .../DafnyCore/Resolver/PreType/PreTypeConstraints.cs | 6 ++++++ Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs | 7 +++++++ .../LitTest/dafny0/OnDemandResolutionCycle.dfy.expect | 3 ++- .../LitTest/git-issues/git-issue-2134.dfy.expect | 6 +++++- docs/DafnyRef/Options.txt | 4 ++++ 7 files changed, 36 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 5f01140691..11de3dee37 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -184,6 +184,13 @@ public enum GeneralTraitsOptions { IsHidden = true }; + public static readonly Option GeneralNewtypes = new("--general-newtypes", () => false, + @" +false - A newtype can only be based on numeric types or another newtype. +true - (requires --type-system-refresh to have any effect) A newtype case be based on any non-reference, non-trait, non-ORDINAL type.".TrimStart()) { + IsHidden = true + }; + public static readonly Option TypeInferenceDebug = new("--type-inference-trace", () => false, @" false - Don't print type-inference debug information. @@ -343,6 +350,9 @@ datatype with a single non-ghost constructor that has a single legacy (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits. datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits. full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.".TrimStart()); + DafnyOptions.RegisterLegacyUi(GeneralNewtypes, DafnyOptions.ParseBoolean, "Language feature selection", "generalNewtypes", @" +0 (default) - A newtype can only be based on numeric types or another newtype. +1 - (requires /typeSystemRefresh:1 to have any effect) A newtype case be based on any non-reference, non-trait, non-ORDINAL type.".TrimStart(), false); DafnyOptions.RegisterLegacyUi(TypeInferenceDebug, DafnyOptions.ParseBoolean, "Language feature selection", "titrace", @" 0 (default) - Don't print type-inference debug information. 1 - Print type-inference debug information.".TrimStart(), defaultValue: false); @@ -522,6 +532,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, ManualLemmaInduction, TypeInferenceDebug, GeneralTraits, + GeneralNewtypes, TypeSystemRefresh, VerificationLogFormat, VerifyIncludedFiles, diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 9f7f771f86..68b208299a 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -88,6 +88,7 @@ static DafnyCommands() { CommonOptionBag.UnicodeCharacters, CommonOptionBag.UseBaseFileName, CommonOptionBag.GeneralTraits, + CommonOptionBag.GeneralNewtypes, CommonOptionBag.TypeSystemRefresh, CommonOptionBag.TypeInferenceDebug, CommonOptionBag.NewTypeInferenceDebug, diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs index 47537846cf..8033dec95b 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs @@ -520,6 +520,8 @@ public enum CommonConfirmationBag { Sizeable, Freshable, IsCoDatatype, + IsNewtypeBaseTypeLegacy, + IsNewtypeBaseTypeGeneral, }; private bool ConfirmConstraint(CommonConfirmationBag check, PreType preType, DPreType auxPreType) { @@ -629,6 +631,10 @@ private bool ConfirmConstraint(CommonConfirmationBag check, PreType preType, DPr } case CommonConfirmationBag.IsCoDatatype: return ancestorDecl is CoDatatypeDecl; + case CommonConfirmationBag.IsNewtypeBaseTypeLegacy: + return pt.Decl is NewtypeDecl || pt.Decl.Name == "int" || pt.Decl.Name == "real"; + case CommonConfirmationBag.IsNewtypeBaseTypeGeneral: + return pt.Decl is NewtypeDecl || (!DPreType.IsReferenceTypeDecl(pt.Decl) && pt.Decl is not TraitDecl && pt.Decl.Name != "ORDINAL"); default: Contract.Assert(false); // unexpected case diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 96f1df3309..43b369bcbc 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -691,6 +691,13 @@ void ComputePreTypeMethod(Method method) { Contract.Assert(object.ReferenceEquals(nd.BaseType, nd.Var.Type)); nd.Var.PreType = nd.BasePreType; } + if (resolver.Options.Get(CommonOptionBag.GeneralNewtypes)) { + AddConfirmation(PreTypeConstraints.CommonConfirmationBag.IsNewtypeBaseTypeGeneral, nd.BasePreType, nd.tok, + "a newtype must be based on some non-reference, non-trait, non-ORDINAL type (got {0})"); + } else { + AddConfirmation(PreTypeConstraints.CommonConfirmationBag.IsNewtypeBaseTypeLegacy, nd.BasePreType, nd.tok, + "a newtype must be based on some numeric type (got {0})"); + } ResolveConstraintAndWitness(nd, true); // fill in the members inherited from the ancestor built-in type (but be careful, since there may still be cycles among these declarations) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OnDemandResolutionCycle.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OnDemandResolutionCycle.dfy.expect index f09702ef5a..7d41039ebc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OnDemandResolutionCycle.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OnDemandResolutionCycle.dfy.expect @@ -3,10 +3,11 @@ OnDemandResolutionCycle.dfy(9,9): Error: Cyclic dependency among declarations: F OnDemandResolutionCycle.dfy(7,5): Error: Cyclic dependency among declarations: B -> B -> FB -> b OnDemandResolutionCycle.dfy(11,6): Error: Cyclic dependency among declarations: c0 -> c1 -> c0 OnDemandResolutionCycle.dfy(15,6): Error: Cyclic dependency among declarations: d -> D -> d +OnDemandResolutionCycle.dfy(14,8): Error: a newtype must be based on some numeric type (got ?1) OnDemandResolutionCycle.dfy(19,9): Error: Cyclic dependency among declarations: FE -> E -> FE -> e OnDemandResolutionCycle.dfy(17,8): Error: Cyclic dependency among declarations: E -> E -> FE -> e OnDemandResolutionCycle.dfy(22,9): Error: Cyclic dependency among declarations: f -> F -> f OnDemandResolutionCycle.dfy(21,8): Error: Cyclic dependency among declarations: F -> F -> f OnDemandResolutionCycle.dfy(24,6): Error: Cyclic dependency among declarations: g -> g OnDemandResolutionCycle.dfy(15,14): Error: integer literal used as if it had type D -11 resolution/type errors detected in OnDemandResolutionCycle.dfy +12 resolution/type errors detected in OnDemandResolutionCycle.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy.expect index 254330a420..ac4b138740 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy.expect @@ -1,7 +1,11 @@ git-issue-2134.dfy(8,12): Error: Cyclic dependency among declarations: P -> A -> B -> P +git-issue-2134.dfy(5,10): Error: a newtype must be based on some numeric type (got ?1) git-issue-2134.dfy(15,12): Error: Cyclic dependency among declarations: P -> A -> Q -> B -> P +git-issue-2134.dfy(12,10): Error: a newtype must be based on some numeric type (got ?1) git-issue-2134.dfy(22,12): Error: Cyclic dependency among declarations: P -> B -> P +git-issue-2134.dfy(20,10): Error: a newtype must be based on some numeric type (got ?1) git-issue-2134.dfy(27,8): Error: Cyclic dependency among declarations: X -> B -> X +git-issue-2134.dfy(26,10): Error: a newtype must be based on some numeric type (got ?1) git-issue-2134.dfy(32,11): Error: Cyclic dependency among declarations: X -> B -> X git-issue-2134.dfy(31,10): Error: Cyclic dependency among declarations: B -> B -> X git-issue-2134.dfy(41,12): Error: Cyclic dependency among declarations: P -> A -> B -> P @@ -10,4 +14,4 @@ git-issue-2134.dfy(55,12): Error: Cyclic dependency among declarations: P -> B - git-issue-2134.dfy(60,8): Error: Cyclic dependency among declarations: X -> B -> X git-issue-2134.dfy(65,11): Error: Cyclic dependency among declarations: X -> B -> X git-issue-2134.dfy(64,7): Error: Cyclic dependency among declarations: B -> B -> X -12 resolution/type errors detected in git-issue-2134.dfy +16 resolution/type errors detected in git-issue-2134.dfy diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 00c04d811f..405096d585 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -105,6 +105,10 @@ Usage: dafny [ option ... ] [ filename ... ] `autoRevealDependencies` makes all functions not explicitly labelled as opaque to be opaque but reveals them automatically in scopes which do not have `{:autoRevealDependencies false}`. `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof. + /generalNewtypes: + 0 (default) - A newtype can only be based on numeric types or another newtype. + 1 - (requires /typeSystemRefresh:1 to have any effect) A newtype case be based on any non-reference, non-trait, non-ORDINAL type. + /generalTraits: legacy (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits. datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.