Speed up simplify with monad laws

After    | File Name                                                       | Before   || Change
--------------------------------------------------------------------------------------------------
5m01.22s | Total                                                           | 5m44.93s || -0m43.71s
--------------------------------------------------------------------------------------------------
2m10.77s | ADTExamples/QueryStructure/Bookstore                            | 2m27.49s || -0m16.71s
0m17.32s | ADTExamples/QueryStructure/ProcessScheduler/TreeBasedRefinement | 0m21.48s || -0m04.16s
0m11.76s | ADTExamples/QueryStructure/ProcessScheduler/ListBasedRefinement | 0m14.58s || -0m02.82s
0m06.19s | ADTExamples/BinaryOperationRefinements                          | 0m07.55s || -0m01.35s
0m06.01s | ADTNotation/ilist                                               | 0m07.28s || -0m01.27s
0m01.42s | Computation/ApplyMonad                                          |   N/A    || +0m01.41s
0m11.53s | ADTExamples/QueryStructure/ListInsertRefinements                | 0m11.17s || +0m00.35s
0m09.03s | ADTExamples/MinCollection                                       | 0m08.83s || +0m00.19s
0m08.43s | ADTExamples/QueryStructure/InsertQSSpecs                        | 0m09.34s || -0m00.91s
0m04.05s | ADTExamples/QueryStructure/ListQueryRefinements                 | 0m03.89s || +0m00.15s
0m03.26s | ADTExamples/QueryStructure/ProcessScheduler/AdditionalLemmas    | 0m02.82s || +0m00.43s
0m03.24s | ADTExamples/QueryStructure/ProcessScheduler/FMapExtensions      | 0m03.09s || +0m00.15s
0m02.81s | ADTExamples/QueryStructure/ProcessScheduler/SetEq               | 0m02.53s || +0m00.28s
0m02.62s | ADTExamples/QueryStructure/GeneralQueryRefinements              | 0m02.39s || +0m00.23s
0m02.40s | Computation/Refinements/General                                 | 0m03.13s || -0m00.73s
0m02.18s | ADTNotation/StringBound                                         | 0m02.89s || -0m00.71s
0m02.09s | ADTExamples/MinPlusMax                                          | 0m01.80s || +0m00.28s
0m02.09s | ADTRefinement/SetoidMorphisms                                   | 0m02.71s || -0m00.62s
0m02.06s | ADTExamples/QueryStructure/GeneralInsertRefinements             | 0m01.86s || +0m00.19s
0m02.02s | ADTRefinement/Refinements/RefineHideADT                         | 0m02.68s || -0m00.66s
0m01.97s | Computation/Monad                                               | 0m02.61s || -0m00.63s
0m01.90s | ADTExamples/QueryStructure/QueryStructure                       | 0m01.99s || -0m00.09s
0m01.89s | ADTExamples/QueryStructure/ProcessScheduler/State               | 0m01.60s || +0m00.28s
0m01.87s | ADTExamples/QueryStructure/ProcessScheduler/DBSchema            | 0m01.81s || +0m00.06s
0m01.87s | ADTRefinement/GeneralBuildADTRefinements                        | 0m02.50s || -0m00.62s
0m01.85s | ADTRefinement/Refinements/ADTCache                              | 0m02.43s || -0m00.58s
0m01.84s | ADTExamples/QueryStructure/QueryQSSpecs                         | 0m01.96s || -0m00.11s
0m01.69s | Computation/SetoidMorphisms                                     | 0m02.20s || -0m00.51s
0m01.68s | ADTRefinement/BuildADTRefinements/SimplifyRep                   | 0m02.17s || -0m00.49s
0m01.66s | ADTRefinement/BuildADTRefinements                               | 0m02.07s || -0m00.40s
0m01.66s | ADTRefinement/Refinements/ADTRepInv                             | 0m02.24s || -0m00.58s
0m01.66s | ComputationExamples                                             | 0m02.19s || -0m00.53s
0m01.64s | ADTRefinement/BuildADTRefinements/HoneRepresentation            | 0m02.19s || -0m00.55s
0m01.62s | ADTRefinement/Refinements/SimplifyRep                           | 0m01.99s || -0m00.36s
0m01.57s | ADTRefinement/BuildADTSetoidMorphisms                           | 0m02.07s || -0m00.49s
0m01.56s | ADTExamples/QueryStructure/QueryStructureSchema                 | 0m01.86s || -0m00.30s
0m01.55s | ADTExamples/CombineBinaryOperationsSpec                         | 0m01.93s || -0m00.37s
0m01.55s | ADT/Core                                                        | 0m01.84s || -0m00.29s
0m01.52s | ADTRefinement/Refinements/DelegateMethods                       | 0m02.02s || -0m00.50s
0m01.51s | ADTRefinement/Refinements/HoneRepresentation                    | 0m01.95s || -0m00.43s
0m01.51s | ADTNotation/BuildADTReplaceMethods                              | 0m01.97s || -0m00.46s
0m01.51s | ADTRefinement                                                   | 0m01.98s || -0m00.47s
0m01.50s | Computation/ReflectiveMonad                                     | 0m01.96s || -0m00.46s
0m01.49s | ADTExamples/BinaryOperationImpl                                 | 0m01.85s || -0m00.36s
0m01.49s | ADTNotation/BuildADT                                            | 0m01.94s || -0m00.44s
0m01.49s | ADTRefinement/Refinements                                       | 0m01.90s || -0m00.40s
0m01.49s | ADTNotation                                                     | 0m01.95s || -0m00.46s
0m01.48s | ADTRefinement/Refinements/HonePickRepresentation                | 0m01.93s || -0m00.44s
0m01.48s | ADTExamples/BinaryOperationSpec                                 | 0m01.94s || -0m00.46s
0m01.48s | ADTRefinement/GeneralRefinements                                | 0m01.94s || -0m00.46s
0m01.46s | ADTExamples/QueryStructure/Heading                              | 0m01.52s || -0m00.06s
0m01.45s | Computation                                                     | 0m01.73s || -0m00.28s
0m01.43s | ADTRefinement/Core                                              | 0m01.91s || -0m00.48s
0m01.41s | ADT                                                             | 0m01.83s || -0m00.42s
0m01.41s | ADTNotation/BuildADTSig                                         | 0m01.89s || -0m00.48s
0m01.41s | ADT/ADTHide                                                     | 0m01.92s || -0m00.51s
0m01.40s | ADTExamples/QueryStructure/Relation                             | 0m01.60s || -0m00.20s
0m01.40s | ADTExamples/QueryStructure/Schema                               | 0m01.58s || -0m00.18s
0m01.38s | ADT/Pick                                                        | 0m01.81s || -0m00.43s
0m01.37s | ADT/ADTSig                                                      | 0m01.83s || -0m00.46s
0m01.33s | Computation/Refinements/Inline                                  | 0m01.73s || -0m00.39s
0m01.31s | Computation/Core                                                | 0m01.74s || -0m00.42s
0m01.30s | ADTExamples/QueryStructure/Tuple                                | 0m01.60s || -0m00.30s
0m01.24s | Computation/Refinements/Tactics                                 | 0m01.63s || -0m00.38s
0m00.47s | LogicLemmas                                                     | 0m00.62s || -0m00.15s
0m00.44s | Common                                                          | 0m00.58s || -0m00.13s
0m00.28s | ADTExamples/QueryStructure/Notations                            | 0m00.32s || -0m00.03s
0m00.24s | ADT/Specs                                                       | 0m00.30s || -0m00.06s
0m00.23s | Notations                                                       | 0m00.30s || -0m00.06s
More simple speed ups

Don't ask me why [simpl map] works.  I don't know.  I'm not sure I
want to know.  (That's not true.  The twisty part of me wants to
know.)  I do want to know if [cbn] from trunk works any better than
[simpl] here.

After    | File Name                                                       | Before   || Change
--------------------------------------------------------------------------------------------------
4m41.66s | Total                                                           | 5m02.94s || -0m21.27s
--------------------------------------------------------------------------------------------------
1m55.17s | ADTExamples/QueryStructure/Bookstore                            | 2m16.14s || -0m20.96s
0m09.88s | ADTExamples/MinCollection                                       | 0m08.88s || +0m01.00s
0m16.68s | ADTExamples/QueryStructure/ProcessScheduler/TreeBasedRefinement | 0m17.36s || -0m00.67s
0m11.40s | ADTExamples/QueryStructure/ListInsertRefinements                | 0m11.47s || -0m00.07s
0m11.20s | ADTExamples/QueryStructure/ProcessScheduler/ListBasedRefinement | 0m11.81s || -0m00.61s
0m07.68s | ADTExamples/QueryStructure/InsertQSSpecs                        | 0m07.55s || +0m00.12s
0m06.27s | ADTExamples/BinaryOperationRefinements                          | 0m06.06s || +0m00.20s
0m05.47s | ADTNotation/ilist                                               | 0m05.47s || +0m00.00s
0m03.90s | ADTExamples/QueryStructure/ListQueryRefinements                 | 0m03.95s || -0m00.05s
0m03.15s | ADTExamples/QueryStructure/ProcessScheduler/FMapExtensions      | 0m03.15s || +0m00.00s
0m02.85s | ADTExamples/QueryStructure/ProcessScheduler/AdditionalLemmas    | 0m02.80s || +0m00.05s
0m02.53s | ADTExamples/QueryStructure/ProcessScheduler/SetEq               | 0m02.50s || +0m00.02s
0m02.45s | ADTExamples/QueryStructure/GeneralQueryRefinements              | 0m02.43s || +0m00.02s
0m02.44s | Computation/Refinements/General                                 | 0m02.43s || +0m00.00s
0m02.23s | ADTNotation/StringBound                                         | 0m02.18s || +0m00.04s
0m02.04s | ADTRefinement/SetoidMorphisms                                   | 0m02.02s || +0m00.02s
0m02.01s | ADTRefinement/Refinements/RefineHideADT                         | 0m01.99s || +0m00.01s
0m01.96s | Computation/Monad                                               | 0m02.02s || -0m00.06s
0m01.91s | ADTRefinement/GeneralBuildADTRefinements                        | 0m01.94s || -0m00.03s
0m01.90s | ADTExamples/QueryStructure/GeneralInsertRefinements             | 0m01.91s || -0m00.01s
0m01.88s | ADTRefinement/Refinements/ADTCache                              | 0m01.85s || +0m00.02s
0m01.84s | ADTExamples/QueryStructure/ProcessScheduler/DBSchema            | 0m01.82s || +0m00.02s
0m01.83s | ADTExamples/MinPlusMax                                          | 0m01.84s || -0m00.01s
0m01.72s | ADTRefinement/Refinements/ADTRepInv                             | 0m01.71s || +0m00.01s
0m01.70s | Computation/SetoidMorphisms                                     | 0m01.75s || -0m00.05s
0m01.70s | ADTRefinement/BuildADTRefinements                               | 0m01.65s || +0m00.05s
0m01.69s | ADTExamples/QueryStructure/QueryQSSpecs                         | 0m01.68s || +0m00.01s
0m01.69s | ADTExamples/QueryStructure/QueryStructure                       | 0m01.69s || +0m00.00s
0m01.68s | ADTExamples/QueryStructure/ProcessScheduler/State               | 0m01.67s || +0m00.01s
0m01.67s | ADTRefinement/BuildADTRefinements/SimplifyRep                   | 0m01.66s || +0m00.01s
0m01.65s | ComputationExamples                                             | 0m01.65s || +0m00.00s
0m01.64s | ADTRefinement/BuildADTRefinements/HoneRepresentation            | 0m01.65s || -0m00.01s
0m01.59s | ADTRefinement/BuildADTSetoidMorphisms                           | 0m01.61s || -0m00.02s
0m01.58s | ADTExamples/QueryStructure/QueryStructureSchema                 | 0m01.56s || +0m00.02s
0m01.55s | ADTExamples/CombineBinaryOperationsSpec                         | 0m01.57s || -0m00.02s
0m01.54s | ADTRefinement/Refinements/DelegateMethods                       | 0m01.53s || +0m00.01s
0m01.53s | Computation/ReflectiveMonad                                     | 0m01.54s || -0m00.01s
0m01.53s | ADTNotation/BuildADTReplaceMethods                              | 0m01.55s || -0m00.02s
0m01.52s | ADTRefinement/Refinements/SimplifyRep                           | 0m01.47s || +0m00.05s
0m01.51s | ADTRefinement/Refinements/HoneRepresentation                    | 0m01.50s || +0m00.01s
0m01.51s | ADTNotation                                                     | 0m01.78s || -0m00.27s
0m01.50s | ADTExamples/BinaryOperationImpl                                 | 0m01.53s || -0m00.03s
0m01.50s | ADTExamples/BinaryOperationSpec                                 | 0m01.50s || +0m00.00s
0m01.50s | ADTRefinement                                                   | 0m01.50s || +0m00.00s
0m01.49s | ADTRefinement/Refinements/HonePickRepresentation                | 0m01.51s || -0m00.02s
0m01.49s | ADTNotation/BuildADT                                            | 0m01.47s || +0m00.02s
0m01.47s | ADTRefinement/Refinements                                       | 0m01.48s || -0m00.01s
0m01.45s | ADTRefinement/GeneralRefinements                                | 0m01.47s || -0m00.02s
0m01.44s | ADT/Pick                                                        | 0m01.39s || +0m00.05s
0m01.43s | ADT                                                             | 0m01.40s || +0m00.03s
0m01.43s | Computation/ApplyMonad                                          | 0m01.45s || -0m00.02s
0m01.42s | ADTRefinement/Core                                              | 0m01.47s || -0m00.05s
0m01.42s | ADTNotation/BuildADTSig                                         | 0m01.43s || -0m00.01s
0m01.42s | ADT/ADTHide                                                     | 0m01.42s || +0m00.00s
0m01.39s | ADT/Core                                                        | 0m01.39s || +0m00.00s
0m01.38s | ADTExamples/QueryStructure/Schema                               | 0m01.37s || +0m00.00s
0m01.37s | ADT/ADTSig                                                      | 0m01.37s || +0m00.00s
0m01.36s | Computation                                                     | 0m01.38s || -0m00.01s
0m01.33s | ADTExamples/QueryStructure/Relation                             | 0m01.33s || +0m00.00s
0m01.33s | Computation/Core                                                | 0m01.34s || -0m00.01s
0m01.31s | ADTExamples/QueryStructure/Tuple                                | 0m01.31s || +0m00.00s
0m01.30s | Computation/Refinements/Inline                                  | 0m01.37s || -0m00.07s
0m01.30s | ADTExamples/QueryStructure/Heading                              | 0m01.30s || +0m00.00s
0m01.28s | Computation/Refinements/Tactics                                 | 0m01.31s || -0m00.03s
0m00.47s | LogicLemmas                                                     | 0m00.45s || +0m00.01s
0m00.43s | Common                                                          | 0m00.45s || -0m00.02s
0m00.27s | ADTExamples/QueryStructure/Notations                            | 0m00.25s || +0m00.02s
0m00.26s | ADT/Specs                                                       | 0m00.27s || -0m00.01s
0m00.25s | Notations                                                       | 0m00.24s || +0m00.01s
Make magic

I'm not going to explain this one, either.  I will ask some questions.

Serious questions:
What arguments are we passing to [map] that make it so slow to
[simpl]?

Sarcastic questions:
When can we get trunk and cbn?
Why is this code so fragile?
How can I prevent the next person who touches the code (maybe myself)
from blowing away the performance?

The problem with having a noisy system is that 5% speed-ups tend to be
lost in the noise of the rest of the code.  I'm not running it again,
because I don't want to spend an hour profiling to justify 10s of
speedup.

After    | File Name                                                       | Before   || Change
--------------------------------------------------------------------------------------------------
4m39.26s | Total                                                           | 4m39.59s || -0m00.33s
--------------------------------------------------------------------------------------------------
1m43.43s | ADTExamples/QueryStructure/Bookstore                            | 1m53.83s || -0m10.39s
0m13.09s | ADTExamples/QueryStructure/ProcessScheduler/ListBasedRefinement | 0m11.07s || +0m02.01s
0m16.84s | ADTExamples/QueryStructure/ProcessScheduler/TreeBasedRefinement | 0m16.72s || +0m00.12s
0m11.64s | ADTExamples/QueryStructure/ListInsertRefinements                | 0m11.24s || +0m00.40s
0m08.98s | ADTExamples/MinCollection                                       | 0m08.80s || +0m00.17s
0m07.55s | ADTExamples/QueryStructure/InsertQSSpecs                        | 0m07.62s || -0m00.07s
0m06.32s | ADTExamples/BinaryOperationRefinements                          | 0m06.02s || +0m00.30s
0m06.04s | ADTNotation/ilist                                               | 0m05.50s || +0m00.54s
0m04.06s | ADTExamples/QueryStructure/ListQueryRefinements                 | 0m03.92s || +0m00.13s
0m03.27s | ADTExamples/QueryStructure/ProcessScheduler/FMapExtensions      | 0m03.15s || +0m00.12s
0m03.09s | ADTExamples/QueryStructure/ProcessScheduler/AdditionalLemmas    | 0m02.85s || +0m00.23s
0m02.70s | ADTExamples/QueryStructure/ProcessScheduler/SetEq               | 0m02.51s || +0m00.19s
0m02.51s | ADTNotation/StringBound                                         | 0m02.18s || +0m00.32s
0m02.51s | ADTRefinement/SetoidMorphisms                                   | 0m02.04s || +0m00.46s
0m02.46s | Computation/Refinements/General                                 | 0m02.41s || +0m00.04s
0m02.41s | ADTExamples/QueryStructure/GeneralQueryRefinements              | 0m02.44s || -0m00.02s
0m02.37s | ADTRefinement/GeneralBuildADTRefinements                        | 0m01.90s || +0m00.47s
0m02.33s | ADTRefinement/Refinements/RefineHideADT                         | 0m02.04s || +0m00.29s
0m02.30s | ADTRefinement/BuildADTSetoidMorphisms                           | 0m01.58s || +0m00.71s
0m02.03s | ADTExamples/QueryStructure/ProcessScheduler/DBSchema            | 0m01.82s || +0m00.20s
0m02.03s | ADTRefinement/Refinements/ADTCache                              | 0m01.86s || +0m00.16s
0m01.99s | Computation/Monad                                               | 0m01.98s || +0m00.01s
0m01.99s | ADTExamples/MinPlusMax                                          | 0m01.84s || +0m00.14s
0m01.97s | ADTRefinement/Core                                              | 0m01.42s || +0m00.55s
0m01.94s | ADTNotation                                                     | 0m01.49s || +0m00.44s
0m01.87s | ADTExamples/QueryStructure/GeneralInsertRefinements             | 0m01.85s || +0m00.02s
0m01.81s | ADTExamples/QueryStructure/QueryQSSpecs                         | 0m01.69s || +0m00.12s
0m01.81s | ComputationExamples                                             | 0m01.66s || +0m00.15s
0m01.80s | ADTRefinement/Refinements/DelegateMethods                       | 0m01.54s || +0m00.26s
0m01.75s | ADT                                                             | 0m01.42s || +0m00.33s
0m01.75s | ADTRefinement/BuildADTRefinements/SimplifyRep                   | 0m01.67s || +0m00.08s
0m01.73s | ADTRefinement/GeneralRefinements                                | 0m01.47s || +0m00.26s
0m01.72s | ADTNotation/BuildADT                                            | 0m01.49s || +0m00.23s
0m01.72s | ADTRefinement/BuildADTRefinements/HoneRepresentation            | 0m01.69s || +0m00.03s
0m01.70s | Computation/SetoidMorphisms                                     | 0m01.76s || -0m00.06s
0m01.70s | ADTRefinement/Refinements/ADTRepInv                             | 0m01.74s || -0m00.04s
0m01.68s | ADTRefinement/Refinements/HoneRepresentation                    | 0m01.58s || +0m00.09s
0m01.68s | ADTRefinement/BuildADTRefinements                               | 0m01.65s || +0m00.03s
0m01.68s | ADTExamples/QueryStructure/ProcessScheduler/State               | 0m01.66s || +0m00.02s
0m01.68s | ADTExamples/CombineBinaryOperationsSpec                         | 0m01.56s || +0m00.11s
0m01.67s | ADTExamples/BinaryOperationSpec                                 | 0m01.49s || +0m00.17s
0m01.67s | ADTExamples/QueryStructure/QueryStructure                       | 0m01.70s || -0m00.03s
0m01.63s | ADTNotation/BuildADTReplaceMethods                              | 0m01.50s || +0m00.12s
0m01.62s | ADT/ADTSig                                                      | 0m01.66s || -0m00.03s
0m01.61s | ADTExamples/BinaryOperationImpl                                 | 0m01.48s || +0m00.13s
0m01.60s | ADTNotation/BuildADTSig                                         | 0m01.43s || +0m00.17s
0m01.56s | ADTRefinement/Refinements/HonePickRepresentation                | 0m01.69s || -0m00.12s
0m01.56s | ADTRefinement/Refinements/SimplifyRep                           | 0m01.71s || -0m00.14s
0m01.55s | ADT/ADTHide                                                     | 0m01.41s || +0m00.14s
0m01.52s | ADTExamples/QueryStructure/QueryStructureSchema                 | 0m01.60s || -0m00.08s
0m01.52s | ADTRefinement/Refinements                                       | 0m01.48s || +0m00.04s
0m01.51s | Computation/ReflectiveMonad                                     | 0m01.51s || +0m00.00s
0m01.50s | ADTRefinement                                                   | 0m01.51s || -0m00.01s
0m01.49s | ADT/Pick                                                        | 0m01.44s || +0m00.05s
0m01.44s | Computation/ApplyMonad                                          | 0m01.45s || -0m00.01s
0m01.44s | ADT/Core                                                        | 0m01.39s || +0m00.05s
0m01.38s | ADTExamples/QueryStructure/Schema                               | 0m01.38s || +0m00.00s
0m01.36s | Computation                                                     | 0m01.40s || -0m00.03s
0m01.34s | ADTExamples/QueryStructure/Relation                             | 0m01.33s || +0m00.01s
0m01.34s | ADTExamples/QueryStructure/Tuple                                | 0m01.32s || +0m00.02s
0m01.34s | Computation/Core                                                | 0m01.37s || -0m00.03s
0m01.32s | Computation/Refinements/Inline                                  | 0m01.37s || -0m00.05s
0m01.32s | ADTExamples/QueryStructure/Heading                              | 0m01.34s || -0m00.02s
0m01.27s | Computation/Refinements/Tactics                                 | 0m01.32s || -0m00.05s
0m00.51s | LogicLemmas                                                     | 0m00.46s || +0m00.04s
0m00.42s | Common                                                          | 0m00.46s || -0m00.04s
0m00.29s | ADTExamples/QueryStructure/Notations                            | 0m00.25s || +0m00.03s
0m00.28s | ADT/Specs                                                       | 0m00.24s || +0m00.04s
0m00.27s | Notations                                                       | 0m00.25s || +0m00.02s
Shove more work into simplify with monad laws

After    | File Name                                                       | Before   || Change
--------------------------------------------------------------------------------------------------
4m22.82s | Total                                                           | 4m29.63s || -0m06.81s
--------------------------------------------------------------------------------------------------
1m36.38s | ADTExamples/QueryStructure/Bookstore                            | 1m39.29s || -0m02.90s
0m01.55s | ADTNotation/BuildADTReplaceMethods                              | 0m02.62s || -0m01.07s
0m16.54s | ADTExamples/QueryStructure/ProcessScheduler/TreeBasedRefinement | 0m16.41s || +0m00.12s
0m11.28s | ADTExamples/QueryStructure/ListInsertRefinements                | 0m11.27s || +0m00.00s
0m11.21s | ADTExamples/QueryStructure/ProcessScheduler/ListBasedRefinement | 0m11.17s || +0m00.04s
0m09.11s | ADTExamples/MinCollection                                       | 0m08.93s || +0m00.17s
0m07.94s | ADTExamples/QueryStructure/InsertQSSpecs                        | 0m07.67s || +0m00.27s
0m06.06s | ADTExamples/BinaryOperationRefinements                          | 0m06.61s || -0m00.55s
0m05.38s | ADTNotation/ilist                                               | 0m05.44s || -0m00.06s
0m03.91s | ADTExamples/QueryStructure/ListQueryRefinements                 | 0m03.95s || -0m00.04s
0m03.15s | ADTExamples/QueryStructure/ProcessScheduler/FMapExtensions      | 0m03.36s || -0m00.20s
0m02.88s | ADTExamples/QueryStructure/ProcessScheduler/AdditionalLemmas    | 0m02.90s || -0m00.02s
0m02.51s | ADTExamples/QueryStructure/ProcessScheduler/SetEq               | 0m02.51s || +0m00.00s
0m02.43s | Computation/Refinements/General                                 | 0m02.53s || -0m00.09s
0m02.41s | ADTExamples/QueryStructure/GeneralQueryRefinements              | 0m02.42s || -0m00.00s
0m02.20s | ADTNotation/StringBound                                         | 0m02.19s || +0m00.01s
0m02.05s | ADTRefinement/SetoidMorphisms                                   | 0m02.33s || -0m00.28s
0m02.02s | ADTExamples/MinPlusMax                                          | 0m01.83s || +0m00.18s
0m02.00s | ADTRefinement/Refinements/RefineHideADT                         | 0m02.06s || -0m00.06s
0m01.97s | Computation/Monad                                               | 0m01.95s || +0m00.02s
0m01.95s | ADTExamples/QueryStructure/QueryStructure                       | 0m01.74s || +0m00.20s
0m01.92s | ADTRefinement/GeneralBuildADTRefinements                        | 0m01.93s || -0m00.01s
0m01.87s | ADTRefinement/Refinements/ADTCache                              | 0m02.11s || -0m00.23s
0m01.86s | ADTExamples/QueryStructure/GeneralInsertRefinements             | 0m01.92s || -0m00.05s
0m01.84s | ADTExamples/QueryStructure/ProcessScheduler/DBSchema            | 0m01.86s || -0m00.02s
0m01.75s | ComputationExamples                                             | 0m01.67s || +0m00.08s
0m01.72s | ADTRefinement/Refinements/ADTRepInv                             | 0m02.29s || -0m00.57s
0m01.71s | ADTRefinement/BuildADTRefinements                               | 0m01.71s || +0m00.00s
0m01.71s | ADTRefinement/GeneralRefinements                                | 0m01.75s || -0m00.04s
0m01.70s | Computation/SetoidMorphisms                                     | 0m01.73s || -0m00.03s
0m01.69s | ADTExamples/QueryStructure/ProcessScheduler/State               | 0m01.69s || +0m00.00s
0m01.68s | ADTRefinement/BuildADTRefinements/SimplifyRep                   | 0m01.72s || -0m00.04s
0m01.68s | ADTExamples/QueryStructure/QueryQSSpecs                         | 0m01.70s || -0m00.02s
0m01.67s | ADTRefinement/BuildADTRefinements/HoneRepresentation            | 0m01.70s || -0m00.03s
0m01.60s | ADTRefinement/BuildADTSetoidMorphisms                           | 0m01.61s || -0m00.01s
0m01.55s | ADTExamples/CombineBinaryOperationsSpec                         | 0m01.64s || -0m00.08s
0m01.55s | ADT/Core                                                        | 0m01.40s || +0m00.15s
0m01.54s | ADTExamples/QueryStructure/QueryStructureSchema                 | 0m01.54s || +0m00.00s
0m01.54s | ADTRefinement/Refinements/DelegateMethods                       | 0m01.56s || -0m00.02s
0m01.52s | Computation/ReflectiveMonad                                     | 0m01.50s || +0m00.02s
0m01.51s | ADT/ADTSig                                                      | 0m01.40s || +0m00.11s
0m01.51s | ADTRefinement/Refinements/HonePickRepresentation                | 0m01.51s || +0m00.00s
0m01.51s | ADTRefinement/Refinements                                       | 0m01.52s || -0m00.01s
0m01.50s | ADTExamples/BinaryOperationImpl                                 | 0m01.48s || +0m00.02s
0m01.50s | ADTExamples/BinaryOperationSpec                                 | 0m01.55s || -0m00.05s
0m01.50s | ADTNotation                                                     | 0m01.90s || -0m00.39s
0m01.49s | ADTRefinement/Refinements/HoneRepresentation                    | 0m01.52s || -0m00.03s
0m01.48s | ADTNotation/BuildADT                                            | 0m01.76s || -0m00.28s
0m01.47s | ADTRefinement                                                   | 0m01.73s || -0m00.26s
0m01.46s | ADTRefinement/Refinements/SimplifyRep                           | 0m01.51s || -0m00.05s
0m01.45s | ADTRefinement/Core                                              | 0m01.62s || -0m00.17s
0m01.44s | ADT/Pick                                                        | 0m01.40s || +0m00.04s
0m01.44s | ADTNotation/BuildADTSig                                         | 0m01.58s || -0m00.14s
0m01.44s | Computation/ApplyMonad                                          | 0m01.63s || -0m00.18s
0m01.42s | ADT/ADTHide                                                     | 0m01.41s || +0m00.01s
0m01.39s | ADT                                                             | 0m01.41s || -0m00.02s
0m01.38s | Computation                                                     | 0m01.35s || +0m00.02s
0m01.35s | ADTExamples/QueryStructure/Schema                               | 0m01.39s || -0m00.03s
0m01.34s | Computation/Core                                                | 0m01.39s || -0m00.04s
0m01.33s | ADTExamples/QueryStructure/Relation                             | 0m01.41s || -0m00.07s
0m01.33s | ADTExamples/QueryStructure/Tuple                                | 0m01.31s || +0m00.02s
0m01.31s | Computation/Refinements/Inline                                  | 0m01.30s || +0m00.01s
0m01.31s | ADTExamples/QueryStructure/Heading                              | 0m01.39s || -0m00.07s
0m01.28s | Computation/Refinements/Tactics                                 | 0m01.25s || +0m00.03s
0m00.46s | LogicLemmas                                                     | 0m00.49s || -0m00.02s
0m00.45s | Common                                                          | 0m00.46s || -0m00.01s
0m00.26s | ADT/Specs                                                       | 0m00.24s || +0m00.02s
0m00.25s | ADTExamples/QueryStructure/Notations                            | 0m00.28s || -0m00.03s
0m00.24s | Notations                                                       | 0m00.24s || +0m00.00s
Actually include ApplyMonad
A few extra facts about FMaps and the SetEq relation
Initial work on the Bag interface

This design seems to mostly make sense, except for the fact that proof
terms tend to grow extremely large. The list implementation works well.
The tree based one is untested, due to exploding proof terms issues.

The core data structures are:
* Typeclass Bag (empty, insert, enumerate, find), offering a unified
interface to access data
* Record IndexedBag (fmap, consistency), wrapping an Fmap with a proof
of its proper indexing through the IndexedTree functor.

Implementations of Bag are now:
* IndexedBagAsBag, showing how IndexedBags can behave as Bags
* ListAsBag, showing how Lists can behave as Bags
Switched ADTs to have constructors and methods.
Cleaned up code base.
List-based implementation of Bookstore slimed down for demos.
Small formatting changes to Bookstore example
Read code through ADTNotation
A pass through ADTRefinement
Small formatting tweaks
New example: Trivial
Move Bags.v to a separate folder
Merge branch 'master' of /afs/csail.mit.edu/group/plv/git/adt-synthesis
Extend Bags.v to create nested tree types from list of attributes

The current way of ensuring that attributes only have a domain of string
or nat relies on Ltac; it would probably better to find a typleclass-
based way of doing the same.
Prove correction (in a certain sense) of nested trees

An important part of the TreeBasedRefinement example is to swap from a
filter over the list of elements to a find over the tree structure. This
was previously justified by manual proofs relying on the KeyedOnPID
predicate; this commit subsumes these proofs by introducing a
bfind_correct predicate in the Bag interface, and proving this predicate
for both the fmap- and the list-based implementations.

The bag interface now has two extra fields, bfind_matcher and
bfind_correct; bfind_matcher is a boolean function which, used in
conjunction with a search toer to filter over the results of benumerate,
must return the same as calling bfind directly.

bstar is the empty search term (such that find bstar == benumerate (the
bstar_search predicate).