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
1f1f8b2c
Commit
1f1f8b2c
authored
Mar 20, 2018
by
Andrei Paskevich
Browse files
Mlw: merge Ecase and Etry into a single match-with-exn constructor
parent
c49dec72
Changes
17
Hide whitespace changes
Inline
Side-by-side
plugins/python/py_main.ml
View file @
1f1f8b2c
...
...
@@ -232,7 +232,7 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
let
var
=
List
.
map
(
fun
(
t
,
o
)
->
deref
env
t
,
o
)
var
in
let
loop
=
mk_expr
~
loc
(
Ewhile
(
expr
env
e
,
inv
,
var
,
block
env
~
loc
s
))
in
if
has_breakl
s
then
mk_expr
~
loc
(
E
try
(
loop
,
false
,
break_handler
~
loc
))
if
has_breakl
s
then
mk_expr
~
loc
(
E
match
(
loop
,
[]
,
break_handler
~
loc
))
else
loop
|
Py_ast
.
Sbreak
->
mk_expr
~
loc
(
Eraise
(
break
~
loc
,
None
))
...
...
@@ -304,7 +304,7 @@ and block env ~loc = function
let
body
=
block
env'
~
loc
:
id
.
id_loc
bl
in
let
body
=
if
not
(
has_returnl
bl
)
then
body
else
let
loc
=
id
.
id_loc
in
mk_expr
~
loc
(
E
try
(
body
,
false
,
return_handler
~
loc
))
in
mk_expr
~
loc
(
E
match
(
body
,
[]
,
return_handler
~
loc
))
in
let
local
bl
id
=
let
loc
=
id
.
id_loc
in
let
ref
=
mk_ref
~
loc
(
mk_var
~
loc
id
)
in
...
...
src/mlw/compile.ml
View file @
1f1f8b2c
...
...
@@ -128,9 +128,10 @@ module ML = struct
f
rs
.
rs_name
;
iter_deps_args
f
args
;
iter_deps_expr
f
e
;
iter_deps_ty
f
res
)
rdef
;
iter_deps_expr
f
e
|
Ematch
(
e
,
branchl
)
->
|
Ematch
(
e
,
branchl
,
xl
)
->
iter_deps_expr
f
e
;
List
.
iter
(
fun
(
p
,
e
)
->
iter_deps_pat
f
p
;
iter_deps_expr
f
e
)
branchl
List
.
iter
(
fun
(
p
,
e
)
->
iter_deps_pat
f
p
;
iter_deps_expr
f
e
)
branchl
;
List
.
iter
(
iter_deps_xbranch
f
)
xl
|
Eif
(
e1
,
e2
,
e3
)
->
iter_deps_expr
f
e1
;
iter_deps_expr
f
e2
;
...
...
@@ -152,9 +153,6 @@ module ML = struct
|
Eexn
(
_xs
,
Some
ty
,
e
)
->
(* FIXME? How come we never do binding here? *)
iter_deps_ty
f
ty
;
iter_deps_expr
f
e
|
Etry
(
e
,
_
,
xl
)
->
iter_deps_expr
f
e
;
List
.
iter
(
iter_deps_xbranch
f
)
xl
|
Eassign
assingl
->
List
.
iter
(
fun
(
_
,
rs
,
_
)
->
f
rs
.
rs_name
)
assingl
|
Eignore
e
->
iter_deps_expr
f
e
...
...
@@ -233,13 +231,15 @@ module ML = struct
let
e_for
pv1
pv2
dir
pv3
e1
=
mk_expr
(
Mltree
.
Efor
(
pv1
,
pv2
,
dir
,
pv3
,
e1
))
ity_unit
let
e_match
e
bl
=
mk_expr
(
Mltree
.
Ematch
(
e
,
bl
))
let
e_match
e
bl
xl
=
mk_expr
(
Mltree
.
Ematch
(
e
,
bl
,
xl
))
(*
let e_match_exn e bl eff_bl lbl_match xl =
let ity = match bl with (_, d) :: _ -> d.e_ity | [] -> assert false in
let e = e_match e bl ity eff_bl lbl_match in
mk_expr (Mltree.Etry (e, true, xl))
*)
let
e_assign
al
ity
eff
lbl
=
if
al
=
[]
then
e_unit
else
mk_expr
(
Mltree
.
Eassign
al
)
ity
eff
lbl
...
...
@@ -555,13 +555,6 @@ module Translate = struct
ML
.
mk_hole
|
Eabsurd
->
ML
.
e_absurd
(
Mltree
.
I
e
.
e_ity
)
eff
lbl
|
Ecase
(
e1
,
bl
)
when
e_ghost
e1
->
(* if [e1] is ghost but the entire [match-with] expression doesn't,
it must be the case the first branch is irrefutable *)
(
match
bl
with
|
[]
->
assert
false
|
(
_
,
e
)
::
_
->
expr
info
svar
e
.
e_mask
e
)
|
Ecase
(
e1
,
bl
)
->
let
bl
=
List
.
map
(
ebranch
info
svar
mask
)
bl
in
ML
.
e_match
(
expr
info
svar
e1
.
e_mask
e1
)
bl
(
Mltree
.
I
e
.
e_ity
)
eff
lbl
|
Eassert
_
->
ML
.
e_unit
|
Eif
(
e1
,
e2
,
e3
)
when
e_ghost
e1
->
...
...
@@ -598,13 +591,28 @@ module Translate = struct
let
rm_ghost
(
_
,
rs
,
_
)
=
not
(
rs_ghost
rs
)
in
let
al
=
List
.
filter
rm_ghost
al
in
ML
.
e_assign
al
(
Mltree
.
I
e
.
e_ity
)
eff
lbl
|
Etry
({
e_node
=
Ecase
(
etry
,
bl
);
e_effect
;
e_label
}
,
true
,
xl
)
->
let
etry
=
expr
info
svar
etry
.
e_mask
etry
in
|
Ecase
(
e1
,
[]
,
xl
)
when
Mxs
.
is_empty
xl
->
expr
info
svar
e1
.
e_mask
e1
|
Ecase
(
e1
,
bl
,
xl
)
when
e_ghost
e1
->
assert
(
Mxs
.
is_empty
xl
);
(* Expr ensures this for the time being *)
(* if [e1] is ghost but the entire [match-with] expression isn't,
it must be the case the first non-absurd branch is irrefutable *)
(
match
bl
with
(* FIXME: skip absurd branches *)
|
[]
->
assert
false
|
(
_
,
e
)
::
_
->
expr
info
svar
e
.
e_mask
e
)
(*
| Ecase (e1, bl) ->
let e1 = expr info svar e1.e_mask e1 in
let bl = List.map (ebranch info svar mask) bl in
ML.e_match e1 bl (Mltree.I e.e_ity) eff lbl
*)
|
Ecase
(
e1
,
bl
,
xl
)
->
let
e1
=
expr
info
svar
e1
.
e_mask
e1
in
let
bl
=
List
.
map
(
ebranch
info
svar
mask
)
bl
in
(* NOTE: why no pv_list_of_mask here? *)
let
mk_xl
(
xs
,
(
pvl
,
e
))
=
xs
,
pvl
,
expr
info
svar
mask
e
in
let
xl
=
Mxs
.
bindings
xl
in
let
xl
=
List
.
map
mk_xl
xl
in
ML
.
e_match_exn
etry
bl
e_effect
e_label
xl
(
Mltree
.
I
e
.
e_ity
)
eff
lbl
let
xl
=
List
.
map
mk_xl
(
Mxs
.
bindings
xl
)
in
ML
.
e_match
e1
bl
xl
(
Mltree
.
I
e
.
e_ity
)
eff
lbl
(*
| Etry (etry, _, xl) ->
let etry = expr info svar mask etry in
let mk_xl (xs, (pvl, e)) =
...
...
@@ -613,6 +621,7 @@ module Translate = struct
let xl = Mxs.bindings xl in
let xl = List.map mk_xl xl in
ML.mk_expr (Mltree.Etry (etry, false, xl)) (Mltree.I e.e_ity) eff lbl
*)
|
Eraise
(
xs
,
ex
)
->
let
ex
=
match
expr
info
svar
xs
.
xs_mask
ex
with
|
{
Mltree
.
e_node
=
Mltree
.
Eblock
[]
}
->
None
|
e
->
Some
e
in
...
...
@@ -824,10 +833,17 @@ module Transform = struct
|
Eexn
(
xs
,
ty
,
e1
)
->
let
e1
,
s1
=
expr
info
subst
e1
in
mk
(
Eexn
(
xs
,
ty
,
e1
))
,
s1
|
Ematch
(
e
,
bl
)
->
|
Ematch
(
e
,
bl
,
xl
)
->
let
e
,
spv
=
expr
info
subst
e
in
let
e_bl
,
spv_bl
=
mk_list_eb
bl
(
branch
info
subst
)
in
mk
(
Ematch
(
e
,
e_bl
))
,
Spv
.
union
spv
spv_bl
let
e_xl
,
spv_xl
=
mk_list_eb
xl
(
xbranch
info
subst
)
in
mk
(
Ematch
(
e
,
e_bl
,
e_xl
))
,
Spv
.
union
(
Spv
.
union
spv
spv_bl
)
spv_xl
(*
| Etry (e, case, bl) ->
let e, spv = expr info subst e in
let e_bl, spv_bl = mk_list_eb bl (xbranch info subst) in
mk (Etry (e, case, e_bl)), Spv.union spv spv_bl
*)
|
Eblock
el
->
let
e_app
,
spv
=
mk_list_eb
el
(
expr
info
subst
)
in
mk
(
Eblock
e_app
)
,
spv
...
...
@@ -842,10 +858,6 @@ module Transform = struct
|
Eraise
(
exn
,
Some
e
)
->
let
e
,
spv
=
expr
info
subst
e
in
mk
(
Eraise
(
exn
,
Some
e
))
,
spv
|
Etry
(
e
,
case
,
bl
)
->
let
e
,
spv
=
expr
info
subst
e
in
let
e_bl
,
spv_bl
=
mk_list_eb
bl
(
xbranch
info
subst
)
in
mk
(
Etry
(
e
,
case
,
e_bl
))
,
Spv
.
union
spv
spv_bl
|
Eassign
_al
->
e
,
Spv
.
empty
|
Econst
_
|
Eabsurd
|
Ehole
->
e
,
Spv
.
empty
...
...
src/mlw/cprinter.ml
View file @
1f1f8b2c
...
...
@@ -836,8 +836,7 @@ module MLToC = struct
C
.
Sblock
b
))))
end
end
|
Etry
(
b
,
case
,
xl
)
->
assert
(
not
case
);
(* TODO *)
|
Ematch
(
b
,
[]
,
(
_
::_
as
xl
))
->
if
debug
then
Format
.
printf
"TRY@."
;
let
is_while
=
match
b
.
e_node
with
Ewhile
_
->
true
|
_
->
false
in
let
breaks
,
returns
=
List
.
fold_left
...
...
@@ -868,7 +867,7 @@ module MLToC = struct
|
Eraise
(
_
,
None
)
->
assert
false
(* nothing to pass to return *)
|
Eraise
_
->
raise
(
Unsupported
"non break/return exception raised"
)
|
Efor
_
->
raise
(
Unsupported
"for loops"
)
(*TODO*)
|
Ematch
(
e1
,
[
Ptuple
rets
,
e2
])
|
Ematch
(
e1
,
[
Ptuple
rets
,
e2
]
,
[]
)
when
List
.
for_all
(
function
Pvar
_
->
true
|_->
false
)
rets
...
...
src/mlw/dexpr.ml
View file @
1f1f8b2c
...
...
@@ -414,11 +414,10 @@ and dexpr_node =
|
DEand
of
dexpr
*
dexpr
|
DEor
of
dexpr
*
dexpr
|
DEif
of
dexpr
*
dexpr
*
dexpr
|
DEcase
of
dexpr
*
(
dpattern
*
dexpr
)
list
|
DEcase
of
dexpr
*
dreg_branch
list
*
dexn_branch
list
|
DEassign
of
(
dexpr
*
rsymbol
*
dexpr
)
list
|
DEwhile
of
dexpr
*
dinvariant
later
*
variant
list
later
*
dexpr
|
DEfor
of
preid
*
dexpr
*
for_direction
*
dexpr
*
dinvariant
later
*
dexpr
|
DEtry
of
dexpr
*
bool
*
(
dxsymbol
*
dpattern
*
dexpr
)
list
|
DEraise
of
dxsymbol
*
dexpr
|
DEghost
of
dexpr
|
DEexn
of
preid
*
dity
*
mask
*
dexpr
...
...
@@ -436,6 +435,10 @@ and dexpr_node =
|
DEuloc
of
dexpr
*
Loc
.
position
|
DElabel
of
dexpr
*
Slab
.
t
and
dreg_branch
=
dpattern
*
dexpr
and
dexn_branch
=
dxsymbol
*
dpattern
*
dexpr
and
dlet_defn
=
preid
*
ghost
*
rs_kind
*
dexpr
and
drec_defn
=
{
fds
:
dfun_defn
list
}
...
...
@@ -756,15 +759,19 @@ let dexpr ?loc node =
dexpr_expected_type
de2
res
;
dexpr_expected_type
de3
res
;
[]
,
res
|
DEcase
(
_
,
[]
)
->
|
DEcase
(
_
,
[]
,
[]
)
->
invalid_arg
"Dexpr.dexpr: empty branch list in DEcase"
|
DEcase
(
de
,
bl
)
->
let
ety
=
dity_fresh
()
in
|
DEcase
(
de
,
bl
,
xl
)
->
let
res
=
dity_fresh
()
in
let
ety
=
if
bl
=
[]
then
res
else
dity_fresh
()
in
dexpr_expected_type
de
ety
;
List
.
iter
(
fun
(
dp
,
de
)
->
dpat_expected_type
dp
ety
;
dexpr_expected_type
de
res
)
bl
;
List
.
iter
(
fun
(
xs
,
dp
,
de
)
->
dpat_expected_type
dp
(
specialize_dxs
xs
);
dexpr_expected_type
de
res
)
xl
;
[]
,
res
|
DEassign
al
->
List
.
iter
(
fun
(
de1
,
rs
,
de2
)
->
...
...
@@ -784,15 +791,6 @@ let dexpr ?loc node =
dexpr_expected_type
de_to
bty
;
dexpr_expected_type
de
dity_unit
;
dvty_unit
|
DEtry
(
_
,_,
[]
)
->
invalid_arg
"Dexpr.dexpr: empty branch list in DEtry"
|
DEtry
(
de
,_,
bl
)
->
let
res
=
dity_fresh
()
in
dexpr_expected_type
de
res
;
List
.
iter
(
fun
(
xs
,
dp
,
de
)
->
dpat_expected_type
dp
(
specialize_dxs
xs
);
dexpr_expected_type
de
res
)
bl
;
[]
,
res
|
DEraise
(
xs
,
de
)
->
dexpr_expected_type
de
(
specialize_dxs
xs
);
[]
,
dity_fresh
()
...
...
@@ -1313,8 +1311,8 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
let
env
,
old
=
add_label
env
id
.
pre_name
in
cexp
uloc
env
de
(
LD
(
LL
old
)
::
lpl
)
|
DEvar_pure
_
|
DEpv_pure
_
|
DEoptexn
_
|
DEsym
_
|
DEconst
_
|
DEnot
_
|
DEand
_
|
DEor
_
|
DEif
_
|
DEcase
_
|
DEassign
_
|
DEwhile
_
|
DEfor
_
|
DEtry
_
|
DEraise
_
|
DEassert
_
|
DEsym
_
|
DEconst
_
|
DEnot
_
|
DEand
_
|
DEor
_
|
DEif
_
|
DEcase
_
|
DEassign
_
|
DEwhile
_
|
DEfor
_
|
DEraise
_
|
DEassert
_
|
DEpure
_
|
DEabsurd
|
DEtrue
|
DEfalse
->
assert
false
(* expr-only *)
|
DEcast
_
|
DEuloc
_
|
DElabel
_
->
assert
false
(* already stripped *)
...
...
@@ -1357,25 +1355,6 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
e_or
(
expr
uloc
env
de1
)
(
expr
uloc
env
de2
)
|
DEif
(
de1
,
de2
,
de3
)
->
e_if
(
expr
uloc
env
de1
)
(
expr
uloc
env
de2
)
(
expr
uloc
env
de3
)
|
DEcase
(
de1
,
bl
)
->
let
e1
=
expr
uloc
env
de1
in
let
mask
=
if
env
.
ghs
then
MaskGhost
else
e1
.
e_mask
in
let
mk_branch
(
dp
,
de
)
=
let
vm
,
pat
=
create_prog_pattern
dp
.
dp_pat
e1
.
e_ity
mask
in
let
e
=
expr
uloc
(
add_pv_map
env
vm
)
de
in
Mstr
.
iter
(
fun
_
v
->
check_used_pv
e
v
)
vm
;
pat
,
e
in
let
bl
=
List
.
rev_map
mk_branch
bl
in
let
pl
=
List
.
rev_map
(
fun
(
p
,_
)
->
[
p
.
pp_pat
])
bl
in
let
v
=
create_vsymbol
(
id_fresh
"x"
)
(
ty_of_ity
e1
.
e_ity
)
in
(* TODO: this is the right place to show the missing patterns,
but we do not have access to the current known_map to do that *)
let
bl
=
if
Pattern
.
is_exhaustive
[
t_var
v
]
pl
then
bl
else
begin
if
List
.
length
bl
>
1
then
Warning
.
emit
?
loc
:
de0
.
de_loc
"Non-exhaustive pattern matching, asserting `absurd'"
;
let
_
,
pp
=
create_prog_pattern
PPwild
e1
.
e_ity
mask
in
(
pp
,
e_absurd
(
ity_of_dity
res
))
::
bl
end
in
e_case
e1
(
List
.
rev
bl
)
|
DEassign
al
->
let
conv
(
de1
,
f
,
de2
)
=
let
e1
=
expr
uloc
{
env
with
ugh
=
false
}
de1
in
...
...
@@ -1402,8 +1381,28 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let
e
=
expr
uloc
env
de
in
let
inv
=
get_later
env
dinv
in
e_for
v
e_from
dir
e_to
i
(
create_invariant
inv
)
e
|
DE
try
(
de1
,
case
,
b
l
)
->
|
DE
case
(
de1
,
bl
,
x
l
)
->
let
e1
=
expr
uloc
env
de1
in
(* regular branches *)
let
mask
=
if
env
.
ghs
then
MaskGhost
else
e1
.
e_mask
in
let
mk_branch
(
dp
,
de
)
=
let
vm
,
pat
=
create_prog_pattern
dp
.
dp_pat
e1
.
e_ity
mask
in
let
e
=
expr
uloc
(
add_pv_map
env
vm
)
de
in
Mstr
.
iter
(
fun
_
v
->
check_used_pv
e
v
)
vm
;
pat
,
e
in
let
bl
=
List
.
rev_map
mk_branch
bl
in
(* TODO: this is the right place to show the missing patterns,
but we do not have access to the current known_map to do that *)
let
exhaustive
=
bl
=
[]
||
let
v
=
create_vsymbol
(
id_fresh
"x"
)
(
ty_of_ity
e1
.
e_ity
)
in
let
pl
=
List
.
rev_map
(
fun
(
p
,_
)
->
[
p
.
pp_pat
])
bl
in
Pattern
.
is_exhaustive
[
t_var
v
]
pl
in
let
bl
=
if
exhaustive
then
bl
else
begin
if
List
.
length
bl
>
1
then
Warning
.
emit
?
loc
:
de0
.
de_loc
"Non-exhaustive pattern matching, asserting `absurd'"
;
let
_
,
pp
=
create_prog_pattern
PPwild
e1
.
e_ity
mask
in
(
pp
,
e_absurd
(
ity_of_dity
res
))
::
bl
end
in
(* exception branches *)
let
add_branch
m
(
xs
,
dp
,
de
)
=
let
xs
=
get_xs
env
xs
in
let
mask
=
if
env
.
ghs
then
MaskGhost
else
xs
.
xs_mask
in
...
...
@@ -1411,7 +1410,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let
e
=
expr
uloc
(
add_pv_map
env
vm
)
de
in
Mstr
.
iter
(
fun
_
v
->
check_used_pv
e
v
)
vm
;
Mxs
.
add
xs
((
pat
,
e
)
::
Mxs
.
find_def
[]
xs
m
)
m
in
let
xsm
=
List
.
fold_left
add_branch
Mxs
.
empty
b
l
in
let
xsm
=
List
.
fold_left
add_branch
Mxs
.
empty
x
l
in
let
is_simple
p
=
match
p
.
pat_node
with
|
Papp
(
fs
,
[]
)
->
is_fs_tuple
fs
|
Pvar
_
|
Pwild
->
true
|
_
->
false
in
...
...
@@ -1445,8 +1444,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let
bl
=
if
Pattern
.
is_exhaustive
[
t
]
pl
then
bl
else
let
_
,
pp
=
create_prog_pattern
PPwild
xs
.
xs_ity
mask
in
(
pp
,
e_raise
xs
e
(
ity_of_dity
res
))
::
bl
in
vl
,
e_case
e
(
List
.
rev
bl
)
in
e_
try
e1
~
case
(
Mxs
.
mapi
mk_branch
xsm
)
vl
,
e_case
e
(
List
.
rev
bl
)
Mxs
.
empty
in
e_
case
e1
(
List
.
rev
bl
)
(
Mxs
.
mapi
mk_branch
xsm
)
|
DEraise
(
xs
,
de
)
->
let
{
xs_mask
=
mask
}
as
xs
=
get_xs
env
xs
in
let
env
=
{
env
with
ugh
=
mask
=
MaskGhost
}
in
...
...
@@ -1474,7 +1473,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
if
not
(
Sxs
.
mem
xs
e
.
e_effect
.
eff_raises
)
then
e
else
let
vl
=
vl_of_mask
(
id_fresh
"r"
)
mask
xs
.
xs_ity
in
let
branches
=
Mxs
.
singleton
xs
(
vl
,
e_of_vl
vl
)
in
e_exn
xs
(
e_
try
e
~
case
:
false
branches
)
e_exn
xs
(
e_
case
e
[]
branches
)
|
DEmark
(
id
,
de
)
->
let
env
,
old
=
add_label
env
id
.
pre_name
in
let
put
_
(
ld
,_
)
e
=
e_let
ld
e
in
...
...
src/mlw/dexpr.mli
View file @
1f1f8b2c
...
...
@@ -112,11 +112,10 @@ and dexpr_node =
|
DEand
of
dexpr
*
dexpr
|
DEor
of
dexpr
*
dexpr
|
DEif
of
dexpr
*
dexpr
*
dexpr
|
DEcase
of
dexpr
*
(
dpattern
*
dexpr
)
list
|
DEcase
of
dexpr
*
dreg_branch
list
*
dexn_branch
list
|
DEassign
of
(
dexpr
*
rsymbol
*
dexpr
)
list
|
DEwhile
of
dexpr
*
dinvariant
later
*
variant
list
later
*
dexpr
|
DEfor
of
preid
*
dexpr
*
for_direction
*
dexpr
*
dinvariant
later
*
dexpr
|
DEtry
of
dexpr
*
bool
*
(
dxsymbol
*
dpattern
*
dexpr
)
list
|
DEraise
of
dxsymbol
*
dexpr
|
DEghost
of
dexpr
|
DEexn
of
preid
*
dity
*
mask
*
dexpr
...
...
@@ -134,6 +133,10 @@ and dexpr_node =
|
DEuloc
of
dexpr
*
Loc
.
position
|
DElabel
of
dexpr
*
Slab
.
t
and
dreg_branch
=
dpattern
*
dexpr
and
dexn_branch
=
dxsymbol
*
dpattern
*
dexpr
and
dlet_defn
=
preid
*
ghost
*
rs_kind
*
dexpr
and
drec_defn
=
private
{
fds
:
dfun_defn
list
}
...
...
src/mlw/expr.ml
View file @
1f1f8b2c
...
...
@@ -322,10 +322,9 @@ and expr_node =
|
Eassign
of
assign
list
|
Elet
of
let_defn
*
expr
|
Eif
of
expr
*
expr
*
expr
|
Ecase
of
expr
*
(
prog_pattern
*
expr
)
lis
t
|
Ecase
of
expr
*
reg_branch
list
*
exn_branch
Mxs
.
t
|
Ewhile
of
expr
*
invariant
list
*
variant
list
*
expr
|
Efor
of
pvsymbol
*
for_bounds
*
pvsymbol
*
invariant
list
*
expr
|
Etry
of
expr
*
bool
*
(
pvsymbol
list
*
expr
)
Mxs
.
t
|
Eraise
of
xsymbol
*
expr
|
Eexn
of
xsymbol
*
expr
|
Eassert
of
assertion_kind
*
term
...
...
@@ -333,6 +332,10 @@ and expr_node =
|
Epure
of
term
|
Eabsurd
and
reg_branch
=
prog_pattern
*
expr
and
exn_branch
=
pvsymbol
list
*
expr
and
cexp
=
{
c_node
:
cexp_node
;
c_cty
:
cty
;
...
...
@@ -390,8 +393,8 @@ let e_fold fn acc e = match e.e_node with
|
Elet
((
LDsym
_
|
LDrec
_
)
,
e
)
|
Eexn
(
_
,
e
)
->
fn
acc
e
|
Elet
(
LDvar
(
_
,
d
)
,
e
)
|
Ewhile
(
d
,_,_,
e
)
->
fn
(
fn
acc
d
)
e
|
Eif
(
c
,
d
,
e
)
->
fn
(
fn
(
fn
acc
c
)
d
)
e
|
Ecase
(
d
,
bl
)
->
List
.
fold
_left
(
fun
acc
(
_
,
e
)
->
fn
acc
e
)
(
fn
acc
d
)
b
l
|
Etry
(
d
,_,
xl
)
->
Mxs
.
fold
(
fun
_
(
_
,
e
)
acc
->
fn
acc
e
)
xl
(
fn
acc
d
)
|
Ecase
(
d
,
bl
,
xl
)
->
Mxs
.
fold
(
fun
_
(
_
,
e
)
acc
->
fn
acc
e
)
x
l
(
List
.
fold_left
(
fun
acc
(
_
,
e
)
->
fn
acc
e
)
(
fn
acc
d
)
bl
)
exception
FoundExpr
of
Loc
.
position
option
*
expr
...
...
@@ -561,8 +564,8 @@ let term_of_post ~prop v h =
let
rec
raw_of_expr
prop
e
=
match
e
.
e_node
with
|
_
when
ity_equal
e
.
e_ity
ity_unit
->
t_void
(* we do not check e.e_effect here, since we check the
effects later for the overall expression. The only
effect-hiding construction, E
try
, is forbidden. *)
effects later for the overall expression. The only
effect-hiding construction, E
case(_,_,xl)
, is forbidden. *)
|
Eassign
_
|
Ewhile
_
|
Efor
_
|
Eassert
_
->
assert
false
|
Evar
v
->
t_var
v
.
pv_vs
|
Econst
c
->
t_const
c
(
ty_of_ity
e
.
e_ity
)
...
...
@@ -593,10 +596,11 @@ let rec raw_of_expr prop e = match e.e_node with
t_or
(
pure_of_expr
true
e0
)
(
pure_of_expr
true
e2
)
|
Eif
(
e0
,
e1
,
e2
)
->
t_if
(
pure_of_expr
true
e0
)
(
pure_of_expr
prop
e1
)
(
pure_of_expr
prop
e2
)
|
Ecase
(
d
,
bl
)
->
|
Ecase
(
d
,
bl
,
xl
)
when
Mxs
.
is_empty
xl
->
if
bl
=
[]
then
pure_of_expr
prop
d
else
let
conv
(
p
,
e
)
=
t_close_branch
p
.
pp_pat
(
pure_of_expr
prop
e
)
in
t_case
(
pure_of_expr
false
d
)
(
List
.
map
conv
bl
)
|
E
try
_
|
Eraise
_
|
Eabsurd
->
raise
Exit
|
E
case
_
|
Eraise
_
|
Eabsurd
->
raise
Exit
and
pure_of_expr
prop
e
=
match
copy_labels
e
(
raw_of_expr
prop
e
)
with
|
{
t_ty
=
Some
_
}
as
t
when
prop
->
fmla_of_term
t
...
...
@@ -649,10 +653,11 @@ let rec post_of_expr res e = match e.e_node with
post_of_term
res
(
pure_of_expr
true
e
)
|
Eif
(
e0
,
e1
,
e2
)
->
t_if
(
pure_of_expr
true
e0
)
(
post_of_expr
res
e1
)
(
post_of_expr
res
e2
)
|
Ecase
(
d
,
bl
)
->
|
Ecase
(
d
,
bl
,
xl
)
when
Mxs
.
is_empty
xl
->
if
bl
=
[]
then
post_of_expr
res
d
else
let
conv
(
p
,
e
)
=
t_close_branch
p
.
pp_pat
(
post_of_expr
res
e
)
in
t_case
(
pure_of_expr
false
d
)
(
List
.
map
conv
bl
)
|
E
try
_
|
Eraise
_
->
raise
Exit
|
E
case
_
|
Eraise
_
->
raise
Exit
|
Eabsurd
->
copy_labels
e
t_false
let
local_post_of_expr
e
=
...
...
@@ -930,16 +935,26 @@ let e_while d inv vl e =
(* match-with, try-with, raise *)
let
e_case
e
bl
=
let
e_case
e
bl
xl
=
(* return type *)
let
ity
=
match
bl
with
|
(
_
,
d
)
::_
->
d
.
e_ity
|
[]
->
invalid_arg
"Expr.e_case"
in
List
.
iter
(
fun
(
p
,
d
)
->
if
not
(
ity_equal
e
.
e_ity
ity_unit
)
&&
mask_spill
e
.
e_mask
p
.
pp_mask
then
|
[]
->
e
.
e_ity
in
(* check types and masks *)
let
check
rity
rmask
pity
pmask
d
=
ity_equal_check
rity
pity
;
if
not
(
ity_equal
rity
ity_unit
)
&&
mask_spill
rmask
pmask
then
Loc
.
errorm
"Non-ghost pattern in a ghost position"
;
ity_equal_check
d
.
e_ity
ity
;
ity_equal_check
e
.
e_ity
p
.
pp_ity
)
bl
;
ity_equal_check
d
.
e_ity
ity
in
List
.
iter
(
fun
(
p
,
d
)
->
check
e
.
e_ity
e
.
e_mask
p
.
pp_ity
p
.
pp_mask
d
)
bl
;
Mxs
.
iter
(
fun
xs
(
vl
,
d
)
->
let
vl_ity
,
vl_mask
=
match
vl
with
|
[]
->
ity_unit
,
MaskVisible
|
[
v
]
->
v
.
pv_ity
,
mask_of_pv
v
|
vl
->
ity_tuple
(
List
.
map
(
fun
v
->
v
.
pv_ity
)
vl
)
,
MaskTuple
(
List
.
map
mask_of_pv
vl
)
in
check
xs
.
xs_ity
xs
.
xs_mask
vl_ity
vl_mask
d
)
xl
;
(* absurd branches can be eliminated, any pattern with
a refutable ghost subpattern makes the whole match
ghost, unless it is the last branch, in which case
...
...
@@ -950,49 +965,29 @@ let e_case e bl =
|
({
pp_fail
=
PGlast
}
,_
)
::
bl
->
last
||
scan
true
bl
|
({
pp_fail
=
PGfail
}
,_
)
::_
->
true
|
[]
->
false
in
let
ghost
=
scan
false
bl
and
dl
=
List
.
map
snd
bl
in
let
add_mask
mask
d
=
mask_union
mask
d
.
e_mask
in
let
mask
=
List
.
fold_left
add_mask
MaskVisible
dl
in
let
eff
=
List
.
fold_left
(
fun
eff
(
p
,
d
)
->
let
ghost
=
scan
false
bl
||
(
e
.
e_effect
.
eff_ghost
&&
not
(
Mxs
.
is_empty
xl
))
in
(* return mask *)
let
mask
=
if
bl
=
[]
then
e
.
e_mask
else
MaskVisible
in
let
mask
=
List
.
fold_left
(
fun
mask
(
_
,
d
)
->
mask_union
mask
d
.
e_mask
)
mask
bl
in
let
mask
=
Mxs
.
fold
(
fun
_
(
_
,
d
)
mask
->
mask_union
mask
d
.
e_mask
)
xl
mask
in
(* branch effect *)
let
xeff
=
eff_empty
,
[]
in
let
xeff
=
List
.
fold_left
(
fun
(
eff
,
dl
)
(
p
,
d
)
->
let
pvs
=
pvs_of_vss
Spv
.
empty
p
.
pp_pat
.
pat_vars
in
let
deff
=
eff_bind
pvs
d
.
e_effect
in
try_effect
dl
eff_union_par
eff
deff
)
eff_empty
bl
in
let
eff
=
try_effect
(
e
::
dl
)
eff_union_seq
e
.
e_effect
eff
in
let
eff
=
try_effect
(
e
::
dl
)
eff_ghostify
ghost
eff
in
mk_expr
(
Ecase
(
e
,
bl
))
ity
mask
eff
let
e_try
e
~
case
xl
=
let
get_mask
=
function
|
[]
->
ity_unit
,
MaskVisible
|
[
v
]
->
v
.
pv_ity
,
mask_of_pv
v
|
vl
->
ity_tuple
(
List
.
map
(
fun
v
->
v
.
pv_ity
)
vl
)
,
MaskTuple
(
List
.
map
mask_of_pv
vl
)
in
Mxs
.
iter
(
fun
xs
(
vl
,
d
)
->
let
ity
,
mask
=
get_mask
vl
in
if
mask_spill
xs
.
xs_mask
mask
then
Loc
.
errorm
"Non-ghost pattern in a ghost position"
;
ity_equal_check
ity
xs
.
xs_ity
;
ity_equal_check
d
.
e_ity
e
.
e_ity
)
xl
;
let
ghost
=
e
.
e_effect
.
eff_ghost
in
let
e0
,
bl
=
if
not
case
then
e
,
[]
else
match
e
.
e_node
with
Ecase
(
e
,
bl
)
->
e
,
bl
|
_
->
invalid_arg
"Expr.e_try"
in
let
eeff
=
Mxs
.
fold
(
fun
xs
_
eff
->
eff_catch
eff
xs
)
xl
e0
.
e_effect
in
let
dl
=
Mxs
.
fold
(
fun
_
(
_
,
d
)
l
->
d
::
l
)
xl
[]
in
let
add_mask
mask
d
=
mask_union
mask
d
.
e_mask
in
let
mask
=
List
.
fold_left
add_mask
e
.
e_mask
dl
in
let
bldl
=
List
.
map
snd
bl
@
dl
in
let
xeff
=
List
.
fold_left
(
fun
eff
(
p
,
d
)
->
let
pvs
=
pvs_of_vss
Spv
.
empty
p
.
pp_pat
.
pat_vars
in
eff_union_par
eff
(
eff_bind
pvs
d
.
e_effect
))
eff_empty
bl
in
let
xeff
=
Mxs
.
fold
(
fun
_
(
vl
,
d
)
eff
->
try_effect
(
d
::
dl
)
eff_union_par
eff
deff
,
d
::
dl
)
xeff
bl
in
let
eff
,
dl
=
Mxs
.
fold
(
fun
_
(
vl
,
d
)
(
eff
,
dl
)
->
let
add
s
v
=
Spv
.
add_new
(
Invalid_argument
"Expr.e_try"
)
v
s
in
let
deff
=
eff_bind
(
List
.
fold_left
add
Spv
.
empty
vl
)
d
.
e_effect
in
try_effect
bldl
eff_union_par
eff
deff
)
xl
xeff
in
let
eff
=
try_effect
(
e0
::
bldl
)
eff_union_seq
eeff
xeff
in
let
eff
=
try_effect
(
e0
::
bldl
)
eff_ghostify
ghost
eff
in
mk_expr
(
Etry
(
e
,
case
,
xl
))
e
.
e_ity
mask
eff
try_effect
(
d
::
dl
)
eff_union_par
eff
deff
,
d
::
dl
)
xl
xeff
in
(* total effect *)
let
eeff
=
Mxs
.
fold
(
fun
xs
_
eff
->
eff_catch
eff
xs
)
xl
e
.
e_effect
in
let
eff
=
try_effect
(
e
::
dl
)
eff_union_seq
eeff
eff
in
let
eff
=
try_effect
(
e
::
dl
)
eff_ghostify
ghost
eff
in
mk_expr
(
Ecase
(
e
,
bl
,
xl
))
ity
mask
eff
let
e_raise
xs
e
ity
=
ity_equal_check
e
.
e_ity
xs
.
xs_ity
;
...
...
@@ -1061,10 +1056,9 @@ let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
|
Efor
(
v
,
b
,
i
,
inv
,
e
)
->
e_for_raw
v
b
i
inv
(
e_rs_subst
sm
e
)
|
Ewhile
(
d
,
inv
,
vl
,
e
)
->
e_while
(
e_rs_subst
sm
d
)
inv
vl
(
e_rs_subst
sm
e
)
|
Eraise
(
xs
,
d
)
->
e_raise
xs
(
e_rs_subst
sm
d
)
e
.
e_ity
|
Ecase
(
d
,
bl
)
->
e_case
(
e_rs_subst
sm
d
)
|
Ecase
(
d
,
bl
,
xl
)
->
e_case
(
e_rs_subst
sm
d
)
(
List
.
map
(
fun
(
pp
,
e
)
->
pp
,
e_rs_subst
sm
e
)
bl
)
|
Etry
(
d
,
case
,
xl
)
->
e_try
(
e_rs_subst
sm
d
)
~
case
(
Mxs
.
map
(
fun
(
v
,
e
)
->
v
,
e_rs_subst
sm
e
)
xl
))
(
Mxs
.
map
(
fun
(
vl
,
e
)
->
vl
,
e_rs_subst
sm
e
)
xl
))
and
c_rs_subst
sm
({
c_node
=
n
;
c_cty
=
c
}
as
d
)
=
match
n
with
|
Cany
|
Cpur
_
->
d
...
...
@@ -1393,10 +1387,17 @@ and print_enode pri fmt e = match e.e_node with
fprintf
fmt
(
protect_on
(
pri
>
0
)
"%a <- %a"
)
(
Pp
.
print_list
Pp
.
comma
print_left
)
al
(
Pp
.
print_list
Pp
.
comma
print_right
)
al
|
Ecase
(
e0
,
bl
)
->
|
Ecase
(
e
,
[]
,
xl
)
->
fprintf
fmt
"try %a with@
\n
@[<hov>%a@]@
\n
end"
print_expr
e
(
Pp
.
print_list
Pp
.
newline
(
print_xbranch
false
))
(
Mxs
.
bindings
xl
)
|
Ecase
(
e0
,
bl
,
xl
)
when
Mxs
.
is_empty
xl
->
(* Elet and Ecase are ghost-containers *)
fprintf
fmt
"match %a with@
\n
@[<hov>%a@]@
\n
end"
print_expr
e0
(
Pp
.
print_list
Pp
.
newline
print_branch
)
bl
|
Ecase
(
e
,
bl
,
xl
)
->
fprintf
fmt
"match %a with@
\n
@[<hov>%a@
\n
%a@]@
\n
end"
print_expr
e
(
Pp
.
print_list
Pp
.
newline
print_branch
)
bl
(
Pp
.
print_list
Pp
.
newline
(
print_xbranch
true
))
(
Mxs
.
bindings
xl
)
|
Ewhile
(
d
,
inv
,
varl
,
e
)
->
fprintf
fmt
"@[<hov 2>while %a do%a%a@
\n
%a@]@
\n
done"
print_expr
d
print_invariant
inv
print_variant
varl
print_expr
e
...
...
@@ -1415,15 +1416,6 @@ and print_enode pri fmt e = match e.e_node with
fprintf
fmt
"raise %a"
print_xs
xs
|
Eraise
(
xs
,
e
)
->
fprintf
fmt
"raise (%a %a)"
print_xs
xs
print_expr
e
|
Etry
({
e_node
=
Ecase
(
e
,
bl
)}
,
true
,
xl
)
->
let
xl
=
Mxs
.
bindings
xl
in
fprintf
fmt
"match %a with@
\n
@[<hov>%a@
\n
%a@]@
\n
end"
print_expr
e
(
Pp
.
print_list
Pp
.
newline
print_branch
)
bl
(
Pp
.
print_list
Pp
.
newline
(
print_xbranch
true
))
xl
|
Etry
(
e
,_,
xl
)
->
let
xl
=
Mxs
.
bindings
xl
in
fprintf
fmt
"try %a with@
\n
@[<hov>%a@]@
\n
end"
print_expr
e
(
Pp
.
print_list
Pp
.
newline
(
print_xbranch
false
))
xl
|
Eabsurd
->
fprintf
fmt
"absurd"
|
Eassert
(
Assert
,
f
)
->
...
...
src/mlw/expr.mli
View file @
1f1f8b2c
...
...
@@ -129,10 +129,9 @@ and expr_node =
|
Eassign
of
assign
list
|
Elet
of
let_defn
*
expr
|
Eif
of
expr
*
expr
*
expr
|
Ecase
of
expr
*
(
prog_pattern
*
expr
)
lis
t
|
Ecase
of
expr
*
reg_branch
list
*
exn_branch
Mxs
.
t
|
Ewhile
of
expr
*
invariant
list
*
variant
list
*
expr
|
Efor
of
pvsymbol
*
for_bounds
*
pvsymbol
*
invariant
list
*
expr
|
Etry
of
expr
*
bool
*
(
pvsymbol
list
*
expr
)
Mxs
.
t
|
Eraise
of
xsymbol
*
expr
|
Eexn
of
xsymbol
*
expr
|
Eassert
of
assertion_kind
*
term
...
...
@@ -140,6 +139,10 @@ and expr_node =
|
Epure
of
term
|
Eabsurd
and
reg_branch
=
prog_pattern
*
expr