Generic traversal `everywhere` macro for Hackett

everywhere.rkt

#lang racket/base

(require
  (for-syntax
   racket/base
   syntax/parse)

  (only-in hackett #%app)
  hackett/private/base
  hackett/private/adt)

; Problems with this implementation:
;  Only the outermost datatype is traversed. Other ADTs
;  referenced in fields are not traversed.
;
;  The type to traverse must be fully ground; no foralls
;  anywhere. I'm not sure what a good implementation
;  should do.
;
;  Uses violating these restrictions get poor error messages.

(provide everywhere)

(begin-for-syntax
  (define-syntax-rule (values->list e)
    (call-with-values (lambda () e) list)))

(define-syntax (everywhere stx)
  (syntax-parse stx
    [(_ e f)
     #:with (_ e-erased e-type) (values->list (τ⇒/λ! #'e '()))
     #:with (_ λ-erased λ-type) (values->list (τ⇒/λ! #'f '())) 
     (attach-type
      #'(#%defer-expansion
         (everywhere-stage2 e-type e-erased λ-type λ-erased))
      #'e-type)]))

(define-syntax (everywhere-stage2 stx)
  (syntax-parse stx
    #:literals (#%type:con)
    [(_ e-type e-erased f-type f-erased)
     #:with (#%type:con to-traverse:type-constructor-val) (apply-current-subst #'e-type)
     #:with (to-transform^) (generate-temporaries (list #'to-transform^))
     #:do [(type<:!
            #'(#%type:app (#%type:app (#%type:con ->) (#%type:wobbly-var to-transform^))
                          (#%type:wobbly-var to-transform^))
            #'f-type
            #:src this-syntax)]
     #:with (#%type:con to-transform) (apply-current-subst #'(#%type:wobbly-var to-transform^))
     #:with [data-con:data-constructor-val ...] (attribute to-traverse.data-constructors)
     #:with (clauses ...)
     (for/list ([this-con (syntax->list #'(data-con ...))])
       (generate-clause #`(to-transform to-traverse f mapper #,this-con)))
     #'(letrec ([mapper (lambda (x f)
                          (case x clauses ...))])
         (mapper e-erased f-erased))]))

; generate a clause of the lambda* traversing the ADT.
;
; Example:
; (generate-clause #'Name #'Expr #'f #'mapper #'app)
; =>
; [[(app e1 e2)] (app (mapper e1 f) (mapper e2 f))]
;
; Example:
; (generate-clause #'Name #'Expr #'f #'mapper #'ref)
; [[(ref e)] (ref (g e))]
;
(define-for-syntax (generate-clause stx)
  (syntax-parse stx
    [(to-transform to-traverse f mapper con:data-constructor-val)
     #:with (((~literal #%type:con) field-type) ...) (data-constructor-field-types '() #'con.type)
     #:with (arg ...) (generate-temporaries #'(field-type ...))
     #:with (res ...)
     (for/list ([ft (syntax->list #'(field-type ...))]
                [a (syntax->list #'(arg ...))])
       (cond
         [(free-identifier=? ft #'to-transform) #`(f #,a)]
         [(free-identifier=? ft #'to-traverse) #`(mapper #,a f)]
         [else a]))
     #'[(con arg ...) (con res ...)]]))

example.rkt

#lang hackett

(require "everywhere.rkt")

(data Expr
      (lam Integer Expr)
      (ref Integer)
      (app Expr Expr)
      #:deriving [Show])

; We want to implement this traversal:
;
; (defn adjust-indexes
;   [[n e] (map-names e (lambda [x] (+ x n)))])
;
; (defn map-names
;   [[(ref x) f] (ref (f x))]
;   [[(lam x b) f] (lam (f x) (map-names b f))]
;   [[(app e1 e2) f] (app (map-names e1 f) (map-names e2 f))])

; Notice that it is not necessary to explicitly provide
; everywhere with the type to traverse or the
; type to transform, given they can be filled in
; by type inference. We do need to provide the type for
; adjust-indexes so that the type of e is available.
(defn adjust-indexes : (-> Integer (-> Expr Expr))
  [[n e] (everywhere e (lambda [x] (+ x n)))])

(adjust-indexes 3 (lam 1 (app (ref 1) (ref 1))))