idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity
707 Commits 6 Branches 9 Tags 114 MiB
df60e07962
Commit Graph

707 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Niklas Larsson
b5f67b94ae Use constants instead of calculation for upper bounds 
Add wrapping to 8-bit adding.

This is a workaround to fix the bootstrap
Fixes #268
 2020-06-11 14:23:41 +02:00
Jan de Muijnck-Hughes
49b4f97c5d Added some modest improvements to code. 2020-06-11 12:51:47 +01:00
Jan de Muijnck-Hughes
ef85348de8 Update src/Text/Literate.idr 
Improve efficiency of lexer for code lines.

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2020-06-11 12:51:47 +01:00
Jan de Muijnck-Hughes
63e127094e Improved parsing for literate modes. 
The tokenizer for literate modes was incorretly detecting code lines in text.
This PR fixes that, and allows for empty code lines.
 2020-06-11 12:51:47 +01:00
Niklas Larsson
fc322bd699 Add a bootstrap from Idris 1 CI script 2020-06-11 12:20:50 +02:00
Edwin Brady
d71bfef73f
Merge pull request #266 from edwinb/vis-case-with 
Propagate visibility appropriately to case/with
 2020-06-10 13:53:17 +01:00
Edwin Brady
df3449f44b Fix the other clashing test output 
I don't understand the difference here - there's probably a commit I
hadn't merged earlier that affected the name generation.
 2020-06-10 13:08:50 +01:00
Edwin Brady
c07876d1a3 Fix clashing test output 2020-06-10 12:53:18 +01:00
Edwin Brady
004b41a3d8 Merge https://github.com/idris-lang/Idris2 into vis-case-with 2020-06-10 12:50:30 +01:00
Edwin Brady
42676d2504
Merge pull request #265 from edwinb/find-ipkg-ide 
In IDE mode, look for a ipkg file before loading
 2020-06-10 12:42:59 +01:00
Edwin Brady
0cc54ff145 Propagate visibility appropriately to case/with 
If a function is public export, the local definitions also need to be
public export for it to reduce properly. But if they're not, we don't
want them exported or they might affect the module hash and cause
unnecessary rebuilds.
 2020-06-10 12:41:02 +01:00
Jan de Muijnck-Hughes
90fb901c8f Fix test reporting when in interactive mode. 
When runing in interactive mode, the diff between expected and output is not being show,
Supposedly, Git-diff returns 0 on successful run and a non-zero for error.
However, this is not being picked up by the test suite.

We change git-diff's error reporting to be more diff like in which:

+ +ve indicates that there is a diff.
+ 0 indicates the files are the same.
+ -ve program error.

This should make diff reporting more robust.
 2020-06-10 09:30:02 +01:00
Edwin Brady
cf23bae7d6 In IDE mode, look for a ipkg file before loading 
This takes the responsibilty of finding the ipkg away from IDE mode,
which seems sensible given that we can do it ourselves. If there isn't
one, it'll load from the local directory as always.
 2020-06-09 23:31:30 +01:00
Edwin Brady
b88f425a57
Merge pull request #257 from edwinb/finalisers 
Add finalisers to Chez and Racket back ends
 2020-06-08 22:59:48 +01:00
Edwin Brady
ca28dab1d7 Add finalisers for Racket back end 
Like Chez, we also need an explicit call to the garbage collector at the
end to ensure that all the finalisers get run on exit.
 2020-06-08 22:13:24 +01:00
Edwin Brady
e32f039227 Fix includes in chez022 test 2020-06-08 20:46:25 +01:00
Edwin Brady
d60feaace0 Add finalisers to Chez back end 
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.

In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...

This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
 2020-06-08 20:34:23 +01:00
Nikita Vilunov
560d472502 add a test for --repl 2020-06-08 19:21:22 +03:00
Edwin Brady
2c77c38f1f Merge branch 'nickdrozd-nats' 2020-06-08 13:22:46 +01:00
Edwin Brady
85bd751283 Update reflection test again 2020-06-08 13:22:18 +01:00
Edwin Brady
4cc4099ace
Merge branch 'master' into nats 2020-06-08 12:11:10 +01:00
Edwin Brady
d6e3f1f746
Merge pull request #100 from ska80/use-contrib 
Use Control.Delayed from the 'contrib' package
 2020-06-08 12:07:09 +01:00
Edwin Brady
abcb1b417f
Merge pull request #248 from vilunov/repl-let 
":let" command for REPL
 2020-06-08 12:00:15 +01:00
Edwin Brady
ff56062a5e
Merge pull request #244 from xoltar/ipkg-format-docs 
Update docs to reflect changes to ipkg format
 2020-06-08 11:55:46 +01:00
Edwin Brady
73de552776
Merge pull request #239 from MarcelineVQ/elab-changes 
add parens for some TTImp Shows
 2020-06-08 11:54:19 +01:00
Edwin Brady
6b0118d7ca
Merge pull request #227 from clayrat/master 
add Data.Fuel
 2020-06-08 11:46:48 +01:00
Edwin Brady
3a0a907c0b
Merge pull request #226 from ShinKage/auto-implicit-depth 
Added auto_implicit_depth pragma
 2020-06-08 11:45:33 +01:00
Edwin Brady
59025b0a85
Merge pull request #183 from keram/remove-clang 
Remove clang from config.mk
 2020-06-08 11:42:37 +01:00
Edwin Brady
47c0675e49
Merge pull request #254 from edwinb/test-fix 
Update test output
 2020-06-08 11:01:27 +01:00
Edwin Brady
4834f2f78c Update test output 
Clash in a reflection test due to conflicting merges. I'd like to find a
way to make the internally generated numbers not matter here (and
elsewhere) but I don't see an obvious way.
 2020-06-08 10:39:58 +01:00
Edwin Brady
e033609310
Merge pull request #207 from mb64/assert_smaller-linear 
Make assert_smaller and assert_total linear
 2020-06-08 10:19:33 +01:00
Edwin Brady
0b20fe2412
Merge branch 'master' into remove-clang 2020-06-08 10:18:31 +01:00
Edwin Brady
8f80e77678
Merge pull request #122 from keram/install-impro-v2 
Add additional information on requirements in INSTALL.md
 2020-06-08 10:16:40 +01:00
Edwin Brady
7455a7c9f3
Merge pull request #232 from mb64/no-thin 
Remove redundant thin functions and replace with insertNames
 2020-06-08 10:15:17 +01:00
Edwin Brady
f9fc61ad4c
Merge pull request #252 from edwinb/totality-case 
Case block improvements
 2020-06-08 01:35:53 +01:00
Edwin Brady
0f27042b32 Fix build given new case elaboration rule 
Actually this was an error in Core.Directory, so the change has caught
it! Always nice to see that happen on making an improvement...
 2020-06-08 01:14:06 +01:00
Edwin Brady
1057cb9314 Go into case branches when productivity checking 
We were only looking inside the branches for termination checking, so
this might have missed some non-productive things.
 2020-06-08 01:10:07 +01:00
Nikita Vilunov
2db3a61160 implement "--repl" 2020-06-08 01:31:16 +03:00
Alex Gryzlov
14002213a1 Merge remote-tracking branch 'upstream/master' 2020-06-08 00:27:58 +02:00
Edwin Brady
d47d495744 Free standing case blocks return () 
Fixes #116. This is the solution Idris 1 took, and while it is a special
case, the syntax does make it explicit (in a way) that the result of the
case is unused - if you mean something other than (), you must now say
so!
 2020-06-07 22:49:19 +01:00
Nick Drozd
85c1e62587 Update test 2020-06-07 14:17:17 -05:00
Nick Drozd
5665cfab21 Copy over more Nat proofs 2020-06-07 12:19:32 -05:00
Nick Drozd
4292d735eb Simplify Nat proofs 
These changes are strictly nonfunctional.
 2020-06-07 12:19:32 -05:00
Nikita Vilunov
018c17b69a Add :let test 2020-06-07 16:40:45 +03:00
Edwin Brady
6898965a56
Merge pull request #249 from edwinb/refl-names 
Reflect 'display names' and record field names
 2020-06-07 12:44:03 +01:00
Edwin Brady
d5e4dec119 Reflect 'display names' and record field names 
These arise in interface declarations (to give a nicer way of displaying
auto generated names) and for record fields.
 2020-06-07 11:51:09 +01:00
Nikita Vilunov
d36e804012 ":let" command for REPL 2020-06-07 12:53:01 +03:00
Mark Barbone
793184a777
Remove thin functions; replace with insertNames 2020-06-07 01:10:06 -04:00
MarcelineVQ
6993c6df6b add parens for some TTImp Shows 
helps with readability since these, especially named-IPi, come up a lot
didn't change everything that could need it like PiInfo or BindMode
PiInfo rarely has DefImplicit (so far) and BindMode hasn't come up a lot (so far)
reduced indentation for TTImp Show implementation
 2020-06-06 17:16:43 -07:00
Edwin Brady
a0d9ce201e
Merge pull request #247 from edwinb/evaluator-fix 
More explicitness in evaluator return type
 2020-06-06 22:42:55 +01:00