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
36813adc
Commit
36813adc
authored
Mar 24, 2013
by
Andrei Paskevich
Browse files
minor
parent
57af1c42
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/util/loc.ml
View file @
36813adc
...
...
@@ -89,6 +89,20 @@ let try4 loc f x y z t =
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
y
z
t
else
try
f
x
y
z
t
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
let
try5
loc
f
x
y
z
t
u
=
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
y
z
t
u
else
try
f
x
y
z
t
u
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
let
try6
loc
f
x
y
z
t
u
v
=
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
y
z
t
u
v
else
try
f
x
y
z
t
u
v
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
let
try7
loc
f
x
y
z
t
u
v
w
=
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
y
z
t
u
v
w
else
try
f
x
y
z
t
u
v
w
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
let
error
?
loc
e
=
match
loc
with
|
None
->
raise
e
|
Some
loc
->
raise
(
Located
(
loc
,
e
))
...
...
src/util/loc.mli
View file @
36813adc
...
...
@@ -44,10 +44,23 @@ val report_position : formatter -> position -> unit
exception
Located
of
position
*
exn
val
try1
:
position
->
(
'
a
->
'
b
)
->
'
a
->
'
b
val
try2
:
position
->
(
'
a
->
'
b
->
'
c
)
->
'
a
->
'
b
->
'
c
val
try3
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
)
->
'
a
->
'
b
->
'
c
->
'
d
val
try4
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
)
->
'
a
->
'
b
->
'
c
->
'
d
->
'
e
val
try1
:
position
->
(
'
a
->
'
b
)
->
(
'
a
->
'
b
)
val
try2
:
position
->
(
'
a
->
'
b
->
'
c
)
->
(
'
a
->
'
b
->
'
c
)
val
try3
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
)
->
(
'
a
->
'
b
->
'
c
->
'
d
)
val
try4
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
)
val
try5
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
)
val
try6
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
)
val
try7
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
->
'
h
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
->
'
h
)
val
error
:
?
loc
:
position
->
exn
->
'
a
...
...
src/whyml/mlw_expr.ml
View file @
36813adc
...
...
@@ -441,6 +441,34 @@ let l_pvset pvs lam =
let
pvs
=
spec_pvset
pvs
lam
.
l_spec
in
List
.
fold_right
Spv
.
remove
lam
.
l_args
pvs
(* fold *)
let
e_fold
fn
acc
e
=
match
e
.
e_node
with
|
Elet
(
ld
,
e
)
->
fn
(
fn
acc
ld
.
let_expr
)
e
|
Erec
(
fdl
,
e
)
->
let
fn_fd
acc
fd
=
fn
acc
fd
.
fun_lambda
.
l_expr
in
fn
(
List
.
fold_left
fn_fd
acc
fdl
)
e
|
Ecase
(
e
,
bl
)
->
let
fnbr
acc
(
_
,
e
)
=
fn
acc
e
in
List
.
fold_left
fnbr
(
fn
acc
e
)
bl
|
Etry
(
e
,
bl
)
->
let
fn_br
acc
(
_
,_,
e
)
=
fn
acc
e
in
List
.
fold_left
fn_br
(
fn
acc
e
)
bl
|
Eif
(
e1
,
e2
,
e3
)
->
fn
(
fn
(
fn
acc
e1
)
e2
)
e3
|
Eapp
(
e
,_,_
)
|
Eassign
(
_
,
e
,_,_
)
|
Eghost
e
|
Eloop
(
_
,_,
e
)
|
Efor
(
_
,_,_,
e
)
|
Eraise
(
_
,
e
)
|
Eabstr
(
e
,_
)
->
fn
acc
e
|
Elogic
_
|
Evalue
_
|
Earrow
_
|
Eany
_
|
Eassert
_
|
Eabsurd
->
acc
exception
Found
of
expr
let
e_find
pr
e
=
let
rec
find
()
e
=
e_fold
find
()
e
;
if
pr
e
then
raise
(
Found
e
)
in
try
find
()
e
;
raise
Not_found
with
Found
e
->
e
(* check admissibility of consecutive events *)
exception
StaleRegion
of
expr
*
ident
...
...
@@ -1010,25 +1038,7 @@ let create_fun_defn id lam =
if
lam
.
l_spec
.
c_letrec
<>
0
then
invalid_arg
"Mlw_expr.create_fun_defn"
;
create_fun_defn
id
lam
Sid
.
empty
(* fold *)
let
e_fold
fn
acc
e
=
match
e
.
e_node
with
|
Elet
(
ld
,
e
)
->
fn
(
fn
acc
ld
.
let_expr
)
e
|
Erec
(
fdl
,
e
)
->
let
fn_fd
acc
fd
=
fn
acc
fd
.
fun_lambda
.
l_expr
in
fn
(
List
.
fold_left
fn_fd
acc
fdl
)
e
|
Ecase
(
e
,
bl
)
->
let
fnbr
acc
(
_
,
e
)
=
fn
acc
e
in
List
.
fold_left
fnbr
(
fn
acc
e
)
bl
|
Etry
(
e
,
bl
)
->
let
fn_br
acc
(
_
,_,
e
)
=
fn
acc
e
in
List
.
fold_left
fn_br
(
fn
acc
e
)
bl
|
Eif
(
e1
,
e2
,
e3
)
->
fn
(
fn
(
fn
acc
e1
)
e2
)
e3
|
Eapp
(
e
,_,_
)
|
Eassign
(
_
,
e
,_,_
)
|
Eghost
e
|
Eloop
(
_
,_,
e
)
|
Efor
(
_
,_,_,
e
)
|
Eraise
(
_
,
e
)
|
Eabstr
(
e
,_
)
->
fn
acc
e
|
Elogic
_
|
Evalue
_
|
Earrow
_
|
Eany
_
|
Eassert
_
|
Eabsurd
->
acc
(* expr to term *)
let
spec_purify
sp
=
let
vs
,
f
=
Mlw_ty
.
open_post
sp
.
c_post
in
...
...
src/whyml/mlw_expr.mli
View file @
36813adc
...
...
@@ -260,4 +260,6 @@ val e_absurd : ity -> expr
val
e_fold
:
(
'
a
->
expr
->
'
a
)
->
'
a
->
expr
->
'
a
val
e_find
:
(
expr
->
bool
)
->
expr
->
expr
val
e_purify
:
expr
->
term
option
src/whyml/mlw_typing.ml
View file @
36813adc
...
...
@@ -1165,8 +1165,6 @@ let eff_of_deff lenv dsp =
let
add_raise
xs
_
eff
=
eff_raise
eff
xs
in
Mexn
.
fold
add_raise
dsp
.
ds_xpost
eff
,
svs
exception
Found
of
Loc
.
position
option
let
check_user_effect
lenv
e
eeff
otv
dsp
=
let
has_read
reg
eff
=
Sreg
.
mem
reg
eff
.
eff_reads
||
Sreg
.
mem
reg
eff
.
eff_ghostr
in
...
...
@@ -1192,40 +1190,35 @@ let check_user_effect lenv e eeff otv dsp =
let
ueff_rw
=
not
(
eff_is_empty
ueff
)
in
let
add_raise
xs
_
ueff
=
if
has_raise
xs
eeff
then
eff_raise
ueff
xs
else
Loc
.
errorm
else
Loc
.
errorm
?
loc
:
e
.
e_loc
"this expression does not raise exception %a"
print_xs
xs
in
let
ueff
=
Mexn
.
fold
add_raise
dsp
.
ds_xpost
ueff
in
(* check that every computed effect is listed *)
let
read
reg
=
let
rec
find_read
()
e
=
e_fold
find_read
()
e
;
if
has_read
reg
e
.
e_effect
then
raise
(
Found
e
.
e_loc
)
in
if
not
(
has_read
reg
ueff
)
then
Loc
.
errorm
?
loc
:
(
try
find_read
()
e
;
None
with
Found
loc
->
loc
)
"this expression produces an unlisted read effect"
in
let
read
reg
=
if
not
(
has_read
reg
ueff
)
then
let
loc
=
(
e_find
(
fun
e
->
e
.
e_loc
<>
None
&&
has_read
reg
e
.
e_effect
)
e
)
.
e_loc
in
Loc
.
errorm
?
loc
"this expression produces an unlisted read effect"
in
if
ueff_ro
then
Sreg
.
iter
read
eeff
.
eff_reads
;
if
ueff_ro
then
Sreg
.
iter
read
eeff
.
eff_ghostr
;
let
write
reg
=
let
rec
find_write
()
e
=
e_fold
find_write
()
e
;
if
has_write
reg
e
.
e_effect
then
raise
(
Found
e
.
e_loc
)
in
if
not
(
has_write
reg
ueff
)
then
Loc
.
errorm
?
loc
:
(
try
find_write
()
e
;
None
with
Found
loc
->
loc
)
"this expression produces an unlisted write effect"
in
let
write
reg
=
if
not
(
has_write
reg
ueff
)
then
let
loc
=
(
e_find
(
fun
e
->
e
.
e_loc
<>
None
&&
has_write
reg
e
.
e_effect
)
e
)
.
e_loc
in
Loc
.
errorm
?
loc
"this expression produces an unlisted write effect"
in
if
ueff_rw
then
Sreg
.
iter
write
eeff
.
eff_writes
;
if
ueff_rw
then
Sreg
.
iter
write
eeff
.
eff_ghostw
;
let
raize
xs
=
let
rec
find_raise
()
e
=
e_fold
find_raise
()
e
;
if
has_raise
xs
e
.
e_effect
then
raise
(
Found
e
.
e_loc
)
in
if
not
(
has_raise
xs
ueff
)
then
Loc
.
errorm
?
loc
:
(
try
find_raise
()
e
;
None
with
Found
loc
->
loc
)
"this expression raises unlisted exception %a"
print_xs
xs
in
let
raize
xs
=
if
not
(
has_raise
xs
ueff
)
then
let
loc
=
(
e_find
(
fun
e
->
e
.
e_loc
<>
None
&&
has_raise
xs
e
.
e_effect
)
e
)
.
e_loc
in
Loc
.
errorm
?
loc
"this expression raises unlisted exception %a"
print_xs
xs
in
Sexn
.
iter
raize
eeff
.
eff_raises
;
Sexn
.
iter
raize
eeff
.
eff_ghostx
;
(* check that we don't look inside opaque type variables *)
let
bad_comp
tv
_
_
=
let
rec
find_compar
()
e
=
e_f
old
find_compar
()
e
;
if
Stv
.
mem
tv
e
.
e_effect
.
eff_compar
then
raise
(
Found
e
.
e_loc
)
in
Loc
.
errorm
?
loc
:
(
try
find_compar
()
e
;
None
with
Found
loc
->
loc
)
"type parameter %a is not opaque in this expression"
Pretty
.
print_tv
tv
in
let
loc
=
(
e_f
ind
(
fun
e
->
e
.
e_loc
<>
None
&&
Stv
.
mem
tv
e
.
e_effect
.
eff_compar
)
e
)
.
e_loc
in
Loc
.
errorm
?
loc
"type parameter %a is not opaque in this expression"
Pretty
.
print_tv
tv
in
ignore
(
Mtv
.
inter
bad_comp
otv
eeff
.
eff_compar
)
let
spec_of_dspec
lenv
eff
vty
dsp
=
{
...
...
@@ -1545,7 +1538,7 @@ and check_effects lenv fd bl (de, dsp) =
let
otv
=
opaque_binders
Stv
.
empty
bl
in
let
lenv
=
add_binders
lenv
lam
.
l_args
in
let
eff
=
fd
.
fun_ps
.
ps_aty
.
aty_spec
.
c_effect
in
Loc
.
try
3
de
.
de_loc
check_user_effect
lenv
lam
.
l_expr
eff
otv
dsp
Loc
.
try
5
de
.
de_loc
check_user_effect
lenv
lam
.
l_expr
eff
otv
dsp
(** Type declaration *)
...
...
@@ -2095,7 +2088,7 @@ let use_clone_pure lib mth uc loc (use,inst) =
let
use_clone_pure
lib
mth
uc
loc
use
=
if
Debug
.
test_flag
Typing
.
debug_parse_only
then
uc
else
Loc
.
try
3
loc
(
use_clone_pure
lib
mth
)
uc
loc
use
Loc
.
try
5
loc
use_clone_pure
lib
mth
uc
loc
use
let
use_clone
lib
mmd
mth
uc
loc
(
use
,
inst
)
=
let
path
,
s
=
Typing
.
split_qualid
use
.
use_theory
in
...
...
@@ -2121,7 +2114,7 @@ let use_clone lib mmd mth uc loc (use,inst) =
let
use_clone
lib
mmd
mth
uc
loc
use
=
if
Debug
.
test_flag
Typing
.
debug_parse_only
then
uc
else
Loc
.
try
3
loc
(
use_clone
lib
mmd
mth
)
uc
loc
use
Loc
.
try
6
loc
use_clone
lib
mmd
mth
uc
loc
use
let
close_theory
(
mmd
,
mth
)
uc
=
if
Debug
.
test_flag
Typing
.
debug_parse_only
then
(
mmd
,
mth
)
else
...
...
@@ -2177,7 +2170,7 @@ let open_file, close_file =
open_module
=
open_module
;
close_module
=
close_module
;
open_namespace
=
open_namespace
;
close_namespace
=
(
fun
loc
->
Loc
.
try1
loc
close_namespace
);
close_namespace
=
(
fun
loc
imp
->
Loc
.
try1
loc
close_namespace
imp
);
new_decl
=
new_decl
;
new_pdecl
=
new_pdecl
;
use_clone
=
use_clone
;
}
...
...
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