Inefficient operations to avoid

[ice1000]

I noticed some (can be optimized in obvious ways) inefficient operations used in the codebase of Aya. Here's a list of them I could recall rn:

• Applying multiple substitution on a term before using it. Substitution on a term should be batched to apply once. Each substitution is a traversal of the AST and a reconstruction of the substituted part, which is really bad.
  • As an example, in ExprTycker::visitApp, the instPi call substitutes the telescope EACH TIME we traverse an argument. This is really really bad. We should only substitute ONCE for each element in the telescope. This could be refactored out easily.

Reference: AndrasKovacs/elaboration-zoo#7 (comment)

[ice1000]

I'm thinking about this again. I think a benchmark comparison for substitution will be very interesting to do. I think we could do that. Let's delay the optimization to the time we have small libraries.

I think for now, we could optimize prepend out first.

[ice1000]

Another case: https://github.com/ice1000/aya-prover/blob/3c983d27407ce804e94d825409edbdadefd9c4ce/base/src/main/java/org/aya/tyck/unify/UntypedDefEq.java#L56

[ice1000]

This does not seem like an issue