git.iko.soy/Idris-dev
on ff0fbfa help sign in
history ofsrc/Core/Evaluate.hs
all commits
490c22aBasically working executor/interpreterDavid Christiansen e3a4097Fix eta problemEdwin Brady 21f2ce3evTree does not handle ImpossibleCaseraichoo 22c355aDocumentation comment additionsDavid Christiansen 306a451Reformat existing comments for Haddock and add Haddock commentsDavid Christiansen 4c5b1bdMerge branch 'master' into bitstringBenjamin Saunders e5706d3HNF in unification to speed things upEdwin Brady 41f3d97Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstringBenjamin Saunders 70aa358Removed the stack depth limit from Core.Evaluate.Luke Palmer 2acbdf6Small conversion changeEdwin Brady 7a66adcMake unification faster by computing HNF rather than normalisingEdwin Brady e2807a1Verified numbersBenjamin Saunders b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders 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 7245290Some tiny RTS optimisationsEdwin 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 bbe9dc1Minor fixes for inlining and integer literalsEdwin Brady 64fc043Fix overenthuiastic unused argument removal problem (Wasn't checking case analysis where the scrutinee was the result of a projection)Edwin Brady 56223efDon't normalise everywhere!Edwin 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 7508b64'par' primitive in builtins (not yet implemented)Edwin Brady 2541a16No need to store original patternsEdwin 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 54ad219Add size change termination Now deals with recursive functions (still only simple structural size changes spotted, however)Edwin 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 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin 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 bb76c6cMore aggressive simplification; fix case generation bugEdwin Brady 16027ddFix with parsing bugEdwin Brady 6b46ffcNew RTS almost ready, but for garbage collection problemEdwin Brady c30e6ceNo need to qualify unambiguous names on :pEdwin Brady 19495edCheck patterns are inaccessibleEdwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady dca8f9fNormalise types before applying forcingEdwin Brady 3f13043Make compile time evaluator take advantage of laziness again (And update test001 to catch it if it goes wrong again)Edwin Brady cd38cefEvaluator tinkeringEdwin Brady a5b7eedAdded a 'boredom threshold' to the evaluator If it takes too long (probably because it's evaluating a non-terminating function) just returns the input. This is hopefully temporary until the totality checker works better...Edwin Brady 4bcfa68Tinker with specialisationEdwin Brady 09f2abdFix let overloading bug with do blocksEdwin Brady 00d7c69Work towards making {static} arguments and specialisation work properlyEdwin Brady 7142d7eTotality checker tweaksEdwin Brady 7fb7decImproved termination check (gets ackermann now, but still no mutual recursive definitions)Edwin Brady 392c225Check definitions structurally as well as by name in conversionEdwin Brady fc6eb53Bug fixes; checking type names in data declsEdwin Brady