idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 18:51:40 +03:00
Code Issues Projects Releases Wiki Activity
1,221 Commits 6 Branches 9 Tags 115 MiB
502f544d73
Commit Graph

1221 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Giuseppe Lomurno
cef2fbbccd Better term printing 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
42404c2d9d Automatic console width detection 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
f658ce357f More improvements 
- More migrations from String to Doc
- File context in parser errors
 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
607352a191 Error suggestions 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
6298a6741d Adds bounds to compiler parser 
- Added primitive to compiler parser for precise text boundaries
- Reworked parser with the new primitive
 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
3b0f11248e Case term fix 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
df3b76b739 More pretty printing 
- More on error messages
- More on REPL outputs
 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
5e9837828a Implementations and errors 
- Added initial implementations for terms and values
- Error messages converted to pretty printer
- Colorization for error messages
- Color and console width option both as command line and repl command
 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
df4f990b3c PTerm and error intial prettyprinting 2020-08-18 19:25:36 +01:00
Niklas Larsson
63b8504e42
Merge pull request #568 from melted/nmop_arity 
Add implicit arity arg to NmOp
 2020-08-18 14:28:09 +02:00
Niklas Larsson
76ee7a3b34
Merge pull request #351 from petithug/fixity-precedence-master 
Restore Bool operators precedence
 2020-08-18 14:08:20 +02:00
Niklas Larsson
2ae431bdc8
Merge pull request #558 from xoltar/at-requires 
Support package names with @, / and - in lambdaRequire, fix an error …
 2020-08-18 14:07:07 +02:00
Niklas Larsson
fed0f1be24
Merge pull request #551 from SmiVan/BitsN-Compile-Fix 
Split CFUnsigned into 8/16/32/64 bits versions
 2020-08-18 14:04:42 +02:00
Niklas Larsson
84ae9d7c6e
Merge pull request #523 from mb64/hasio-statet 
Implement HasIO for StateT
 2020-08-18 14:02:02 +02:00
Niklas Larsson
93ecb72012
Merge pull request #526 from alexhumphreys/feat/buildExpressionParser 
Add BuildExpressionParser to contrib
 2020-08-18 14:01:20 +02:00
Niklas Larsson
ac92e41e6e
Merge pull request #531 from jfdm/make-timings-hierarchical-in-output 
Makes timing output more intuative to read.
 2020-08-18 13:59:07 +02:00
Niklas Larsson
bed1b8c550
Merge pull request #564 from ska80/post-idris2boot-cleanups 
More post-Idris2-boot cleanups
 2020-08-18 13:54:02 +02:00
Niklas Larsson
b9beca1986 Add implicit arity arg to NmOp 
Like in CExp.
 2020-08-18 13:51:41 +02:00
Fangyi Zhou
df4c454f4e Typo in updates.rst 2020-08-17 19:33:14 +01:00
Kamil Shakirov
68bd8bba52 More post-Idris2-boot cleanups 2020-08-17 13:16:22 +06:00
Niklas Larsson
e985f719f7
Merge pull request #562 from idris-lang/bootstrap_badge 
Remove bootstrap badge from README
 2020-08-16 19:52:42 +02:00
Niklas Larsson
298d3627b9
Remove bootstrap badge from README 2020-08-16 19:51:28 +02:00
Niklas Larsson
0502d7be23
Merge pull request #561 from idris-lang/remove_full_bootstrap 
Remove the CI for bootstrapping from Idris 1
 2020-08-16 19:48:50 +02:00
Niklas Larsson
fae5c5ac34
Remove the CI for bootstrapping from Idris 1 
In order to not be held back by compatibility, it was decided that 0.2.1
would be the last version supporting bootstrap via Idris2-boot.
 2020-08-16 16:23:36 +02:00
Edwin Brady
db9f7bbf0d
Merge pull request #560 from edwinb/version 
Version increment
 2020-08-16 14:30:22 +01:00
Edwin Brady
dc9637aaa0 Update bootstrap scheme for release 2020-08-16 12:33:11 +01:00
Edwin Brady
0d81e3b59c Version increment 2020-08-16 12:06:38 +01:00
Ohad Kammar
10b8698843 Remove forgotten linearity annotation on cong2 2020-08-16 08:20:31 +01:00
Ohad Kammar
d82a3e0e42 contrib: Add a 2-holed congruence function 
For lack of a better place, I've put it in `Syntax.PreorderReasoning`

These equations are natural in equational reasoning, but less so when
rewriting, so that's why it's there
 2020-08-16 08:20:31 +01:00
Keller, Bryn
a6e3c85d22 Support package names with @, / and - in lambdaRequire, fix an error message, and add an idris list to js array primitive 2020-08-14 20:06:30 -07:00
Ivan Smirnov
7980e18602 Incremented TTC version 2020-08-12 13:35:31 +01:00
Ivan Smirnov
0f97b393cc Split CFUnsigned into 8/16/32/64 bits versions 
Adjusted the chez, gambit and racket compilers accordingly.
 2020-08-11 15:57:22 +01:00
Edwin Brady
ad1474a83b
Merge pull request #547 from edwinb/fix536 
Fix repeated argument check
 2020-08-10 14:39:57 +01:00
Edwin Brady
04e05e3f86 Fix repeated argument check 
As it was, it could break if the argument was repeated more than twice.
When checking dot patterns, we need to check that no further holes are
solved, and that the pattern variable doesn't unify with some other
pattern variable, but if it had already made progress (either for a good
or bad reason) we missed this. Fixes #536
 2020-08-10 14:03:34 +01:00
Alex Humphreys
f47d9cfef2 Add integer paser and extra test 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-10 13:26:20 +02:00
Alex Humphreys
f020fd29e8 Use overloaded Fin literals 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-10 13:26:20 +02:00
Thomas Dziedzic
a1739a69a0
Update app docs (#537) 2020-08-10 10:05:23 +01:00
Ohad Kammar
7f960ed938 Remove bindning to y as no longer necessary 2020-08-09 10:18:34 +01:00
Ohad Kammar
ff76dee6c7 Try a fix for the preorder reasoning error 
Correct the dependency in `FastDerivation` to use the RHS in `step`
Try to avoid shadowing `y` in the LHS of `Calc`
 2020-08-09 10:18:34 +01:00
russoul
d387c76e9b update stdio docs 2020-08-08 12:49:33 +01:00
Thomas Dziedzic
f337698608 update ffi docs with Bits* 2020-08-08 12:48:46 +01:00
Alex Humphreys
d4cbb8a620 Move natural and digit combinators 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-07 19:20:32 +02:00
Edwin Brady
15b31e69d0
Merge pull request #533 from edwinb/dpair-parse 
Refactor grammar for dependent pairs
 2020-08-07 17:04:39 +01:00
Edwin Brady
b786621ed6 Refactor grammar for dependent pairs 
As it was, there was significant backtracking for big expressions,
getting to the end, not finding a **, so having to try again for
application expressions. Fixes #532
 2020-08-07 16:30:25 +01:00
Jan de Muijnck-Hughes
5b5a6b9a38 Makes timing output more intuative to read. 
The timings flag (`--timing`) displays various timing information during the entire compilation process.
This is useful when performing adhoc profiling of the compiler.
However, the information is a mixture of timestamps and relative progress.
The information is inherently nested, and such nesting is not immediatly clear in the output.
This can be confusing.

This minor changes nests the timing information on output so that when aligned one can see the timestamps at the highest level, and progress during the elaboration stage.
 2020-08-07 13:26:44 +01:00
Alex Humphreys
40427bd527 Move combinators to Data.String.Parser 2020-08-06 13:16:47 +02:00
Alex Humphreys
97b41d1ad9 Rename BuildExpressionParser to Parser.Expression 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 12:42:38 +02:00
Alex Humphreys
22915d23ca Remove LO function 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 12:27:42 +02:00
Alex Humphreys
eca083cdcc Add License comment to BuildExpressionParser 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 08:59:57 +02:00
Alex Humphreys
29e49a74c5 Add BuildExpressionParser to contrib 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 08:59:57 +02:00