Commit Graph

981 Commits

Author SHA1 Message Date
Sventimir
f3168d16aa Add a proof that (NotBothZero 0 0) is uninhabited. 2020-08-12 17:12:35 +02:00
Sventimir
208fb6fe04 Turn Validator into a proper monad transformer. 2020-08-11 20:52:13 +02:00
Sventimir
6389aa4099 Add initial validation framework. 2020-08-11 18:27:06 +02: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
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
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
André Videla
3d53c2874b
Merge pull request #508 from ShinKage/string-overload
Overloaded strings interface
2020-08-05 13:21:12 +01:00
Giuseppe Lomurno
723457fd6c Remove public export 2020-08-05 13:42:04 +02:00
Giuseppe Lomurno
627d340b62 Docs for overloaded literals 2020-08-05 11:51:27 +02:00
Giuseppe Lomurno
c28133b7d9 Renamed IsString to FromString
- Renaming of the string overload interface
- Added test cases for both string and integer literals overload
2020-08-05 02:33:05 +02:00
Giuseppe Lomurno
b7ba5e88eb Overloaded strings interface
As for integer literals, adds an interface for overloaded string
literals, and the implementation for the prettyprinter library in
contrib.
2020-08-05 02:00:05 +02:00
Edwin Brady
28bb45c61f
Merge pull request #522 from edwinb/more-search
More search improvements
2020-08-04 22:05:23 +01:00
Edwin Brady
45aa8f5815 Add a test for proof search 2020-08-04 20:55:48 +01:00
Edwin Brady
663f895058 Fix unification error
A typo! But it causes some things to fail to unify, especially in proof
search.
2020-08-04 20:53:01 +01:00
G. Allais
0a7ea69df5
[ refactor ] introduce List1 to remove impossible case (#520) 2020-08-04 20:03:18 +01:00
Edwin Brady
3c601d9878 Fix recursive call checking in proof search
Need to use full names consistently to check for structural difference
2020-08-04 19:24:58 +01:00
Edwin Brady
ea39a9eae2
Merge pull request #521 from edwinb/search-unpacking
Look at intermediate results in program search
2020-08-04 13:35:40 +01:00
Edwin Brady
711b507053
Merge pull request #487 from rbarreiro/js_doc
javascript codegen minimal doc
2020-08-04 13:21:47 +01:00
Edwin Brady
2761a27357
Merge pull request #476 from nickdrozd/algebra-implementations
Add some algebra implementations
2020-08-04 13:21:12 +01:00
Edwin Brady
fd3d086ebc Add an export declaration
Not strictly necessary, but needed to keep Idris2-boot happy!
2020-08-04 13:09:53 +01:00
Edwin Brady
3a6614b227 Look at intermediate results in program search
This has involved quite a bit of reorganisation and some improvements in
resugaring so that the results look nice. In summary:

* Expression search now gives back a RawImp rather than a checked term,
  which allows it to include case expressions
* Case with one pattern is resugared to a destructuring let
* Some name generation issues address in function generation

We look at intermediate results for local variables which are functions
that return a concrete type, or recursive calls that return a single
constructor type. In these cases, we:

* let bind the local variable/recursive call
* generate a new definition for the scope, as a 'case' function

When we recursively generate the definition, it's a bit more restricted
so as not to explode the search space. We only take the first result, we
only look one constructor deep, and we go right to left on variable
splitting so only deconstruct the name we've just added.
2020-08-04 12:51:57 +01:00
Wanja Chresta
14086fa1dd Add installation instructions for nix 2020-08-04 12:25:49 +01:00
Mark Barbone
cef248e5a7 Make showParens public 2020-08-04 10:58:00 +01:00
Niklas Larsson
b7cf3588c9
Merge pull request #519 from melted/startup_scheme
Quote the chez path in windows sh startup
2020-08-04 10:57:53 +02:00
Niklas Larsson
1b19564530 Quote the chez path in windows sh startup 2020-08-04 10:30:53 +02:00
Kamiλ Shakirov
143d2c5b11 Fix the code generator name for JavaScript CG
js -> javascript
2020-07-30 14:20:50 +01:00
Kamiλ Shakirov
d5f35ff0be Add another recent video talk on Idris 2
Also, rearrange videos in reverse chronological order to show the most recent videos first
2020-07-30 11:31:20 +01:00
Ohad Kammar
91c5ddd411
Merge pull request #506 from ohad/irrelevant-list-nonempty
Add irrelevance annotations to Data.List functions taking NonEmpty
2020-07-30 10:02:46 +01:00
Ohad Kammar
5cfbac4a51 Add irrelevance annotations to Data.List functions taking NonEmpty 2020-07-30 06:01:42 +01:00
Edwin Brady
5ad779f9de
Merge pull request #503 from edwinb/search0-heuristic
Add a heuristic for sorting search results
2020-07-30 00:38:00 +01:00
Edwin Brady
ff48bb2310 Update literate test results
New search heuristic finds a slightly better zipWith, in particular.
2020-07-30 00:08:06 +01:00
Edwin Brady
8d7fa5c642 Add a heuristic for sorting search results
Sort by proportion of bound variables used, which is likely to get us
the right answer quicker. The results are generated in batches of 16 (a
completely arbitrary choice) then sorted.
2020-07-29 23:54:52 +01:00
Alex Gryzlov
69612bf6bf
Add list lemmas (#491) 2020-07-29 10:51:07 +01:00
Edwin Brady
78ecd8a9f1
Merge pull request #501 from ohad/undotting-subsingletons
Take into account syntactic sub-singletons when dotting in patterns
2020-07-28 00:23:46 +01:00
Ohad Kammar
20ca6cc651 Address comments from code-review (bugs fixed)
Use `NTCons` when counting number of type constructors
Use `Maybe` for return type
2020-07-27 22:48:44 +01:00
Ohad Kammar
ac0b5a3f3b Take into account syntactic sub-singletons when dotting in patterns
When an erased pattern argument in a non-erased context is of a
datatype that has 0 or 1 constructors, there is no need to dot it
(i.e., require that the canonical term is inferred by other
dependencies): it has to be the unique constructor that appears in the
source.
2020-07-27 20:47:30 +01:00
Edwin Brady
77039bcdea
Merge pull request #500 from edwinb/more-search-stuff
More search stuff
2020-07-27 16:42:59 +01:00
Edwin Brady
7083f7ac13 Add a 'reject' count to :gd
This gives the number of implementations to reject before accepting one.
It's intended as a reasonably cheap way of giving multiple results from
interactive editing (e.g. the vim mode, which goes via the REPL and
--client rather than the IDE mode)
2020-07-27 14:56:16 +01:00
Edwin Brady
f33873d051 Add IDE mode commands for gdnext and psnext
I forgot to add these to the parser!
2020-07-27 14:44:09 +01:00
Edwin Brady
3a0a566607
Merge pull request #498 from edwinb/search-stuff
More search improvements
2020-07-27 14:14:59 +01:00
Edwin Brady
df635cf8d7 Add :psnext and :gdnext at the REPL
These continue the search from :ps and :gd next respectively, giving the
next search result until there are no more results.
Correspondingly, added ':proof-search-next' and ':generate-def-next' in
IDE mode, which continue the search from the previous ':proof-search'
and ':generate-def' respectively.
2020-07-27 13:45:10 +01:00
Edwin Brady
f8ef44f1b0 Allow multiple results from generate-defs
Return a 'Search' rather than a single definition. Also, change the
order of search in expressions so that we look at recursive calls
earlier when under a constructor - the assumption being that this is
more likely than nested constructors.
2020-07-27 12:04:39 +01:00
Edwin Brady
58bc918f5d
Merge pull request #497 from edwinb/exprsearch
Reorganise expression search
2020-07-26 18:08:42 +01:00
Edwin Brady
c860e5e690 Merge github.com:idris-lang/Idris2 2020-07-26 17:39:00 +01:00