Commit Graph

11 Commits

Author SHA1 Message Date
Edwin Brady
4ae01d7264 %default doesn't affect interface methods
The required totality of interface methods is now only affected if
there's an explicit modifier on the method. This allows us to set
%default total on the Prelude, which is a good thing to do anyway,
without also requiring that every implementation of the interface in the
prelude has to be total, which would potentially be a pain.

Another good affect is that it speeds up totality checking elsewhere
because totality checking is done lazily, and so with the total flag set
we know in advance that prelude functions are total.
2020-05-28 15:52:03 +01:00
Edwin Brady
9129df359f Simplify doParse
If we're going to use assert_total. we might as well not have the
distinction between empty and non empty results, which only makes the
code harder to follow.

Also there's some kind of issue which seems to mean the token list can't
be erased if we do that. I will investigate if I can make a smaller
example.
2020-05-27 18:16:54 +01:00
Jinwoo Lee
893fbb78c9 Provide sum' and product' separate from sum and product
Not to break backwards compatibility.
2020-05-25 09:59:18 -07:00
Jinwoo Lee
728149f2d1 [prelude] Use foldl for sum and product
To make them tail recursive. Fixes #132.
2020-05-25 09:59:18 -07:00
Edwin Brady
1ea54e764b
Merge pull request #144 from idris-lang/coverage
%default covering
2020-05-24 20:42:08 +01:00
Edwin Brady
222a6a7f31 More fine-grained assert_total in unpack
If it's around the whole thing, it might drop out if unpack is partially
evaluated by the unifier. It should be as fine grained as possible.
2020-05-24 19:13:24 +01:00
Edwin Brady
3ec8631480 More coverage checking fixes
Still a couple of things to resolve in coverage and totality checking
before we can switch on %default, so don't expect quite the right
behaviour just yet. More progress though!

Also working on this has caught a few totality errors in the Idris 2
code base that Idris 1 missed... so these are fixed on the way.
2020-05-24 18:33:43 +01:00
Alex Gryzlov
723f690f7e erase function argument of cong 2020-05-24 05:16:52 +02:00
Edwin Brady
0f724fbc7f Report errors on totality check failure
This means temporarily removing some '%default total' from the libraries
and tests, since the input for codata checking isn't right yet (it needs
appropriate use of inlining)
2020-05-21 13:08:19 +01:00
Kamil Shakirov
b801b97fcc Refactor makefiles 2020-05-19 18:50:47 +06:00
Edwin Brady
dec7dff622 Add libraries 2020-05-18 14:00:08 +01:00