fix: Set/forall comprehensions with subtyping for issue #697

Source/Dafny/AST/DafnyAst.cs

@@ -5573,7 +5573,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport {
  FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
 
  bool ICodeContext.IsGhost {
- get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper
+ get { return false; }
  }
  List<TypeParameter> ICodeContext.TypeArgs { get { return new List<TypeParameter>(); } }
  List<Formal> ICodeContext.Ins { get { return new List<Formal>(); } }
@@ -5656,7 +5656,7 @@ public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
  FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } }
 
  bool ICodeContext.IsGhost {
- get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper
+ get { return false; }
  }
  List<TypeParameter> ICodeContext.TypeArgs { get { return TypeArgs; } }
  List<Formal> ICodeContext.Ins { get { return new List<Formal>(); } }
@@ -5703,6 +5703,8 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl {
  public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special }
  public readonly SubsetTypeDecl.WKind WitnessKind;
  public readonly Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost
+ public bool ConstraintIsCompilable = false; // Will be resolved later.
+ public bool CheckedIfConstraintIsCompilable = false; // Will be resolved later.
  public SubsetTypeDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, ModuleDefinition module,
  BoundVar id, Expression constraint, WKind witnessKind, Expression witness,
  Attributes attributes)

Source/Dafny/Compilers/Compiler.cs

@@ -4610,14 +4610,13 @@ void writeObj(ConcreteSyntaxTree w) {
  wBody.Write(", {0}, ", expr is ForallExpr ? "true" : "false");
  var native = AsNativeType(e.BoundVars[i].Type);
  ConcreteSyntaxTree newWBody = CreateLambda(new List<Type> { bv.Type }, e.tok, new List<string> { IdName(bv) }, Type.Bool, wBody, untyped: true);
- newWBody = EmitReturnExpr(newWBody);
+ newWBody = MaybeInjectSubsetConstraint(newWBody, inLetExprBody, e.BoundVars[i], e, true, e is ForallExpr);
  wBody.Write(')');
  wBody = newWBody;
  }
  TrExpr(logicalBody, wBody, true);
 
- } else if (expr is SetComprehension) {
- var e = (SetComprehension)expr;
+ } else if (expr is SetComprehension setComprehension) {
  // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like:
  // ((System.Func<Set<G>>)(() => {
  // var _coll = new List<G>();
@@ -4634,29 +4633,33 @@ void writeObj(ConcreteSyntaxTree w) {
  // }
  // return Dafny.Set<G>.FromCollection(_coll);
  // }))()
- wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr);
- e = (SetComprehension)su.Substitute(e);
+ wr = CaptureFreeVariables(setComprehension, true, out var su, inLetExprBody, wr);
+ setComprehension = (SetComprehension)su.Substitute(setComprehension);
 
- Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
+ Contract.Assert(setComprehension.Bounds != null); // the resolver would have insisted on finding bounds
  var collectionName = idGenerator.FreshId("_coll");
- var bwr = CreateIIFE0(e.Type.AsSetType, e.tok, wr);
+ var bwr = CreateIIFE0(setComprehension.Type.AsSetType, setComprehension.tok, wr);
  wr = bwr;
- EmitSetBuilder_New(wr, e, collectionName);
- var n = e.BoundVars.Count;
- Contract.Assert(e.Bounds.Count == n);
- for (var i = 0; i < n; i++) {
- var bound = e.Bounds[i];
- var bv = e.BoundVars[i];
+ EmitSetBuilder_New(wr, setComprehension, collectionName);
+ var n = setComprehension.BoundVars.Count;
+ Contract.Assert(setComprehension.Bounds.Count == n);
+ int i;
+ for (i = 0; i < n; i++) {
+ var bound = setComprehension.Bounds[i];
+ var bv = setComprehension.BoundVars[i];
  ConcreteSyntaxTree collectionWriter;
  var tmpVar = idGenerator.FreshId("_compr_");
  wr = CreateForeachLoop(tmpVar, GetCollectionEnumerationType(bound, bv), IdName(bv), bv.Type, true, bv.tok, out collectionWriter, wr);
+ // var s = {List(Cell(1)), List(Cell(2), Cell(4)), List(Cell(2), Cell(3))};
+ // set x: List<EvenCell> | x in s 
+ wr = MaybeInjectSubsetConstraint(wr, inLetExprBody, bv, setComprehension);
  CompileCollection(bound, bv, inLetExprBody, true, null, collectionWriter);
  }
  ConcreteSyntaxTree guardWriter;
  var thn = EmitIf(out guardWriter, false, wr);
- TrExpr(e.Range, guardWriter, inLetExprBody);
- EmitSetBuilder_Add(e.Type.AsSetType, collectionName, e.Term, inLetExprBody, thn);
- var s = GetCollectionBuilder_Build(e.Type.AsSetType, e.tok, collectionName, wr);
+ TrExpr(setComprehension.Range, guardWriter, inLetExprBody);
+ EmitSetBuilder_Add(setComprehension.Type.AsSetType, collectionName, setComprehension.Term, inLetExprBody, thn);
+ var s = GetCollectionBuilder_Build(setComprehension.Type.AsSetType, setComprehension.tok, collectionName, wr);
  EmitReturnExpr(s, bwr);
 
  } else if (expr is MapComprehension) {
@@ -4695,6 +4698,7 @@ void writeObj(ConcreteSyntaxTree w) {
  ConcreteSyntaxTree collectionWriter;
  var tmpVar = idGenerator.FreshId("_compr_");
  wr = CreateForeachLoop(tmpVar, GetCollectionEnumerationType(bound, bv), IdName(bv), bv.Type, true, bv.tok, out collectionWriter, wr);
+ wr = MaybeInjectSubsetConstraint(wr, inLetExprBody, bv, e);
  CompileCollection(bound, bv, inLetExprBody, true, null, collectionWriter);
  }
  ConcreteSyntaxTree guardWriter;
@@ -4736,6 +4740,52 @@ void writeObj(ConcreteSyntaxTree w) {
  }
  }
 
+ private ConcreteSyntaxTree MaybeInjectSubsetConstraint(ConcreteSyntaxTree wr, bool inLetExprBody, BoundVar bv,
+ Expression e, bool isReturning = false, bool elseReturnValue = false) {
+ int i;
+ if (bv.Type is UserDefinedType
+ {
+ TypeArgs: var typeArgs,
+ ResolvedClass:
+ var subsetTypeDecl and
+ SubsetTypeDecl
+ {
+ TypeArgs: var typeParametersArgs,
+ Var: var var,
+ ConstraintIsCompilable: true,
+ Constraint: var constraint
+ }
+ }) {
+ var bvIdentifier = new IdentifierExpr(e.tok, bv);
+ var typeParameters = new Dictionary<TypeParameter, Type> { };
+ for (i = 0; i < typeParametersArgs.Count(); i++) {
+ typeParameters[typeParametersArgs[i]] = typeArgs[i];
+ }
+ var subContract = new Substituter(null,
+ new Dictionary<IVariable, Expression>()
+ {
+ {var, bvIdentifier}
+ },
+ new Dictionary<TypeParameter, Type>(
+ typeParameters
+ )
+ );
+ var constraintInContext = subContract.Substitute(constraint);
+ var thenWriter = EmitIf(out var guardWriter, isReturning, wr);
+ TrExpr(constraintInContext, guardWriter, inLetExprBody);
+ if (isReturning) {
+ wr = EmitReturnExpr(wr);
+ TrExpr(new LiteralExpr(e.tok, elseReturnValue), wr, inLetExprBody);
+ thenWriter = EmitReturnExpr(thenWriter);
+ }
+ wr = thenWriter;
+ } else if (isReturning) {
+ wr = EmitReturnExpr(wr);
+ }
+
+ return wr;
+ }
+
  protected ConcreteSyntaxTree CaptureFreeVariables(Expression expr, bool captureOnlyAsRequiredByTargetLanguage, out Substituter su, bool inLetExprBody, ConcreteSyntaxTree wr) {
  if (captureOnlyAsRequiredByTargetLanguage && TargetLambdaCanUseEnclosingLocals) {
  // nothing to do