Move away from the current `rewrite` macro implementation

[LPTK]

The rewrite macros comprise top-level rewrite calls from the RuleBasedTransformer class, as well as term-level t.rewrite calls, which desugar into the same.

These are currently expanded into calls to RuleBasedTransformer#registerRule – conceptually, an invocation such as rewrite { case code"t" if c => rhs } expands into:

registerRule(
  expression representation of code pattern t, 
  extractArtifact => {
    // ... extract the different trees obtained from extractArtifact
    // ... and pass them through the sub-patterns
    //       (for example, see `SubPattern` in `case code"${SubPattern(x,y,z)}:Int" => ...`)
    if (the guard/condition c of the pattern matching case is respected)
      Some(adapted version of rhs)
    else None
  }
)

This is generated after some crazy macro hackery during which untypecheck is used to get around owner chain corruptions, which incurs limitations on what can go inside a rewrite rule right-hand side. It incurs problems with path-dependent types, some of which are fixed in a very ad-hoc way.

A saner approach would likely be to perform the main code transformation before type checking (using a macro annotation), since the translation is mostly syntactic anyway. But we would have to split from that code the functionality that inspects the types of the pattern and right-hand side in order to refine the type of the rewritten term and to check that the transformation is type-preserving. Indeed, that functionality needs to be expressed in a macro def, as it requires type checking information – but the good news is that it does not change the shape of the tree and should not result in owner chain problems.