Merge branch 'master' into fix-4952

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -184,6 +184,13 @@ public enum GeneralTraitsOptions {
     IsHidden = true
   };
 
+  public static readonly Option<bool> 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<bool> 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<PrintModes> option, Boogie.CommandLineParseState ps,
       ManualLemmaInduction,
       TypeInferenceDebug,
       GeneralTraits,
+      GeneralNewtypes,
       TypeSystemRefresh,
       VerificationLogFormat,
       VerifyIncludedFiles,

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,

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

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)

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

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

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:<value>
+      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:<value>
       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.

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.
-