Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
124
Issues
124
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
0dc78832
Commit
0dc78832
authored
May 30, 2011
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
no more prelude theory for programs
parent
2899d9b7
Changes
12
Hide whitespace changes
Inline
Side-by-side
Showing
12 changed files
with
147 additions
and
147 deletions
+147
-147
src/parser/denv.ml
src/parser/denv.ml
+12
-1
src/parser/denv.mli
src/parser/denv.mli
+1
-1
src/parser/typing.ml
src/parser/typing.ml
+9
-20
src/parser/typing.mli
src/parser/typing.mli
+0
-2
src/programs/pgm_main.ml
src/programs/pgm_main.ml
+10
-10
src/programs/pgm_module.ml
src/programs/pgm_module.ml
+48
-16
src/programs/pgm_module.mli
src/programs/pgm_module.mli
+18
-4
src/programs/pgm_typing.ml
src/programs/pgm_typing.ml
+18
-28
src/programs/pgm_typing.mli
src/programs/pgm_typing.mli
+4
-4
src/programs/pgm_wp.ml
src/programs/pgm_wp.ml
+26
-42
tests/test-jcf.why
tests/test-jcf.why
+1
-0
theories/programs.why
theories/programs.why
+0
-19
No files found.
src/parser/denv.ml
View file @
0dc78832
...
...
@@ -51,7 +51,18 @@ and type_var = {
}
let
tyvar
v
=
Tyvar
v
let
tyapp
(
s
,
tyl
)
=
Tyapp
(
s
,
tyl
)
let
rec
type_inst
s
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
n
->
Mtv
.
find
n
s
|
Ty
.
Tyapp
(
ts
,
tyl
)
->
Tyapp
(
ts
,
List
.
map
(
type_inst
s
)
tyl
)
let
tyapp
ts
tyl
=
match
ts
.
ts_def
with
|
None
->
Tyapp
(
ts
,
tyl
)
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
let
s
=
List
.
fold_left2
add
Mtv
.
empty
ts
.
ts_args
tyl
in
type_inst
s
ty
type
dty
=
dty_view
...
...
src/parser/denv.mli
View file @
0dc78832
...
...
@@ -32,7 +32,7 @@ val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var
type
dty
val
tyvar
:
type_var
->
dty
val
tyapp
:
tysymbol
*
dty
list
->
dty
val
tyapp
:
tysymbol
->
dty
list
->
dty
type
dty_view
=
|
Tyvar
of
type_var
...
...
src/parser/typing.ml
View file @
0dc78832
...
...
@@ -198,10 +198,6 @@ let add_ind_decls = with_tuples ~reset:true add_ind_decl
let
add_prop_decl
=
with_tuples
~
reset
:
true
add_prop_decl
let
rec
type_inst
s
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
n
->
Mtv
.
find
n
s
|
Ty
.
Tyapp
(
ts
,
tyl
)
->
tyapp
(
ts
,
List
.
map
(
type_inst
s
)
tyl
)
let
rec
dty
uc
env
=
function
|
PPTtyvar
{
id
=
x
}
->
tyvar
(
find_user_type_var
x
env
)
...
...
@@ -211,17 +207,10 @@ let rec dty uc env = function
let
np
=
List
.
length
p
in
if
np
<>
a
then
error
~
loc
(
TypeArity
(
x
,
a
,
np
));
let
tyl
=
List
.
map
(
dty
uc
env
)
p
in
begin
match
ts
.
ts_def
with
|
None
->
tyapp
(
ts
,
tyl
)
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
let
s
=
List
.
fold_left2
add
Mtv
.
empty
ts
.
ts_args
tyl
in
type_inst
s
ty
end
tyapp
ts
tyl
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
tyapp
(
ts
,
List
.
map
(
dty
uc
env
)
tyl
)
tyapp
ts
(
List
.
map
(
dty
uc
env
)
tyl
)
let
find_ns
find
p
ns
=
let
loc
=
qloc
p
in
...
...
@@ -407,7 +396,7 @@ and dpat_node loc uc env = function
let
s
=
fs_tuple
n
in
let
tyl
=
List
.
map
(
fun
_
->
fresh_type_var
loc
)
pl
in
let
env
,
pl
=
dpat_args
s
.
ls_name
loc
uc
env
tyl
pl
in
let
ty
=
tyapp
(
ts_tuple
n
,
tyl
)
in
let
ty
=
tyapp
(
ts_tuple
n
)
tyl
in
env
,
Papp
(
s
,
pl
)
,
ty
|
PPpas
(
p
,
x
)
->
let
env
,
p
=
dpat
uc
env
p
in
...
...
@@ -493,16 +482,16 @@ and dterm_node ~localize loc uc env = function
let
s
=
fs_tuple
n
in
let
tyl
=
List
.
map
(
fun
_
->
fresh_type_var
loc
)
tl
in
let
tl
=
dtype_args
s
.
ls_name
loc
uc
env
tyl
tl
in
let
ty
=
tyapp
(
ts_tuple
n
,
tyl
)
in
let
ty
=
tyapp
(
ts_tuple
n
)
tyl
in
Tapp
(
s
,
tl
)
,
ty
|
PPinfix
(
e1
,
x
,
e2
)
->
let
s
,
tyl
,
ty
=
specialize_fsymbol
(
Qident
x
)
uc
in
let
tl
=
dtype_args
s
.
ls_name
loc
uc
env
tyl
[
e1
;
e2
]
in
Tapp
(
s
,
tl
)
,
ty
|
PPconst
(
ConstInt
_
as
c
)
->
Tconst
c
,
tyapp
(
Ty
.
ts_int
,
[]
)
Tconst
c
,
tyapp
Ty
.
ts_int
[]
|
PPconst
(
ConstReal
_
as
c
)
->
Tconst
c
,
tyapp
(
Ty
.
ts_real
,
[]
)
Tconst
c
,
tyapp
Ty
.
ts_real
[]
|
PPlet
(
x
,
e1
,
e2
)
->
let
e1
=
dterm
~
localize
uc
env
e1
in
let
ty
=
e1
.
dt_ty
in
...
...
@@ -574,7 +563,7 @@ and dterm_node ~localize loc uc env = function
|
TRterm
t
->
let
id
=
{
id
=
"fc"
;
id_lab
=
[]
;
id_loc
=
loc
}
in
let
tyl
,
ty
=
List
.
fold_right
(
fun
(
_
,
uty
)
(
tyl
,
ty
)
->
let
nty
=
tyapp
(
ts_func
,
[
uty
;
ty
])
in
ty
::
tyl
,
nty
)
let
nty
=
tyapp
ts_func
[
uty
;
ty
]
in
ty
::
tyl
,
nty
)
uqu
([]
,
t
.
dt_ty
)
in
let
h
=
{
dt_node
=
Tvar
id
.
id
;
dt_ty
=
ty
}
in
...
...
@@ -591,8 +580,8 @@ and dterm_node ~localize loc uc env = function
|
[]
->
assert
false
in
let
tyl
,
ty
=
List
.
fold_right
(
fun
(
_
,
uty
)
(
tyl
,
ty
)
->
let
nty
=
tyapp
(
ts_func
,
[
uty
;
ty
])
in
ty
::
tyl
,
nty
)
uqu
([]
,
tyapp
(
ts_pred
,
[
uty
])
)
let
nty
=
tyapp
ts_func
[
uty
;
ty
]
in
ty
::
tyl
,
nty
)
uqu
([]
,
tyapp
ts_pred
[
uty
]
)
in
let
h
=
{
dt_node
=
Tvar
id
.
id
;
dt_ty
=
ty
}
in
let
h
=
List
.
fold_left2
(
fun
h
(
uid
,
uty
)
ty
->
...
...
src/parser/typing.mli
View file @
0dc78832
...
...
@@ -59,8 +59,6 @@ val create_denv : unit -> denv
val
create_user_type_var
:
string
->
Denv
.
type_var
val
find_user_type_var
:
string
->
denv
->
Denv
.
type_var
val
type_inst
:
Denv
.
dty
Ty
.
Mtv
.
t
->
Ty
.
ty
->
Denv
.
dty
val
mem_var
:
string
->
denv
->
bool
val
find_var
:
string
->
denv
->
Denv
.
dty
val
add_var
:
string
->
Denv
.
dty
->
denv
->
denv
...
...
src/programs/pgm_main.ml
View file @
0dc78832
...
...
@@ -39,10 +39,10 @@ let add_module ?(type_only=false) env penv (ltm, lmod) m =
if
Mnm
.
mem
id
.
id
lmod
then
raise
(
Loc
.
Located
(
loc
,
ClashModule
id
.
id
));
let
wp
=
not
type_only
in
let
uc
=
create_module
(
Ident
.
id_user
id
.
id
loc
)
in
let
prelude
=
Env
.
find_theory
env
[
"
programs"
]
"Prelude
"
in
let
prelude
=
Env
.
find_theory
env
[
"
bool"
]
"Bool
"
in
let
uc
=
use_export_theory
uc
prelude
in
let
uc
=
List
.
fold_left
(
Pgm_typing
.
decl
~
wp
env
penv
ltm
lmod
)
uc
m
.
mod_decl
let
uc
=
List
.
fold_left
(
Pgm_typing
.
decl
~
wp
env
penv
ltm
lmod
)
uc
m
.
mod_decl
in
let
m
=
close_module
uc
in
Mnm
.
add
id
.
id
m
.
m_pure
ltm
,
...
...
@@ -57,17 +57,17 @@ let retrieve penv file c =
else
let
type_only
=
Debug
.
test_flag
Typing
.
debug_type_only
in
let
env
=
Pgm_env
.
get_env
penv
in
List
.
fold_left
(
add_module
~
type_only
env
penv
)
List
.
fold_left
(
add_module
~
type_only
env
penv
)
(
Mnm
.
empty
,
Mnm
.
empty
)
ml
let
pgm_env_of_env
=
let
h
=
Env
.
Wenv
.
create
17
in
fun
env
->
try
Env
.
Wenv
.
find
h
env
with
Not_found
->
let
penv
=
Pgm_env
.
create
env
retrieve
in
Env
.
Wenv
.
set
h
env
penv
;
fun
env
->
try
Env
.
Wenv
.
find
h
env
with
Not_found
->
let
penv
=
Pgm_env
.
create
env
retrieve
in
Env
.
Wenv
.
set
h
env
penv
;
penv
let
read_channel
env
file
c
=
...
...
src/programs/pgm_module.ml
View file @
0dc78832
...
...
@@ -20,6 +20,8 @@
open
Why
open
Util
open
Ident
open
Ty
open
Decl
open
Theory
open
Term
...
...
@@ -93,8 +95,8 @@ let pure_uc uc = uc.uc_pure
let
add_pervasives
uc
=
(* type unit = () *)
let
ts
=
Ty
.
create_tysymbol
let
ts
=
Ty
.
create_tysymbol
(
id_fresh
"unit"
)
[]
(
Some
(
Ty
.
ty_app
(
Ty
.
ts_tuple
0
)
[]
))
in
add_ty_decl
uc
[
ts
,
Decl
.
Tabstract
]
...
...
@@ -162,15 +164,41 @@ let add_psymbol ps uc =
let
ls_Exit
=
create_lsymbol
(
id_fresh
"%Exit"
)
[]
(
Some
ty_exn
)
let
create_module
n
=
let
m
=
{
(* type unit = () *)
let
ty_unit
=
ty_tuple
[]
let
ts_unit
=
create_tysymbol
(
id_fresh
"unit"
)
[]
(
Some
ty_unit
)
(* logic ignore 'a : () *)
let
ts_label
=
create_tysymbol
(
id_fresh
"label"
)
[]
None
let
ty_label
=
ty_app
ts_label
[]
let
fs_at
=
let
ty
=
ty_var
(
create_tvsymbol
(
id_fresh
"a"
))
in
create_lsymbol
(
id_fresh
"at"
)
[
ty
;
ty_label
]
(
Some
ty
)
let
fs_old
=
let
ty
=
ty_var
(
create_tvsymbol
(
id_fresh
"a"
))
in
create_lsymbol
(
id_fresh
"old"
)
[
ty
]
(
Some
ty
)
let
th_prelude
=
let
uc
=
create_theory
(
id_fresh
"Prelude"
)
in
let
uc
=
use_export
uc
(
tuple_theory
0
)
in
let
uc
=
add_ty_decl
uc
[
ts_unit
,
Tabstract
]
in
let
uc
=
add_ty_decl
uc
[
ts_label
,
Tabstract
]
in
let
uc
=
add_logic_decl
uc
[
fs_at
,
None
]
in
let
uc
=
add_logic_decl
uc
[
fs_old
,
None
]
in
close_theory
uc
let
empty_module
n
=
let
m
=
{
uc_name
=
id_register
n
;
uc_impure
=
Theory
.
create_theory
n
;
uc_effect
=
Theory
.
create_theory
n
;
uc_pure
=
Theory
.
create_theory
n
;
uc_decls
=
[]
;
uc_import
=
[
empty_ns
];
uc_export
=
[
empty_ns
];
}
uc_export
=
[
empty_ns
];
}
in
(* pervasives *)
let
m
=
add_esymbol
ls_Exit
m
in
...
...
@@ -199,9 +227,9 @@ let close_module uc = match uc.uc_export with
{
m_name
=
uc
.
uc_name
;
m_decls
=
List
.
rev
uc
.
uc_decls
;
m_export
=
e
;
m_impure
=
close_theory
uc
.
uc_impure
;
m_effect
=
close_theory
uc
.
uc_effect
;
m_pure
=
close_theory
uc
.
uc_pure
;
m_impure
=
close_theory
uc
.
uc_impure
;
m_effect
=
close_theory
uc
.
uc_effect
;
m_pure
=
close_theory
uc
.
uc_pure
;
}
|
_
->
raise
CloseModule
...
...
@@ -213,21 +241,21 @@ let use_export uc m =
|
i0
::
sti
,
e0
::
ste
->
{
uc
with
uc_import
=
merge_ns
false
m
.
m_export
i0
::
sti
;
uc_export
=
merge_ns
true
m
.
m_export
e0
::
ste
;
uc_impure
=
Theory
.
use_export
uc
.
uc_impure
m
.
m_impure
;
uc_effect
=
Theory
.
use_export
uc
.
uc_effect
m
.
m_effect
;
uc_impure
=
Theory
.
use_export
uc
.
uc_impure
m
.
m_impure
;
uc_effect
=
Theory
.
use_export
uc
.
uc_effect
m
.
m_effect
;
uc_pure
=
Theory
.
use_export
uc
.
uc_pure
m
.
m_pure
;
}
|
_
->
assert
false
let
use_export_theory
uc
th
=
let
uc
=
{
uc
with
{
uc
with
uc_impure
=
Theory
.
use_export
uc
.
uc_impure
th
;
uc_effect
=
Theory
.
use_export
uc
.
uc_effect
th
;
uc_pure
=
Theory
.
use_export
uc
.
uc_pure
th
;
}
in
(* all type symbols from th are added as (pure) mtsymbols *)
let
add_ts
_
ts
=
ignore
let
add_ts
_
ts
=
ignore
(
create_mtsymbol
~
impure
:
ts
~
effect
:
ts
~
pure
:
ts
~
singleton
:
false
)
in
let
rec
add_ns
ns
uc
=
...
...
@@ -236,6 +264,10 @@ let use_export_theory uc th =
in
add_ns
th
.
th_export
uc
let
create_module
id
=
let
uc
=
empty_module
id
in
use_export_theory
uc
th_prelude
let
add_impure_pdecl
env
ltm
d
uc
=
{
uc
with
uc_impure
=
Typing
.
add_decl
env
ltm
uc
.
uc_impure
d
}
...
...
@@ -246,14 +278,14 @@ let add_pure_pdecl env ltm d uc =
{
uc
with
uc_pure
=
Typing
.
add_decl
env
ltm
uc
.
uc_pure
d
;
}
let
add_pdecl
env
ltm
d
uc
=
{
uc
with
{
uc
with
uc_impure
=
Typing
.
add_decl
env
ltm
uc
.
uc_impure
d
;
uc_effect
=
Typing
.
add_decl
env
ltm
uc
.
uc_effect
d
;
uc_pure
=
Typing
.
add_decl
env
ltm
uc
.
uc_pure
d
;
}
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
End:
*)
src/programs/pgm_module.mli
View file @
0dc78832
...
...
@@ -19,6 +19,7 @@
open
Why
open
Ident
open
Ty
open
Term
open
Theory
open
Pgm_types
...
...
@@ -72,17 +73,30 @@ val add_impure_decl : Decl.decl -> uc -> uc
val
add_effect_decl
:
Decl
.
decl
->
uc
->
uc
val
add_pure_decl
:
Decl
.
decl
->
uc
->
uc
val
add_impure_pdecl
:
val
add_impure_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
val
add_effect_pdecl
:
val
add_effect_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
val
add_pure_pdecl
:
val
add_pure_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
val
add_pdecl
:
val
add_pdecl
:
Env
.
env
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Ptree
.
decl
->
uc
->
uc
(** add in impure, effect and pure *)
(** builtins *)
val
ts_label
:
tysymbol
val
ty_label
:
ty
val
ts_unit
:
tysymbol
val
ty_unit
:
ty
val
fs_old
:
lsymbol
val
fs_at
:
lsymbol
val
th_prelude
:
theory
(** exceptions *)
exception
CloseModule
src/programs/pgm_typing.ml
View file @
0dc78832
...
...
@@ -80,18 +80,16 @@ let is_mutable_field ts i =
(* phase 1: typing programs (using destructive type inference) **************)
let
dty_app
(
ts
,
tyl
)
=
assert
(
ts
.
ts_def
=
None
);
tyapp
(
ts
,
tyl
)
let
find_ts
~
pure
uc
s
=
ns_find_ts
(
get_namespace
(
if
pure
then
pure_uc
uc
else
impure_uc
uc
))
[
s
]
let
find_ls
~
pure
uc
s
=
ns_find_ls
(
get_namespace
(
if
pure
then
pure_uc
uc
else
impure_uc
uc
))
[
s
]
(* TODO: improve efficiency *)
let
dty_bool
uc
=
dty_app
(
find_ts
~
pure
:
true
uc
"bool"
,
[]
)
let
dty_int
_uc
=
dty_app
(
Ty
.
ts_int
,
[]
)
let
dty_unit
_uc
=
dty_app
(
ts_tuple
0
,
[]
)
let
dty_label
uc
=
dty_app
(
find_ts
~
pure
:
true
uc
"label_"
,
[]
)
let
dty_bool
uc
=
tyapp
(
find_ts
~
pure
:
true
uc
"bool"
)
[]
let
dty_int
_uc
=
tyapp
Ty
.
ts_int
[]
let
dty_unit
_uc
=
tyapp
(
ts_tuple
0
)
[]
let
dty_label
_uc
=
tyapp
ts_label
[]
(* note: local variables are simultaneously in locals (to type programs)
and in denv (to type logic elements) *)
...
...
@@ -111,7 +109,7 @@ let loc_of_id id = Util.of_option id.Ident.id_loc
let
loc_of_ls
ls
=
ls
.
ls_name
.
Ident
.
id_loc
let
dcurrying
tyl
ty
=
let
make_arrow_type
ty1
ty2
=
dty_app
(
ts_arrow
,
[
ty1
;
ty2
])
in
let
make_arrow_type
ty1
ty2
=
tyapp
ts_arrow
[
ty1
;
ty2
]
in
List
.
fold_right
make_arrow_type
tyl
ty
type
region_policy
=
Region_var
|
Region_ret
|
Region_glob
...
...
@@ -176,7 +174,7 @@ let rec specialize_ty ?(policy=Region_var) ~loc htv ty = match ty.ty_node with
in
let
regions
=
List
.
map
mk_region
(
Util
.
prefix
n
tl
)
in
let
tl
=
List
.
map
(
specialize_ty
~
policy
~
loc
htv
)
(
Util
.
chop
n
tl
)
in
tyapp
(
ts
,
regions
@
tl
)
tyapp
ts
(
regions
@
tl
)
let
rec
specialize_type_v
?
(
policy
=
Region_var
)
~
loc
htv
=
function
|
Tpure
ty
->
...
...
@@ -245,7 +243,7 @@ let dexception uc qid =
let
sl
=
Typing
.
string_list_of_qualid
[]
qid
in
let
loc
=
Typing
.
qloc
qid
in
let
_
,
_
,
ty
as
r
=
specialize_exception
loc
sl
uc
in
let
ty_exn
=
dty_app
(
ts_exn
,
[]
)
in
let
ty_exn
=
tyapp
ts_exn
[]
in
if
not
(
Denv
.
unify
ty
ty_exn
)
then
errorm
~
loc
"@[this expression has type %a,@ but is expected to be an exception@]"
...
...
@@ -291,17 +289,10 @@ let rec dtype ~user env = function
print_qualid
x
(
a
-
mt
.
mt_regions
)
np
;
let
tyl
=
List
.
map
(
dtype
~
user
env
)
p
in
let
tyl
=
create_regions
~
user
mt
.
mt_regions
@
tyl
in
begin
match
ts
.
ts_def
with
|
None
->
tyapp
(
ts
,
tyl
)
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
let
s
=
List
.
fold_left2
add
Mtv
.
empty
ts
.
ts_args
tyl
in
Typing
.
type_inst
s
ty
end
tyapp
ts
tyl
|
PPTtuple
tyl
->
let
ts
=
ts_tuple
(
List
.
length
tyl
)
in
tyapp
(
ts
,
List
.
map
(
dtype
~
user
env
)
tyl
)
tyapp
ts
(
List
.
map
(
dtype
~
user
env
)
tyl
)
let
rec
dutype_v
env
=
function
|
Ptree
.
Tpure
pt
->
...
...
@@ -389,9 +380,9 @@ let rec dexpr ~ghost env e =
and
dexpr_desc
~
ghost
env
loc
=
function
|
Ptree
.
Econstant
(
ConstInt
_
as
c
)
->
DEconstant
c
,
dty_app
(
Ty
.
ts_int
,
[]
)
DEconstant
c
,
tyapp
Ty
.
ts_int
[]
|
Ptree
.
Econstant
(
ConstReal
_
as
c
)
->
DEconstant
c
,
dty_app
(
Ty
.
ts_real
,
[]
)
DEconstant
c
,
tyapp
Ty
.
ts_real
[]
|
Ptree
.
Eident
(
Qident
{
id
=
x
})
when
Mstr
.
mem
x
env
.
locals
->
(* local variable *)
let
tyv
=
Mstr
.
find
x
env
.
locals
in
...
...
@@ -437,7 +428,7 @@ and dexpr_desc ~ghost env loc = function
let
ghost
=
ghost
(* || is_ps_ghost e1 *)
in
let
e2
=
dexpr
~
ghost
env
e2
in
let
ty2
=
create_type_var
loc
and
ty
=
create_type_var
loc
in
if
not
(
Denv
.
unify
e1
.
dexpr_type
(
dty_app
(
ts_arrow
,
[
ty2
;
ty
])
))
then
if
not
(
Denv
.
unify
e1
.
dexpr_type
(
tyapp
ts_arrow
[
ty2
;
ty
]
))
then
errorm
~
loc
:
e1
.
dexpr_loc
"this expression is not a function"
;
expected_type
e2
ty2
;
DEapply
(
e1
,
e2
)
,
ty
...
...
@@ -461,13 +452,13 @@ and dexpr_desc ~ghost env loc = function
let
n
=
List
.
length
el
in
let
s
=
Typing
.
fs_tuple
n
in
let
tyl
=
List
.
map
(
fun
_
->
create_type_var
loc
)
el
in
let
ty
=
dty_app
(
Typing
.
ts_tuple
n
,
tyl
)
in
let
ty
=
tyapp
(
Typing
.
ts_tuple
n
)
tyl
in
let
create
d
ty
=
{
dexpr_desc
=
d
;
dexpr_type
=
ty
;
dexpr_loc
=
loc
}
in
let
apply
e1
e2
ty2
=
let
e2
=
dexpr
~
ghost
env
e2
in
assert
(
Denv
.
unify
e2
.
dexpr_type
ty2
);
let
ty
=
create_type_var
loc
in
assert
(
Denv
.
unify
e1
.
dexpr_type
(
dty_app
(
ts_arrow
,
[
ty2
;
ty
])
));
assert
(
Denv
.
unify
e1
.
dexpr_type
(
tyapp
ts_arrow
[
ty2
;
ty
]
));
create
(
DEapply
(
e1
,
e2
))
ty
in
let
e
=
create
(
DElogic
s
)
(
dcurrying
tyl
ty
)
in
...
...
@@ -484,7 +475,7 @@ and dexpr_desc ~ghost env loc = function
let
f
=
dexpr
~
ghost
env
f
in
assert
(
Denv
.
unify
f
.
dexpr_type
tyf
);
let
ty
=
create_type_var
loc
in
assert
(
Denv
.
unify
d
.
dexpr_type
(
dty_app
(
ts_arrow
,
[
tyf
;
ty
])
));
assert
(
Denv
.
unify
d
.
dexpr_type
(
tyapp
ts_arrow
[
tyf
;
ty
]
));
create
(
DEapply
(
d
,
f
))
ty
|
None
->
errorm
~
loc
"some record fields are missing"
...
...
@@ -704,7 +695,7 @@ let rec dty_of_ty denv ty = match ty.ty_node with
|
Ty
.
Tyvar
v
->
Denv
.
tyvar
(
Typing
.
find_user_type_var
v
.
tv_name
.
id_string
denv
)
|
Ty
.
Tyapp
(
ts
,
tyl
)
->
Denv
.
tyapp
(
ts
,
List
.
map
(
dty_of_ty
denv
)
tyl
)
Denv
.
tyapp
ts
(
List
.
map
(
dty_of_ty
denv
)
tyl
)
let
iadd_local
env
x
ty
=
let
v
=
create_ivsymbol
x
ty
in
...
...
@@ -1165,8 +1156,7 @@ and iexpr_desc gl env loc ty = function
let
f
=
ifmla
env
f
in
IEassert
(
k
,
f
)
|
DElabel
(
s
,
e1
)
->
let
ty
=
Ty
.
ty_app
(
find_ts
~
pure
:
true
gl
"label_"
)
[]
in
let
env
,
v
=
iadd_local
env
(
id_fresh
s
)
ty
in
let
env
,
v
=
iadd_local
env
(
id_fresh
s
)
ty_label
in
IElabel
(
v
.
i_impure
,
iexpr
gl
env
e1
)
|
DEany
c
->
let
c
=
iutype_c
gl
env
c
in
...
...
@@ -1408,7 +1398,7 @@ let mk_false loc gl = mk_bool_constant loc gl (find_ls ~pure:true gl "False")
let
mk_true
loc
gl
=
mk_bool_constant
loc
gl
(
find_ls
~
pure
:
true
gl
"True"
)
(* check that variables occurring in 'old' and 'at' are not local variables *)
let
check_at_fmla
f
=
let
check_at_fmla
_
f
=
assert
false
(*TODO*)
(* Saturation of postconditions: a postcondition must be set for
...
...
src/programs/pgm_typing.mli
View file @
0dc78832
...
...
@@ -22,8 +22,8 @@ open Util
val
debug
:
Debug
.
flag
val
decl
:
wp
:
bool
->
Env
.
env
->
Pgm_env
.
t
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Pgm_module
.
t
Theory
.
Mnm
.
t
->
val
decl
:
wp
:
bool
->
Env
.
env
->
Pgm_env
.
t
->
Theory
.
theory
Theory
.
Mnm
.
t
->
Pgm_module
.
t
Theory
.
Mnm
.
t
->
Pgm_module
.
uc
->
Ptree
.
program_decl
->
Pgm_module
.
uc
src/programs/pgm_wp.ml
View file @
0dc78832
...
...
@@ -99,9 +99,8 @@ let wp_forall v f =
(* utility functions for building WPs *)
let
fresh_label
env
=
let
ty
=
ty_app
(
find_ts
~
pure
:
true
env
"label_"
)
[]
in
create_vsymbol
(
id_fresh
"label"
)
ty
let
fresh_label
()
=
create_vsymbol
(
id_fresh
"label"
)
ty_label
let
wp_binder
x
f
=
match
x
.
pv_tv
with
|
Tpure
_
->
wp_forall
x
.
pv_pure
f
...
...
@@ -121,46 +120,31 @@ let add_binder x rm =
let
add_binders
=
List
.
fold_right
add_binder
(* replace old(t) with at(t,lab) everywhere in formula f *)
let
rec
old_label
env
lab
f
=
TermTF
.
t_map
(
old_label_term
env
lab
)
(
old_label
env
lab
)
f
and
old_label_term
env
lab
t
=
match
t
.
t_node
with
|
Tapp
(
ls
,
[
t
])
when
ls_equal
ls
(
find_ls
~
pure
:
true
env
"old"
)
->
let
t
=
old_label_term
env
lab
t
in
(* NECESSARY? *)
t_app
(
find_ls
~
pure
:
true
env
"at"
)
[
t
;
t_var
lab
]
t
.
t_ty
let
rec
old_label
lab
t
=
match
t
.
t_node
with
|
Tapp
(
ls
,
[
t
])
when
ls_equal
ls
fs_old
->
let
t
=
old_label
lab
t
in
(* NECESSARY? *)
t_app
fs_at
[
t
;
t_var
lab
]
t
.
t_ty
|
_
->
TermTF
.
t_map
(
old_label_term
env
lab
)
(
old_label
env
lab
)
t
t_map
(
old_label
lab
)
t
(* replace at(t,lab) with t everywhere in formula f *)
let
rec
erase_label
env
lab
f
=
TermTF
.
t_map
(
erase_label_term
env
lab
)
(
erase_label
env
lab
)
f
and
erase_label_term
env
lab
t
=
match
t
.
t_node
with
let
rec
erase_label
lab
t
=
match
t
.
t_node
with
|
Tapp
(
ls
,
[
t
;
{
t_node
=
Tvar
l
}])
when
ls_equal
ls
(
find_ls
~
pure
:
true
env
"at"
)
&&
vs_equal
l
lab
->
erase_label
_term
env
lab
t
when
ls_equal
ls
fs_at
&&
vs_equal
l
lab
->
erase_label
lab
t
|
_
->
TermTF
.
t_map
(
erase_label_term
env
lab
)
(
erase_label
env
lab
)
t
let
rec
unref
env
s
f
=
TermTF
.
t_map
(
unref_term
env
s
)
(
unref
env
s
)
f
and
unref_term
env
s
t
=
match
t
.
t_node
with
(***
| R.Rglobal {p_ls=ls1}, Tapp (ls2, _) when ls_equal ls1 ls2 ->
t_var v
| R.Rlocal {pv_vs=vs1}, Tvar vs2 when vs_equal vs1 vs2 ->
t_var v
***)
t_map
(
erase_label
lab
)
t
let
rec
unref
s
t
=
match
t
.
t_node
with
|
Tvar
vs
->
begin
try
t_var
(
Mvs
.
find
vs
s
)
with
Not_found
->
t
end
|
Tapp
(
ls
,
_
)
when
ls_equal
ls
(
find_ls
~
pure
:
true
env
"old"
)
->
|
Tapp
(
ls
,
_
)
when
ls_equal
ls
fs_old
->
assert
false
|
Tapp
(
ls
,
_
)
when
ls_equal
ls
(
find_ls
~
pure
:
true
env
"at"
)
->
|
Tapp
(
ls
,
_
)
when
ls_equal
ls
fs_at
->
(* do not recurse in at(...) *)
t
|
_
->
TermTF
.
t_map
(
unref_term
env
s
)
(
unref
env
s
)
t
t_map
(
unref
s
)
t
let
find_constructor
env
ts
=
let
km
=
get_known
(
pure_uc
env
)
in
...
...
@@ -268,7 +252,7 @@ let quantify env rm sreg f =
in
Spv
.
fold
add
vars
Mvs
.
empty
in
let
f
=
unref
env
vv'
f
in
let
f
=
unref
vv'
f
in
let
f
=
let
add_update
x
f
=
let
v'
=
Mvs
.
find
x
.
pv_pure
vv'
in
...
...
@@ -338,10 +322,10 @@ let abstract_wp env rm ef (q',ql') (q,ql) =
wp_ands
(
f
::
List
.
map2
quantify_h
ql'
ql
)
let
opaque_wp
env
rm
ef
q'
q
=
let
lab
=
fresh_label
env
in
let
q'
=
post_map
(
old_label
env
lab
)
q'
in
let
lab
=
fresh_label
()
in
let
q'
=
post_map
(
old_label
lab
)
q'
in
let
f
=
abstract_wp
env
rm
ef
q'
q
in
erase_label
env
lab
f
erase_label
lab
f
(*s [filter_post k q] removes exc. postconditions from [q] which do not
appear in effect [ef] *)
...
...
@@ -445,10 +429,10 @@ let add_expl msg f =
*)
let
rec
wp_expr
env
rm
e
q
=
let
lab
=
fresh_label
env
in
let
q
=
post_map
(
old_label
env
lab
)
q
in
let
lab
=
fresh_label
()
in
let
q
=
post_map
(
old_label
lab
)
q
in
let
f
=
wp_desc
env
rm
e
q
in
let
f
=
erase_label
env
lab
f
in
let
f
=
erase_label
lab
f
in
let
f
=
wp_label
~
loc
:
e
.
expr_loc
f
in
if
Debug
.
test_flag
debug
then
begin
eprintf
"@[--------@
\n
@[<hov 2>e = %a@]@
\n
"
Pgm_pretty
.
print_expr
e
;
...
...
@@ -502,11 +486,11 @@ and wp_desc env rm e q = match e.expr_desc with
wp_expr
env
rm
e1
q1
|
Eloop
({
loop_invariant
=
inv
;
loop_variant
=
var
}
,
e1
)
->
let
wfr
=
well_founded_rel
var
in
let
lab
=
fresh_label
env
in
let
lab
=
fresh_label
()
in
let
q1
=
while_post_block
env
inv
var
lab
e1
in
let
q1
=
sup
q1
q
in
(* exc. posts taken from [q] *)
let
we
=
wp_expr
env
rm
e1
q1
in
let
we
=
erase_label
env
lab
we
in
let
we
=
erase_label
lab
we
in
let
sreg
=
e
.
expr_effect
.
E
.
writes
in
let
w
=
match
inv
with
|
None
->
...
...
@@ -615,7 +599,7 @@ and wp_desc env rm e q = match e.expr_desc with
wp_implies
f
q
|
Elabel
(
lab
,
e1
)
->
let
w1
=
wp_expr
env
rm
e1
q
in
erase_label
env
lab
w1
erase_label
lab
w1
|
Eany
c
->
(* TODO: propagate call labels into c.c_post *)
let
w
=
opaque_wp
env
rm
c
.
c_effect
.
E
.
writes
c
.
c_post
q
in
...
...