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
8e33e369
Commit
8e33e369
authored
Jul 06, 2012
by
Andrei Paskevich
Browse files
whyml: letrec bodies must be first-order values
parent
08c5987e
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/whyml/mlw_dtree.ml
View file @
8e33e369
...
...
@@ -61,7 +61,7 @@ type dinvariant = Ptree.lexpr option
type
dexpr
=
{
de_desc
:
dexpr_desc
;
de_type
:
d
i
ty
;
de_type
:
d
v
ty
;
de_lab
:
Ident
.
Slab
.
t
;
de_loc
:
loc
;
}
...
...
@@ -93,6 +93,6 @@ and dexpr_desc =
|
DEghost
of
dexpr
|
DEany
of
dtype_c
and
drecfun
=
loc
*
ident
*
ghost
*
d
i
ty
*
dlambda
and
drecfun
=
loc
*
ident
*
ghost
*
d
v
ty
*
dlambda
and
dlambda
=
dbinder
list
*
dvariant
list
*
dpre
*
dexpr
*
dpost
*
dxpost
src/whyml/mlw_dty.ml
View file @
8e33e369
...
...
@@ -192,58 +192,25 @@ and unify_reg r1 r2 =
|
Rreg
(
reg1
,_
)
,
Rreg
(
reg2
,_
)
when
reg_equal
reg1
reg2
->
()
|
_
->
raise
Exit
let
unify
?
(
weak
=
false
)
d1
d2
=
let
unify
~
weak
d1
d2
=
try
unify
~
weak
d1
d2
with
Exit
->
raise
(
TypeMismatch
(
ity_of_dity
d1
,
ity_of_dity
d2
))
let
ts_arrow
=
let
v
=
List
.
map
(
fun
s
->
create_tvsymbol
(
Ident
.
id_fresh
s
))
[
"a"
;
"b"
]
in
Ty
.
create_tysymbol
(
Ident
.
id_fresh
"arrow"
)
v
None
let
unify_weak
d1
d2
=
unify
~
weak
:
true
d1
d2
let
unify
d1
d2
=
unify
~
weak
:
false
d1
d2
let
make_arrow_type
tyl
ty
=
let
arrow
ty1
ty2
=
ts_app_real
ts_arrow
[
ty1
;
ty2
]
in
List
.
fold_right
arrow
tyl
ty
type
dvty
=
dity
list
*
dity
(* A -> B -> C == ([A;B],C) *)
let
rec
unify_list
d1
el
res
=
let
rec
check_val
loc
=
function
|
Dts
(
ts
,
_
)
when
ts_equal
ts
ts_arrow
->
Loc
.
errorm
~
loc
"This expression is not a first-order value"
|
Dvar
{
contents
=
Dval
d
}
->
check_val
loc
d
|
_
->
()
in
let
unify_loc
loc
d1
d2
=
check_val
loc
d2
;
try
unify
d1
d2
with
|
TypeMismatch
(
ity1
,
ity2
)
->
Loc
.
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
->
Loc
.
error
~
loc
exn
in
match
d1
,
el
with
|
Dts
(
ts
,
[
d1
;
d2
])
,
((
loc
,
dity
)
::
el
)
when
ts_equal
ts
ts_arrow
->
(* this is an ugly and overcomplicated way to treat
implicit fields in record update expressions *)
if
Loc
.
equal
loc
Loc
.
dummy_position
then
(
unify_loc
loc
d1
dity
;
unify_list
d2
el
res
)
else
(
unify_list
d2
el
res
;
unify_loc
loc
d1
dity
)
|
Dvar
{
contents
=
Dval
d1
}
,
_
->
unify_list
d1
el
res
|
_
->
unify
d1
(
make_arrow_type
(
List
.
map
snd
el
)
res
)
let
rec
vty_of_dity
=
function
|
Dvar
{
contents
=
Dval
d
}
->
vty_of_dity
d
|
Dts
(
ts
,
[
d1
;
d2
])
when
ts_equal
ts
ts_arrow
->
VTarrow
(
vty_arrow
(
vty_value
(
ity_of_dity
d1
))
(
vty_of_dity
d2
))
|
dity
->
VTvalue
(
vty_value
(
ity_of_dity
dity
))
let
vty_of_dvty
(
argl
,
res
)
=
let
add
a
v
=
VTarrow
(
vty_arrow
(
vty_value
(
ity_of_dity
a
))
v
)
in
List
.
fold_right
add
argl
(
VTvalue
(
vty_value
(
ity_of_dity
res
)))
type
tvars
=
dity
list
let
empty_tvars
=
[]
let
add_tvars
tvs
dity
=
dity
::
tvs
let
add_dity
tvs
dity
=
dity
::
tvs
let
add_dvty
tvs
(
argl
,
res
)
=
res
::
List
.
rev_append
argl
tvs
let
tv_in_tvars
tv
tvs
=
try
List
.
iter
(
occur_check
tv
)
tvs
;
false
with
Exit
->
true
...
...
@@ -251,7 +218,7 @@ let tv_in_tvars tv tvs =
let
reg_in_tvars
tv
tvs
=
try
List
.
iter
(
occur_check_reg
tv
)
tvs
;
false
with
Exit
->
true
let
specialize_scheme
tvs
dity
=
let
specialize_scheme
tvs
(
argl
,
res
)
=
let
htvs
=
Htv
.
create
17
in
let
hreg
=
Htv
.
create
17
in
let
rec
specialize
=
function
...
...
@@ -277,7 +244,7 @@ let specialize_scheme tvs dity =
end
|
Rreg
_
as
r
->
r
in
specialize
dity
List
.
map
specialize
argl
,
specialize
res
(* Specialization of symbols *)
...
...
@@ -320,11 +287,11 @@ let specialize_vtarrow vars vta =
let
conv
vtv
=
dity_of_vtv
htv
hreg
vars
vtv
in
let
rec
specialize
a
=
let
arg
=
conv
a
.
vta_arg
in
let
res
=
match
a
.
vta_result
with
|
VTvalue
v
->
conv
v
let
argl
,
res
=
match
a
.
vta_result
with
|
VTvalue
v
->
[]
,
conv
v
|
VTarrow
a
->
specialize
a
in
make_arrow_type
[
arg
]
res
arg
::
arg
l
,
res
in
specialize
vta
...
...
@@ -334,7 +301,7 @@ let specialize_psymbol ps =
let
specialize_plsymbol
pls
=
let
htv
=
Htv
.
create
3
and
hreg
=
Hreg
.
create
3
in
let
conv
vtv
=
dity_of_vtv
htv
hreg
vars_empty
vtv
in
make_arrow_type
(
List
.
map
conv
pls
.
pl_args
)
(
conv
pls
.
pl_value
)
List
.
map
conv
pls
.
pl_args
,
conv
pls
.
pl_value
let
dity_of_ty
htv
hreg
vars
ty
=
dity_of_ity
htv
hreg
vars
(
ity_of_ty
ty
)
...
...
@@ -343,4 +310,4 @@ let specialize_lsymbol ls =
let
htv
=
Htv
.
create
3
and
hreg
=
Hreg
.
create
3
in
let
conv
ty
=
dity_of_ty
htv
hreg
vars_empty
ty
in
let
ty
=
Util
.
def_option
ty_bool
ls
.
ls_value
in
make_arrow_type
(
List
.
map
conv
ls
.
ls_args
)
(
conv
ty
)
List
.
map
conv
ls
.
ls_args
,
conv
ty
src/whyml/mlw_dty.mli
View file @
8e33e369
...
...
@@ -31,31 +31,29 @@ open Mlw_module
type
dreg
type
dity
type
dvty
=
dity
list
*
dity
(* A -> B -> C == ([A;B],C) *)
type
tvars
(* a set of type variables *)
val
empty_tvars
:
tvars
val
add_tvars
:
tvars
->
dity
->
tvars
val
add_dity
:
tvars
->
dity
->
tvars
val
add_dvty
:
tvars
->
dvty
->
tvars
val
create_user_type_variable
:
Ptree
.
ident
->
dity
val
create_type_variable
:
unit
->
dity
val
create_user_type_variable
:
Ptree
.
ident
->
dity
val
its_app
:
user
:
bool
->
itysymbol
->
dity
list
->
dity
val
ts_app
:
tysymbol
->
dity
list
->
dity
val
make_arrow_type
:
dity
list
->
dity
->
dity
val
unify
:
?
weak
:
bool
->
dity
->
dity
->
unit
(** destructive unification, with or without region unification *)
val
unify_list
:
dity
->
(
Loc
.
position
*
dity
)
list
->
dity
->
unit
val
unify
:
dity
->
dity
->
unit
val
unify_weak
:
dity
->
dity
->
unit
(* don't unify regions *)
val
ity_of_dity
:
dity
->
ity
val
vty_of_d
i
ty
:
d
i
ty
->
vty
val
vty_of_d
v
ty
:
d
v
ty
->
vty
(** use with care, only once unification is done *)
val
specialize_scheme
:
tvars
->
d
i
ty
->
d
i
ty
val
specialize_scheme
:
tvars
->
d
v
ty
->
d
v
ty
val
specialize_lsymbol
:
lsymbol
->
d
i
ty
val
specialize_lsymbol
:
lsymbol
->
d
v
ty
val
specialize_pvsymbol
:
pvsymbol
->
dity
val
specialize_psymbol
:
psymbol
->
d
i
ty
val
specialize_plsymbol
:
plsymbol
->
d
i
ty
val
specialize_psymbol
:
psymbol
->
d
v
ty
val
specialize_plsymbol
:
plsymbol
->
d
v
ty
val
specialize_xsymbol
:
xsymbol
->
dity
src/whyml/mlw_typing.ml
View file @
8e33e369
...
...
@@ -91,7 +91,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
type
denv
=
{
uc
:
module_uc
;
locals
:
(
tvars
*
d
i
ty
)
Mstr
.
t
;
locals
:
(
tvars
*
d
v
ty
)
Mstr
.
t
;
tvars
:
tvars
;
uloc
:
Ptree
.
loc
option
;
}
...
...
@@ -167,16 +167,19 @@ let dity_bool = ts_app ts_bool []
let
dity_unit
=
ts_app
ts_unit
[]
let
dity_mark
=
ts_app
ts_mark
[]
let
unify_loc
loc
fn_unify
x1
x2
=
try
fn_unify
x1
x2
with
|
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
->
error
~
loc
exn
let
unify_loc
unify_fn
loc
x1
x2
=
try
unify_fn
x1
x2
with
|
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
->
error
~
loc
exn
let
expected_type
?
(
weak
=
false
)
e
dity
=
unify_loc
e
.
de_loc
(
unify
~
weak
)
dity
e
.
de_type
let
expected_type
{
de_loc
=
loc
;
de_type
=
(
argl
,
res
)
}
dity
=
if
argl
<>
[]
then
errorm
~
loc
"This expression is not a first-order value"
;
unify_loc
unify
loc
dity
res
let
expected_type_weak
{
de_loc
=
loc
;
de_type
=
(
argl
,
res
)
}
dity
=
if
argl
<>
[]
then
errorm
~
loc
"This expression is not a first-order value"
;
unify_loc
unify_weak
loc
dity
res
let
rec
extract_labels
labs
loc
e
=
match
e
.
Ptree
.
expr_desc
with
|
Ptree
.
Enamed
(
Ptree
.
Lstr
s
,
e
)
->
extract_labels
(
Slab
.
add
s
labs
)
loc
e
...
...
@@ -244,24 +247,24 @@ let mk_var e =
let
mk_id
s
loc
=
{
id
=
s
;
id_loc
=
loc
;
id_lab
=
[]
}
let
mk_dexpr
desc
d
i
ty
loc
labs
=
{
de_desc
=
desc
;
de_type
=
d
i
ty
;
de_loc
=
loc
;
de_lab
=
labs
}
let
mk_dexpr
desc
d
v
ty
loc
labs
=
{
de_desc
=
desc
;
de_type
=
d
v
ty
;
de_loc
=
loc
;
de_lab
=
labs
}
let
mk_let
~
loc
~
uloc
e
(
desc
,
d
i
ty
)
=
if
test_var
e
then
desc
,
d
i
ty
else
let
mk_let
~
loc
~
uloc
e
(
desc
,
d
v
ty
)
=
if
test_var
e
then
desc
,
d
v
ty
else
let
loc
=
def_option
loc
uloc
in
let
e1
=
mk_dexpr
desc
d
i
ty
loc
Slab
.
empty
in
DElet
(
mk_id
"q"
loc
,
false
,
e
,
e1
)
,
d
i
ty
let
e1
=
mk_dexpr
desc
d
v
ty
loc
Slab
.
empty
in
DElet
(
mk_id
"q"
loc
,
false
,
e
,
e1
)
,
d
v
ty
(* patterns *)
let
add_var
id
dity
denv
=
let
tvars
=
add_
tvars
denv
.
tvars
dity
in
let
locals
=
Mstr
.
add
id
.
id
(
tvars
,
dity
)
denv
.
locals
in
let
tvars
=
add_
dity
denv
.
tvars
dity
in
let
locals
=
Mstr
.
add
id
.
id
(
tvars
,
([]
,
dity
)
)
denv
.
locals
in
{
denv
with
locals
=
locals
;
tvars
=
tvars
}
let
specialize_qualid
uc
p
=
match
uc_find_ps
uc
p
with
|
PV
pv
->
DEglobal_pv
pv
,
specialize_pvsymbol
pv
|
PV
pv
->
DEglobal_pv
pv
,
([]
,
specialize_pvsymbol
pv
)
|
PS
ps
->
DEglobal_ps
ps
,
specialize_psymbol
ps
|
PL
pl
->
DEglobal_pl
pl
,
specialize_plsymbol
pl
|
LS
ls
->
DEglobal_ls
ls
,
specialize_lsymbol
ls
...
...
@@ -287,8 +290,8 @@ let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
let
dity
=
create_type_variable
()
in
PPvar
(
Denv
.
create_user_id
id
)
,
dity
,
add_var
id
dity
denv
|
Ptree
.
PPpapp
(
q
,
ppl
)
->
let
sym
,
d
i
ty
=
specialize_qualid
denv
.
uc
q
in
dpat_app
denv
loc
(
mk_dexpr
sym
d
i
ty
loc
Slab
.
empty
)
ppl
let
sym
,
d
v
ty
=
specialize_qualid
denv
.
uc
q
in
dpat_app
denv
loc
(
mk_dexpr
sym
d
v
ty
loc
Slab
.
empty
)
ppl
|
Ptree
.
PPprec
fl
when
is_pure_record
denv
.
uc
fl
->
let
kn
=
Theory
.
get_known
(
get_theory
denv
.
uc
)
in
let
fl
=
List
.
map
(
find_pure_field
denv
.
uc
)
fl
in
...
...
@@ -308,7 +311,7 @@ let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
|
Ptree
.
PPpor
(
lpp1
,
lpp2
)
->
let
pp1
,
dity1
,
denv
=
dpattern
denv
lpp1
in
let
pp2
,
dity2
,
denv
=
dpattern
denv
lpp2
in
unify_loc
lpp2
.
pat_loc
unify
dity1
dity2
;
unify_loc
unify
lpp2
.
pat_loc
dity1
dity2
;
PPor
(
pp1
,
pp2
)
,
dity1
,
denv
|
Ptree
.
PPpas
(
pp
,
id
)
->
let
pp
,
dity
,
denv
=
dpattern
denv
pp
in
...
...
@@ -319,15 +322,18 @@ and dpat_app denv gloc ({ de_loc = loc } as de) ppl =
let
pp
,
ty
,
denv
=
dpattern
denv
lp
in
pp
::
ppl
,
(
lp
.
pat_loc
,
ty
)
::
tyl
,
denv
in
let
ppl
,
tyl
,
denv
=
List
.
fold_right
add_pp
ppl
([]
,
[]
,
denv
)
in
let
pp
=
match
de
.
de_desc
with
|
DEglobal_pl
pl
->
Mlw_expr
.
PPpapp
(
pl
,
ppl
)
|
DEglobal_ls
ls
->
PPlapp
(
ls
,
ppl
)
let
pp
,
ls
=
match
de
.
de_desc
with
|
DEglobal_pl
pl
->
Mlw_expr
.
PPpapp
(
pl
,
ppl
)
,
pl
.
pl_ls
|
DEglobal_ls
ls
->
Mlw_expr
.
PPlapp
(
ls
,
ppl
)
,
ls
|
DEglobal_pv
pv
->
errorm
~
loc
"%a is not a constructor"
print_pv
pv
|
DEglobal_ps
ps
->
errorm
~
loc
"%a is not a constructor"
print_ps
ps
|
_
->
assert
false
in
let
res
=
create_type_variable
()
in
Loc
.
try2
gloc
unify_list
de
.
de_type
tyl
res
;
let
argl
,
res
=
de
.
de_type
in
if
List
.
length
argl
<>
List
.
length
ppl
then
error
~
loc
:
gloc
(
Term
.
BadArity
(
ls
,
List
.
length
argl
,
List
.
length
ppl
));
let
unify_arg
ta
(
loc
,
tv
)
=
unify_loc
unify
loc
ta
tv
in
List
.
iter2
unify_arg
argl
tyl
;
pp
,
res
,
denv
(* specifications *)
...
...
@@ -352,22 +358,22 @@ let deff_of_peff uc pe =
let
dxpost
uc
ql
=
List
.
map
(
fun
(
q
,
f
)
->
find_xsymbol
uc
q
,
f
)
ql
let
rec
dtype_c
denv
tyc
=
let
tyv
,
d
i
ty
=
dtype_v
denv
tyc
.
pc_result_type
in
let
tyv
,
d
v
ty
=
dtype_v
denv
tyc
.
pc_result_type
in
{
dc_result
=
tyv
;
dc_effect
=
deff_of_peff
denv
.
uc
tyc
.
pc_effect
;
dc_pre
=
tyc
.
pc_pre
;
dc_post
=
fst
tyc
.
pc_post
;
dc_xpost
=
dxpost
denv
.
uc
(
snd
tyc
.
pc_post
);
}
,
d
i
ty
d
v
ty
and
dtype_v
denv
=
function
|
Tpure
pty
->
let
dity
=
dity_of_pty
~
user
:
true
denv
pty
in
DSpecV
(
false
,
dity
)
,
dity
DSpecV
(
false
,
dity
)
,
([]
,
dity
)
|
Tarrow
(
bl
,
tyc
)
->
let
denv
,
bl
,
tyl
=
dbinders
denv
bl
in
let
tyc
,
dity
=
dtype_c
denv
tyc
in
DSpecA
(
bl
,
tyc
)
,
make_arrow_type
tyl
dity
let
tyc
,
(
argl
,
res
)
=
dtype_c
denv
tyc
in
DSpecA
(
bl
,
tyc
)
,
(
tyl
@
argl
,
res
)
let
dvariant
uc
=
function
|
Some
(
le
,
Some
q
)
->
[
le
,
Some
(
find_variant_ls
uc
q
)]
...
...
@@ -381,11 +387,20 @@ let dvariant uc = function
let
de_unit
~
loc
=
hidden_ls
~
loc
(
Term
.
fs_tuple
0
)
let
de_app
loc
e
el
=
let
res
=
create_type_variable
()
in
let
tyl
=
List
.
map
(
fun
a
->
(
a
.
de_loc
,
a
.
de_type
))
el
in
Loc
.
try2
loc
unify_list
e
.
de_type
tyl
res
;
DEapply
(
e
,
el
)
,
res
let
de_app
_loc
e
el
=
let
argl
,
res
=
e
.
de_type
in
let
rec
unify_list
argl
el
=
match
argl
,
el
with
|
arg
::
argl
,
e
::
el
when
Loc
.
equal
e
.
de_loc
Loc
.
dummy_position
->
expected_type
e
arg
;
unify_list
argl
el
|
arg
::
argl
,
e
::
el
->
let
res
=
unify_list
argl
el
in
expected_type
e
arg
;
res
|
argl
,
[]
->
argl
,
res
|
[]
,
_
when
fst
e
.
de_type
=
[]
->
errorm
~
loc
:
e
.
de_loc
"This expression is not a function and cannot be applied"
|
[]
,
_
->
errorm
~
loc
:
e
.
de_loc
"This function is applied to too many arguments"
in
DEapply
(
e
,
el
)
,
unify_list
argl
el
let
rec
dexpr
denv
e
=
let
loc
=
e
.
Ptree
.
expr_loc
in
...
...
@@ -398,9 +413,9 @@ let rec dexpr denv e =
and
de_desc
denv
loc
=
function
|
Ptree
.
Eident
(
Qident
{
id
=
x
})
when
Mstr
.
mem
x
denv
.
locals
->
(* local variable *)
let
tvs
,
d
i
ty
=
Mstr
.
find
x
denv
.
locals
in
let
d
i
ty
=
specialize_scheme
tvs
d
i
ty
in
DElocal
x
,
d
i
ty
let
tvs
,
d
v
ty
=
Mstr
.
find
x
denv
.
locals
in
let
d
v
ty
=
specialize_scheme
tvs
d
v
ty
in
DElocal
x
,
d
v
ty
|
Ptree
.
Eident
p
->
specialize_qualid
denv
.
uc
p
|
Ptree
.
Eapply
(
e1
,
e2
)
->
...
...
@@ -409,24 +424,25 @@ and de_desc denv loc = function
de_app
loc
(
dexpr
denv
e
)
el
|
Ptree
.
Elet
(
id
,
gh
,
e1
,
e2
)
->
let
e1
=
dexpr
denv
e1
in
let
d
i
ty
=
e1
.
de_type
in
let
d
v
ty
=
e1
.
de_type
in
let
tvars
=
match
e1
.
de_desc
with
|
DEfun
_
->
denv
.
tvars
|
_
->
add_
tvars
denv
.
tvars
d
i
ty
in
let
locals
=
Mstr
.
add
id
.
id
(
tvars
,
d
i
ty
)
denv
.
locals
in
|
_
->
add_
dvty
denv
.
tvars
d
v
ty
in
let
locals
=
Mstr
.
add
id
.
id
(
tvars
,
d
v
ty
)
denv
.
locals
in
let
denv
=
{
denv
with
locals
=
locals
;
tvars
=
tvars
}
in
let
e2
=
dexpr
denv
e2
in
DElet
(
id
,
gh
,
e1
,
e2
)
,
e2
.
de_type
|
Ptree
.
Eletrec
(
rdl
,
e1
)
->
let
rdl
=
dletrec
denv
rdl
in
let
add_one
denv
(
_
,
{
id
=
id
}
,
_
,
d
i
ty
,
_
)
=
{
denv
with
locals
=
Mstr
.
add
id
(
denv
.
tvars
,
d
i
ty
)
denv
.
locals
}
in
let
add_one
denv
(
_
,
{
id
=
id
}
,
_
,
d
v
ty
,
_
)
=
{
denv
with
locals
=
Mstr
.
add
id
(
denv
.
tvars
,
d
v
ty
)
denv
.
locals
}
in
let
denv
=
List
.
fold_left
add_one
denv
rdl
in
let
e1
=
dexpr
denv
e1
in
DEletrec
(
rdl
,
e1
)
,
e1
.
de_type
|
Ptree
.
Efun
(
bl
,
tr
)
->
let
lam
,
dity
=
dlambda
denv
bl
None
tr
in
DEfun
lam
,
dity
let
denv
,
bl
,
tyl
=
dbinders
denv
bl
in
let
lam
,
(
argl
,
res
)
=
dlambda
denv
bl
None
tr
in
DEfun
lam
,
(
tyl
@
argl
,
res
)
|
Ptree
.
Ecast
(
e1
,
pty
)
->
let
e1
=
dexpr
denv
e1
in
expected_type
e1
(
dity_of_pty
~
user
:
false
denv
pty
);
...
...
@@ -443,7 +459,9 @@ and de_desc denv loc = function
expected_type
e1
dity_bool
;
let
e2
=
dexpr
denv
e2
in
let
e3
=
dexpr
denv
e3
in
expected_type
e3
e2
.
de_type
;
let
res
=
create_type_variable
()
in
expected_type
e2
res
;
expected_type
e3
res
;
DEif
(
e1
,
e2
,
e3
)
,
e2
.
de_type
|
Ptree
.
Etuple
el
->
let
ls
=
fs_tuple
(
List
.
length
el
)
in
...
...
@@ -474,8 +492,8 @@ and de_desc denv loc = function
|
Some
e
->
dexpr
denv
e
|
None
->
let
loc
=
Loc
.
dummy_position
in
let
d
,
d
i
ty
=
de_app
loc
(
hidden_ls
~
loc
pj
)
[
e0
]
in
mk_dexpr
d
d
i
ty
loc
Slab
.
empty
in
let
d
,
d
v
ty
=
de_app
loc
(
hidden_ls
~
loc
pj
)
[
e0
]
in
mk_dexpr
d
d
v
ty
loc
Slab
.
empty
in
let
res
=
de_app
loc
(
hidden_ls
~
loc
cs
)
(
List
.
map
get_val
pjl
)
in
mk_let
~
loc
~
uloc
:
denv
.
uloc
e1
res
|
Ptree
.
Eupdate
(
e1
,
fl
)
->
...
...
@@ -487,8 +505,8 @@ and de_desc denv loc = function
|
Some
e
->
dexpr
denv
e
|
None
->
let
loc
=
Loc
.
dummy_position
in
let
d
,
d
i
ty
=
de_app
loc
(
hidden_pl
~
loc
pj
)
[
e0
]
in
mk_dexpr
d
d
i
ty
loc
Slab
.
empty
in
let
d
,
d
v
ty
=
de_app
loc
(
hidden_pl
~
loc
pj
)
[
e0
]
in
mk_dexpr
d
d
v
ty
loc
Slab
.
empty
in
let
res
=
de_app
loc
(
hidden_pl
~
loc
cs
)
(
List
.
map
get_val
pjl
)
in
mk_let
~
loc
~
uloc
:
denv
.
uloc
e1
res
|
Ptree
.
Eassign
(
e1
,
q
,
e2
)
->
...
...
@@ -496,34 +514,37 @@ and de_desc denv loc = function
let
e1
=
{
expr_desc
=
Eapply
(
fl
,
e1
);
expr_loc
=
loc
}
in
let
e1
=
dexpr
denv
e1
in
let
e2
=
dexpr
denv
e2
in
expected_type
~
weak
:
true
e2
e1
.
de_type
;
DEassign
(
e1
,
e2
)
,
dity_unit
let
res
=
create_type_variable
()
in
expected_type
e1
res
;
expected_type_weak
e2
res
;
DEassign
(
e1
,
e2
)
,
([]
,
dity_unit
)
|
Ptree
.
Econstant
(
ConstInt
_
as
c
)
->
DEconstant
c
,
dity_int
DEconstant
c
,
([]
,
dity_int
)
|
Ptree
.
Econstant
(
ConstReal
_
as
c
)
->
DEconstant
c
,
dity_real
DEconstant
c
,
([]
,
dity_real
)
|
Ptree
.
Enot
e1
->
let
e1
=
dexpr
denv
e1
in
expected_type
e1
dity_bool
;
DEnot
e1
,
dity_bool
DEnot
e1
,
([]
,
dity_bool
)
|
Ptree
.
Elazy
(
op
,
e1
,
e2
)
->
let
e1
=
dexpr
denv
e1
in
let
e2
=
dexpr
denv
e2
in
expected_type
e1
dity_bool
;
expected_type
e2
dity_bool
;
DElazy
(
op
,
e1
,
e2
)
,
dity_bool
DElazy
(
op
,
e1
,
e2
)
,
([]
,
dity_bool
)
|
Ptree
.
Ematch
(
e1
,
bl
)
->
let
e1
=
dexpr
denv
e1
in
let
ety
=
create_type_variable
()
in
let
res
=
create_type_variable
()
in
expected_type
e1
ety
;
let
branch
(
pp
,
e
)
=
let
ppat
,
dity
,
denv
=
dpattern
denv
pp
in
unify_loc
pp
.
pat_loc
unify
e1
.
de_type
dity
;
unify_loc
unify
pp
.
pat_loc
ety
dity
;
let
e
=
dexpr
denv
e
in
expected_type
e
res
;
ppat
,
e
in
DEmatch
(
e1
,
List
.
map
branch
bl
)
,
res
DEmatch
(
e1
,
List
.
map
branch
bl
)
,
([]
,
res
)
|
Ptree
.
Eraise
(
q
,
e1
)
->
let
res
=
create_type_variable
()
in
let
xs
=
find_xsymbol
denv
.
uc
q
in
let
dity
=
specialize_xsymbol
xs
in
let
e1
=
match
e1
with
...
...
@@ -531,9 +552,11 @@ and de_desc denv loc = function
|
None
when
ity_equal
xs
.
xs_ity
ity_unit
->
de_unit
~
loc
|
_
->
errorm
~
loc
"exception argument expected"
in
expected_type
e1
dity
;
DEraise
(
xs
,
e1
)
,
res
DEraise
(
xs
,
e1
)
,
([]
,
create_type_variable
()
)
|
Ptree
.
Etry
(
e1
,
cl
)
->
let
res
=
create_type_variable
()
in
let
e1
=
dexpr
denv
e1
in
expected_type
e1
res
;
let
branch
(
q
,
id
,
e
)
=
let
xs
=
find_xsymbol
denv
.
uc
q
in
let
dity
=
specialize_xsymbol
xs
in
...
...
@@ -541,21 +564,21 @@ and de_desc denv loc = function
|
Some
id
->
id
,
add_var
id
dity
denv
|
None
->
mk_id
"void"
loc
,
denv
in
let
e
=
dexpr
denv
e
in
expected_type
e
e1
.
de_type
;
expected_type
e
res
;
xs
,
id
,
e
in
let
cl
=
List
.
map
branch
cl
in
DEtry
(
e1
,
cl
)
,
e1
.
de_type
|
Ptree
.
Eabsurd
->
DEabsurd
,
create_type_variable
()
DEabsurd
,
([]
,
create_type_variable
()
)
|
Ptree
.
Eassert
(
ak
,
lexpr
)
->
DEassert
(
ak
,
lexpr
)
,
dity_unit
DEassert
(
ak
,
lexpr
)
,
([]
,
dity_unit
)
|
Ptree
.
Emark
(
id
,
e1
)
->
let
e1
=
dexpr
denv
e1
in
DEmark
(
id
,
e1
)
,
e1
.
de_type
|
Ptree
.
Eany
tyc
->
let
tyc
,
d
i
ty
=
dtype_c
denv
tyc
in
DEany
tyc
,
d
i
ty
let
tyc
,
d
v
ty
=
dtype_c
denv
tyc
in
DEany
tyc
,
d
v
ty
|
Ptree
.
Eghost
e1
->
let
e1
=
dexpr
denv
e1
in
DEghost
e1
,
e1
.
de_type
...
...
@@ -579,24 +602,34 @@ and de_desc denv loc = function
DEfor
(
id
,
efrom
,
dir
,
eto
,
inv
,
e1
)
,
e1
.
de_type
and
dletrec
denv
rdl
=
(* add all functions into environment *)
let
add_one
denv
(
_
,
id
,_,_,_,_
)
=
let
res
=
create_type_variable
()
in
add_var
id
res
denv
,
res
in
let
denv
,
tyl
=
Util
.
map_fold_left
add_one
denv
rdl
in
(* then type-check all of them and unify *)
let
type_one
(
loc
,
id
,
gh
,
bl
,
var
,
tr
)
res
=
let
lam
,
dity
=
dlambda
denv
bl
var
tr
in
Loc
.
try2
id
.
id_loc
unify
dity
res
;
loc
,
id
,
gh
,
dity
,
lam
in
List
.
map2
type_one
rdl
tyl
(* add all functions into the environment *)
let
add_one
denv
(
_
,
id
,_,
bl
,_,_
)
=
let
argl
=
List
.
map
(
fun
_
->
create_type_variable
()
)
bl
in
let
dvty
=
argl
,
create_type_variable
()
in
let
tvars
=
add_dvty
denv
.
tvars
dvty
in
let
locals
=
Mstr
.
add
id
.
id
(
tvars
,
dvty
)
denv
.
locals
in
{
denv
with
locals
=
locals
;
tvars
=
tvars
}
,
dvty
in
let
denv
,
dvtyl
=
Util
.
map_fold_left
add_one
denv
rdl
in
(* then unify the binders *)
let
bind_one
(
_
,_,_,
bl
,_,_
)
(
argl
,
res
)
=
let
denv
,
bl
,
tyl
=
dbinders
denv
bl
in
List
.
iter2
unify
argl
tyl
;
denv
,
bl
,
tyl
,
res
in
let
denvl
=
List
.
map2
bind_one
rdl
dvtyl
in
(* then type-check the bodies *)
let
type_one
(
loc
,
id
,
gh
,
_
,
var
,
tr
)
(
denv
,
bl
,
tyl
,
tyv
)
=
let
lam
,
(
argl
,
res
)
=
dlambda
denv
bl
var
tr
in
if
argl
<>
[]
then
errorm
~
loc
"The body of a recursive function must be a first-order value"
;
unify_loc
unify
loc
tyv
res
;
loc
,
id
,
gh
,
(
tyl
,
tyv
)
,
lam
in
List
.
map2
type_one
rdl
denvl
and
dlambda
denv
bl
var
(
p
,
e
,
(
q
,
xq
))
=
let
denv
,
bl
,
tyl
=
dbinders
denv
bl
in
let
e
=
dexpr
denv
e
in
let
var
=
dvariant
denv
.
uc
var
in
let
xq
=
dxpost
denv
.
uc
xq
in
(
bl
,
var
,
p
,
e
,
q
,
xq
)
,
make_arrow_type
tyl
e
.
de_type
(
bl
,
var
,
p
,
e
,
q
,
xq
)
,
e
.
de_type
(** stage 2 *)
...
...
@@ -704,7 +737,7 @@ let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
let
itya
,
vtvv
=
try
Mls
.
find
(
uc_find_ls
lenv
.
mod_uc
p
)
pjm
with
Not_found
->
errorm
~
loc
:
(
qloc
p
)
"'%a' must be a field name"
print_qualid
p
in
let
sbs
=
unify_loc
loc
(
ity_match
ity_subst_empty
)
itya
vtv
.
vtv_ity
in
let
sbs
=
unify_loc
(
ity_match
ity_subst_empty
)
loc
itya
vtv
.
vtv_ity
in
let
mut
=
Util
.
option_map
(
reg_full_inst
sbs
)
vtvv
.
vtv_mut
in
let
ghost
=
vtv
.
vtv_ghost
||
vtvv
.
vtv_ghost
in
vty_value
~
ghost
?
mut
(
ity_full_inst
sbs
vtvv
.
vtv_ity
)
...
...
@@ -790,7 +823,7 @@ and expr_desc lenv loc de = match de.de_desc with
assert
(
Mstr
.
mem
x
lenv
.
let_vars
);
begin
match
Mstr
.
find
x
lenv
.
let_vars
with
|
LetV
pv
->
e_value
pv
|
LetA
ps
->
e_cast
ps
(
vty_of_d
i
ty
de
.
de_type
)
|
LetA
ps
->
e_cast
ps
(
vty_of_d
v
ty
de
.
de_type
)
end
|
DElet
(
x
,
gh
,
{
de_desc
=
DEfun
lam
}
,
de2
)
->
let
def
=
expr_fun
lenv
x
gh
lam
in
...
...
@@ -827,18 +860,18 @@ and expr_desc lenv loc de = match de.de_desc with
|
DEapply
(
de1
,
del
)
->
let
el
=
List
.
map
(
expr
lenv
)
del
in
begin
match
de1
.
de_desc
with
|
DEglobal_pl
pls
->
e_plapp
pls
el
(
ity_of_dity
de
.
de_type
)
|
DEglobal_ls
ls
->
e_lapp
ls
el
(
ity_of_dity
de
.
de_type
)
|
DEglobal_pl
pls
->
e_plapp
pls
el
(
ity_of_dity
(
snd
de
.
de_type
)
)
|
DEglobal_ls
ls
->
e_lapp
ls
el
(
ity_of_dity
(
snd
de
.
de_type
)
)
|
_
->
e_app
(
expr
lenv
de1
)
el
end
|
DEglobal_pv
pv
->
e_value
pv
|
DEglobal_ps
ps
->
e_cast
ps
(
vty_of_d
i
ty
de
.
de_type
)
e_cast
ps
(
vty_of_d
v
ty
de
.
de_type
)
|
DEglobal_pl
pl
->
e_plapp
pl
[]
(
ity_of_dity
de
.
de_type
)
e_plapp
pl
[]
(
ity_of_dity
(
snd
de
.
de_type
)
)
|
DEglobal_ls
ls
->
e_lapp
ls
[]
(
ity_of_dity
de
.
de_type
)
e_lapp
ls
[]
(
ity_of_dity
(
snd
de
.
de_type
)
)