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
b013cab5
Commit
b013cab5
authored
Jan 23, 2017
by
Mário Pereira
Browse files
Code extraction (wip)
The creation of a new record is now properly printed into the OCaml syntax
parent
a53472b5
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/mlw/compile.ml
View file @
b013cab5
...
...
@@ -242,12 +242,12 @@ module Translate = struct
in
filter2_ghost_params_cps
l
(
fun
x
->
x
)
let
rec
filter_ghost_params_pat
=
function
|
MaskVisible
->
Format
.
printf
"visible@
\n
"
|
MaskGhost
->
Format
.
printf
"ghost@
\n
"
|
MaskTuple
l
->
Format
.
printf
"list@
\n
"
;
List
.
iter
(
filter_ghost_params_pat
)
l
(*
let rec filter_ghost_params_pat = function
*)
(*
| MaskVisible -> Format.printf "visible@\n"
*)
(*
| MaskGhost -> Format.printf "ghost@\n"
*)
(*
| MaskTuple l ->
*)
(*
Format.printf "list@\n";
*)
(*
List.iter (filter_ghost_params_pat) l
*)
let
rec
pat
p
=
match
p
.
pat_node
with
...
...
@@ -367,8 +367,8 @@ module Translate = struct
ML
.
mk_expr
(
ML
.
Eassign
[(
rs
,
pv
)])
(
ML
.
I
e
.
e_ity
)
eff
|
_
->
(* TODO *)
assert
false
and
ebranch
info
({
pp_pat
=
p
}
as
pp
,
e
)
=
(
filter_ghost_params_pat
pp
.
pp_mask
;
pat
p
,
expr
info
e
)
and
ebranch
info
({
pp_pat
=
p
}
,
e
)
=
(
pat
p
,
expr
info
e
)
let
its_args
ts
=
ts
.
its_ts
.
ts_args
let
itd_name
td
=
td
.
itd_its
.
its_ts
.
ts_name
...
...
@@ -450,6 +450,16 @@ module Translate = struct
let
module_
info
m
=
List
.
concat
(
List
.
map
(
mdecl
info
)
m
.
mod_units
)
end
(** Erasure operations related to ghost code *)
module
Erasure
=
struct
open
ML
end
(*
...
...
src/mlw/ocaml_printer.ml
View file @
b013cab5
...
...
@@ -22,6 +22,7 @@ open Ty
open
Theory
open
Pmodule
open
Stdlib
open
Pdecl
module
Print
=
struct
...
...
@@ -167,6 +168,14 @@ module Print = struct
let
pv_name
pv
=
pv
.
pv_vs
.
vs_name
let
get_record
info
rs
=
match
Mid
.
find_opt
rs
.
rs_name
info
.
info_mo_known_map
with
|
Some
{
pd_node
=
PDtype
itdl
}
->
let
itd
=
List
.
find
(
fun
{
itd_constructors
=
constr
}
->
List
.
exists
(
rs_equal
rs
)
constr
)
itdl
in
List
.
filter
(
fun
e
->
not
(
rs_ghost
e
))
itd
.
itd_fields
|
_
->
[]
let
rec
print_apply
info
fmt
rs
pvl
=
let
isfield
=
match
rs
.
rs_field
with
...
...
@@ -190,8 +199,24 @@ module Print = struct
|
_
,
[
t1
]
when
isfield
->
fprintf
fmt
"%a.%a"
(
print_expr
info
)
t1
print_ident
rs
.
rs_name
|
_
,
tl
when
isconstructor
()
->
fprintf
fmt
"@[<hov 2>%a (%a)@]"
print_ident
rs
.
rs_name
(
print_list
comma
(
print_expr
info
))
tl
let
pjl
=
get_record
info
rs
in
if
pjl
=
[]
then
fprintf
fmt
"@[<hov 2>%a (%a)@]"
print_ident
rs
.
rs_name
(
print_list
comma
(
print_expr
info
))
tl
else
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
)
|
_
->
()
in
let
print_rs
info
fmt
rs
=
fprintf
fmt
"%a"
(
print_lident
info
)
rs
.
rs_name
in
fprintf
fmt
"@[<hov 2>{ %a }@]"
(
print_list2
semi
equal
(
print_rs
info
)
(
print_expr
info
))
(
pjl
,
tl
)
|
_
,
tl
->
fprintf
fmt
"@[<hov 2>%a %a@]"
print_ident
rs
.
rs_name
(
print_list
space
(
print_expr
info
))
tl
...
...
tests/test_extraction_mario.mlw
View file @
b013cab5
...
...
@@ -31,6 +31,9 @@ module M
ghost mutable v : seq 'a;
}
let create_cursor (l: list int) (i i2: int) : cursor int =
{ collection = l; index = i; index2 = i2; v = empty }
use import ref.Ref
let update (c: cursor int) : int
...
...
@@ -118,6 +121,11 @@ module M
let _ = 42 in (* FIXME? print _ in OCaml *)
x
(* let filter_record (c: cursor 'a) : int = *)
(* match c with *)
(* | { collection = l; index = i; index2 = i2; v = v} -> i *)
(* end *)
end
(*
...
...
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