Commit Graph

8 Commits

Author SHA1 Message Date
Edwin Brady
cf23bae7d6 In IDE mode, look for a ipkg file before loading
This takes the responsibilty of finding the ipkg away from IDE mode,
which seems sensible given that we can do it ourselves. If there isn't
one, it'll load from the local directory as always.
2020-06-09 23:31:30 +01:00
Mark Barbone
c4cdebb578
Fix tests 2020-06-01 19:13:46 -04:00
Edwin Brady
2eb2ce6097 Add Bits primitives
Including appropriate casts, and Num/Eq/Ord/Show implementations.
Also includes new primitives in Data.Buffer, and calls to foreign
functions in C as 'unsigned'.
2020-06-01 11:48:03 +01:00
Edwin Brady
d869eb666c Experiment %syntactic flag on with
This means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.

There are more flags we want on with (well, at least one: "proof")
2020-05-29 16:39:11 +01:00
Edwin Brady
8c5d5055fa Update scheme
Changing the prelude totality default means we need to update the scheme
to be able to cope with its new meaning
2020-05-28 16:05:08 +01:00
Jinwoo Lee
4a52a84113 update golden files 2020-05-25 10:06:52 -07: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
Edwin Brady
a972778eab Add test script
They don't all pass yet, for minor reasons. Coming shortly...
Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 18:25:18 +01:00