Merge branch 'master' into add-rust-install-instructions

.github/workflows/check-deep-tests-reusable.yml

@@ -1,6 +1,7 @@
 name: Check Deep Tests (Reusable Workflow)
 
 on:
+  workflow_dispatch:
   workflow_call:
 
 jobs:

.github/workflows/check-for-workflow-run.js

@@ -16,13 +16,18 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
   const runFilterDesc = sha ? `${workflow_id} on ${sha}` : workflow_id
   for (const run of result.data.workflow_runs) {
     if ((!sha || run.head_sha === sha)) {
-      if (run.conclusion === "success") {
-        // The SHA is fully tested, exit with success
-        console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
-        return
-      } else if (run.status === "failure" || run.status === "timed_out") {
-        core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
-        return
+      // The status property can be one of: “queued”, “in_progress”, or “completed”.
+      if (run.status === "completed") {
+        // The conclusion property can be one of:
+        // “success”, “failure”, “neutral”, “cancelled”, “skipped”, “timed_out”, or “action_required”.
+        if (run.conclusion === "success") {
+          // The SHA is fully tested, exit with success
+          console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
+          return
+        } else if (run.conclusion === "failure" || run.conclusion === "timed_out") {
+          core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
+          return
+        }
       }
     }
   }

Source/DafnyCore/AST/Grammar/IndentationFormatter.cs

@@ -23,11 +23,15 @@ public IndentationFormatter(TokenNewIndentCollector formatter) {
   /// Creates an IndentationFormatter for the given program,
   /// by immediately processing all nodes and assigning indentations to most structural tokens 
   /// </summary>
-  public static IndentationFormatter ForProgram(Program program, bool reduceBlockiness = true) {
-    var tokenNewIndentCollector = new TokenNewIndentCollector(program) {
+  public static IndentationFormatter ForProgram(Program program, Uri fileToFormat, bool reduceBlockiness = true) {
+    var tokenNewIndentCollector = new TokenNewIndentCollector(program, fileToFormat) {
       ReduceBlockiness = reduceBlockiness
     };
     foreach (var child in program.DefaultModuleDef.PreResolveChildren) {
+      var isPhysicalToken = child.Tok.line != 0;
+      if (isPhysicalToken && child.Tok.Uri != fileToFormat) {
+        continue;
+      }
       if (child is TopLevelDecl topLevelDecl) {
         tokenNewIndentCollector.SetDeclIndentation(topLevelDecl, 0);
       } else if (child is Include include) {

Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

@@ -83,8 +83,9 @@ private Indentations PosToIndentations(int pos) {
   public int binOpIndent = -1;
   public int binOpArgIndent = -1;
 
-  internal TokenNewIndentCollector(Program program) {
+  internal TokenNewIndentCollector(Program program, Uri fileToFormat) {
     this.program = program;
+    this.fileToFormat = fileToFormat;
     preResolve = true;
   }
 
@@ -222,6 +223,7 @@ public int GetRightAlignIndentAfter(IToken token, int indentFallback) {
   }
 
   private static readonly Regex FollowedByNewlineRegex = new Regex("^[ \t]*([\r\n]|//)");
+  private readonly Uri fileToFormat;
 
   public static bool IsFollowedByNewline(IToken token) {
     return FollowedByNewlineRegex.IsMatch(token.TrailingTrivia);
@@ -231,7 +233,7 @@ public static bool IsFollowedByNewline(IToken token) {
   // 'inline' is the hypothetical indentation of this token if it was on its own line
   // 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation
   public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) {
-    if (token.FromIncludeDirective(program) || (token.line == 0 && token.col == 0)) {
+    if (token.Uri != fileToFormat || (token.line == 0 && token.col == 0)) {
       // Just ignore this token.
       return;
     }

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -170,4 +170,6 @@ public interface RedirectingTypeDecl : ICallable {
   SubsetTypeDecl.WKind WitnessKind { get; }
   Expression/*?*/ Witness { get; }  // non-null iff WitnessKind is Compiled or Ghost
   FreshIdGenerator IdGenerator { get; }
+
+  [FilledInDuringResolution] bool ConstraintIsCompilable { get; set; }
 }

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -103,6 +103,7 @@ public SystemModuleManager(DafnyOptions options) {
     NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"),
       new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
       new List<TypeParameter>(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax);
+    ((RedirectingTypeDecl)NatDecl).ConstraintIsCompilable = true;
     SystemModule.SourceDecls.Add(NatDecl);
     // create trait 'object'
     ObjectDecl = new TraitDecl(RangeToken.NoToken, new Name("object"), SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), false, null);

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -15,6 +15,12 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect
   public SubsetTypeDecl.WKind WitnessKind { get; set; } = SubsetTypeDecl.WKind.CompiledZero;
   public Expression/*?*/ Witness { get; set; } // non-null iff WitnessKind is Compiled or Ghost
   [FilledInDuringResolution] public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers)
+
+  [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; }
+
+  [FilledInDuringResolution] public bool NativeTypeRangeImpliesAllConstraints; // indicates that all values in the range of the native type are values of the newtype
+  [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype
+
   public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List<Type> parentTraits,
     List<MemberDecl> members, Attributes attributes, bool isRefining)
     : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining, parentTraits) {
@@ -24,6 +30,7 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Ty
     Contract.Requires(isRefining ^ (baseType != null));
     Contract.Requires(members != null);
     BaseType = baseType;
+    this.NewSelfSynonym();
   }
   public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint,
     SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -11,8 +11,10 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl, ICanAutoReve
   public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special }
   public readonly WKind WitnessKind;
   public Expression/*?*/ Witness;  // non-null iff WitnessKind is Compiled or Ghost
-  [FilledInDuringResolution] public bool ConstraintIsCompilable;
   [FilledInDuringResolution] public bool CheckedIfConstraintIsCompilable = false; // Set to true lazily by the Resolver when the Resolver fills in "ConstraintIsCompilable".
+
+  [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; }
+
   public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, ModuleDefinition module,
     BoundVar id, Expression constraint, WKind witnessKind, Expression witness,
     Attributes attributes)

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -64,6 +64,12 @@ public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
   ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } }
   BoundVar RedirectingTypeDecl.Var { get { return null; } }
   Expression RedirectingTypeDecl.Constraint { get { return null; } }
+
+  bool RedirectingTypeDecl.ConstraintIsCompilable {
+    get => false;
+    set => throw new NotSupportedException();
+  }
+
   SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return SubsetTypeDecl.WKind.CompiledZero; } }
   Expression RedirectingTypeDecl.Witness { get { return null; } }
   FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -3291,6 +3291,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         } else {
           Contract.Assert(false, $"not implemented for C#: {e.E.Type} -> {e.ToType}");
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for C#: {e.E.Type} -> {e.ToType}");
       }

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -2356,11 +2356,14 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
             wr.Write(".{0}()", Capitalize(GetNativeTypeName(nt)));
           }
         }
-      } else {
-        Contract.Assert(e.E.Type.IsBigOrdinalType);
+      } else if (e.E.Type.IsBigOrdinalType) {
         Contract.Assert(e.ToType.IsNumericBased(Type.NumericPersuasion.Int));
         // identity will do
         wr.Append(Expr(e.E, inLetExprBody, wStmts));
+      } else {
+        // identity will do
+        Contract.Assert(e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null);
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       }
     }
 

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -3576,6 +3576,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
             wr.Write(".{0}()", Capitalize(GetNativeTypeName(nt)));
           }
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for go: {e.E.Type} -> {e.ToType}");
       }

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -4186,6 +4186,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         } else {
           Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}");
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}");
       }

Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs

@@ -2432,6 +2432,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         if (e.ToType.IsCharType) {
           wr.Write(").toNumber())");
         }
+      } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) {
+        wr.Append(Expr(e.E, inLetExprBody, wStmts));
       } else {
         Contract.Assert(false, $"not implemented for javascript: {e.E.Type} -> {e.ToType}");
       }

Source/DafnyCore/Compilers/Python/PythonBackend.cs

@@ -4,6 +4,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using System.Runtime.InteropServices;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -46,6 +47,17 @@ private static string FindModuleName(string externFilename) {
     return Path.GetExtension(externFilename) == ".py" ? Path.GetFileNameWithoutExtension(externFilename) : null;
   }
 
+  private static readonly Dictionary<OSPlatform, string> PlatformDefaults = new() {
+    {OSPlatform.Linux, "python3"},
+    {OSPlatform.Windows, "python"},
+    {OSPlatform.FreeBSD, "python3"},
+    {OSPlatform.OSX, "python3"},
+  };
+  private static string DefaultPythonCommand => PlatformDefaults.SingleOrDefault(
+      kv => RuntimeInformation.IsOSPlatform(kv.Key),
+      new(OSPlatform.Linux, "python3")
+    ).Value;
+
   bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) {
     // Grossly, we need to look in the file to figure out where to put it
     var moduleName = FindModuleName(externFilename);
@@ -88,7 +100,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
       }
     }
     if (!runAfterCompile) {
-      var psi = PrepareProcessStartInfo("python3");
+      var psi = PrepareProcessStartInfo(DefaultPythonCommand);
       psi.Arguments = $"-m compileall -q {Path.GetDirectoryName(targetFilename)}";
       return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling Python files.");
     }
@@ -99,7 +111,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
     string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter,
     TextWriter errorWriter) {
     Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
-    var psi = PrepareProcessStartInfo("python3", Options.MainArgs.Prepend(targetFilename));
+    var psi = PrepareProcessStartInfo(DefaultPythonCommand, Options.MainArgs.Prepend(targetFilename));
     psi.EnvironmentVariables["PYTHONIOENCODING"] = "utf8";
     return 0 == RunProcess(psi, outputWriter, errorWriter);
   }