Elaboration and unification using the #213 approach leads to very big trees, while those trees are shared, they're still big trees, additionally close is required again and it ends up being a VERY slow operation.
This changes the representation to a locally nameless one and it also removes the global_var, as they're not needed anymore.
This makes the tests 10x slower, but on the benchmarks the fastest approach uses a lazy version of shifting, which will be implemented in the future.
Goals
A simpler and easier to optimize representation.
Context
Elaboration and unification using the #213 approach leads to very big trees, while those trees are shared, they're still big trees, additionally
closeis required again and it ends up being a VERY slow operation.This changes the representation to a locally nameless one and it also removes the
global_var, as they're not needed anymore.This makes the tests 10x slower, but on the benchmarks the fastest approach uses a lazy version of shifting, which will be implemented in the future.
Related
199