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
f6fbaaa4
Commit
f6fbaaa4
authored
Apr 23, 2010
by
Andrei Paskevich
Browse files
respect query_remove in Eliminate_definition
parent
f6150a86
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/transform/eliminate_definition.ml
View file @
f6fbaaa4
...
...
@@ -138,21 +138,22 @@ let add_ld kn task ls ld =
|
Fmla
f
->
add_pd
kn
task
ls
.
ls_name
.
id_long
ls
(
f_app
ls
tl
)
[]
f
let
add_ld
kn
task
(
ls
,
ld
)
=
match
ld
with
|
None
->
task
let
add_ld
q
kn
task
(
ls
,
ld
)
=
match
ld
with
|
None
->
task
|
Some
_
when
Driver
.
query_remove
q
ls
.
ls_name
->
task
|
Some
ld
->
add_ld
kn
task
ls
ld
let
add_ls
task
(
ls
,_
)
=
add_decl
task
(
create_logic_decl
[
ls
,
None
])
let
elim
t
task
=
match
t
.
task_decl
with
let
elim
q
t
task
=
match
t
.
task_decl
with
|
Decl
{
d_node
=
Dlogic
ll
}
->
let
task
=
List
.
fold_left
add_ls
task
ll
in
let
task
=
List
.
fold_left
(
add_ld
t
.
task_known
)
task
ll
in
let
task
=
List
.
fold_left
(
add_ld
q
t
.
task_known
)
task
ll
in
task
|
td
->
add_tdecl
task
td
let
elim
=
Register
.
store
(
fun
()
->
Trans
.
map
elim
None
)
let
elim
=
Register
.
store
_query
(
fun
q
->
Trans
.
map
(
elim
q
)
None
)
let
()
=
Register
.
register_transform
"eliminate_definition"
elim
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