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
4ff04130
Commit
4ff04130
authored
Sep 28, 2013
by
Andrei Paskevich
Browse files
Loc.try[1-7] functions now take location as an optional parameter
parent
6e5d6e58
Changes
11
Hide whitespace changes
Inline
Side-by-side
CHANGES
View file @
4ff04130
...
...
@@ -4,6 +4,7 @@
backward compatible
* [emacs] why.el renamed to why3.el
o [GTK sourceview] why.lang renamed to why3.lang
* Loc.try[1-7] functions now take location as an optional parameter
version 0.81, March 25, 2013
============================
...
...
plugins/tptp/tptp_typing.ml
View file @
4ff04130
...
...
@@ -118,7 +118,7 @@ let defined_ty ~loc denv env impl dw tyl =
|
DT
DTdummy
->
error
~
loc
InvalidDummy
|
DT
(
DTtype
|
DTprop
)
|
DF
_
|
DP
_
->
error
~
loc
TypeExpected
in
Loc
.
try2
loc
ty_app
ts
tyl
Loc
.
try2
~
loc
ty_app
ts
tyl
let
defined_arith
~
loc
denv
env
impl
dw
tl
=
let
ts
=
match
tl
with
...
...
@@ -185,7 +185,7 @@ let defined_arith ~loc denv env impl dw tl =
|
DP
DPisrat
->
ns_find_ls
th
.
th_export
[
"is_rat"
]
|
DP
(
DPtrue
|
DPfalse
|
DPdistinct
)
|
DT
_
->
assert
false
in
Loc
.
try2
loc
t_app_infer
ls
tl
Loc
.
try2
~
loc
t_app_infer
ls
tl
let
defined_expr
~
loc
is_fmla
denv
env
impl
dw
tl
=
match
dw
,
tl
with
|
(
DT
DTdummy
)
,
_
->
error
~
loc
InvalidDummy
...
...
@@ -201,7 +201,7 @@ let defined_expr ~loc is_fmla denv env impl dw tl = match dw, tl with
dist
(
List
.
fold_left
add
acc
tl
)
tl
|
_
->
acc
in
Loc
.
try2
loc
dist
t_true
tl
Loc
.
try2
~
loc
dist
t_true
tl
|
_
->
defined_arith
~
loc
denv
env
impl
dw
tl
(** TPTP environment *)
...
...
@@ -270,13 +270,13 @@ let find_dobj ~loc denv env impl s =
|
_
->
assert
false
(* impossible *)
let
ty_check
loc
s
ty1
t
=
Loc
.
try3
loc
ty_match
s
ty1
(
Opt
.
get
t
.
t_ty
)
Loc
.
try3
~
loc
ty_match
s
ty1
(
Opt
.
get
t
.
t_ty
)
let
rec
ty
denv
env
impl
{
e_loc
=
loc
;
e_node
=
n
}
=
match
n
with
|
Eapp
(
aw
,
al
)
->
let
ts
=
find_ts
~
loc
env
impl
aw
al
in
let
tyl
=
List
.
map
(
ty
denv
env
impl
)
al
in
Loc
.
try2
loc
ty_app
ts
tyl
Loc
.
try2
~
loc
ty_app
ts
tyl
|
Edef
(
dw
,
al
)
->
let
tyl
=
List
.
map
(
ty
denv
env
impl
)
al
in
defined_ty
~
loc
denv
env
impl
dw
tyl
...
...
src/core/decl.ml
View file @
4ff04130
...
...
@@ -673,8 +673,7 @@ let check_match kn d =
|
Tcase
(
t1
,
bl
)
->
let
find
ts
=
List
.
map
fst
(
find_constructors
kn
ts
)
in
let
bl
=
List
.
map
(
fun
b
->
let
p
,
t
=
t_open_branch
b
in
[
p
]
,
t
)
bl
in
let
try3
f
=
match
t
.
t_loc
with
Some
l
->
Loc
.
try3
l
f
|
None
->
f
in
ignore
(
try3
Pattern
.
CompileTerm
.
compile
find
[
t1
]
bl
);
ignore
(
Loc
.
try3
?
loc
:
t
.
t_loc
Pattern
.
CompileTerm
.
compile
find
[
t1
]
bl
);
t_fold
check
()
t
|
_
->
t_fold
check
()
t
in
...
...
src/driver/driver.ml
View file @
4ff04130
...
...
@@ -154,7 +154,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
|
PTyapp
((
loc
,_
)
as
q
,
tyl
)
->
let
ts
=
find_ts
th
q
in
let
tyl
=
List
.
map
ty_of_pty
tyl
in
Loc
.
try2
loc
Ty
.
ty_app
ts
tyl
Loc
.
try2
~
loc
Ty
.
ty_app
ts
tyl
|
PTuple
tyl
->
let
ts
=
Ty
.
ts_tuple
(
List
.
length
tyl
)
in
Ty
.
ty_app
ts
(
List
.
map
ty_of_pty
tyl
)
...
...
src/parser/typing.ml
View file @
4ff04130
...
...
@@ -198,7 +198,7 @@ let rec dty uc = function
|
PPTtyapp
(
x
,
p
)
->
let
ts
=
find_tysymbol
x
uc
in
let
tyl
=
List
.
map
(
dty
uc
)
p
in
Loc
.
try2
(
qloc
x
)
tyapp
ts
tyl
Loc
.
try2
~
loc
:
(
qloc
x
)
tyapp
ts
tyl
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
tyapp
ts
(
List
.
map
(
dty
uc
)
tyl
)
...
...
@@ -209,7 +209,7 @@ let rec ty_of_pty uc = function
|
PPTtyapp
(
x
,
p
)
->
let
ts
=
find_tysymbol
x
uc
in
let
tyl
=
List
.
map
(
ty_of_pty
uc
)
p
in
Loc
.
try2
(
qloc
x
)
ty_app
ts
tyl
Loc
.
try2
~
loc
:
(
qloc
x
)
ty_app
ts
tyl
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
ty_app
ts
(
List
.
map
(
ty_of_pty
uc
)
tyl
)
...
...
@@ -261,8 +261,8 @@ let binop = function
let
check_pat_linearity
p
=
let
s
=
ref
Sstr
.
empty
in
let
add
id
=
s
:=
Loc
.
try3
id
.
id_
loc
Sstr
.
add_new
(
DuplicateVar
id
.
id
)
id
.
id
!
s
let
add
{
id
=
id
;
id_loc
=
loc
}
=
s
:=
Loc
.
try3
~
loc
Sstr
.
add_new
(
DuplicateVar
id
)
id
!
s
in
let
rec
check
p
=
match
p
.
pat_desc
with
|
PPpwild
->
()
...
...
@@ -293,7 +293,7 @@ and dpat_node loc uc env = function
|
PPprec
fl
->
let
renv
=
ref
env
in
let
fl
=
List
.
map
(
fun
(
q
,
e
)
->
find_lsymbol
q
uc
,
e
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
parse_record
(
get_known
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
parse_record
(
get_known
uc
)
fl
in
let
tyl
,
ty
=
Denv
.
specialize_lsymbol
~
loc
cs
in
let
get_val
pj
ty
=
match
Mls
.
find_opt
pj
flm
with
|
Some
e
->
...
...
@@ -351,7 +351,7 @@ let param_tys uc pl =
let
ty_of_param
(
loc
,
id
,
gh
,
ty
)
=
if
gh
then
Loc
.
errorm
~
loc
"ghost parameters are not allowed here"
;
Opt
.
iter
(
fun
{
id
=
id
;
id_loc
=
loc
}
->
s
:=
Loc
.
try3
loc
Sstr
.
add_new
(
DuplicateVar
id
)
id
!
s
)
id
;
s
:=
Loc
.
try3
~
loc
Sstr
.
add_new
(
DuplicateVar
id
)
id
!
s
)
id
;
ty_of_dty
(
dty
uc
ty
)
in
List
.
map
ty_of_param
pl
...
...
@@ -364,7 +364,7 @@ let quant_var uc env (id,ty) =
let
quant_vars
uc
env
qvl
=
let
s
=
ref
Sstr
.
empty
in
let
add
env
(({
id
=
id
;
id_loc
=
loc
}
,
_
)
as
qv
)
=
s
:=
Loc
.
try3
loc
Sstr
.
add_new
(
DuplicateVar
id
)
id
!
s
;
s
:=
Loc
.
try3
~
loc
Sstr
.
add_new
(
DuplicateVar
id
)
id
!
s
;
quant_var
uc
env
qv
in
Lists
.
map_fold_left
add
env
qvl
...
...
@@ -523,7 +523,7 @@ and dterm_node ~localize loc uc env = function
Teps
(
id
,
ty
,
Fquant
(
Tforall
,
uqu
,
trl
,
f
))
,
ty
|
PPrecord
fl
->
let
fl
=
List
.
map
(
fun
(
q
,
e
)
->
find_lsymbol
q
uc
,
e
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
parse_record
(
get_known
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
parse_record
(
get_known
uc
)
fl
in
let
tyl
,
ty
=
Denv
.
specialize_lsymbol
~
loc
cs
in
let
get_val
pj
ty
=
match
Mls
.
find_opt
pj
flm
with
|
Some
e
->
...
...
@@ -538,7 +538,7 @@ and dterm_node ~localize loc uc env = function
|
PPupdate
(
e
,
fl
)
->
let
e
=
dterm
~
localize
uc
env
e
in
let
fl
=
List
.
map
(
fun
(
q
,
e
)
->
find_lsymbol
q
uc
,
e
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
parse_record
(
get_known
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
parse_record
(
get_known
uc
)
fl
in
let
tyl
,
ty
=
Denv
.
specialize_lsymbol
~
loc
cs
in
let
get_val
pj
ty
=
match
Mls
.
find_opt
pj
flm
with
|
Some
e
->
...
...
@@ -723,7 +723,7 @@ let add_types dl th =
|
Qident
_
|
Qdot
_
->
find_tysymbol
q
th
in
Loc
.
try2
(
qloc
q
)
ty_app
ts
(
List
.
map
apply
tyl
)
Loc
.
try2
~
loc
:
(
qloc
q
)
ty_app
ts
(
List
.
map
apply
tyl
)
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
ty_app
ts
(
List
.
map
apply
tyl
)
...
...
@@ -766,17 +766,17 @@ let add_types dl th =
let
ty
=
ty_app
ts
(
List
.
map
ty_var
ts
.
ts_args
)
in
let
projection
(
_
,
id
,_,_
)
fty
=
match
id
with
|
None
->
None
|
Some
id
->
|
Some
({
id
=
x
;
id_loc
=
loc
}
as
id
)
->
try
let
pj
=
Hstr
.
find
ht
id
.
id
in
let
pj
=
Hstr
.
find
ht
x
in
let
ty
=
Opt
.
get
pj
.
ls_value
in
ignore
(
Loc
.
try2
id
.
id_
loc
ty_equal_check
ty
fty
);
ignore
(
Loc
.
try2
~
loc
ty_equal_check
ty
fty
);
Some
pj
with
Not_found
->
let
fn
=
create_user_id
id
in
let
pj
=
create_fsymbol
~
opaque
fn
[
ty
]
fty
in
Hstr
.
replace
csymbols
id
.
id
id
.
id_
loc
;
Hstr
.
replace
ht
id
.
id
pj
;
Hstr
.
replace
csymbols
x
loc
;
Hstr
.
replace
ht
x
pj
;
Some
pj
in
let
constructor
(
loc
,
id
,
pl
)
=
...
...
@@ -844,7 +844,7 @@ let add_logics dl th =
let
opaque
=
opaque_tvs
d
.
ld_params
d
.
ld_type
in
let
ls
=
create_lsymbol
~
opaque
v
pl
ty
in
Hstr
.
add
lsymbols
id
ls
;
Loc
.
try2
d
.
ld_loc
add_param_decl
th
ls
Loc
.
try2
~
loc
:
d
.
ld_loc
add_param_decl
th
ls
in
let
th'
=
List
.
fold_left
create_symbol
th
dl
in
(* 2. then type-check all definitions *)
...
...
@@ -924,7 +924,7 @@ let type_fmla uc gfn f =
let
add_prop
k
loc
s
f
th
=
let
pr
=
create_prsymbol
(
create_user_id
s
)
in
let
f
=
type_fmla
th
(
fun
_
->
None
)
f
in
Loc
.
try4
loc
add_prop_decl
th
k
pr
f
Loc
.
try4
~
loc
add_prop_decl
th
k
pr
f
let
loc_of_id
id
=
Opt
.
get
id
.
Ident
.
id_loc
...
...
@@ -938,7 +938,7 @@ let add_inductives s dl th =
let
opaque
=
opaque_tvs
d
.
in_params
None
in
let
ps
=
create_psymbol
~
opaque
v
pl
in
Hstr
.
add
psymbols
id
ps
;
Loc
.
try2
d
.
in_loc
add_param_decl
th
ps
Loc
.
try2
~
loc
:
d
.
in_loc
add_param_decl
th
ps
in
let
th'
=
List
.
fold_left
create_symbol
th
dl
in
(* 2. then type-check all definitions *)
...
...
@@ -1053,11 +1053,11 @@ let add_decl loc th = function
|
PMAint
i
->
MAint
i
in
let
add
s
=
add_meta
th
(
lookup_meta
s
)
(
List
.
map
convert
al
)
in
Loc
.
try1
loc
add
id
.
id
Loc
.
try1
~
loc
add
id
.
id
let
add_decl
loc
th
d
=
if
Debug
.
test_flag
debug_parse_only
then
th
else
Loc
.
try3
loc
add_decl
loc
th
d
Loc
.
try3
~
loc
add_decl
loc
th
d
let
type_inst
th
t
s
=
let
add_inst
s
=
function
...
...
@@ -1065,7 +1065,7 @@ let type_inst th t s =
let
find
ns
x
=
find_namespace_ns
x
ns
in
let
ns1
=
Opt
.
fold
find
t
.
th_export
p
in
let
ns2
=
Opt
.
fold
find
(
get_namespace
th
)
q
in
Loc
.
try6
loc
clone_ns
t
.
th_known
t
.
th_local
[]
ns2
ns1
s
Loc
.
try6
~
loc
clone_ns
t
.
th_known
t
.
th_local
[]
ns2
ns1
s
|
CStsym
(
loc
,
p
,
[]
,
PPTtyapp
(
q
,
[]
))
->
let
ts1
=
find_tysymbol_ns
p
t
.
th_export
in
let
ts2
=
find_tysymbol
q
th
in
...
...
@@ -1077,7 +1077,7 @@ let type_inst th t s =
let
id
=
id_user
(
ts1
.
ts_name
.
id_string
^
"_subst"
)
loc
in
let
tvl
=
List
.
map
(
fun
id
->
create_user_tv
id
.
id
)
tvl
in
let
def
=
Some
(
ty_of_pty
th
pty
)
in
let
ts2
=
Loc
.
try3
loc
create_tysymbol
id
tvl
def
in
let
ts2
=
Loc
.
try3
~
loc
create_tysymbol
id
tvl
def
in
if
Mts
.
mem
ts1
s
.
inst_ts
then
error
~
loc
(
ClashSymbol
ts1
.
ts_name
.
id_string
);
{
s
with
inst_ts
=
Mts
.
add
ts1
ts2
s
.
inst_ts
}
...
...
@@ -1128,7 +1128,7 @@ let add_use_clone env lenv th loc (use, subst) =
|
None
->
use_or_clone
th
in
Loc
.
try1
loc
use_or_clone
th
Loc
.
try1
~
loc
use_or_clone
th
let
close_theory
lenv
th
=
if
Debug
.
test_flag
debug_parse_only
then
lenv
else
...
...
@@ -1139,7 +1139,7 @@ let close_theory lenv th =
Mstr
.
add
id
th
lenv
let
close_namespace
loc
import
th
=
Loc
.
try2
loc
close_namespace
th
import
Loc
.
try2
~
loc
close_namespace
th
import
(* incremental parsing *)
...
...
src/transform/eval_match.ml
View file @
4ff04130
...
...
@@ -49,7 +49,7 @@ let apply_projection kn ls t = match t.t_node with
List
.
fold_left2
find
t_true
tl
pjl
|
_
->
assert
false
let
make_
flat_case
kn
t
bl
=
let
flat_case
kn
t
bl
=
let
mk_b
b
=
let
p
,
t
=
t_open_branch
b
in
[
p
]
,
t
in
let
find_constructors
kn
ts
=
List
.
map
fst
(
find_constructors
kn
ts
)
in
Pattern
.
CompileTerm
.
compile
(
find_constructors
kn
)
[
t
]
(
List
.
map
mk_b
bl
)
...
...
@@ -129,10 +129,7 @@ let eval_match ~inline kn t =
let_map
eval
env
t1
tb2
|
Tcase
(
t1
,
bl1
)
->
let
t1
=
eval
env
t1
in
let
make_flat_case
=
match
t
.
t_loc
with
|
Some
loc
->
Loc
.
try3
loc
make_flat_case
|
None
->
make_flat_case
in
let
fn
env
t
=
eval
env
(
make_flat_case
kn
t
bl1
)
in
let
fn
env
t2
=
eval
env
(
Loc
.
try3
?
loc
:
t
.
t_loc
flat_case
kn
t2
bl1
)
in
begin
try
dive_to_constructor
kn
fn
env
t1
with
Exit
->
branch_map
eval
env
t1
bl1
end
|
Tquant
(
q
,
qf
)
->
...
...
src/util/loc.ml
View file @
4ff04130
...
...
@@ -73,39 +73,37 @@ let report_position fmt = fprintf fmt "%a:@\n" gen_report_position
exception
Located
of
position
*
exn
let
try1
loc
f
x
=
let
error
?
loc
e
=
match
loc
with
|
Some
loc
->
raise
(
Located
(
loc
,
e
))
|
None
->
raise
e
let
try1
?
loc
f
x
=
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
else
try
f
x
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
try
f
x
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
let
try2
loc
f
x
y
=
let
try2
?
loc
f
x
y
=
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
y
else
try
f
x
y
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
try
f
x
y
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
let
try3
loc
f
x
y
z
=
let
try3
?
loc
f
x
y
z
=
if
Debug
.
test_flag
Debug
.
stack_trace
then
f
x
y
z
else
try
f
x
y
z
with
Located
_
as
e
->
raise
e
|
e
->
raise
(
Located
(
loc
,
e
))
try
f
x
y
z
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
let
try4
loc
f
x
y
z
t
=
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
))
try
f
x
y
z
t
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
let
try5
loc
f
x
y
z
t
u
=
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
))
try
f
x
y
z
t
u
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
let
try6
loc
f
x
y
z
t
u
v
=
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
))
try
f
x
y
z
t
u
v
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
let
try7
loc
f
x
y
z
t
u
v
w
=
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
))
try
f
x
y
z
t
u
v
w
with
Located
_
as
e
->
raise
e
|
e
->
error
?
loc
e
(* located messages *)
...
...
src/util/loc.mli
View file @
4ff04130
...
...
@@ -44,21 +44,21 @@ 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
try1
:
?
loc
:
position
->
(
'
a
->
'
b
)
->
(
'
a
->
'
b
)
val
try2
:
?
loc
:
position
->
(
'
a
->
'
b
->
'
c
)
->
(
'
a
->
'
b
->
'
c
)
val
try3
:
?
loc
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
)
->
(
'
a
->
'
b
->
'
c
->
'
d
)
val
try4
:
position
->
val
try4
:
?
loc
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
)
val
try5
:
position
->
val
try5
:
?
loc
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
)
val
try6
:
position
->
val
try6
:
?
loc
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
)
val
try7
:
position
->
val
try7
:
?
loc
:
position
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
->
'
h
)
->
(
'
a
->
'
b
->
'
c
->
'
d
->
'
e
->
'
f
->
'
g
->
'
h
)
...
...
src/whyml/mlw_decl.ml
View file @
4ff04130
...
...
@@ -273,9 +273,8 @@ let check_match lkn _kn d =
let
t_p
=
t_var
(
create_vsymbol
(
id_fresh
"x"
)
typ
)
in
let
t_e
=
t_var
(
create_vsymbol
(
id_fresh
"y"
)
tye
)
in
let
bl
=
List
.
map
(
fun
(
pp
,_
)
->
[
pp
.
ppat_pattern
]
,
t_e
)
bl
in
let
try3
f
=
match
e
.
e_loc
with
Some
l
->
Loc
.
try3
l
f
|
None
->
f
in
let
find
ts
=
List
.
map
fst
(
Decl
.
find_constructors
lkn
ts
)
in
ignore
(
try3
Pattern
.
CompileTerm
.
compile
find
[
t_p
]
bl
);
let
get
ts
=
List
.
map
fst
(
Decl
.
find_constructors
lkn
ts
)
in
ignore
(
Loc
.
try3
?
loc
:
e
.
e_loc
Pattern
.
CompileTerm
.
compile
get
[
t_p
]
bl
);
e_fold
checkE
()
e
|
_
->
e_fold
checkE
()
e
in
...
...
src/whyml/mlw_driver.ml
View file @
4ff04130
...
...
@@ -121,7 +121,7 @@ let load_driver lib file extra_files =
|
PTyapp
((
loc
,_
)
as
q
,
tyl
)
->
let
ts
=
find_ts
th
q
in
let
tyl
=
List
.
map
ty_of_pty
tyl
in
Loc
.
try2
loc
Ty
.
ty_app
ts
tyl
Loc
.
try2
~
loc
Ty
.
ty_app
ts
tyl
|
PTuple
tyl
->
let
ts
=
Ty
.
ts_tuple
(
List
.
length
tyl
)
in
Ty
.
ty_app
ts
(
List
.
map
ty_of_pty
tyl
)
...
...
src/whyml/mlw_typing.ml
View file @
4ff04130
...
...
@@ -240,7 +240,7 @@ let hidden_pl ~loc pl =
let
hidden_ls
~
loc
ls
=
{
de_desc
=
DEglobal_ls
ls
;
de_type
=
Loc
.
try1
loc
specialize_lsymbol
ls
;
de_type
=
Loc
.
try1
~
loc
specialize_lsymbol
ls
;
de_loc
=
loc
;
de_lab
=
Slab
.
empty
}
(* helper functions for let-expansion *)
...
...
@@ -293,7 +293,7 @@ let specialize_qualid uc p = match uc_find_ps uc p with
|
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
,
Loc
.
try1
(
qloc
p
)
specialize_lsymbol
ls
|
LS
ls
->
DEglobal_ls
ls
,
Loc
.
try1
~
loc
:
(
qloc
p
)
specialize_lsymbol
ls
|
XS
xs
->
errorm
~
loc
:
(
qloc
p
)
"unexpected exception symbol %a"
print_xs
xs
let
chainable_qualid
uc
p
=
match
uc_find_ps
uc
p
with
...
...
@@ -345,13 +345,13 @@ let rec dpattern denv ({ pat_loc = loc } as pp) dity = match pp.pat_desc with
|
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
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
Decl
.
parse_record
kn
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
Decl
.
parse_record
kn
fl
in
let
wild
=
{
pat_desc
=
Ptree
.
PPpwild
;
pat_loc
=
loc
}
in
let
get_val
pj
=
Mls
.
find_def
wild
pj
flm
in
dpat_app
denv
loc
(
hidden_ls
~
loc
cs
)
(
List
.
map
get_val
pjl
)
dity
|
Ptree
.
PPprec
fl
->
let
fl
=
List
.
map
(
find_prog_field
denv
.
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
parse_record
denv
.
uc
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
parse_record
denv
.
uc
fl
in
let
wild
=
{
pat_desc
=
Ptree
.
PPpwild
;
pat_loc
=
loc
}
in
let
get_val
pj
=
Mls
.
find_def
wild
pj
.
pl_ls
flm
in
dpat_app
denv
loc
(
hidden_pl
~
loc
cs
)
(
List
.
map
get_val
pjl
)
dity
...
...
@@ -397,7 +397,7 @@ let dbinders denv bl =
in
let
denv
,
id
=
match
id
with
|
Some
({
id
=
x
;
id_loc
=
loc
}
as
id
)
->
s
:=
Loc
.
try3
loc
Sstr
.
add_new
(
DuplicateProgVar
x
)
x
!
s
;
s
:=
Loc
.
try3
~
loc
Sstr
.
add_new
(
DuplicateProgVar
x
)
x
!
s
;
add_var
id
dity
denv
,
id
|
None
->
denv
,
{
id
=
"_"
;
id_loc
=
loc
;
id_lab
=
[]
}
...
...
@@ -577,14 +577,14 @@ and de_desc denv loc = function
|
Ptree
.
Erecord
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
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
Decl
.
parse_record
kn
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
Decl
.
parse_record
kn
fl
in
let
get_val
pj
=
match
Mls
.
find_opt
pj
flm
with
|
Some
e
->
dexpr
denv
e
|
None
->
error
~
loc
(
Decl
.
RecordFieldMissing
(
cs
,
pj
))
in
de_app
loc
(
hidden_ls
~
loc
cs
)
(
List
.
map
get_val
pjl
)
|
Ptree
.
Erecord
fl
->
let
fl
=
List
.
map
(
find_prog_field
denv
.
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
parse_record
denv
.
uc
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
parse_record
denv
.
uc
fl
in
let
get_val
pj
=
match
Mls
.
find_opt
pj
.
pl_ls
flm
with
|
Some
e
->
dexpr
denv
e
|
None
->
error
~
loc
(
Decl
.
RecordFieldMissing
(
cs
.
pl_ls
,
pj
.
pl_ls
))
in
...
...
@@ -594,7 +594,7 @@ and de_desc denv loc = function
let
e0
=
mk_var
"q "
e1
in
let
kn
=
Theory
.
get_known
(
get_theory
denv
.
uc
)
in
let
fl
=
List
.
map
(
find_pure_field
denv
.
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
Decl
.
parse_record
kn
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
Decl
.
parse_record
kn
fl
in
let
get_val
pj
=
match
Mls
.
find_opt
pj
flm
with
|
Some
e
->
dexpr
denv
e
|
None
->
...
...
@@ -607,7 +607,7 @@ and de_desc denv loc = function
let
e1
=
dexpr
denv
e1
in
let
e0
=
mk_var
"q "
e1
in
let
fl
=
List
.
map
(
find_prog_field
denv
.
uc
)
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
loc
parse_record
denv
.
uc
fl
in
let
cs
,
pjl
,
flm
=
Loc
.
try2
~
loc
parse_record
denv
.
uc
fl
in
let
get_val
pj
=
match
Mls
.
find_opt
pj
.
pl_ls
flm
with
|
Some
e
->
dexpr
denv
e
|
None
->
...
...
@@ -854,7 +854,7 @@ let create_post lenv res pat f =
|
Ptree
.
PPpvar
{
id
=
x
}
->
Mstr
.
add
x
res
lenv
.
log_vars
|
Ptree
.
PPptuple
[]
->
Loc
.
try2
pat
.
pat_loc
Ty
.
ty_equal_check
res
.
vs_ty
ty_unit
;
Loc
.
try2
~
loc
:
pat
.
pat_loc
Ty
.
ty_equal_check
res
.
vs_ty
ty_unit
;
lenv
.
log_vars
|
Ptree
.
PPpwild
->
lenv
.
log_vars
...
...
@@ -1165,7 +1165,7 @@ let e_arrow_dity ps (argl,res) =
let
rec
expr
lenv
de
=
let
loc
=
de
.
de_loc
in
let
e
=
Loc
.
try3
loc
expr_desc
lenv
loc
de
in
let
e
=
Loc
.
try3
~
loc
expr_desc
lenv
loc
de
in
e_label
~
loc
de
.
de_lab
e
and
expr_desc
lenv
loc
de
=
match
de
.
de_desc
with
...
...
@@ -1353,7 +1353,7 @@ and expr_rec lenv dfdl =
|
Mlw_ty
.
TypeMismatch
_
as
exn
->
List
.
iter
(
fun
(
ps
,_,_,_
)
->
let
loc
=
Opt
.
get
ps
.
ps_name
.
Ident
.
id_loc
in
Loc
.
try2
loc
check_user_ps
true
ps
)
fdl
;
Loc
.
try2
~
loc
check_user_ps
true
ps
)
fdl
;
raise
exn
in
let
fdl
=
try
create_rec_defn
fdl
with
|
Loc
.
Located
(
_
,
Mlw_ty
.
TypeMismatch
_
)
...
...
@@ -1361,13 +1361,13 @@ and expr_rec lenv dfdl =
List
.
iter
(
fun
(
ps
,
lam
)
->
let
loc
=
Opt
.
get
ps
.
ps_name
.
Ident
.
id_loc
in
let
fd
=
create_fun_defn
(
id_clone
ps
.
ps_name
)
lam
in
Loc
.
try2
loc
check_user_ps
true
fd
.
fun_ps
)
fdl
;
Loc
.
try2
~
loc
check_user_ps
true
fd
.
fun_ps
)
fdl
;
raise
exn
in
let
step3
fd
=
fd
.
fun_ps
,
lambda_invariant
lenv
fd
.
fun_lambda
in
let
fdl
=
create_rec_defn
(
List
.
map
step3
fdl
)
in
let
step4
fd
(
id
,_,_,
bl
,
(
de
,
dsp
))
=
Loc
.
try4
de
.
de_loc
check_lambda_effect
lenv
fd
bl
dsp
;
Loc
.
try2
id
.
id_loc
check_user_ps
true
fd
.
fun_ps
in
Loc
.
try4
~
loc
:
de
.
de_loc
check_lambda_effect
lenv
fd
bl
dsp
;
Loc
.
try2
~
loc
:
id
.
id_loc
check_user_ps
true
fd
.
fun_ps
in
List
.
iter2
step4
fdl
dfdl
;
fdl
...
...
@@ -1389,8 +1389,8 @@ and expr_fun lenv x gh bl (de, dsp as tr) =
{
lam
with
l_spec
=
spec
}
in
let
lam
=
lambda_invariant
lenv
lam
in
let
fd
=
create_fun_defn
(
Denv
.
create_user_id
x
)
lam
in
Loc
.
try4
de
.
de_loc
check_lambda_effect
lenv
fd
bl
dsp
;
Loc
.
try2
x
.
id_loc
check_user_ps
false
fd
.
fun_ps
;
Loc
.
try4
~
loc
:
de
.
de_loc
check_lambda_effect
lenv
fd
bl
dsp
;
Loc
.
try2
~
loc
:
x
.
id_loc
check_user_ps
false
fd
.
fun_ps
;
fd
and
expr_lam
lenv
gh
pvl
(
de
,
dsp
)
=
...
...
@@ -1407,7 +1407,7 @@ let add_type_invariant loc uc id params inv =
let
x
=
"self"
in
let
its
=
match
uc_find_ts
uc
(
Qident
id
)
with
|
PT
its
when
its
.
its_inv
->
its
|
_
->
errorm
~
loc
"type %s does not have an invariant"
id
.
id
in
|
_
->
Loc
.
errorm
~
loc
"type %s does not have an invariant"
id
.
id
in
let
add_tv
acc
{
id
=
id
;
id_loc
=
loc
}
=
let
e
=
Loc
.
Located
(
loc
,
DuplicateTypeVar
id
)
in
Sstr
.
add_new
e
id
acc
,
Typing
.
create_user_tv
id
in
...
...
@@ -1580,8 +1580,8 @@ let add_types ~wp uc tdl =
|
PPTtyapp
(
q
,
tyl
)
->
let
tyl
=
List
.
map
parse
tyl
in
begin
match
get_ts
q
with
|
TS
ts
->
Loc
.
try2
(
qloc
q
)
ity_pur
ts
tyl
|
PT
ts
->
Loc
.
try2
(
qloc
q
)
ity_app_fresh
ts
tyl
|
TS
ts
->
Loc
.
try2
~
loc
:
(
qloc
q
)
ity_pur
ts
tyl
|
PT
ts
->
Loc
.
try2
~
loc
:
(
qloc
q
)
ity_app_fresh
ts
tyl
end
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
...
...
@@ -1613,15 +1613,15 @@ let add_types ~wp uc tdl =
if
not
gh
then
nogh
:=
ity_nonghost_reg
!
nogh
ity
;
let
regs
=
Sreg
.
union
regs
ity
.
ity_vars
.
vars_reg
in
(
regs
,
inv
)
,
(
None
,
fd
)
|
Some
id
->
|
Some
({
id
=
x
;
id_loc
=
loc
}
as
id
)
->
try
let
fd
=
Hstr
.
find
projs
id
.
id
in
if
gh
<>
fd
.
fd_ghost
then
Loc
.
errorm
~
loc
:
id
.
id_loc
let
fd
=
Hstr
.
find
projs
x
in
if
gh
<>
fd
.
fd_ghost
then
Loc
.
errorm
~
loc
"this field must be ghost in every constructor"
;
ignore
(
Loc
.
try3
id
.
id_
loc
ity_match
sbs
fd
.
fd_ity
ity
);
ignore
(
Loc
.
try3
~
loc
ity_match
sbs
fd
.
fd_ity
ity
);
(
regs
,
inv
)
,
(
Some
(
Denv
.
create_user_id
id
)
,
fd
)
with
Not_found
->
Hstr
.
replace
projs
id
.
id
fd
;
Hstr
.
replace
projs
x
fd
;
if
not
gh
then
nogh
:=
ity_nonghost_reg
!
nogh
ity
;
let
regs
=
Sreg
.
union
regs
ity
.
ity_vars
.
vars_reg
in
(
regs
,
inv
)
,
(
Some
(
Denv
.
create_user_id
id
)
,
fd
)
...
...
@@ -1690,8 +1690,8 @@ let add_types ~wp uc tdl =
|
PPTtyapp
(
q
,
tyl
)
->
let
tyl
=
List
.
map
parse
tyl
in
begin
match
get_ts
q
with
|
TS
ts
->
Loc
.
try2
(
qloc
q
)
ity_pur
ts
tyl
|
PT
ts
->
Loc
.
try3
(
qloc
q
)
ity_app
ts
tyl
[]
|
TS
ts
->
Loc
.
try2
~
loc
:
(
qloc
q
)
ity_pur
ts
tyl
|
PT
ts
->
Loc
.
try3
~
loc
:
(
qloc
q
)
ity_app
ts
tyl
[]
end
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
...
...
@@ -1711,15 +1711,15 @@ let add_types ~wp uc tdl =
let
fd
=
mk_field
ity
gh
None
in
match
id
with
|
None
->
None
,
fd
|
Some
id
->
|
Some
({
id
=
x
;
id_loc
=
loc
}
as
id
)
->
try
let
fd
=
Hstr
.
find
projs
id
.
id
in
if
gh
<>
fd
.
fd_ghost
then
Loc
.
errorm
~
loc
:
id
.
id_loc
let
fd
=
Hstr
.
find
projs
x
in
if
gh
<>
fd
.
fd_ghost
then
Loc
.
errorm
~
loc
"this field must be ghost in every constructor"
;
Loc
.
try2
id
.
id_
loc
ity_equal_check
fd
.
fd_ity
ity
;
Loc
.
try2
~
loc
ity_equal_check
fd
.
fd_ity
ity
;
Some
(
Denv
.
create_user_id
id
)
,
fd
with
Not_found
->
Hstr
.
replace
projs
id
.
id
fd
;
Hstr
.
replace
projs
x
fd
;
Some
(
Denv
.
create_user_id
id
)
,
fd
in