Agda-2.3.2.2: benchmark/notes

20110629: after new level representation and optimised positivity check
          (used interface file for monad example)

20110701: actually type checking the monad example

20110706: (15:00) better precision in ArgsCmp constraints (avoiding rechecking
          the first arguments)

20110822: (13:30) switched compareArgs to compareElim (without getting rid of
          projection arguments). 1 second faster on monad and 1.5 seconds
          faster on monadpostulate, not sure why.

20110823: Got rid of projection arguments. Cut the monad examples in half, but
          no effect on prim which is kind of odd since ... oh we're using a
          datatype in prim. Changing that to a record and rerunning.

20110823: (08:00) Sigma record in prim and added all projections instead of
          just the first three.

20110825: Allow instantiation of blocked terms, and short-cut instantiation of
          metas.

20110830: New computer.

20110830: (18:00) Added patternmatch test case. Needs abnormal amounts of
          memory. No idea why.

20110901: Removed a clause from the patternmatch case. The reason it requires
          so much memory is coverage checking. It's expected with the current
          algorithm. It could potentially be improved by separating coverage
          checking from unreachability checking, but this isn't really a
          problem in practise. GHC checks both completeness and overlap
          instantly, so it is possible.

20110901: (12:30) Set.mapMonotonic instead of Set.map when lowering sets of
          free variables under a binder.

20110901: (13:30) New projection benchmarks (record, data and nested) to test
          eliminator detection for projection-like functions.

20110902: Implemented projection detection.

20110906: New state monad implementation (IORef s -> m a)

20110907: (01:00) Pushing types into constructor applications.

          (03:00) Treating (\x -> x) as (\(x : _) -> x). Note increase in
          number of metas.

          (03:26) Pushing types into lambdas, helps a little, but not as much
          as we would like: For cwf we had 2794 metas before the (\x -> x)
          change, 3242 after, and 3038 after this fix.

          (04:48) Taking better care of types in lambdas. Metas for cwf now
          down to 2834, so almost what we had before.

          (05:33) Removed all 'abstract's from the cwf benchmark. Very little
          difference! 3.1s -> 3.7s and 43MB -> 61MB.

20110908: Fixed issues 311, 450 and 451.

20110909: Minor improvement of FreeVars.singleton and added
          Data.List.Any.Properties as a benchmark.

20110910: Can't remember.

20110915: (07.38) New constraint handling machinery.
          (08.47) No more quadratic nubbing in localNames
          (09.14) Don't reduce sorts when reducing types
          (13.11) Got rid of most MonadTCMs

20110919: Positivity checker needs to look at pattern matching.

20110922: Just minor stuff.

20110924: (09.49) New mutual syntax.
          (10.04) Avoid generating sort metas when checking isType_ of a Fun or a Pi
          (     ) Same for isType_ of Set or Set a

20120406: Qualified mixfix operators

20120702: Pre-sharing
20120705: Sharing is working but under-utilized
20121005: (18.37) With sharing
          (20.31) Without sharing