git.iko.soy/Idris-dev
on d1663cc help sign in
history ofsrc/Core/CaseTree.hs
all commits
dcd4007Normalise pattern types when typecheckingEdwin Brady 9c0cb92Better unused argument spottingEdwin Brady 521dc75Prune case trees properly on optimised NatEdwin Brady 029da07Take into account that GMP operations can move dataEdwin Brady 3c32b65Whitespace cleanup.George Leontiev 60a441bFix bug in compilation of optimised NatsEdwin Brady 93992c3Compile Nat as Int, (and plus/mult/fromInteger)Edwin Brady c182c92Allow simple function types to be reflectedEdwin Brady fd9bd68Add '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.Edwin Brady 773e454Make ChType a member of IntTy ITChar.Jan Bessai bb52adeRemove incompete(?) pattern support for SIMD valuesBenjamin Saunders 0aa3fd6Beginnings of integer SIMD support (no backend yet)Benjamin Saunders dad12e6Don't inline for compilation (because the evaluator makes bad choices) Instead, inline the compile-time representation to help the totality checker only. This can cause subexpressions to be duplicated, so should be avoided at run-time. For the run-time representation, inline later at IRTS level.Edwin Brady 45272d9Fix term size calculation for inlining Now counting binders other than Let, so lots of things previously inlined over-aggressively are now not inlined.Edwin 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 490c22aBasically working executor/interpreterDavid Christiansen edfe5b3Strip impossible cases when building case treesEdwin Brady adf51f4Make Haddock able to parse Idris's sourceDavid Christiansen 4c5b1bdMerge branch 'master' into bitstringBenjamin Saunders 75e7758Some progress on implementation paper revisionsEdwin Brady e5706d3HNF in unification to speed things upEdwin Brady 41f3d97Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstringBenjamin Saunders e2807a1Verified numbersBenjamin Saunders b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders 4bc6424Compile on GHC 7.0Seo Sanghyeon 449e292Tweak totality checkerEdwin 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 267f044Improve case compilation by checking most distinct argument firstEdwin Brady bbbe563Merge pull request #114 from raichoo/wordEdwin Brady f6451efword 8/16 primitive typesraichoo 06283b6Improve evaluation of projection By caching result of evaluation, so that it's already evaluated when next projection happens.Edwin Brady 20627e4Better strategy for building case trees at compile timeEdwin Brady 7af45b4Fix error in case tree optimisation (hence fix issue #70)Edwin Brady 2856967Normalise LHS before compilation ...otherwise in some situations the forcing optimisation may lead to uncompilable codeEdwin Brady 64fc043Fix overenthuiastic unused argument removal problem (Wasn't checking case analysis where the scrutinee was the result of a projection)Edwin Brady 2616a69Fix call graph generationEdwin Brady 449bb27Fix allocation of big integersEdwin Brady 29c67e9Pattern matching on strings, big integers and charactersEdwin Brady 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 9e58e28Type safe message passing concurrencyEdwin 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 ebb75fbCalculate size change graphsEdwin Brady fb2b17dAdd collapsing optimisation and more aggressive erasureEdwin 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 76442a7Better rendering of case trees in debug infoEdwin Brady 72d4d96Starting unused argument analysisEdwin Brady 6d7c9bcCall graph changeEdwin Brady 0f957f6Add Proj operator to runtime version of TT Allows extracting arguments without checking constructor first which will make erasing unused values easier shortlyEdwin Brady 0679225Tweak match compilation (right to left, rather than l to r) Now matches on values before indices, to give a chance of erasing indices.Edwin Brady