;;; =================================
;;;  CMPU-145, Spring 2013
;;;  Code from class
;;;  May 1, 2013
;;; =================================
;;;  Implementing data structures and functions for propositional logic.

(load "asmt-helper.txt")

(header "Code from class" "May 1")

(problem "Defining S-NOT and S-AND data structures")

;;;  Data structures:  S-NOT and S-AND
;;;    For representing NOT and AND sentences

(define-struct s-not (arg))
(define-struct s-and (lefty righty))

;;;  Once the above data structures are defined, we automatically
;;;  get the following functions:
;;;    CONSTRUCTORS  --  make-s-not, make-s-and
;;;    ACCESSORS     --  s-not-arg, s-and-lefty, s-and-righty
;;;    TYPE-CHECKERS --  s-not?, s-and?
;;;    SETTERS       --  we won't need them

(tester 'make-s-not)
(tester 'make-s-and)

;;;  Defining some abbreviations for the constructor functions

(define s-not make-s-not)
(define s-and make-s-and)

(tester 's-not)
(tester 's-and)

;;;  Defining some global variables whose values are symbols.
;;;  Allows us to avoid having to quote symbols!

(define a 'a)
(define b 'b)
(define c 'c)
(define d 'd)

;;;  A sample sentence:  (NOT A) AND (B AND (NOT C))

(tester '(s-and (s-not a)
                (s-and b (s-not c))))


(problem "Converting a sentence to a string")

;;; Convert a sentence into a string:  Let Scheme do it!

;;;  SENT->STRING
;;; ----------------------------
;;;  INPUT:  S, a sentence in prop logic (using symbols, s-not and s-and)
;;;  OUTPUT:  A string representation of that sentence

(define sent->string
  (lambda (s)
    (cond
      ;; Base Case:  S is a propositional letter
      ((symbol? s)
       (symbol->string s))
      ;; Recursive Case 1:  S is a NOT sentence
      ((s-not? s)
       (string-append "NOT{"
                      (sent->string (s-not-arg s))
                      "}"))
      ;; Recursive Case 2:  S is an AND sentence
      ((s-and? s)
       (string-append "("
                      (sent->string (s-and-lefty s))
                      ") AND ("
                      (sent->string (s-and-righty s))
                      ")"))
      ;; Default Case:  Other???
      (#t
       "$"))))

(tester '(sent->string a))
(tester '(sent->string (s-not a)))
(tester '(sent->string (s-and a b)))
(tester '(sent->string (s-and (s-not a)
                              (s-and b
                                     (s-not c)))))

(problem "Computing the truth value of a sentence")

;;;  Given an interpretation of the propositional letters,
;;;  INTERP computes the truth value of any sentence!
;;;  Note that we use TRUE-LETTERS to represent a basic interpretation function.

;;;  INTERP
;;; --------------------------------------
;;;  INPUTS:  S, a sentence in prop logic (using symbols, s-not and s-and)
;;;           TRUE-LETTERS, a list of the prop letters that are interpreted
;;;             as TRUE
;;;  OUTPUT:  The truth value of S according to the semantic rules of
;;;           prop logic and TRUE-LETTERS

(define interp
  (lambda (s true-letters)
    (cond
      ;; Base Case: S is a prop letter
      ((symbol? s)
       ;; If S appears in TRUE-LETTERS, then it's interpreted as TRUE
       (if (member s true-letters) #t #f))
      ;; Rec Case:  S is a NOT sentence
      ((s-not? s)
       ;; Use Scheme's NOT function to flip the truth value of
       ;; the recursive function call
       (not (interp (s-not-arg s) true-letters)))
      ;; Rec Case:  S is an AND sentence
      ((s-and? s)
       ;; Use Scheme's AND special form to return #t iff
       ;; both recursive function calls return #t
       (and (interp (s-and-lefty s) true-letters)
            (interp (s-and-righty s) true-letters)))
      ;; Default:
      (#t
       (printf "Uh oh~%")
       #t))))

(tester '(interp (s-and (s-not a)
                        (s-and b (s-not c)))
                 '(a b)))
(tester '(interp (s-and (s-not a)
                        (s-and b (s-not c)))
                 '(b)))