diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index b096b892a62..9b9d6d5558d 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -8299,6 +8299,41 @@ public override IEnumerable NonSpecificationSubExpressions { } } + public class ForeachLoopStmt : OneBodyLoopStmt { + public readonly List BoundVars; // note, can be the empty list, in which case Range denotes "true" + public Expression Range; // mostly readonly, except that it may in some cases be updated during resolution to conjoin the precondition of the call in the body + + public List Bounds; // initialized and filled in by resolver + // invariant: if successfully resolved, Bounds.Count == BoundVars.Count; + + + public ForeachLoopStmt(IToken tok, IToken endTok, List boundVars, Attributes attrs, Expression range, + List invariants, Specification decreases, Specification mod, + BlockStmt /*?*/ body) + : base(tok, endTok, invariants, decreases, mod, body, attrs) { + // TODO: double check these + Contract.Requires(tok != null); + Contract.Requires(endTok != null); + Contract.Requires(cce.NonNullElements(boundVars)); + Contract.Requires(range != null); + Contract.Requires(boundVars.Count != 0 || LiteralExpr.IsTrue(range)); + this.BoundVars = boundVars; + this.Range = range; + } + + public List UnenumerableBoundVars() { + Contract.Ensures(Contract.Result>() != null); + var v = ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable; + return ComprehensionExpr.BoundedPool.MissingBounds(BoundVars, Bounds, v); + } + + public List InfiniteBoundVars() { + Contract.Ensures(Contract.Result>() != null); + var v = ComprehensionExpr.BoundedPool.PoolVirtues.Finite; + return ComprehensionExpr.BoundedPool.MissingBounds(BoundVars, Bounds, v); + } + } + public class AlternativeLoopStmt : LoopStmt { public readonly bool UsesOptionalBraces; public readonly List Alternatives; @@ -11809,10 +11844,8 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) { } } - public class SetComprehension : ComprehensionExpr { - public override string WhatKind => "set comprehension"; - - public readonly bool Finite; + public class CollectionComprehension : ComprehensionExpr { + public virtual bool Finite => true; public readonly bool TermIsImplicit; // records the given syntactic form public bool TermIsSimple { get { @@ -11824,7 +11857,7 @@ public bool TermIsSimple { } } - public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) + public CollectionComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) : base(tok, endTok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); @@ -11833,9 +11866,31 @@ public SetComprehension(IToken tok, IToken endTok, bool finite, List b Contract.Requires(term != null || bvars.Count == 1); TermIsImplicit = term == null; - Finite = finite; } } + + public class SetComprehension : CollectionComprehension { + public override string WhatKind => "set comprehension"; + + public override bool Finite => finite; + private readonly bool finite; + + public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression /*?*/ term, Attributes attrs) + : base(tok, endTok, bvars, range, term, attrs) { + this.finite = finite; + } + } + + public class SeqComprehension : CollectionComprehension { + public override string WhatKind => "seq comprehension"; + + public override bool Finite => true; + + public SeqComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) + : base(tok, endTok, bvars, range, term, attrs) { + } + } + public class MapComprehension : ComprehensionExpr { public override string WhatKind => "map comprehension"; diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 76b2e0bb08c..6dedbd73af8 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -433,6 +433,8 @@ public virtual Expression CloneExpr(Expression expr) { return new MapComprehension(tk, tkEnd, mc.Finite, bvs, range, mc.TermLeft == null ? null : CloneExpr(mc.TermLeft), term, CloneAttributes(e.Attributes)); } else if (e is LambdaExpr l) { return new LambdaExpr(tk, tkEnd, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term); + } else if (e is SeqComprehension sc) { + return new SeqComprehension(tk, tkEnd, bvs, range, sc.TermIsImplicit ? null : term, CloneAttributes(e.Attributes)); } else { Contract.Assert(e is SetComprehension); var tt = (SetComprehension)e; diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 544331b95ef..316c7939c57 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -2572,6 +2572,7 @@ OneStmt | IfStmt | WhileStmt | ForLoopStmt + | ForeachLoopStmt | AssertStmt | AssumeStmt | BreakStmt @@ -3363,6 +3364,35 @@ ForallStmt .) . +/*------------------------------------------------------------------------*/ +ForeachLoopStmt += (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); + IToken/*!*/ x = Token.NoToken; + List bvars = null; + Attributes qattrs = null; + Expression range = null; + List invariants = new List(); + List decreases = new List(); + Attributes decAttrs = null; + Attributes modAttrs = null; + List mod = null; + BlockStmt block = null; + IToken bodyStart, bodyEnd; + IToken tok = Token.NoToken; + .) + "foreach" (. x = t; tok = x; .) + + QuantifierDomain + (. if (range == null) { range = new LiteralExpr(x, true); } + .) + LoopSpec + BlockStmt + (. s = new ForeachLoopStmt(x, block.EndTok, bvars, qattrs, range, + invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), + block); + .) + . + /*------------------------------------------------------------------------*/ ModifyStmt = (. IToken tok; IToken endTok = Token.NoToken; @@ -4080,34 +4110,13 @@ SetDisplayExpr SeqDisplayExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken x = null; - Type explicitTypeArg = null; - Expression n, f; - e = dummyExpr; .) - ( - "seq" (. x = t; .) - [ (. var gt = new List(); .) - GenericInstantiation (. if (gt.Count > 1) { - SemErr("seq type expects only one type argument"); - } else { - explicitTypeArg = gt[0]; - } - .) - ] - "(" - Expression - "," - Expression - ")" (. e = new SeqConstructionExpr(x, explicitTypeArg, n, f); .) - | - "[" (. List elements = new List(); - x = t; - - .) - [ Expressions ] (. e = new SeqDisplayExpr(x, elements); - .) - "]" - ) + "[" (. List elements = new List(); + x = t; + .) + [ Expressions ] (. e = new SeqDisplayExpr(x, elements); + .) + "]" . /*------------------------------------------------------------------------*/ @@ -4173,6 +4182,7 @@ EndlessExpression | QuantifierExpression /* types are such that we can allow bitwise operations in the quantifier body */ | SetComprehensionExpr + | SeqComprehensionExpr | StmtInExpr Expression (. e = new StmtExpr(s.Tok, s, e); .) | LetExpression @@ -4685,6 +4695,53 @@ SetComprehensionExpr += (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); + Type explicitTypeArg = null; + Expression n, f; + BoundVar bv; + List bvars = new List(); + Expression range; + Expression body = null; + Attributes attrs = null; + q = dummyExpr; + .) + "seq" (. IToken seqToken = t; .) + ( + [ (. var gt = new List(); .) + GenericInstantiation (. if (gt.Count > 1) { + SemErr("seq type expects only one type argument"); + } else { + explicitTypeArg = gt[0]; + } + .) + ] + "(" + Expression + "," + Expression + ")" (. q = new SeqConstructionExpr(seqToken, explicitTypeArg, n, f); .) + | + IdentTypeOptional (. bvars.Add(bv); .) + { "," + IdentTypeOptional (. bvars.Add(bv); .) + } + { Attribute } + "|" Expression + [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ + QSep + Expression + ] + (. if (body == null && bvars.Count != 1) { + SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); + } else { + q = new SeqComprehension(seqToken, t, bvars, range, body, attrs); + } + .) + ) + . /*------------------------------------------------------------------------*/ Expressions<.List args.> diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7058d28004a..92ff4941370 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6640,6 +6640,12 @@ protected override void VisitOneStmt(Statement stmt) { s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable); s.BoundVars.Iter(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.Type)); + } else if (stmt is ForeachLoopStmt) { + var s = (ForeachLoopStmt)stmt; + s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); + s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable); + s.BoundVars.Iter(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.Type)); + } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; if (s.AssumeToken == null) { @@ -6711,8 +6717,8 @@ protected override void VisitOneExpr(Expression expr) { if (e is QuantifierExpr quantifierExpr) { whereToLookForBounds = quantifierExpr.LogicalBody(); polarity = quantifierExpr is ExistsExpr; - } else if (e is SetComprehension setComprehension) { - whereToLookForBounds = setComprehension.Range; + } else if (e is CollectionComprehension) { + whereToLookForBounds = e.Range; } else if (e is MapComprehension) { whereToLookForBounds = e.Range; } else { @@ -7042,6 +7048,8 @@ protected override void VisitOneStmt(Statement stmt) { resolver.CheckLocalityUpdates(astmt.Proof, new HashSet(), "an assert-by body"); } else if (stmt is ForallStmt forall && forall.Body != null) { resolver.CheckLocalityUpdates(forall.Body, new HashSet(), "a forall statement"); + } else if (stmt is ForeachLoopStmt foreachS && foreachS.Body != null) { + resolver.CheckLocalityUpdates(foreachS.Body, new HashSet(), "a foreach loop"); } } } @@ -8090,6 +8098,18 @@ protected override bool VisitOneStmt(Statement stmt, ref bool inGhostContext) { } Visit(s.SubStatements, inGhostContext); return false; + } else if (stmt is ForeachLoopStmt) { + var s = (ForeachLoopStmt)stmt; + foreach (var v in s.BoundVars) { + VisitType(v.Tok, v.Type, inGhostContext); + } + // do substatements and subexpressions + Visit(Attributes.SubExpressions(s.Attributes), true); + if (s.Range != null) { + Visit(s.Range, inGhostContext); + } + Visit(s.SubStatements, inGhostContext); + return false; } else if (stmt is ExpectStmt) { var s = (ExpectStmt)stmt; Visit(Attributes.SubExpressions(s.Attributes), true); @@ -8718,6 +8738,48 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC } } + } else if (stmt is ForeachLoopStmt) { + var s = (ForeachLoopStmt)stmt; + if (proofContext != null && s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { + Error(s.Mod.Expressions[0].tok, $"a loop in {proofContext} is not allowed to use 'modifies' clauses"); + } + + s.IsGhost = mustBeErasable; + if (!mustBeErasable && s.IsGhost) { + resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost for-loop"); + } + if (s.IsGhost) { + if (s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { + Error(s, "'decreases *' is not allowed on ghost loops"); + } + } + if (s.IsGhost && s.Mod.Expressions != null) { + s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + } + if (s.Body != null) { + Visit(s.Body, s.IsGhost, proofContext); + if (s.Body.IsGhost) { + s.IsGhost = true; + } + } + + var unenumerableBoundVars = s.UnenumerableBoundVars(); + if (unenumerableBoundVars.Count != 0) { + foreach (var bv in unenumerableBoundVars) { + Error(s, "foreach statements must have enumerable ranges, but Dafny's heuristics can't figure out how to produce an enumeration for '{0}'", bv.Name); + } + } + + if (s.IsGhost || !s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { + var infiniteBoundVars = s.InfiniteBoundVars(); + if (infiniteBoundVars.Count != 0) { + foreach (var bv in infiniteBoundVars) { + // TODO: Fix error message + Error(s, "foreach statements in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{0}'", bv.Name); + } + } + } + } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.IsGhost = mustBeErasable || s.Kind != ForallStmt.BodyKind.Assign || ExpressionTester.UsesSpecFeatures(s.Range); @@ -11382,6 +11444,21 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { scope.PushMarker(); ScopePushAndReport(scope, loopIndex, "index-variable"); ResolveAttributes(s, new ResolveOpts(codeContext, true)); + } else if (s is ForeachLoopStmt foreachS) { + int prevErrorCount = reporter.Count(ErrorLevel.Error); + scope.PushMarker(); + foreach (BoundVar v in foreachS.BoundVars) { + ScopePushAndReport(scope, v, "local-variable"); + ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); + } + ResolveExpression(foreachS.Range, new ResolveOpts(codeContext, true)); + Contract.Assert(foreachS.Range.Type != null); // follows from postcondition of ResolveExpression + ConstrainTypeExprBool(foreachS.Range, "range restriction in foreach statement must be of type bool (instead got {0})"); + // Since the range is more likely to infer the types of the bound variables, resolve it + // first (above) and only then resolve the attributes (below). + ResolveAttributes(foreachS, new ResolveOpts(codeContext, true)); + + // TODO: Probably have to special-case decreases here too } ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs, ref usesHeap); @@ -11408,7 +11485,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { reporter.Warning(MessageSource.Resolver, s.Tok, text); } - if (s is ForLoopStmt) { + if (s is ForLoopStmt || s is ForeachLoopStmt) { scope.PopMarker(); } @@ -15208,8 +15285,8 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { allTypeParameters.PopMarker(); expr.Type = Type.Bool; - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is ComprehensionExpr) { + var e = (ComprehensionExpr)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { @@ -15228,8 +15305,16 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ResolveAttributes(e, opts); scope.PopMarker(); - expr.Type = new SetType(e.Finite, e.Term.Type); - + + switch (e) { + case SetComprehension se: + expr.Type = new SetType(se.Finite, se.Term.Type); + break; + case SeqComprehension se: + expr.Type = new SeqType(se.Term.Type); + break; + } + } else if (expr is MapComprehension) { var e = (MapComprehension)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index a526cd1f093..a89377ad0fd 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -1149,8 +1149,8 @@ public static bool UsesSpecFeatures(Expression expr) { var e = (QuantifierExpr)expr; Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody()); - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is CollectionComprehension) { + var e = (CollectionComprehension)expr; return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); } else if (expr is MapComprehension) { var e = (MapComprehension)expr; diff --git a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs index f074c4f58a3..015ec51b21b 100644 --- a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs @@ -400,6 +400,10 @@ public Boogie.Expr TrExpr(Expression expr) { } return s; + } else if (expr is SeqComprehension) { + // TODO + return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType); + } else if (expr is MapDisplayExpr) { MapDisplayExpr e = (MapDisplayExpr)expr; Boogie.Type maptype = predef.MapType(expr.tok, e.Finite, predef.BoxType, predef.BoxType); diff --git a/Test/dafny0/ForeachLoops.dfy b/Test/dafny0/ForeachLoops.dfy new file mode 100644 index 00000000000..3687111d602 --- /dev/null +++ b/Test/dafny0/ForeachLoops.dfy @@ -0,0 +1,8 @@ +// RUN: %dafny "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Foo() { + foreach x: nat | x == 5 { + print x; + } +} \ No newline at end of file diff --git a/Test/dafny0/SeqComprehensions.dfy b/Test/dafny0/SeqComprehensions.dfy new file mode 100644 index 00000000000..e9b27a0c941 --- /dev/null +++ b/Test/dafny0/SeqComprehensions.dfy @@ -0,0 +1,3 @@ +method Foo() { + var s := seq x: int | x == 2; +} \ No newline at end of file