on d5726ec help sign in
all commits
dfb2663Run erasure analysis even when not compiling.Matus Tejiscak 72b473dMove Erasure back into Idris/.Matus Tejiscak 4ae96c9Remove unused reachability analysis.Matus Tejiscak fe0e037Move erasure to IRTS.Matus Tejiscak 6e04313Fix coverage again, add comment.Matus Tejiscak 0179c54Fix coverage.Matus Tejiscak 44ee6d3Handle overapplied functions correctly.Matus Tejiscak 8576fbaRemove debug printouts.Matus Tejiscak e866fa6Don't erase from unknown names.Matus Tejiscak 589bb4bCtor erasure fixed.Matus Tejiscak 8c7af47Also print residual deps.Matus Tejiscak 99d5a0aOnly compile the reachable names.Matus Tejiscak 14d352eFix eta-expansion, list reachable names.Matus Tejiscak d403d47Add some debug printouts.Matus Tejiscak d4562c4Remove the old findUnusedArgs.Matus Tejiscak b1bef1cConnect erasure with analysis.Matus Tejiscak ad0dce1Invert the meaning of used/unused in CGInfo.Matus Tejiscak f0d7876Add basic conversion to unused-map.Matus Tejiscak dd7a2b2Remove unsafeDebugIO and traceShow.Matus Tejiscak a92914bAlso account for called references.Matus Tejiscak a368e1dPrinting reinstated.Matus Tejiscak f5532ebDeps inverted.Matus Tejiscak da67875Forward chaining search implemented.Matus Tejiscak 49c7abcRemove cached deps'.Matus Tejiscak 7e308ddEliminate unused inputs to erasure analysisMatus Tejiscak 4dc937aCompilability.Matus Tejiscak 06e0bb9Cached deps added.Matus Tejiscak 6041ec1Improved dep pretty-printing.Matus Tejiscak aff2988Redefine dep analysis data structures.Matus Tejiscak 20b544cIntercommit.Matus Tejiscak 1b75037Intercommit.Matus Tejiscak ccadc82Ctor usage analysis roughly complete.Matus Tejiscak 59c3cd1Make ProjCase take exactly one alternative. (TODO: is this safe?)Matus Tejiscak 961c6bcRemove export of traceUnused.Matus Tejiscak 2ac5aaaRename UnusedArgs to Erasure.Matus Tejiscak f675e05Add CodegenInfo structure, give CGs uniform typesEdwin Brady d763c9cUse postulates for decEq primitive proofsEdwin Brady 3cef609Annotate 'Lazy' with reason for lazinessEdwin Brady d4ffc21Add ManagedPtr typeEdwin Brady e175b1ajavascript: use %include directive to include external javascript filesraichoo fb3c24cMake EVAL and APPLY smallerEdwin Brady 130f437Remove | annotation, make Force/Delay implicitEdwin Brady 57af985Add 'force' (opposite of 'lazy')Edwin Brady 6eee6c8Add assert_total functionEdwin Brady 9e350acInline assert_smaller correctlyEdwin Brady e9c9297Make lookupCtxtExact return Maybe instead of ListDavid Raymond Christiansen 46e894dUse Data.Text for variable namesEdwin Brady 7604451Cache argument types for building case treesEdwin Brady 0f97368Merge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna