git.iko.soy/Idris-dev
on 751a6ee help sign in
history ofsrc/Idris/Coverage.hs
all commits
c78fb14Fixed errors; partially complete default arg subsTimo Petteri Sinnemäki d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki 9c99a07Add 'covering' function optionEdwin Brady 678fc86Finish guardedness checkEdwin Brady b0720b0Change guardedness check for new-style coinductionEdwin Brady 88aa6d1Support mixed induction/coinduction with Inf typeEdwin Brady 3cef609Annotate 'Lazy' with reason for lazinessEdwin Brady 7f3d436Remove some commented out codeEdwin Brady c1ef938New syntax for documentation commentsDavid Raymond Christiansen 130f437Remove | annotation, make Force/Delay implicitEdwin Brady f6bebd3Proper pretty-printing of dependent pairsDavid Raymond Christiansen e80f871Annotate and colour pairs and () properlyDavid Raymond Christiansen 6eee6c8Add assert_total functionEdwin Brady 526cd75Add assert_smaller functionEdwin Brady c0cc1ddMerge remote-tracking branch 'upstream/master' into semantic-pprintDavid Raymond Christiansen dc4ce0cReplace the string-slinging show with pretty-printDavid Raymond Christiansen fe3f03fAdded %error_reverse annotationEdwin Brady 803194fArgument options (instead of just a Bool for lazy)Edwin Brady d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 7604451Cache argument types for building case treesEdwin Brady 3eb8fc8Fix earlier %assert_total propagationEdwin Brady 3985f42Propagate assert_total to case blocksEdwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna 65c301cRecursive constructor disjointness + cleanupMatus Tejiscak 0f97368Merge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna 40e6293Some interactive editing fixesEdwin Brady 58a12c1Totality checker improvements (soundness)Edwin Brady ec3daa4Make sure deferred definitions get totality checkedEdwin Brady 3c32b65Whitespace cleanup.George Leontiev 76722bfRemove forcing optimisation from coverage checkerEdwin Brady 0e76ac9Remember whether implicits are machine generatedEdwin Brady b9d0b7eRemove irrelevant commentEdwin Brady f39cad9Fix coverage checking for functions matching constantsEdwin Brady daab1a3Partially defined names should not reduce at compile-timeEdwin Brady f1c3c75Merge branch 'color-repl' of https://github.com/david-christiansen/Idris-dev into david-christiansen-color-replEdwin Brady a063bfaSome refactoring in CaseOp Separate case trees for totality checking, compile time and run time and lift into their own data structure, so that it's clear which one to use when.Edwin Brady b762f14Basic colourisation in REPLDavid Christiansen ffb9ea9Semantic colouring of identifiers in REPLDavid Christiansen 1d4d226Optimise datatypes with one constructor and one argument No need to pack them up (because we're strict!) so just treat them as a newtype would be in Haskell.Edwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin Brady f226a47Make coverage checker look inside pairs/dependent pairs Fixes #446Edwin Brady 2e8904dMuch faster coverage checking by ignorng forced arguments No need to generate cases to check for them, because we already know their value is forced by another part of the same constructor!Edwin Brady 83956b4Minor problem with previous coverage checker patch fixedEdwin Brady b8bba09Speed improvement for coverage checking Lots of repeated work in checking repeated clauses chopped out (there's more of this to come)Edwin Brady 5dbafdcVarious logging tweaks Just altering some levels to get more useful debugging out of case block elaboration and coverage checkingEdwin Brady 4bd5a5bSmall coverage checker fix Need to generate possible cases by looking at the patterns, not by looking at the function type alone. Of course, this is what it was trying to do, but there was a mistake... Fixes #397Edwin Brady d9435c6New size change graph builder Looks at patterns, rather than case tree, and therefore finds it easier to spot structurally smaller arguments which are more complex.Edwin Brady