[future] Use eager evaluation for chaining values.

The current future system is lazy when "chaining" (*) a resolved
future, which implies that chaining with a resolved future will produce
a non-resolved one.

This misfeature interacts badly with the "purification" optimization,
which in turn provokes a swarm of spurious state setting calls in real
use.

To solve this problem, we revert to the more natural semantics of
respecting the evaluation semantics when mapping over a future, indeed
respecting the previous resolution status.

This commit solves a kind of _critical_ bug in the current system,
with the particular bad path origination in `Future.split2` due to the
following accumulation of circumstances:

```
split2 x -> chain x (fun x -> fst x)

 =>

  let y = chain ~pure x (fun x -> fst x) in
  if is_over x && greedy then ignore(force ~pure y);
  y

=> [y <- Closure (fun x -> fst x)]

  ignore(force (Closure (fun x -> fst x)))

=>

  purify_future (force ~pure) (Closure (fun x -> fst x))

```
and then, the test in `purify_future` fails, triggering the
spurious state reset operation.

This problem was first noted at
https://sympa.inria.fr/sympa/arc/coqdev/2016-02/msg00081.html , and
seems related to https://coq.inria.fr/bugs/show_bug.cgi?id=5382

We fix the problem by making chaining eager, but other solutions would
be possible. Given that the main user of `chain` is `split2` which
does `snd/fst`, I recommend this solution.

The difference in calls to `unfreeze_state` is dramatic:
```
| File                                   | Freeze Calls After | Freeze Calls Before |
|----------------------------------------+--------------------+---------------------|
| theories/Init/Notations.v              |                  0 |                   0 |
| theories/Init/Logic.v                  |                 57 |                 614 |
| theories/Init/Datatypes.v              |                 13 |                 132 |
| theories/Init/Logic_Type.v             |                  7 |                  57 |
| theories/Init/Specif.v                 |                  5 |                  35 |
| theories/Init/Nat.v                    |                  0 |                   0 |
| theories/Init/Peano.v                  |                 22 |                 264 |
| theories/Init/Wf.v                     |                  8 |                  89 |
| theories/Init/Tactics.v                |                  2 |                  24 |
| theories/Init/Tauto.v                  |                  0 |                   0 |
| theories/Init/Prelude.v                |                  0 |                   0 |
| Bool/Bool.v                            |                104 |                1220 |
| Program/Basics.v                       |                  0 |                   0 |
| Classes/Init.v                         |                  0 |                   0 |
| Program/Tactics.v                      |                  0 |                   0 |
| Relations/Relation_Definitions.v       |                  0 |                   0 |
| Classes/RelationClasses.v              |                 21 |                 341 |
| Classes/Morphisms.v                    |                 47 |                 689 |
| Classes/CRelationClasses.v             |                 18 |                 245 |
| Classes/CMorphisms.v                   |                 50 |                 587 |
| Classes/Morphisms_Prop.v               |                  3 |                 127 |
| Classes/Equivalence.v                  |                  6 |                 105 |
| Classes/SetoidTactics.v                |                  0 |                   0 |
| Setoids/Setoid.v                       |                  4 |                  33 |
| Structures/Equalities.v                |                  8 |                  93 |
| Relations/Relation_Operators.v         |                  0 |                   0 |
| Relations/Operators_Properties.v       |                 35 |                 627 |
| Relations/Relations.v                  |                  2 |                  24 |
| Structures/Orders.v                    |                 12 |                 148 |
| Numbers/NumPrelude.v                   |                  0 |                   0 |
| Structures/OrdersTac.v                 |                 13 |                 234 |
| Structures/OrdersFacts.v               |                 73 |                 931 |
| Structures/GenericMinMax.v             |                 82 |                1294 |
| Numbers/NatInt/NZAxioms.v              |                  0 |                   0 |
| Numbers/NatInt/NZBase.v                |                  7 |                  87 |
| Numbers/NatInt/NZAdd.v                 |                 14 |                 168 |
| Numbers/NatInt/NZMul.v                 |                 12 |                 144 |
| Logic/Decidable.v                      |                 28 |                 336 |
| Numbers/NatInt/NZOrder.v               |                 81 |                1174 |
| Numbers/NatInt/NZAddOrder.v            |                 24 |                 288 |
| Numbers/NatInt/NZMulOrder.v            |                 46 |                 552 |
| Numbers/NatInt/NZParity.v              |                 35 |                 420 |
| Numbers/NatInt/NZPow.v                 |                 29 |                 348 |
| Numbers/NatInt/NZSqrt.v                |                 54 |                 673 |
| Numbers/NatInt/NZLog.v                 |                 64 |                 797 |
| Numbers/NatInt/NZDiv.v                 |                 49 |                 588 |
| Numbers/NatInt/NZGcd.v                 |                 36 |                 432 |
| Numbers/NatInt/NZBits.v                |                  0 |                   0 |
| Numbers/Natural/Abstract/NAxioms.v     |                  0 |                   0 |
| Numbers/NatInt/NZProperties.v          |                  0 |                   0 |
| Numbers/Natural/Abstract/NBase.v       |                 14 |                 177 |
| Numbers/Natural/Abstract/NAdd.v        |                  6 |                  72 |
| Numbers/Natural/Abstract/NOrder.v      |                 29 |                 349 |
| Numbers/Natural/Abstract/NAddOrder.v   |                  5 |                  60 |
| Numbers/Natural/Abstract/NMulOrder.v   |                  8 |                  96 |
| Numbers/Natural/Abstract/NSub.v        |                 36 |                 432 |
| Numbers/Natural/Abstract/NMaxMin.v     |                 18 |                 216 |
| Numbers/Natural/Abstract/NParity.v     |                  4 |                  48 |
| Numbers/Natural/Abstract/NPow.v        |                 26 |                 312 |
| Numbers/Natural/Abstract/NSqrt.v       |                  9 |                 108 |
| Numbers/Natural/Abstract/NLog.v        |                  0 |                   0 |
| Numbers/Natural/Abstract/NDiv.v        |                 50 |                 600 |
| Numbers/Natural/Abstract/NGcd.v        |                 14 |                 168 |
| Numbers/Natural/Abstract/NLcm.v        |                 29 |                 348 |
| Numbers/Natural/Abstract/NBits.v       |                168 |                2016 |
| Numbers/Natural/Abstract/NProperties.v |                  0 |                   0 |
| Arith/PeanoNat.v                       |                 77 |                 990 |
| Arith/Le.v                             |                  2 |                  57 |
| Arith/Lt.v                             |                 14 |                 168 |
| Arith/Plus.v                           |                 20 |                 269 |
| Arith/Gt.v                             |                 17 |                 248 |
| Arith/Minus.v                          |                 11 |                 132 |
| Arith/Mult.v                           |                 14 |                 168 |
| Arith/Between.v                        |                 19 |                 299 |
| Logic/EqdepFacts.v                     |                 26 |                 539 |
| Logic/Eqdep_dec.v                      |                 13 |                 361 |
| Arith/Peano_dec.v                      |                  3 |                  26 |
| Arith/Compare_dec.v                    |                 35 |                 360 |
| Arith/Factorial.v                      |                  3 |                  36 |
| Arith/EqNat.v                          |                 10 |                 111 |
| Arith/Wf_nat.v                         |                 18 |                 173 |
| Arith/Arith_base.v                     |                  0 |                   0 |
| Numbers/BinNums.v                      |                  0 |                   0 |
| PArith/BinPosDef.v                     |                  0 |                   0 |
| PArith/BinPos.v                        |                229 |                2810 |
| NArith/BinNatDef.v                     |                  0 |                   0 |
| NArith/BinNat.v                        |                107 |                1330 |
| PArith/Pnat.v                          |                 51 |                 688 |
| NArith/Nnat.v                          |                 30 |                 360 |
| setoid_ring/Ring_theory.v              |                 43 |                 756 |
| Lists/List.v                           |                195 |                2908 |
| setoid_ring/BinList.v                  |                  6 |                  90 |
| Numbers/Integer/Abstract/ZAxioms.v     |                  0 |                   0 |
| Numbers/Integer/Abstract/ZBase.v       |                  3 |                  36 |
| Numbers/Integer/Abstract/ZAdd.v        |                 46 |                 552 |
| Numbers/Integer/Abstract/ZMul.v        |                  8 |                  96 |
| Numbers/Integer/Abstract/ZLt.v         |                 21 |                 252 |
| Numbers/Integer/Abstract/ZAddOrder.v   |                 45 |                 543 |
| Numbers/Integer/Abstract/ZMulOrder.v   |                 24 |                 288 |
| Numbers/Integer/Abstract/ZMaxMin.v     |                 22 |                 264 |
| Numbers/Integer/Abstract/ZSgnAbs.v     |                 41 |                 492 |
| Numbers/Integer/Abstract/ZParity.v     |                  6 |                  72 |
| Numbers/Integer/Abstract/ZPow.v        |                 10 |                 120 |
| Numbers/Integer/Abstract/ZDivTrunc.v   |                 68 |                 816 |
| Numbers/Integer/Abstract/ZDivFloor.v   |                 70 |                 840 |
| Numbers/Integer/Abstract/ZGcd.v        |                 29 |                 348 |
| Numbers/Integer/Abstract/ZLcm.v        |                 50 |                 600 |
| Numbers/Integer/Abstract/ZBits.v       |                205 |                2460 |
| Numbers/Integer/Abstract/ZProperties.v |                  0 |                   0 |
| ZArith/BinIntDef.v                     |                  0 |                   0 |
| ZArith/BinInt.v                        |                212 |                2839 |
|----------------------------------------+--------------------+---------------------|
```

(*) I would call it `Future.map` better than chain.

0 files changed, 0 insertions, 0 deletions