edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-22 04:11:31 +03:00
Code Issues Projects Releases Wiki Activity
651 Commits 2 Branches 1 Tag 4.2 MiB
3a436061ca
Commit Graph

651 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
df3f8b73f8 Further tweak to linearity rules 
When we check a scope in RigW, need to mark all linear things outside
that scope as irrelevant within the scope (since the scope may be used
multiple times).
 2019-12-29 15:21:08 +00:00
Edwin Brady
6d0c4d9ea8 Slight tweak to linearity checking rules 
Need to reset mutiplicity to 1 when checking a new scope.
 2019-12-27 17:13:39 +00:00
Arnaud Bailly
c385a2a9cc Merge branch 'master' of https://github.com/edwinb/Idris2 into better-ide-mode 2019-12-27 09:25:55 +01:00
Christian Rasmussen
a70c68da91 Add test for Double subtraction 2019-12-22 21:50:18 +01:00
Christian Rasmussen
479872290d Fix Double subtraction in interpreter 
Fixes #171
 2019-12-22 20:48:00 +01:00
Timmy Jose
1c1e2b16ca Reorder Scheme compilers order to pick Chez Scheme first. 
This fixes the issue where some Scheme compiler like mit-scheme is
installed and that gets picked up first, leading to an infinite
loop in the tests.

Also see attached image in the PR.
 2019-12-21 18:42:09 +05:30
Milan Kral
eb7be5eba1 Use HTTPS instead of HTTP 2019-12-18 21:37:50 +01:00
Edwin Brady
e0eecc8c12 Small tweak to auto search rules 
After resolving default hints, go back to normal hints because resolving
the top level default might have opened up further search possibilities.
 2019-12-14 23:29:28 +00:00
Edwin Brady
f95214ff8c Need to save types on lambdas in TTC 
Turns out we need this after all, since the types may be necessary
during linearity checking if imported names are imported and reduced
during elaboration for some reason (e.g. during unification)
 2019-12-13 17:02:46 +00: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
Arnaud Bailly
d5e63338ca Merge remote-tracking branch 'upstream/master' into better-ide-mode 2019-12-08 13:09:08 +01: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
Alex Gryzlov
1652a6be7d Merge remote-tracking branch 'upstream/master' into misc-fixes 2019-11-25 19:18:09 +03: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
Alex Gryzlov
742f8e662a fix total006 test 2019-11-12 17:03:13 +03:00
Alex Gryzlov
f0ca75b537 add some lib fuctions from Idris1 2019-11-12 15:58:21 +03:00
Alex Gryzlov
148698e790 misc fixes and refactorings 2019-11-12 15:58:04 +03: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
cc6dc2839e
implement GetOptions and correctly reply nil when no holes 2019-11-11 09:28:11 +01:00
Arnaud Bailly
fe4fb532cd export Network.Socket functions fix #152 2019-11-11 08:38:10 +01:00
Arnaud Bailly
b536a4b272
fix compile errors following merge 2019-11-10 15:16:18 +01:00
Arnaud Bailly
3eeac400fb [wip] output from IDE mode 2019-10-31 07:14:46 +01:00
Arnaud Bailly
58e2ae2de8 make tests pass, tweaking repl's output 2019-10-31 07:14:46 +01:00