1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
Commit Graph

1342 Commits

Author SHA1 Message Date
Guillaume ALLAIS
09f418f250 [ admin ] removing useless import 2020-09-16 15:45:16 +01:00
Guillaume ALLAIS
2bb95e59ef [ re ] eta-contract parameter candidates 2020-09-16 15:45:16 +01:00
Guillaume ALLAIS
88c4b4d02f [ new ] mapTermM and mapTerm 2020-09-16 15:45:16 +01:00
Guillaume ALLAIS
1152aa3cdd [ re ] inline lets when detecting parameters 2020-09-16 15:45:16 +01:00
Guillaume ALLAIS
644495f097 [ debug ] logging for datatype parameters 2020-09-16 15:45:16 +01:00
Guillaume ALLAIS
364ff73a1f [ refactor ] split up Core.Context
`Core.Context` is 2k+ LoC and contains a *lot* of different thins.
Rather than moving the `log` functions above of `addData` to be able
to add logging there, fork them off to independent files to make the
whole thing more readable.
2020-09-16 15:45:16 +01:00
Giuseppe Lomurno
98e54cea2f Missing runElab decl check 2020-09-16 12:06:38 +01:00
Chetan Taralekar
3c24bc5ed5
Fix ide mode repl not converting escaped characters () 2020-09-16 10:55:44 +01:00
MarcelineVQ
ea0df039fe change runReader's to take state first to allow easier use
following up on the change made in 5c76053cf3
to encourage people to do it in this manner going forward
2020-09-15 22:46:07 +01:00
MarcelineVQ
19bad79847 change runState's to take state first to allow easier use 2020-09-15 09:23:41 +01:00
MarcelineVQ
5c76053cf3 change StateT, swap result parameters
Nipping this historical artifact in the bud before it roots. It's often
useful to be able to `map` directly to the result of a StateT computation
and due to how Functor works this is made harder when the tuple is
(a,state) vs (state,a)
2020-09-15 09:23:41 +01:00
Guillaume ALLAIS
65e194e9bb [ re ] Positivity checking for empty types 2020-09-14 18:37:47 +01:00
Ohad Kammar
2ae330785b
[contrib] Add misc libraries to contrib ()
* [contrib] Add misc libraries to contrib

Expose some `private` function in libs/base that I needed, and seem like
their visibility was forgotten

I'd appreciate a code review, especially to tell me I'm
re-implementing something that's already elsewhere in the library

Mostly extending existing functionality:
* `Data/Void.idr`: add some utility functions for manipulating absurdity.
* `Decidable/Decidable/Extra.idr`: add support for double negation elimination in decidable relations
* `Data/Fun/Extra.idr`:
  + add `application` (total and partil) for n-ary functions
  + add (slightly) dependent versions of these operations
* `Decidable/Order/Strict.idr`: a strict preorder is what you get when
  you remove the diagonal from a pre-order. For example, `<` is the
  associated preorder for `<=` over `Nat`.
  Analogous to `Decidable.Order`. The proof search mechanism struggled
  a bit, so I had to hack it --- sorry.

Eventually we should move `Data.Fun.Extra.Pointwise` to `Data.Vect.Quantifiers` in base
but we don't have any interesting uses for it at the moment so it's not
urgent.

Co-authored by @gallais
2020-09-14 16:22:46 +01:00
MarcelineVQ
5673d188f3 add nicer errors for bad specifiers 2020-09-13 10:10:53 +01:00
MarcelineVQ
5acb306bf9 add ability to target scheme flavor in foreign specifiers
There's some missing flexibility in how foreign specifiers can be used with
scheme that is addressed here with minimal changes to how scheme specifiers
are read. This opens up uses for users that they otherwise would have had
to modify the compiler's support files to accomplish.
2020-09-13 10:10:53 +01:00
Matus Tejiscak
9652179990 Add two cases to the record projection test. 2020-09-11 00:29:14 +02:00
Matus Tejiscak
ba89bbcc0d Fix tests some more. 2020-09-10 20:41:58 +02:00
Matus Tejiscak
d98686d4f8 Update doc, fix tests. 2020-09-10 20:33:08 +02:00
Matus Tejiscak
e491e2969e Re-introduce %prefix_record_projections. 2020-09-10 20:18:51 +02:00
Matus Tejiscak
aebe3c19d9 Revert postfix dotted application. 2020-09-10 19:00:48 +02:00
Ohad Kammar
cdd0d07877 [minor] Remove whitespace 2020-09-10 08:08:59 +01:00
Ohad Kammar
2ece0e438f Refactor dynamic rebinding of default totality requirement
Dynamic rebind now reinstates default if an error is raised

(following @gallais 's code review)
2020-09-10 08:08:59 +01:00
Ohad Kammar
b2a9ba651c Bugfix 654: forgot to update GenerateDef
When synthesizing clauses, allow synthesised clauses to be
partial.

It's an arbitrary choice, the other choice can be the default
option. But if the place in which we're synthesising has a non-default
choice, then we're synthesising under the wrong option too.
2020-09-10 08:08:59 +01:00
Ohad Kammar
2f5ae26f36 Fix typo 2020-09-10 08:08:59 +01:00
Ohad Kammar
0600a9ba11 Fix bug
Auxiliary functions introduced in elaboration (e.g., through case splits and with clauses) now
have the same totality annotation as the function they're defined in.

Moved auxiliary function `findSetTotal` into `Context.idr` since it's
now used by `ProcessDef.idr` too.

Added a totality requirement argument to `checkClause` so that the
with-clause case could propagate it to the functions it generates in
elaboration.

Sandwhich the rhs elaboration in pattern matches with code that sets
the global, default, totality requirement to the current one, and
restores the previous default afterwards. It's a bit of a hacky way to
do it, but I don't think we have a better alternative with the current
design.
2020-09-10 08:08:59 +01:00
Shay Lewis
53c2bf5885 make constructor injectivity proofs use arguments at 0 multiplicity 2020-09-09 19:57:12 +01:00
G. Allais
1963ac8786
[ fix ] Lazier match in NPrimVal vs. ConCase () 2020-09-09 17:17:07 +01:00
G. Allais
a0c0974676
[ debug ] pretty printer for case trees () 2020-09-09 16:22:22 +01:00
russoul
9565f6cf8b Fix DPair parsing 2020-09-05 11:08:44 +01:00
G. Allais
937aa8fc43
[ refactor ] introducing Namespace ()
Until now namespaces were stored as (reversed) lists of strings.
It led to:

* confusing code where we work on the underlying representation of
  namespaces rather than say what we mean (using `isSuffixOf` to mean
  `isParentOf`)

* potentially introducing errors by not respecting the invariant cf.
  bug report  (but also name generation in the scheme backend
  although that did not lead to bugs as it was self-consistent AFAICT)

* ad-hoc code to circumvent overlapping interface implementation when
  showing / pretty-printing namespaces

This PR introduces a `Namespace` newtype containing a list of strings.
Nested namespaces are still stored in reverse order but the exposed
interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
2020-09-05 09:41:31 +01:00
Guillaume ALLAIS
529944267b Revert "[ refactor ] Introducing Namespace and ModuleIdent ()"
This reverts commit 481dc431e7.
2020-09-04 09:16:06 +01:00
Niklas Larsson
71b9b9dc08
Merge pull request from foss-mc/patch-racket
Improve Racket supporting code
2020-09-03 14:43:57 +02:00
G. Allais
481dc431e7
[ refactor ] Introducing Namespace and ModuleIdent ()
Until now namespaces were stored as (reversed) lists of strings.
It led to:

* confusing code where we work on the representation rather than say
  what we mean (e.g. using `isSuffixOf` to mean `isParentOf`)

* potentially introducing errors by not respecting the invariant cf.
  bug report  (but also name generation in the scheme backend
  although that did not lead to bugs as it was self-consistent AFAICT)

* ad-hoc code to circumvent overlapping interface implementations when
  showing / pretty-printing namespaces

This introduces a Namespace newtype containing non-empty lists of
strings. Nested namespaces are still stored in reverse order but the
exposed interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
2020-09-02 20:05:33 +01:00
MarcelineVQ
3e4e33110b add semigroup/monoid instances for Unit/()
quite useful to have for more complex libraries and types
2020-09-02 08:42:00 +01:00
russoul
394b433c59 Typo 2020-09-01 16:18:13 +03:00
russoul
a6d767f8fa Remove unused 2020-09-01 15:46:17 +03:00
russoul
16407b7f08 Make sure there is no unexpected holes 2020-09-01 14:34:46 +03:00
russoul
8338b7adbc Tweaks 2020-09-01 14:32:24 +03:00
russoul
52e4a059de Remove unused def 2020-09-01 14:17:39 +03:00
russoul
87a58d30d0 Tweak record error, update expected output 2020-09-01 13:46:06 +03:00
russoul
b5fb108680 Update CHANGELOG.md 2020-09-01 13:33:22 +03:00
russoul
cb1a5f663c Implement V2 2020-09-01 13:31:59 +03:00
russoul
406f9f5099 Space 2020-09-01 13:31:22 +03:00
russoul
0dfd59d695 Add typedriven resolution, make code a bit prettier 2020-09-01 13:31:22 +03:00
Guillaume ALLAIS
9734b72349 [ test ] for empty records 2020-09-01 13:31:22 +03:00
russoul
53fe889b28 Refine test a bit 2020-09-01 13:31:22 +03:00
russoul
f50034a050 Spaces 2020-09-01 13:31:22 +03:00
russoul
0e7ba90e9f Remove Kleisli composition (not used anymore) 2020-09-01 13:31:22 +03:00
russoul
ef00018329 Remove redundant import 2020-09-01 13:31:22 +03:00
russoul
d5a0a58e0b Fix typo 2020-09-01 13:31:22 +03:00