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
122
Issues
122
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
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
c9b80a74
Commit
c9b80a74
authored
Jul 19, 2017
by
Mário Pereira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Compile: cosmetic
parent
45a76d04
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
17 additions
and
28 deletions
+17
-28
src/mlw/compile.ml
src/mlw/compile.ml
+17
-28
No files found.
src/mlw/compile.ml
View file @
c9b80a74
...
...
@@ -233,7 +233,7 @@ module Translate = struct
(* remove ghost components from tuple, using mask *)
let
visible_of_mask
m
sl
=
match
m
with
|
MaskGhost
->
assert
false
(* FIXME *)
|
MaskGhost
->
assert
false
(* FIXME
?
*)
|
MaskVisible
->
sl
|
MaskTuple
ml
->
let
add_ity
acc
m
ity
=
if
mask_ghost
m
then
acc
else
ity
::
acc
in
...
...
@@ -299,19 +299,17 @@ module Translate = struct
(* individual types *)
let
mlty_of_ity
mask
t
=
let
rec
loop
t
=
match
t
.
ity_node
with
|
_
when
mask_ghost
mask
->
ML
.
tunit
|
Ityvar
(
tvs
,
_
)
->
Mltree
.
Tvar
tvs
|
Ityapp
({
its_ts
=
ts
}
,
itl
,
_
)
when
is_ts_tuple
ts
->
let
itl
=
List
.
rev
(
visible_of_mask
mask
itl
)
in
Mltree
.
Ttuple
(
List
.
map
loop
itl
)
|
Ityapp
({
its_ts
=
ts
}
,
itl
,
_
)
->
let
itl
=
List
.
rev
(
visible_of_mask
mask
itl
)
in
Mltree
.
Tapp
(
ts
.
ts_name
,
List
.
map
loop
itl
)
|
Ityreg
{
reg_its
=
its
;
reg_args
=
args
}
->
let
args
=
List
.
map
loop
args
in
Mltree
.
Tapp
(
its
.
its_ts
.
ts_name
,
args
)
in
|
_
when
mask_ghost
mask
->
ML
.
tunit
|
Ityvar
(
tvs
,
_
)
->
Mltree
.
Tvar
tvs
|
Ityapp
({
its_ts
=
ts
}
,
itl
,
_
)
when
is_ts_tuple
ts
->
let
itl
=
List
.
rev
(
visible_of_mask
mask
itl
)
in
Mltree
.
Ttuple
(
List
.
map
loop
itl
)
|
Ityapp
({
its_ts
=
ts
}
,
itl
,
_
)
->
Mltree
.
Tapp
(
ts
.
ts_name
,
List
.
map
loop
itl
)
|
Ityreg
{
reg_its
=
its
;
reg_args
=
args
}
->
let
args
=
List
.
map
loop
args
in
Mltree
.
Tapp
(
its
.
its_ts
.
ts_name
,
args
)
in
loop
t
let
pvty
pv
=
...
...
@@ -625,12 +623,9 @@ module Translate = struct
(* assert false (\*TODO*\) *)
and
ebranch
info
({
pp_pat
=
p
;
pp_mask
=
m
}
,
e
)
=
(* If the [case] expression is not ghost but there is (at least) one ghost
branch, then it must be the case that this is an effectful [case],
i.e., at least one of the non-ghost branches is effectful. In extract
code, the onlye sound meaning for this [case] expression is to keep for
each branch the effectul sub-expression. This is similar to the case
of a [let x = e1 in e2] where [x] is a ghost [pvsymbol] *)
(* if the [case] expression is not ghost but there is (at least) one ghost
branch, then it must be the case that all the branches return [unit]
and at least one of the non-ghost branches is effectful *)
if
e
.
e_effect
.
eff_ghost
then
(
pat
m
p
,
ML
.
mk_unit
)
else
(
pat
m
p
,
expr
info
e
)
...
...
@@ -683,7 +678,7 @@ module Translate = struct
let
rec
fun_expr_of_mask
mask
e
=
let
open
Mltree
in
let
mk_e
e_node
=
{
e
with
e_node
=
e_node
}
in
(* assert (mask <> MaskGhost); *)
assert
(
mask
<>
MaskGhost
);
match
e
.
e_node
with
|
Econst
_
|
Evar
_
|
Efun
_
|
Eassign
_
|
Ewhile
_
|
Efor
_
|
Eraise
_
|
Eexn
_
|
Eabsurd
|
Ehole
->
e
...
...
@@ -725,15 +720,9 @@ module Translate = struct
(* raise (ExtractionVal _rs) *)
|
PDlet
(
LDsym
(
_
,
{
c_node
=
Cfun
e
}))
when
is_val
e
.
e_node
->
[]
|
PDlet
(
LDsym
({
rs_cty
=
cty
}
as
rs
,
{
c_node
=
Cfun
e
;
c_cty
=
_c_cty
}))
->
|
PDlet
(
LDsym
({
rs_cty
=
cty
}
as
rs
,
{
c_node
=
Cfun
e
}))
->
let
args
=
params
cty
.
cty_args
in
(* let open Format in *)
(* let pr_mask fmt = function *)
(* | MaskVisible -> fprintf fmt "Visible@." *)
(* | MaskTuple _ -> fprintf fmt "Tuple@." *)
(* | MaskGhost -> fprintf fmt "Ghost@." in *)
let
res
=
mlty_of_ity
cty
.
cty_mask
cty
.
cty_result
in
(* eprintf "Mask of %s:%a@." rs.rs_name.id_string pr_mask c_cty.cty_mask; *)
let
e
=
expr
info
e
in
let
e
=
fun_expr_of_mask
cty
.
cty_mask
e
in
[
Mltree
.
Dlet
(
Mltree
.
Lsym
(
rs
,
res
,
args
,
e
))]
...
...
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