It turns out we need a new kind of map, mapping possibly ambiguous names
to values. This is what 'Context' does but we can only have one of them
because it resolves names to a position in an array and it'd be
confusing to have more than one index per name.
Mostly direct from Blodwen (some minor modifications to deal with new
way of going into a new scope in the elaborator as well as the usual
bits dealing with name lookup and Glued terms)
Like Idris 1, these are implicitly added on encountering a repeated name
or a non-constructor application. Unlike Idris 1 (and Blodwen) they are
checking by unification rather than matching (which means in particular
that function argument names can't be bound in dot patterns) which is
slightly less expressive, but better overall because matching is
potentially more error prone.
Slight change of plan: instead of having special names, add Lazy, Inf,
Delay and Force and keywords and elaborate them specially.
Correspondingly, add DelayCase for case trees. Given that implicit
laziness is important, it seems better to do it this way than constantly
check whether the name we're working with is important.
This turns out to make implicit laziness much easier, because the
unifier can flag whether it had to go under a 'Delayed' to succeed, and
report that back to the elaborator which can then insert the necessary
coercion.
This slows things down a bit because to find the holes and give them the
right multiplicities, we need to normalise all the arguments which might
have been metavariables. Maybe we should skip this if we're not using
anything linear, for efficiency?
As patterns are handled by deciding which side of the as is considered
'used'. In case blocks, that should be the variable name, but in general
it should be the pattern, so IAs now has a flag to say which one.
Changed nested names (and case blocks) to store the resolved name as the
outer name, rather than the unresolved name, otherwise we'll have issues
when loading from TTC
When we encounter them, not that they're a binding as normal, but also
record the thing they expand to. Then bind as a PLet, and convert that
to a Let on the RHS so it has computational force. The case tree
compiler knows about as patterns, so they get compiled to use the
appropriate name on the rhs (rather than a let).
This only searches for lambdas and locals so far, and doesn't take into
account that it shouldn't search for holes, but it does set up the basic
mechanism.
Only save the parts of terms and definitions which are needed for
typechecking and evaluation (so, for example, we don't need types for
machine generated metavariables, don't need types on lambdas, etc).
Added Core.Directory (more or less directly from Blodwen) and now
writing out TTCs from the test Main, but it's still not writing out
definitions because we're not yet making a note of the names which need
saving (this will be the defined names and any holes introduced).
Also it's clear from logging that holes/guess/constraints aren't being
cleared so this needs to be fixed next.
This checks lambdas where the type isn't immediately a pi binder. First
normalises, if that doesn't work, just guesses and unifies with the
expected type.
Hole list represented as a map now for quicker deletion of solved holes.
Unification returns whether it solved any holes as part of its result,
so we know if it's worth going back to solve constraints if progress has
been made.
Changed 'check' so that it returns the type as a 'Glued', which is a
pair of a term and its normalised form (or, more accurately, the process
to generate each in Core). Sometimes the elaborator needs Term,
sometimes in needs NF; this way we can return both but only actually
generate it when its needed.
So far, mostly done applications, binders and variables. Unification is
still to do.
Better to have the elaborator across multiple files, for ease of
navigation. Also abandon the idea of local unification variables -
we'll keep them global, and try let binding them on leaving a scope.
Also removed 'MV' as a special name type, and added a Meta constructor
in TT which is applied to exactly the right number of arguments for the
environment the meta was constructed in.
It's possible the local unification UCtxt may be more trouble than it's
worth! Instead perhaps we can try let binding unification solutions where
possible on leaving the scope in which they're introduced.
Unification based only on constructor arguments and matching - anything
else fails. Idea is to solve 'easy' local unification problems quickly,
without having to create a global metavar applied to the current context.
