Mentions légales du service
Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container registry
Monitor
Service Desk
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Why3
why3
Commits
1df49fa6
Commit
1df49fa6
authored
14 years ago
by
Andrei Paskevich
Browse files
Options
Downloads
Patches
Plain Diff
fix potential unsoundness in Ty.ty_match
parent
4c04f865
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/core/ty.ml
+11
-11
11 additions, 11 deletions
src/core/ty.ml
with
11 additions
and
11 deletions
src/core/ty.ml
+
11
−
11
View file @
1df49fa6
...
@@ -163,7 +163,8 @@ let ty_app s tl =
...
@@ -163,7 +163,8 @@ let ty_app s tl =
match
s
.
ts_def
with
match
s
.
ts_def
with
|
Some
ty
->
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
tv_inst
(
List
.
fold_left2
add
Mtv
.
empty
s
.
ts_args
tl
)
ty
let
m
=
List
.
fold_left2
add
Mtv
.
empty
s
.
ts_args
tl
in
tv_inst
m
ty
|
_
->
|
_
->
ty_app
s
tl
ty_app
s
tl
...
@@ -190,17 +191,16 @@ let rec ty_inst s ty = match ty.ty_node with
...
@@ -190,17 +191,16 @@ let rec ty_inst s ty = match ty.ty_node with
|
_
->
ty_map
(
ty_inst
s
)
ty
|
_
->
ty_map
(
ty_inst
s
)
ty
let
rec
ty_match
s
ty1
ty2
=
let
rec
ty_match
s
ty1
ty2
=
if
ty_equal
ty1
ty2
then
s
let
set
=
function
else
match
ty1
.
ty_node
,
ty2
.
ty_node
with
|
None
->
Some
ty2
|
Tyvar
n1
,
_
->
|
Some
ty1
as
r
when
ty_equal
ty1
ty2
->
r
Mtv
.
change
n1
(
function
|
_
->
raise
Exit
|
None
->
Some
ty2
in
|
Some
ty1
as
r
when
ty_equal
ty1
ty2
->
r
match
ty1
.
ty_node
,
ty2
.
ty_node
with
|
_
->
raise
Exit
)
s
|
Tyapp
(
f1
,
l1
)
,
Tyapp
(
f2
,
l2
)
when
ts_equal
f1
f2
->
|
Tyapp
(
f1
,
l1
)
,
Tyapp
(
f2
,
l2
)
when
ts_equal
f1
f2
->
List
.
fold_left2
ty_match
s
l1
l2
List
.
fold_left2
ty_match
s
l1
l2
|
_
->
|
Tyvar
n1
,
_
->
Mtv
.
change
n1
set
s
raise
Exit
|
_
->
raise
Exit
exception
TypeMismatch
of
ty
*
ty
exception
TypeMismatch
of
ty
*
ty
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
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!
Save comment
Cancel
Please
register
or
sign in
to comment