Commit Graph

17 Commits

Author SHA1 Message Date
Edwin Brady
078b5be85f
Merge pull request #144 from sysvinit/debug-trace
Port Debug.Trace from Idris 1
2019-12-06 10:38:28 +00:00
Edwin Brady
aae3d0f718 Reorganise Language.Reflection modules 2019-11-30 13:23:03 +00:00
Molly Miller
0fb873949f Implement Debug.Trace, from Idris 1's base package 2019-10-28 20:23:11 +00:00
Edwin Brady
8975eeafb7 Make a start on reflection 2019-08-27 15:49:21 +01:00
Alex Gryzlov
b9b41dea40 port Data.List 2019-07-24 16:11:27 +03:00
Edwin Brady
623024d179
Merge pull request #28 from jfdm/add-either
Inclusion of Either within Base.
2019-07-18 20:31:51 +01:00
Jan de Muijnck-Hughes
5823d6b294 Inclusion of Either within Base.
Straightforward port of Either from Idris to Idris2.
2019-07-18 16:32:19 +01:00
David Smith
96ec5f6b3a Add Data.Morphisms to base 2019-07-18 14:46:59 +01:00
Edwin Brady
fd4f90e331 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 20:18:40 +02:00
Edwin Brady
1cc097aefc Add Data.Primitives.Views 2019-07-08 22:11:34 +02:00
Edwin Brady
2967a19963 Add more stream functions to Data.Stream 2019-07-08 18:10:47 +02:00
Edwin Brady
11199acab6 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 12:55:55 +02:00
Edwin Brady
0f56c239c2 Parse pattern matching lambda
This is now enough for Chapter 5 tests to work
2019-07-03 13:04:25 +01:00
Edwin Brady
00514887c4 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-06-30 23:54:50 +01:00
Edwin Brady
577b68dd5a Make a start on Data.Vect 2019-06-30 17:38:40 +01:00
Edwin Brady
f37da6c5b7 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 15:50:58 +01:00
Edwin Brady
c121910298 Add 'base' libraries 2019-06-15 11:54:22 +01:00