git.iko.soy/Idris-dev
on ff0fbfa help sign in
history ofsrc/Idris/Coverage.hs
all commits
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 b1e95cbFix coverage checkerEdwin Brady 7fb7decImproved termination check (gets ackermann now, but still no mutual recursive definitions)Edwin Brady 98be75cAdded (experimentally) auto implicit argumentsEdwin Brady fc6eb53Bug fixes; checking type names in data declsEdwin Brady de6bb41Added 'total' keyword and positivity checkEdwin Brady ae4be75Well founded recursion checkEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady 60c4ef9Added 'impossible' keywordEdwin Brady