Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
97790713
Commit
97790713
authored
Dec 26, 2016
by
Mário Pereira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Code extraction: extraction of type declarations (wip)
parent
0211e117
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
110 additions
and
27 deletions
+110
-27
.mailmap
.mailmap
+3
-3
src/mlw/compile.ml
src/mlw/compile.ml
+46
-4
src/mlw/ocaml_printer.ml
src/mlw/ocaml_printer.ml
+51
-20
tests/test_extraction_mario.mlw
tests/test_extraction_mario.mlw
+10
-0
No files found.
.mailmap
View file @
97790713
...
...
@@ -25,9 +25,9 @@ Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <thi-minh-tuyen.nguyen@inria.fr>
Andrei Paskevich <andrei@lri.fr> <andrei@tertium.org>
Mário
José Parreira
Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
Mário
José Parreira
Pereira <mpereira@lri.fr> <parreira@lri.fr>
Mário
José Parreira
Pereira <mpereira@lri.fr> <mpereira@lri.fr>
Mário Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
Mário Pereira <mpereira@lri.fr> <parreira@lri.fr>
Mário Pereira <mpereira@lri.fr> <mpereira@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@atafat-desktop.(none)>
Piotr Trojanek <piotr.trojanek@altran.com> <piotr.trojanek@gmail.com>
src/mlw/compile.ml
View file @
97790713
...
...
@@ -122,7 +122,7 @@ module ML = struct
(* TODO add return type? *)
|
Dexn
of
ident
*
ty
option
let
create
_expr
e_node
e_ity
e_effect
=
let
mk
_expr
e_node
e_ity
e_effect
=
{
e_node
=
e_node
;
e_ity
=
e_ity
;
e_effect
=
e_effect
}
(* TODO add here some smart constructors for ML expressions *)
...
...
@@ -155,8 +155,20 @@ module Translate = struct
let
vsty
vs
=
vs
.
vs_name
,
type_
vs
.
vs_ty
let
type_args
=
(* point-free *)
List
.
map
(
fun
x
->
x
.
tv_name
)
(** programs *)
(* individual types *)
let
rec
ity
t
=
match
t
.
ity_node
with
|
Ityvar
({
tv_name
=
tv
}
,
_
)
->
ML
.
Tvar
tv
|
Ityapp
({
its_ts
=
ts
}
,
itl
,
_
)
->
ML
.
Tapp
(
ts
.
ts_name
,
List
.
map
ity
itl
)
|
_
->
(* TODO *)
assert
false
let
pv_name
pv
=
pv
.
pv_vs
.
vs_name
let
pvty
pv
=
...
...
@@ -172,11 +184,39 @@ module Translate = struct
match
e
.
e_node
with
|
Evar
pvs
->
let
pv_id
=
pv_name
pvs
in
ML
.
create
_expr
(
ML
.
Eident
pv_id
)
e
.
e_ity
e
.
e_effect
ML
.
mk
_expr
(
ML
.
Eident
pv_id
)
e
.
e_ity
e
.
e_effect
|
Elet
(
LDvar
(
pvs
,
e1
)
,
e2
)
->
let
ml_let
=
ML
.
ml_let
(
pv_name
pvs
)
(
expr
e1
)
(
expr
e2
)
in
ML
.
create_expr
ml_let
e
.
e_ity
e
.
e_effect
|
_
->
assert
false
(* TODO *)
ML
.
mk_expr
ml_let
e
.
e_ity
e
.
e_effect
|
_
->
(* TODO *)
assert
false
let
its_args
ts
=
ts
.
its_ts
.
ts_args
let
itd_name
td
=
td
.
itd_its
.
its_ts
.
ts_name
let
ddata_constructs
=
(* point-free *)
List
.
map
(
fun
({
rs_cty
=
rsc
}
as
rs
)
->
rs
.
rs_name
,
List
.
map
(
fun
{
pv_vs
=
pv
}
->
type_
pv
.
vs_ty
)
rsc
.
cty_args
)
(** Question pour Jean-Christophe et Andreï :
est-ce que vous pouriez m'expliquer le champ itd_fields,
utilisé dans une déclaration de type ? *)
(* type declarations/definitions *)
let
tdef
itd
=
let
s
=
itd
.
itd_its
in
let
id
=
itd_name
itd
in
let
args
=
its_args
s
in
begin
match
s
.
its_def
,
itd
.
itd_constructors
with
|
None
,
[]
->
(* let args = its_args s in *)
ML
.
Dtype
[
id
,
type_args
args
,
ML
.
Dabstract
]
|
None
,
cl
->
(* let args = its_args s in *)
ML
.
Dtype
[
id
,
type_args
args
,
ML
.
Ddata
(
ddata_constructs
cl
)]
|
Some
t
,
_
->
ML
.
Dtype
[
id
,
type_args
args
,
ML
.
Dalias
(
ity
t
)]
(* | _ -> (\* TODO *\) assert false *)
end
(* program declarations *)
let
pdecl
pd
=
...
...
@@ -198,6 +238,8 @@ module Translate = struct
[]
|
PDpure
->
[]
|
PDtype
itl
->
List
.
map
tdef
itl
|
_
->
(* TODO *)
assert
false
(* unit module declarations *)
...
...
src/mlw/ocaml_printer.ml
View file @
97790713
...
...
@@ -16,7 +16,6 @@ open Format
open
Pmodule
open
Theory
open
Ident
open
Printer
open
Pp
module
Print
=
struct
...
...
@@ -50,41 +49,42 @@ module Print = struct
let
print_tv
fmt
tv
=
fprintf
fmt
"'%s"
(
id_unique
aprinter
tv
)
(** Types *)
let
protect_on
b
s
=
if
b
then
"("
^^
s
^^
")"
else
s
let
star
fmt
()
=
fprintf
fmt
" *@ "
let
rec
print_ty
fmt
=
function
let
rec
print_ty
?
(
paren
=
false
)
fmt
=
function
|
Tvar
id
->
print_tv
fmt
id
|
Ttuple
[]
->
fprintf
fmt
"unit"
|
Ttuple
tl
->
fprintf
fmt
"%a"
(
print_list
star
print_ty
)
tl
fprintf
fmt
(
protect_on
paren
"%a"
)
(
print_list
star
(
print_ty
~
paren
:
false
)
)
tl
|
Tapp
(
ts
,
[]
)
->
print_ident
fmt
ts
|
Tapp
(
ts
,
[
ty
])
->
fprintf
fmt
"%a@ %a"
print_ty
ty
print_ident
ts
fprintf
fmt
(
protect_on
paren
"%a@ %a"
)
(
print_ty
~
paren
:
true
)
ty
print_ident
ts
|
Tapp
(
ts
,
tl
)
->
fprintf
fmt
"(%a)@ %a"
(
print_list
comma
print_ty
)
tl
fprintf
fmt
(
protect_on
paren
"(%a)@ %a"
)
(
print_list
comma
(
print_ty
~
paren
:
false
)
)
tl
print_ident
ts
let
print_vsty
fmt
(
v
,
ty
)
=
fprintf
fmt
"%a:@ %a"
print_ident
v
print_ty
ty
fprintf
fmt
"%a:@ %a"
print_ident
v
(
print_ty
~
paren
:
false
)
ty
let
print_tv_arg
=
print_tv
let
print_tv_args
fmt
=
function
|
[]
->
()
|
[
tv
]
->
fprintf
fmt
"%a@ "
print_tv_arg
tv
|
tvl
->
fprintf
fmt
"(%a)@ "
(
print_list
comma
print_tv_arg
)
tvl
let
print_vs_arg
fmt
vs
=
fprintf
fmt
"@[(%a)@]"
print_vsty
vs
let
rec
print_ty
fmt
=
function
|
Tvar
id
->
print_tv
fmt
id
|
Ttuple
[]
->
fprintf
fmt
"unit"
|
Ttuple
tl
->
fprintf
fmt
"%a"
(
print_list
star
print_ty
)
tl
|
Tapp
(
ts
,
[]
)
->
print_ident
fmt
ts
|
_
->
assert
false
(* TODO *)
let
print_path
=
print_list
dot
pp_print_string
(* point-free *)
...
...
@@ -106,11 +106,39 @@ module Print = struct
print_ident
id
print_expr
e1
print_expr
e2
|
_
->
assert
false
(* TODO *)
|
_
->
(* TODO *)
assert
false
and
print_expr
fmt
e
=
print_enode
fmt
e
.
e_node
let
print_type_decl
fmt
(
id
,
args
,
tydef
)
=
let
print_constr
fmt
(
id
,
constrs
)
=
match
constrs
with
|
[]
->
fprintf
fmt
"@[<hov 4>| %a@]"
print_ident
id
(* FIXME: first letter must be uppercase
-> print_uident *)
|
l
->
fprintf
fmt
"@[<hov 4>| %a of %a@]"
print_ident
id
(* FIXME: print_uident *)
(
print_list
star
(
print_ty
~
paren
:
false
))
l
in
let
print_def
fmt
=
function
|
Dabstract
->
()
|
Ddata
csl
->
fprintf
fmt
" =@
\n
%a"
(
print_list
newline
print_constr
)
csl
|
Dalias
ty
->
fprintf
fmt
" =@ %a"
(
print_ty
~
paren
:
false
)
ty
|
_
->
(* TODO *)
assert
false
in
fprintf
fmt
"@[<hov 2>%s %a%a%a@]"
(
if
true
then
"type"
else
"and"
)
(* FIXME: mutual recursive types *)
print_tv_args
args
print_ident
id
(* FIXME: first letter must be lowercase
-> print_lident *)
print_def
tydef
let
print_decl
fmt
=
function
|
Dlet
(
isrec
,
[
id
,
vl
,
e
])
->
fprintf
fmt
"@[<hov 2>%s %a@ %a =@ %a@]"
...
...
@@ -119,7 +147,10 @@ module Print = struct
(
print_list
space
print_vs_arg
)
vl
print_expr
e
;
fprintf
fmt
"@
\n
@
\n
"
|
_
->
assert
false
(* TODO *)
|
Dtype
dl
->
print_list
newline
print_type_decl
fmt
dl
;
fprintf
fmt
"@
\n
@
\n
"
|
_
->
(* TODO *)
assert
false
end
...
...
tests/test_extraction_mario.mlw
View file @
97790713
...
...
@@ -13,6 +13,16 @@ module M
= let y = x in
y
type t 'a 'b 'c 'd
type list 'a = Nil | Cons 'a (list 'a)
type btree 'a = E | N (btree 'a) 'a (btree 'a)
type ntree 'a = Empty | Node 'a (list 'a)
type list_int = list int
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