;;; -*- scheme -*-
;;; Problem Set 3:  An Introduction to Propositional Calculus

#|

well-formedness

A formula is either
  1. a variable
  2. a list of
    a. the symbol 'not and a variable
    b. the symbol 'or and 2 variables
    c. the symbol 'and and 2 variables
    d. the symbol 'implies and 2 variables
  3. 'true or 'false

|#

;;; a variable is just a symbol
(define variable? symbol?)

;;; a formula is just a list
(define formula? list?)
;;; the operator of a formula is just the first element
(define op first)
;;; the terms of the formula are the rest of the list
(define terms rest)

;;; return #t if the given operator is a binary operator
(define (nary-op? x)
  (case (op x)
    ((and or implies) #t)
    (else #f)))

;;; return true if the operator of formula x is negation.
(define (unary-op? x)
  (eq? (op x) 'not))

;;; return #f if a given object is not in the given list, true
;;; otherwise.
(define already-on-list member)

;;; add the given object to the given list, unless it is in the list
;;; already.
(define (add-to-list-maybe obj l)
  (if (already-on-list obj l)
    l
    (cons obj l)))

;;;function returns an empty variable assignment
(define (empty-var-assignment) empty)

;;; add variables v with value val to the boolean assignment rho
(define (extend v val rho)
  (cons (list v val) rho))

;;; return the value assigned to v in the given boolean assignment
(define (var-value v rho)
  (let ((var-binding (assoc v rho)))
    (if var-binding
      (second var-binding)
      'undefined)))

;;; return true if variable v is bound to value in boolean assignment bv
(define (var-assigned? v rho)
  (not (eq? (var-value v rho) 'undefined)))

;;; convert an assignment into a list of lists of variables and values
(define (assignment->list/pairs rho) rho)


;;; a signed formula is just a list of a formula and a truth value
(define make-signed-form list)
;;; the formula is the first part
(define signed-form-form first)
;;; and the truth value is the second part
(define signed-form-tv second)

;;; alpha-type? returns #t if the given term with the given truth value
;;; is an alpha term
(define (alpha-type? term tv)
  (or (variable? term)
      (case (op term)
        ((not) #t)
        ((and) tv)
        ((or implies) (not tv))
        (else #f))))

;;; given a binary operation term and a signature signed-terms returns a
;;; list of signed formulas that represent the operand terms of the
;;; given term.
(define (signed-terms term tv)
  (case (op term)
    ((and) (list (make-signed-form (first (terms term)) tv)
                 (make-signed-form (second (terms term)) tv)))
    ((or)  (list (make-signed-form (first (terms term)) tv)
                 (make-signed-form (second (terms term)) tv)))
    ((implies) (list (make-signed-form (first (terms term)) (not tv))
                     (make-signed-form (second (terms term)) tv)))))

;;; return #t if the given formula is a tautology, or a falsifying
;;; assignment otherwise
(define (tautology? x)
  (let ((falsifying-assignment (satisfy (list 'not x))))
    (or falsifying-assignment #t)))