| 1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889 |
- 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
- 20140323: Added Benchmark facility for billing CPU time to accounts.
|
