on d90e30e help sign in
all commits
7143962Make totality a warning until compilingDavid Raymond Christiansen 92d7b51Fix boolElim optimisationEdwin Brady e2249c0Add workaround for some non-trivial case-matches on detaggable data.Matus Tejiscak d7e4bfaFix indentation.Matus Tejiscak fb3d76cAdd a check for missed newtype optimisations.Matus Tejiscak 8e3d3c0Fix erasure from data constructors.Matus Tejiscak 4be2fbaAllow second argument of assert_smaller to be of different type than first argument since this could be useful for functions that are written with Universe-style pattern matching, i.e., where the rhs pattern has different type than the lhs expression.Ahmad Salim Al-Sibahi 24ced57Fix name confusion.Matus Tejiscak 013d766Use ASTUtils in Compiler.hs.Matus Tejiscak 171e45bExact name lookups in getArity.Matus Tejiscak 4bc8589Improve --dumpcases.Matus Tejiscak 5f93139Move forcing to Compiler.hs.Matus Tejiscak 0203531Fix case-inspection of lazy values.Matus Tejiscak 779ecf2Fix laziness in Compiler.hs.Matus Tejiscak 2604c1dFix compilation of applied de bruijn vars.Matus Tejiscak 4e1d50eUse method info to erase stuff in Compiler.hs.Matus Tejiscak cee5985Recognise instance constructors in Compiler.hs.Matus Tejiscak 5bdfe51Comment clarification.Matus Tejiscak ca257e0Remove commented-out dead code.Matus Tejiscak 67b01ecRefactor Compiler.hs.Matus Tejiscak 37b3f6cAdd instance ctor application analysis.Matus Tejiscak 826fa9cReplace projections from instance ctors with special names.Matus Tejiscak e8c6a5barity in Compiler a bit safer.Matus Tejiscak b7d5cbcBroaden cover of getArity.Matus Tejiscak 7f5043aRespect unused args in case-projections from data ctors.Matus Tejiscak 7408d94Add newtype-case elimination.Matus Tejiscak b51cf28Include erasure in data constructors.Matus Tejiscak 080a291Compile data ctors with real arity.Matus Tejiscak 5b62302Add "detaggable" as an argument to OptInfo.Matus Tejiscak c1f89faRemove the last occurrence of "force".Matus Tejiscak 7688a12More small fixes.Matus Tejiscak f8e2582Erase unused case-branches.Matus Tejiscak 5ae2e58Fix erasure from data ctors.Matus Tejiscak eea9302Disable forcing and collapsibility (dirty hack).Matus Tejiscak 7e633eeImprove reporting of accessibility errors.Matus Tejiscak 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