Merge branch 'master' into fix-3216-could-not-prove

.github/workflows/msbuild.yml

@@ -55,7 +55,7 @@ jobs:
       run: dotnet build Source/Dafny.sln
     - name: Check whitespace and style
       working-directory: dafny
-      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs
+      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
     - name: Create NuGet package (just to make sure it works)
       run: dotnet pack --no-build dafny/Source/Dafny.sln
     - name: Check uniformity of integration tests that exercise backends

Makefile

@@ -58,7 +58,7 @@ z3-ubuntu:
 	chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
-	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs
+	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
 
 clean:
 	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -390,7 +390,7 @@ public bool Resolve(ModuleSignature sig, ModuleResolver resolver, bool isAnExpor
           importSig = ((AbstractModuleDecl)d).OriginalSignature;
         }
 
-        if (importSig.ModuleDef is not { SuccessfullyResolved: true }) {
+        if (importSig is not { ModuleDef: { SuccessfullyResolved: true } }) {
           return false;
         }
       } else if (d is LiteralModuleDecl) {

Source/DafnyCore/AST/Tokens.cs

@@ -7,7 +7,7 @@
 
 namespace Microsoft.Dafny;
 
-public interface IToken : Microsoft.Boogie.IToken {
+public interface IToken : Microsoft.Boogie.IToken, IComparable<IToken> {
   public RangeToken To(IToken end) => new RangeToken(this, end);
 
   /*
@@ -121,6 +121,13 @@ public override int GetHashCode() {
   public override string ToString() {
     return $"'{val}': {Path.GetFileName(Filepath)}@{pos} - @{line}:{col}";
   }
+
+  public int CompareTo(IToken other) {
+    if (line != other.line) {
+      return line.CompareTo(other.line);
+    }
+    return col.CompareTo(other.col);
+  }
 }
 
 public abstract class TokenWrapper : IToken {
@@ -183,6 +190,10 @@ public virtual IToken Prev {
     get { return WrappedToken.Prev; }
     set { throw new NotSupportedException(); }
   }
+
+  public int CompareTo(IToken other) {
+    return WrappedToken.CompareTo(other);
+  }
 }
 
 public static class TokenExtensions {

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -31,7 +31,10 @@ public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParame
   }
 
   public override IEnumerable<INode> Children =>
-    base.Children.Concat(new[] { Constraint });
+    base.Children.Concat(new[] { Constraint }).Concat(
+      Witness != null ? new[] { Witness } :
+        Enumerable.Empty<INode>()
+      );
 
   BoundVar RedirectingTypeDecl.Var => Var;
   Expression RedirectingTypeDecl.Constraint => Constraint;

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -3,7 +3,7 @@ module {:extern "DAST"} DAST {
 
   datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)
 
-  datatype Newtype = Newtype(name: string, base: Type, witnessExpr: Optional<Expression>)
+  datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Optional<Expression>)
 
   datatype Type =
     Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
@@ -58,7 +58,8 @@ module {:extern "DAST"} DAST {
     New(path: seq<Ident>, args: seq<Expression>) |
     NewArray(dims: seq<Expression>) |
     DatatypeValue(path: seq<Ident>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
-    NewtypeValue(tpe: Type, value: Expression) |
+    SubsetUpgrade(value: Expression, typ: Type) |
+    SubsetDowngrade(value: Expression) |
     SeqValue(elements: seq<Expression>) |
     SetValue(elements: seq<Expression>) |
     This() |
@@ -69,7 +70,7 @@ module {:extern "DAST"} DAST {
     SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
     TupleSelect(expr: Expression, index: nat) |
     Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
-    Lambda(params: seq<Formal>, body: seq<Statement>) |
+    Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) |
     IIFE(name: Ident, typ: Type, value: Expression, iifeBody: Expression) |
     Apply(expr: Expression, args: seq<Expression>) |
     TypeTest(on: Expression, dType: seq<Ident>, variant: string) |

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -149,21 +149,25 @@ public object Finish() {
   interface NewtypeContainer {
     void AddNewtype(Newtype item);
 
-    public NewtypeBuilder Newtype(string name, DAST.Type baseType, DAST.Expression witness) {
-      return new NewtypeBuilder(this, name, baseType, witness);
+    public NewtypeBuilder Newtype(string name, List<DAST.Type> typeParams, DAST.Type baseType, List<DAST.Statement> witnessStmts, DAST.Expression witness) {
+      return new NewtypeBuilder(this, name, typeParams, baseType, witnessStmts, witness);
     }
   }
 
   class NewtypeBuilder : ClassLike {
     readonly NewtypeContainer parent;
     readonly string name;
+    readonly List<DAST.Type> typeParams;
     readonly DAST.Type baseType;
+    readonly List<DAST.Statement> witnessStmts;
     readonly DAST.Expression witness;
 
-    public NewtypeBuilder(NewtypeContainer parent, string name, DAST.Type baseType, DAST.Expression witness) {
+    public NewtypeBuilder(NewtypeContainer parent, string name, List<DAST.Type> typeParams, DAST.Type baseType, List<DAST.Statement> statements, DAST.Expression witness) {
       this.parent = parent;
       this.name = name;
+      this.typeParams = typeParams;
       this.baseType = baseType;
+      this.witnessStmts = statements;
       this.witness = witness;
     }
 
@@ -178,7 +182,9 @@ public void AddField(DAST.Formal item) {
     public object Finish() {
       parent.AddNewtype((Newtype)Newtype.create(
         Sequence<Rune>.UnicodeFromString(this.name),
+        Sequence<DAST.Type>.FromArray(this.typeParams.ToArray()),
         this.baseType,
+        Sequence<DAST.Statement>.FromArray(this.witnessStmts.ToArray()),
         this.witness == null ? Optional<DAST._IExpression>.create_None() : Optional<DAST._IExpression>.create_Some(this.witness)
       ));
       return parent;
@@ -699,6 +705,31 @@ public DAST.Statement Build() {
     }
   }
 
+  class StatementBuffer : StatementContainer {
+    readonly List<object> statements = new();
+
+    public void AddStatement(DAST.Statement item) {
+      statements.Add(item);
+    }
+
+    public void AddBuildable(BuildableStatement item) {
+      statements.Add(item);
+    }
+
+    public List<object> ForkList() {
+      var ret = new List<object>();
+      statements.Add(ret);
+      return ret;
+    }
+
+    public List<DAST.Statement> PopAll() {
+      var builtResult = new List<DAST.Statement>();
+      StatementContainer.RecursivelyBuild(statements, builtResult);
+
+      return builtResult;
+    }
+  }
+
   class ExprBuffer : ExprContainer {
     Stack<object> exprs = new();
     public readonly object parent;
@@ -761,8 +792,8 @@ CallExprBuilder Call() {
       return ret;
     }
 
-    LambdaExprBuilder Lambda(List<DAST.Formal> formals) {
-      var ret = new LambdaExprBuilder(formals);
+    LambdaExprBuilder Lambda(List<DAST.Formal> formals, DAST.Type retType) {
+      var ret = new LambdaExprBuilder(formals, retType);
       AddBuildable(ret);
       return ret;
     }
@@ -773,6 +804,18 @@ IIFEExprBuilder IIFE(string name, DAST.Type tpe) {
       return ret;
     }
 
+    SubsetUpgradeBuilder SubsetUpgrade(DAST.Type tpe) {
+      var ret = new SubsetUpgradeBuilder(tpe);
+      AddBuildable(ret);
+      return ret;
+    }
+
+    SubsetDowngradeBuilder SubsetDowngrade() {
+      var ret = new SubsetDowngradeBuilder();
+      AddBuildable(ret);
+      return ret;
+    }
+
     protected static void RecursivelyBuild(List<object> body, List<DAST.Expression> builtExprs) {
       foreach (var maybeBuilt in body) {
         if (maybeBuilt is DAST.Expression built) {
@@ -886,10 +929,12 @@ public DAST.Expression Build() {
 
 class LambdaExprBuilder : StatementContainer, BuildableExpr {
   readonly List<DAST.Formal> formals;
+  readonly DAST.Type retType;
   readonly List<object> body = new();
 
-  public LambdaExprBuilder(List<DAST.Formal> formals) {
+  public LambdaExprBuilder(List<DAST.Formal> formals, DAST.Type retType) {
     this.formals = formals;
+    this.retType = retType;
   }
 
   public void AddStatement(DAST.Statement item) {
@@ -912,6 +957,7 @@ public DAST.Expression Build() {
 
     return (DAST.Expression)DAST.Expression.create_Lambda(
       Sequence<DAST.Formal>.FromArray(formals.ToArray()),
+      retType,
       Sequence<DAST.Statement>.FromArray(builtBody.ToArray())
     );
   }
@@ -988,3 +1034,67 @@ public void AddBuildable(BuildableExpr item) {
     }
   }
 }
+
+class SubsetUpgradeBuilder : ExprContainer, BuildableExpr {
+  readonly DAST.Type tpe;
+  object value = null;
+
+  public SubsetUpgradeBuilder(DAST.Type tpe) {
+    this.tpe = tpe;
+  }
+
+  public void AddExpr(DAST.Expression item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public void AddBuildable(BuildableExpr item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public DAST.Expression Build() {
+    var builtValue = new List<DAST.Expression>();
+    ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
+
+    return (DAST.Expression)DAST.Expression.create_SubsetUpgrade(
+      builtValue[0],
+      tpe
+    );
+  }
+}
+
+class SubsetDowngradeBuilder : ExprContainer, BuildableExpr {
+  object value = null;
+
+  public void AddExpr(DAST.Expression item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public void AddBuildable(BuildableExpr item) {
+    if (value != null) {
+      throw new InvalidOperationException();
+    } else {
+      value = item;
+    }
+  }
+
+  public DAST.Expression Build() {
+    var builtValue = new List<DAST.Expression>();
+    ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
+
+    return (DAST.Expression)DAST.Expression.create_SubsetDowngrade(
+      builtValue[0]
+    );
+  }
+}