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
55897939
Commit
55897939
authored
Jan 26, 2017
by
Mário Pereira
Browse files
Code extraction (wip)
Partial applied constructors are eta-expanded
parent
0fe17d4d
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/mlw/compile.ml
View file @
55897939
...
...
@@ -203,6 +203,9 @@ module Translate = struct
open
Pmodule
(* for the type of modules *)
open
Pdecl
(* for the type of program declarations *)
(* useful predicates and transformations *)
let
pv_not_ghost
e
=
not
e
.
pv_ghost
(* types *)
let
rec
type_
ty
=
match
ty
.
ty_node
with
...
...
@@ -296,25 +299,37 @@ module Translate = struct
let
args
=
(* point-free *)
List
.
map
pvty
let
app
info
rs
pvl
=
let
isconstructor
()
=
match
Mid
.
find_opt
rs
.
rs_name
info
.
info_mo_known_map
with
|
Some
{
pd_node
=
PDtype
its
}
->
let
is_constructor
its
=
List
.
exists
(
rs_equal
rs
)
its
.
itd_constructors
in
List
.
exists
is_constructor
its
|
_
->
false
in
match
pvl
with
|
pvl
when
isconstructor
()
->
let
def
pv
=
ML
.
mk_expr
(
ML
.
Evar
pv
)
(
ML
.
I
pv
.
pv_ity
)
eff_empty
in
let
p
e
=
not
e
.
pv_ghost
in
filter_ghost_params
p
def
pvl
|
pvl
->
let
isconstructor
info
rs
=
match
Mid
.
find_opt
rs
.
rs_name
info
.
info_mo_known_map
with
|
Some
{
pd_node
=
PDtype
its
}
->
let
is_constructor
its
=
List
.
exists
(
rs_equal
rs
)
its
.
itd_constructors
in
List
.
exists
is_constructor
its
|
_
->
false
let
make_eta_expansion
rsc
pvl
cty_app
=
(* FIXME : effects and types of the expression in this situation *)
let
args_f
=
let
def
pv
=
pv_name
pv
,
ity
pv
.
pv_ity
,
pv
.
pv_ghost
in
filter_ghost_params
pv_not_ghost
def
cty_app
.
cty_args
in
let
args
=
let
def
pv
=
ML
.
mk_expr
(
ML
.
Evar
pv
)
(
ML
.
I
pv
.
pv_ity
)
eff_empty
in
let
args
=
filter_ghost_params
pv_not_ghost
def
pvl
in
let
extra_args
=
(* FIXME : ghost status in this extra arguments *)
List
.
map
def
cty_app
.
cty_args
in
args
@
extra_args
in
let
eapp
=
ML
.
mk_expr
(
ML
.
Eapp
(
rsc
,
args
))
(
ML
.
C
cty_app
)
cty_app
.
cty_effect
in
ML
.
mk_expr
(
ML
.
Efun
(
args_f
,
eapp
))
(
ML
.
C
cty_app
)
cty_app
.
cty_effect
let
app
info
rs
pvl
=
let
def
pv
=
ML
.
mk_expr
(
ML
.
Evar
pv
)
(
ML
.
I
pv
.
pv_ity
)
eff_empty
in
if
isconstructor
info
rs
then
filter_ghost_params
pv_not_ghost
def
pvl
else
let
al
_
=
ML
.
mk_unit
in
let
p
e
=
not
e
.
pv_ghost
in
filter2_ghost_params
p
def
al
pvl
filter2_ghost_params
pv_not_ghost
def
al
pvl
(* expressions *)
let
rec
expr
info
({
e_effect
=
eff
}
as
e
)
=
...
...
@@ -334,38 +349,38 @@ module Translate = struct
let
ml_let
=
ML
.
ml_let
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
p
pv
=
not
pv
.
pv_ghost
in
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
args
=
filter2_ghost_params
p
def
al
cty
.
cty_args
in
let
args
=
filter2_ghost_params
p
v_not_ghost
def
al
cty
.
cty_args
in
let
ef
=
expr
info
ef
in
let
ein
=
expr
info
ein
in
let
ml_letrec
=
ML
.
Eletrec
(
false
,
[
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
);
_
})
,
ein
)
->
let
p
pv
=
not
pv
.
pv_ghost
in
let
def
pv
=
ML
.
mk_expr
(
ML
.
Evar
pv
)
(
ML
.
I
pv
.
pv_ity
)
eff_empty
in
let
al
_
=
ML
.
mk_unit
in
let
args
=
filter2_ghost_params
p
def
al
pvl
in
|
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
.
Eletrec
(
false
,
[
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
,
args
))
(
ML
.
I
ein
.
e_ity
)
ein
.
e
_effect
in
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
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
|
Eexec
({
c_node
=
Capp
(
rs
,
_
)}
,
_
)
when
rs_ghost
rs
->
ML
.
mk_unit
|
Eexec
({
c_node
=
Capp
(
rs
,
pvl
)}
,
_
)
->
|
Eexec
({
c_node
=
Capp
(
rs
,
pvl
)
;
_
}
,
_
)
->
let
pvl
=
app
info
rs
pvl
in
ML
.
mk_expr
(
ML
.
Eapp
(
rs
,
pvl
))
(
ML
.
I
e
.
e_ity
)
eff
|
Eexec
({
c_node
=
Cfun
e
;
c_cty
=
cty
}
,
_
)
->
Format
.
printf
"Length of args:%d@
\n
"
(
List
.
length
cty
.
cty_args
);
let
p
pv
=
not
pv
.
pv_ghost
in
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
args
=
filter2_ghost_params
p
def
al
cty
.
cty_args
in
let
args
=
filter2_ghost_params
p
v_not_ghost
def
al
cty
.
cty_args
in
ML
.
mk_expr
(
ML
.
Efun
(
args
,
expr
info
e
))
(
ML
.
I
e
.
e_ity
)
eff
|
Eexec
_
->
assert
false
|
Eabsurd
->
...
...
@@ -406,7 +421,7 @@ module Translate = struct
let
ddata_constructs
=
(* point-free *)
List
.
map
(
fun
({
rs_cty
=
rsc
}
as
rs
)
->
rs
.
rs_name
,
let
args
=
List
.
filter
(
fun
x
->
not
x
.
pv
_ghost
)
rsc
.
cty_args
in
let
args
=
List
.
filter
pv_not
_ghost
rsc
.
cty_args
in
List
.
map
(
fun
{
pv_vs
=
vs
}
->
type_
vs
.
vs_ty
)
args
)
in
let
drecord_fields
({
rs_cty
=
rsc
}
as
rs
)
=
(* point-free *)
...
...
src/mlw/ocaml_printer.ml
View file @
55897939
...
...
@@ -198,9 +198,9 @@ module Print = struct
|
_
->
false
in
match
extract_op
rs
.
rs_name
,
pvl
with
|
Some
o
,
[
t
1
;
t
2
]
->
fprintf
fmt
"@[<hov 1>%a %s %a@]"
(
print_expr
info
)
t
1
o
(
print_expr
info
)
t
2
|
Some
o
,
[
e
1
;
e
2
]
->
fprintf
fmt
"@[<hov 1>%a %s %a@]"
(
print_expr
info
)
e
1
o
(
print_expr
info
)
e
2
|
_
,
[]
->
print_ident
fmt
rs
.
rs_name
|
_
,
[
t1
]
when
isfield
->
...
...
@@ -214,7 +214,6 @@ module Print = struct
let
rec
print_list2
sep
sep_m
print1
print2
fmt
(
l1
,
l2
)
=
match
l1
,
l2
with
|
x1
::
r1
,
x2
::
r2
->
printf
"x1:%a@
\n
"
print_ident
x1
.
rs_name
;
print1
fmt
x1
;
sep_m
fmt
()
;
print2
fmt
x2
;
sep
fmt
()
;
print_list2
sep
sep_m
print1
print2
fmt
(
r1
,
r2
)
|
_
->
()
...
...
@@ -222,7 +221,7 @@ module Print = struct
let
print_rs
info
fmt
rs
=
fprintf
fmt
"%a"
(
print_lident
info
)
rs
.
rs_name
in
fprintf
fmt
"@[<hov 2>{ %a
}@]"
fprintf
fmt
"@[<hov 2>{ %a}@]"
(
print_list2
semi
equal
(
print_rs
info
)
(
print_expr
info
))
(
pjl
,
tl
)
|
_
,
tl
->
fprintf
fmt
"@[<hov 2>%a %a@]"
...
...
@@ -234,21 +233,26 @@ module Print = struct
|
Evar
pvs
->
(
print_lident
info
)
fmt
(
pv_name
pvs
)
|
Elet
(
pv
,
e1
,
e2
)
->
fprintf
fmt
"@[<hov 2>let %a =@ @[%a@]@] in@ %a"
(
print_lident
info
)
(
pv_name
pv
)
(
print_expr
info
)
e1
(
print_expr
info
)
e2
fprintf
fmt
"@[<hov 2>let %a =@ %a@] in@
\n
%a"
(
print_lident
info
)
(
pv_name
pv
)
(
print_expr
info
)
e1
(
print_expr
info
)
e2
|
Eabsurd
->
fprintf
fmt
"assert false (* absurd *)"
|
Eapp
(
s
,
[]
)
when
rs_equal
s
rs_true
->
fprintf
fmt
"true"
|
Eapp
(
s
,
[]
)
when
rs_equal
s
rs_false
->
fprintf
fmt
"false"
fprintf
fmt
"false"
|
Eapp
(
s
,
[
e1
;
e2
])
when
rs_equal
s
rs_func_app
->
fprintf
fmt
"@[<hov 1>%a %a@]"
(
print_expr
info
)
e1
(
print_expr
info
)
e2
|
Eapp
(
s
,
pvl
)
->
print_apply
info
fmt
s
pvl
|
Ematch
(
e
,
pl
)
->
fprintf
fmt
"@[begin match @[%a@] with@
\n
@[<hov>%a@] end@]"
(
print_expr
info
)
e
(
print_list
newline
(
print_branch
info
))
pl
|
Eassign
[(
rs
,
pv
)]
->
fprintf
fmt
"%a <-@ %a"
print_ident
rs
.
rs_name
print_ident
(
pv_name
pv
)
fprintf
fmt
"%a <-@ %a"
print_ident
rs
.
rs_name
print_ident
(
pv_name
pv
)
|
Eif
(
e1
,
e2
,
e3
)
->
fprintf
fmt
"@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]"
...
...
@@ -261,7 +265,6 @@ module Print = struct
fprintf
fmt
"@[<hv>begin@;<1 2>@[%a@]@ end@]"
(
print_list
semi
(
print_expr
info
))
el
|
Efun
(
varl
,
e
)
->
printf
"list length:%d@
\n
"
(
List
.
length
varl
);
fprintf
fmt
"@[<hov 2>(fun %a ->@ %a)@]"
(
print_list
space
print_vs_arg
)
varl
(
print_expr
info
)
e
|
Eletrec
(
is_rec
,
[
rs
,
[]
,
ef
]
,
ein
)
->
...
...
tests/test_extraction_mario.mlw
View file @
55897939
...
...
@@ -83,10 +83,16 @@ module M
be careful with side-effects
"let c = Cons e in" should be translated to
"let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml
Mário: I think A-normal form takes care of the side-effects problem
*)
let constructor1 () =
let x = Cons in
x 42
*)
let foofoo (x: int) : int =
let ghost y = x + 1 in
x
let test (x: int) : int =
let y =
...
...
@@ -133,10 +139,25 @@ module M
partial 42
let test_local (x: int) : int =
let fact (x: int) (y: int): int = x + y
in
let fact (x: int) (y: int): int = x + y in
fact x 42
let test_lets (x: int) : int =
let y = x in
let z = y + 1 in
let yxz = y * x * z in
let xzy = x + z + y in
let res = yxz - xzy in
res
let test_partial2 (x: int) : int =
let sum : int -> int -> int = fun x y -> x + y in
let incr_a (a: int) = sum a in
incr_a x x
let constr_partial (x: int) : list int =
let x = Cons 42 in
x Nil
(* let filter_record (c: cursor 'a) : int = *)
(* match c with *)
...
...
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