;;; File: "mendelsonpropositionaleasy.scm"
;;; Copyright (c) 2009 by Shaughan Lavine. All Rights Reserved.

;;; Called "easy" because this is just a naive implementation of Mendelson's
;;; definitions for teaching purposes, rather than an efficient logical system.
;;; For example, everything is a string. In Scheme, it would make much more sense
;;; to use lists, but that is not Mendelson's presentation, and for good reason:
;;; He isn't using Scheme or any other programming language.

;;;------------------------------------------------------------------------
;;;| This file, as supplied, WILL NOT WORK: the libraries are not provided.|
;;;| I'll supply a zipped version soon that has everything.                |
;;;------------------------------------------------------------------------

(include "include-gam.scm") ; Includes srfi1, srfi2, srfi13, srfi14
(namespace ("mendelson#"))
(##include "~~/lib/gambit#.scm") ; Gambit primitives added in their namespace
(include "include-gam#.scm") ; srfi1, srfi2, srfi13, srfi14 in their namespaces

;;;==========================================================================

;;; Constructors for propositional calculus

;; The obvious and natural constructors for propositional calulus
;; appear commented out immediately below. The slightly more
;; complicated ones actually used permit dropping parentheses,
;; which is useful for displaying formulas with parentheses
;; hidden according to Mendelson's conventions. They get used in
;; the Printing and Displaying section below.

;; (define (make-statement-letter let #!optional (num #f))
;;   (if (char-set-contains? char-set:upper-case char) ; test from srfi14
;;                                         ; used instead of
;;                                         ; char-upper-case?
;;                                         ; for non-ASCII
;;                                         ; character sets
;;       (cond ((not num)(string char))
;;             ((and (integer? num)
;;                   (exact? num)
;;                   (positive? num))
;;              (string-append (string char)
;;                             (number->string num)))
;;             (else #f))
;;       #f))

;; ;; '(string-join list delimiter 'suffix) makes a string out of a list of
;; ;; strings, putting delimiter after each.
;; (define (space-string-join lis) (string-join (map string-trim-both lis) " " 'suffix))

;; (define (make-negation statement-frm)
;;   (space-string-join (list "(" "-|" statement-frm ")")))

;; (define (make-binary-connective connective left-statement-frm right-statement-frm)
;;   (space-string-join (list "(" left-statement-frm connective right-statement-frm ")")))

;; (define (make-conjunction left-statement-frm right-statement-frm)
;;   (make-binary-connective "^" left-statement-frm right-statement-frm))

;; (define (make-disjunction left-statement-frm right-statement-frm)
;;   (make-binary-connective "v" left-statement-frm right-statement-frm))

;; (define (make-conditional left-statement-frm right-statement-frm)
;;   (make-binary-connective "=>" left-statement-frm right-statement-frm))

;; (define (make-biconditional left-statement-frm right-statement-frm)
;;   (make-binary-connective "<=>" left-statement-frm right-statement-frm))

(define (make-statement-letter let #!optional (num #f) (parens #t))
                                        ; parens is optional, defaults to #t.
                                        ; #t if parentheses are supplied normally
  (if (char-set-contains? char-set:upper-case char) ; test from srfi14
                                        ; used instead of
                                        ; char-upper-case?
                                        ; for non-ASCII
                                        ; character sets
      (cond ((not num)(string char))
            ((and (integer? num)
                  (exact? num)
                  (positive? num))
             (string-append (string char)
                            (number->string num)))
            (else #f))
      #f))

(define (maybe-parenthesize strin tst)
  (if tst
      (string-append "( " strin ") ")
      strin))

;; '(string-join list delimiter 'suffix) makes a string out of a list of
;; strings, putting delimiter after each.
(define (space-string-join lis) (string-join (map string-trim-both lis) " " 'suffix))

(define (make-negation statement-frm #!optional (parens #t))
  (maybe-parenthesize
   (space-string-join (list "-|" statement-frm))
   parens))

(define (make-binary-connective
         connective left-statement-frm right-statement-frm #!optional (parens #t))
  (maybe-parenthesize
   (space-string-join (list left-statement-frm connective right-statement-frm))
   parens))

(define (make-conjunction left-statement-frm right-statement-frm)
  (make-binary-connective "^" left-statement-frm right-statement-frm))

(define (make-disjunction left-statement-frm right-statement-frm)
  (make-binary-connective "v" left-statement-frm right-statement-frm))

(define (make-conditional left-statement-frm right-statement-frm)
  (make-binary-connective "=>" left-statement-frm right-statement-frm))

(define (make-biconditional left-statement-frm right-statement-frm)
  (make-binary-connective "<=>" left-statement-frm right-statement-frm))

;;; Parsers

(define (statement-letter strin)
  (and-let* ; srfi2 Like let*, but returns '#f if any of the values is '#f
   (((string? strin))(stri (string-trim-right strin))) ; Final space is optional
   (cond ((eqv? (string-length stri) 1)
          (let ((char (string-ref stri 0)))
            (if (char-set-contains? char-set:upper-case char) (list "statement letter" stri)  #f)))
         ((> (string-length stri) 1)
          (let ((char (string-ref stri 0))
                (num (string->number (substring/shared stri 1))))
            (if (and (char-set-contains? char-set:upper-case char)
                     (number? num)(positive? num) (exact? num))
                (list "statement letter" strin)
                #f)))
         (else #f))))

(define (statement-letter-letter strin)
  (string-ref strin 0))

(define (statement-letter-subscript strin)
  (if (> (string-length strin) 1)
      (string->number (substring/shared strin 1))
      #f))

(define (statement-letter-list-statement-letter lis)
  (second lis))

(define (negation strin)
  (if (and
       (string? strin)
       (>= (string-length strin) 8)
       (string-prefix? "( -| " strin)
       (string-suffix? ") " strin))
      (list "-|" (string-drop-right (string-drop strin 5) 2)) ; drop "( -| " on the left
                                        ; then ") " on the right.
      #f))

(define (mangle alist anindex afunc) ; 'receive is the macro of srfi8, though it is used in, e.g., srfi1,
                                        ; and so it is taken from there.
                                        ; 'mangle takes a list and an index and returns a length three list of
                                        ; the item at the index, afunc applied to the list of items before the index,
                                        ; and afunc applied to the list of items after the index.
  (receive (left-sentential-form-list rest) (split-at alist anindex)
    (receive (op right-sentential-form-list) (car+cdr rest)
      (list op (afunc left-sentential-form-list) (afunc right-sentential-form-list)))))

(define (match lis) ; If lis begins with "(", returns the index of the matching ")".
                                        ; Otherwise, returns 0.
  (let depth-indx ((dpth 0) (indx 0) (lis lis))
    (cond
     ((null? lis) #f)
     ((equal? "(" (first lis)) (depth-indx (+ dpth 1) (+ indx 1) (cdr lis)))
     ((equal? ")" (first lis)) (if (equal? dpth 1) indx
                                   (depth-indx (- dpth 1) (+ indx 1) (cdr lis))))
     (else (if (equal? dpth 0)
               0
               (depth-indx dpth (+ indx 1) (cdr lis)))))))

(define (binary-connective strin)
  (if (and
       (string? strin)
       (string-prefix? "( " strin)
       (not (string-prefix? "( -| " strin))
       (string-suffix? ") " strin))
                                        ; 'string-tokenize converts a string into the list of its
                                        ;  maximal substrings of nonwhitespace printing characters
      (let* ((lis (string-tokenize (string-drop-right (string-drop strin 2) 2))))
             (mangle lis (+ (match lis) 1) space-string-join))
      #f))

(define (binary-connective-is statement-form-strin connective-strin)
  (let ((reslt (binary-connective statement-form-strin)))
    (if (and reslt
             (equal? connective-strin (first reslt))) reslt
             #f)))

(define (conjunction strin) (binary-connective-is strin "^"))
(define (disjunction strin) (binary-connective-is strin "v"))
(define (conditional strin) (binary-connective-is strin "=>"))
(define (biconditional strin) (binary-connective-is strin "<=>"))

;;; Tests
;;; Only one is really needed: Given (statement-form strin),
;;; one can test for a conjunction, for example, with
;;; (and (conjunction strin) (statement-form strin)).
;;; More efficient tests are, in fact, provided below.

(define (nullary-operator strin) (cond ((member strin  '("statement letter")) => first)
                                       (else #f)))

(define (unary-operator strin) (cond ((member strin '("-|")) => first)
                                     (else #f)))

(define (binary-operator strin) (cond ((member strin '("^" "v" "=>" "<=>")) => first)
                                      (else #f)))

;; '(statement-letter strin) and '(negation strin) should be '(nullary-connective strin) and
;; '(unary-connective strin) but that isn't worth implementing while there is only one
;; connective of each kind.
(define (statement-form strin)
  (cond
   ((statement-letter strin) => (lambda (res) res))
   ((negation strin) =>
    (lambda (res)
      (and-let*
       ((negatd (statement-form (second res))))
       (list (first res) negatd))))
   ((binary-connective strin) =>
    (lambda (res)
      (and-let* ((op (binary-operator (first res)))
                 op ; Tests that op-rest isn't #f
                 (parsed-left-statement-frm (statement-form (second res)))
                 (parsed-right-statement-frm (statement-form (third res))))
                (list op parsed-left-statement-frm parsed-right-statement-frm))))
   (else #f)))

(define (statement-form-kind-list lis) (first lis))

(define (statement-form-kind strin) (and-let* ((parsd (statement-form strin))) (first parsd)))

(define (statement-letter-list lis) (equal? "statement letter"  (first lis)))

(define (nullary-statement-form-list lis) (nullary-operator (first lis)))

(define (negation-statement-form-list lis) (equal? "-|" (first lis)))

(define (unary-statement-form-list lis) (unary-operator (first lis)))

(define (conjunction-statement-form-list lis) (equal? "^" (first lis)))

(define (disjunction-statement-form-list lis) (equal? "v" (first lis)))

(define (conditional-statement-form-list lis) (equal? "=>" (first lis)))

(define (biconditional-statement-form-list lis) (equal? "<=>" (first lis)))

(define (binary-statement-form-list lis) (binary-operator (first lis)))

(define (statement-letter-list-statement-letter lis) (string-trim-right (second lis)))

(define (left-statement-form-list lis)
  (and (or
        (unary-statement-form-list lis)
        (binary-statement-form-list lis))
       (second lis)))

(define (right-statement-form-list lis)
  (and (binary-statement-form-list lis)
       (third lis)))

(define (statement-form-kind-is? strin kind) (equal? (statement-form-kind strin) kind))

;; The obvious definition for 'statement-letter? is what follows commented out,
;; but what follows that is more efficient.
;; (define (statement-letter? strin) (statement-form-kind-is? strin "statement letter"))
(define (statement-letter? strin) (statement-letter strin))

(define (negation? strin) (statement-form-kind-is? strin "-|"))

(define (conjunction? strin) (statement-form-kind-is? strin "^"))

(define (disjunction? strin) (statement-form-kind-is? strin "v"))

(define (conditional? strin) (statement-form-kind-is? strin "=>"))

(define (biconditional? strin) (statement-form-kind-is? strin "<=>"))

;;; Truth-functional semantics
;;; What we're doing here is weird from the point of view of programming:
;;; it would be much simpler and more efficient to use Schemes built-in
;;; logical operators. But Mendelson is doing everything from scratch, as
;;; did those who wrote Scheme, and so are we.

;; A few auxiliary functions:

(define (pair-statement-letter<? l1 l2)
  (if
   (and
    (statement-letter l1)
    (statement-letter l2))
   (let ((l1l (statement-letter-letter l1))
         (l2l (statement-letter-letter l2))
         (l1s (statement-letter-subscript l1))
         (l2s (statement-letter-subscript l2)))
     (or
      (char<? l1l l2l)
      (and
       (char=? l1l l2l)
       (or
        (and (not l1s) l2s)
        (and l2s (< l1s l2s))))))
   #f))

(define (statement-letter<? . strings)
  (cond
   ((null-list? strings) #t)
   ((and (statement-letter? (first strings))
         (null-list? (cdr strings))) #t)
   ((receive (firs rest)(car+cdr strings) ; A more efficient version of
                                        ; (let ((firs (first strings))(rest (cdr strings)))
      (and
       (pair-statement-letter<? firs (first rest))
       (apply statement-letter<? rest)))
    #t)
   (else #f)))

(define (uniq-sorted lis elt< #!optional (= equal?))
  (list-delete-neighbor-dups
   (list-merge-sort lis elt<) =))

;; It is assumed that lis is of the form (statement-form strin) and that lis
;; is not #f
(define (unsorted-statement-letters-of-list lis)
  (cond
   ((nullary-statement-form-list lis)
    (list (statement-letter-list-statement-letter lis)))
   ((unary-statement-form-list lis)
    (unsorted-statement-letters-of-list (left-statement-form-list lis)))
   ((binary-statement-form-list lis)
    (append (unsorted-statement-letters-of-list (left-statement-form-list lis))
            (unsorted-statement-letters-of-list (right-statement-form-list lis))))
   (else #f)))

(define (statement-letters-of-list lis)
  (uniq-sorted (unsorted-statement-letters-of-list lis) pair-statement-letter<?))

(define (statement-letters-of strin)
  (and-let* ((lis (statement-form strin)))
            (statement-letters-of-list lis)))

(define (apply-and lis) ; Needed because 'and is a macro
  (if (null-list? lis) #t
      (and (first lis) (apply-and (cdr lis)))))

(define (statement-letters-of-list-of-strings lis)
  (and-let* ((lis (map statement-form lis))((apply-and lis)))
            (uniq-sorted
             (append-map unsorted-statement-letters-of-list lis)
             pair-statement-letter<?)))

;; Our truth values will be 'T and 'F, not the built-in booleans #t and #f of scheme
;; Thus, "T" is a statement letter, but 'T is a truth value, eliminating Mendelson's ambiguity
(define (is-a-truth-value obj) (memq obj '(T F)))

(define (is-true? obj)(equal? obj 'T))

(define (lookup obj tabl)
  (cond ((assoc obj tabl) => second)
        (else #f)))

(define not-tt '((T F)
                 (F T)))

(define and-tt '(((T T) T)
                 ((F T) F)
                 ((T F) F)
                 ((F F) F)))

(define or-tt '(((T T) T)
                ((F T) T)
                ((T F) T)
                ((F F) F)))

(define if-tt '(((T T) T)
                ((F T) T)
                ((T F) F)
                ((F F) T)))

(define iff-tt '(((T T) T)
                 ((F T) F)
                 ((T F) F)
                 ((F F) T)))

;; A truth-list is a list of 'Ts and 'Fs

(define (truth-assign statement-letter-lis truth-value-lis)
  (zip  statement-letter-lis truth-value-lis))

(define (number->truth-value-list num lgth)
  (case lgth ((0) '())
        (else (cons (if (even? num) 'T 'F)
                    (number->truth-value-list (quotient num 2)(- lgth 1))))))

(define (list-all-truth-value-lists n)
  (map (lambda (num)(number->truth-value-list num n))(list-tabulate (expt 2 n) values)))

(define (compute-truth-value-list statement-form-lis truth-assig)
  (let
      ((ctvl (lambda (sfl) (compute-truth-value-list sfl truth-assig))))
                                        ; ctvl is merely to avoid repeating 'truth-assig over and over
    (cond
     ((statement-letter-list statement-form-lis)
      (lookup (statement-letter-list-statement-letter statement-form-lis) truth-assig))
     ((negation-statement-form-list statement-form-lis)
      (lookup
       (ctvl (left-statement-form-list statement-form-lis))
       not-tt))
     ((conjunction-statement-form-list statement-form-lis)
      (lookup
       (list
        (ctvl (left-statement-form-list statement-form-lis))
        (ctvl (right-statement-form-list statement-form-lis)))
       and-tt))
     ((disjunction-statement-form-list statement-form-lis)
      (lookup
       (list
        (ctvl (left-statement-form-list statement-form-lis))
        (ctvl (right-statement-form-list statement-form-lis)))
       or-tt))
     ((conditional-statement-form-list statement-form-lis)
      (lookup
       (list
        (ctvl (left-statement-form-list statement-form-lis))
        (ctvl (right-statement-form-list statement-form-lis)))
       if-tt))
     ((biconditional-statement-form-list statement-form-lis)
      (lookup
       (list
        (ctvl (left-statement-form-list statement-form-lis))
        (ctvl (right-statement-form-list statement-form-lis)))
       iff-tt)))))

(define (compute-truth-value statement-frm truth-assig)
  (and-let* ((sfl (statement-form statement-frm)))
            (compute-truth-value-list sfl truth-assig)))

(define (truth-assignments-for-statement-letter-list-map mapped-func statement-letter-lis)
  (let ((lengt (length statement-letter-lis)))
    (map mapped-func
         (list-tabulate (expt 2 lengt)
                        (lambda (num)
                          (truth-assign statement-letter-lis
                                        (number->truth-value-list num lengt)))))))

(define (truth-assignments-for-statement-form-list-map mapped-func statement-form-lis)
  (let* ((statement-letter-lis (statement-letters-of-list statement-form-lis)))
    (truth-assignments-for-statement-letter-list-map mapped-func statement-letter-lis)))

(define (truth-value-list-of-statement-form-list statement-form-lis)
  (truth-assignments-for-statement-form-list-map
   (lambda (truth-assig)
     (compute-truth-value-list statement-form-lis truth-assig))
   statement-form-lis))

(define (truth-value-list-of-statement-form statement-frm)
  (and-let* ((sfl (statement-form statement-frm)))
            (truth-value-list-of-statement-form-list sfl)))

(define (all-T? truth-value-lis)
  (null? (remove is-true? truth-value-lis)))

(define (tautology? statement-frm)
  (and-let* ((tt  (truth-value-list-of-statement-form statement-frm)))
            (all-T? tt)))

(define (tautological-consequence? statement-form-lis statement-frm)
  (and-let* ((statement-lets
              (statement-letters-of-list-of-strings
               (cons statement-frm statement-form-lis)))
             (lengt (length statement-lets)))
            (all-T?
             (map (lambda (truth-assig)
                    (compute-truth-value statement-frm truth-assig))
                  (filter
                   (lambda (truth-assig)
                     (all-T?
                      (map (lambda (sen-fun)
                             (compute-truth-value sen-fun truth-assig))
                           statement-form-lis)))
                   (list-tabulate (expt 2 lengt)
                                  (lambda (num)
                                    (truth-assign statement-lets
                                                  (number->truth-value-list num lengt)))))))))

(define (truth-table-of-statement-form statement-frm)
  (and-let* ((sfl (statement-form statement-frm)))
            (truth-assignments-for-statement-form-list-map
             (lambda (truth-assig)
               (list (map second truth-assig)
                     (compute-truth-value-list sfl truth-assig)))
             sfl)))

;;; Disjunctive normal form

(define (make-false-statement-form statement-let)
  (make-conjunction statement-let (make-negation statement-let)))

(define (binary-join statement-form-lis make-binary-connectiv)
  (if (null? (cdr statement-form-lis))
      (first statement-form-lis)
      (make-binary-connectiv
       (conjoin (drop-right statement-form-lis 1))
       (last statement-form-lis))))

(define (conjoin statement-form-lis)
  (binary-join statement-form-lis make-conjunction))

(define (disjoin statement-form-lis)
  (binary-join statement-form-lis make-disjunction))

(define (disjunctive-normal-form truth-tabl statement-letter-lis)
  (and-let* (((apply = (map length
                            (cons statement-letter-lis
                                  (map first truth-tabl)))))
             (filtered-truth-table-lins
              (filter-map (lambda (truth-table-lin)
                            (if (equal? 'T (second truth-table-lin))
                                (first truth-table-lin)
                                #f))
                          truth-tabl)))
            (if (null? filtered-truth-table-lins)
                (disjoin (map make-false-statement-form statement-letter-lis))
                (disjoin (map
                          (lambda (filtered-truth-table-lin)
                            (let ((truth-assig (truth-assign statement-letter-lis filtered-truth-table-lin)))
                              (conjoin
                               (map (lambda (statement-let)
                                      (cond ((equal? 'T (lookup statement-let truth-assig)) statement-let)
                                            ((equal? 'F (lookup statement-let truth-assig)) (make-negation statement-let))))
                                    statement-letter-lis))))
                          filtered-truth-table-lins)))))

(define (disjunctive-normal-form-of-statement-form statement-frm)
  (disjunctive-normal-form (truth-table-of-statement-form statement-frm)
                           (statement-letters-of statement-frm)))

(define (list-of-statement-letters int)
  (list-tabulate int
                 (lambda (n)
                   (make-statement-letter
                    (integer->char (+ 65 (remainder n 26)))
                                        ; The ASCII codes for A... are 65...
                    (let ((q (quotient n 26)))
                      (if (zero? q) #f q))))))

(define (disjunctive-normal-form-of-truth-table truth-tabl)
  (disjunctive-normal-form truth-tabl
                           (list-of-statement-letters (length (first (first truth-tabl))))))

;;; Printing and displaying

;;; Basic statement-form display

(define (process-strin strin beginnin endin mappin)
  (string-append
   beginnin
   (apply string-append (map mappin (string-tokenize strin)))
   endin))

(define tex-beginning "\\[")

(define tex-ending "\\]")

(define (tex-mapping obj)
  (cond
   ((integer? obj) (string-append "_{" (number->string obj) "}"))
   ((equal? "-|" obj) "\\lnot ")
   ((equal? "^" obj) "\\land ")
   ((equal? "v" obj) "\\lor ")
   ((equal? "=>" obj) "\\Rightarrow ")
   ((equal? "<=>" obj) "\\Leftrightarrow ")
   ((equal? 'T obj) "\\mathsf{T}")
   ((equal? 'F obj) "\\mathsf{F}")
   (else obj)))

(define (tex-display statement-frm)
  (begin
    (display (process-strin statement-frm tex-beginning tex-ending tex-mapping))
    (newline)))

(define twiki-beginning "%\\[")

(define twiki-ending "\\]%")

(define (twiki-mapping obj)
  (cond
   ((integer? obj) (string-append "_{" (number->string obj) "}"))
   ((equal? "-|" obj) "\\lnot ")
   ((equal? "^" obj) "\\land ")
   ((equal? "v" obj) "\\lor ")
   ((equal? "=>" obj) "\\Rightarrow ")
   ((equal? "<=>" obj) "\\Leftrightarrow ")
   ((equal? 'T obj) "\\mathsf{T}")
   ((equal? 'F obj) "\\mathsf{F}")
   (else obj)))

(define (twiki-display statement-frm)
  (begin
    (display (process-strin statement-frm twiki-beginning twiki-ending twiki-mapping))
    (newline)))

;; The utf8 display functions will only work properly if you have an appropriate font---one
;; that has the symbols---installed, and if your encoding is set to utf8. The font I use is
;; DejaVu Sans Mono.

(define utf-beginning "")

(define utf-ending "")

(define (utf-mapping obj)
  (cond
   ((integer? obj) (number->string obj))
   ((equal? "-|" obj) "¬")
   ((equal? "^" obj) "&#8743;")
   ((equal? "v" obj) "&#8744;")
   ((equal? "=>" obj) "&#8658;")
   ((equal? "<=>" obj) "&#8660;")
   ((equal? 'T obj) "T")
   ((equal? 'F obj) "F")
   (else obj)))

(define (utf-display statement-frm)
  (begin
    (display (process-strin statement-frm utf-beginning utf-ending utf-mapping))
    (newline)))

;;; Dropping parentheses according to precedence
;;; and associated display

(define (list<= lis . res)
  (if
   (or (null? res)
       (null? (cdr res)))
   #t
   (and (member (second res) (member (first res) lis))
        (list< lis (drop res 2)))))

(define (list< lis . res)
  (if
   (or (null? res)
       (null? (cdr res)))
   #t
   (and  (member (second res) (member (first res) lis))
         (not (equal? (second res) (first res)))
         (list<= lis (drop res 2)))))

(define statement-form-kind-order
  '("statement letter" "-|" "^" "v" "=>" "<=>"))

(define (statement-form-kind< . res)
  (apply list< statement-form-kind-order res))

(define (statement-form-kind<= . res)
  (apply list<= statement-form-kind-order  res))

(define (statement-form-list->statement-form statement-form-lis)
                                        ; This could have come much earlier, but it wasn't needed.
                                        ; The version here includes optional parentheses.
  (cond
   ((statement-letter-list statement-form-lis)
    (statement-letter-list-statement-letter statement-form-lis))
   ((negation-statement-form-list statement-form-lis)
    (make-negation
     (statement-form-list->statement-form
      (left-statement-form-list statement-form-lis))
     (last statement-form-lis))) ; parens
   ((binary-statement-form-list statement-form-lis)
    (make-binary-connective
     (statement-form-kind-list statement-form-lis)
     (statement-form-list->statement-form
      (left-statement-form-list statement-form-lis))
     (statement-form-list->statement-form
      (right-statement-form-list statement-form-lis))
     (last statement-form-lis))))) ; parens

(define (deparenthesize-list statement-form-lis)
  (let ((parens #f)) ; The outermost parentheses are dropped by setting parens to #f here.
                                        ; Value can't be #f in and-let*: that makes the and-let* take value #f.
    (let deparen ((statement-form-lis statement-form-lis)
                  (parens parens))
      (let ((main-connectiv (statement-form-kind-list statement-form-lis)))
        (cond
         ((statement-letter-list statement-form-lis)
          (append statement-form-lis (list parens)))
         ((negation-statement-form-list statement-form-lis)
          (list "-|"
                (deparen
                 (left-statement-form-list statement-form-lis)
                 (statement-form-kind<
                  main-connectiv
                  (statement-form-kind-list
                   (left-statement-form-list statement-form-lis))))
                                        ; If '(statement-form-kind< ... is #f,
                                        ; that turns off the parentheses in the make-* functions.
                parens))
         ((binary-statement-form-list statement-form-lis)
          (list main-connectiv
                (deparen
                 (left-statement-form-list statement-form-lis)
                 (statement-form-kind<
                  main-connectiv
                  (statement-form-kind-list
                   (left-statement-form-list statement-form-lis))))
                (deparen
                 (right-statement-form-list statement-form-lis)
                 (statement-form-kind<= ; <= on the right because we associate to the left
                  main-connectiv
                  (statement-form-kind-list
                   (right-statement-form-list statement-form-lis))))
                parens)))))))

(define (deparenthesize statement-frm)
  (statement-form-list->statement-form
   (deparenthesize-list (statement-form statement-frm))))

(define (tex-pretty-display statement-frm)
  (tex-display (deparenthesize statement-frm)))

(define (twiki-pretty-display statement-frm)
  (twiki-display (deparenthesize statement-frm)))

(define (utf-pretty-display statement-frm)
  (utf-display (deparenthesize statement-frm)))

;;; Display truth tables
;;; This is a pain because they are abbreviated truth tables

(define (tokenized-deparenthesized-statement-form->sub-statement-form-list-list statement-form-lis)
                                        ; Takes a statement form list and returns a
                                        ; list of statement form lists that maps
                                        ; each token of the tokenized list of the
                                        ; deparenthesized statement form to the
                                        ; statement form list with main connective
                                        ; at that position or #f
  (let ((paren-tkn (lambda (sfl) (if (last sfl) '(#f) '())))) ; #f if there are parens, nothing otherwise
    (let tdsf->ssfll ((lis (deparenthesize-list statement-form-lis)))
      (cond ; based on statement-form-list->statement-form statement-form-lis
       ((statement-letter-list lis) (list lis))
       ((negation-statement-form-list lis)
        (append
         (paren-tkn lis)
         (list lis)
         (tdsf->ssfll
          (left-statement-form-list lis))
         (paren-tkn lis)
         ))
       ((binary-statement-form-list lis)
        (append
         (paren-tkn lis)
         (tdsf->ssfll
          (left-statement-form-list lis))
         (list lis)
         (tdsf->ssfll
          (right-statement-form-list lis))
         (paren-tkn lis)
         ))))))

(define (abbreviated-truth-table-layout statement-frm)
  (let* ((sfl (statement-form statement-frm))
         (sfll
          (tokenized-deparenthesized-statement-form->sub-statement-form-list-list
           sfl)))
    (append
     (list (string-tokenize (deparenthesize statement-frm)))
     (truth-assignments-for-statement-form-list-map
      (lambda (truth-assig)
        (map (lambda (sfl)
               (if sfl
                   (compute-truth-value-list sfl truth-assig)
                   " ")) sfll))
      sfl))))

(define (truth-value-mapping obj)
  (cond
   ((eq? obj 'T) "T")
   ((eq? obj 'F) "F")
   (else " ")))

(define (display-abbreviated-truth-table statement-frm)
  (let* ((ttl (abbreviated-truth-table-layout statement-frm))
         (sft (first ttl))
         (space-lis
          (map
           (lambda (strin)
             (make-string ; string of spaces to fill in Ts and Fs
              (- (string-length strin) 1)
              #\space))
           sft)))
    (begin
      (display (string-append (string-concatenate sft) "\n"))
      (map
       (lambda (lin)
         (display
          (string-concatenate
           (append
            (map string-append space-lis
                 (map truth-value-mapping lin))
            '("\n")))))
       (cdr ttl)))) #!void)

(define (process-abbreviated-truth-table-list
         lis beginnin endin mappin col-sep start-form end-form
         #!optional (args #f) (first-col-sep col-sep) (last-col-sep col-sep))
  (string-append
   (beginnin args) "\n"
   (string-concatenate
    (map
     (lambda (rw)
       (string-append
        first-col-sep
        (string-join
         (map (lambda (entr) (string-append start-form entr end-form))
              (map mappin rw))
         col-sep)
        last-col-sep "\n"))
     lis))
   endin "\n"))

(define (tex-abbreviated-truth-table-beginning lngth)
  (string-append "\\begin{tabular}{|" (make-string lngth #\c) "|}\\hline"))

(define tex-abbreviated-truth-table-ending
  "\\hline\\end{tabular}\n")

(define tex-first-column-separator "")

(define tex-last-column-separator "\\\\")

(define tex-column-separator "&")

(define tex-start-formula "$")

(define tex-end-formula "$")

(define (tex-display-abbreviated-truth-table tabl)
  (display
   (process-abbreviated-truth-table-list
    tabl
    tex-abbreviated-truth-table-beginning
    tex-abbreviated-truth-table-ending
    tex-mapping
    tex-column-separator
    tex-start-formula
    tex-end-formula
    (length (first tabl))
    tex-first-column-separator
    tex-last-column-separator)))

(define (twiki-abbreviated-truth-table-beginning . unused)
  "%TABLE{databg=\"none\" tableframe=\"box\" tablerules=\"none\" }%")

(define twiki-abbreviated-truth-table-ending
  "\n")

(define twiki-column-separator "  |  ")

(define twiki-start-formula "%$")

(define twiki-end-formula "$%")

(define (twiki-display-abbreviated-truth-table tabl)
  (display
   (process-abbreviated-truth-table-list
    tabl
    twiki-abbreviated-truth-table-beginning
    twiki-abbreviated-truth-table-ending
    twiki-mapping
    twiki-column-separator
    twiki-start-formula
    twiki-end-formula)))

(define (utf-abbreviated-truth-table-beginning lngth) "")

(define utf-abbreviated-truth-table-ending
  "\n")

(define utf-column-separator "")

(define utf-start-formula "")

(define utf-end-formula "")

(define (utf-display-abbreviated-truth-table tabl)
  (display
   (process-abbreviated-truth-table-list
    tabl
    utf-abbreviated-truth-table-beginning
    utf-abbreviated-truth-table-ending
    utf-mapping
    utf-column-separator
    utf-start-formula
    utf-end-formula)))

(define (process-truth-function
         tabl beginnin endin mappin col-sep start-form end-form
         #!optional (args #f) (first-col-sep col-sep) (last-col-sep col-sep))
  (process-abbreviated-truth-table-list
   (map
    (lambda (rw) (append (first rw) (list (second rw))))
    tabl)
   beginnin endin mappin col-sep start-form end-form
   args first-col-sep last-col-sep))

(define (tex-truth-function-beginning lngth)
  (string-append "\\begin{tabular}{|" (make-string lngth #\c) "|c|}\\hline"))

(define (tex-display-truth-function tabl)
  (display
   (process-truth-function
    tabl
    tex-truth-function-beginning
    tex-abbreviated-truth-table-ending
    tex-mapping
    tex-column-separator
    tex-start-formula
    tex-end-formula
    (length (first (first tabl)))
    tex-first-column-separator
    tex-last-column-separator)))

(define (twiki-display-truth-function tabl)
  (display
   (process-truth-function
    tabl
    twiki-abbreviated-truth-table-beginning
    twiki-abbreviated-truth-table-ending
    twiki-mapping
    twiki-column-separator
    twiki-start-formula
    twiki-end-formula)))

(define (utf-display-truth-function tabl)
  (display
   (process-truth-function
    tabl
    utf-abbreviated-truth-table-beginning
    utf-abbreviated-truth-table-ending
    utf-mapping
    utf-column-separator
    utf-start-formula
    utf-end-formula)))

;;; Input functions: Take an input string of a deparenthesized statement form
;;; and convert it to a proper statement form, providing helpful error messages.
;;; Allow input of truth tables.

(define (get-string promp) ; 'read-line executes at the #\) and therefore
                                        ; reads the newline at the end of the command line.
                                        ; Use '(first-get get-string promp) for the first get-string.
  (display promp)
  (string-trim-both ; remove whitespace on the ends of the string
   (read-line)))

(define-macro (first-get get-comman promp) ; eats the newline at the end of the command
  `(begin
     (read-line)
     (,get-comman ,promp)))

(define (unsafe-get-symbol promp)
  (string->symbol
   (get-string promp)))

(define-macro (thunk fun)
  `(lambda () ,fun))

(define-macro (bound-global-symbol? symbl)
  `(if (symbol? ,symbl) ;test if symbl is a symbl
       (let* ((ceh (current-exception-handler)) ; copy the current exception handler
              (exception-handler ; define a new exception handler that returns #f
                                        ; instead of an error when an unbound-global-exception is raised
                                        ; and returns #t when there is a 'macro-used-as-variable exception,
                                        ; since the symbol is then bound to a macro
               (lambda (exc)
                 (cond ((unbound-global-exception? exc) #f)
                       ((and (expression-parsing-exception? exc)
                             (eq? (expression-parsing-exception-kind exc)
                                  'macro-used-as-variable)) #t)
                       (else (ceh exc))))))
         (with-exception-catcher
          exception-handler
          (thunk
           (let
               ((foo (eval ,symbl))) ;evaluate symbl to see if it is bound
             #t))))
       (error "*** ERROR IN bound-global-symbol?, not a symbol: " ,symbl)))

(define (get-symbol promp)
  (let ((symbl (first-get unsafe-get-symbol promp)))
    (let safe-symbl ((symbl symbl))
      (if (bound-global-symbol? symbl)
          (begin
            (let ((respons (get-string (string-append
                                        "*************\n"
                                        "Are you sure?\n"
                                        "'" (symbol->string symbl)
                                        " is already defined.\n"
                                        "Redefining some symbols can cause bad things\n"
                                        "to happen. If you are in doubt, respond no.\n\n"
                                        "Respond yes, no, q to quit, or <enter> for no.\n"
                                        "*************\n"
                                        "?? "))))
              (let chck ((respons respons))
                (cond
                 ((equal? respons "yes") symbl)
                 ((or (equal? respons "no") (equal? respons "")) (safe-symbl (unsafe-get-symbol promp)))
                 ((equal? respons "q") #f)
                 (else (chck (get-string "You must respond yes, no, <enter>, or q.\n?? ")))))))
          symbl))))

(define (statement-form-character? char)
  (or
   (char-set-contains? char-set:upper-case char)
   (char-set-contains? char-set:digit char)
   (member char '(#\( #\) #\space #\^ #\v #\- #\| #\< #\= #\>))))

(define (string->list-of-chars strin)
  (string-fold-right cons '() strin))

(define (string->statement-form-token-list strin)
                                        ; some basic sanity checks
  (and-let*
                                        ; strin is a string
   (((if (string? strin)
         #t
         (begin
           (display strin)
           (display " is not a string.\n")
           #f)))
                                        ; All characters are legal.
    ((apply-and (string-for-each (lambda (char)
                                   (if
                                    (statement-form-character? char)
                                    #t
                                    (begin
                                      (display char)
                                      (display " is not allowed in statement forms.\n")
                                      #f)))
                                 strin)))
                                        ; Parentheses are balanced.
    ((if (zero? (string-fold (lambda (char cnt)
                               (cond
                                ((eqv? char #\() (+ cnt 1))
                                ((eqv? char #\)) (- cnt 1))
                                (else cnt)))
                             0
                             strin))
         strin
         (begin
           (display "Unmatched parentheses.\n")
           #f))))
   (let tokeniz ((input-lis (string->list strin)) (output-lis '()))
     (cond
      ((null? input-lis) (reverse output-lis)) ; done
      ((eqv? (first input-lis) #\space) ; drop spaces
       (tokeniz (cdr input-lis) output-lis))
      ((memv (first input-lis) '(#\( #\) #\^ #\v)) ; one-character tokens
       (tokeniz (cdr input-lis) (cons (first input-lis) output-lis)))
      ((eqv? (first input-lis) #\-)
       (if (eqv? (second input-lis) #\|)
           (tokeniz (cddr input-lis) (cons "-|" output-lis))
           (begin
             (display "- must be followed by |.\n")
             #f)))
      ((eqv? (first input-lis) #\<)
       (if (and  (eqv? (second input-lis) #\=)  (eqv? (third input-lis) #\>))
           (tokeniz (cdddr input-lis) (cons "<=>" output-lis))
           (begin
             (display "< must be followed by =>\n")
             #f)))
      ((eqv? (first input-lis) #\=)
       (if (eqv? (second input-lis) #\>)
           (tokeniz (cddr input-lis) (cons "=>" output-lis))
           (begin
             (display "= must be followed by >\n")
             #f)))
      ((char-set-contains? char-set:upper-case (first input-lis))
       (receive (subscrip input-lis) (span (lambda (char) (char-set-contains? char-set:digit char)) (cdr input-lis))
         (tokeniz input-lis
                                        ; drop any numerical subscript from input-lis after removing the letter
                  (cons
                   (string-append (string (first input-lis))
                                  (apply string subscrip))
                   output-lis))))
      (else (display (list->string input-lis))
            (display " cannot end this statement form.\nDo you have a digit that is not part of a statement letter?\n")
            #f)))))

         ;;-- Main.ShaughanLavine - First posted version 10 Sep 2009 - Current version posted 7 Oct 2009
         ;;