; A predicate spec is a pair of a symbol and a non-negative int indicating its arity.
; A predicate list is a list of predicate-specs.
; ps is the predicate specs.
; fs is the function specs.
(define ps '((= . 2) (p . 0)))
(define fs '((* . 2)))
; Below, s is a putative well formed formula and
; fl is the list of allowed free variables therein.
(define (wff s fl) (let ((h (car s))
   (vn (lambda (n pl) (let y ((n n)(pl pl)) (if (zero? n) (null? pl)
      (and (pair? pl) (wff (car pl) fl) (y (- n 1)(cdr pl))))))))
(cond
  ((or (eq? 'and h) (eq? 'or h))
     (let alls ((k (cdr s))) (or (null? k) (and (wff (car k) fl) (alls (cdr k))))))
  ((eq? 'not h) (vn 1 (cdr s)))
  ((or (eq? 'implies h) (eq? 'iff h)) (vn 2 (cdr s)))
  ((or (eq? 'all h) (eq? 'is h))
     (let ((v (cadr s))) (and (symbol? v)
        '(not (let kw ((l '(and or not implies iff all is)))
        ; remove the quote sign above to disallow ids which are key words.
          (and (pair? l) (or (eq? v (car l)) (kw (cdr l))))))
        (wff (caddr s) (cons v fl))
        (null? (cdddr s)))))
  (#t (let isp ((p ps)) (and (pair? p) (or (and (eq? h (caar p))
        (let y ((tl (cdr s))(n (cdar p))) (if (zero? n) (null? tl)
           (and (pair? tl) (or 
           (and (pair? (car tl)) (let ((h (caar tl)))
           (let isf ((p fs)) (and (pair? p) (or
           (and (eq? h (caar p)) (y (cdar tl)(cdar p)))(isf (cdr p)))))))
        (let y ((sl fl)) (and (pair? sl)
              (or (eq? (car tl) (car sl)) (y (cdr sl))))))
           (y (cdr tl) (- n 1))))))
     (isp (cdr p)))))))))
   
; tests:

(map (lambda (x) (let ((v (wff x '(a b c)))) (display (list v x)) (newline) v)) '(
   (p)
   (= a b)
   (= 3 a) ; 3 isn't a valid ident
   (all and (p)) ; keyword as id illegal.
   (is x (= x c))
   (p b) ; too many operands
   (= a b c) ; too many operands
   (= b) ; too few operands
   (iff (p) (= a b))
   (iff (p)) ; too few phrases
   (implies (p) (p) (= c c)) ; too many phrases
   (not) ; too few phrases
   (and)
   (or (is x (= x c)) (p))
   (all a (all b (is x (= (* a x) b))))
   (all x (all y (all z (= (* (* x y) z) (* x (* y z))))))
   )) ; => (#t #t #f #t #t #f #f #f #t #f #f #f #t #t #t #t)