git.iko.soy/Idris-dev
on aa7262e help sign in
history ofsrc/Idris/REPL.hs
all commits
fab5d73Adding support for Windows MingW32chetant f50f006Expand backend control options and infrastructureBenjamin Saunders 0b3b0b5Display useful information on :doc (It's ugly though...)Edwin Brady 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin 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 665676bAdded :l and :m commands to REPLEdwin Brady 15fc297Merge branch 'master' of https://github.com/edwinb/Idris-devJason Dagit a41fe5bUse strict StateTJason Dagit 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 5c9a88auppercase modulenamesraichoo 997a982Added --total and --partial command line optionsEdwin Brady f2af303:addproof now adds most recent proof if no argument given Consistent with old behaviour, and with tutorialEdwin Brady 3c641aeAdded --dumpdefuns flagEdwin 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 72d4d96Starting unused argument analysisEdwin Brady 6d7c9bcCall graph changeEdwin Brady 4ff3b25Added --dumpc flagEdwin Brady bb76c6cMore aggressive simplification; fix case generation bugEdwin Brady 1e52324Added simple library packaging system Now used for the prelude (see lib/base.ipkg)Edwin Brady 2832517Move main setup code to Idris.REPLEdwin Brady 16a6c95Set up for adding new compiler back ends more easilyEdwin Brady 34e8788Added Util.System for compatibility (thanks to Dirk Ullrich)Edwin Brady ef1d7baMerge pull request #48 from raichoo/masterEdwin Brady 7cdb0c0Removed Epic dependencyEdwin Brady f959008New RTS in placeEdwin Brady 6b46ffcNew RTS almost ready, but for garbage collection problemEdwin Brady b642db5Almost working new back endEdwin Brady 7f2d76cenhanced proof handelingraichoo b8815e2added proof listraichoo c30e6ceNo need to qualify unambiguous names on :pEdwin Brady 0887715Output C file (not finished...)Edwin Brady fa0ecdeStarted C generationEdwin Brady 11a8847Add PreC, for an imperative intermediate form that should be easy to generate code fromEdwin Brady 782d0f7put toSC in the right placeEdwin Brady 6554c7dTowards primitives in new VMEdwin Brady c07696dSome new bytecode compilingEdwin Brady 541faf5New lambda lifter, and debug info in replEdwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady 2899286An introductionEdwin Brady b01a78eQuick hack at :info for exploring type classesEdwin Brady a678b80:t prints all names, rather than checking for unique nameEdwin Brady dca8f9fNormalise types before applying forcingEdwin Brady 4bcfa68Tinker with specialisationEdwin Brady 00d7c69Work towards making {static} arguments and specialisation work properlyEdwin Brady 1b7d089Recheck totality after an interactive proofEdwin Brady 9864c25Add :total commandEdwin Brady b1e95cbFix coverage checkerEdwin Brady