1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 04:09:10 +03:00
Commit Graph

637 Commits

Author SHA1 Message Date
Edwin Brady
4cc4099ace
Merge branch 'master' into nats 2020-06-08 12:11:10 +01:00
Edwin Brady
d6e3f1f746
Merge pull request 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 from vilunov/repl-let
":let" command for REPL
2020-06-08 12:00:15 +01:00
Edwin Brady
ff56062a5e
Merge pull request 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 from MarcelineVQ/elab-changes
add parens for some TTImp Shows
2020-06-08 11:54:19 +01:00
Edwin Brady
6b0118d7ca
Merge pull request from clayrat/master
add Data.Fuel
2020-06-08 11:46:48 +01:00
Edwin Brady
3a0a907c0b
Merge pull request from ShinKage/auto-implicit-depth
Added auto_implicit_depth pragma
2020-06-08 11:45:33 +01:00
Edwin Brady
59025b0a85
Merge pull request from keram/remove-clang
Remove clang from config.mk
2020-06-08 11:42:37 +01:00
Edwin Brady
47c0675e49
Merge pull request 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 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 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 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 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 . 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 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 from edwinb/evaluator-fix
More explicitness in evaluator return type
2020-06-06 22:42:55 +01:00
Edwin Brady
93022af74e More explicitness in evaluator return type
Another one from the "stop trying to be clever" files :). Instead of a
continuation for fallthrough in the evaluator, be explicit about whether
there's a result, no match, or evaluation is stuck.
Fixes 
2020-06-06 22:20:25 +01:00
Edwin Brady
595e1768e2
Merge pull request from edwinb/unifier-fix
Various fixes
2020-06-06 21:18:25 +01:00
Edwin Brady
252e07833b Fix case trees at multiplicity zero
Can't ignore a constructor a multiplicity zero if the whole function is
multiplicity zero
2020-06-06 20:45:20 +01:00
Frederik Vigen
2f34f85e2f Added fix to recvAll that doesn't use signal (Left 0) but the size of the buffer 2020-06-06 20:51:19 +02:00
Edwin Brady
0d4b087e6f Another assumption about scope of metavariables
When instantiating a term, we had an attempt at an optimisation that
assumed variables would be in scope order. But it's not safe to make
that assumption, and it turns out it makes no measurable difference to
performance anyway.
2020-06-06 18:55:59 +01:00
Edwin Brady
4dfbc0fcdc Change representation of names in Nested
Instead of using a raw name, which is error prone, use a Var so we have
a proper reference into the environment. This is important when we're
combining case blocks and where clauses, because we need to rebuild the
environment properly for calls to functions defined in the where block.
2020-06-06 18:45:47 +01:00
Edwin Brady
7733c85fd5 New way of instantiating metavariables
The old way only worked by chance, because the argumemt order happens to
be the same in all cases. I noticed due to some experiments elsewhere
with different ways of elaborating case, which broke that assumption.

The meaning of the list of Vars is actually the opposite of what it was
taken to be... fortunately, the performance works out roughly the same.
Also this way is (arguably) simpler, which is usually a good sign.
2020-06-06 18:43:06 +01:00
Niklas Larsson
8af183d52b
Merge pull request from Sventimir/factorisation
Factors of natural numbers
2020-06-06 13:20:44 +02:00
Niklas Larsson
5c915a578c
Merge pull request from ska80/patch-2
Add more video talks on development of Idris 2
2020-06-06 13:18:20 +02:00
Keller, Bryn
a5449d926e Update docs to reflect changes to ipkg format 2020-06-05 22:14:16 -07:00
Kamiλ Shakirov
2212e81c1f
Add more video talks on development of a Idris 2 2020-06-06 00:41:58 +06:00
Alex Gryzlov
1fe9bb8977 Merge remote-tracking branch 'upstream/master' 2020-06-05 19:40:55 +02:00
Edwin Brady
4aa1c1f44a
Merge pull request from edwinb/case-conversion
Look inside case blocks in conversion check
2020-06-04 18:43:24 +01:00
Edwin Brady
c17d4ff0a5 Look inside case blocks in conversion check
This is quite fiddly as it the blocks might be in different contexts so
we need to keep track of which variables correspond in the scrutinees of
the blocks. Once that's done, check the terms at the leaves convert,
then check the corresponding variables convert.

This may not be perfect yet, because we only look at case scrutinees to
find correspondence. It might also be a bit slower than it could be, but
at least these checks are quite rare.

Fixes  and maybe some others?
2020-06-04 18:21:44 +01:00
Alex Gryzlov
ca32ff9000 Merge remote-tracking branch 'upstream/master' 2020-06-04 00:23:35 +02:00
Edwin Brady
1e393b6ffc
Merge pull request from edwinb/reflect-binders
Make lambda elaborator dependent
2020-06-03 20:48:54 +01:00
Edwin Brady
b9ac6e14db Make lambda elaborator dependent
Also remove forall, since I haven't tested it and its type was wrong
anyway. It can go back when we have a use for it...
2020-06-03 20:23:36 +01:00
Edwin Brady
fe9f71d060
Merge pull request from edwinb/reflect-binders
Add reflection under (explicit) binders
2020-06-03 10:13:43 +01:00
Sventimir
7a874b28a4 Merge branch 'master' into factorisation 2020-06-03 11:13:01 +02:00
Edwin Brady
946e1b3a51 Slightly neater reflection008 test 2020-06-03 09:25:09 +01:00