Edwin Brady
bf64f843aa
A bit more totality checking polish
...
Need to check for 'assert_total' in getRefs, and get Inf and Lazy the
right way around!
2019-06-25 12:57:49 +01:00
Edwin Brady
0b4f4ec46d
Fix naming issue in totality checker
...
Also added a new test
2019-06-25 10:26:14 +01:00
Edwin Brady
5caa277cbe
Fix some totality issues, add tests
...
These are related to the change in naming and metavariables, mostly
2019-06-25 00:42:52 +01:00
Edwin Brady
fb7190b337
Add first batch of totality checking tests
2019-06-24 18:14:07 +01:00
Edwin Brady
b1acceb870
Add a simple lazy Inf test
2019-06-24 18:08:32 +01:00
Edwin Brady
32583d608d
More interface tests
...
and a small fix for the generation of method types which was okay for
Blodwen, but not here
2019-06-24 18:04:43 +01:00
Edwin Brady
e9514f3c22
Add first interface tests
2019-06-24 17:36:55 +01:00
Edwin Brady
e6292acdf0
Finish adding interactive tests from Blodwen
...
This involved implementing the 'TryWithImplicits' hack for allowing
unbound implicits in types with case blocks
2019-06-24 16:23:32 +01:00
Edwin Brady
1e2fcb8ccd
Fix small error is as patterns
...
Also added new interactive test
2019-06-24 15:30:36 +01:00
Edwin Brady
7a47c9ae0c
Add a couple of interactive tests
2019-06-24 15:16:49 +01:00
Edwin Brady
af9dc69c61
Add record tests from Blodwen
2019-06-24 12:44:34 +01:00
Edwin Brady
0a15c2cda1
Pay attention to visibility of names
...
Name lookup and search should ignore names which aren't visible (that
is, private names in another namespace)
2019-06-24 00:57:22 +01:00
Edwin Brady
67a43e0000
Check names are visible/public
2019-06-24 00:12:58 +01:00
Edwin Brady
9c902de5d1
Fix case tree compiler for coverage checking
...
We can't refine by a name in Rig0 because we can't assume it covers all
possibilities, so only refine by them at the end, at which point we
check that there's only one case left (otherwise we have to match on it,
which is not allowed for an erased thing)
2019-06-23 20:36:06 +01:00
Edwin Brady
6a72508e80
Eliminate cycles in auto search
...
This is important for, e.g. interfaces with parent constraints, so we
don't keep looping making the constraint bigger
2019-06-17 09:50:05 +01:00
Edwin Brady
772b098de0
The Prelude type checks!
2019-06-13 13:23:21 +01:00
Edwin Brady
2374f23320
Add default alternatives
2019-06-11 13:52:49 +01:00
Edwin Brady
07229bdb5e
Add first Idris2 tests
2019-06-11 11:54:47 +01:00
