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
44e81c0a
Commit
44e81c0a
authored
Nov 13, 2012
by
Andrei Paskevich
Browse files
fix #15067
parent
c7a7ea65
Changes
6
Hide whitespace changes
Inline
Side-by-side
src/whyml/mlw_dty.ml
View file @
44e81c0a
...
...
@@ -37,11 +37,10 @@ and rvar =
|
Rtvs
of
tvsymbol
*
dity
*
region
Lazy
.
t
|
Rval
of
dreg
let
ity_of_dity
?
(
strict
=
true
)
dity
=
let
ity_of_dity
dity
=
let
rec
get_ity
=
function
|
Dvar
{
contents
=
Dtvs
_
}
when
strict
->
|
Dvar
{
contents
=
Dtvs
_
}
->
Loc
.
errorm
"undefined type variable"
|
Dvar
{
contents
=
Dtvs
tv
}
->
ity_var
tv
|
Dvar
{
contents
=
Dval
dty
}
->
get_ity
dty
|
Duvar
tv
->
ity_var
tv
|
Dits
(
its
,
dl
,
rl
)
->
...
...
@@ -49,8 +48,6 @@ let ity_of_dity ?(strict=true) dity =
|
Dts
(
ts
,
dl
)
->
ity_pur
ts
(
List
.
map
get_ity
dl
)
and
get_reg
=
function
|
Rreg
(
r
,_
)
->
r
|
Rvar
{
contents
=
Rtvs
(
_
,
dity
,_
)
}
when
not
strict
->
create_region
(
id_fresh
"rho"
)
(
get_ity
dity
)
|
Rvar
{
contents
=
Rtvs
(
_
,_,
r
)
}
->
Lazy
.
force
r
|
Rvar
{
contents
=
Rval
dreg
}
->
get_reg
dreg
in
...
...
@@ -182,17 +179,18 @@ and unify_reg r1 r2 =
|
Rreg
(
reg1
,_
)
,
Rreg
(
reg2
,_
)
when
reg_equal
reg1
reg2
->
()
|
_
->
raise
Exit
exception
DTypeMismatch
of
dity
*
dity
let
unify
~
weak
d1
d2
=
try
unify
~
weak
d1
d2
with
Exit
->
raise
(
TypeMismatch
(
ity_of_dity
~
strict
:
false
d1
,
ity_of_dity
~
strict
:
false
d2
))
try
unify
~
weak
d1
d2
with
Exit
->
raise
(
DTypeMismatch
(
d1
,
d2
))
let
unify_weak
d1
d2
=
unify
~
weak
:
true
d1
d2
let
unify
d1
d2
=
unify
~
weak
:
false
d1
d2
type
dvty
=
dity
list
*
dity
(* A -> B -> C == ([A;B],C) *)
let
vty_of_dvty
?
(
strict
=
true
)
(
argl
,
res
)
=
let
ity_of_dity
dity
=
ity_of_dity
~
strict
dity
in
let
vty_of_dvty
(
argl
,
res
)
=
let
ity_of_dity
dity
=
ity_of_dity
dity
in
let
vtv
=
VTvalue
(
vty_value
(
ity_of_dity
res
))
in
let
conv
a
=
create_pvsymbol
(
id_fresh
"x"
)
(
vty_value
(
ity_of_dity
a
))
in
if
argl
=
[]
then
vtv
else
VTarrow
(
vty_arrow
(
List
.
map
conv
argl
)
vtv
)
...
...
@@ -302,3 +300,58 @@ let specialize_lsymbol ls =
let
conv
ty
=
dity_of_ty
htv
hreg
vars_empty
ty
in
let
ty
=
Opt
.
get_def
ty_bool
ls
.
ls_value
in
List
.
map
conv
ls
.
ls_args
,
conv
ty
(* Pretty-printing *)
let
debug_print_reg_types
=
Debug
.
register_info_flag
"print_reg_types"
~
desc
:
"Print@ types@ of@ regions@ (mutable@ fields)."
let
print_dity
fmt
dity
=
let
protect_on
x
s
=
if
x
then
"("
^^
s
^^
")"
else
s
in
let
rec
print_dity
inn
fmt
=
function
|
Dvar
{
contents
=
Dtvs
tv
}
|
Duvar
tv
->
Pretty
.
print_tv
fmt
tv
|
Dvar
{
contents
=
Dval
dty
}
->
print_dity
inn
fmt
dty
|
Dts
(
ts
,
tl
)
when
is_ts_tuple
ts
->
Format
.
fprintf
fmt
"(%a)"
(
Pp
.
print_list
Pp
.
comma
(
print_dity
false
))
tl
|
Dts
(
ts
,
[]
)
->
Pretty
.
print_ts
fmt
ts
|
Dts
(
ts
,
tl
)
->
Format
.
fprintf
fmt
(
protect_on
inn
"%a@ %a"
)
Pretty
.
print_ts
ts
(
Pp
.
print_list
Pp
.
space
(
print_dity
true
))
tl
|
Dits
(
its
,
[]
,
rl
)
->
Format
.
fprintf
fmt
(
protect_on
inn
"%a@ <%a>"
)
Mlw_pretty
.
print_its
its
(
Pp
.
print_list
Pp
.
comma
print_dreg
)
rl
|
Dits
(
its
,
tl
,
rl
)
->
Format
.
fprintf
fmt
(
protect_on
inn
"%a@ <%a>@ %a"
)
Mlw_pretty
.
print_its
its
(
Pp
.
print_list
Pp
.
comma
print_dreg
)
rl
(
Pp
.
print_list
Pp
.
space
(
print_dity
true
))
tl
and
print_dreg
fmt
=
function
|
Rreg
(
r
,_
)
when
Debug
.
test_flag
debug_print_reg_types
->
Format
.
fprintf
fmt
"@[%a:@,%a@]"
Mlw_pretty
.
print_reg
r
Mlw_pretty
.
print_ity
r
.
reg_ity
|
Rreg
(
r
,_
)
->
Mlw_pretty
.
print_reg
fmt
r
|
Rvar
{
contents
=
Rtvs
(
tv
,
dity
,_
)
}
when
Debug
.
test_flag
debug_print_reg_types
->
let
r
=
create_region
(
id_clone
tv
.
tv_name
)
Mlw_ty
.
ity_unit
in
Format
.
fprintf
fmt
"@[%a:@,%a@]"
Mlw_pretty
.
print_reg
r
(
print_dity
false
)
dity
|
Rvar
{
contents
=
Rtvs
(
tv
,_,_
)
}
->
let
r
=
create_region
(
id_clone
tv
.
tv_name
)
Mlw_ty
.
ity_unit
in
Mlw_pretty
.
print_reg
fmt
r
|
Rvar
{
contents
=
Rval
dreg
}
->
print_dreg
fmt
dreg
in
print_dity
false
fmt
dity
let
()
=
Exn_printer
.
register
begin
fun
fmt
exn
->
match
exn
with
|
DTypeMismatch
(
t1
,
t2
)
->
Format
.
fprintf
fmt
"Type mismatch between %a and %a"
print_dity
t1
print_dity
t2
|
_
->
raise
exn
end
src/whyml/mlw_dty.mli
View file @
44e81c0a
...
...
@@ -33,11 +33,13 @@ val create_user_type_variable: Ptree.ident -> dity
val
its_app
:
itysymbol
->
dity
list
->
dity
val
ts_app
:
tysymbol
->
dity
list
->
dity
exception
DTypeMismatch
of
dity
*
dity
val
unify
:
dity
->
dity
->
unit
val
unify_weak
:
dity
->
dity
->
unit
(* don't unify regions *)
val
ity_of_dity
:
?
strict
:
bool
->
dity
->
ity
val
vty_of_dvty
:
?
strict
:
bool
->
dvty
->
vty
val
ity_of_dity
:
dity
->
ity
val
vty_of_dvty
:
dvty
->
vty
(** use with care, only once unification is done *)
val
specialize_scheme
:
tvars
->
dvty
->
dvty
...
...
@@ -47,3 +49,5 @@ val specialize_pvsymbol: pvsymbol -> dity
val
specialize_psymbol
:
psymbol
->
dvty
val
specialize_plsymbol
:
plsymbol
->
dvty
val
specialize_xsymbol
:
xsymbol
->
dity
val
print_dity
:
Format
.
formatter
->
dity
->
unit
src/whyml/mlw_pretty.ml
View file @
44e81c0a
...
...
@@ -93,7 +93,7 @@ let rec print_ity_node inn fmt ity = match ity.ity_node with
(
print_list
space
(
print_ity_node
true
))
tl
and
print_regty
fmt
reg
=
if
Debug
.
test_flag
debug_print_reg_types
then
print_reg
fmt
reg
else
if
Debug
.
not
test_flag
debug_print_reg_types
then
print_reg
fmt
reg
else
fprintf
fmt
"@[%a:@,%a@]"
print_reg
reg
(
print_ity_node
false
)
reg
.
reg_ity
let
print_ity
=
print_ity_node
false
...
...
@@ -439,10 +439,10 @@ let () = Exn_printer.register
|
Mlw_ty
.
UnboundException
xs
->
fprintf
fmt
"This function raises %a but does not \
specify a post-condition for it"
print_xs
xs
|
Mlw_ty
.
RegionMismatch
(
r1
,
r2
)
->
|
Mlw_ty
.
RegionMismatch
(
r1
,
r2
,_
s
)
->
fprintf
fmt
"Region mismatch between %a and %a"
print_regty
r1
print_regty
r2
|
Mlw_ty
.
TypeMismatch
(
t1
,
t2
)
->
|
Mlw_ty
.
TypeMismatch
(
t1
,
t2
,_
s
)
->
fprintf
fmt
"Type mismatch between %a and %a"
print_ity
t1
print_ity
t2
|
Mlw_ty
.
PolymorphicException
(
id
,_
ity
)
->
...
...
src/whyml/mlw_ty.ml
View file @
44e81c0a
...
...
@@ -285,17 +285,6 @@ exception BadRegArity of itysymbol * int * int
exception
DuplicateRegion
of
region
exception
UnboundRegion
of
region
exception
RegionMismatch
of
region
*
region
exception
TypeMismatch
of
ity
*
ity
let
ity_equal_check
ty1
ty2
=
if
not
(
ity_equal
ty1
ty2
)
then
raise
(
TypeMismatch
(
ty1
,
ty2
))
(* dead code
let reg_equal_check r1 r2 =
if not (reg_equal r1 r2) then raise (RegionMismatch (r1, r2))
*)
type
ity_subst
=
{
ity_subst_tv
:
ity
Mtv
.
t
;
ity_subst_reg
:
region
Mreg
.
t
;
(* must preserve ghost-ness *)
...
...
@@ -306,12 +295,14 @@ let ity_subst_empty = {
ity_subst_reg
=
Mreg
.
empty
;
}
let
tv_inst
s
v
=
Mtv
.
find_def
(
ity_var
v
)
v
s
.
ity_subst
_tv
let
reg_inst
s
r
=
Mreg
.
find_def
r
r
s
.
ity_subst
_reg
exception
RegionMismatch
of
region
*
region
*
ity_subst
exception
TypeMismatch
of
ity
*
ity
*
ity_subst
let
ity_inst
s
ity
=
if
ity_closed
ity
&&
ity_pure
ity
then
ity
else
ity_v_map
(
tv_inst
s
)
(
reg_inst
s
)
ity
let
ity_equal_check
ty1
ty2
=
if
not
(
ity_equal
ty1
ty2
)
then
raise
(
TypeMismatch
(
ty1
,
ty2
,
ity_subst_empty
))
let
reg_equal_check
r1
r2
=
if
not
(
reg_equal
r1
r2
)
then
raise
(
RegionMismatch
(
r1
,
r2
,
ity_subst_empty
))
let
reg_full_inst
s
r
=
Mreg
.
find
r
s
.
ity_subst_reg
...
...
@@ -349,7 +340,11 @@ and reg_match s r1 r2 =
let
ity_match
s
ity1
ity2
=
try
ity_match
s
ity1
ity2
with
Exit
->
raise
(
TypeMismatch
(
ity_inst
s
ity1
,
ity2
))
with
Exit
->
raise
(
TypeMismatch
(
ity1
,
ity2
,
s
))
let
reg_match
s
r1
r2
=
try
reg_match
s
r1
r2
with
Exit
->
raise
(
RegionMismatch
(
r1
,
r2
,
s
))
let
rec
ty_of_ity
ity
=
match
ity
.
ity_node
with
|
Ityvar
v
->
ty_var
v
...
...
@@ -632,7 +627,7 @@ let eff_assign e ?(ghost=false) r ty =
|
Ityvar
tv'
->
tv_equal
tv
tv'
|
_
->
false
in
if
not
(
Mtv
.
for_all
check
sub
.
ity_subst_tv
)
then
raise
(
TypeMismatch
(
r
.
reg_ity
,
ty
));
raise
(
TypeMismatch
(
r
.
reg_ity
,
ty
,
ity_subst_empty
));
(* r:t[r1,r2] <- t[r1,r1] introduces an alias *)
let
add_right
_
v
s
=
Sreg
.
add_new
(
IllegalAlias
v
)
v
s
in
ignore
(
Mreg
.
fold
add_right
sub
.
ity_subst_reg
Sreg
.
empty
);
...
...
src/whyml/mlw_ty.mli
View file @
44e81c0a
...
...
@@ -119,12 +119,8 @@ val ity_s_any : (itysymbol -> bool) -> (tysymbol -> bool) -> ity -> bool
val
its_clone
:
Theory
.
symbol_map
->
itysymbol
Mits
.
t
*
region
Mreg
.
t
(* traversal functions on type variables and regions *)
val
ity_v_map
:
(
tvsymbol
->
ity
)
->
(
region
->
region
)
->
ity
->
ity
val
ity_closed
:
ity
->
bool
val
ity_pure
:
ity
->
bool
val
ity_closed
:
ity
->
bool
val
ity_pure
:
ity
->
bool
val
ity_inv
:
ity
->
bool
(* these functions attend the sub-regions *)
...
...
@@ -145,14 +141,14 @@ val ity_int : ity
val
ity_bool
:
ity
val
ity_unit
:
ity
exception
RegionMismatch
of
region
*
region
exception
TypeMismatch
of
ity
*
ity
type
ity_subst
=
private
{
ity_subst_tv
:
ity
Mtv
.
t
;
ity_subst_reg
:
region
Mreg
.
t
;
}
exception
RegionMismatch
of
region
*
region
*
ity_subst
exception
TypeMismatch
of
ity
*
ity
*
ity_subst
val
ity_subst_empty
:
ity_subst
val
ity_match
:
ity_subst
->
ity
->
ity
->
ity_subst
...
...
@@ -161,6 +157,8 @@ val reg_match : ity_subst -> region -> region -> ity_subst
val
ity_equal_check
:
ity
->
ity
->
unit
val
reg_equal_check
:
region
->
region
->
unit
val
ity_full_inst
:
ity_subst
->
ity
->
ity
val
reg_full_inst
:
ity_subst
->
region
->
region
...
...
src/whyml/mlw_typing.ml
View file @
44e81c0a
...
...
@@ -184,10 +184,13 @@ let dity_mark = ts_app ts_mark []
*)
let
unify_loc
unify_fn
loc
x1
x2
=
try
unify_fn
x1
x2
with
|
TypeMismatch
(
ity1
,
ity2
)
->
errorm
~
loc
|
TypeMismatch
(
ity1
,
ity2
,_
)
->
errorm
~
loc
"This expression has type %a,@ but is expected to have type %a"
Mlw_pretty
.
print_ity
ity2
Mlw_pretty
.
print_ity
ity1
|
exn
when
not
(
Debug
.
test_flag
Debug
.
stack_trace
)
->
error
~
loc
exn
|
DTypeMismatch
(
dity1
,
dity2
)
->
errorm
~
loc
"This expression has type %a,@ but is expected to have type %a"
Mlw_dty
.
print_dity
dity2
Mlw_dty
.
print_dity
dity1
|
exn
when
Debug
.
nottest_flag
Debug
.
stack_trace
->
error
~
loc
exn
let
expected_type
{
de_loc
=
loc
;
de_type
=
(
argl
,
res
)
}
dity
=
if
argl
<>
[]
then
errorm
~
loc
"This expression is not a first-order value"
;
...
...
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