aboutsummaryrefslogtreecommitdiffstats
path: root/Grammar.pp
diff options
context:
space:
mode:
authorIvan Enderlin <ivan.enderlin@hoa-project.net>2012-12-18 09:36:18 +0100
committerIvan Enderlin <ivan.enderlin@hoa-project.net>2012-12-18 09:36:18 +0100
commitc600c7f731c50442a5b2b9254358a9f85d4f44e4 (patch)
tree3386e2bdc47222296802732ced3a6ec2cea9124b /Grammar.pp
parentb2b6ddd2703fd4df29d8726ec044fd7edffe40c7 (diff)
downloadPraspel-c600c7f731c50442a5b2b9254358a9f85d4f44e4.zip
Praspel-c600c7f731c50442a5b2b9254358a9f85d4f44e4.tar.gz
Praspel-c600c7f731c50442a5b2b9254358a9f85d4f44e4.tar.bz2
Allow variables in realdom arguments.
Also, prefix clauses tokens by “at_”.
Diffstat (limited to 'Grammar.pp')
-rw-r--r--Grammar.pp33
1 files changed, 17 insertions, 16 deletions
diff --git a/Grammar.pp b/Grammar.pp
index 3baf9fe..57bef00 100644
--- a/Grammar.pp
+++ b/Grammar.pp
@@ -46,13 +46,13 @@
%skip inline_comment //[^\n]*
// Clauses.
-%token is @is
-%token requires @requires
-%token ensures @ensures
-%token throwable @throwable
-%token invariant @invariant
-%token behavior @behavior
-%token forexample @forexample
+%token at_is @is
+%token at_requires @requires
+%token at_ensures @ensures
+%token at_throwable @throwable
+%token at_invariant @invariant
+%token at_behavior @behavior
+%token at_forexample @forexample
// Constructions.
%token old \\old
@@ -131,22 +131,22 @@ method:
| ( behavior() | forexample() ) ::semicolon::*
#is:
- ::is:: <pure>
+ ::at_is:: <pure>
#requires:
- ::requires:: expression()?
+ ::at_requires:: expression()?
#ensures:
- ::ensures:: expression()?
+ ::at_ensures:: expression()?
#throwable:
- ::throwable:: exceptional_expression()?
+ ::at_throwable:: exceptional_expression()?
#invariant:
- ::invariant:: expression()?
+ ::at_invariant:: expression()?
behavior:
- ::behavior:: behavior_content()
+ ::at_behavior:: behavior_content()
( ::and:: behavior_content() )*
behavior_content:
@@ -164,7 +164,7 @@ behavior_content:
::_brace:: #behavior
#forexample:
- ::forexample:: string()
+ ::at_forexample:: string()
expression:
( declaration() | constraint() | domainof() | predicate() )
@@ -202,7 +202,8 @@ constraint:
::pred:: ::parenthesis_:: string()? ::_parenthesis::
disjunction:
- ( constant() | realdom() ) ( ::or:: disjunction() #disjunction )*
+ ( constant() | realdom() | extended_identifier() )
+ ( ::or:: disjunction() #disjunction )*
disjunction_of_constants:
constant() ( ::or:: disjunction_of_constants() #disjunction )*
@@ -213,7 +214,7 @@ disjunction_of_constants:
::_parenthesis::
argument:
- <default> | realdom() | constant() | array()
+ <default> | realdom() | constant() | array() | extended_identifier()
constant:
scalar() | array()