Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
2214aa5f
Commit
2214aa5f
authored
Mar 17, 2010
by
Andrei Paskevich
Browse files
add the initial task parameter to fold_map, map, decl, and expr in Trans.
In the majority of cases, it is just None.
parent
a4e8c067
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/core/trans.ml
View file @
2214aa5f
...
...
@@ -96,11 +96,11 @@ let fold_l fn v =
let
rewind
=
List
.
fold_left
rewind
in
accum
memo_t
rewind
[
v
]
[]
let
fold_map
fn
v
=
conv_res
(
fold
fn
(
v
,
None
))
snd
let
fold_map_l
fn
v
=
conv_res
(
fold_l
fn
(
v
,
None
))
(
List
.
rev_map
snd
)
let
fold_map
fn
v
t
=
conv_res
(
fold
fn
(
v
,
t
))
snd
let
fold_map_l
fn
v
t
=
conv_res
(
fold_l
fn
(
v
,
t
))
(
List
.
rev_map
snd
)
let
map
fn
=
fold
(
fun
t1
t2
->
fn
t1
t2
)
None
let
map_l
fn
=
fold_l
(
fun
t1
t2
->
fn
t1
t2
)
None
let
map
fn
=
fold
(
fun
t1
t2
->
fn
t1
t2
)
let
map_l
fn
=
fold_l
(
fun
t1
t2
->
fn
t1
t2
)
let
decl
fn
=
let
memo_t
=
Hashtbl
.
create
63
in
...
...
@@ -134,6 +134,3 @@ let rewrite fnT fnF d = match d.d_node with
let
expr
fnT
fnF
=
decl
(
fun
d
->
[
rewrite
fnT
fnF
d
])
src/core/trans.mli
View file @
2214aa5f
...
...
@@ -42,17 +42,17 @@ val compose_l : task tlist -> 'a tlist -> 'a tlist
val
fold
:
(
task_hd
->
'
a
->
'
a
)
->
'
a
->
'
a
trans
val
fold_l
:
(
task_hd
->
'
a
->
'
a
list
)
->
'
a
->
'
a
tlist
val
fold_map
:
(
task_hd
->
'
a
*
task
->
(
'
a
*
task
)
)
->
'
a
->
task
trans
val
fold_map
:
(
task_hd
->
'
a
*
task
->
(
'
a
*
task
))
->
'
a
->
task
->
task
trans
val
fold_map_l
:
(
task_hd
->
'
a
*
task
->
(
'
a
*
task
)
list
)
->
'
a
->
task
tlist
val
fold_map_l
:
(
task_hd
->
'
a
*
task
->
(
'
a
*
task
)
list
)
->
'
a
->
task
->
task
tlist
val
map
:
(
task_hd
->
task
->
task
)
->
task
trans
val
map_l
:
(
task_hd
->
task
->
task
list
)
->
task
tlist
val
map
:
(
task_hd
->
task
->
task
)
->
task
->
task
trans
val
map_l
:
(
task_hd
->
task
->
task
list
)
->
task
->
task
tlist
val
decl
:
(
decl
->
decl
list
)
->
task
trans
val
decl_l
:
(
decl
->
decl
list
list
)
->
task
tlist
val
decl
:
(
decl
->
decl
list
)
->
task
->
task
trans
val
decl_l
:
(
decl
->
decl
list
list
)
->
task
->
task
tlist
val
expr
:
(
term
->
term
)
->
(
fmla
->
fmla
)
->
task
trans
val
expr
:
(
term
->
term
)
->
(
fmla
->
fmla
)
->
task
->
task
trans
src/transform/inlining.ml
View file @
2214aa5f
...
...
@@ -107,7 +107,7 @@ let fold isnotinlinedt isnotinlinedf task0 (env, task) =
env
,
add_decl
task
(
create_prop_decl
k
pr
(
replacep
env
f
))
let
t
~
isnotinlinedt
~
isnotinlinedf
=
Trans
.
fold_map
(
fold
isnotinlinedt
isnotinlinedf
)
empty_env
Trans
.
fold_map
(
fold
isnotinlinedt
isnotinlinedf
)
empty_env
None
let
all
()
=
t
~
isnotinlinedt
:
(
fun
_
->
false
)
~
isnotinlinedf
:
(
fun
_
->
false
)
...
...
src/transform/simplify_recursive_definition.ml
View file @
2214aa5f
...
...
@@ -128,6 +128,6 @@ let elt d =
|
Dind
_
->
[
d
]
(* TODO *)
|
Dprop
_
->
[
d
]
let
t
()
=
Trans
.
decl
elt
let
t
()
=
Trans
.
decl
elt
None
let
()
=
Driver
.
register_transform
"simplify_recursive_definition"
t
src/transform/split_conjunction.ml
View file @
2214aa5f
...
...
@@ -94,8 +94,8 @@ let split_pos1 = split_pos (fun acc x -> x::acc)
let
rec
split_pos2
acc
d
=
split_pos
split_neg2
acc
d
and
split_neg2
acc
d
=
split_neg
split_pos2
acc
d
let
split_pos
()
=
Trans
.
decl_l
(
elt
split_pos1
)
let
split_pos_neg
()
=
Trans
.
decl_l
(
elt
split_pos2
)
let
split_pos
()
=
Trans
.
decl_l
(
elt
split_pos1
)
None
let
split_pos_neg
()
=
Trans
.
decl_l
(
elt
split_pos2
)
None
let
()
=
Driver
.
register_transform_l
"split_goal_pos"
split_pos
let
()
=
Driver
.
register_transform_l
"split_goal_pos_neg"
split_pos_neg
Write
Preview
Supports
Markdown
0%
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!
Cancel
Please
register
or
sign in
to comment