Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
852600ca
Commit
852600ca
authored
Jun 10, 2015
by
David Hauzar
Browse files
Merge branch 'master' into counter-examples
parents
c4248ce9
0febaa22
Changes
7
Hide whitespace changes
Inline
Side-by-side
src/mlw/dexpr.ml
View file @
852600ca
...
...
@@ -307,7 +307,9 @@ type ghost = bool
type
dbinder
=
preid
option
*
ghost
*
dity
type
'
a
later
=
vsymbol
Mstr
.
t
->
'
a
type
register_old
=
pvsymbol
->
string
->
pvsymbol
type
'
a
later
=
pvsymbol
Mstr
.
t
->
register_old
->
'
a
(* specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are
already established. *)
...
...
@@ -712,10 +714,8 @@ let create_assert = to_fmla
let
create_invariant
pl
=
List
.
map
to_fmla
pl
let
create_pre
=
create_invariant
let
create_post
ty
ql
=
List
.
map
(
fun
(
v
,
f
)
->
let
f
=
(*Mlw_wp.remove_old*)
(
to_fmla
f
)
in
match
v
with
let
f
=
to_fmla
f
in
match
v
with
|
None
->
Ity
.
create_post
(
create_vsymbol
(
id_fresh
"result"
)
ty
)
f
|
Some
v
->
Ty
.
ty_equal_check
ty
v
.
vs_ty
;
Ity
.
create_post
v
f
)
ql
...
...
@@ -771,8 +771,8 @@ let check_spec dsp ecty e =
(* computed effect vs user effect *)
let
check_rwd
=
dsp
.
ds_checkrw
in
let
uwrl
,
ue
=
effect_of_dspec
dsp
in
let
ucty
=
create_cty
ecty
.
cty_args
ecty
.
cty_pre
ecty
.
cty_post
ecty
.
cty_
xpost
ue
ecty
.
cty_result
in
let
ucty
=
create_cty
ecty
.
cty_args
ecty
.
cty_pre
ecty
.
cty_post
ecty
.
cty_
x
post
ecty
.
cty_
oldies
ue
ecty
.
cty_result
in
let
ueff
=
ucty
.
cty_effect
and
eeff
=
ecty
.
cty_effect
in
let
urds
=
ueff
.
eff_reads
and
erds
=
eeff
.
eff_reads
in
(* check that every user effect actually happens *)
...
...
@@ -843,29 +843,80 @@ let check_fun rsym dsp e =
type
env
=
{
rsm
:
rsymbol
Mstr
.
t
;
pvm
:
pvsymbol
Mstr
.
t
;
vsm
:
vsymbol
Mstr
.
t
;
old
:
(
pvsymbol
Mstr
.
t
*
(
let_defn
*
pvsymbol
)
Hpv
.
t
)
Mstr
.
t
;
}
let
env_empty
=
{
rsm
=
Mstr
.
empty
;
pvm
=
Mstr
.
empty
;
vsm
=
Mstr
.
empty
;
old
=
Mstr
.
empty
;
}
let
add_rsymbol
({
rsm
=
rsm
;
vsm
=
vsm
}
as
env
)
rs
=
exception
UnboundLabel
of
string
let
find_old
pvm
(
ovm
,
old
)
v
=
let
n
=
v
.
pv_vs
.
vs_name
.
id_string
in
(* if v is top-level, both ov and pv are None.
If v is local, ov and pv must be equal to v.
If they are not equal, then v is defined under the label,
so we return v and do not register an "oldie" for it. *)
let
ov
=
Mstr
.
find_opt
n
ovm
in
let
pv
=
Mstr
.
find_opt
n
pvm
in
if
not
(
Opt
.
equal
pv_equal
ov
pv
)
then
v
else
match
Hpv
.
find_opt
old
v
with
|
Some
(
_
,
o
)
->
o
|
None
->
let
e
=
e_pure
(
t_var
v
.
pv_vs
)
in
let
id
=
id_clone
v
.
pv_vs
.
vs_name
in
let
ld
=
let_var
id
~
ghost
:
true
e
in
Hpv
.
add
old
v
ld
;
snd
ld
let
register_old
env
v
l
=
find_old
env
.
pvm
(
Mstr
.
find_exn
(
UnboundLabel
l
)
l
env
.
old
)
v
let
get_later
env
later
=
later
env
.
pvm
(
register_old
env
)
let
add_label
({
pvm
=
pvm
;
old
=
old
}
as
env
)
l
=
let
ht
=
Hpv
.
create
3
in
{
env
with
old
=
Mstr
.
add
l
(
pvm
,
ht
)
old
}
,
ht
let
rebase_old
{
pvm
=
pvm
}
preold
old
fvs
=
let
rebase
v
(
_
,
{
pv_vs
=
o
})
sbs
=
if
not
(
Mvs
.
mem
o
fvs
)
then
sbs
else
match
preold
with
|
Some
preold
->
Mvs
.
add
o
(
t_var
(
find_old
pvm
preold
v
)
.
pv_vs
)
sbs
|
None
->
raise
(
UnboundLabel
"'0"
)
in
Hpv
.
fold
rebase
old
Mvs
.
empty
let
rebase_pre
env
preold
old
pl
=
let
pl
=
List
.
map
to_fmla
pl
in
let
fvs
=
List
.
fold_left
t_freevars
Mvs
.
empty
pl
in
let
sbs
=
rebase_old
env
preold
old
fvs
in
List
.
map
(
t_subst
sbs
)
pl
let
rebase_variant
env
preold
old
varl
=
let
add
s
(
t
,_
)
=
t_freevars
s
t
in
let
fvs
=
List
.
fold_left
add
Mvs
.
empty
varl
in
let
sbs
=
rebase_old
env
preold
old
fvs
in
let
conv
(
t
,
rel
)
=
t_subst
sbs
t
,
rel
in
List
.
map
conv
varl
let
get_oldies
old
=
Hpv
.
fold
(
fun
v
(
_
,
o
)
sbs
->
Mpv
.
add
o
v
sbs
)
old
Mpv
.
empty
let
add_rsymbol
({
rsm
=
rsm
;
pvm
=
pvm
}
as
env
)
rs
=
let
n
=
rs
.
rs_name
.
id_string
in
let
v
s
m
=
match
rs
.
rs_logic
with
|
RLpv
pv
->
Mstr
.
add
n
pv
.
pv_vs
vs
m
|
_
->
v
s
m
in
{
env
with
rsm
=
Mstr
.
add
n
rs
rsm
;
v
s
m
=
v
s
m
}
let
p
vm
=
match
rs
.
rs_logic
with
|
RLpv
pv
->
Mstr
.
add
n
pv
pv
m
|
_
->
p
vm
in
{
env
with
rsm
=
Mstr
.
add
n
rs
rsm
;
p
vm
=
p
vm
}
let
add_pvsymbol
({
pvm
=
pvm
;
vsm
=
vsm
}
as
env
)
pv
=
let
add_pvsymbol
({
pvm
=
pvm
}
as
env
)
pv
=
let
n
=
pv
.
pv_vs
.
vs_name
.
id_string
in
{
env
with
pvm
=
Mstr
.
add
n
pv
pvm
;
vsm
=
Mstr
.
add
n
pv
.
pv_vs
vsm
}
{
env
with
pvm
=
Mstr
.
add
n
pv
pvm
}
let
add_pv_map
({
pvm
=
pvm
;
vsm
=
vsm
}
as
env
)
vm
=
let
um
=
Mstr
.
map
(
fun
pv
->
pv
.
pv_vs
)
vm
in
{
env
with
pvm
=
Mstr
.
set_union
vm
pvm
;
vsm
=
Mstr
.
set_union
um
vsm
}
let
add_pv_map
({
pvm
=
pvm
}
as
env
)
vm
=
{
env
with
pvm
=
Mstr
.
set_union
vm
pvm
}
let
add_binders
env
pvl
=
List
.
fold_left
add_pvsymbol
env
pvl
...
...
@@ -876,13 +927,15 @@ let cty_of_spec env bl dsp dity =
let
ty
=
ty_of_ity
ity
in
let
bl
=
binders
bl
in
let
env
=
add_binders
env
bl
in
let
dsp
=
dsp
env
.
vsm
ty
in
let
_
,
eff
=
effect_of_dspec
dsp
in
let
preold
=
Mstr
.
find_opt
"'0"
env
.
old
in
let
env
,
old
=
add_label
env
"'0"
in
let
dsp
=
get_later
env
dsp
ty
in
let
_
,
eff
=
effect_of_dspec
dsp
in
let
eff
=
eff_strong
eff
in
let
p
=
c
re
at
e_pre
dsp
.
ds_pre
in
let
p
=
re
bas
e_pre
env
preold
old
dsp
.
ds_pre
in
let
q
=
create_post
ty
dsp
.
ds_post
in
let
xq
=
create_xpost
dsp
.
ds_xpost
in
create_cty
bl
p
q
xq
eff
ity
create_cty
bl
p
q
xq
(
get_oldies
old
)
eff
ity
(** Expressions *)
...
...
@@ -937,7 +990,8 @@ and try_cexp uloc env ghost de0 = match de0.de_node with
|
_
->
app
(
cexp
uloc
env
ghost
de
)
el
in
down
de0
[]
|
DEfun
(
bl
,
dsp
,
de
)
->
let
c
,
dsp
,
_
=
lambda
uloc
env
(
binders
bl
)
dsp
de
in
let
dvl
_
_
=
[]
in
let
c
,
dsp
,
_
=
lambda
uloc
env
(
binders
bl
)
dsp
dvl
de
in
check_fun
None
dsp
c
;
[]
,
c_ghostify
ghost
c
|
DEany
(
bl
,
dsp
,
dity
)
->
...
...
@@ -1038,8 +1092,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
|
DEwhile
(
de1
,
dinv
,
dvarl
,
de2
)
->
let
e1
=
expr
uloc
env
de1
in
let
e2
=
expr
uloc
env
de2
in
let
inv
=
dinv
env
.
vsm
in
let
varl
=
dvarl
env
.
vsm
in
let
inv
=
get_later
env
dinv
in
let
varl
=
get_later
env
dvarl
in
e_while
e1
(
create_invariant
inv
)
varl
e2
|
DEfor
(
id
,
de_from
,
dir
,
de_to
,
dinv
,
de
)
->
let
e_from
=
expr
uloc
env
de_from
in
...
...
@@ -1047,7 +1101,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let
v
=
create_pvsymbol
id
ity_int
in
let
env
=
add_pvsymbol
env
v
in
let
e
=
expr
uloc
env
de
in
let
inv
=
dinv
env
.
vsm
in
let
inv
=
get_later
env
dinv
in
e_for
v
e_from
dir
e_to
(
create_invariant
inv
)
e
|
DEtry
(
de1
,
bl
)
->
let
e1
=
expr
uloc
env
de1
in
...
...
@@ -1080,21 +1134,19 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
|
DEghost
de
->
e_ghostify
true
(
expr
uloc
env
de
)
|
DEassert
(
ak
,
f
)
->
e_assert
ak
(
create_assert
(
f
env
.
vsm
))
e_assert
ak
(
create_assert
(
get_later
env
f
))
|
DEpure
t
->
e_pure
(
t
env
.
vsm
)
e_pure
(
get_later
env
t
)
|
DEabsurd
->
e_absurd
(
ity_of_dity
res
)
|
DEtrue
->
e_true
|
DEfalse
->
e_false
|
DEmark
_
->
assert
false
(* TODO *)
(*
let ld,v = create_let_defn_pv id Mlw_wp.e_now in
let env = add_pvsymbol env v in
e_let ld (expr uloc env de)
*)
|
DEmark
({
pre_name
=
l
}
,
de
)
->
let
env
,
old
=
add_label
env
l
in
let
put
_
(
ld
,_
)
e
=
e_let
ld
e
in
Hpv
.
fold
put
old
(
expr
uloc
env
de
)
|
DEcast
_
|
DEuloc
_
|
DElabel
_
->
assert
false
(* already stripped *)
...
...
@@ -1118,15 +1170,15 @@ and rec_defn uloc env ghost {fds = dfdl} =
let
step1
env
(
id
,
gh
,
kind
,
bl
,
dsp
,
dvl
,
({
de_dvty
=
dvty
}
as
de
))
=
let
pvl
=
binders
bl
in
let
ity
=
Loc
.
try1
?
loc
:
de
.
de_loc
ity_of_dity
(
dity_of_dvty
dvty
)
in
let
cty
=
create_cty
pvl
[]
[]
Mexn
.
empty
eff_empty
ity
in
let
cty
=
create_cty
pvl
[]
[]
Mexn
.
empty
Mpv
.
empty
eff_empty
ity
in
let
rs
=
create_rsymbol
id
~
ghost
:
(
gh
||
ghost
)
~
kind
:
RKnone
cty
in
add_rsymbol
env
rs
,
(
rs
,
kind
,
dsp
,
dvl
,
de
)
in
let
env
,
fdl
=
Lists
.
map_fold_left
step1
env
dfdl
in
let
step2
({
rs_cty
=
c
}
as
rs
,
kind
,
dsp
,
dvl
,
de
)
(
fdl
,
dspl
)
=
let
lam
,
dsp
,
env
=
lambda
uloc
env
c
.
cty_args
dsp
de
in
let
lam
,
dsp
,
dvl
=
lambda
uloc
env
c
.
cty_args
dsp
dvl
de
in
if
c_ghost
lam
&&
not
(
rs_ghost
rs
)
then
Loc
.
errorm
?
loc
:
rs
.
rs_name
.
id_loc
"Function %s must be explicitly marked ghost"
rs
.
rs_name
.
id_string
;
(
rs
,
lam
,
dvl
env
.
vsm
,
kind
)
::
fdl
,
dsp
::
dspl
in
(
rs
,
lam
,
dvl
,
kind
)
::
fdl
,
dsp
::
dspl
in
(* check for unexpected aliases in case of trouble *)
let
fdl
,
dspl
=
try
List
.
fold_right
step2
fdl
([]
,
[]
)
with
|
Loc
.
Located
(
_
,
Ity
.
TypeMismatch
_
)
|
Ity
.
TypeMismatch
_
as
exn
->
...
...
@@ -1143,15 +1195,19 @@ and rec_defn uloc env ghost {fds = dfdl} =
add_rsymbol
env
s
in
ld
,
List
.
fold_left2
add_fd
env
rdl
dspl
and
lambda
uloc
env
pvl
dsp
de
=
and
lambda
uloc
env
pvl
dsp
dvl
de
=
let
env
=
add_binders
env
pvl
in
let
e
=
expr
uloc
env
de
in
let
ty
=
ty_of_ity
e
.
e_ity
in
let
dsp
=
dsp
env
.
vsm
ty
in
let
p
=
create_pre
dsp
.
ds_pre
in
let
preold
=
Mstr
.
find_opt
"'0"
env
.
old
in
let
env
,
old
=
add_label
env
"'0"
in
let
dsp
=
get_later
env
dsp
ty
in
let
dvl
=
get_later
env
dvl
in
let
dvl
=
rebase_variant
env
preold
old
dvl
in
let
p
=
rebase_pre
env
preold
old
dsp
.
ds_pre
in
let
q
=
create_post
ty
dsp
.
ds_post
in
let
xq
=
create_xpost
dsp
.
ds_xpost
in
c_fun
pvl
p
q
xq
e
,
dsp
,
env
c_fun
pvl
p
q
xq
(
get_oldies
old
)
e
,
dsp
,
dvl
let
rec_defn
?
(
keep_loc
=
true
)
drdf
=
reunify_regions
()
;
...
...
@@ -1173,7 +1229,7 @@ let let_defn ?(keep_loc=true) (id,ghost,kind,de) =
let
e
=
expr
uloc
env_empty
de
in
if
e_ghost
e
&&
not
ghost
then
Loc
.
errorm
?
loc
:
id
.
pre_loc
"Function %s must be explicitly marked ghost"
id
.
pre_name
;
let
c
=
c_fun
[]
[]
[]
Mexn
.
empty
e
in
let
c
=
c_fun
[]
[]
[]
Mexn
.
empty
Mpv
.
empty
e
in
(* the rsymbol will carry a single postcondition "the result
is equal to the logical constant". Any user-written spec
will be checked once, in-place, under Eexec. Since kind
...
...
@@ -1202,3 +1258,8 @@ let expr ?(keep_loc=true) de =
reunify_regions
()
;
let
uloc
=
if
keep_loc
then
None
else
Some
None
in
expr
uloc
env_empty
de
let
()
=
Exn_printer
.
register
(
fun
fmt
e
->
match
e
with
|
UnboundLabel
s
->
Format
.
fprintf
fmt
"unbound label %s"
s
|
_
->
raise
e
)
src/mlw/dexpr.mli
View file @
852600ca
...
...
@@ -55,10 +55,16 @@ type dbinder = preid option * ghost * dity
(** Specifications *)
type
'
a
later
=
vsymbol
Mstr
.
t
->
'
a
(* Specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are
already established. *)
exception
UnboundLabel
of
string
type
register_old
=
pvsymbol
->
string
->
pvsymbol
(** Program variables occurring under [old] or [at] are passed to
a registrar function. The label string must be ['0] for [old]. *)
type
'
a
later
=
pvsymbol
Mstr
.
t
->
register_old
->
'
a
(** Specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are
already established. *)
type
dspec_final
=
{
ds_pre
:
term
list
;
...
...
src/mlw/expr.ml
View file @
852600ca
...
...
@@ -170,7 +170,7 @@ let create_projection s v =
let
arg
=
create_pvsymbol
(
id_fresh
"arg"
)
ity
in
let
ls
=
create_fsymbol
id
[
arg
.
pv_vs
.
vs_ty
]
v
.
pv_vs
.
vs_ty
in
let
q
=
make_post
(
fs_app
ls
[
t_var
arg
.
pv_vs
]
v
.
pv_vs
.
vs_ty
)
in
let
c
=
create_cty
[
arg
]
[]
[
q
]
Mexn
.
empty
eff
v
.
pv_ity
in
let
c
=
create_cty
[
arg
]
[]
[
q
]
Mexn
.
empty
Mpv
.
empty
eff
v
.
pv_ity
in
mk_rs
ls
.
ls_name
c
(
RLls
ls
)
(
Some
v
)
exception
FieldExpected
of
rsymbol
...
...
@@ -196,7 +196,7 @@ let create_constructor ~constr id s fl =
let
ls
=
create_fsymbol
~
constr
id
argl
ty
in
let
argl
=
List
.
map
(
fun
a
->
t_var
a
.
pv_vs
)
fl
in
let
q
=
make_post
(
fs_app
ls
argl
ty
)
in
let
c
=
create_cty
fl
[]
[
q
]
Mexn
.
empty
eff_empty
ity
in
let
c
=
create_cty
fl
[]
[
q
]
Mexn
.
empty
Mpv
.
empty
eff_empty
ity
in
mk_rs
ls
.
ls_name
c
(
RLls
ls
)
None
let
rs_of_ls
ls
=
...
...
@@ -205,7 +205,7 @@ let rs_of_ls ls =
let
t_args
=
List
.
map
(
fun
v
->
t_var
v
.
pv_vs
)
v_args
in
let
q
=
make_post
(
t_app
ls
t_args
ls
.
ls_value
)
in
let
ity
=
ity_of_ty
(
t_type
q
)
in
let
c
=
create_cty
v_args
[]
[
q
]
Mexn
.
empty
eff_empty
ity
in
let
c
=
create_cty
v_args
[]
[
q
]
Mexn
.
empty
Mpv
.
empty
eff_empty
ity
in
mk_rs
ls
.
ls_name
c
(
RLls
ls
)
None
let
rs_ghost
s
=
s
.
rs_cty
.
cty_effect
.
eff_ghost
...
...
@@ -492,8 +492,12 @@ let e_exec ({c_cty = cty} as c) = match cty.cty_args with
let
c_any
c
=
mk_cexp
Cany
c
let
c_fun
args
p
q
xq
({
e_effect
=
eff
}
as
e
)
=
mk_cexp
(
Cfun
e
)
(
create_cty
args
p
q
xq
eff
e
.
e_ity
)
let
c_fun
args
p
q
xq
old
({
e_effect
=
eff
}
as
e
)
=
(* reset variables are forbidden in post-conditions *)
let
c
=
try
create_cty
args
p
q
xq
old
eff
e
.
e_ity
with
|
BadGhostWrite
(
v
,
r
)
->
localize_ghost_write
v
r
[
e
]
|
StaleVariable
(
v
,
r
)
->
localize_cover_stale
v
r
[
e
]
in
mk_cexp
(
Cfun
e
)
c
let
c_app
s
vl
ityl
ity
=
mk_cexp
(
Capp
(
s
,
vl
))
(
cty_apply
s
.
rs_cty
vl
ityl
ity
)
...
...
@@ -741,7 +745,8 @@ and c_rs_subst sm ({c_node = n; c_cty = c} as d) =
let
al
=
List
.
map
(
fun
v
->
v
.
pv_ity
)
c
.
cty_args
in
c_app
(
Mrs
.
find_def
s
s
sm
)
vl
al
c
.
cty_result
|
Cfun
e
->
c_fun
c
.
cty_args
c
.
cty_pre
c
.
cty_post
c
.
cty_xpost
(
e_rs_subst
sm
e
))
c_fun
c
.
cty_args
c
.
cty_pre
c
.
cty_post
c
.
cty_xpost
c
.
cty_oldies
(
e_rs_subst
sm
e
))
and
rec_fixp
dl
=
let
update
sm
(
s
,
({
c_cty
=
c
}
as
d
))
=
...
...
@@ -809,7 +814,7 @@ let let_rec fdl =
(* create the clean rsymbol *)
let
id
=
id_clone
s
.
rs_name
in
let
c
=
create_cty
c
.
cty_args
pre
c
.
cty_post
c
.
cty_xpost
start_eff
c
.
cty_result
in
c
.
cty_post
c
.
cty_xpost
c
.
cty_oldies
start_eff
c
.
cty_result
in
let
ns
=
create_rsymbol
id
~
ghost
:
(
rs_ghost
s
)
~
kind
:
RKnone
c
in
let
sm
=
Mrs
.
add_new
(
Invalid_argument
"Expr.let_rec"
)
s
ns
sm
in
sm
,
(
ns
,
c_ghostify
(
rs_ghost
s
)
d
)
in
...
...
src/mlw/expr.mli
View file @
852600ca
...
...
@@ -176,8 +176,8 @@ val ls_decr_of_let_defn : let_defn -> lsymbol option
val
c_app
:
rsymbol
->
pvsymbol
list
->
ity
list
->
ity
->
cexp
val
c_fun
:
pvsymbol
list
->
pre
list
->
post
list
->
post
list
Mexn
.
t
->
expr
->
cexp
val
c_fun
:
pvsymbol
list
->
pre
list
->
post
list
->
post
list
Mexn
.
t
->
pvsymbol
Mpv
.
t
->
expr
->
cexp
val
c_any
:
cty
->
cexp
...
...
src/mlw/ity.ml
View file @
852600ca
...
...
@@ -712,7 +712,7 @@ let eff_read_post e rd =
let
_
=
check_covers
e
.
eff_covers
rd
in
{
e
with
eff_reads
=
Spv
.
union
e
.
eff_reads
rd
}
let
eff_bind
rd
e
=
if
S
pv
.
is_empty
rd
then
e
else
let
eff_bind
rd
e
=
if
M
pv
.
is_empty
rd
then
e
else
{
e
with
eff_reads
=
Mpv
.
set_diff
e
.
eff_reads
rd
}
let
eff_read
rd
=
...
...
@@ -888,16 +888,18 @@ type cty = {
cty_pre
:
pre
list
;
cty_post
:
post
list
;
cty_xpost
:
post
list
Mexn
.
t
;
cty_oldies
:
pvsymbol
Mpv
.
t
;
cty_effect
:
effect
;
cty_result
:
ity
;
cty_freeze
:
ity_subst
;
}
let
cty_unsafe
args
pre
post
xpost
effect
result
freeze
=
{
let
cty_unsafe
args
pre
post
xpost
oldies
effect
result
freeze
=
{
cty_args
=
args
;
cty_pre
=
pre
;
cty_post
=
post
;
cty_xpost
=
xpost
;
cty_oldies
=
oldies
;
cty_effect
=
effect
;
cty_result
=
result
;
cty_freeze
=
freeze
;
...
...
@@ -939,17 +941,26 @@ let check_post exn ity post =
|
Teps
_
->
Ty
.
ty_equal_check
ty
(
t_type
q
)
|
_
->
raise
exn
)
post
let
create_cty
args
pre
post
xpost
effect
result
=
let
create_cty
args
pre
post
xpost
oldies
effect
result
=
let
exn
=
Invalid_argument
"Ity.create_cty"
in
(* pre, post, and xpost are well-typed *)
check_pre
pre
;
check_post
exn
result
post
;
Mexn
.
iter
(
fun
xs
xq
->
check_post
exn
xs
.
xs_ity
xq
)
xpost
;
(* the arguments must be pairwise distinct *)
let
sarg
=
List
.
fold_right
(
Spv
.
add_new
exn
)
args
Spv
.
empty
in
(* complete the reads and freeze the external context
FIXME/TODO: detect stale variables in post and xpost *)
let
reads
=
spec_t_fold
t_freepvs
sarg
pre
post
xpost
in
let
effect
=
eff_read_pre
reads
effect
in
(* complete the reads and freeze the external context.
oldies must be fresh: collisions with args and external
reads are forbidden, to simplify instantiation later. *)
let
preads
=
spec_t_fold
t_freepvs
sarg
pre
[]
Mexn
.
empty
in
let
qreads
=
spec_t_fold
t_freepvs
Spv
.
empty
[]
post
xpost
in
let
effect
=
eff_read_post
effect
qreads
in
Mpv
.
iter
(
fun
{
pv_ghost
=
gh
;
pv_ity
=
o
}
{
pv_ity
=
t
}
->
if
not
(
gh
&&
o
==
ity_purify
t
)
then
raise
exn
)
oldies
;
let
oldies
=
Mpv
.
set_inter
oldies
effect
.
eff_reads
in
let
effect
=
eff_bind
oldies
effect
in
let
preads
=
Mpv
.
fold
(
Util
.
const
Spv
.
add
)
oldies
preads
in
if
not
(
Mpv
.
set_disjoint
preads
oldies
)
then
raise
exn
;
let
effect
=
eff_read_pre
preads
effect
in
let
freeze
=
Spv
.
diff
effect
.
eff_reads
sarg
in
let
freeze
=
Spv
.
fold
freeze_pv
freeze
isb_empty
in
check_tvs
effect
.
eff_reads
result
pre
post
xpost
;
...
...
@@ -984,11 +995,11 @@ let create_cty args pre post xpost effect result =
let
resets
=
Mreg
.
map
(
fun
_
->
Sreg
.
empty
)
unknwn
in
let
covers
=
Mreg
.
set_union
resets
effect
.
eff_covers
in
let
effect
=
{
effect
with
eff_covers
=
covers
}
in
cty_unsafe
args
pre
post
xpost
effect
result
freeze
cty_unsafe
args
pre
post
xpost
oldies
effect
result
freeze
let
cty_apply
c
vl
args
res
=
let
vsb_add
vsb
{
pv_vs
=
u
}
{
pv_vs
=
v
}
=
if
vs_equal
u
v
then
vsb
else
Mvs
.
add
u
(
t_var
v
)
vsb
in
let
vsb_add
vsb
{
pv_vs
=
u
}
v
=
if
vs_equal
u
v
.
pv_vs
then
vsb
else
Mvs
.
add
u
v
vsb
in
let
match_v
isb
u
v
=
ity_match
isb
u
.
pv_ity
v
.
pv_ity
in
(* stage 1: apply c to vl *)
let
rec
apply
gh
same
isb
vsb
ul
vl
=
match
ul
,
vl
with
...
...
@@ -1015,6 +1026,13 @@ let cty_apply c vl args res =
|
[]
,
[]
->
same
,
rul
,
rvl
,
vsb
|
_
->
invalid_arg
"Ity.cty_apply"
in
let
same
,
rcargs
,
rargs
,
vsb
=
cut
same
[]
[]
vsb
cargs
args
in
let
vsb
,
oldies
=
if
Mvs
.
is_empty
vsb
then
vsb
,
c
.
cty_oldies
else
Mpv
.
fold
(
fun
{
pv_vs
=
o
}
v
(
s
,
m
)
->
let
id
=
id_clone
o
.
vs_name
in
let
v
=
Mvs
.
find_def
v
v
.
pv_vs
vsb
in
let
n
=
create_pvsymbol
id
~
ghost
:
true
(
ity_purify
v
.
pv_ity
)
in
Mvs
.
add
o
n
s
,
Mpv
.
add
n
v
m
)
c
.
cty_oldies
(
vsb
,
Mpv
.
empty
)
in
let
vsb
=
Mvs
.
map
(
fun
v
->
t_var
v
.
pv_vs
)
vsb
in
let
same
=
same
&&
ity_equal
c
.
cty_result
res
in
if
same
&&
vl
=
[]
then
(* trivial *)
c
else
let
isb
=
if
same
then
isb_empty
else
...
...
@@ -1045,7 +1063,7 @@ let cty_apply c vl args res =
let
subst_l
l
=
List
.
map
subst_t
l
in
cty_unsafe
(
List
.
rev
rargs
)
(
subst_l
c
.
cty_pre
)
(
subst_l
c
.
cty_post
)
(
Mexn
.
map
subst_l
c
.
cty_xpost
)
effect
res
freeze
oldies
effect
res
freeze
let
cty_add_reads
c
pvs
=
(* the external reads are already frozen and
...
...
src/mlw/ity.mli
View file @
852600ca
...
...
@@ -338,24 +338,29 @@ type cty = private {
cty_pre
:
pre
list
;
cty_post
:
post
list
;
cty_xpost
:
post
list
Mexn
.
t
;
cty_oldies
:
pvsymbol
Mpv
.
t
;
cty_effect
:
effect
;
cty_result
:
ity
;
cty_freeze
:
ity_subst
;
}
val
create_cty
:
pvsymbol
list
->
pre
list
->
post
list
->
post
list
Mexn
.
t
->
effect
->
ity
->
cty
(** [create_cty args pre post xpost effect result] creates a cty.
pre
list
->
post
list
->
post
list
Mexn
.
t
->
pvsymbol
Mpv
.
t
->
effect
->
ity
->
cty
(** [create_cty args pre post xpost oldies effect result] creates a cty.
The [cty_xpost] field does not have to cover all raised exceptions.
[cty_effect.eff_reads] is completed wrt the specification and [args].
[cty_freeze] freezes every unbound pvsymbol in [cty_effect.eff_reads].
All effects on regions outside [cty_effect.eff_reads] are removed.
Fresh regions in [result] are reset. Every type variable in [pre],
[post], and [xpost] must come from [cty_reads], [args] or [result]. *)
[post], and [xpost] must come from [cty_reads], [args] or [result].
[oldies] maps ghost pure snapshots of the parameters and external
reads to the original pvsymbols: these snaphosts are removed from
[cty_effect.eff_reads] and replaced with the originals. *)
val
cty_apply
:
cty
->
pvsymbol
list
->
ity
list
->
ity
->
cty
(** [cty_apply cty pvl rest res] instantiates [cty] up to the types in
[pvl], [rest] and [res], then applies it to the arguments in [pvl],
[pvl], [rest]
,
and [res], then applies it to the arguments in [pvl],
and returns the computation type of the result, [rest -> res],
with every type variable and region in [pvl] being frozen. *)
...
...
src/mlw/mdecl.ml
View file @
852600ca
...
...
@@ -66,7 +66,7 @@ let create_semi_constructor id s fl pjl invl =
let
get_pj
p
=
match
p
.
rs_logic
with
RLls
s
->
s
|
_
->
assert
false
in
let
mk_q
{
pv_vs
=
v
}
p
=
t_equ
(
fs_app
(
get_pj
p
)
[
t
]
v
.
vs_ty
)
(
t_var
v
)
in
let
q
=
create_post
res
(
t_and_simp_l
(
List
.
map2
mk_q
fl
pjl
))
in
let
c
=
create_cty
fl
invl
[
q
]
Mexn
.
empty
eff_empty
ity
in
let
c
=
create_cty
fl
invl
[
q
]
Mexn
.
empty
Mpv
.
empty
eff_empty
ity
in
create_rsymbol
id
c
let
create_flat_record_decl
id
args
priv
mut
fldl
invl
=
...
...
Write
Preview
Supports
Markdown
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