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
120
Issues
120
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
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
c131576c
Commit
c131576c
authored
Feb 10, 2017
by
Mário Pereira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Code extraction (wip)
parent
14889667
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
99 additions
and
80 deletions
+99
-80
src/mlw/compile.ml
src/mlw/compile.ml
+60
-33
src/mlw/ocaml_printer.ml
src/mlw/ocaml_printer.ml
+39
-47
No files found.
src/mlw/compile.ml
View file @
c131576c
...
...
@@ -118,8 +118,7 @@ module ML = struct
|
Evar
of
pvsymbol
|
Eapp
of
rsymbol
*
expr
list
|
Efun
of
var
list
*
expr
|
Elet
of
pvsymbol
*
expr
*
expr
|
Eletrec
of
is_rec
*
(
rsymbol
*
var
list
*
expr
)
list
*
expr
|
Elet
of
let_def
*
expr
|
Eif
of
expr
*
expr
*
expr
|
Ecast
of
expr
*
ty
|
Eassign
of
(
pvsymbol
*
rsymbol
*
pvsymbol
)
list
...
...
@@ -134,6 +133,18 @@ module ML = struct
|
Etry
of
expr
*
(
exn
*
pvsymbol
option
*
expr
)
list
|
Eabsurd
and
let_def
=
|
Lvar
of
pvsymbol
*
expr
|
Lsym
of
rsymbol
*
var
list
*
expr
|
Lrec
of
rdef
list
and
rdef
=
{
rec_sym
:
rsymbol
;
(* exported *)
rec_rsym
:
rsymbol
;
(* internal *)
rec_args
:
var
list
;
rec_exp
:
expr
;
}
type
is_mutable
=
bool
type
typedef
=
...
...
@@ -150,24 +161,19 @@ module ML = struct
type
decl
=
(* TODO add support for the extraction of ocaml modules *)
|
Dtype
of
its_defn
list
|
Dlet
of
rsymbol
*
var
list
*
expr
|
Dletrec
of
rdef
list
|
Dlet
of
let_def
(* TODO add return type? *)
|
Dexn
of
xsymbol
*
ty
option
and
rdef
=
{
rec_sym
:
rsymbol
;
(* exported *)
rec_rsym
:
rsymbol
;
(* internal *)
rec_args
:
var
list
;
rec_exp
:
expr
;
}
(* type pmodule = { *)
(* } *)
let
mk_expr
e_node
e_ity
e_effect
=
{
e_node
=
e_node
;
e_ity
=
e_ity
;
e_effect
=
e_effect
}
(* smart constructors *)
let
ml_let
id
e1
e2
=
Elet
(
id
,
e1
,
e2
)
let
ml_let
_var
pv
e1
e2
=
Elet
(
Lvar
(
pv
,
e1
)
,
e2
)
let
tunit
=
Ttuple
[]
...
...
@@ -345,13 +351,15 @@ module Translate = struct
let
al
_
=
ML
.
mk_unit
in
filter2_ghost_params
pv_not_ghost
def
al
pvl
(* let rec let_defn *)
(* expressions *)
let
rec
expr
info
({
e_effect
=
eff
}
as
e
)
=
assert
(
not
eff
.
eff_ghost
);
match
e
.
e_node
with
|
Econst
c
->
let
c
=
match
c
with
Number
.
ConstInt
c
->
c
|
_
->
assert
false
in
ML
.
mk_expr
(
ML
.
Econst
c
)
(
ML
.
I
e
.
e_ity
)
eff
let
c
=
match
c
with
Number
.
ConstInt
c
->
c
|
_
->
assert
false
in
ML
.
mk_expr
(
ML
.
Econst
c
)
(
ML
.
I
e
.
e_ity
)
eff
|
Evar
pvs
->
ML
.
mk_expr
(
ML
.
Evar
pvs
)
(
ML
.
I
e
.
e_ity
)
eff
|
Elet
(
LDvar
(
pvs
,
e1
)
,
e2
)
when
is_underscore
pvs
&&
e_ghost
e2
->
...
...
@@ -359,10 +367,10 @@ module Translate = struct
|
Elet
(
LDvar
(
pvs
,
e1
)
,
e2
)
when
is_underscore
pvs
->
ML
.
mk_expr
(
ML
.
eseq
(
expr
info
e1
)
(
expr
info
e2
))
(
ML
.
I
e
.
e_ity
)
eff
|
Elet
(
LDvar
(
pvs
,
e1
)
,
e2
)
when
e_ghost
e1
->
let
ml_let
=
ML
.
ml_let
pvs
ML
.
mk_unit
(
expr
info
e2
)
in
ML
.
mk_expr
ml_let
(
ML
.
I
e
.
e_ity
)
eff
let
ml_let
=
ML
.
ml_let
_var
pvs
ML
.
mk_unit
(
expr
info
e2
)
in
ML
.
mk_expr
ml_let
(
ML
.
I
e
.
e_ity
)
eff
|
Elet
(
LDvar
(
pvs
,
e1
)
,
e2
)
->
let
ml_let
=
ML
.
ml_let
pvs
(
expr
info
e1
)
(
expr
info
e2
)
in
let
ml_let
=
ML
.
ml_let
_var
pvs
(
expr
info
e1
)
(
expr
info
e2
)
in
ML
.
mk_expr
ml_let
(
ML
.
I
e
.
e_ity
)
eff
|
Elet
(
LDsym
(
rs
,
{
c_node
=
Cfun
ef
;
c_cty
=
cty
})
,
ein
)
->
let
def
pv
=
pv_name
pv
,
ity
pv
.
pv_ity
,
pv
.
pv_ghost
in
...
...
@@ -370,21 +378,39 @@ module Translate = struct
let
args
=
filter2_ghost_params
pv_not_ghost
def
al
cty
.
cty_args
in
let
ef
=
expr
info
ef
in
let
ein
=
expr
info
ein
in
let
ml_letrec
=
ML
.
Elet
rec
(
false
,
[
rs
,
args
,
ef
]
,
ein
)
in
let
ml_letrec
=
ML
.
Elet
(
ML
.
Lsym
(
rs
,
args
,
ef
)
,
ein
)
in
ML
.
mk_expr
ml_letrec
(
ML
.
I
e
.
e_ity
)
eff
|
Elet
(
LDsym
(
rsf
,
{
c_node
=
Capp
(
rs_app
,
pvl
);
c_cty
=
cty
})
,
ein
)
when
isconstructor
info
rs_app
->
let
eta_app
=
make_eta_expansion
rs_app
pvl
cty
in
let
ein
=
expr
info
ein
in
let
ml_letrec
=
ML
.
Elet
rec
(
false
,
[
rsf
,
[]
,
eta_app
]
,
ein
)
in
let
ml_letrec
=
ML
.
Elet
(
ML
.
Lsym
(
rsf
,
[]
,
eta_app
)
,
ein
)
in
ML
.
mk_expr
ml_letrec
(
ML
.
I
e
.
e_ity
)
e
.
e_effect
|
Elet
(
LDsym
(
rsf
,
{
c_node
=
Capp
(
rs_app
,
pvl
);
c_cty
=
cty
})
,
ein
)
->
let
pvl
=
app
info
rs_app
pvl
in
let
eapp
=
ML
.
mk_expr
(
ML
.
Eapp
(
rs_app
,
pvl
))
(
ML
.
C
cty
)
cty
.
cty_effect
in
let
ein
=
expr
info
ein
in
let
ml_letrec
=
ML
.
Eletrec
(
false
,
[
rsf
,
[]
,
eapp
]
,
ein
)
in
let
ml_letrec
=
ML
.
Elet
(
ML
.
Lsym
(
rsf
,
[]
,
eapp
)
,
ein
)
in
ML
.
mk_expr
ml_letrec
(
ML
.
I
e
.
e_ity
)
e
.
e_effect
|
Elet
(
LDrec
rdefl
,
ein
)
->
let
def
pv
=
pv_name
pv
,
ity
pv
.
pv_ity
,
pv
.
pv_ghost
in
let
al
pv
=
pv_name
pv
,
ML
.
tunit
,
false
in
let
ein
=
expr
info
ein
in
let
rdefl
=
List
.
map
(
fun
rdef
->
match
rdef
with
|
{
rec_sym
=
rs1
;
rec_rsym
=
rs2
;
rec_fun
=
{
c_node
=
Cfun
ef
;
c_cty
=
cty
}}
->
let
args
=
filter2_ghost_params
pv_not_ghost
def
al
cty
.
cty_args
in
let
ef
=
expr
info
ef
in
{
ML
.
rec_sym
=
rs1
;
ML
.
rec_rsym
=
rs2
;
ML
.
rec_args
=
args
;
ML
.
rec_exp
=
ef
}
|
_
->
assert
false
)
rdefl
in
let
ml_letrec
=
ML
.
Elet
(
ML
.
Lrec
rdefl
,
ein
)
in
ML
.
mk_expr
ml_letrec
(
ML
.
I
e
.
e_ity
)
e
.
e_effect
|
Eexec
({
c_node
=
Capp
(
rs
,
[]
)}
,
_
)
when
is_rs_tuple
rs
->
ML
.
mk_unit
...
...
@@ -398,22 +424,23 @@ module Translate = struct
let
al
pv
=
pv_name
pv
,
ML
.
tunit
,
false
in
let
args
=
filter2_ghost_params
pv_not_ghost
def
al
cty
.
cty_args
in
ML
.
mk_expr
(
ML
.
Efun
(
args
,
expr
info
e
))
(
ML
.
I
e
.
e_ity
)
eff
|
Eexec
({
c_node
=
Cany
}
,
_
)
->
assert
false
|
Eexec
({
c_node
=
Cany
}
,
_
)
->
(* Error message here *)
assert
false
|
Eabsurd
->
ML
.
mk_expr
ML
.
Eabsurd
(
ML
.
I
e
.
e_ity
)
eff
|
Ecase
(
e1
,
_
)
when
e_ghost
e1
->
ML
.
mk_unit
|
Ecase
(
e1
,
pl
)
->
let
e1
=
expr
info
e1
in
let
pl
=
List
.
map
(
ebranch
info
)
pl
in
ML
.
mk_expr
(
ML
.
Ematch
(
e1
,
pl
))
(
ML
.
I
e
.
e_ity
)
eff
let
e1
=
expr
info
e1
in
let
pl
=
List
.
map
(
ebranch
info
)
pl
in
ML
.
mk_expr
(
ML
.
Ematch
(
e1
,
pl
))
(
ML
.
I
e
.
e_ity
)
eff
|
Eassert
_
->
ML
.
mk_unit
ML
.
mk_unit
|
Eif
(
e1
,
e2
,
e3
)
->
let
e1
=
expr
info
e1
in
let
e2
=
expr
info
e2
in
let
e3
=
expr
info
e3
in
ML
.
mk_expr
(
ML
.
Eif
(
e1
,
e2
,
e3
))
(
ML
.
I
e
.
e_ity
)
eff
let
e1
=
expr
info
e1
in
let
e2
=
expr
info
e2
in
let
e3
=
expr
info
e3
in
ML
.
mk_expr
(
ML
.
Eif
(
e1
,
e2
,
e3
))
(
ML
.
I
e
.
e_ity
)
eff
|
Ewhile
(
e1
,
_
,
_
,
e2
)
->
let
e1
=
expr
info
e1
in
let
e2
=
expr
info
e2
in
...
...
@@ -446,7 +473,7 @@ module Translate = struct
let
itd_name
td
=
td
.
itd_its
.
its_ts
.
ts_name
(* type declarations/definitions *)
let
tdef
i
nfo
i
td
=
let
tdef
itd
=
let
s
=
itd
.
itd_its
in
let
ddata_constructs
=
(* point-free *)
List
.
map
(
fun
({
rs_cty
=
rsc
}
as
rs
)
->
...
...
@@ -494,7 +521,7 @@ module Translate = struct
let
def
=
fun
x
->
x
in
let
al
=
fun
x
->
x
in
filter2_ghost_params
p
def
al
(
args
cty
.
cty_args
)
in
[
ML
.
Dlet
(
rs
,
args_filter
,
expr
info
e
)]
[
ML
.
Dlet
(
ML
.
Lsym
(
rs
,
args_filter
,
expr
info
e
)
)]
|
PDlet
(
LDrec
rl
)
->
let
rec_def
=
List
.
map
(
fun
{
rec_fun
=
e
;
rec_sym
=
rs1
;
rec_rsym
=
rs2
}
->
...
...
@@ -507,13 +534,13 @@ module Translate = struct
{
ML
.
rec_sym
=
rs1
;
ML
.
rec_rsym
=
rs2
;
ML
.
rec_args
=
args_filter
;
ML
.
rec_exp
=
expr
info
e
})
rl
in
[
ML
.
Dlet
rec
rec_def
]
[
ML
.
Dlet
(
ML
.
Lrec
rec_def
)
]
|
PDlet
(
LDsym
_
)
|
PDpure
|
PDlet
(
LDvar
(
_
,
_
))
->
[]
|
PDtype
itl
->
[
ML
.
Dtype
(
List
.
map
(
tdef
info
)
itl
)]
[
ML
.
Dtype
(
List
.
map
tdef
itl
)]
|
PDexn
xs
->
if
ity_equal
xs
.
xs_ity
ity_unit
then
[
ML
.
Dexn
(
xs
,
None
)]
...
...
src/mlw/ocaml_printer.ml
View file @
c131576c
...
...
@@ -59,6 +59,11 @@ module Print = struct
let
forget_var
(
id
,
_
,
_
)
=
forget_id
id
let
forget_vars
=
List
.
iter
forget_var
let
forget_let_defn
=
function
|
Lvar
(
v
,_
)
->
forget_pv
v
|
Lsym
(
s
,_,_
)
->
forget_rs
s
|
Lrec
rdl
->
List
.
iter
(
fun
fd
->
forget_rs
fd
.
rec_sym
)
rdl
let
rec
forget_pat
=
function
|
Pwild
->
()
|
Pident
id
->
forget_id
id
...
...
@@ -251,17 +256,43 @@ module Print = struct
fprintf
fmt
"@[<hov 2>%a %a@]"
print_ident
rs
.
rs_name
(
print_list
space
(
print_expr
info
))
tl
and
print_let_def
info
fmt
=
function
|
Lvar
(
pv
,
e
)
->
fprintf
fmt
"@[<hov 2>let %a =@ %a@]"
(
print_lident
info
)
(
pv_name
pv
)
(
print_expr
info
)
e
;
(* forget_id (pv_name pv) *)
|
Lsym
(
rs
,
args
,
ef
)
->
fprintf
fmt
"@[<hov 2>let %a %a@ =@ @[%a@]@]"
(
print_lident
info
)
rs
.
rs_name
(
print_list
space
(
print_vs_arg
info
))
args
(
print_expr
info
)
ef
;
forget_vars
args
|
Lrec
(
rdef
)
->
let
print_one
fst
fmt
=
function
|
{
rec_sym
=
rs1
;
rec_args
=
args
;
rec_exp
=
e
}
->
fprintf
fmt
"@[<hov 2>%s %a@ %a@ =@ %a@]"
(
if
fst
then
"let rec"
else
"and"
)
(
print_lident
info
)
rs1
.
rs_name
(
print_list
space
(
print_vs_arg
info
))
args
(
print_expr
info
)
e
;
forget_vars
args
;
forget_tvs
()
in
List
.
iter
(
fun
fd
->
Hrs
.
replace
ht_rs
fd
.
rec_rsym
fd
.
rec_sym
)
rdef
;
print_list_next
newline
print_one
fmt
rdef
;
List
.
iter
(
fun
fd
->
Hrs
.
remove
ht_rs
fd
.
rec_rsym
)
rdef
and
print_enode
info
fmt
=
function
|
Econst
c
->
let
n
=
Number
.
compute_int
c
in
fprintf
fmt
"(Z.of_string
\"
%s
\"
)"
(
BigInt
.
to_string
n
)
|
Evar
pvs
->
(
print_lident
info
)
fmt
(
pv_name
pvs
)
|
Elet
(
pv
,
e1
,
e2
)
->
fprintf
fmt
"@[
<hov 2>let %a =@ %a@] in@
\n
%a"
(
print_l
ident
info
)
(
pv_name
pv
)
(
print_expr
info
)
e
1
(
print_expr
info
)
e2
;
forget_
id
(
pv_name
pv
)
|
Elet
(
let_def
,
e
)
->
fprintf
fmt
"@[
%a@] in@
%a"
(
print_l
et_def
info
)
let_def
(
print_expr
info
)
e
;
forget_
let_defn
let_def
|
Eabsurd
->
fprintf
fmt
"assert false (* absurd *)"
|
Eapp
(
s
,
[]
)
when
rs_equal
s
rs_true
->
...
...
@@ -298,19 +329,6 @@ module Print = struct
|
Efun
(
varl
,
e
)
->
fprintf
fmt
"@[<hov 2>(fun %a ->@ %a)@]"
(
print_list
space
(
print_vs_arg
info
))
varl
(
print_expr
info
)
e
|
Eletrec
(
is_rec
,
[
rs
,
[]
,
ef
]
,
ein
)
->
fprintf
fmt
"@[<hov 2>let %s%a =@ @[%a@]@] in@ %a"
(
if
is_rec
then
"rec "
else
""
)
(
print_lident
info
)
rs
.
rs_name
(
print_expr
info
)
ef
(
print_expr
info
)
ein
|
Eletrec
(
is_rec
,
[
rs
,
args
,
ef
]
,
ein
)
->
fprintf
fmt
"@[<hov 2>let %s%a %a@ =@ @[%a@]@] in@ %a"
(
if
is_rec
then
"rec "
else
""
)
(
print_lident
info
)
rs
.
rs_name
(
print_list
space
(
print_vs_arg
info
))
args
(
print_expr
info
)
ef
(
print_expr
info
)
ein
|
Ewhile
(
e1
,
e2
)
->
fprintf
fmt
"@[<hov 2>while %a do@ %a@ done@]"
(
print_expr
info
)
e1
(
print_expr
info
)
e2
...
...
@@ -334,7 +352,6 @@ module Print = struct
|
Etry
_
->
(* TODO *)
assert
false
|
Enot
_
->
(* TODO *)
assert
false
|
Ebinop
_
->
(* TODO *)
assert
false
|
Eletrec
_
->
(* TODO *)
assert
false
|
Ecast
_
->
(* TODO *)
assert
false
|
Eassign
_
->
(* TODO *)
assert
false
...
...
@@ -380,34 +397,9 @@ module Print = struct
print_def
its
.
its_def
let
print_decl
info
fmt
=
function
|
Dlet
(
rs
,
[]
,
e
)
->
fprintf
fmt
"@[<hov 2>let %a =@ %a@]"
print_ident
rs
.
rs_name
(
print_expr
info
)
e
;
forget_tvs
()
;
fprintf
fmt
"@
\n
@
\n
"
|
Dlet
(
rs
,
pvl
,
e
)
->
fprintf
fmt
"@[<hov 2>let %a@ %a =@ %a@]"
(
print_lident
info
)
rs
.
rs_name
(
print_list
space
(
print_vs_arg
info
))
pvl
(
print_expr
info
)
e
;
forget_vars
pvl
;
forget_tvs
()
;
fprintf
fmt
"@
\n
@
\n
"
|
Dletrec
rdef
->
let
print_one
fst
fmt
=
function
|
{
rec_sym
=
rs1
;
rec_args
=
args
;
rec_exp
=
e
}
->
fprintf
fmt
"@[<hov 2>%s %a@ %a@ =@ %a@]"
(
if
fst
then
"let rec"
else
"and"
)
(
print_lident
info
)
rs1
.
rs_name
(
print_list
space
(
print_vs_arg
info
))
args
(
print_expr
info
)
e
;
forget_vars
args
;
forget_tvs
()
in
List
.
iter
(
fun
fd
->
Hrs
.
replace
ht_rs
fd
.
rec_rsym
fd
.
rec_sym
)
rdef
;
print_list_next
newline
print_one
fmt
rdef
;
List
.
iter
(
fun
fd
->
Hrs
.
remove
ht_rs
fd
.
rec_rsym
)
rdef
;
|
Dlet
(
ldef
)
->
print_let_def
info
fmt
ldef
;
forget_tvs
()
;
fprintf
fmt
"@
\n
@
\n
"
|
Dtype
dl
->
print_list
newline
(
print_type_decl
info
)
fmt
dl
;
...
...
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