Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".
A %macro must always be fully applied. Whenever the elaborator
encounters a %macro application (except in a function LHS) it evaluates
the application and sends the result to %runElab. So:
%macro
foo : args -> Elab TT
...
def = foo a b c
is equivalent to
foo : args -> Elab TT
...
def = %runElab foo a b c
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'.
This allows a function to be inlined for totality checking purposes
only. So, for example, (>>=) might be a function, but if it evaluates to
something constructor guarded in some context, then it might still be
productive.
If we never evaluate under Delay at all, we won't inline interface
methods, which means productive things defined in an interface can never
be today. So, make sure to set the tcinline flag before quoting the
Delayed closure.
