edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 05:32:03 +03:00
Code Issues Projects Releases Wiki Activity
580 Commits 2 Branches 1 Tag 4.2 MiB
eb7be5eba1
Commit Graph

580 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Milan Kral
eb7be5eba1 Use HTTPS instead of HTTP 2019-12-18 21:37:50 +01:00
Edwin Brady
952abe7fc8 Deal with auto implicits when adding lambdas 
We were only checking the type for implicit lambdas, so using lambdas in
functions with an auto implicit was giving a strange error.
 2019-12-09 18:00:36 +00:00
Edwin Brady
c85ffd2c29 Return correct type on variadic application 
In the case where the function type is not yet known, and there's a
postponed unification problem, we were returning the function type not
the result type.
--debug-elab-check ought to be extended to catch this sort of thing.
Fixes #168
 2019-12-08 00:25:49 +00:00
Edwin Brady
9ee40b94a9 Add missing conversion check 
Fixes #166
 2019-12-07 21:04:41 +00:00
Edwin Brady
663e1b8f69 Add uniqueSearch data type option 
This changes the behaviour of 'auto' implicits so that by default they
return the first result, rather than checking for unique results. This
is consistent with Idris 1. However, we still want to check for
uniqueness somtimes (for example, with interface search, which should
reject overlapping results) so the 'uniqueSearch' option means that any
auto implicit search for the type should check uniqueness of results.

Fixes #169
 2019-12-07 18:54:02 +00:00
Edwin Brady
ebb1ec3a3a
Merge pull request #167 from ska80/unwords+unlines/idris1 
Add unwords and unlines to base/Data.Strings from Idris 1
 2019-12-07 15:28:14 +00:00
Edwin Brady
5d4cf051d9
Merge pull request #165 from ska80/remove-swp 
Remove Vim swap files
 2019-12-07 15:27:27 +00:00
Edwin Brady
0c4301d1c2
Merge pull request #159 from ska80/integral-nat 
Add an implementation of Integral for Nat
 2019-12-07 15:26:50 +00:00
Edwin Brady
cbf2f4ac9f
Merge pull request #155 from bwignall/typo 
Fix small double-and typo
 2019-12-07 15:18:06 +00:00
Edwin Brady
f6397ad0f6
Merge branch 'master' into typo 2019-12-07 15:17:51 +00:00
Edwin Brady
ba5a798549
Merge pull request #153 from abailly/export-network 
export Network.Socket functions
 2019-12-07 15:14:42 +00:00
Edwin Brady
6c165cab52 Change default precedence of op 
For consistency with Idris 1, they should be lowest precedence (other
than $) rather than highest.

Fixes #112
 2019-12-06 11:21:05 +00:00
Edwin Brady
050fcfa45a
Merge pull request #148 from msmorgan/list-replicate 
Add replicate to base/Data.List.
 2019-12-06 10:59:12 +00:00
Edwin Brady
468555bb2e
Merge pull request #143 from ohad/bugfix-#133 
Bugfix #133 and library support for tail-recursive list manipulation
 2019-12-06 10:56:03 +00:00
Edwin Brady
262177016c
Merge pull request #147 from msmorgan/list-zip 
Add zip functions to base/Data.List.
 2019-12-06 10:42:11 +00:00
Edwin Brady
79320c1574
Merge pull request #145 from lodi/nixprep 
allow overriding racket/chicken paths through environment variables
 2019-12-06 10:40:32 +00:00
Edwin Brady
078b5be85f
Merge pull request #144 from sysvinit/debug-trace 
Port Debug.Trace from Idris 1
 2019-12-06 10:38:28 +00:00
Edwin Brady
d9f1b01ef7
Merge branch 'master' into bugfix-#133 2019-12-06 10:28:07 +00:00
Edwin Brady
0a51a72806 Add runElab to syntax tree 
Nothing done yet in the elaborator, but it's ready to be filled in later
 2019-12-05 18:58:53 +00:00
Edwin Brady
d5cde3f4f9 Add unquoting/escaping 2019-11-30 19:42:39 +00:00
Edwin Brady
07509f6103 Begin elaboration of quoting terms 2019-11-30 15:26:17 +00:00
Edwin Brady
aae3d0f718 Reorganise Language.Reflection modules 2019-11-30 13:23:03 +00:00
Kamil Shakirov
8afad8ef0a Add unwords and unlines to base/Data.Strings from Idris 1 2019-11-26 01:17:18 +06:00
Edwin Brady
1c006b647a Reflect/reify for TTImp 
This is further progress towards a metaprogramming system in a form
similar to Elaborator Reflection or Template Haskell, but trying to
avoid leaking too many implementation details of the elaborator itself.
 2019-11-24 21:17:16 +00:00
Edwin Brady
f0da43156a Use latest bound name in building case function 
We were using the least recently bound, leading to the wrong type being
shown in some cases with shadowing
 2019-11-23 14:44:31 +00:00
Kamil Shakirov
3dade792bc Remove Vim swap files 2019-11-20 10:12:53 +06:00
Edwin Brady
2e9eabff71 Merge branch 'master' of github.com:edwinb/Idris2 2019-11-19 14:07:55 +00:00
Edwin Brady
17c83d6f4a
Merge pull request #137 from msmorgan/remove-trailing-whitespace 
Remove trailing whitespace from Idris sources.
 2019-11-18 20:44:46 +01:00
Kamil Shakirov
15f6e863c4 Add implementation of Integral for Nat 2019-11-15 17:46:26 +06:00
Edwin Brady
a3dc1ff228 Add ITransform to TTImp 
This is for rewrite rules/transformations which arise from partial
evaluation. Details not yet implemented.
 2019-11-13 17:57:39 +01:00
Brian Wignall
fc9f2a995d Fix small double-and typo 2019-11-11 16:38:53 -05:00
Edwin Brady
ca3ea38cde Make sure Force is erased for termination checker 
But only for 'Lazy', not for 'Inf'. This is necessary to build the size
change graphs correctly.
 2019-11-11 19:35:23 +00:00
Arnaud Bailly
fe4fb532cd export Network.Socket functions fix #152 2019-11-11 08:38:10 +01:00
Michael Morgan
9190ccf883 Add replicate to base/Data.List. 2019-10-29 16:08:13 -07:00
Michael Morgan
2a014d1e19 Add zip functions to base/Data.List. 
This includes the following functions: zipWith, zip, zipWith3, zip3
 2019-10-29 15:51:15 -07:00
lodi
76ff99d370 allow overriding racket/chicken paths through environment variables 
This is to help Idris2 codegen the correct scripts on NixOS where
Racket and Chicken aren't installed in the standard locations, and
the /usr/bin/env trampoline is disabled at package build time.
This now matches the existing Chez behavior.

Also, fixed the test runner to restore the correct working directory
after a failed test, and fixed the top-level Makefile to allow the
IDRIS2_VERSION variable to be queried without building the project.
 2019-10-28 22:44:16 -04:00
Molly Miller
0fb873949f Implement Debug.Trace, from Idris 1's base package 2019-10-28 20:23:11 +00:00
Ohad Kammar
7e8642e8f8 Fix a stack overflow with a tail recursive list integer length function 
Relates to #133 and #135.
 2019-10-27 08:26:06 +02:00
Ohad Kammar
fd980bc92f Add tail-recursive versions for most of the Data.List functions 
Also include proof the tail-recursive versions are extensionally equivalent to the non-tail-recursive one

I'm a bit worried that some of those proofs came through, as
visibility modifiers should get in the way. If they cause problems at
some future point, just delete/comment them out.
 2019-10-27 04:07:01 +02:00
Ohad Kammar
fa29941819 Add DIY syntax for: 
1. with-proof construct
2. equational reasoning

temporarily, until Idris2 supports those features
 2019-10-27 04:05:31 +02:00
Edwin Brady
ab98b4d3c9 Print banner before typechecking 
Otherwise it hides the errors
 2019-10-26 13:39:50 +01:00
Michael Morgan
e6121e0935 Remove trailing whitespace from Idris sources. 
This is the result of running the command:

$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +

I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
 2019-10-25 14:24:25 -07:00
Edwin Brady
f09138d508 Fix broken test 2019-10-25 17:32:29 +01:00
Edwin Brady
dab2bb36c1
Merge pull request #136 from clayrat/sourcedir 
Add 'sourcedir' option to IPKG
 2019-10-25 14:09:54 +01:00
Edwin Brady
3b73bf2813
Merge branch 'master' into sourcedir 2019-10-25 14:07:52 +01:00
Edwin Brady
779b09086b
Merge pull request #135 from ohad/bugfix-#133 
Bugfix #133
 2019-10-25 14:06:50 +01:00
Edwin Brady
da1964ce3d
Merge pull request #134 from ohad/bugfix-#109 
Add multiple-parameter test as idris/basic029
 2019-10-25 14:05:45 +01:00
Edwin Brady
c458957bd6 Get correct namespace in parameters blocks 
Fixes #132. When getting the names in the block, we need to return the
fully explicit name, because we can't assume they'll all be in the same
namespace as we can have namespaces inside parameters blocks.
 2019-10-25 14:03:15 +01:00
Alex Gryzlov
fcb337b3dc fix dir order & add comment 2019-10-24 20:45:16 +03:00
Alex Gryzlov
54ac723744 add sourcedir option 2019-10-24 20:33:28 +03:00