;;; $Id: bexp-mod.scm,v 1.3 2006/02/14 03:25:56 leavens Exp $
;;;
;;; <bexp> ::=
;;;       <varref>              "var-exp (varref)"
;;;     | (and <bexp> <bexp>)   "and-exp (left right)"
;;;     | (or <bexp> <bexp>)    "or-exp (left right)"
;;;     | (not <bexp>)          "not-exp (arg)"
;;; <varref> ::=
;;;       P                     "P ()"
;;;     | Q                     "Q ()"

(module bexp-mod (lib "typedscm.ss" "typedscm")

(provide bexp? varref? var-exp? and-exp? or-exp? not-exp? P? Q?
        var-exp and-exp or-exp not-exp P Q
        var-exp->varref and-exp->left and-exp->right
        or-exp->left or-exp->right not-exp->arg
        parse-bexp parse-varref)

;; type predicate
(deftype bexp? (type-predicate-for bexp))
(deftype varref? (type-predicate-for varref))

;; case testers (discriminators)
(deftype var-exp? (-> (bexp) boolean))
(deftype and-exp? (-> (bexp) boolean))
(deftype or-exp? (-> (bexp) boolean))
(deftype not-exp? (-> (bexp) boolean))
(deftype P? (-> (varref) boolean))
(deftype Q? (-> (varref) boolean))

;; constructors
(deftype var-exp (-> (varref) bexp))
(deftype and-exp (-> (bexp bexp) bexp))
(deftype or-exp (-> (bexp bexp) bexp))
(deftype not-exp (-> (bexp) bexp))
(deftype P (-> () varref))
(deftype Q (-> () varref))

;; observers 
(deftype var-exp->varref (-> (bexp) varref))
(deftype and-exp->left (-> (bexp) bexp))
(deftype and-exp->right (-> (bexp) bexp))
(deftype or-exp->left (-> (bexp) bexp))
(deftype or-exp->right (-> (bexp) bexp))
(deftype not-exp->arg (-> (bexp) bexp))

;; parsing/bless input correctness
(deftype parse-bexp (-> (datum) bexp))
(deftype parse-varref (-> (datum) varref))

(defrep (bexp (list-of datum)) (varref symbol))

(define bexp?
  (lambda (d)
    (has-type-trusted
      boolean
      (or (and (var-exp? d) (varref? (cadr d)))
          (and (and-exp? d) (bexp? (cadr d)) (bexp? (caddr d)))
          (and (or-exp? d) (bexp? (cadr d)) (bexp? (caddr d)))
          (and (not-exp? d) (bexp? (cadr d)))))))

(define varref?
  (lambda (d)
    (or (eq? d 'P) (eq? d 'Q)
        ;; DrScheme can be case sensitive
        (eq? d 'p) (eq? d 'q))))

;; (note: var-exps are represented internally using lists.
;; If you only use the helpers in this file, this shouldn't bother you. :-)
(define var-exp?
  (lambda (be)
    (and (list? be) (= (length be) 2)
         (eq? (car be) 'var-exp))))

(define and-exp?
  (lambda (be)
    (and (list? be) (= (length be) 3)
         (eq? (car be) 'and-exp))))

(define or-exp?
  (lambda (be)
    (and (list? be) (= (length be) 3)
         (eq? (car be) 'or-exp))))

(define not-exp?
  (lambda (be)
    (and (list? be) (= (length be) 2)
         (eq? (car be) 'not-exp))))

(define var-exp
  (lambda (vr)
    (if (varref? vr)
        (list (has-type datum 'var-exp) vr)
        (error "invalid varref:" vr))))

(define and-exp
  (lambda (left right)
    (list 'and-exp left right)))

(define or-exp
  (lambda (left right)
    (list 'or-exp left right)))

(define not-exp
  (lambda (be)
    (list 'not-exp be)))


(define P?
  (lambda (vr)
    (or (eq? vr 'P) (eq? vr 'p))))

(define Q?
  (lambda (vr)
    (or (eq? vr 'Q) (eq? vr 'q))))

(define P
  (lambda ()
    'p))

(define Q
  (lambda ()
    'q))

(deftype extract-maker (-> ((-> (bexp) boolean) string)
                           (-> (bexp) (list-of datum))))
(define extract-maker
  (lambda (test? name)
    (lambda (x)
      (if (test? x)
          x
          (error (string-append
                  "expecting a(n) "
                  name
                  " bexp, but given:")
                 x)))))

(define var-exp->varref
  (lambda (be)
    (test-type
      symbol?
      (cadr ((extract-maker var-exp? "var-exp") be)))))

(define and-exp->left 
  (lambda (be)
    (test-type
      (list-of datum?)
      (cadr ((extract-maker and-exp? "and-exp") be)))))

(define and-exp->right 
  (lambda (be)
    (test-type
      (list-of datum?)
      (caddr ((extract-maker and-exp? "and-exp") be)))))

(define or-exp->left 
  (lambda (be)
    (test-type
      (list-of datum?)
      (cadr ((extract-maker or-exp? "or-exp") be)))))

(define or-exp->right 
  (lambda (be)
    (test-type
      (list-of datum?)
      (caddr ((extract-maker or-exp? "or-exp") be)))))

(define not-exp->arg
  (lambda (be)
    (test-type
      (list-of datum?)
      (cadr ((extract-maker not-exp? "not-exp") be)))))

(define parse-bexp
  (lambda (d)
    (test-type
      (list-of datum?)
      (cond
       ((symbol? d)
        (var-exp (parse-varref d)))
       ((and (list? d) (= (length d) 3) (eq? 'and (car d)))
        (and-exp (parse-bexp (cadr d)) (parse-bexp (caddr d))))
       ((and (list? d) (= (length d) 3) (eq? 'or (car d)))
        (or-exp (parse-bexp (cadr d)) (parse-bexp (caddr d))))
       ((and (list? d) (= (length d) 2) (eq? 'not (car d)))
        (not-exp (parse-bexp (cadr d))))
       (else (error "parse-bexp: bad syntax:" d))))))

(define parse-varref
  (lambda (d)
    (cond
      ;; avoid case sensitivity problems in DrScheme :-(
     ((or (eq? d 'P) (eq? d 'p)) (P))
     ((or (eq? d 'Q) (eq? d 'q)) (Q))
     (else (error "parse-varref: bad syntax:" d)))))

) ;; end module