[racket] Macros baffle me

I don't think you want to use syntax->datum or datum->syntax in this
macro. Here's another way to write it.

Robby

#lang racket
(define-syntax-rule
  (with-vars (vars ...) x)
  (for*/and ([vars (in-list '(#t #f))]
             ...)
    x))

(define-syntax-rule (then x y) (implies x y))
(define equiv equal?)

(define-for-syntax (collect-fvars stx exp)
  (let loop ([exp exp])
    (define (collect stx-lst)
      (apply append (map loop (syntax->list stx-lst))))
    (syntax-case exp (or then and not)
      [(or x ...) (collect #'(x ...))]
      [(and x ...) (collect #'(x ...))]
      [(then x y) (collect #'(x y))]
      [(equiv x y) (collect #'(x y))]
      [(not x) (collect #'(x))]
      [x
       (identifier? #'x)
       (list #'x)]
      [_ (raise-syntax-error #f "unknown expression" stx exp)])))

(define-syntax (tauta stx)
  (syntax-case stx ()
    [(_ exp)
     #`(with-vars #,(collect-fvars stx #'exp) exp)]))

(tauta (or (then P Q) (then Q (not P))))
(tauta (or P (not P))) ; excluded middle
(tauta (or (and P Q) (or (not P) (not Q))))
(tauta (equiv (then P Q) (then (not Q) (not P)))) ;equiv
(tauta (then (and (then (not A) B) (then (not A) (not B))) A))
;reductio ad absurdum
(tauta (equiv (not (and A B)) (or (not A) (not B)))) ; De Morgan's law

On Fri, May 2, 2014 at 8:26 AM, Sean Kanaley <skanaley at gmail.com> wrote:
> Here's a solution (at the bottom) with the datum/syntax converters.  flatten
> is built-in, free-vars is basically filtering stuff and then removing
> duplicates, with-vars can take advantage of the built-in nested for, and
> then tauta.
>
> tauta can get the "quoted" form of the expression like when you used eval by
> calling syntax->datum on the syntax given to tauta, minus "tauta" itself,
> which is the x pattern.  But the pattern itself is not a syntax object so
> requires the syntax quote "#'", at which point you can de-syntaxify it with
> syntax->datum, getting '(or (and P Q) etc.).  You can try this in the REPL,
> just do (syntax->datum #'(or (and P Q) etc.)).
>
> Once free vars has this as '(P Q), map this list by re-syntaxifying the
> symbols with datum->syntax.  The first parameter to datum->syntax basically
> is the key to "breaking" hygiene lisp-style.  We want to say that the free
> variable symbols in "x" are the *same* as in our new datum->syntaxified
> symbols that get passed to with-vars to bind in the for/and, so we say they
> ultimately belong to the same lexical context (your top level code) by
> passing the same syntax ("stx") that tauta was called in.  In other words,
> those generated vars are created as if you yourself defined them in the
> module.  Without passing stx to datum->syntax, it would be as if someone
> else defined them elsewhere but coincidentally with the same names, and for
> safety hygienic systems disallow this shadowing (their x and your x are more
> like x1 and x2, being secretly renamed by the system).  So we tell it we
> really mean our own code's context.  In general, you can break hygiene this
> way by using whichever syntax object refers to wherever you want to pretend
> the syntax came from.
>
> #lang racket
> (require (for-syntax racket))
>
> (define-syntax-rule (with-vars (vars ...) x)
>   (for*/and ([vars (in-list '(#t #f))]
>              ...)
>       x))
>
> (define-for-syntax (free-vars xs)
>   (define (keyword? x)
>     (member x '(and or then -> <-> not
>                     equiv display displayln)))
>   (remove-duplicates
>    (filter (compose not keyword?)
>            (flatten xs))))
>
> (define (then x y) (or y (not x)))
> (define (equiv x y) (and (then x y) (then y x)))
>
> (define-syntax (tauta stx)
>   (syntax-case stx ()
>     [(_ x)
>      (with-syntax ([(vars ...) (map (λ (var) (datum->syntax stx var))
>                                     (free-vars (syntax->datum #'x)))])
>        #'(with-vars (vars ...) x))]))
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>