Allowing universal quantifiers in effect expressions.
This commit is contained in:
parent
104f7165cd
commit
2e52357dd2
@ -85,11 +85,11 @@ ExpressionPointer parsePreconditionExpression(Context &context,
|
|||||||
|
|
||||||
ExpressionPointer expression;
|
ExpressionPointer expression;
|
||||||
|
|
||||||
if ((expression = expressions::And::parse(context, expressionContext, parsePreconditionExpression)))
|
if ((expression = expressions::And::parse(context, expressionContext, parsePreconditionExpression))
|
||||||
return expression;
|
|| (expression = expressions::ForAll::parse(context, expressionContext, parsePreconditionExpression)))
|
||||||
|
{
|
||||||
if ((expression = expressions::ForAll::parse(context, expressionContext, parsePreconditionExpression)))
|
|
||||||
return expression;
|
return expression;
|
||||||
|
}
|
||||||
|
|
||||||
const auto position = parser.position();
|
const auto position = parser.position();
|
||||||
|
|
||||||
@ -172,8 +172,11 @@ ExpressionPointer parseEffectExpression(Context &context, ExpressionContext &exp
|
|||||||
|
|
||||||
ExpressionPointer expression;
|
ExpressionPointer expression;
|
||||||
|
|
||||||
if ((expression = expressions::And::parse(context, expressionContext, parseEffectExpression)))
|
if ((expression = expressions::And::parse(context, expressionContext, parseEffectExpression))
|
||||||
|
|| (expression = expressions::ForAll::parse(context, expressionContext, parseEffectExpression)))
|
||||||
|
{
|
||||||
return expression;
|
return expression;
|
||||||
|
}
|
||||||
|
|
||||||
const auto position = parser.position();
|
const auto position = parser.position();
|
||||||
|
|
||||||
@ -181,8 +184,7 @@ ExpressionPointer parseEffectExpression(Context &context, ExpressionContext &exp
|
|||||||
|
|
||||||
const auto expressionIdentifierPosition = parser.position();
|
const auto expressionIdentifierPosition = parser.position();
|
||||||
|
|
||||||
if (parser.testIdentifierAndSkip("forall")
|
if (parser.testIdentifierAndSkip("when"))
|
||||||
|| parser.testIdentifierAndSkip("when"))
|
|
||||||
{
|
{
|
||||||
parser.seek(expressionIdentifierPosition);
|
parser.seek(expressionIdentifierPosition);
|
||||||
const auto expressionIdentifier = parser.parseIdentifier();
|
const auto expressionIdentifier = parser.parseIdentifier();
|
||||||
|
Reference in New Issue
Block a user