Edwin Brady
f05e088c33
Merge pull request #1368 from Heather/clean
...
windows executables should end with .exe
2014-07-09 19:39:38 +01:00
Edwin Brady
9af885a6e1
Highlight differing implicits in errors
...
But only if there are otherwise no visible differences in the error
2014-07-09 18:59:47 +01:00
Edwin Brady
f5c6883dd7
Update CHANGELOG for unbound implicits
2014-07-09 17:57:52 +01:00
Heather
24acd057c1
windows executables should end with .exe
2014-07-09 16:17:17 +04:00
Edwin Brady
32d47a5304
Ensure erasure happens under 'force'
...
Fixes #1367
I'm not yet convinced there isn't still potentially a similar problem
under other forms of ProjCase, but since these only arise in unusual
circumstances at the moment there isn't a problem *yet*!
2014-07-08 20:46:49 +01:00
Edwin Brady
6f6a167de1
No need for 'using' in HVect
2014-07-08 13:45:20 +01:00
Edwin Brady
505905da12
Remove some needless 'using' blocks
...
since the elaborator is now cleverer
2014-07-08 13:32:54 +01:00
Edwin Brady
99ebe20f15
Merge pull request #1364 from puffnfresh/neweffects-bad-constraints
...
Remove bad Applicative constraints from neweffects
2014-07-08 12:29:36 +01:00
Edwin Brady
2d413784a8
Merge pull request #1363 from bmsherman/parseDef
...
Fix parser for :def REPL command
2014-07-08 12:29:27 +01:00
Edwin Brady
5ffef8982e
Type class resolution fix
...
Check whether any errors introduced by a match are unrecoverable, rather
than merely checking if any more errors are introduced. Otherwise, in
some circumstances (where other problems are resolved by the match) we
might get a type class resolved where it shouldn't be, leading to
mysterious errors later.
Fixes #1365
2014-07-08 12:25:46 +01:00
Edwin Brady
e363c092a2
Better treatment of unbound implicits
...
Now uses the elaborator to generate any necessary extra bindings, using
the same machinery as pattern match elaboration. The end result is that
you no longer need 'using' in a lot of cases (it is still useful if you
want to give explicit types, of course). e.g. this now works as it
stands:
data Elem : a -> Vect n a -> Type where
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs)
This should also reduce the number of weird "no such variable" errors
signfificantly. In particular, it fixes #1354
2014-07-08 02:40:37 +01:00
Brian McKenna
8279c8059a
Remove bad Applicative constraints from neweffects
2014-07-06 16:46:50 -06:00
bmsherman
fc5a9cba5f
Fix parser for :def REPL command
2014-07-06 13:17:25 -04:00
Edwin Brady
3c4bd14521
Merge pull request #1361 from trillioneyes/repl-definitions
...
Repl definitions
2014-07-06 16:10:42 +01:00
Edwin Brady
d9513aa588
Merge pull request #1360 from ziman/case-elab-erasure
...
Make case elaboration respect dots
2014-07-06 16:09:27 +01:00
Edwin Brady
cefb325b51
Merge pull request #1358 from ahmadsalim/documentation/partialevaluation
...
Added some additional documentation for partial evaluation
2014-07-06 16:08:44 +01:00
Matus Tejiscak
61f34560f5
Simplify argsToAlt.
2014-07-06 01:47:50 +01:00
Matus Tejiscak
98352eeb15
Comment clarification.
2014-07-06 01:44:00 +01:00
Matus Tejiscak
019b608d3e
Purify toPats.
2014-07-06 01:08:35 +01:00
Matus Tejiscak
15b9807b33
Disable PAny for repeated patvars.
2014-07-06 00:46:23 +01:00
Matus Tejiscak
2490a15c1c
Implement accessible+inaccessible splitting.
2014-07-05 20:57:07 +01:00
Matus Tejiscak
1e3734863c
More changes to argsToAlt.
2014-07-05 20:47:12 +01:00
Matus Tejiscak
2cc6526fc3
Adjust code around argsToAlt.
2014-07-05 20:17:41 +01:00
Matus Tejiscak
747aaf501c
Extend argsToAlt to return a quadruple.
2014-07-05 20:08:09 +01:00
Alyssa Carter
204ebf5f71
Added support for data definitions
2014-07-04 14:22:57 -07:00
Alyssa Carter
bfdec8f2ba
Removed some commented-out code
2014-07-04 11:58:46 -07:00
Alyssa Carter
c1277c8035
Handling more forms of definition.
...
In particular, it should now be possible to define multiple names at once, and to
leave off type declarations when the type can be inferred.
2014-07-04 11:55:07 -07:00
Ahmad Salim Al-Sibahi
60b1f18d62
Added some additional documentation for partial evaluation
2014-07-04 20:30:00 +02:00
Matus Tejiscak
c201192844
Bring erasure info to the case tree builder.
2014-07-04 17:22:47 +01:00
Matus Tejiscak
d8ed044c94
Add getInaccessibleArgs.
2014-07-04 17:06:51 +01:00
Matus Tejiscak
2e9c299b47
Add ReaderT to CaseBuilder.
2014-07-04 14:45:09 +01:00
Matus Tejiscak
b0cb4e2aaa
Create the CaseBuilder monad alias.
2014-07-04 14:03:05 +01:00
Alyssa Carter
a5e8ca30aa
Changed :let to work with an arbitrary number of PDecls (though only one name at a time for now).
...
It is no longer possible to leave off the type declaration. This will be fixed soon.
2014-07-03 15:32:44 -07:00
Alyssa Carter
e26074179c
Preliminary support for a :let command in the repl
2014-07-02 16:12:07 -07:00
Edwin Brady
f2e30f26ee
Merge pull request #1352 from Heather/string
...
Predicates for Prelude Strings
2014-07-01 11:41:55 +01:00
Edwin Brady
59ebac45ae
Merge pull request #1345 from bmsherman/idrisNetFix
...
Fix typo in Idris network C code
2014-07-01 11:41:41 +01:00
Edwin Brady
9183cd711c
Merge pull request #1336 from Heather/system
...
add system to Effects.System as is
2014-07-01 11:40:46 +01:00
Edwin Brady
f60626f550
Merge pull request #1334 from Melvar/fix-ipc-enc
...
Set the handles used for --client to use UTF-8
2014-07-01 11:40:13 +01:00
Edwin Brady
fc947a6d9e
Merge pull request #1229 from LeifW/travis_deps
...
Don't bother installing data-lens
2014-07-01 11:39:44 +01:00
Heather
97e0778488
Predicates for Prelude Strings
2014-07-01 08:54:13 +04:00
raichoo
ed971db126
Merge pull request #1349 from raichoo/javascript
...
javascript: simple dead code elimination
2014-06-30 22:02:04 +02:00
raichoo
baf52184fd
javascript: simple dead code elimination
2014-06-30 21:25:55 +02:00
David Christiansen
7064d6dcd3
Merge pull request #1344 from mrb/maximum_succ_proof
...
suc{Max,Min}{L,R} + add mrb to CONTRIBUTORS
2014-06-30 20:16:10 +02:00
David Christiansen
49cf17932b
Merge pull request #1346 from bmsherman/searchVarMatching
...
Correctly count applications of variables in :search
2014-06-30 20:15:39 +02:00
David Christiansen
9040aba62b
Merge pull request #1348 from david-christiansen/quasiquote
...
Add goal types to quasiquotes.
2014-06-30 20:14:38 +02:00
David Raymond Christiansen
dac312b626
Add goal types to quasiquotes.
...
A quasiquote expression can be given a goal type for the elaborator,
which helps with disambiguation. For instance, `(() : ()) quotes the
unit constructor, while `(() : Type) quotes the unit type. Both goal
types and quasiquote are typechecked in the global environment.
2014-06-30 18:49:22 +02:00
Heather
ded4d17deb
add system to Effects/System neweffects
2014-06-30 15:06:37 +04:00
Heather
81a1dde6d4
add system to Effects.System as is
2014-06-30 15:06:36 +04:00
raichoo
a3ccdefb54
Merge pull request #1347 from raichoo/javascript
...
Javascript
2014-06-30 11:22:03 +02:00
bmsherman
78b29239b1
Correctly count applications of variables in :search
2014-06-30 01:09:08 -04:00
