idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 08:42:11 +03:00
Code Issues Projects Releases Wiki Activity
1,053 Commits 6 Branches 9 Tags 113 MiB
969a6e1a45
Commit Graph

1053 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
f303e469fb Improve elaborator reflection performance 
In a 'Bind', normalise the result of the first action, rather than
quoting the HNF. This improves performance since the HNF could be quite
big when quoted back.

Ideally, we wouldn't have to quote and unquote here, and we can probably
achieve this by tinkering with the evaluator.

This has an unfortunate effect on the reflection002 test, in that the
"typed template Idris" example now evaluates too much. But, I think the
overall performance is too important for the primary motivation
behind elaborator reflection. I will return to this!
 2020-07-17 15:18:23 +01:00
Nick Drozd
a2bdf8e6d7 Add some algebra implementations 2020-07-17 08:25:20 -05:00
Niklas Larsson
fd9de745ae
Merge pull request #467 from elsanussi-s-mneina/patch-1 
fix typo: "lowercase later" to "lowercase letter"
 2020-07-16 14:10:56 +02:00
elsanussi-s-mneina
19bced702d
fix typo: "lowercase later" to "lowercase letter" 
I think this is a spelling mistake.
 2020-07-15 09:50:19 -04:00
Niklas Larsson
6233bbd583
Merge pull request #465 from memoryruins/case-declarations 
Wrap Javascript case clauses in brackets to prevent conflicting declarations
 2020-07-14 21:29:02 +02:00
memoryruins
7ab00bd191 add test for js case clause scopes 2020-07-14 14:22:08 -04:00
Guillaume ALLAIS
62a5406533 [ fix #454 ] compiling nonexisting file 2020-07-14 15:23:00 +01:00
memoryruins
1c6804f82b wrap js case clauses in brackets to prevent conflicting declarations 2020-07-14 09:44:54 -04:00
Mark Barbone
acda3b44a9
Make Text.Parser.between lazy (#385) 2020-07-14 14:33:22 +01:00
Dmitry
de00ff74d5
Allow to override log level with package options (#411) 2020-07-14 12:17:03 +01:00
G. Allais
0908e76515
[ fix #346 ] Pull List.length into prelude (#450) 2020-07-14 12:15:57 +01:00
Nicolas Biri
aba76206c9 Remove dependency to Vector length in deleteAt 2020-07-14 09:45:33 +01:00
Niklas Larsson
7920eb8a0e
Merge pull request #456 from chrrasmussen/patch-1 
Update reference to %auto_implicits in implementation notes
 2020-07-13 11:53:01 +02:00
Niklas Larsson
26f9c8a25c
Merge pull request #459 from rbarreiro/master 
fix #447
 2020-07-13 10:18:36 +02:00
Niklas Larsson
d6c4393517
Merge pull request #427 from nickdrozd/more-changes 
Minor simplifications
 2020-07-13 10:17:31 +02:00
Nick Drozd
e14a589e90 Consolidate boolean expressions 2020-07-12 21:00:33 -05:00
Nick Drozd
6519b5608d Further simplify List 2020-07-12 21:00:33 -05:00
Nick Drozd
718da3d7e6 Simplify Vect 2020-07-12 20:59:00 -05:00
Edwin Brady
e93fba3952
Merge pull request #462 from edwinb/prelude-org 
Reorganising the prelude
 2020-07-13 01:30:01 +01:00
Edwin Brady
3794b20d0c Normalise to / in generating interface names 
In practice, this is only for consistency in the tests. Is this the
right way?
 2020-07-12 17:33:33 +01:00
Edwin Brady
6a53e0177c Reorganise prelude into multiple files 
This is partly to tidy things up, but also a good test for 'import as'.
Requires some internal changes since there are parts of reflection,
unelaboration and a compiler hack that rely on where things are in the
Prelude.
 2020-07-12 16:55:48 +01:00
Edwin Brady
9d6f365ad7 Merge github.com:idris-lang/Idris2 2020-07-12 12:49:15 +01:00
Edwin Brady
183bac8667 Update namespaces with aliases in output 2020-07-12 12:48:48 +01:00
Rui Barreiro
bfecdb41d1 trigger ci 2020-07-12 11:59:58 +01:00
Rui Barreiro
98f2b8a246 update test 2020-07-12 10:26:30 +01:00
Rui Barreiro
ccf441f42b fix #447 2020-07-12 10:13:45 +01:00
Niklas Larsson
fb481cd2d1
Merge pull request #448 from melted/simplify_ipkg 
Make the idris2 executable depend on the idris2 lib
 2020-07-11 11:01:47 +02:00
Christian Rasmussen
6211922960
%auto_implicit has been renamed to %unbound_implicits 2020-07-11 02:33:23 +02:00
Edwin Brady
b3bb73cfd6
Merge pull request #455 from edwinb/export-nat-prfs 
Data.Nat proofs should be exported
 2020-07-10 23:30:09 +01:00
Edwin Brady
58e28170ac Data.Nat proofs should be exported 
I assumed these were copied directly from the Idris 1 libraries, where
there was an %access directive that we don't have any more.
 2020-07-10 22:59:46 +01:00
Jan de Muijnck-Hughes
5774a9c6ae If we know the types of a & b start searching. 
This is helpful when defining auto-implicits of the form:

    pairEqF : DecEq a
           => (thisX, x, y : a)
           -> {prfRefl : Equal x thisX}
           -> (prfEq   : decEq x thisX = Yes prfRefl)
           => Pair a a
    pairEqF thisX x y {prfRefl} {prfEq} = MkPair x y

before auto-implicit search would fail to find `Refl` for `prfRefl`.
With this fix the solution is found.

This fix means we can avoid having to write the following.

    pairEqF' : DecEq a
            => (thisX, x, y : a)
            -> (prfEq   : decEq x thisX = Yes (the (Equal x x) Refl))
            => Pair a a
    pairEqF' thisX x y {prfEq} = MkPair x y
 2020-07-10 21:00:38 +01:00
Jan de Muijnck-Hughes
fcbfcf6fe2 Added take to Vect. 2020-07-10 21:00:38 +01:00
Edwin Brady
9156084075
Merge pull request #449 from ohad/specifying-vector-transposition 
Include a (non-linear) definition for transpose that uses zipWith
 2020-07-10 18:09:27 +01:00
Denis Buzdalov
0aeadbad19 Recently added implementation were slightly fixed and nicened. 2020-07-10 17:28:49 +01:00
Ohad Kammar
eceaf98007 Generalise cons-specialised linear zipWith to linear zipWith (lzipWith) 2020-07-10 17:17:19 +01:00
Edwin Brady
606059e3d9
Merge pull request #451 from edwinb/impl-docs 
Add some implementation notes to the docs
 2020-07-10 16:25:26 +01:00
Edwin Brady
da4885c4fa Fix formatting 2020-07-10 16:01:17 +01:00
Edwin Brady
874587906f A few more internal details in the docs 2020-07-10 15:59:47 +01:00
Edwin Brady
3312961b54 Fix reference id 2020-07-10 15:23:44 +01:00
Edwin Brady
56e21fa27a Add some implementation notes to the docs 2020-07-10 15:21:24 +01:00
Dmitry
c35b8e39f7
Add command line option to typecheck package without codegen (#412) 2020-07-10 14:08:21 +01:00
Ohad Kammar
8f09ef9b93 Include a (non-linear) definition for transpose that uses zipWith, 
as it might be easier to reason about, since users may already have proved
stuff about zipWith that they want to reuse
 2020-07-10 12:47:05 +01:00
Niklas Larsson
4a5ca77cbe Make the idris2 executable depend on the idris2 lib 2020-07-10 12:46:44 +02:00
Niklas Larsson
ffb1d6406f
Merge pull request #445 from melted/update_ipkg 
Update ipkg files
 2020-07-10 11:28:20 +02:00
Niklas Larsson
a5b101dc3c Update ipkg files 2020-07-10 11:03:21 +02:00
Niklas Larsson
80f4ced386
Merge pull request #442 from melted/fix_bootstrap2 
Fix bootstrap
 2020-07-10 00:48:26 +02:00
Niklas Larsson
cddf8c6fa5 Fix bootstrap 
Replace if-expression with a function
 2020-07-09 22:46:21 +02:00
Matthew Ess
6452cdbbd4
Add Ord implementation for Either (#439) 2020-07-09 19:28:59 +01:00
SmiVan
3c051f3375 Amend typo in INSTALL.md 2020-07-09 11:58:53 +01:00
Niklas Larsson
eca9c12cf5
Merge pull request #438 from melted/fix_b 
Fix bootstrap
 2020-07-09 00:45:30 +02:00