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
0f417be4
Commit
0f417be4
authored
Sep 19, 2011
by
Andrei Paskevich
Browse files
don't break the chain at Trans.goal and Trans.add_decls
parent
214b1af1
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/core/trans.ml
View file @
0f417be4
...
...
@@ -115,16 +115,16 @@ let apply_to_goal fn d = match d.d_node with
|
_
->
assert
false
let
gen_goal
add
fn
=
let
fn
=
Wdecl
.
memoize
5
(
apply_to_goal
fn
)
in
function
let
fn
=
Wdecl
.
memoize
5
(
apply_to_goal
fn
)
in
store
(
function
|
Some
{
task_decl
=
{
td_node
=
Decl
d
};
task_prev
=
prev
}
->
List
.
fold_left
add
prev
(
fn
d
)
|
_
->
assert
false
|
_
->
assert
false
)
let
gen_goal_l
add
fn
=
let
fn
=
Wdecl
.
memoize
5
(
apply_to_goal
fn
)
in
function
let
fn
=
Wdecl
.
memoize
5
(
apply_to_goal
fn
)
in
store
(
function
|
Some
{
task_decl
=
{
td_node
=
Decl
d
};
task_prev
=
prev
}
->
List
.
map
(
List
.
fold_left
add
prev
)
(
fn
d
)
|
_
->
assert
false
|
_
->
assert
false
)
let
goal
=
gen_goal
add_decl
let
goal_l
=
gen_goal_l
add_decl
...
...
@@ -134,10 +134,10 @@ let tgoal_l = gen_goal_l add_tdecl
let
rewrite
fn
=
decl
(
fun
d
->
[
decl_map
fn
d
])
let
rewriteTF
fnT
fnF
=
rewrite
(
TermTF
.
t_select
fnT
fnF
)
let
gen_add_decl
add
decls
=
function
let
gen_add_decl
add
decls
=
store
(
function
|
Some
{
task_decl
=
{
td_node
=
Decl
d
};
task_prev
=
prev
}
->
add_decl
(
List
.
fold_left
add
prev
decls
)
d
|
_
->
assert
false
|
_
->
assert
false
)
let
add_decls
=
gen_add_decl
add_decl
let
add_tdecls
=
gen_add_decl
add_tdecl
...
...
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