Idris2-boot/libs/base/base.ipkg

package base

modules = Control.Monad.Identity,
          Control.Monad.State,
          Control.Monad.Trans,
          Control.WellFounded,

          Data.Buffer,
          Data.Either,
          Data.Fin,
          Data.IORef,
          Data.List,
          Data.List.Views,
          Data.Maybe,
          Data.Morphisms,
          Data.Nat,
          Data.Nat.Views,
          Data.Primitives.Views,
          Data.So,
          Data.Stream,
          Data.Strings,
          Data.Vect,

          Decidable.Equality,

          System,
          System.Concurrency.Raw,
          System.File,
          System.REPL
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`package base`

Add some Control.Monad things This required a small change to auto implicit search (and I'm still not sure about this). Now search arguments right to left, because solving later arguments may resolve earlier arguments by unification and this can happen in particular when chasing parent interfaces (which may have fewer parameters). 2019-07-10 21:18:40 +03:00			`modules = Control.Monad.Identity,`
			`Control.Monad.State,`
			`Control.Monad.Trans,`
			`Control.WellFounded,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00
			`Data.Buffer,`
Inclusion of Either within Base. Straightforward port of Either from Idris to Idris2. 2019-07-18 18:32:19 +03:00			`Data.Either,`
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway). 2019-07-01 01:54:50 +03:00			`Data.Fin,`
Add Data.Primitives.Views 2019-07-08 23:11:34 +03:00			`Data.IORef,`
Improve 'with' implementation Now supports with applications on the RHS when auto implicits are involved. Auto implicit bound names in patterns now become searches on the rhs in a with-application (I should write this construct up properly in a paper some time!) 2019-07-08 13:55:55 +03:00			`Data.List,`
			`Data.List.Views,`
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway). 2019-07-01 01:54:50 +03:00			`Data.Maybe,`
Add Data.Morphisms to base 2019-07-18 16:46:06 +03:00			`Data.Morphisms,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`Data.Nat,`
Improve 'with' implementation Now supports with applications on the RHS when auto implicits are involved. Auto implicit bound names in patterns now become searches on the rhs in a with-application (I should write this construct up properly in a paper some time!) 2019-07-08 13:55:55 +03:00			`Data.Nat.Views,`
Add Data.Primitives.Views 2019-07-08 23:11:34 +03:00			`Data.Primitives.Views,`
Parse pattern matching lambda This is now enough for Chapter 5 tests to work 2019-07-03 15:04:25 +03:00			`Data.So,`
Add more stream functions to Data.Stream 2019-07-08 19:10:47 +03:00			`Data.Stream,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`Data.Strings,`
Make a start on Data.Vect 2019-06-30 19:38:40 +03:00			`Data.Vect,`
Inclusion of Either within Base. Straightforward port of Either from Idris to Idris2. 2019-07-18 18:32:19 +03:00
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway). 2019-07-01 01:54:50 +03:00			`Decidable.Equality,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00
			`System,`
			`System.Concurrency.Raw,`
Start adding tests for TypeDD book Also detailing any changes needed to the code. Added primitives for Doubles, and repl/replWith to get Chapter 2 code to work. 2019-06-30 17:50:58 +03:00			`System.File,`
			`System.REPL`