fix: Fill in missing type substitutions

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -825,8 +825,8 @@ public static IEnumerable<TopLevelDeclWithMembers> AllTypesWithMembers(List<TopL
   /// declarations.
   /// Note, an iterator declaration is a type, in this sense.
   /// Note, if the given list are the top-level declarations of a module, the yield will include
-  /// greatest lemmas but not their associated prefix lemmas (which are tucked into the greatest lemma's
-  /// .PrefixLemma field).
+  /// extreme predicates/lemmas but not their associated prefix predicates/lemmas (which are tucked
+  /// into the extreme predicate/lemma's PrefixPredicate/PrefixLemma field).
   /// </summary>
   public static IEnumerable<ICallable> AllCallables(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
@@ -845,6 +845,21 @@ public static IEnumerable<ICallable> AllCallables(List<TopLevelDecl> declaration
     }
   }
 
+  /// <summary>
+  /// Yields all functions and methods that are members of some type in the given list of
+  /// declarations, including prefix lemmas and prefix predicates.
+  /// </summary>
+  public static IEnumerable<ICallable> AllCallablesIncludingPrefixDeclarations(List<TopLevelDecl> declarations) {
+    foreach (var decl in AllCallables(declarations)) {
+      yield return decl;
+      if (decl is ExtremeLemma extremeLemma) {
+        yield return extremeLemma.PrefixLemma;
+      } else if (decl is ExtremePredicate extremePredicate) {
+        yield return extremePredicate.PrefixPredicate;
+      }
+    }
+  }
+
   /// <summary>
   /// Yields all functions and methods that are members of some non-iterator type in the given
   /// list of declarations, as well as any IteratorDecl's in that list.

Source/DafnyCore/Resolver.cs

@@ -2290,50 +2290,50 @@ void RegisterMembers(ModuleDefinition moduleDef, TopLevelDeclWithMembers cl,
             reporter.Info(MessageSource.Resolver, m.tok, string.Format("_k: {0}", k.Type));
             formals.Add(k);
             if (m is ExtremePredicate) {
-              var cop = (ExtremePredicate)m;
-              formals.AddRange(cop.Formals.ConvertAll(cloner.CloneFormal));
+              var extremePredicate = (ExtremePredicate)m;
+              formals.AddRange(extremePredicate.Formals.ConvertAll(cloner.CloneFormal));
 
-              List<TypeParameter> tyvars = cop.TypeArgs.ConvertAll(cloner.CloneTypeParam);
+              List<TypeParameter> tyvars = extremePredicate.TypeArgs.ConvertAll(cloner.CloneTypeParam);
 
               // create prefix predicate
-              cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.HasStaticKeyword,
+              extremePredicate.PrefixPredicate = new PrefixPredicate(extremePredicate.tok, extraName, extremePredicate.HasStaticKeyword,
                 tyvars, k, formals,
-                cop.Req.ConvertAll(cloner.CloneAttributedExpr),
-                cop.Reads.ConvertAll(cloner.CloneFrameExpr),
-                cop.Ens.ConvertAll(cloner.CloneAttributedExpr),
-                new Specification<Expression>(new List<Expression>() { new IdentifierExpr(cop.tok, k.Name) }, null),
-                cop.Body,
+                extremePredicate.Req.ConvertAll(cloner.CloneAttributedExpr),
+                extremePredicate.Reads.ConvertAll(cloner.CloneFrameExpr),
+                extremePredicate.Ens.ConvertAll(cloner.CloneAttributedExpr),
+                new Specification<Expression>(new List<Expression>() { new IdentifierExpr(extremePredicate.tok, k.Name) }, null),
+                cloner.CloneExpr(extremePredicate.Body),
                 null,
-                cop);
-              extraMember = cop.PrefixPredicate;
+                extremePredicate);
+              extraMember = extremePredicate.PrefixPredicate;
               // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles.
-              moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop);
+              moduleDef.CallGraph.AddEdge(extremePredicate.PrefixPredicate, extremePredicate);
             } else {
-              var com = (ExtremeLemma)m;
+              var extremeLemma = (ExtremeLemma)m;
               // _k has already been added to 'formals', so append the original formals
-              formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));
+              formals.AddRange(extremeLemma.Ins.ConvertAll(cloner.CloneFormal));
               // prepend _k to the given decreases clause
               var decr = new List<Expression>();
-              decr.Add(new IdentifierExpr(com.tok, k.Name));
-              decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
+              decr.Add(new IdentifierExpr(extremeLemma.tok, k.Name));
+              decr.AddRange(extremeLemma.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
               // Create prefix lemma.  Note that the body is not cloned, but simply shared.
               // For a greatest lemma, the postconditions are filled in after the greatest lemma's postconditions have been resolved.
               // For a least lemma, the preconditions are filled in after the least lemma's preconditions have been resolved.
-              var req = com is GreatestLemma
-                ? com.Req.ConvertAll(cloner.CloneAttributedExpr)
+              var req = extremeLemma is GreatestLemma
+                ? extremeLemma.Req.ConvertAll(cloner.CloneAttributedExpr)
                 : new List<AttributedExpression>();
-              var ens = com is GreatestLemma
+              var ens = extremeLemma is GreatestLemma
                 ? new List<AttributedExpression>()
-                : com.Ens.ConvertAll(cloner.CloneAttributedExpr);
-              com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.HasStaticKeyword,
-                com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),
-                req, cloner.CloneSpecFrameExpr(com.Mod), ens,
+                : extremeLemma.Ens.ConvertAll(cloner.CloneAttributedExpr);
+              extremeLemma.PrefixLemma = new PrefixLemma(extremeLemma.tok, extraName, extremeLemma.HasStaticKeyword,
+                extremeLemma.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, extremeLemma.Outs.ConvertAll(cloner.CloneFormal),
+                req, cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
                 new Specification<Expression>(decr, null),
                 null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the greatest lemma is known
-                cloner.CloneAttributes(com.Attributes), com);
-              extraMember = com.PrefixLemma;
+                cloner.CloneAttributes(extremeLemma.Attributes), extremeLemma);
+              extraMember = extremeLemma.PrefixLemma;
               // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles.
-              moduleDef.CallGraph.AddEdge(com.PrefixLemma, com);
+              moduleDef.CallGraph.AddEdge(extremeLemma.PrefixLemma, extremeLemma);
             }
 
             extraMember.InheritVisibility(m, false);

Source/DafnyCore/Rewriter.cs

@@ -154,7 +154,7 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {
     internal override void PostCyclicityResolve(ModuleDefinition m) {
       var finder = new Triggers.QuantifierCollector(Reporter);
 
-      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
+      foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(m.TopLevelDecls)) {
         finder.Visit(decl, null);
       }
 

Source/DafnyCore/Substituter.cs

@@ -38,13 +38,19 @@ public virtual Expression Substitute(Expression expr) {
         return new StaticReceiverExpr(e.tok, ty, e.IsImplicit) { Type = ty };
       } else if (expr is LiteralExpr literalExpr) {
         if (literalExpr.Value == null) {
-          return new LiteralExpr(literalExpr.tok) { Type = Resolver.SubstType(literalExpr.Type, typeMap) };
+          var ty = Resolver.SubstType(literalExpr.Type, typeMap);
+          if (ty != literalExpr.Type) {
+            return new LiteralExpr(literalExpr.tok) { Type = ty };
+          }
         } else {
           // nothing to substitute
         }
       } else if (expr is Translator.BoogieWrapper) {
         var e = (Translator.BoogieWrapper)expr;
-        return new Translator.BoogieWrapper(e.Expr, Resolver.SubstType(e.Type, typeMap));
+        var ty = Resolver.SubstType(e.Type, typeMap);
+        if (ty != e.Type) {
+          return new Translator.BoogieWrapper(e.Expr, ty);
+        }
       } else if (expr is WildcardExpr) {
         // nothing to substitute
       } else if (expr is ThisExpr) {
@@ -74,7 +80,7 @@ public virtual Expression Substitute(Expression expr) {
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         List<Expression> newElements = SubstituteExprList(e.Elements);
-        if (newElements != e.Elements || !Resolver.SubstType(e.Type, typeMap).Equals(e.Type)) {
+        if (newElements != e.Elements || Resolver.SubstType(e.Type, typeMap) != e.Type) {
           if (expr is SetDisplayExpr) {
             newExpr = new SetDisplayExpr(expr.tok, ((SetDisplayExpr)expr).Finite, newElements);
           } else if (expr is MultiSetDisplayExpr) {
@@ -96,18 +102,25 @@ public virtual Expression Substitute(Expression expr) {
           }
         }
         var ty = Resolver.SubstType(e.Type, typeMap);
-        if (anyChanges || !ty.Equals(e.Type)) {
+        if (anyChanges || ty != e.Type) {
           newExpr = new MapDisplayExpr(expr.tok, e.Finite, elmts);
         }
       } else if (expr is MemberSelectExpr) {
         var mse = (MemberSelectExpr)expr;
-        Expression substE = Substitute(mse.Obj);
-        MemberSelectExpr fseNew = new MemberSelectExpr(mse.tok, substE, mse.MemberName);
-        fseNew.Member = mse.Member;
-        fseNew.TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass.ConvertAll(t => Resolver.SubstType(t, typeMap));
-        fseNew.TypeApplication_JustMember = mse.TypeApplication_JustMember.ConvertAll(t => Resolver.SubstType(t, typeMap));
-        fseNew.AtLabel = mse.AtLabel ?? oldHeapLabel;
-        newExpr = fseNew;
+        var newObj = Substitute(mse.Obj);
+        var newTypeApplicationAtEnclosingClass = SubstituteTypeList(mse.TypeApplication_AtEnclosingClass);
+        var newTypeApplicationJustMember = SubstituteTypeList(mse.TypeApplication_JustMember);
+        if (newObj != mse.Obj ||
+            newTypeApplicationAtEnclosingClass != mse.TypeApplication_AtEnclosingClass ||
+            newTypeApplicationJustMember != mse.TypeApplication_JustMember) {
+          var fseNew = new MemberSelectExpr(mse.tok, newObj, mse.MemberName) {
+            Member = mse.Member,
+            TypeApplication_AtEnclosingClass = newTypeApplicationAtEnclosingClass,
+            TypeApplication_JustMember = newTypeApplicationJustMember,
+            AtLabel = mse.AtLabel ?? oldHeapLabel
+          };
+          newExpr = fseNew;
+        }
       } else if (expr is SeqSelectExpr) {
         SeqSelectExpr sse = (SeqSelectExpr)expr;
         Expression seq = Substitute(sse.Seq);
@@ -159,13 +172,14 @@ public virtual Expression Substitute(Expression expr) {
         newExpr = new ApplyExpr(e.tok, fn, args, e.CloseParen);
 
       } else if (expr is DatatypeValue) {
-        DatatypeValue dtv = (DatatypeValue)expr;
+        var dtv = (DatatypeValue)expr;
         var newArguments = SubstituteExprList(dtv.Bindings.Arguments); // substitute into the expressions, but drop any binding names (since those are no longer needed)
-        if (newArguments != dtv.Bindings.Arguments) {
-          DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArguments);
-          newDtv.Ctor = dtv.Ctor;  // resolve on the fly (and set newDtv.Type below, at end)
-          newDtv.InferredTypeArgs = Util.Map(dtv.InferredTypeArgs, tt => Resolver.SubstType(tt, typeMap));
-          // ^ Set the correct type arguments to the constructor
+        var newTypeArgs = SubstituteTypeList(dtv.InferredTypeArgs);
+        if (newArguments != dtv.Bindings.Arguments || newTypeArgs != dtv.InferredTypeArgs) {
+          var newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArguments) {
+            Ctor = dtv.Ctor,
+            InferredTypeArgs = newTypeArgs
+          };
           newExpr = newDtv;
         }
 
@@ -209,29 +223,39 @@ public virtual Expression Substitute(Expression expr) {
       } else if (expr is BoxingCastExpr) {
         var e = (BoxingCastExpr)expr;
         var se = Substitute(e.E);
-        if (se != e.E) {
-          newExpr = new BoxingCastExpr(se, e.FromType, e.ToType);
+        var fromType = Resolver.SubstType(e.FromType, typeMap);
+        var toType = Resolver.SubstType(e.ToType, typeMap);
+        if (se != e.E || fromType != e.FromType || toType != e.ToType) {
+          newExpr = new BoxingCastExpr(se, fromType, toType);
         }
       } else if (expr is UnaryExpr) {
         var e = (UnaryExpr)expr;
-        Expression se = Substitute(e.E);
-        if (se != e.E) {
+        var se = Substitute(e.E);
+        if (e is TypeUnaryExpr typeUnaryExpr) {
+          var toType = Resolver.SubstType(typeUnaryExpr.ToType, typeMap);
+          if (se != e.E || toType != typeUnaryExpr.ToType) {
+            if (e is ConversionExpr) {
+              var ee = (ConversionExpr)e;
+              newExpr = new ConversionExpr(expr.tok, se, toType);
+            } else if (e is TypeTestExpr) {
+              var ee = (TypeTestExpr)e;
+              newExpr = new TypeTestExpr(expr.tok, se, toType);
+            } else {
+              Contract.Assert(false); // unexpected UnaryExpr subtype
+            }
+          }
+        } else if (se != e.E) {
           if (e is FreshExpr) {
             var ee = (FreshExpr)e;
             newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel ?? oldHeapLabel };
           } else if (e is UnaryOpExpr) {
             var ee = (UnaryOpExpr)e;
             newExpr = new UnaryOpExpr(expr.tok, ee.Op, se);
-          } else if (e is ConversionExpr) {
-            var ee = (ConversionExpr)e;
-            newExpr = new ConversionExpr(expr.tok, se, ee.ToType);
-          } else if (e is TypeTestExpr) {
-            var ee = (TypeTestExpr)e;
-            newExpr = new TypeTestExpr(expr.tok, se, ee.ToType);
           } else {
             Contract.Assert(false);  // unexpected UnaryExpr subtype
           }
         }
+
       } else if (expr is BinaryExpr) {
         BinaryExpr e = (BinaryExpr)expr;
         Expression e0 = Substitute(e.E0);

Test/git-issues/git-issue-2947.dfy

@@ -0,0 +1,49 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+codatatype Stream<X> = Nil | Cons(head: X, tail: Stream<X>)
+
+least predicate Finite<Y>(s: Stream<Y>) {
+  // The following once generated malformed Boogie, because of a missing
+  // type substitution in the datatype value Nil
+  s == Nil || Finite(s.tail)
+}
+
+least predicate F0<Y>(s: Stream<Y>) {
+  var nil := Nil;
+  s == nil || F0(s.tail)
+}
+
+least predicate F1<Y>(s: Stream<Y>) {
+  s.Nil? || F1(s.tail)
+}
+
+least predicate G0<Y>(s: Stream<Y>) {
+  s is Stream<Y>
+}
+
+least predicate G1<Y>(s: Stream<Y>) {
+  s == Identity(s)
+}
+
+least predicate G2<Y>(s: Stream<Y>) {
+  s == Identity<Stream<Y>>(s)
+}
+
+function Identity<W>(w: W): W { w }
+
+least lemma About<Z>(s: Stream<Z>)
+  requires s == Nil
+  requires s.Nil?
+  requires var nil := Nil; s == nil
+  requires s is Stream<Z>
+  requires s == Identity(s)
+  requires s == Identity<Stream<Z>>(s)
+  requires Finite(s)
+  requires F0(s)
+  requires F1(s)
+  requires G0(s)
+  requires G1(s)
+  requires G2(s)
+{
+}

Test/git-issues/git-issue-2947.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors

docs/dev/news/2984.fix

@@ -0,0 +1 @@
+Fix malformed Boogie generated for extreme predicates