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 <skana...@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
>
____________________
Racket Users list:
http://lists.racket-lang.org/users
