Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
05bb92ba
Commit
05bb92ba
authored
Jul 25, 2018
by
Andrei Paskevich
Browse files
Parser: "(+)_spec" can be user-defined, "(+)'spec" can not.
parent
a8f712d7
Changes
3
Expand all
Hide whitespace changes
Inline
Side-by-side
src/parser/handcrafted.messages
View file @
05bb92ba
This diff is collapsed.
Click to expand it.
src/parser/lexer.mll
View file @
05bb92ba
...
...
@@ -239,8 +239,10 @@ rule token = parse
{
RIGHTSQ
}
|
"]"
(
quote
+
as
s
)
{
RIGHTSQ_QUOTE
s
}
|
")"
(
[
'\''
'
_'
]
alpha
suffix
core_suffix
*
as
s
)
|
")"
(
'\''
alpha
suffix
core_suffix
*
as
s
)
{
RIGHTPAR_QUOTE
s
}
|
")"
(
'
_'
alpha
suffix
core_suffix
*
as
s
)
{
RIGHTPAR_USCORE
s
}
|
op_char_pref
op_char_4
*
quote
*
as
s
{
OPPREF
s
}
|
op_char_1234
*
op_char_1
op_char_1234
*
quote
*
as
s
...
...
src/parser/parser.mly
View file @
05bb92ba
...
...
@@ -151,6 +151,7 @@
%
token
<
string
>
QUOTE_LIDENT
%
token
<
string
>
RIGHTSQ_QUOTE
(* ]'' *)
%
token
<
string
>
RIGHTPAR_QUOTE
(* )'spec *)
%
token
<
string
>
RIGHTPAR_USCORE
(* )_spec *)
(* keywords *)
...
...
@@ -1263,12 +1264,16 @@ lident_rich:
lident_op
:
|
LEFTPAR
lident_op_str
RIGHTPAR
{
mk_id
$
2
$
startpos
(
$
2
)
$
endpos
(
$
2
)
}
|
LEFTPAR
lident_op_str
RIGHTPAR_USCORE
{
mk_id
(
$
2
^$
3
)
$
startpos
$
endpos
}
|
LEFTPAR
lident_op_str
RIGHTPAR_QUOTE
{
mk_id
(
$
2
^$
3
)
$
startpos
$
endpos
}
lident_op_nq
:
|
LEFTPAR
lident_op_str
RIGHTPAR
{
mk_id
$
2
$
startpos
(
$
2
)
$
endpos
(
$
2
)
}
|
LEFTPAR
lident_op_str
RIGHTPAR_USCORE
{
mk_id
(
$
2
^$
3
)
$
startpos
$
endpos
}
|
LEFTPAR
lident_op_str
RIGHTPAR_QUOTE
{
let
loc
=
floc
$
startpos
$
endpos
in
Loc
.
errorm
~
loc
"Symbol (%s)%s cannot be user-defined"
$
2
$
3
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment