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
125
Issues
125
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
332f8a72
Commit
332f8a72
authored
Mar 26, 2018
by
Mário Pereira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Extraction of zero-argument functions (wip)
Bench reestablished
parent
55bbff3d
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
334 additions
and
328 deletions
+334
-328
src/mlw/compile.ml
src/mlw/compile.ml
+101
-315
src/mlw/compile.mli
src/mlw/compile.mli
+0
-8
src/mlw/cprinter.ml
src/mlw/cprinter.ml
+1
-1
src/mlw/mltree.ml
src/mlw/mltree.ml
+229
-0
src/mlw/ocaml_printer.ml
src/mlw/ocaml_printer.ml
+0
-1
src/tools/why3extract.ml
src/tools/why3extract.ml
+2
-2
tests/test-extraction/main.ml
tests/test-extraction/main.ml
+1
-1
No files found.
src/mlw/compile.ml
View file @
332f8a72
This diff is collapsed.
Click to expand it.
src/mlw/compile.mli
View file @
332f8a72
...
...
@@ -9,18 +9,10 @@
(* *)
(********************************************************************)
open
Ident
val
clean_name
:
string
->
string
val
module_name
:
?
fname
:
string
->
string
list
->
string
->
string
module
ML
:
sig
val
get_decl_name
:
Mltree
.
decl
->
ident
list
val
iter_deps
:
(
Ident
.
ident
->
unit
)
->
Mltree
.
decl
->
unit
end
module
Translate
:
sig
val
module_
:
Pmodule
.
pmodule
->
Mltree
.
pmodule
...
...
src/mlw/cprinter.ml
View file @
332f8a72
...
...
@@ -1008,7 +1008,7 @@ module MLToC = struct
let
translate_decl
(
info
:
info
)
(
d
:
Mltree
.
decl
)
:
C
.
definition
option
=
let
decide_print
id
=
query_syntax
info
.
syntax
id
=
None
in
match
Compile
.
ML
.
get_decl_name
d
with
match
Mltree
.
get_decl_name
d
with
|
[
id
]
when
decide_print
id
->
if
debug
then
Format
.
printf
"print %s@."
id
.
id_string
;
translate_decl
info
d
...
...
src/mlw/mltree.ml
View file @
332f8a72
...
...
@@ -121,3 +121,232 @@ type pmodule = {
mod_decl
:
decl
list
;
(* module declarations *)
mod_known
:
known_map
;
(* known identifiers *)
}
let
rec
get_decl_name
=
function
|
Dtype
itdefl
->
let
add_id
=
function
(* add name of constructors and projections *)
|
Some
(
Ddata
l
)
->
List
.
map
(
fun
(
idc
,
_
)
->
idc
)
l
|
Some
(
Drecord
l
)
->
List
.
map
(
fun
(
_
,
idp
,
_
)
->
idp
)
l
|
_
->
[]
in
let
add_td_ids
{
its_name
=
id
;
its_def
=
def
}
=
id
::
(
add_id
def
)
in
List
.
flatten
(
List
.
map
add_td_ids
itdefl
)
|
Dlet
(
Lrec
rdef
)
->
List
.
map
(
fun
{
rec_sym
=
rs
}
->
rs
.
rs_name
)
rdef
|
Dlet
(
Lvar
({
pv_vs
=
{
vs_name
=
id
}}
,
_
))
|
Dlet
(
Lsym
({
rs_name
=
id
}
,
_
,
_
,
_
))
|
Dlet
(
Lany
({
rs_name
=
id
}
,
_
,
_
))
|
Dexn
({
xs_name
=
id
}
,
_
)
->
[
id
]
|
Dmodule
(
_
,
dl
)
->
List
.
concat
(
List
.
map
get_decl_name
dl
)
let
rec
add_known_decl
decl
k_map
id
=
match
decl
with
|
Dmodule
(
_
,
dl
)
->
let
add_decl
k_map
d
=
let
idl
=
get_decl_name
d
in
List
.
fold_left
(
add_known_decl
d
)
k_map
idl
in
List
.
fold_left
add_decl
k_map
dl
|
_
->
Mid
.
add
id
decl
k_map
let
rec
iter_deps_ty
f
=
function
|
Tvar
_
->
()
|
Tapp
(
id
,
ty_l
)
->
f
id
;
List
.
iter
(
iter_deps_ty
f
)
ty_l
|
Ttuple
ty_l
->
List
.
iter
(
iter_deps_ty
f
)
ty_l
let
iter_deps_typedef
f
=
function
|
Ddata
constrl
->
List
.
iter
(
fun
(
_
,
tyl
)
->
List
.
iter
(
iter_deps_ty
f
)
tyl
)
constrl
|
Drecord
pjl
->
List
.
iter
(
fun
(
_
,
_
,
ty
)
->
iter_deps_ty
f
ty
)
pjl
|
Dalias
ty
->
iter_deps_ty
f
ty
|
Drange
_
|
Dfloat
_
->
()
let
iter_deps_its_defn
f
its_d
=
Opt
.
iter
(
iter_deps_typedef
f
)
its_d
.
its_def
let
iter_deps_args
f
=
List
.
iter
(
fun
(
_
,
ty_arg
,
_
)
->
iter_deps_ty
f
ty_arg
)
let
rec
iter_deps_xbranch
f
(
xs
,
_
,
e
)
=
f
xs
.
xs_name
;
iter_deps_expr
f
e
and
iter_deps_pat_list
f
patl
=
List
.
iter
(
iter_deps_pat
f
)
patl
and
iter_deps_pat
f
=
function
|
Pwild
|
Pvar
_
->
()
|
Papp
(
ls
,
patl
)
->
f
ls
.
ls_name
;
iter_deps_pat_list
f
patl
|
Ptuple
patl
->
iter_deps_pat_list
f
patl
|
Por
(
p1
,
p2
)
->
iter_deps_pat
f
p1
;
iter_deps_pat
f
p2
|
Pas
(
p
,
_
)
->
iter_deps_pat
f
p
and
iter_deps_expr
f
e
=
match
e
.
e_node
with
|
Econst
_
|
Evar
_
|
Eabsurd
|
Ehole
->
()
|
Eapp
(
rs
,
exprl
)
->
f
rs
.
rs_name
;
List
.
iter
(
iter_deps_expr
f
)
exprl
|
Efun
(
args
,
e
)
->
List
.
iter
(
fun
(
_
,
ty_arg
,
_
)
->
iter_deps_ty
f
ty_arg
)
args
;
iter_deps_expr
f
e
|
Elet
(
Lvar
(
_
,
e1
)
,
e2
)
->
iter_deps_expr
f
e1
;
iter_deps_expr
f
e2
|
Elet
(
Lsym
(
_
,
ty_result
,
args
,
e1
)
,
e2
)
->
iter_deps_ty
f
ty_result
;
List
.
iter
(
fun
(
_
,
ty_arg
,
_
)
->
iter_deps_ty
f
ty_arg
)
args
;
iter_deps_expr
f
e1
;
iter_deps_expr
f
e2
|
Elet
(
Lany
(
_
,
ty_result
,
args
)
,
e2
)
->
iter_deps_ty
f
ty_result
;
List
.
iter
(
fun
(
_
,
ty_arg
,
_
)
->
iter_deps_ty
f
ty_arg
)
args
;
iter_deps_expr
f
e2
|
Elet
((
Lrec
rdef
)
,
e
)
->
List
.
iter
(
fun
{
rec_sym
=
rs
;
rec_args
=
args
;
rec_exp
=
e
;
rec_res
=
res
}
->
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
,
xl
)
->
iter_deps_expr
f
e
;
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
;
iter_deps_expr
f
e3
|
Eblock
exprl
->
List
.
iter
(
iter_deps_expr
f
)
exprl
|
Ewhile
(
e1
,
e2
)
->
iter_deps_expr
f
e1
;
iter_deps_expr
f
e2
|
Efor
(
_
,
_
,
_
,
_
,
e
)
->
iter_deps_expr
f
e
|
Eraise
(
xs
,
None
)
->
f
xs
.
xs_name
|
Eraise
(
xs
,
Some
e
)
->
f
xs
.
xs_name
;
iter_deps_expr
f
e
|
Eexn
(
_xs
,
None
,
e
)
->
(* FIXME? How come we never do binding here? *)
iter_deps_expr
f
e
|
Eexn
(
_xs
,
Some
ty
,
e
)
->
(* FIXME? How come we never do binding here? *)
iter_deps_ty
f
ty
;
iter_deps_expr
f
e
|
Eassign
assingl
->
List
.
iter
(
fun
(
_
,
rs
,
_
)
->
f
rs
.
rs_name
)
assingl
|
Eignore
e
->
iter_deps_expr
f
e
let
rec
iter_deps
f
=
function
|
Dtype
its_dl
->
List
.
iter
(
iter_deps_its_defn
f
)
its_dl
|
Dlet
(
Lsym
(
_rs
,
ty_result
,
args
,
e
))
->
iter_deps_ty
f
ty_result
;
iter_deps_args
f
args
;
iter_deps_expr
f
e
|
Dlet
(
Lany
(
_rs
,
ty_result
,
args
))
->
iter_deps_ty
f
ty_result
;
iter_deps_args
f
args
|
Dlet
(
Lrec
rdef
)
->
List
.
iter
(
fun
{
rec_sym
=
rs
;
rec_args
=
args
;
rec_exp
=
e
;
rec_res
=
res
}
->
f
rs
.
rs_name
;
iter_deps_args
f
args
;
iter_deps_expr
f
e
;
iter_deps_ty
f
res
)
rdef
|
Dlet
(
Lvar
(
_
,
e
))
->
iter_deps_expr
f
e
|
Dexn
(
_
,
None
)
->
()
|
Dexn
(
_
,
Some
ty
)
->
iter_deps_ty
f
ty
|
Dmodule
(
_
,
dl
)
->
List
.
iter
(
iter_deps
f
)
dl
let
ity_unit
=
I
Ity
.
ity_unit
let
ity_of_mask
ity
mask
=
let
mk_ty
acc
ty
=
function
MaskGhost
->
acc
|
_
->
ty
::
acc
in
match
ity
,
mask
with
|
_
,
MaskGhost
->
ity_unit
|
_
,
MaskVisible
->
ity
|
I
({
ity_node
=
Ityapp
({
its_ts
=
s
}
,
tl
,
_
)})
,
MaskTuple
m
when
is_ts_tuple
s
&&
List
.
length
tl
=
List
.
length
m
->
let
tl
=
List
.
fold_left2
mk_ty
[]
tl
m
in
I
(
ity_tuple
tl
)
|
_
->
ity
(* FIXME ? *)
let
mk_expr
e_node
e_ity
mask
e_effect
e_label
=
{
e_node
;
e_ity
=
ity_of_mask
e_ity
mask
;
e_effect
;
e_label
;
}
let
tunit
=
Ttuple
[]
let
is_unit
=
function
|
I
i
->
ity_equal
i
Ity
.
ity_unit
|
_
->
false
let
enope
=
Eblock
[]
let
mk_hole
=
mk_expr
Ehole
(
I
Ity
.
ity_unit
)
MaskVisible
Ity
.
eff_empty
Slab
.
empty
let
mk_var
id
ty
ghost
=
(
id
,
ty
,
ghost
)
let
mk_var_unit
=
mk_var
(
id_register
(
id_fresh
"_"
))
tunit
false
let
mk_its_defn
its_name
its_args
its_private
its_def
=
{
its_name
;
its_args
;
its_private
;
its_def
;
}
(* smart constructors *)
let
e_unit
=
mk_expr
enope
(
I
Ity
.
ity_unit
)
MaskVisible
Ity
.
eff_empty
Slab
.
empty
let
var_defn
pv
e
=
Lvar
(
pv
,
e
)
let
sym_defn
f
ty_res
args
e
=
Lsym
(
f
,
ty_res
,
args
,
e
)
let
e_let
ld
e
=
mk_expr
(
Elet
(
ld
,
e
))
let
e_app
rs
pvl
=
mk_expr
(
Eapp
(
rs
,
pvl
))
let
e_fun
args
e
=
mk_expr
(
Efun
(
args
,
e
))
let
e_ignore
e
=
if
is_unit
e
.
e_ity
then
e
else
mk_expr
(
Eignore
e
)
ity_unit
MaskVisible
e
.
e_effect
e
.
e_label
let
e_if
e1
e2
e3
=
mk_expr
(
Eif
(
e1
,
e2
,
e3
))
e2
.
e_ity
let
e_while
e1
e2
=
mk_expr
(
Ewhile
(
e1
,
e2
))
ity_unit
let
e_for
pv1
pv2
dir
pv3
e1
=
mk_expr
(
Efor
(
pv1
,
pv2
,
dir
,
pv3
,
e1
))
ity_unit
let
e_match
e
bl
xl
=
mk_expr
(
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 (Etry (e, true, xl))
*)
let
e_assign
al
ity
mask
eff
lbl
=
if
al
=
[]
then
e_unit
else
mk_expr
(
Eassign
al
)
ity
mask
eff
lbl
let
e_absurd
=
mk_expr
Eabsurd
let
e_seq
e1
e2
=
let
e
=
match
e1
.
e_node
,
e2
.
e_node
with
|
(
Eblock
[]
|
Ehole
)
,
e
|
e
,
(
Eblock
[]
|
Ehole
)
->
e
|
Eblock
e1
,
Eblock
e2
->
Eblock
(
e1
@
e2
)
|
_
,
Eblock
e2
->
Eblock
(
e1
::
e2
)
|
Eblock
e1
,
_
->
Eblock
(
e1
@
[
e2
])
|
_
->
Eblock
[
e1
;
e2
]
in
mk_expr
e
let
var_list_of_pv_list
pvl
=
let
mk_var
pv
=
mk_expr
(
Evar
pv
)
(
I
pv
.
pv_ity
)
MaskVisible
eff_empty
Slab
.
empty
in
List
.
map
mk_var
pvl
src/mlw/ocaml_printer.ml
View file @
332f8a72
...
...
@@ -41,7 +41,6 @@ type info = {
module
Print
=
struct
open
Mltree
open
Compile
.
ML
(* extraction labels *)
let
optional_arg
=
create_label
"ocaml:optional"
...
...
src/tools/why3extract.ml
View file @
332f8a72
...
...
@@ -146,7 +146,7 @@ let print_preludes =
let
print_mdecls
?
fname
m
mdecls
=
let
(
fg
,
pargs
,
pr
)
=
Pdriver
.
lookup_printer
opt_driver
in
let
test_decl_not_driver
decl
=
let
decl_name
=
M
L
.
get_decl_name
decl
in
let
decl_name
=
M
ltree
.
get_decl_name
decl
in
let
test_id_not_driver
id
=
Printer
.
query_syntax
pargs
.
Pdriver
.
syntax
id
=
None
in
List
.
exists
test_id_not_driver
decl_name
in
...
...
@@ -292,7 +292,7 @@ let rec visit ~recurs mm id =
if
not
(
Ident
.
Hid
.
mem
visited
id
)
then
begin
try
let
d
=
find_decl
mm
id
in
Ident
.
Hid
.
add
visited
id
()
;
if
recurs
then
M
L
.
iter_deps
(
visit
~
recurs
mm
)
d
;
if
recurs
then
M
ltree
.
iter_deps
(
visit
~
recurs
mm
)
d
;
toextract
:=
{
info_rec
=
recurs
;
info_id
=
id
}
::
!
toextract
with
Not_found
->
()
end
...
...
tests/test-extraction/main.ml
View file @
332f8a72
...
...
@@ -12,7 +12,7 @@ let () = assert (test_int () = b42)
let
()
=
assert
(
test_int63
()
=
b42
)
let
()
=
assert
(
test_ref
()
=
b42
)
let
()
=
assert
(
test_array63
()
=
b42
)
let
()
=
assert
(
test_partial2
()
=
b42
)
let
()
=
assert
(
test_partial2
=
b42
)
let
()
=
main
()
let
()
=
Format
.
printf
"OCaml extraction test successful@."
...
...
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