Branch: master
Commits on Apr 9, 2015
  1. Fix default for execonly and Nix build

    puffnfresh committed Apr 9, 2015
Commits on Jan 25, 2015
  1. Add IDRIS_LIBRARY_PATH environment variable

    puffnfresh committed Jan 25, 2015
    Allows specifying where to find Idris libraries.
    After doing a build, you can even point Idris to the repo's lib path:
        IDRIS_LIBRARY_PATH=libs dist/build/idris/idris
Commits on Jul 11, 2014
  1. Add Ord instance for Bool

    puffnfresh committed Jul 11, 2014
Commits on Jul 6, 2014
  1. Remove bad Applicative constraints from neweffects

    puffnfresh committed Jul 6, 2014
Commits on Apr 27, 2014
  1. Remove whitespace for :addproof - like :load does

    puffnfresh committed Apr 27, 2014
    This should probably happen for all commands which take a filename.
Commits on Apr 21, 2014
  1. --link and --include give flags, not directories

    puffnfresh committed Apr 21, 2014
  2. Make completeCmd total

    puffnfresh committed Apr 21, 2014
Commits on Apr 14, 2014
  1. Add instance Uninhabited _|_

    puffnfresh committed Apr 14, 2014
Commits on Apr 12, 2014
  1. Add Foldable for SortedSet

    puffnfresh committed Apr 12, 2014
  2. Remove Ord constraints from SortedMap toList

    puffnfresh committed Apr 12, 2014
Commits on Apr 6, 2014
  1. Make parsing respect the nocolour flag

    puffnfresh committed Apr 6, 2014
    This fixes #1034
Commits on Feb 10, 2014
  1. Execute JavaScript output after DOMContentLoaded

    puffnfresh committed Feb 10, 2014
    Previously, JavaScript generated for the browser would only execute on
    the DOMContentLoaded event. We should also check if the browser is
    already ready. We can do this with the following:
        document.readyState == "complete" || document.readyState == "loaded"
Commits on Jan 4, 2014
  1. Fix SimpleParser ambiguous type error

    puffnfresh committed Jan 4, 2014
Commits on Dec 22, 2013
  1. Make dumping of default superclass instances consistent

    puffnfresh committed Dec 22, 2013
  2. Make :info show default superclass instances

    puffnfresh committed Dec 22, 2013
Commits on Dec 19, 2013
  1. Fix LLVM compilation error because of moved `getCC`

    puffnfresh committed Dec 19, 2013
  2. Merge branch 'master' into cabal-library

    puffnfresh committed Dec 19, 2013
Commits on Dec 11, 2013
  1. Default superclass intances

    puffnfresh committed Dec 11, 2013
    This allows code like:
        data Identity i = Id i
        class Functor (f : Type -> Type) where
          map : (a -> b) -> f a -> f b
        class Functor f => Applicative (f : Type -> Type) where
          instance Functor f where
            map f fa = ap (pure f) fa
          pure : a -> f a
          ap : f (a -> b) -> f a -> f b
        instance Applicative Identity where
          pure = Id
          ap (Id f) (Id a) = Id (f a)
        data Nat = Z
                 | S Nat
        x : Identity Nat
        x = map S (Id Z)
    Note the default Functor instance defined as part of the Applicative
    class. This allows the Identity data type to omit an explicit Functor
    instance and one gets defined from the Applicative instance.
    This feature is largely copied from the approach done in She:
    It basically does macro expansion of each default superclass instance
    (e.g. Functor) when the containing class (e.g. Applicative) gets an
    instance defined. Currently, default superclass instance definitions
    are not type-checked, only their macro expansions are.
    Default superclass instances are limited to being defined for types
    which are syntactically equal to one of the superclass constraints.
Commits on Dec 2, 2013
Commits on Nov 30, 2013
  1. Move externally useful Util.System functions to IRTS.System

    puffnfresh committed Nov 30, 2013
    Functions moved:
    * getTargetDir
    * getCC
    * getLibFlags
    * getIdrisLibDir
    * getIncFlags
    * getMvn
    * getExecutablePom
  2. Replace partial `showDeclImp` function with total `dumpDecl`

    puffnfresh committed Nov 30, 2013
    Remove original `dumpDecl` and replace call to `dumpDecls` with call
    to `showDecls True`.
Commits on Nov 29, 2013
  1. Use `showCG` instead of `show` when loading package names

    puffnfresh committed Nov 29, 2013
    `showCG` is for showing names, but for code generation
    `show` is for showing names, but human readable
    At the moment these do the same for namespaces but we probably
    shouldn't rely on that.
  2. Merge branch 'master' into cabal-library

    puffnfresh committed Nov 29, 2013
  3. Add a Cabal library

    puffnfresh committed Nov 29, 2013
    Moves Core to Idris.Core
    The library allows using the Idris' backend from other Haskell code.
    For example, we could use Idris as a general TT compiler with multiple
        run :: Idris ()
        run = do
          let ddir = "libs" -- TODO: Use Idris.Util
          addImportDir $ ddir </> "prelude"
          addImportDir $ ddir </> "base"
          _ <- loadModule stdout "Builtins"
          _ <- loadModule stdout "Prelude"
          pterm <- fmap (flip delab program) getIState
          elabDecls toplevel [makeDecl pterm]
          compile ViaNode "wow.js" runProgram
    Everything but Main, Util, Pkg and Paths_idris is currently exported.