Niklas Larsson
e86b0f6d0a
Check for TTY when setting colour
...
This means that when doing a redirect to file, one doesn't have to turn
off colour manually.
2015-08-28 18:42:06 +02:00
David Christiansen
378bbd6f98
Merge pull request #2560 from jeremy-w/patch-1
...
Fix typo in doc comment
2015-08-28 08:45:11 -07:00
Jeremy W. Sherman
5b841fb7b1
Fix typo in doc comment
...
Reported by user Freefood in #idris on Freenode.
2015-08-28 07:37:39 -04:00
David Christiansen
102bd6b523
Merge pull request #2558 from david-christiansen/windows-colour
...
Experimental support for console colours on Windows
2015-08-27 16:41:10 -07:00
David Raymond Christiansen
dfba993f4c
Experimental support for console colours on Windows
2015-08-27 14:29:38 -07:00
David Christiansen
768ddb1cd2
Merge pull request #2557 from Heather/typo
...
typo: concatenatation -> concatenation
2015-08-27 08:45:58 -07:00
Heather
50104a4c1c
typo: concatenatation -> concatenation
2015-08-27 17:20:23 +04:00
David Christiansen
0b3f26087d
Merge pull request #2551 from david-christiansen/wip/tactical
...
Insert namespace information to declaration-level %runElab
2015-08-26 22:45:27 -07:00
David Christiansen
7642503875
Merge pull request #2554 from LeifW/remove_lens_dep
...
Remove direct dep on lens
2015-08-26 17:36:32 -07:00
David Raymond Christiansen
ffb50e2023
Insert namespace information to declaration-level %runElab
2015-08-26 17:07:01 -07:00
Leif Warner
13623f63f7
Remove direct dep on lens
...
While lens is a transitive dep of trifecta, we're not using it directly.
Don't think specifying ranges on it is helpful for us.
2015-08-26 15:26:07 -07:00
Niklas Larsson
3e9a19e7fe
Merge pull request #2553 from melted/icon2
...
Added the icon in the wrong dir
2015-08-26 22:15:59 +02:00
Niklas Larsson
dec64c40fc
Added the icon in the wrong dir
2015-08-26 22:14:52 +02:00
Niklas Larsson
9af1241c90
Merge pull request #2552 from melted/icon
...
Add a windows icon.
2015-08-26 21:59:41 +02:00
Niklas Larsson
659ab8ce93
Add a windows icon.
2015-08-26 21:58:25 +02:00
David Christiansen
822142ab0a
Merge pull request #2548 from david-christiansen/wip/tactical
...
Latest Elab reflection updates in preparation for upcoming release
2015-08-26 09:10:28 -07:00
David Christiansen
7b580241ea
Merge pull request #2547 from Melvar/fix-number-show
...
Fix show for negative numbers
2015-08-26 09:08:09 -07:00
Edwin Brady
f5aecf7bb7
Deferred autos
...
These should be solved after type class resolution - they are intended
as 'side conditions' that can be proved independently, so they aren't
supposed to influence resolution. Fixes #2549 .
2015-08-26 11:50:51 +01:00
Edwin Brady
81e19625f2
Type class resolution shouldn't use match_apply
...
This can resolve things too early which shouldn't be resolved. We only
had match_apply as a workaround for some earlier bugs...
2015-08-26 10:38:13 +01:00
David Raymond Christiansen
a297e02d29
Fix typo in docstring for Tactics.apply
2015-08-25 19:00:09 -07:00
David Raymond Christiansen
a953ba2762
Update test for new API
2015-08-25 17:38:03 -07:00
Melvar Chen
9dd4233da4
Adjust test primitive002 to backends' output
2015-08-26 02:35:00 +02:00
Melvar Chen
c51bf7eca5
Fix comparison ops in JS backend
2015-08-26 02:35:00 +02:00
Melvar Chen
deb4d41599
Show Double with full precision on C backend
2015-08-26 02:35:00 +02:00
Melvar Chen
073d5efad7
Fix primitives002 to do what it's supposed to
2015-08-26 02:34:59 +02:00
David Raymond Christiansen
6432db2140
Show MNs that occur in the goal in the interactive provers
...
Previously, some assumptions were erroneously hidden, because we only
checked for relevance to the other assumptions.
Fixes #2545 .
2015-08-25 15:52:16 -07:00
David Raymond Christiansen
7bde028b12
Use subst for intro, rather than updsubst
...
This is because we are introducing things that aren't holes, and the
application status being "complete" might block for substitution of an
introduction. This fixes a bug in the interactive prover and the
interactive elaborator where introduction only worked when precisely the
same name was provided, becuase it was incompletely substituted.
2015-08-25 15:51:54 -07:00
David Raymond Christiansen
29e29c20bf
Add letbind to Elab reflection
2015-08-25 12:40:03 -07:00
David Raymond Christiansen
ce764bf33f
Split Tactics.intro into two versions
...
Most uses in my real code called the (Just n) variant, and this was
needlessly noisy. Now, the surface API just takes a name, and there's an
alternate version to figure out the name.
2015-08-25 12:20:21 -07:00
Melvar Chen
a097d05384
Adjust test for changed negative number output
2015-08-25 02:18:25 +02:00
David Raymond Christiansen
93761d531a
Fix source locations for decl syntax
...
The new decl syntax directive caused errors to be reported at the syntax
declaration site rather than the use site. Now, they are reported at the
use site. The solution used is the same as for the term syntax fix.
2015-08-24 16:43:27 -07:00
David Raymond Christiansen
9e8a976383
Merge remote-tracking branch 'upstream/master' into wip/tactical
2015-08-22 14:49:10 -07:00
Edwin Brady
0655d3d96d
Allow syntax rules at the declaration level
...
decl syntax [lhs] = decl1
decl2
...
The lhs has the same form as expression syntax rules, except that any
names bounds in braces {n} are replaced in top level name bindings as
well as explicit lambda/pi/let bindings.
This is mostly intended to be used in conjection with top level %runElab
declarations, but probably has wider use.
2015-08-22 16:58:35 +02:00
Melvar Chen
cd1d1c830b
Fix showing of negative numbers in primitive types
2015-08-22 13:09:56 +02:00
David Raymond Christiansen
766b73a0a5
Look up operator fixity in Elab
...
This is necessary for deriving good Show instances on infix operators.
2015-08-21 17:52:54 -07:00
David Christiansen
b693b814aa
Merge pull request #2540 from david-christiansen/wip/tactical
...
Recent updates and bug fixes for Elab reflection
2015-08-21 16:16:31 -07:00
David Christiansen
77324bdeff
Merge pull request #2539 from david-christiansen/hl-kw
...
Better error when asking for non-existent goal type
2015-08-21 15:56:23 -07:00
David Raymond Christiansen
ab63941a04
Added top-level %runElab support
...
Now, %runElab also works in a declaration context, eliminating the need
for a useless definition of type () when running for side effects.
2015-08-21 15:10:43 -07:00
Edwin Brady
239c8caffa
Move resolveTC to ProofSearch.hs
...
It is, in some sense, a proof search, and this means that auto proof
search can now solve things which require type class resolution.
One side-effect is that type class resolution will now only solve holes
which actually are type classes! So this may break code which was
abusing the type class resolution mechanism - such code can most likely
be rewritten to do proof search.
2015-08-21 17:54:31 +02:00
Edwin Brady
3288a6c8b0
Fix coverage checker for sigma types
...
Using the old name meant it checked the wrong thing so always reported
covering cases
2015-08-21 17:54:31 +02:00
Edwin Brady
0140e67bc9
Tweak to hole lifting
...
Where the hole has a function type, it should display the whole function
type!
2015-08-21 17:54:31 +02:00
David Raymond Christiansen
fbb201c5ff
Merge branch 'hl-kw' into wip/tactical
2015-08-20 22:40:02 -07:00
David Raymond Christiansen
d741a30ed5
Extra info for errors in advanced mode
...
When showing error context information, display the difference between
unification and conversion errors. This is convenient when debugging
Elab scripts.
2015-08-20 22:37:27 -07:00
David Raymond Christiansen
1c87b5e26a
Thread the fresh name counter through runElab
...
Before, recursive reflected elaborator invocations could lead to name
capture, because each recursive invocation had its own fresh name
counter. This made combining their results unsafe. Now, they share a
counter, which makes it safe again.
2015-08-20 22:36:07 -07:00
David Raymond Christiansen
6ada023143
Better error when asking for non-existent goal type
2015-08-20 21:44:59 -07:00
raichoo
ba3fab0800
Merge pull request #2538 from raichoo/master
...
javascript: support prim_eqPtr
2015-08-20 21:52:01 +02:00
David Christiansen
d0b6faf026
Merge pull request #2536 from david-christiansen/hl-kw
...
Preserve binder locations in custom syntax
2015-08-20 12:10:48 -07:00
raichoo
39c7ea13e2
javascript: support prim_eqPtr
2015-08-20 20:40:25 +02:00
David Christiansen
02ea51a484
Merge pull request #2535 from david-christiansen/hl-if-then-else
...
Parser-driven highlighting for if/then/else
2015-08-19 17:47:14 -07:00
David Christiansen
a311df12ff
Merge pull request #2532 from david-christiansen/hl-kw
...
Stop traveling through time when highlighting
2015-08-19 17:45:51 -07:00
