Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
3e532a25
Commit
3e532a25
authored
Aug 06, 2018
by
Andrei Paskevich
1
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Pmodule: fix merge_ps (bad order of operations)
parent
51e1d35f
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
5 additions
and
2 deletions
+5
-2
src/mlw/pmodule.ml
src/mlw/pmodule.ml
+5
-2
No files found.
src/mlw/pmodule.ml
View file @
3e532a25
...
...
@@ -85,14 +85,17 @@ let merge_ps chk x vo vn =
(* once again, no way to export notation *)
|
_
,
OO
_
->
assert
false
(* but we can merge two compatible symbols *)
|
RS
r1
,
RS
r2
when
not
(
rs_equal
r1
r2
)
->
|
RS
r1
,
RS
r2
->
if
rs_equal
r1
r2
then
vo
else
if
not
(
same_overload
r1
r2
)
then
vn
else
if
ity_equal
(
fsty
r1
)
(
fsty
r2
)
then
vn
else
OO
(
Srs
.
add
r2
(
Srs
.
singleton
r1
))
(* or add a compatible symbol to notation *)
|
OO
s1
,
RS
r2
->
let
r1
=
Srs
.
choose
s1
and
ty
=
fsty
r2
in
if
Srs
.
mem
r2
s1
then
vo
else
let
r1
=
Srs
.
choose
s1
in
if
not
(
same_overload
r1
r2
)
then
vn
else
let
ty
=
fsty
r2
in
let
confl
r
=
not
(
ity_equal
(
fsty
r
)
ty
)
in
let
s1
=
Srs
.
filter
confl
s1
in
if
Srs
.
is_empty
s1
then
vn
else
...
...
François Bobot
@bobot
mentioned in issue
#163 (closed)
·
Aug 07, 2018
mentioned in issue
#163 (closed)
mentioned in issue #163
Toggle commit list
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