Add support for let bindings and as patterns

[jmchapman]

[jespercockx]

This close to impossible to support with the current architecture of Agda: as patterns are treated as let-bindings, and let-bindings are inlined eagerly in the internal syntax. So we would have to somehow reconstruct which terms correspond to a let-bound variable.

[jespercockx]

Actually, let-bindings do not work either, for the same reason.

[flupe]

Related: agda/agda#7253

[anka-213]

Would preserving record update syntax currently be impossible for the same reason? It would be nice to have, so we can generate record update syntax in Haskell. Currently record update syntax is expanded to constructing a new record from scratch and I guess that it's expanded like that in Agda's internal syntax, so we can't distinguish between record update and manually constructed records in agda2hs?

[jespercockx]

I think all record expressions get desugared to constructor applications in the internal syntax, so there's indeed no way to know from just the internal syntax. We could try to guess, or we could have specific functions compile to a record update. But neither of these are as nice as what we would be able to do if we had access to the surface-level Agda syntax.