git.iko.soy/Idris-dev
on 4e7a0ee help sign in
history ofsrc/IRTS/Compiler.hs
all commits
f675e05Add CodegenInfo structure, give CGs uniform typesEdwin Brady d763c9cUse postulates for decEq primitive proofsEdwin Brady 3cef609Annotate 'Lazy' with reason for lazinessEdwin Brady d4ffc21Add ManagedPtr typeEdwin Brady e175b1ajavascript: use %include directive to include external javascript filesraichoo fb3c24cMake EVAL and APPLY smallerEdwin Brady 130f437Remove | annotation, make Force/Delay implicitEdwin Brady 57af985Add 'force' (opposite of 'lazy')Edwin Brady 6eee6c8Add assert_total functionEdwin Brady 9e350acInline assert_smaller correctlyEdwin Brady e9c9297Make lookupCtxtExact return Maybe instead of ListDavid Raymond Christiansen 46e894dUse Data.Text for variable namesEdwin Brady 7604451Cache argument types for building case treesEdwin Brady 0f97368Merge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna b3bf956When specialising, reduce more namesEdwin Brady 9c0cb92Better unused argument spottingEdwin Brady 521dc75Prune case trees properly on optimised NatEdwin Brady 3c32b65Whitespace cleanup.George Leontiev f34f0afBetter display of metavariable types in :tEdwin Brady b9a3a69Fix missing case in Defunctionalise.hsEdwin Brady b5eee09Convert IO errors into erros in the Idris monadDavid Christiansen 53b28e6Update compiler to use new error handlingDavid Christiansen 60a441bFix bug in compilation of optimised NatsEdwin Brady 93992c3Compile Nat as Int, (and plus/mult/fromInteger)Edwin Brady e8f4bb1Some packaging fixesEdwin Brady af4fda7%flag directiveEdwin 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 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 8eb2087Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325Edwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin Brady 2311d55rename O into Zraichoo 68c5bb7Merge pull request #390 from Ralith/vector-ftypesEdwin Brady d9e7912FTy convenience names for fixed-width intsBenjamin Saunders f0c1e19Vector FFI and bitcastsBenjamin Saunders 7eaa86aMake LLVM optional but the defaultNiklas Larsson 773e454Make ChType a member of IntTy ITChar.Jan Bessai 0aa3fd6Beginnings of integer SIMD support (no backend yet)Benjamin Saunders 7b6448eOptimization level selectionBenjamin Saunders f149970Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of hostBenjamin Saunders 0cbc384Merge branch 'llvm3' of https://github.com/Ralith/Idris-dev into Ralith-llvm3Edwin Brady 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 14ee023Skeleton of stub-generating LLVM codegenBenjamin Saunders eacfe5cAdded backend target specification to %lib, %link and %include directivesJan Bessai 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 e4fc71aMerge pull request #322 from raichoo/javascriptEdwin 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 2613689javascript: make FFI work with HOFsraichoo 1cf8b7bRevert "Revert "Merge pull request #294 from bitlisp/unified-int-primitives""David Christiansen 05895a5Revert "Merge pull request #294 from bitlisp/unified-int-primitives"Edwin Brady