Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
W
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Nils Fitinghoff
why3
Commits
8f5c6138
Commit
8f5c6138
authored
Nov 9, 2018
by
nilfit
Browse files
Options
Downloads
Patches
Plain Diff
remove outdated comments/TODOs
parent
d77f26b7
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/mlw/rust_printer.ml
+17
-44
17 additions, 44 deletions
src/mlw/rust_printer.ml
with
17 additions
and
44 deletions
src/mlw/rust_printer.ml
+
17
−
44
View file @
8f5c6138
...
...
@@ -26,8 +26,8 @@ module Rust = struct
type
pat
=
|
Pwild
(* _ *)
|
Pvar
of
ident
*
bool
(* mut?
vs
*)
(* TODO m
ut? ref? maybe we need to wrap all out vsymbols
*)
|
Pvar
of
ident
*
bool
(* mut?
id
*)
(* TODO m
ay need to be able to mark as ref too
*)
|
Pde_str
of
ident
*
rsymbol
list
*
pat
list
(* destructure struct *)
(* S { l1: p1, l2: p2; .. } rust *)
|
Pde_enum
of
lsymbol
*
pat
list
(* destructure enum *)
...
...
@@ -36,7 +36,6 @@ module Rust = struct
|
Ptuple
of
pat
list
(* (p1, p2, p3) *)
|
Por
of
pat
*
pat
(* p1 | p2 *)
|
Pat
of
vsymbol
*
pat
(* vs @ pat *)
(* TODO test @ in more situations *)
|
Pbox
of
pat
(* the `box` keyword (unstable) *)
type
var
=
ident
*
ty
(* ref? mut? *)
...
...
@@ -259,7 +258,9 @@ module Translate = struct
])
|
Por
(
p1
,
p2
)
->
Rust
.
Por
(
translate_pat
info
p1
,
translate_pat
info
p2
)
|
Pas
(
p
,
vs
)
->
Rust
.
Pat
(
vs
,
translate_pat
info
p
)
(* TODO pattern bindings are not allowed after @: l @ (a, b) *)
(* Pattern bindings are not allowed after @, e.g. s @ S {a}. This would
* alias s.a and a, so it is not allowed. This means not all extracted as
* patterns will pass compilation in Rust. *)
let
is_mapped_to_bigint
info
ity
=
match
ity
.
ity_node
with
...
...
@@ -322,7 +323,8 @@ module Translate = struct
|
I
{
ity_node
=
Ityapp
({
its_ts
=
ts
}
,_,_
)
}
->
ts
.
ts_name
|
_
->
assert
false
in
(
match
query_syntax
info
.
literal
id
with
|
Some
s
->
Rust
.
Econst
(
Some
s
,
n
)
(* TODO there can never be an Econst (None, ..) *)
|
Some
s
->
Rust
.
Econst
(
Some
s
,
n
)
(* TODO there can never be an Econst (None, ..), the option is not needed *)
|
None
->
raise
(
MissingSyntaxLiteral
id
.
id_string
))
(* there is no default, driver must make a decision about how to represent
literals *)
...
...
@@ -337,7 +339,7 @@ module Translate = struct
let
e''
=
{
e'
with
e_node
=
Eapp
(
rs
,
el
@
el2
)}
in
translate_expr
info
e''
|
e1
::
el'
->
Rust
.
Ecall
(
translate_expr
info
e1
,
List
.
map
(
translate_expr
info
)
el'
)
|
_
->
raise
(
TODO
(
"infix @ with "
^
|
_
->
raise
(
TODO
(
"infix @ with "
^
(* TODO this can only happen for el=[] now *)
string_of_int
(
List
.
length
el
)
^
" args"
)))
else
(
let
el
=
List
.
map
(
translate_expr
info
)
el
in
...
...
@@ -365,7 +367,6 @@ module Translate = struct
else
e
in
let
el
=
List
.
mapi
(
maybe_box
rs
)
el
in
Rust
.
Eenum
(
rs
,
el
)
(* FIXME seems to use the name of the type instead of the variant *)
|
rsl
->
let
maybe_box
(
rs
:
rsymbol
)
(
e
:
Rust
.
expr
)
=
if
Sid
.
contains
boxes
.
box_fields
rs
.
rs_name
then
box_expr
e
...
...
@@ -378,7 +379,7 @@ module Translate = struct
(* use rs_nargs to know when and where to split into multiple calls *)
let
nargs
=
(
try
Hrs
.
find
rs_nargs
rs
with
Not_found
->
raise
(
TODO
(
"rs_nargs not found "
^
rs
.
rs_name
.
id_string
)))
in
TODO
(
"rs_nargs not found "
^
rs
.
rs_name
.
id_string
^
". Should it be in a driver?"
)))
in
(* the second result signals that the last application is partial
* and how many args are not applied *)
let
rec
split_args
el
nargs
:
Rust
.
expr
list
list
*
int
option
=
...
...
@@ -428,7 +429,8 @@ module Translate = struct
|
Elet
(
Lvar
(
pv
,
e_var
)
,
e
)
->
(* If the type has some mutable component, make the variable mutable.
* This will result in variables being unnecessarily marked mutable. *)
(* TODO do some analysis on what will actually be mutated instead *)
(* TODO do some analysis on what will actually be mutated.
* May have to look for Eapp with write effects. *)
let
mut
=
not
pv
.
pv_ity
.
ity_pure
in
let
pat
=
Rust
.
Pvar
(
pv
.
pv_vs
.
vs_name
,
mut
)
in
Rust
.
Elet
(
pat
,
translate_expr
info
e_var
,
translate_expr
info
e
)
...
...
@@ -438,14 +440,14 @@ module Translate = struct
let
er
=
translate_expr
info
e_body
in
let
vr
=
translate_vars_closure
info
vars
in
let
e_after
=
translate_expr
info
e_after
in
let
pat
=
Rust
.
Pvar
(
rs
.
rs_name
,
false
)
in
(* TODO mutability *)
let
pat
=
Rust
.
Pvar
(
rs
.
rs_name
,
false
)
in
(* TODO mutability
?
*)
Rust
.
Elet
(
pat
,
Rust
.
Eclosure
(
vr
,
er
)
,
e_after
)
|
Elet
(
Lany
(
_
,
_
,
_
)
,
_
)
->
raise
(
TODO
"Elet(Lany)"
)
|
Elet
(
Lrec
_
,
_
)
->
raise
(
TODO
"Elet(Lrec)"
)
|
Eif
(
ei
,
et
,
ee
)
->
Rust
.
Eif
(
translate_expr
info
ei
,
translate_expr
info
et
,
translate_expr
info
ee
)
(* TODO special cases *)
(* TODO special cases
like if true
*)
|
Eassign
[(
rho
,
rs
,
e
)]
->
Rust
.
Eassign
(
rho
,
rs
,
translate_expr
info
e
)
|
Eassign
al
->
...
...
@@ -454,15 +456,13 @@ module Translate = struct
Rust
.
Eassign
(
rho
,
rs
,
translate_expr
info
e
)
in
Rust
.
Eblock
(
List
.
map
translate_assign
al
)
|
Ematch
(
e1
,
[(
p
,
e2
)]
,
[]
)
->
(* TODO is this always irrefutable? *)
Rust
.
Elet
(
translate_pat
info
p
,
translate_expr
info
e1
,
translate_expr
info
e2
)
|
Ematch
(
e
,
bl
,
[]
)
->
(* no exception branches -> normal Ematch *)
Rust
.
Ematch
(
translate_expr
info
e
,
List
.
map
(
translate_branch
info
)
bl
)
|
Ematch
(
e
,
bl
,
xl
)
->
raise
(
TODO
"Ematch+exn"
)
(* TODO in general: wrap exn branches in Error patterns and normal
* branches in Oks? *)
(* TODO wrap exn branches in Error patterns and normal branches in Oks *)
|
Eblock
el
->
Rust
.
Eblock
(
List
.
map
(
translate_expr
info
)
el
)
|
Ewhile
(
test
,
body
)
->
Rust
.
Ewhile
(
translate_expr
info
test
,
Rust
.
Eblock
[(
translate_expr
info
body
)])
...
...
@@ -538,11 +538,8 @@ module Translate = struct
|
Rust
.
Ewhile
(
t
,
b
)
->
map_and_union
[
t
;
b
]
|
Rust
.
Efor
(
i
,
r
,
b
)
->
map_and_union
[
r
;
b
]
(* FIXME what about i? *)
|
Rust
.
Erange_inc
(
l
,
h
)
->
map_and_union
[
l
;
h
]
|
Rust
.
Eclosure
(
vl
,
e
)
->
(* let sl = List.map (fun (_, t) -> discover_lts_tvs_ty t) vl in *)
(* leave the arg types to be inferred *)
let
s
=
discover_lts_tvs_expr
e
in
s
(* union_slt_stv_list (s::sl) *)
|
Rust
.
Eclosure
(
_
,
e
)
->
discover_lts_tvs_expr
e
|
Rust
.
Efn
((
_
,
args
,
_
,
e1
,
stv
,
slt
)
,
e2
)
->
(* TODO promote tvs from the fn args/body? *)
(* let sl = List.map (fun (_, t) -> discover_lts_tvs_ty t) args in *)
...
...
@@ -550,16 +547,6 @@ module Translate = struct
let
s2
=
discover_lts_tvs_expr
e2
in
s2
)
(* TODO in which places in the expr do we have to look?
* e_ity can have tvs
* e_effect.eff_spoils ?
* e_attrs is harmless
* e_node has to be expanded
** Econst no
** Evar pv.pv_ity can have tvs
** ...
* It is probably best to leave this and see which tvs actually get used
*)
let
rec
discover_lts_tvs_def
(
d
:
Rust
.
def
)
:
Slt
.
t
*
Stv
.
t
=
let
tvs_snd_ty
(
_
,
t
)
=
discover_lts_tvs_ty
t
in
...
...
@@ -569,13 +556,6 @@ module Translate = struct
let
ts
=
discover_lts_tvs_ty
t
in
let
vs
=
union_slt_stv_list
(
List
.
map
tvs_snd_ty
vl
)
in
union_slt_stv_list
[
es
;
ts
;
vs
;
(
lts
,
tvs
)]
(*
let e_stv = discover_lts_tvs_expr e in
let t_stv = discover_lts_tvs_ty t in
let v_stv = List.fold_left Stv.union Stv.empty
(List.map tvs_snd_ty vl) in
union_stv_list [e_stv; t_stv; v_stv; tvs]
*)
|
Rust
.
Dstatic
_
->
Slt
.
empty
,
Stv
.
empty
(* TODO make sure this is correct *)
|
Rust
.
Dtype
td
->
...
...
@@ -625,7 +605,6 @@ module Translate = struct
(* all constructors *)
Rust
.
Denum
(
List
.
map
translate_cons
csl
)
|
Drecord
fl
->
(* TODO do something with field-wise mutability *)
let
translate_field
(
_
,
id
,
t
)
=
let
t
=
translate_ty
info
t
in
let
t
=
if
Sid
.
contains
boxes
.
box_fields
id
then
box_ty
t
else
t
in
...
...
@@ -666,7 +645,6 @@ module Translate = struct
|
Tvar
_
->
[]
|
Tapp
(
id
,
tl
)
->
if
id_in_itl
id
then
[
id
]
else
List
.
flatten
(
List
.
map
find_itl_ids
tl
)
(* TODO stop if id is already boxed *)
|
Ttuple
tl
->
List
.
flatten
(
List
.
map
find_itl_ids
tl
)
in
let
itd_of_id
id
=
List
.
find
(
fun
itd
->
id_equal
id
itd
.
its_name
)
itl
in
...
...
@@ -694,7 +672,6 @@ module Translate = struct
(* TODO `type t` with no definition puts us in this case *)
|
None
->
(
Sid
.
empty
,
Sbe
.
empty
,
vn
,
false
)
(* raise (TODO "type def None def") *)
|
Some
d
->
(
match
d
with
|
Ddata
csl
->
...
...
@@ -753,7 +730,7 @@ module Translate = struct
let
vr
=
translate_vars
info
vars
in
let
arg_counts
=
List
.
length
vars
::
find_arg_counts
e
in
Hrs
.
add
rs_nargs
rs
arg_counts
;
(* TODO can the tvs be found from rs_cty? *)
(* TODO can the tvs be found from rs_cty
instead
? *)
let
slt
,
stv
=
discover_lts_tvs_def
(
Rust
.
Dfn
(
rs
,
vr
,
tr
,
er
,
Stv
.
empty
,
Slt
.
empty
))
in
[
Rust
.
Dfn
(
rs
,
vr
,
tr
,
er
,
stv
,
slt
)]
...
...
@@ -767,14 +744,12 @@ module Translate = struct
let
s
=
rs
.
rs_name
.
id_string
^
", _, ["
^
args
^
"]"
in
[
Rust
.
Dsyntax
(
"TODO Dlet(Lany "
^
s
^
")"
)]
(* raise (TODO ("Dlet(Lany " ^ s ^ ")")) *)
(* | Dlet _ -> raise (TODO "Dlet") *)
|
Dtype
itsl
->
let
bf
,
be
=
box_typedefs
itsl
boxes
.
box_fields
boxes
.
box_enum
in
boxes
.
box_fields
<-
bf
;
boxes
.
box_enum
<-
be
;
List
.
map
(
fun
its
->
Rust
.
Dtype
(
translate_its
info
its
))
itsl
|
Dexn
(
_
,
_
)
->
raise
(
TODO
"Dexn"
)
(* [Rust.Dsyntax ("[[TODO Dexn]]")] *)
|
Dmodule
(
s
,
dl
)
->
(* TODO dl can contain functor args *)
[
Rust
.
Dmodule
(
s
,
List
.
flatten
(
List
.
map
(
translate_decl
info
)
dl
))]
...
...
@@ -950,7 +925,6 @@ module Print = struct
|
Pwild
->
fprintf
fmt
"_"
|
Pvar
(
id
,
mut
)
->
fprintf
fmt
"%s%a"
(
if
mut
then
"mut "
else
""
)
(
print_lident
info
)
id
(* TODO ref are still not mut *)
|
Pde_str
(
id
,
rsl
,
pl
)
->
fprintf
fmt
"@[<hov 2>%a { %a }@]"
(
print_uident
info
)
id
(
print_list2
comma
colon
(
print_rs
info
)
(
print_pat
info
))
...
...
@@ -1081,7 +1055,6 @@ module Print = struct
let
rec
print_def
info
fmt
(
d
:
def
)
=
match
d
with
(* | Dfn (rs, args, res_ty, e, tvs, lts) -> *)
|
Dfn
fn
->
print_fn
info
fmt
fn
|
Dstatic
(
pv
,
e
)
->
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment