[plt-dev] Hunting down an elusive certification bug

On Sat, 28 Feb 2009, Matthew Flatt wrote:

> At Sat, 28 Feb 2009 15:45:11 -0500 (EST), Dimitris Vyzovitis wrote:
>> Where foo is syntax-local-value looked up as a macro, and then called
>> on the syntax (directly, as a function without local expand).
>> The result is deconstructed as #'(pat ...)
>
> That sounds like the problem. When you call a transformer directly,
> then you're taking on the role of the macro expander, and you're
> obligated to do all the same sort of things that the expander does.
>
> If `local-expand' applies, but if you need to pull a syntax-object
> vector apart, then my guess is that the deconstruction is still going
> to cause certificate problems. You might be able to avoid the
> certificate problem by expecting a `begin' form back instead of a
> vector --- just because `local-expand' by default pushes certificates
> down one level when it see a `begin' form.
>
> The more general solution is to do what the macro expander does, which
> is to record a certifier along with the transformer and use it on the
> result, possibly use `syntax-recertify' on pieces that you pull apart,
> and so on. You can see examples of this in `match' (look for
> `match-expander-transform' in the implementation) and `for'.
> Unfortunately, this is all a bit complex, but that's the trade-off in
> implementing your own sub-expander.

This seems to work with minimum pain:

Expansion for splice with:
...
  (let ((intro (make-syntax-introducer)))
    (syntax-local-introduce
     (intro (macro (intro (syntax-local-introduce stx))))))

Where the splicing macro is defined capturing the certifier:
...
  (let (cert (syntax-local-certifier))
     (lambda (x)
       (syntax-case x ()
         ((_ arg ...)
          (with-syntax (((body (... ...)) (list (cert (syntax rule)) ...)))
            (syntax/loc x (body (... ...))))))))))

-- vyzo