;;; $Id: negate-bexp-mod.scm,v 1.2 2006/01/04 07:00:55 leavens Exp $
;;; AUTHOR: Gary T. Leavens

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

(provide negate-bexp)

(require (lib "bexp-mod.scm" "lib342"))

(deftype negate-bexp (-> (bexp) bexp))
(define negate-bexp
  (lambda (be)
    (cond
      ((var-exp? be)
       (not-exp (var-exp (negate-varref (var-exp->varref be)))))
      ((and-exp? be)
        (or-exp (negate-bexp (and-exp->left be))
                (negate-bexp (and-exp->right be))))
      ((or-exp? be)
       (and-exp (negate-bexp (or-exp->left be))
                (negate-bexp (or-exp->right be))))
      (else ;; for the not-exp we take advantage of double negation
        (not-exp->arg be)))))

(deftype negate-varref (-> (varref) varref))
(define negate-varref
  (lambda (vr)
     vr))

) ;; end module