diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-25 18:02:27 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-25 18:02:27 +0200 |
| commit | 43732086e664ff1fe59617a673e82cab6464c5e1 (patch) | |
| tree | 464400e45215687469921b25660b71f4825cbb3d /lib/future.ml | |
| parent | 67b85b04d6d78d8e4bbec58eab4b0630abfcd67d (diff) | |
Future: memory optimization when forcing a chained pure computation
Kudos to PMP for spotting that!
Diffstat (limited to 'lib/future.ml')
| -rw-r--r-- | lib/future.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/future.ml b/lib/future.ml index 1f68061ef..b82948276 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -167,11 +167,12 @@ let transactify f x = let purify_future f x = if is_over x then f x else purify f x let compute x = purify_future (compute ~pure:false) x -let force x = purify_future (force ~pure:false) x +let force ~pure x = purify_future (force ~pure) x let chain ?(greedy=true) ~pure x f = let y = chain ~pure x f in - if is_over x && greedy then ignore(force y); + if is_over x && greedy then ignore(force ~pure y); y +let force x = force ~pure:false x let join kx = let v = force kx in |