idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity
921 Commits 5 Branches 9 Tags 122 MiB
048f1887ea
Commit Graph

921 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Donovan Crichton
048f1887ea Added explicit case to headEq to allow matching on Pi Types. 2020-07-25 12:59:33 +10:00
Giuseppe Lomurno
39f23ffd9b Prec version of pretty interface 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
ab1f383912 Laziness annotations for performance 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
62524e8462 Tree representation for prettyprinting 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
3d51af46c2 Namespace change 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
eb659ba907 Added prettyprinting library 2020-07-24 15:19:17 +01:00
Adam Harries
3f4fd8e4aa
Document samples/ffi, and change name of .so to better suit convention. (#474) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2020-07-24 13:21:48 +01:00
Niklas Larsson
2542c325b1
Merge pull request #482 from iclanzan/patch-2 
Fix typo
 2020-07-23 14:51:31 +02:00
Niklas Larsson
57f89ccd9a
Merge pull request #485 from melted/directive_arg 
Add `--directive` cli option
 2020-07-23 14:50:53 +02:00
Niklas Larsson
7e0bca23fd Add --directive cli option 
It sends a codegen directive to the current codegen. It's useful
for sending options you don't want to hard code in the source. Examples
include enabling profiling or setting a target.
 2020-07-23 13:50:46 +02:00
Niklas Larsson
ff235bd30b
Merge pull request #483 from nixCodeX/fromInteger-0 
Fix fromInteger 0 for Bits8, Bits16, Bits32, Bits64
 2020-07-21 17:32:49 +02:00
Jonathan Tanner
5c73ada68a Fix fromInteger 0 for Bits8, Bits16, Bits32, Bits64 2020-07-21 15:29:09 +01:00
Sorin Iclanzan
2d15b59e6d
Fix typo 2020-07-21 09:26:46 -04:00
Denis Buzdalov
0119c217c9 Putting .ipkg mentioning to a variable and making names symmetrical. 2020-07-21 11:05:47 +01:00
Niklas Larsson
8a210d536e
Merge pull request #408 from melted/buffer_api 
Add concatBuffers and splitBuffer to Data.Buffer
 2020-07-21 10:43:17 +02:00
Jonathan Chan
dab2b0d146 Export (~>) publicly. 
If `(~>)` isn't publicly exported, the type checker doesn't know that `Mor` constructs something of type `~>`.
 2020-07-20 15:55:24 +01:00
Edwin Brady
0871494b5e
Merge pull request #479 from edwinb/fix-443 
Delay building references for case blocks
 2020-07-18 20:00:03 +01:00
Edwin Brady
690328421a Delay building references for case blocks 
...until the definition is complete. This is necessary since sometimes
information outside the case block can help resolve interfaces, and in
the simplest case, we might just have delayed resolving a default
Integer. It turns out this was also an obscure bug waiting to happen
with coverage checking of nested case blocks (so there's a test update
there too).

Fixes #443
 2020-07-18 19:22:03 +01:00
Edwin Brady
b6506442e7
Merge pull request #477 from edwinb/reflection-perf 
Improve elaborator reflection performance
 2020-07-17 16:15:01 +01:00
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
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