Module Expr.BoxSource

Low-level handling of boxed expressions

This module contains helper functions for Bindlib, and wrappers to use boxed expressions.

We use the boxed_expr = naked_expr box marked type throughout, rather than the more straightforward expr box = naked_expr marked box, because the latter would force us to resolve the box every time we need to recover the annotation, which happens often. It's more efficient and convenient to add the annotation outside of the box, and delay its injection (using lift) to when the parent term gets built.