This ignores empty lines in the REPL and doesn't show a parse error on
CTRL+D/EOF anymore.
Add NOP variant to REPLCmd to represent an empty command.
Split command in eoi or nonEmptyCommand. nonEmptyCommand is still
guaranteed to consume input. command may be eoi in which case it does
not consume input.
Print a newline after receiving EOF on the console. Since this is only
relevant in the REPL (quiet or not) this uses putStrLn rather than
iputStrLn.
Elaborate the scope of a let without the computational behaviour,
meaning that `let x = v in e` is equivalent to `(\x => e) v`. This makes
things more consistent (in that let bindings already don't propagate
inside case or with blocks) at the cost of not being able to rely on the
computational behaviour in types. More importantly, it removes a
significant potential source of slowness.
Fixes#58
If you need the computational behaviour, you can use a local function
definition instead.
This is for finding support libraries for code generators, e.g. the
shared objects that chez will load for glue code for foreign libraries.
It'll be used more shortly...
Fixes#42. If we don't do this, the name is treated in the saem way as
an unbound implicit, which is not what we want, so update with the
method applied to the parameters.
Just like all other pi-bound things, if m is an unbound implicit and we
have m ?x = m y as a unification problem, we can conclude ?x = y because
it has to be true for all ms.
This was implemented in Blodwen but I hadn't got around to it yet for
Idris2... fortunately it's a bit easier in Idris2!
Fixes#44
This will be useful shortly, and in general because it'll give us more
flexibility in unification to be able to spot things which are
guaranteed invertible like constructors.
We were only checking parameters, meaning that there were potential
clashes leading to confusing behaviour, and meaning that it was somehow
relevant what the names were in the interface!
Now by marking a method as multiplicity 0, we can explicitly say that
it's compile time only, so we can use it to compute types based on other
erased things - see tests/idris2/interface008 for a small example.
This fixes#8 - at least in that it allows the interface to be expressed
properly now, although the multiplicity annotations mean that
unfortunately it can't be compatible with Idris 1.
Don't use the interface itself when checking parent implementations
exist, otherwise we'll end up in a cycle (because the parent
implementation will sort of exist as a result!)
This means that even if the relevant parameters aren't used by a method
body, the method can still see what the implicits are (though they will
be 0 multiplicity).
This is relevant to #8, but doesn't really fix it because we still need
a way of saying that methods are 0 multiplicity.
We need to turn pairs into separate constraints, which is a bit of a
hack but the constraints need to be separate in order to build the
chasing functions which find the parent constraints correctly.
Possibly there is a neater way, which is to teach the search algorithm
to look in the hints for pairs, but that's a lot more complicated (and
probably unnecessarily so).
Fixes#25
This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.
These are 'nested' namespaces which are a bit special in that even
private names are visible from the enclosing namespace. This gets the
behaviour for record visibility from Idris 1.
Now supports with applications on the RHS when auto implicits are
involved. Auto implicit bound names in patterns now become searches on
the rhs in a with-application (I should write this construct up properly
in a paper some time!)
We use this to decide whether a determining argument is satisfied or not
for unbound implicits. We can tell from the name, which would be a PV,
but this way relies on fewer assumptions.
Elaborate via either === (homogeneous equality) or ~=~ (heterogeneous
equality) both of which are synonyms for Equal. This is to get the Idris
1 behaviour that equality is homogeneous by default to reduce the need
for type annotations, but heterogeneous if that doesn't work.
Idris 1 will fill in the last metavariables by matching rather than
unification, as a convenience. I still think this is okay, even if it's
a bit hacky, because it's a huge convenience and doesn't affect other
unification problems.
Also abstract over lets in guesses, like in delayed elaborators, to
avoid any difficulties when linearity checking and to make sure that let
bound things don't get reevaluated.
This is enough to get the Chapter 6 TypeDD tests working
Where "simple" means the solution is just a local variable or smaller
metavariable application. This is a big win when environments get big,
and I suspect there might be more where this came from if we always
shrink the environments of metavariable solutions as far as possible. It
really saves a lot of work in "quote" in particular.
