The model of wrapper + desc similar to the OCaml compiler is convenient as it provides some additional guarantees, such as that every term has a location, type annotation or another other property.
But it isn't really needed and it adds some code complexity, now every function needs an additional tt_syntax_func, additionally some terms don't need a wrapper.
This provided a couple meaningful % improvement on the equality check.
Goals
Faster and easier to work with representation.
Context
The model of
wrapper + descsimilar to the OCaml compiler is convenient as it provides some additional guarantees, such as that every term has a location, type annotation or another other property.But it isn't really needed and it adds some code complexity, now every function needs an additional
tt_syntax_func, additionally some terms don't need a wrapper.This provided a couple meaningful % improvement on the equality check.
Related
199