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

Jump to bottom

Parsing experiments #18

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

Parsing experiments #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
5f2e230
Support for x to y
robin-aws Aug 12, 2022
897241e
Adding `<- C | R` as alternative for `:|`
robin-aws Aug 12, 2022
56e8236
Add SeqRangeExpr
robin-aws Aug 13, 2022
0b6bb17
Support wildcard
robin-aws Aug 13, 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
15 changes: 15 additions & 0 deletions Source/Dafny/AST/DafnyAst.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10139,6 +10139,21 @@ public SeqDisplayExpr(IToken tok, List<Expression> elements)
}
}

public class SeqRangeExpr : Expression {
public readonly Expression Start;
public readonly Expression End;
public readonly bool GoingUp;
public SeqRangeExpr(IToken tok, Expression start, Expression end, bool goingUp)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(start != null);
Contract.Requires(end != null);
Start = start;
End = end;
GoingUp = goingUp;
}
}

public class MemberSelectExpr : Expression {
public readonly Expression Obj;
public readonly string MemberName;
Expand Down
66 changes: 56 additions & 10 deletions Source/Dafny/Dafny.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -381,6 +381,7 @@ bool IsParenStar() {
bool IsEquivOp() => IsEquivOp(la);
bool IsImpliesOp() => IsImpliesOp(la);
bool IsExpliesOp() => IsExpliesOp(la);
bool IsRangeOp() => IsRangeOp(la);
bool IsAndOp() => IsAndOp(la);
bool IsOrOp() => IsOrOp(la);
static bool IsEquivOp(IToken la) {
Expand All @@ -392,6 +393,9 @@ static bool IsImpliesOp(IToken la) {
static bool IsExpliesOp(IToken la) {
return la.val == "<==" || la.val == "\u21d0";
}
static bool IsRangeOp(IToken la) {
return la.val == "to" || la.val == "downto";
}
static bool IsAndOp(IToken la) {
return la.val == "&&" || la.val == "\u2227";
}
Expand Down Expand Up @@ -2868,6 +2872,13 @@ UpdateStmt<out Statement/*!*/ s>
"assume" (. suchThatAssume = t; .)
]
Expression<out suchThat, false, true>
| "<" "-" (. x = Token.NoToken; .)
Expression<out e, false, true, false> (. /* Ignore for now */ .)
"|"
[ IF(la.kind == _assume) /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */
"assume" (. suchThatAssume = t; .)
]
Expression<out suchThat, false, true>
| ":-" (. x = t; .)
[ IF(IsAssumeTypeKeyword(la)) /* an Expression can also begin with these keywords, so this says to resolve it to pick up the keyword here */
("expect"|"assert"|"assume") (. keywordToken = t; .)
Expand Down Expand Up @@ -3013,6 +3024,13 @@ VarDeclStatement<.out Statement/*!*/ s.>
"assume" (. suchThatAssume = t; .)
]
Expression<out suchThat, false, true>
| "<" "-" (. assignTok = Token.NoToken; .)
Expression<out suchThat, false, true, false> (. /* Ignore for now */ .)
"|"
[ IF(la.kind == _assume) /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */
"assume" (. suchThatAssume = t; .)
]
Expression<out suchThat, false, true>
| ":-" (. assignTok = t; .)
[ IF(IsAssumeTypeKeyword(la)) /* an Expression can also begin with these keywords, so this says to resolve it to pick up the keyword here */
("expect"|"assert"|"assume") (. keywordToken = t; .)
Expand Down Expand Up @@ -3216,6 +3234,7 @@ ForLoopStmt<out Statement stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null);
IToken x;
BoundVar loopIndex;
Expression over;
Expression start;
Expression end = null;
bool goingUp = true;
Expand All @@ -3237,11 +3256,18 @@ ForLoopStmt<out Statement stmt>
{ Attribute<ref attrs> }
IdentTypeOptional<out loopIndex>
":="
Expression<out start, false, false>
ForLoopDirection<out goingUp>
( Expression<out end, false, false>
| "*"
)
Expression<out over, false, false>
(.
if (over is SeqRangeExpr range) {
start = range.Start;
end = range.End is WildcardExpr ? null : range.End;
goingUp = range.GoingUp;
} else {
SemErr(over.tok, "A 'for' loop must iterate over a range expression");
start = dummyExpr;
end = dummyExpr;
}
.)
LoopSpec<invariants, decreases, ref mod, ref decAttrs, ref modAttrs>
( IF(la.kind == _lbrace) /* if there's an open brace, claim it as the beginning of the loop body (as opposed to a BlockStmt following the loop) */
BlockStmt<out body, out bodyStart, out bodyEnd> (. endTok = body.EndTok; isDirtyLoop = false; .)
Expand Down Expand Up @@ -3306,15 +3332,23 @@ BindingGuard<out Expression e, bool allowLambda>
BoundVar bv; IToken x;
Attributes attrs = null;
Expression body;
e = dummyExpr; /* mute the warning */
.)
IdentTypeOptional<out bv> (. bvars.Add(bv); x = bv.tok; .)
{ ","
IdentTypeOptional<out bv> (. bvars.Add(bv); .)
}
{ Attribute<ref attrs> }
":|"
Expression<out body, true, allowLambda>
(. e = new ExistsExpr(x, t, bvars, null, body, attrs); .)
(
":|"
Expression<out body, true, allowLambda>
(. e = new ExistsExpr(x, t, bvars, null, body, attrs); .)
| "<" "-"
Expression<out body, false, true, false> (. /* Ignore for now */ .)
"|"
Expression<out body, true, allowLambda>
(. e = new ExistsExpr(x, t, bvars, null, body, attrs); .)
)
.


Expand Down Expand Up @@ -3733,9 +3767,9 @@ EquivExpression<out Expression e0, bool allowLemma, bool allowLambda, bool allow

/*------------------------------------------------------------------------*/
ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, bool allowBitwiseOps>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; bool goingUp;.)
LogicalExpression<out e0, allowLemma, allowLambda, allowBitwiseOps>
[ IF(IsImpliesOp() || IsExpliesOp()) /* read an ImpliesExpliesExpression as far as possible */
[ IF(IsImpliesOp() || IsExpliesOp() || IsRangeOp()) /* read an ImpliesExpliesExpression as far as possible */
/* Note, the asymmetry in the parsing of implies and explies expressions stems from the fact that
* implies is right associative whereas reverse implication is left associative
*/
Expand All @@ -3751,6 +3785,8 @@ ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, b
.)
}
[ IF(IsImpliesOp()) ImpliesOp (. SemErr(t, "Ambiguous use of ==> and <==. Use parentheses to disambiguate."); .) ]
| ForLoopDirection<out goingUp>
PossiblyWildExpression<out e1, allowLambda, true> (. e0 = new SeqRangeExpr(t, e0, e1, goingUp); .)
)
]
.
Expand Down Expand Up @@ -4431,6 +4467,16 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
}
}
.)
| "<" "-"
Expression<out e, false, true, false> (. /* Ignore for now */ .)
"|"
(. exact = false;
foreach (var lhs in letLHSs) {
if (lhs.Arguments != null) {
SemErr(lhs.tok, "LHS of let-such-that expression must be variables, not general patterns");
}
}
.)
| ":-" (. isLetOrFail = true; .)
)
Expression<out e, false, true> (. letRHSs.Add(e); .)
Expand Down