[racket] Macros baffle me

In general, I don't have problems with macros in Common Lisp or in Scheme.
However, macros in Racket baffle me. I simply cannot figure out how
syntax->datum, syntax->list and datum->syntax work. In any case, I need a
macro to prove that a proposition is a tautology. Below you will find what
I did. There are a few examples on how to run the program. What bothers me
in this program is the need of calling ev on a quoted version of the fm wff:

(define (ev xs)
  (eval `(with-vars ,(free-vars xs) ,xs)))

(define-syntax-rule (tauta fm) (ev 'fm))

I suppose that one can avoid calling eval by a judicious use of
syntax->datum, syntax->list and datum->syntax. I would appreciate
suggestions to improve the program.



#lang racket

;; (with-vars (P Q ) (or Q (or (not P) P))) builds:
;;   (for/and [(P (in-list (list #t #f)))] (for/and [(Q (in-list (list #t
#f)))] (or Q (or (not P) P))))
(define-syntax with-vars
  (syntax-rules ()
    ((with-vars (v) cm) (for/and [(v (in-list (list #t #f)))] cm))
    ((with-vars (w v ...) cm)
     (for/and [(w (in-list (list #t #f)))] (with-vars (v ...) cm))) ))

;; flattens a list; for instance, (or (not P) Q) becomes (or not P Q)
(define (flatten lst)
  (cond ((null? lst) '())
        ((pair? (car lst)) (append (flatten (car lst)) (flatten (cdr lst))))
        (else
          (cons (car lst) (flatten (cdr lst))))))

;; gets the variables in a wff. For instance (free-vars ' (or Q (or (not P)
P)))
;; produces (P Q)
(define (free-vars s)
  (let loop [(x (flatten s))]
    (cond [(null? x) x]
          [(member (car x) '(and or then -> <-> not
                                 equiv display displayln)) (loop (cdr x))]
          [(member (car x) (cdr x)) (loop (cdr x))]
          [else (cons (car x) (loop (cdr x)))] )))

(define (then x y) (or y (not x)))

(define (equiv x y) (and (then x y) (then y x)))

;; I want to avoid this step. (ev '(or Q (or (not P) P)))) gets the list
;; (P Q) of free variables, builds and evals (with-vars (P Q) (or Q (or
(not P) P))).
(define (ev xs)
  (eval `(with-vars ,(free-vars xs) ,xs)))

(define-syntax-rule (tauta fm) (ev 'fm))

; (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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140501/9b29eae0/attachment.html>