Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Foreach #7

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Foreach #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
e154fc2
Add SeqComprehension and parsing support
robin-aws Mar 17, 2022
1f55a85
First cut of resolution, dummy translation for now
robin-aws Mar 17, 2022
48ffdfb
First cut of defining foreach loops
robin-aws Mar 17, 2022
5997da4
First cut of resolution of foreach statements
robin-aws Mar 26, 2022
3beff4f
Discover bounds of foreach loops
robin-aws Mar 26, 2022
069c6c2
typo
robin-aws Mar 29, 2022
65f1d80
Merge branch 'master' of https://github.com/dafny-lang/dafny into for…
robin-aws Mar 29, 2022
0c3123a
Fix parsing ambiguity with sequence constructions
robin-aws Apr 1, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 61 additions & 6 deletions Source/Dafny/AST/DafnyAst.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8299,6 +8299,41 @@ public override IEnumerable<Expression> NonSpecificationSubExpressions {
}
}

public class ForeachLoopStmt : OneBodyLoopStmt {
public readonly List<BoundVar> 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<ComprehensionExpr.BoundedPool> Bounds; // initialized and filled in by resolver
// invariant: if successfully resolved, Bounds.Count == BoundVars.Count;


public ForeachLoopStmt(IToken tok, IToken endTok, List<BoundVar> boundVars, Attributes attrs, Expression range,
List<AttributedExpression> invariants, Specification<Expression> decreases, Specification<FrameExpression> 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<BoundVar> UnenumerableBoundVars() {
Contract.Ensures(Contract.Result<List<BoundVar>>() != null);
var v = ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable;
return ComprehensionExpr.BoundedPool.MissingBounds(BoundVars, Bounds, v);
}

public List<BoundVar> InfiniteBoundVars() {
Contract.Ensures(Contract.Result<List<BoundVar>>() != 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<GuardedAlternative> Alternatives;
Expand Down Expand Up @@ -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 {
Expand All @@ -11824,7 +11857,7 @@ public bool TermIsSimple {
}
}

public SetComprehension(IToken tok, IToken endTok, bool finite, List<BoundVar> bvars, Expression range, Expression/*?*/ term, Attributes attrs)
public CollectionComprehension(IToken tok, IToken endTok, List<BoundVar> 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));
Expand All @@ -11833,9 +11866,31 @@ public SetComprehension(IToken tok, IToken endTok, bool finite, List<BoundVar> 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<BoundVar> 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<BoundVar> bvars, Expression range, Expression/*?*/ term, Attributes attrs)
: base(tok, endTok, bvars, range, term, attrs) {
}
}

public class MapComprehension : ComprehensionExpr {
public override string WhatKind => "map comprehension";

Expand Down
2 changes: 2 additions & 0 deletions Source/Dafny/Cloner.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
111 changes: 84 additions & 27 deletions Source/Dafny/Dafny.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2572,6 +2572,7 @@ OneStmt<out Statement/*!*/ s>
| IfStmt<out s>
| WhileStmt<out s>
| ForLoopStmt<out s>
| ForeachLoopStmt<out s>
| AssertStmt<out s, false>
| AssumeStmt<out s>
| BreakStmt<out s>
Expand Down Expand Up @@ -3363,6 +3364,35 @@ ForallStmt<out Statement/*!*/ s>
.)
.

/*------------------------------------------------------------------------*/
ForeachLoopStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
IToken/*!*/ x = Token.NoToken;
List<BoundVar> bvars = null;
Attributes qattrs = null;
Expression range = null;
List<AttributedExpression> invariants = new List<AttributedExpression>();
List<Expression> decreases = new List<Expression>();
Attributes decAttrs = null;
Attributes modAttrs = null;
List<FrameExpression> mod = null;
BlockStmt block = null;
IToken bodyStart, bodyEnd;
IToken tok = Token.NoToken;
.)
"foreach" (. x = t; tok = x; .)

QuantifierDomain<out bvars, out qattrs, out range>
(. if (range == null) { range = new LiteralExpr(x, true); }
.)
LoopSpec<invariants, decreases, ref mod, ref decAttrs, ref modAttrs>
BlockStmt<out block, out bodyStart, out bodyEnd>
(. s = new ForeachLoopStmt(x, block.EndTok, bvars, qattrs, range,
invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs),
block);
.)
.

/*------------------------------------------------------------------------*/
ModifyStmt<out Statement s>
= (. IToken tok; IToken endTok = Token.NoToken;
Expand Down Expand Up @@ -4080,34 +4110,13 @@ SetDisplayExpr<out Expression e>
SeqDisplayExpr<out Expression e>
= (. 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<Type>(); .)
GenericInstantiation<gt> (. if (gt.Count > 1) {
SemErr("seq type expects only one type argument");
} else {
explicitTypeArg = gt[0];
}
.)
]
"("
Expression<out n, true, true>
","
Expression<out f, true, true>
")" (. e = new SeqConstructionExpr(x, explicitTypeArg, n, f); .)
|
"[" (. List<Expression> elements = new List<Expression/*!*/>();
x = t;

.)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements);
.)
"]"
)
"[" (. List<Expression> elements = new List<Expression/*!*/>();
x = t;
.)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements);
.)
"]"
.

/*------------------------------------------------------------------------*/
Expand Down Expand Up @@ -4173,6 +4182,7 @@ EndlessExpression<out Expression e, bool allowLemma, bool allowLambda, bool allo
| MatchExpression<out e, allowLemma, allowLambda, allowBitwiseOps>
| QuantifierExpression<out e, allowLemma, allowLambda> /* types are such that we can allow bitwise operations in the quantifier body */
| SetComprehensionExpr<out e, allowLemma, allowLambda, allowBitwiseOps>
| SeqComprehensionExpr<out e, allowLemma, allowLambda, allowBitwiseOps>
| StmtInExpr<out s>
Expression<out e, allowLemma, allowLambda, allowBitwiseOps> (. e = new StmtExpr(s.Tok, s, e); .)
| LetExpression<out e, allowLemma, allowLambda, allowBitwiseOps>
Expand Down Expand Up @@ -4685,6 +4695,53 @@ SetComprehensionExpr<out Expression q, bool allowLemma, bool allowLambda, bool a
}
.)
.

/*------------------------------------------------------------------------*/
SeqComprehensionExpr<out Expression q, bool allowLemma, bool allowLambda, bool allowBitwiseOps>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
Type explicitTypeArg = null;
Expression n, f;
BoundVar bv;
List<BoundVar/*!*/> bvars = new List<BoundVar>();
Expression range;
Expression body = null;
Attributes attrs = null;
q = dummyExpr;
.)
"seq" (. IToken seqToken = t; .)
(
[ (. var gt = new List<Type>(); .)
GenericInstantiation<gt> (. if (gt.Count > 1) {
SemErr("seq type expects only one type argument");
} else {
explicitTypeArg = gt[0];
}
.)
]
"("
Expression<out n, true, true>
","
Expression<out f, true, true>
")" (. q = new SeqConstructionExpr(seqToken, explicitTypeArg, n, f); .)
|
IdentTypeOptional<out bv> (. bvars.Add(bv); .)
{ ","
IdentTypeOptional<out bv> (. bvars.Add(bv); .)
}
{ Attribute<ref attrs> }
"|" Expression<out range, allowLemma, allowLambda, allowBitwiseOps>
[ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */
QSep
Expression<out body, allowLemma, allowLambda, allowBitwiseOps>
]
(. 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<Expression> args.>
Expand Down
Loading