Skip to content
GitLab
Menu
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
edbc438b
Commit
edbc438b
authored
Dec 07, 2010
by
François Bobot
Browse files
whybench : memoization don't work??!!?? so precompute....
parent
87b2b7a3
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/bench/whybench.ml
View file @
edbc438b
...
...
@@ -313,20 +313,25 @@ let () =
let
fold_prob
acc
=
function
|
None
,
_
->
acc
|
Some
f
,
_
->
let
gen
env
task
=
let
fwhy
()
=
let
fname
,
cin
=
match
f
with
|
"-"
->
"stdin"
,
stdin
|
f
->
f
,
open_in
f
in
let
m
=
Env
.
read_channel
?
format
:!
opt_parser
env
fname
cin
in
close_in
cin
;
let
th
=
Mnm
.
bindings
m
in
let
map
(
name
,
th
)
=
name
,
Task
.
split_theory
th
None
task
in
let
fold
acc
(
n
,
l
)
=
List
.
rev_append
(
List
.
map
(
fun
v
->
(
n
,
v
))
l
)
acc
in
th
|>
List
.
map
map
|>
List
.
fold_left
fold
[]
in
Scheduler
.
do_why_sync
fwhy
()
in
let
env
=
env
in
let
task
=
!
opt_task
in
let
tlist
=
let
fname
,
cin
=
match
f
with
|
"-"
->
"stdin"
,
stdin
|
f
->
f
,
open_in
f
in
let
m
=
Env
.
read_channel
?
format
:!
opt_parser
env
fname
cin
in
close_in
cin
;
let
th
=
Mnm
.
bindings
m
in
let
map
(
name
,
th
)
=
name
,
Task
.
split_theory
th
None
task
in
let
fold
acc
(
n
,
l
)
=
List
.
rev_append
(
List
.
map
(
fun
v
->
(
n
,
v
))
l
)
acc
in
th
|>
List
.
map
map
|>
List
.
fold_left
fold
[]
in
(* let gen = Env.Wenv.memoize 3 (fun env -> *)
(* let memo = Trans.store (fun task -> gen env task) in *)
(* Trans.apply memo) in *)
let
gen
_
_
=
tlist
in
let
gen
env
task
=
Scheduler
.
do_why_sync
(
gen
env
)
task
in
{
B
.
ptask
=
gen
;
ptrans
=
transl
;
}
::
acc
in
...
...
src/core/env.ml
View file @
edbc438b
...
...
@@ -72,6 +72,7 @@ let find_theory env sl s =
let
env_tag
env
=
env
.
env_tag
module
Wenv
=
Hashweak
.
Make
(
struct
type
t
=
env
let
tag
=
env_tag
end
)
(** Parsers *)
...
...
src/core/env.mli
View file @
edbc438b
...
...
@@ -25,6 +25,8 @@ type env
val
env_tag
:
env
->
Hashweak
.
tag
module
Wenv
:
Hashweak
.
S
with
type
key
=
env
type
retrieve_theory
=
env
->
string
list
->
theory
Mnm
.
t
val
create_env
:
retrieve_theory
->
env
...
...
Write
Preview
Supports
Markdown
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