#lang racket
; CSE 3302 Lab 2 Spring 2013 - just the simple version of generating assignments (only true lists)

(define (first x) (car x))

(define (second x) (car (cdr x)))

; Tests for a name, rather than a list or boolean operator
(define (name? x)
  (and (not (pair? x))
       (not (null? x)) 
       (not (number? x))
       (not (eq? x 'N))
       (not (eq? x 'A))
       (not (eq? x 'O))
       (char? x)))

; Tests for legal simple expression
(define (exp? x)
  (cond
    ((name? x) #t)
    ((not (pair? x)) #f)
    ((eq? (first x) 'N) (and (exp? (second x))
                             (null? (cdr (cdr x)))))
    ((eq? (first x) 'O) (expList? (cdr x)))
    ((eq? (first x) 'A) (expList? (cdr x)))
    (else #f)))

; Tests arguments to boolean operators O and A
; Should not be called from top level
(define (expList? x)
  (cond
    ((not (pair? x)) #f)
    ((exp? (car x)) (or (null? (cdr x))
                        (expList? (cdr x))))
    (else #f)))

; tests membership in ordered list of chars
(define (member? x l)
  (cond
    ((null? l) #f)
    ((char=? x (car l)) #t)
    ((char<? x (car l)) #f)
    (else (member? x (cdr l)))))

; inserts new member into ordered list of chars
(define (insert x l)
  (cond
    ((null? l) (cons x '()))
    ((char=? x (car l)) l)
    ((char<? x (car l)) (cons x l))
    (else (cons (car l) (insert x (cdr l))))))

; Collects all names in an expression into ordered list of chars
(define (collectR exp l)
  (cond
    ((name? exp) (insert exp l))
    ((eq? (first exp) 'N) (collectR (second exp) l))
    ((eq? (first exp) 'O) (collectList (cdr exp) l))
    ((eq? (first exp) 'A) (collectList (cdr exp) l))
    (else (error "bad case" exp))))

(define (collect exp) ; Interface to other code
  (collectR exp '()))

(define (collectList expList l) ; Collects propositions from a list of expressions
  (cond
    ((null? expList) l)
    (else (collectR (car expList) (collectList (cdr expList) l)))))

; Evaluates expression using list of true propositions
(define (boolEval exp list)
  (define (notEval exp)
    (not (boolEvalR exp)))
  (define (orEval exp)
    (cond
      ((null? exp) #f)
      (else (or (boolEvalR (car exp))
                (orEval (cdr exp))))))
  (define (andEval exp)
    (cond
      ((null? exp) #T)
      (else (and (boolEvalR (car exp))
                 (andEval (cdr exp))))))
  (define (boolEvalR exp)
    (cond
      ((name? exp) (member? exp list))
      ((eq? (first exp) 'N) (notEval (second exp)))
      ((eq? (first exp) 'O) (orEval (cdr exp)))
      ((eq? (first exp) 'A) (andEval (cdr exp)))
      (else (error "bad case" exp))))
  (boolEvalR exp))

; Simple way of generating (and evaluating all assignments - 
; similar to hand generation of truth table column-by-column
(define (treeEvaluate exp props)
  (define (treeEvaluateR unmapped trueList)
    (cond
      ((null? unmapped)
       (begin
         (display " true: ")
         (display trueList)
         (display " evaluates to ")
         (displayln (boolEval exp trueList))
         1))
      (else (+ (treeEvaluateR (cdr unmapped) (cons (car unmapped) trueList))
               (treeEvaluateR (cdr unmapped) trueList)))))
  (treeEvaluateR (reverse props) '()))

(define (process exp)
  (if (exp? exp)
      (begin
        (display "generating for: ")
        (displayln exp)
        (let ((props (collect exp)))
          (display "collected props: ")
          (displayln props)
          (treeEvaluate exp props)))
      (begin
        (display exp)
        (displayln " is malformed"))))

; Tautologies:

(process '(O #\a (N #\a)))

(process '(O (A #\a #\b (N #\a) (N #\b)) (N (A #\a #\b (N #\a) (N #\b)))))

(process '(O #\p (O (N #\p) #\q) (O (N #\q) #\r) (O (N #\r) #\s) (N #\s) #\s))

(process '(O (N (O (N #\p) #\q)) (O #\q (N #\p))))

(process '(O (N #\a) (O (N #\b) #\a)))

(process '(O (N (A #\a #\b)) #\a))

(process '(O (N #\a) (O #\a #\b)))

(process '(O (N (O (N #\a) #\b)) (O (N (O (N #\a) (O (N #\b) #\c))) (O (N #\a) #\c))))


; Satisfiable:

(process '(O #\a #\b))

(process '(A #\a #\b #\c (N #\a) (N #\b) (N #\c)))

(process '(N (O (A #\a #\b (N #\a) (N #\b)) (N (A #\a #\b (N #\a) (N #\b))))))

(process '(A (O #\p #\q) (O (N #\q) #\r) (O (N #\p) #\r) (N #\r)))

(process '(A #\p (O (N #\p) #\q) (O (N #\q) #\r) (O (N #\r) #\s) (N #\s) #\s))

(process '(O (N (A (O #\p #\q) (O #\r #\s))) (A (O #\r #\q) (O #\r #\s))))

(process #\r)