Commit Graph

970 Commits

Author SHA1 Message Date
Markus Pfeiffer
63ddd149ed Remove a superflousy declared argument to idris2_openFile
This didn't cause a problem before as it was likely just ignored by the C
function. According to Edwin the extra argument is a leftover from when this
was a pure scheme call.
2020-07-07 11:44:37 +01:00
arty
1d14026f9d Add comment about TTC files in TTC error 2020-07-07 11:20:04 +01:00
Nick Drozd
7d5788471d Update tests 2020-07-07 10:48:23 +01:00
Nick Drozd
2ae6e06565 Simplify Fin 2020-07-07 10:48:23 +01:00
Nick Drozd
7d1ee9dd08 Simplify Equality 2020-07-07 10:48:23 +01:00
Nick Drozd
48fe4382eb Simplify List 2020-07-07 10:48:23 +01:00
Nick Drozd
877f3702ad Simplify Maybe 2020-07-07 10:48:23 +01:00
Nick Drozd
465be9cb86 Simplify Either 2020-07-07 10:48:23 +01:00
Nick Drozd
faabbfcea1 Add some Uninhabited implementations 2020-07-07 10:48:23 +01:00
Nick Drozd
7c923944ae Add %default total to a few modules 2020-07-07 10:48:23 +01:00
Michael Birch
5c9339bde8
Merge sort implementation for Vect (#417) 2020-07-07 10:25:42 +01:00
Rui Barreiro
ca7a6cecff fix switch from takeLast to extension 2020-07-06 20:36:48 +01:00
Rui Barreiro
e8fc14e890
Update src/Compiler/ES/Javascript.idr
Co-authored-by: Andy Lok <andylokandy@hotmail.com>
2020-07-06 20:24:11 +01:00
Edwin Brady
77ad6eac0a
Merge pull request #422 from edwinb/record-implicits
Pay attention to implicits in record update
2020-07-06 18:06:43 +01:00
Edwin Brady
0cf37f621b Pay attention to implicits in record update
Resolves #421
2020-07-06 17:39:55 +01:00
Rui Barreiro
3acc30599e Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-06 17:09:11 +01:00
Rui Barreiro
a6be3ee104 added nodejs version to README 2020-07-06 17:09:00 +01:00
Rui Barreiro
68c9990c8a moved big foreign functions to support and added outputDir 2020-07-06 16:58:02 +01:00
Niklas Larsson
468c8cbae3
Merge pull request #414 from melted/simple_parser
Add a simple parser combinator library for strings
2020-07-06 17:16:19 +02:00
Edwin Brady
50435cc1a1
Merge pull request #420 from edwinb/some-fixes
Resolving some issues
2020-07-06 15:17:21 +01:00
Edwin Brady
f649a61f4d More accurate comment!
The desugaring of alternatives will correspond, but the variable matches
won't necessarily.
2020-07-06 14:45:36 +01:00
Niklas Larsson
d9e9298eb3
Merge pull request #419 from markuspf/fix-closeDir-name
Fix forward declaration of idris_closeDir
2020-07-06 15:36:23 +02:00
Edwin Brady
abdadead0a More liberal with alternatives in with blocks
Only need to match one possibility (it's essentially impossible to match
more than one after all!). Fixes #297.
2020-07-06 14:23:15 +01:00
Edwin Brady
666ecb36b5 Preserve @ patterns when totality checking case
Resolves #300
2020-07-06 14:03:34 +01:00
Edwin Brady
e25f0a57f9 Use correct implicit generation function
Should make a default implicit, not an auto implicit, when running out
of arguments and expecting a default implicit. Fixes #371
2020-07-06 14:02:45 +01:00
Markus Pfeiffer
0b32bf8a2f Fix forward declaration of idris_closeDir 2020-07-06 13:56:36 +01:00
Niklas Larsson
52c6db09d1 Add <?> for replacing error messages 2020-07-06 14:13:56 +02:00
Niklas Larsson
60a067fab1 Remove dumpState 2020-07-06 13:57:13 +02:00
Tim Engler
14725dac67 Describe what is meant by "use"
I hit a roadblock trying to understand linear types, because I couldn't figure out what is meant to "use" a variable. I eventually think I figured it out, by reading "Linear types can change the world!", but it was not easy to do so. I think a better description of what "use" means would be very helpful for those unfamiliar with linear types, so I took a stab at it. Hope it helps.
2020-07-06 12:38:03 +01:00
Rui Barreiro
b3216758e9 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-06 11:32:59 +01:00
Denis Buzdalov
066b37feb4 Tiny doc fix about combination of import public and import .. as. 2020-07-06 11:23:56 +01:00
Niklas Larsson
5060eaafaf Make things public export to work with bootstrap 2020-07-05 21:51:12 +02:00
Niklas Larsson
af83c9303b Add test and documentation 2020-07-05 21:51:12 +02:00
Niklas Larsson
d779c85df4 Add optional 2020-07-05 21:51:11 +02:00
Niklas Larsson
0e51124a43 Add option 2020-07-05 21:51:11 +02:00
Niklas Larsson
bba15974a5 Add takeWhile
add substring and length primitives to Data.Strings
2020-07-05 21:51:11 +02:00
Niklas Larsson
a78ee1dfca Expand test code a bit with pure parsing 2020-07-05 21:51:11 +02:00
Niklas Larsson
39535bf11a Add lifting 2020-07-05 21:51:11 +02:00
Niklas Larsson
d97789190d Add bounds checking 2020-07-05 21:51:11 +02:00
Niklas Larsson
f290c6c3ce Start on a simple string parser 2020-07-05 21:51:11 +02:00
Edwin Brady
6f8aed5478
Merge pull request #416 from edwinb/with-name
Use a String, not an Int, for case/with names
2020-07-05 20:26:32 +01:00
Edwin Brady
8774df8800 Use a String, not an Int, for case/with names
The Int represented the resolved name, but this isn't guaranteed to be
up to date after reloading and, worse, it doesn't display helpfully. I'm
bored of updating the tests which fail as a result!

This also fixes #407, which is about displaying the wrong name after
reloading the ttc.
2020-07-05 20:02:50 +01:00
Rui Barreiro
35961676bc changed tests 2020-07-05 18:55:34 +01:00
Rui Barreiro
46cc328235 plain javascript backend 2020-07-05 18:34:33 +01:00
Edwin Brady
7a0b25f994
Merge pull request #369 from cypheon/tailrec-unpack
Make Prelude.unpack tail-recursive
2020-07-05 14:11:02 +01:00
Edwin Brady
a9478875b3
Merge pull request #392 from buzden/append-properties
Injectivity and similar properties were added for lists'a append
2020-07-05 14:08:07 +01:00
Edwin Brady
e3dcc2da1b
Merge pull request #354 from stepancheg/generated
Insert @generated marker into generated Scheme files
2020-07-05 14:05:22 +01:00
Edwin Brady
5487290499
Merge pull request #282 from ether42/master
Fix MkRecord signature
2020-07-05 14:03:57 +01:00
Rui Barreiro
88f8e745b1 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-07-05 12:19:45 +01:00
Rui Barreiro
4db8c84fe3 self tail rec 2020-07-05 11:53:45 +01:00