Edwin Brady
69f3c23cbb
Treat local hints differently in auto search
...
Local hints need to reduce (just like global hints do) so we expand
their definition to the lifted name before applying them.
We're identifying the global hints by knowing that the binder name is a
nested function name. This is a bit of hack, and it'd probably be better
to record that information in the binder instead, but that's a more
substantial change than I want to do right now.
2020-12-27 13:41:48 +00:00
alissa42
02e12a82cf
Adding default implementation of Foldable.null
2020-12-24 08:49:32 +00:00
Michael Messer
7dc84696a3
If the width terminal is zero make it Unbounded ( #870 )
2020-12-23 16:55:36 +00:00
André Videla
9c400a185e
Add Traversable to List1
2020-12-21 15:10:00 +00:00
Denis Buzdalov
60e9cf44b0
Add List, LazyList and Stream unfolds and some LazyList's functions
2020-12-18 22:54:03 +00:00
Lynn
681c1bf10f
Install hint for Apple Silicon ( closes #836 )
2020-12-18 15:07:35 +00:00
Denis Buzdalov
bff74807fd
Some functions, mostly for lazy lists ( #854 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2020-12-18 10:33:56 +00:00
tensorknower69
aa940c3d18
change runState's signature
2020-12-17 10:10:18 +00:00
tensorknower69
c48b1e090e
add execStateT and evalStateT
2020-12-17 10:10:18 +00:00
raptazure
043faf8baf
docs: fix grammar
2020-12-16 10:02:34 +00:00
Edwin Brady
771e4034fa
Merge pull request #846 from edwinb/interfaces
...
Local hints (basic version)
2020-12-14 14:46:18 +00:00
Edwin Brady
6c9ad81c12
Add missing test
...
:# ../../../src/Compiler/.ANF.idr.swp
2020-12-14 13:38:40 +00:00
Edwin Brady
c1f58d963f
Merge branch 'master' into interfaces
2020-12-14 13:34:31 +00:00
Edwin Brady
252292451f
Add local hints (basic version)
...
This gives us the ability to define and use implementations locally, in
where clauses/local let bindings, as well as flag local definitions as
hints.
It's not yet quite equivalent to global hints, however, since it translated
the hint to a local let binding, which doesn't reduce, so if something
relies on the reduction behaviour of the hint, it won't work. This
refinement is coming later
2020-12-14 13:25:50 +00:00
Mathew Polzin
a7e0df1300
Merge branch 'master' into scratch-work-search-repl
2020-12-13 17:05:54 -08:00
Mathew Polzin
e16ad58d6e
allow unification over holes in saarch and branch defs at start of process to restore at the end.
2020-12-13 17:03:35 -08:00
Wen Kokke
daff1f2fb8
Added assert_linear. ( #844 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-12-13 16:06:18 +00:00
G. Allais
3f6b99e979
[ fix #657 ] RigCount for interface parameters ( #808 )
2020-12-11 11:58:26 +00:00
Dong Tsing-hsuen
88aa55e875
[ new ] null method in Foldable ( #832 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-12-10 18:04:23 +00:00
Guillaume ALLAIS
4356d377c5
[ refactor ] parser for lambda & lambdacase
2020-12-10 18:01:14 +00:00
Guillaume ALLAIS
4025896572
[ fix #833 , #677 ] bound variables start with a lowercase letter
2020-12-10 18:01:14 +00:00
Guillaume ALLAIS
0a685f8d2c
[ debug ] remove max from log
...
Users should be allowed to de-escalate the level of detail they're
getting.
2020-12-10 14:27:02 +00:00
Mathew Polzin
8206945efb
got a number of things matching using unify, but still not totally happy with the result. might need to reivest in just dropping implicits and comparing on local names.
2020-12-08 20:47:52 -08:00
Guillaume ALLAIS
5de647cc3f
[ refactor ] use difference list for efficient append
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
0675e58cca
[ error ] crash rather than generating garbage
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
89daa5c1f6
[ cleanup ] existing list function & needlessly effectfule ones
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
3c0ff432bd
[ cleanup ] redundant parens, language keyword
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
243ed5df2c
[ cleanup ] remove trailing "pure ()"
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
39f26e7ed6
[ minor ] avoid repetition
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
f8c248dc7a
[ refactor ] introduce Core.update
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
e5c6dfac5b
[ refactor ] remove toString, natMinus
...
* toString is an inefficient fastPack
* natMinus is an inefficient minus (we have already checked isLTE)
2020-12-08 13:07:53 +00:00
Guillaume ALLAIS
98674fc40a
[ cleanup ] use pattern-matching binds in monadic code
2020-12-08 13:07:53 +00:00
Denis Buzdalov
a1b624a3bc
Tiny fix of the formatting in the recently added documentation.
2020-12-08 08:56:38 +00:00
Mathew Polzin
1ed79cd7ed
got it finding some things by type. can't deal with out-of-order implicits yet.
2020-12-07 19:12:43 -08:00
Fabián Heredia Montiel
87358f19da
Increase timings of concurrency tests due to flaky windows runs
2020-12-07 21:20:09 +00:00
Ruslan Feizerahmanov
1dba32a0c4
[ doc ] new application syntax ( #820 )
2020-12-07 18:59:49 +00:00
Jan de Muijnck-Hughes
3a6e779acf
Extended Literate support to include LaTeX.
2020-12-07 14:54:35 +00:00
Jan de Muijnck-Hughes
9c5198cde3
Fixed docs and improved Literate mode.
...
+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
2020-12-07 14:54:35 +00:00
Nicolas A. Schmidt
ef6cbcf658
Auto-implicit __con now added before implicits. ( #659 )
2020-12-07 11:41:47 +00:00
Denis Buzdalov
b3542d66fc
Have lambda-case available everywhere lambda is ( #819 )
2020-12-07 11:34:48 +00:00
Guillaume ALLAIS
d30e984137
[ debug ] Give the option to log off
2020-12-07 11:33:37 +00:00
David Smith
c6abab438c
export a function to parse ipkg files ( #822 )
2020-12-07 10:53:01 +00:00
Andy Lok
9f72a514f1
Rename startWith to isBaseOf
2020-12-07 15:26:00 +08:00
Andy Lok
5578761bdb
Improve splitPath
2020-12-07 05:19:53 +08:00
Andy Lok
d3a74e0199
Update document
2020-12-07 04:27:54 +08:00
Andy Lok
f5e0853264
Refactor Utils.Path
2020-12-07 04:16:28 +08:00
Andy Lok
8eea90527a
Refactor System.Path
2020-12-07 04:10:15 +08:00
Edwin Brady
63a46722ef
Force/Delay need to be inlined in Builtins
...
Otherwise (especially in the case of delay) the argument might be
evaluated prematurely.
2020-12-06 20:00:48 +00:00
Andor Penzes
aeab632c7e
[doc] JS FFI examples.
2020-12-06 19:07:34 +00:00
Andy Lok
9e22a6e07b
Add javascript FFI for fastUnpack ( #816 )
2020-12-06 09:54:58 +00:00
