Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
3cab5a04
Commit
3cab5a04
authored
Aug 20, 2010
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
programs: fixed typing of polymorphic references
parent
629a9304
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
23 additions
and
10 deletions
+23
-10
src/programs/pgm_typing.ml
src/programs/pgm_typing.ml
+15
-1
tests/test-pgm-jcf.mlw
tests/test-pgm-jcf.mlw
+8
-9
No files found.
src/programs/pgm_typing.ml
View file @
3cab5a04
...
...
@@ -1196,6 +1196,18 @@ let add_exception loc x ty gl =
errorm
~
loc
"clash with previous exception %s"
x
;
add_exception
(
id_user
x
loc
)
ty
gl
let
rec
polymorphic_pure_type
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
_
->
true
|
Ty
.
Tyapp
(
_
,
tyl
)
->
List
.
exists
polymorphic_pure_type
tyl
let
cannot_be_generalized
gl
=
function
|
Tpure
{
ty_node
=
Ty
.
Tyapp
(
ts
,
[
ty
])
}
when
ts_equal
ts
gl
.
ts_ref
->
polymorphic_pure_type
ty
|
Tpure
{
ty_node
=
Ty
.
Tyvar
_
}
->
true
|
Tpure
_
|
Tarrow
_
->
false
let
decl
env
gl
=
function
|
Pgm_ptree
.
Dlogic
dl
->
let
dl
=
logic_list0_decl
dl
in
...
...
@@ -1227,10 +1239,12 @@ let decl env gl = function
let
gl
,
dl
=
map_fold_left
one
gl
dl
in
gl
,
[
Dletrec
dl
]
|
Pgm_ptree
.
Dparam
(
id
,
tyv
)
->
let
loc
=
id
.
id_loc
in
let
denv
=
create_denv
gl
in
let
tyv
=
dtype_v
denv
tyv
in
let
tyv
=
type_v
gl
Mstr
.
empty
tyv
in
let
ls
,
gl
=
add_global
id
.
id_loc
id
.
id
tyv
gl
in
if
cannot_be_generalized
gl
tyv
then
errorm
~
loc
"cannot be generalized"
;
let
ls
,
gl
=
add_global
loc
id
.
id
tyv
gl
in
let
gl
=
add_global_if_pure
gl
ls
in
gl
,
[
Dparam
(
ls
,
tyv
)]
|
Pgm_ptree
.
Dexn
(
id
,
ty
)
->
...
...
tests/test-pgm-jcf.mlw
View file @
3cab5a04
{
use import int.Gcd
use import int.ComputerDivision
use import list.List
}
let rec gcd u v variant { v } =
{ u >= 0 and v >= 0 }
if v = 0 then
u
else
gcd v (mod u v)
{ gcd u v result }
parameter assign : r : ref 'a -> 'a -> unit
parameter alloc : 'a -> ref 'a
parameter head : list 'a -> 'a
exception E of 'a
(*
Local Variables:
...
...
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