idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-28 06:05:56 +03:00
Code Issues Projects Releases Wiki Activity
803 Commits 6 Branches 9 Tags 116 MiB
fc6b184106
Commit Graph

803 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
7a0b25f994
Merge pull request #369 from cypheon/tailrec-unpack 
Make Prelude.unpack tail-recursive
 2020-07-05 14:11:02 +01:00
Edwin Brady
a9478875b3
Merge pull request #392 from buzden/append-properties 
Injectivity and similar properties were added for lists'a append
 2020-07-05 14:08:07 +01:00
Edwin Brady
e3dcc2da1b
Merge pull request #354 from stepancheg/generated 
Insert @generated marker into generated Scheme files
 2020-07-05 14:05:22 +01:00
Edwin Brady
5487290499
Merge pull request #282 from ether42/master 
Fix MkRecord signature
 2020-07-05 14:03:57 +01:00
Edwin Brady
9d1bb82c48
Merge pull request #242 from nickdrozd/algebra 
Add Algebra interfaces and laws
 2020-07-05 00:04:13 +01:00
Edwin Brady
2321513b86
Merge pull request #410 from edwinb/import-revise 
A variety of namespace and import goodies
 2020-07-05 00:02:36 +01:00
Edwin Brady
4c5d26f050 Add note on import...as to tutorial 2020-07-04 23:30:13 +01:00
Edwin Brady
6bb6ced43a Remove name visibility check 
It doesn't seem to serve any useful purpose, other than to annoy!
 2020-07-04 23:12:15 +01:00
Edwin Brady
950431a9ce Note in tutorial on qualified do 2020-07-04 23:12:03 +01:00
Edwin Brady
2ce0335fd5 Implement qualified do 
This allows do blocks to be qualified with the namespace that the (>>=)
operator is defined in. Inspired by Purescript's version of the same
thing, and this ghc proposal:
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0216-qualified-do.rst
 2020-07-04 23:01:43 +01:00
Edwin Brady
a5c9250524 Update bootstrap scheme 
This is needed because the existing version won't build the Prelude
correctly as it doesn't do import...as correctly.

I don't believe this affects Idris2-boot, since it has its own Prelude.
 2020-07-04 22:10:44 +01:00
Edwin Brady
45a9668370 Export all of the Prelude as Prelude 
There is an argument that, for import public, this should be automatic
(that is, the publicly imported things should be reexported with the
parent namespace). I decided not to do this, because another use of
import public which we do a lot in the Idris 2 code base is purely as a
convenience, where we still expect things to be in their original
namespace.
Also, where there's a choice between things being explicit and implicit,
I prefer to err on the side of explicit now.
So, if what you really want in an API is to reexport, you can do that,
but explicitly.
 2020-07-04 21:57:54 +01:00
Edwin Brady
3a343e434b Don't add an alias if the name already exists 
This way, a name in a module overrides the name in a module it imports,
if it's imported via "import ... as".
 2020-07-04 21:54:42 +01:00
Edwin Brady
f60ae32242 Better implementation of %hide 
Instead of setting the name as private, make sure it doesn't appear in
lookups at all. That is, truly hide it!
 2020-07-04 21:38:35 +01:00
Edwin Brady
c1ed3c2fc8 Don't reload hints on import as 
We only need to reload the defined names so that we can set up the
aliases - everything else is already loaded, and in particular adding
hints twice will break implicit search.
 2020-07-04 21:25:41 +01:00
Edwin Brady
028624a18d Add "import X as Y" properly 
Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".
 2020-07-04 20:26:49 +01:00
Edwin Brady
3a41ccb612 Only save interfaces defined in current file 
It wasn't a noticeable cost, but this is tidier.
 2020-07-04 17:48:01 +01:00
Jan de Muijnck-Hughes
874236aac0 A port of Subset and Exists from Idris1. 
The ports are rather straight forward and I have purposefully written
the documentation to be beginner friendly.

Note, I have diverged from Idris1 over the naming of the projection
functions to make them consistent with `Pair` and `DPair`.
 2020-07-04 11:03:14 +01:00
Alex Gryzlov
afde930e7a
Vect updates (#335) 2020-07-04 11:02:04 +01:00
Niklas Larsson
71db21b19d
Merge pull request #406 from andrevidela/add-log-option 
Add support for --log flag
 2020-07-04 11:20:42 +02:00
André Videla
d52030a7fc Add support for --log flag 
The flag takes a natural number as argument
It would be ideal to generalise the argument parser to be able
to parse any argument of any type, but right now we only add
`RequiredNat` as a new flag option.
 2020-07-03 18:12:17 +01:00
Guillaume ALLAIS
bd14d37ddc [ fix ] make some exports public 2020-07-03 12:01:09 +01:00
Jan de Muijnck-Hughes
5abf053818 Fixed visibility of some list functions. 2020-07-03 11:59:55 +01:00
Niklas Larsson
c0e535516c
Merge pull request #380 from chrrasmussen/add-docs-about-dirs 
Add documentation for sourcedir/builddir/outputdir
 2020-07-02 00:16:23 +02:00
Niklas Larsson
3507512e49
Merge pull request #401 from melted/buffer_has_io 
Convert Data.Buffer to HasIO
 2020-07-02 00:01:28 +02:00
Christian Rasmussen
b4ba476c8a
Merge branch 'master' into add-docs-about-dirs 2020-07-01 23:51:40 +02:00
Niklas Larsson
f54ebcb3b1
Merge pull request #391 from ska80/upd-docs 
Update docs
 2020-07-01 23:47:16 +02:00
Niklas Larsson
6673f49731 Convert Data.Buffer to HasIO 2020-07-01 23:33:30 +02:00
André Videla
5996361488
Update INSTALL.md 
Fix typo on INSTALL.md
 2020-07-01 18:15:49 +01:00
André Videla
cec56561c6
Merge pull request #387 from LibreCybernetics/fix-export-vect 
Make Applicative implementation of Vect n public export.
 2020-07-01 17:26:08 +01:00
Edwin Brady
c4d56e5481
Merge pull request #396 from edwinb/lazy-lazy 
Don't commit to a Force too early
 2020-07-01 12:29:52 +01:00
Edwin Brady
e7830b2b40 Merge github.com:idris-lang/Idris2 into lazy-lazy 2020-07-01 11:59:35 +01:00
Edwin Brady
c216e1c560 Update test output 2020-07-01 11:53:06 +01:00
Edwin Brady
0d4db3ee75 Add 'force' and 'delay' as functions 
Since Force and Delay are keywords now, these may help in higher order
cases in particular.
 2020-07-01 11:35:27 +01:00
Edwin Brady
669e50ff55 Remove my debugging noise from test case 2020-07-01 00:43:33 +01:00
Edwin Brady
25491060e2 Don't commit to a Force too early 
If we have a delayed thing, but we don't yet know the expected type,
don't commit to forcing because the expected type might turn out to be a
delay.
Fixes #395
 2020-07-01 00:40:44 +01:00
Mark Barbone
4916dd23a9
Make Data.Vect linear (#333) 2020-06-30 15:05:19 +01:00
Denis Buzdalov
77f1d69acb Injectivity and similar properties were added for lists'a append. 2020-06-30 17:00:47 +03:00
Kamil Shakirov
f094a52ba9 Update docs 2020-06-30 18:44:36 +06:00
Denis Buzdalov
df60e07962 List's snoc injectivity property was renamed approporiately. 2020-06-30 13:18:42 +01:00
Edwin Brady
393c1ed464
Merge pull request #388 from edwinb/samples-dir 
Copy samples directory from Idris2-boot
 2020-06-30 11:23:40 +01:00
Edwin Brady
4f10bfcfd2 Copy samples directory from Idris2-boot 
This is referred to in the documentation, so should be there
 2020-06-30 10:51:09 +01:00
Fabián Heredia Montiel
e488c6cf0e Make applicative implementation of Vect public export 2020-06-29 18:27:57 -05:00
Niklas Larsson
53621f84c5
Merge pull request #370 from ShinKage/ansi 
Adds ANSI codes support in contrib
 2020-06-29 19:43:46 +02:00
Edwin Brady
a35965be84
Merge pull request #384 from edwinb/unify-invert 
Use 'unify' rather than 'convert' if possible
 2020-06-29 16:22:31 +01:00
Edwin Brady
a52308d77d Add test files 2020-06-29 15:13:42 +01:00
Edwin Brady
ffbea6d160 Use 'unify' rather than 'convert' if possible 
'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes #66.
 2020-06-29 15:04:32 +01:00
Edwin Brady
84477adfc9
Merge pull request #383 from edwinb/coverwhere 
Pay attention to nested names in coverage check
 2020-06-29 13:52:32 +01:00
Edwin Brady
b2da2fe558 Pay attention to nested names in coverage check 
Fixes #164
 2020-06-29 13:27:00 +01:00
Niklas Larsson
4db58171f9
Merge pull request #381 from chrrasmussen/avoid-traversing-modules-twice 
Avoid traversing all Idris modules twice when installing
 2020-06-29 12:03:08 +02:00