git.iko.soy/Idris-dev
on de0bcbd help sign in
history ofsrc/Core/Evaluate.hs
all commits
93992c3Compile Nat as Int, (and plus/mult/fromInteger)Edwin Brady df41e3dGive a bit more context for error messagesEdwin Brady af4fda7%flag directiveEdwin Brady 81425d2Add skeleton of inlinerEdwin Brady 1931074Prevent io_bind reducing at REPLEdwin Brady 3fcbff5A little reorganisation of clauses elaboration To be more clear which case tree is whichEdwin 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 c182c92Allow simple function types to be reflectedEdwin Brady 6d7dc4eSimplify evaluator It tries to support too much, but since it's part of the kernel it should do as little clever stuff as possible. Now just normalises, simplifies or specialises, the latter two simply meaning that certain names are blocked from being reduced.Edwin Brady dd12ac4Remove unused code in Evaluator plus some setting up for more control in inlining - VApp now takes two copies of its argument: one fully evaluated, one with names frozen. Plan is that dictionaries (in particular) will only unfold if doing so leads to further evaluation, so we need to keep both forms.Edwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin 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 adf646eChange default specialisation behaviour to not unfold namesEdwin Brady ad66486Add %specialise annotation for functions (Part 1 of partial evaluation) %specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. The t1 part is optional, and means unlimited (which is the default for all names at the minute anyway)Edwin Brady 773e454Make ChType a member of IntTy ITChar.Jan Bessai 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 ddaf6b6Fix Haddock parser errorDavid Christiansen 633f698Take care to avoid duplicating redexes when reducing lambdas Binders in values are annotated with a 'reducible' flag, which is set to False if simplifying and the argument appears more than once.Edwin Brady e6d48b6Take care with 'let' in specialiser - avoid duplicating a redex Let now only reduces if the binding appears at most once in scope during specialisationEdwin 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 99a8a66Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked.Edwin Brady 00ae7feMerge branch 'master' into providersDavid Christiansen a807a34Remove the unused arg from lookup functionsDavid Christiansen 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