git.iko.soy/Idris-dev
on baff441 help sign in
history ofsrc/Idris/REPL.hs
all commits
75e0141add command to change current directoryHannes Mehnert a029bd8reduce duplication by providing a show instance for CmdArgHannes Mehnert ab498e9Add syntax for language extensions and turn off type providers by defaultDavid Christiansen 161ef3dMerge remote-tracking branch 'upstream/master' into providersDavid Christiansen 228ffdbquiet mode: for editorsraichoo 3262127Dynamically load C libraries in REPLDavid Christiansen 82190d3Basics of command to execute IO actions in the interpreterDavid Christiansen 2297270unify help and completion of REPL - previously they were not in sync, now it is one lookup tableHannes Mehnert 306a451Reformat existing comments for Haddock and add Haddock commentsDavid Christiansen c020e50javascript: split javascript and node targetraichoo 52203a3Complete tactic names in proverDavid Christiansen cc80288Rename the REPL's Haskeline uses to make them obviously REPL-specificDavid Christiansen 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen cc3c913Complete arguments of commands (though slightly crudely)David Christiansen fc58a50Simple completion supportDavid Christiansen e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 2a13be4Distinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon!Edwin Brady a6ed7c3javascript: got rid of --javascript use --targetraichoo 7a66adcMake unification faster by computing HNF rather than normalisingEdwin Brady 59be497javascript backendraichoo 12dcee5Merge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascriptIrene Knapp 06fffa3JavaScript stuff.Irene Knapp e3d393cAdded the ability to dump bytecode to a fileDaniel Waterworth 5d4c45fWhitespace fixDaniel Waterworth 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