Solving later arguments first means that they can refer to solutions of
earlier arguments. This isn't really the best solution for ensuring that
metavariables refer to things defined earlier, but it helps, and it does
fix#304.
Instead of the previous unreliable hack, actually look for occurrences
of the solved metavariable. Block if there are any, and fail if there
are any under a constructor. I had expected this to hurt performance
quite a bit, but it seems it doesn't.
This was prompted by #304, which is now partly fixed, but there's still
a refinement to unification needed to fix it fully (and at least it
doesn't segfault due to the cycle now!)
A bug found via the very handy, but occasionally bad for performance so
off by default, --debug-elab-check. The multiplicity of a lambda type
needs to be checked against the expected multiplicity, not the given
multiplicity. Oops!
If you have any (\0 x => e) or similar, you may find you need to fix a
type error after this update...
At least as long as the number is small enough (currently set to < 100).
This is because it can open up further evaluation opportunities when
typechecking, and can make the term we're working with smaller - it also
makes display a bit neater.
Overall this makes some pathological cases of terrible performance much
better, without hurting anything else.
While Bird Style literate mode is useful, it does not lend itself well
to more modern markdown-like notations such as Org-Mode and CommonMark.
This commit extends Idris2's existing literate mode to recognise both
'visible' and 'invisible' code blocks and lines in predefined markdown
styles.
The styles and their elements are:
+ Bird Style :: `>` denotes a visible code line, `<` a hidden code
line.
+ OrgMode :: Org Mode source blocks for idris are recognised as
visible code blocks, and comment blocks are invisible
code blocks. Invisible code lines are denoted with
`#+IDRIS:`.
+ CommonMark :: Only code blocks denoted by standard code blocks
labelled as idris are recognised.
For backwards compatibility, we recognise literate modes by file
extension:
+ Bird Style :: `.lidr`
+ OrgMode :: `.org`
+ CommonMark :: `.md`
In future we should add support for literate `LaTeX` files, and more
intelligent processing of literate documents using a pandoc like
library in Idris such as: [Edda](https://github.com/jfdm/edda).
It's not actually used as part of any compilation pipeline yet, and I've
only tested it by eyeballing the output, but it'll be useful soon, and
it's good for it to be available to any new back ends that might need
it. It will need some optimisation.
e.g. in a C file. This means we don't accidentally treat things as
empty, since previously we just defined these as empty types, but that
broke coverage checking. Fixes#240
The names the locals were being applied to weren't being updated
properly, so applications of local functions inside case blocks were
sometimes given the wrong arguments. This is one of the few places where
it's hard to keep track of names in the type system! So naturally that'd
be where things go wrong I suppose...
Make desugaring/elaboration of interfaces, interface implementations,
records, and parameter blocks take into account the pragma
`%unbound_implicits off`.
Main changes:
(a) Execute the pragma also during desugaring
(b) Check whether `isUnboundImplicits` is on at each desugaring step
Alternatives I didn't take:
(1) Changing `findBindableNames` to effectfully check the flag.
Rationale:
Apart from turning a pure function into an effectful one, this
would mean repeatedly calling `findBindableNames`, only to do
nothing once the flag is read.
(2) Adding another function that takes multiple places (list of terms)
that might contain bindable names, and before dispatching
`findBindableNames` on each term, checking the flag.
Rationale: I didn't want to add another abstraction. (weak
rationale)
@edwinb @gallais : if you prefer (2), I can do that.
