[plt-scheme] How to implement custom macro expanders that use syntax objects

MzScheme macros are implemented by transformer procedures that consume
an "expression" syntax object and produce an "expression" syntax
object. (In a definition context, the "expression" can actually be a
definition.)

New syntactic forms with non-"expression" sub-forms can support macro
transformers for the sub-forms. Typically, a sub-form transformer
should not be used as an expression transformer. To distinguish
sub-form transformers from expression transformers, the sub-form
transformer can be wrapped in a structure:

 (define-struct sub-form-macro (transformer))

 (define-syntax X 
   (make-sub-form-macro
     (lambda (sub-form-stx)  ...)))

The implementation of the new syntactic form can recognize sub-form
macro bindings using `syntax-local-value':

 (syntax-case stx ()
  [(id . _)
   (let ([v (syntax-local-value #'id #f)])
    (cond
     [(sub-form-macro? v)
      ;; apply macro transformation...
      ...]
     [else
      ;; not a macro sub-form
      ...]))

Applying the macro transformation is mostly a matter of applying the
transformation procedure. To support the same hygiene benefits as
expression transformers, however, the input syntax to the transformer
should be marked, and the result should be marked again (where the
marks cancel on parts of the output that were present in the input,
and thus stick only to new parts of the output):

  (let ([i (make-syntax-introducer)])
    (let ([expanded-stx (i ((sub-macro-form-transformer v) 
                            (i stx)))])
      expanded-stx))

This isn't quite right, though. The problem is that a macro expander
needs to handle two tasks:

 * using marks (i.e., an "introducer") to track introduced identifiers,
   and

 * certifying introduced identifiers.

For the latter, the certificates need to originate from the context of
the macro *definition*. Thus, we need to refine the definition of a
sub-form macro:

 (define-struct sub-form-macro (transformer certifier))

 (define-syntax X 
   (make-sub-form-macro
     (lambda (sub-form-stx)  ...)
     (syntax-local-certifier)))

Conceptually, this certifier can then be used on the expanded result,
using the introducer as the last argument:

  (let ([i (make-syntax-introducer)])
    (let ([expanded-stx (i ((sub-macro-form-transformer v) 
                            (i stx)))])
      ((sub-macro-form-certifier) expanded-stx #f i)))

This is still not quite right, though, because the result syntax object
is likely to be deconstructed by further processing of the form, and
deconstructing the term will lose the certificates. Thus, the
certificates should be applied only at the leaves of the
transformation.

The example below shows how a "certify" procedure is threaded through
an expansion, extended during macro expansions, and applied only at the
leaves. To summarize, the key parts of the implementation are:

 1. Capture a certifier at the same time as the transformer procedure
    is evaluated, so that the certifier is associated with the defining
    context (not the use context, which is already handled by the
    expression macro expander for the enclosing form).

 2. Mark before and after transforming by using a fresh introducer
    procedure.

 3. At the leaves of the transformer result, apply the certifier ---
    using the introducer, so that the certificates apply to introduced
    expressions.

----------------------------------------

#|

(stlc <stexpr>) returns a function that because like the
statically-typed expresson <stexpr> --- assuming that the result
is used consistent with its type.

 <stexpr> = <id>
          | (lambda (<id> : <type>) <stexpr>)
          | (<stexpr> <stexpr>)

  <type> = ?
         | (<type> -> <type>)

where "?" is "the Scheme type".

Examples:
 (stlc ((lambda (x : ?) x) (lambda (y : ?) y))) => syntax error: ill-typed
 (stlc ((lambda (x : (? -> ?)) x) (lambda (y : ?) y))) => a procedure
 (stlc (let (x : (? -> ?) (lambda (y : ?) y)) x)) => a procedure

|#

(module stlc-helper mzscheme
  (define-struct stlc-macro (transformer certifier))
  (provide (struct stlc-macro (transformer certifier))))

(module stlc mzscheme
  (provide stlc
	   define-stlc-syntax)
  (require-for-syntax stlc-helper)

  (define-syntax define-stlc-syntax
    (syntax-rules ()
      [(_ id expr) (define-syntax id (make-stlc-macro
				      expr
				      (syntax-local-certifier)))]))

  (define-syntax (stlc stx)

    (define (expand-stlc v exp env cert)
      ;; Generate a "mark" to track introductions:
      (let ([i (make-syntax-introducer)])
	;; Mark, transform, and mark:
	(let ([expanded-stx (i ((stlc-macro-transformer v) 
				(i exp)))])
	  ;; Continue parsing with expanded expression, and
	  ;;  extend the certifier to add certificates from
	  ;;  the macro v:
	  (type-expr expanded-stx
		     env
		     ;; Replace the following with (lambda (x) x)
		     ;;  to see the last example below fail
		     (lambda (id)
		       ((stlc-macro-certifier v) (cert id) #f i))))))

    (define (type-expr expr env cert)
      (let ([v (syntax-case expr (lambda)
		 [(id . rest)
		  (identifier? #'id)
		  (syntax-local-value (cert #'id) (lambda () #f))]
		 [_else #f])])
	(if (stlc-macro? v)
	    ;; Expand the macro:
	    (expand-stlc v expr env cert)
	    ;; Parse normally:
	    (syntax-case expr (lambda)
	      [id
	       (identifier? #'id)
	       ;; Type an id:
	       (let ([t (ormap (lambda (binding)
				 (and (bound-identifier=? (car binding) #'id)
				      (cdr binding)))
			       env)])
		 (if t
		     ;; Return certified id:
		     (values (cert #'id) t)
		     ;; No type in env:
		     (raise-syntax-error
		      #f
		      "free variable"
		      stx
		      expr)))]
	      [(lambda (id : ty) body)
	       ;; Function
	       (let ([arg-t (parse-type #'ty)])
		 (let-values ([(body body-t)
			       (type-expr #'body
					  (cons (cons #'id arg-t)
						env)
					  cert)])
		   (values #`(lambda (id) #,body)
			   `(,arg-t -> ,body-t))))]
	      [(e1 e2)
	       ;; Application
	       (let-values ([(e1 t1) (type-expr #'e1 env cert)]
			    [(e2 t2) (type-expr #'e2 env cert)])
		 (unless (and (list? t1)
			      (equal? (car t1) t2))
		   (raise-syntax-error
		    #f
		    "ill-typed application"
		    stx
		    expr))
		 (values #`(#,e1 #,e2)
			 (caddr t1)))]
	      [_
	       (raise-syntax-error
		#f
		"bad expression"
		stx
		expr)]))))

    (define (parse-type ty)
      (syntax-case ty (? ->)
	[? '?]
	[(t1 -> t2)
	 (list (parse-type #'t1)
	       '->
	       (parse-type #'t2))]
	[else
	 (raise-syntax-error
	  #f
	  "bad type expression"
	  stx
	  ty)]))

    (syntax-case stx ()
      [(_ expr)
       (let-values ([(expr ty) (type-expr #'expr null (lambda (x) x))])
	 expr)])))

(require stlc)

;; Hygiene example (where `let' expands to `lambda'):
(define-stlc-syntax let
  (syntax-rules (:)
    [(_ (id : t val) body) ((lambda (id : t) body) val)]))
(stlc (lambda (lambda : ?) (let (y : ? lambda) y)))

;; Certificate example:
(module m mzscheme
  (require stlc)
  (provide b)
  
  ;; `a' is not exported:
  (define-stlc-syntax a
    (syntax-rules ()
      [(_ x) x]))

  (define-stlc-syntax b
    (syntax-rules ()
      [(_ x) (a x)])))
(require m)
;; Expansion of `b' includes a reference to `a' that must
;; be certified:
(stlc (lambda (x : ?) (b x)))