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
16f8a21a
Commit
16f8a21a
authored
Jun 10, 2017
by
Andrei Paskevich
Browse files
minor fixes
parent
2f6f9ac4
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/mlw/dexpr.ml
View file @
16f8a21a
...
...
@@ -1527,6 +1527,7 @@ and lambda uloc env pvl mask dsp dvl de =
let
env
,
old
=
add_label
env
old_mark
in
let
e
=
if
pvl
=
[]
then
expr
uloc
env
de
else
let
ity
=
ity_of_dity
(
dity_of_dvty
de
.
de_dvty
)
in
let
mask
=
if
env
.
ghs
then
MaskGhost
else
mask
in
let
xs
=
create_xsymbol
old_mark_id
~
mask
ity
in
let
e
=
expr
uloc
(
add_xsymbol
env
xs
)
de
in
if
not
(
Sxs
.
mem
xs
e
.
e_effect
.
eff_raises
)
then
e
else
...
...
src/mlw/expr.ml
View file @
16f8a21a
...
...
@@ -916,7 +916,8 @@ let e_case e bl =
|
(
_
,
d
)
::_
->
d
.
e_ity
|
[]
->
invalid_arg
"Expr.e_case"
in
List
.
iter
(
fun
(
p
,
d
)
->
if
mask_spill
e
.
e_mask
p
.
pp_mask
then
if
not
(
ity_equal
e
.
e_ity
ity_unit
)
&&
mask_spill
e
.
e_mask
p
.
pp_mask
then
Loc
.
errorm
"Non-ghost pattern in a ghost position"
;
ity_equal_check
d
.
e_ity
ity
;
ity_equal_check
e
.
e_ity
p
.
pp_ity
)
bl
;
...
...
@@ -969,7 +970,8 @@ let e_try e xl =
let
e_raise
xs
e
ity
=
ity_equal_check
e
.
e_ity
xs
.
xs_ity
;
let
ghost
=
mask_spill
e
.
e_mask
xs
.
xs_mask
in
let
ghost
=
not
(
ity_equal
e
.
e_ity
ity_unit
)
&&
mask_spill
e
.
e_mask
xs
.
xs_mask
in
let
eff
=
eff_ghostify
ghost
(
eff_raise
eff_empty
xs
)
in
let
eff
=
try_effect
[
e
]
eff_union_seq
e
.
e_effect
eff
in
mk_expr
(
Eraise
(
xs
,
e
))
ity
MaskVisible
eff
...
...
src/mlw/ity.ml
View file @
16f8a21a
...
...
@@ -877,6 +877,7 @@ let freeze_xs xs s = ity_freeze s xs.xs_ity
let
create_xsymbol
id
?
(
mask
=
MaskVisible
)
ity
=
mask_check
(
Invalid_argument
"Ity.create_xsymbol"
)
ity
mask
;
let
mask
=
if
ity_equal
ity
ity_unit
then
MaskVisible
else
mask
in
{
xs_name
=
id_register
id
;
xs_ity
=
ity
;
xs_mask
=
mask_reduce
mask
}
module
Exn
=
MakeMSH
(
struct
...
...
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