Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
8831bd3a
Commit
8831bd3a
authored
Mar 17, 2016
by
Andrei Paskevich
Browse files
Mlw: "let constant" admits a type cast
parent
32c45d99
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/parser/parser.mly
View file @
8831bd3a
...
...
@@ -633,7 +633,7 @@ numeral:
prog_decl
:
|
VAL
ghost
kind
labels
(
lident_rich
)
mk_expr
(
val_defn
)
{
Dlet
(
$
4
,
$
2
,
$
3
,
$
5
)
}
|
LET
ghost
kind
labels
(
lident_rich
)
mk_expr
(
fun_defn
)
{
Dlet
(
$
4
,
$
2
,
$
3
,
$
5
)
}
|
LET
ghost
kind
labels
(
lident_rich
)
EQUAL
seq_expr
{
Dlet
(
$
4
,
$
2
,
$
3
,
$
6
)
}
|
LET
ghost
kind
labels
(
lident_rich
)
const_defn
{
Dlet
(
$
4
,
$
2
,
$
3
,
$
5
)
}
|
LET
REC
with_list1
(
rec_defn
)
{
Drec
$
3
}
|
EXCEPTION
labels
(
uident
)
{
Dexn
(
$
2
,
PTtuple
[]
,
Ity
.
MaskVisible
)
}
|
EXCEPTION
labels
(
uident
)
return
{
Dexn
(
$
2
,
fst
$
3
,
snd
$
3
)
}
...
...
@@ -663,6 +663,10 @@ val_defn:
|
params
ret_opt
spec
{
Eany
(
$
1
,
Expr
.
RKnone
,
fst
$
2
,
snd
$
2
,
$
3
)
}
const_defn
:
|
cast
EQUAL
seq_expr
{
{
$
3
with
expr_desc
=
Ecast
(
$
3
,
$
1
)
}
}
|
EQUAL
seq_expr
{
$
2
}
(* Program expressions *)
mk_expr
(
X
)
:
d
=
X
{
mk_expr
d
$
startpos
$
endpos
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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