git.iko.soy/Idris-dev
on d66da21 help sign in
history ofsrc/Idris/Coverage.hs
all commits
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 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