git.iko.soy/Idris-dev
on 3cb1f21 help sign in
history ofsrc/Idris/Coverage.hs
all commits
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 56bd9a1Look through call graph for mutual recursion when productivity checking Otherwise we might miss non-productive calls, particularly important when using 'with'. Fixes issue #183Edwin Brady 3149de0Coinductive types do not get smaller! Fix size change graph builder.Edwin Brady 0a4f002Productivity check fix Guardedness check didn't actually check it was under a constructor!Edwin Brady 700759fCache missing cases found by totality checker, for display Now :missing works correctly (fixes issue #210) Also, remove a large chunk of unused code in coverage checker.Edwin Brady a807a34Remove the unused arg from lookup functionsDavid Christiansen b441aabFix comedy error in termination checkerEdwin Brady 4e19c35Make coverage checker a lot faster ...with strategic use of 'nub' so as not to generate a crazy number of clauses!Edwin Brady 4c45c09Speed up termination checker Lots of duplication of work was happening, both ignoring functions that were already known to be total, and repeating checks when arguments not decreasing, now pruned.Edwin Brady f31c76aMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady a6c36d3Undo previous change until I work out why it was important...Edwin Brady e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 2a13be4Distinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon!Edwin Brady 11dbfc0Correct totality check of f=f, and add regression testEdwin Brady 449e292Tweak totality checkerEdwin Brady