git.iko.soy/Idris-dev
on 4dddfaf help sign in
history ofsrc/Idris/Coverage.hs
all commits
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 906862aFix traversal of size change graphs Fixes issue #134 - new regression test addedEdwin Brady 8d090c0A couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before doing any totality checkingEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo 20627e4Better strategy for building case trees at compile timeEdwin Brady c10146bLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call.Edwin Brady bbe9dc1Minor fixes for inlining and integer literalsEdwin Brady d90165ecoverage fix for unhandled casesraichoo a52bb30Separate compile time and run time inlinings Run time can be more aggressive - compile time needs to be careful since over aggressive inline can make the termination check harder, especially for type class instances.Edwin Brady 7438e0fDocument --warnpartial Behaviour fixed so that it doesn't report declared partial functionsEdwin Brady 3f6fd87Bring tutorial up to date with new termination checkerEdwin Brady 71a3efaLibrary now builds with "--total"Edwin Brady 9affb75Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possibleEdwin Brady f8920a0Deal with higher order recursive arguments in size change graphsEdwin Brady 54ad219Add size change termination Now deals with recursive functions (still only simple structural size changes spotted, however)Edwin Brady ebb75fbCalculate size change graphsEdwin Brady d27925cMerge branch 'master' of https://github.com/raichoo/Idris-devEdwin Brady bf8685eSeparate "productive" and "total" in totality checker Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet!Edwin Brady 30e4ed8Added simple productivity checker for coinductive definitions Recursive calls must be an argument to a coinductive constructorEdwin Brady 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady 5a6299bUnification fix Specifically to stop it filling in things which are given by the programmer (caused by a bug replacing nullary constructors with terms!)Edwin Brady 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady dc67893Remove some unused codeEdwin Brady 97e28f7Export tactic-implicit arguments properlyEdwin Brady 33baa44More on errors; propagate line numbersEdwin Brady ed72247Try to get line numbers betterEdwin Brady c7a3b59Coverage checker tweakEdwin Brady f49cd3bPass options on functions in typeclasses through to instancesEdwin Brady 9839562Fix silly error in termination checker :)Edwin Brady 7142d7eTotality checker tweaksEdwin Brady