;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;
;;;; LogicLab 0.1.x
;;;;
;;;; (C) Copyright 2024-2025 Stephen M. Watt.  All rights reserved.
;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Table of Contents:
;; * General utilities
;; * List utilities
;; * Lists as sets
;; * Logical formula data type
;; * Predicates
;; * Ordering
;; * Valuations
;; * Truth valuations
;; * Higher-level operations on formulas
;; * Single rules    (apply to top-level only)
;; * Transformations (apply deeply)
;; * Terms
;; * Prime implicants and minimal DNF
;; * Logical formulas with selextion
;; * Parsing
;; * Formatting
;; * Truth tables
;; * Formal deduction axioms
;; * Formal deduction
;; * Random formulas
;;
;; * Testing utilities
;; * Tests
;;
;; * Stuff to do after tests
;;
;; Comment conventions:
;;   ^;;;; <text>   File header
;;   ^;;;+ <text>   Section header
;;   ^;;; <text>    Comment for a group of related definitions
;;   ^;; <text>     Comment for a single definition or details of section

(define *LogicLab-version* "0.1.1")
(printf "~nLogicLab Version ~a~n~n" *LogicLab-version*)

;; These control the tests run at the end of the file.

(define *do-specific-tests?*    #f)
(define *do-random-tests?*      #f)
(define *do-tests-with-output?* #f)

; TODO quantifiers
; TODO subscripted variables
; TODO lift quantifiers
; TODO skolemize
; TODO dual
; TODO make n-ary equiv into xnor
; TODO apply entailment rule to sub-part


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ General utilities
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;
;;; Debugging
;;;
(define *do-debug* #f)
(define (debug . args) (when *do-debug* (apply printf args)))
(define (dblook msg val) (when *do-debug* (printf "~a ~a~n" msg val)) val)
(define-syntax dbecho
  (syntax-rules ()
    ((_ msg expr)
        (begin (printf "~a~n" msg)
               (pretty-print 'expr) (newline)
               (pretty-print expr) (newline))) ))

;;;
;;; Fluid fluid binding
;;;
;;; E.g. (with-global (*lfws-verbose* #f) expr)
(define-syntax with-global
  (syntax-rules ()
    ((_ (var new-val) expr)
     (let ([old-val var] [tmp '()])
         (set! var new-val)
         (set! tmp expr)
         (set! var old-val)
         tmp)) ))

(define-syntax fn-with-global
  (syntax-rules ()
    ((_ (var new-val) fn)
     (lambda args (with-global (var new-val) (apply fn args))) )))
;;;
;;; Printing
;;;
(define (pretty-println msg v)
   (display msg) (pretty-display v) (newline) )

(define (display-strings ls) (for ([s ls]) (displayln s)))

(define (format-nary-with-prefix prefix args)
  (let ([fmt (apply string-append (cons prefix (for/list ([t args]) " ~a")))])
    (apply format (cons fmt args))))

;;;
;;; Error handling
;;;
;; Funnel all errors through here.

(define (error! . args) (error (format-nary-with-prefix "Error:" args)))
(define (bug!   . args) (error (format-nary-with-prefix "Bug:"   args)))
(define warning printf)

;;;
;;; Functional operators
;;;
(define (identity-fn x) x )
(define (compose f1 f2) (lambda args (f1 (apply f2 args))))

;;;
;;; Frequent compositions
;;;
(define (non-null? a)  (not (null? a)))
(define (<> a b)       (not (= a b)))
(define (neq? a b)     (not (eq? a b)))
(define (nequal? a b)  (not (equal? a b)))
(define (eq-car?  v a) (and (pair? v) (eq? (car v) a)))
(define (eq-caar? v a) (and (pair? v) (pair? (car v)) (eq? (caar v) a)))
(define (car-else l a) (if  (pair? l) (car l) a))

;; Give a for loop range like (in-range origin limit) but reversed.
(define (reverse-range origin limit) (in-range (- limit 1) (- origin 1) -1))

;; Character operations
(define (char-alphanumeric? c) (or (char-alphabetic? c) (char-numeric? c)))

;;;
;;; Membership related
;;;

;; Return the position of first value in list ell that is equal to v according
;; to test feq.  If there is no such element, return -1.
(define (find-position v ell feq)
  (define (inner ell ix)
    (cond
      [(null? ell) -1]
      [(feq v (car ell)) ix]
      [else (inner (cdr ell) (+ 1 ix))]) )
  (inner ell 0) )

(define (member? a l)
  (ormap (lambda (e) (equal? a e)) l))

(define (vector-member? a v) 
  (let ([found #f])
    (do ([i 0 (+ 1 i)])
       [(or found (= i (vector-length v))) found]
       (when (equal? (vector-ref v i) a) (set! found #t)) )))

;; Like assq, but returns cdr or default value if not found.
(define (lookq obj alist default)
  (let ((v (assq obj alist))) (if (pair? v) (cdr v) default)) )

;;;
;;; Efficient list length tests
;;;
(define (list-length=? ell n)
  (if (= n 0)
    (null? ell)
    (and (pair? ell) (list-length=? (cdr ell) (- n 1))) ) )

(define (list-length>? ell n)
  (cond
    [(null? ell) (< n 0)]
    [(= n 0)     #t]
    [else (list-length>? (cdr ell) (- n 1))] ))

(define (list-length<? ell n)
  (cond
    [(null? ell) (> n 0)]
    [(<= n 0)    #f]
    [else (list-length<? (cdr ell) (- n 1))] ))

(define (list-length>=? ell n) (not (list-length<? ell n)))
(define (list-length<=? ell n) (not (list-length>? ell n)))

; Racket has builtin
;  (string<? (symbol->string a) (symbol->string b)) )

;;; Other
(define (bool->zero-one b) (if b 1 0))
(define (vector->string v) (build-string (vector-length v)(curry vector-ref v)))

;; (0 1 .. n-1)
(define (ints-upto n)
  (define (to n tail) (if (= n 0) (cons 0 tail) (to (- n 1) (cons n tail))))
  (if (or (not (integer? n)) (<= n 0)) '() (to (- n 1) '())))

;; Count elements in list satisfying a property.
(define (list-count pred ell)
  (let ([n 0]) (for ([e ell]) (when (pred e) (set! n (+ n 1)))) n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ List utilities
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Prepend a new list onto tail with the elements of ell separated by sep.
;; Examples:
;;   (prepend-with-seps 9 '(1 2 3) '())     -> '(1 9 2 9 3)
;;   (prepend-with-seps 9 '(1 2 3) '(x y))  -> '(1 9 2 9 3 x y)
(define (prepend-with-seps sep ell tail)
  (define (cons-with-seps rell tail)
    (if (null? rell)
      tail
      (cons-with-seps (cdr rell) (cons (car rell) (cons sep tail))) ))
  (cond
    [(null? ell)        tail]
    [(null? (cdr ell)) (cons (car ell) tail)]
    [else
      (let ([r (reverse ell)])
        (cons-with-seps (cdr r) (cons (car r) tail)) )] ))

;; Select the subset of ell given by the bits in n,
;; Example:  (select-combination 11 '(a0 a1 a2 a3))  -> '(a0 a1 a3)

(define (select-combination n ell)
  (do ([n n (quotient n 2)] [ell ell (cdr ell)] [combo '()])
     [(or (= n 0) (null? ell)) (reverse combo)]
     (when (= (remainder n 2) 1) (set! combo (cons (car ell) combo))) ))


;; Return a list containing the span elements of ell starting at start-ix.
;; Example:  (sub-list 2 3 '(a b c d e f g)) gives '(c d e).

(define (sub-list start-ix span ell)
    (take (drop ell start-ix) span))

;; Create a new list with the n-th element replaced by x
(define (list-replace ell n x)
  (when (null? ell) (error! "List too short in list-replace"))
  (if (= n 0)
    (cons x (cdr ell))
    (cons (car ell) (list-replace (cdr ell) (- n 1) x))))

;; Replace the span elements of ell starting at start-ix with new-val.
;; Example:  (sub-list-subs 2 3 '(a b c d e f g) 'x) gives '(a b x f g).

(define (sub-list-subs start-ix span ell new-val)
    (append (take ell start-ix) (list new-val) (drop ell (+ start-ix span))))

;; Copy input list skipping element i.  E.g. '(a b c) 1 -> '(a c)
(define (list-without-ref ell i)
  (define (l-wo-r ell i reversed-prefix)
    (cond
      [(null? ell) (error! "list-without-ref index error")]
      [(= i 0) (append (reverse reversed-prefix) (cdr ell))]
      [else (l-wo-r (cdr ell) (- i 1) (cons (car ell) reversed-prefix))]))
  (l-wo-r ell i '()))

;;
;; Return a list of all permutations of n elements from ell, each with
;; the remaining elements in the original order.
;; E.g. (permutations '(a b c))
;;      -> '((a b c) (a c b) (b a c) (b c a) (c a b) (c b a))
;;      (permutations '(a b c d) 2)
;;      -> '((a b  c d) (a c  b d) (a d  b c) (b a  c d) (b c  a d) (b d  a c)
;;           (c a  b d) (c b  a d) (c d  a b) (d a  b c) (d b  a c) (d c  a b))
(define (permutations ell [n (length ell)]) 
  (define (perms l n)
    (if (or (= n 0) (null? l))
      (list l)
      (apply append
        (for/list ([i (length l)])
          (map (lambda (p) (cons (list-ref l i) p))
               (perms (list-without-ref l i) (- n 1)) ))) ))
  (perms ell n))

;; Make a new list, given a list of indices. '(a b c) '(2 1) --> '(c b)
(define (list-multi-ref ell index-list) (map (curry list-ref ell) index-list))


;; Produce a list of all combinations from a list of lists.
;;  '((a1 a2) (b1) (c1 c2 c3)) -->
;;  '((a1 b1 c1) (a1 b1 c2) (a1 b1 c3) (a2 b1 c1) (a2 b1 c2) (a2 b1 c3))
(define (all-combos lol)
  (if (null? lol)
    '(())
    (apply append
      (for/list ([a (car lol)]) (map (curry cons a) (all-combos (cdr lol)))) )))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Lists as sets
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (lset-union1 e lset) (if (member? e lset) lset (cons e lset)))

(define (lset-empty) '())
(define (lset->list a) a)

(define (list->lset ell)
  (let ([r '()])
    (for ([e ell]) (set! r (lset-union1 e r)))
    (reverse r) ) )

(define (lset-union . args)
  (define (u2 a b) (let ([r a])
    (for ([e b]) (set! r (lset-union1 e r)))
    r ) )
  (if (null? args) '() (foldl u2 (reverse (car args)) (cdr args))) )
(define (lset-intersect . args)
  (define (i2 a b) (let ([r '()])
    (for ([e b]) (when (member? e a) (set! r (lset-union1 e r))))
    r ) )
  (if (null? args) '() (foldl i2 (car args) (cdr args)) ) )
(define (lset-minus whole remove)
  (let ([r '()])
    (for ([e whole]) (unless (member? e remove) (set! r (lset-union1 e r))))
    (reverse r) ) )

(define (lset-empty? a)
  (null? a) )
(define (lset-size a)
  (length a) )
(define (lset-subset? small big)
  (andmap (lambda (e) (member? e big)) small) )
(define (lset-equal? a b)
  (and (subset a b) (subset b a)) )

(define (lset->vector ls) (list->vector (lset->list ls)))
(define (vector->lset v)  (list->lset (vector->list v)))

;;
;; find-minimal-cover finds a minimal subset of 'choices' to cover the target.
;; The result is not necessarily unique.   
;; If no set covers, then the empty set is returned.
;;
;; The arguments are:
;; target:     a list of elements.
;; choices:    as a list of pairs, each pair having a label as its
;;               car and a list of elements for the choice as its cdr.
;; preference: either 'long or 'short, which gives a tie-breaker
;;               if two cover elements both satisfy the requirements.
;;
;; Example:
;; (find-minimal-cover '(6 7 8) '((A 3 6) (B 4 5 6 7) (C 7 8 9) (D 8)) pref)
;; will return '((B 4 5 6 7) (C 7 8 9))  if pref is 'long
;; or          '((B 4 5 6 7) (D 8))      if pref is 'short
;;
(define (find-minimal-cover target choices preference)
    (let ([npos (expt 2 (length choices))]
          [adequate-combos '()]
          [combo-len (lambda (c) (apply + (map length c)))])
      (do ([i 0 (+ 1 i)]) 
          [(= i npos)]
        (let* ([combo (select-combination i choices)]
               [vals  (apply lset-union (map cdr combo))])
            (when (null? (lset-minus target vals))
              (set! adequate-combos (cons combo adequate-combos)) ) ))
      ; If no combinations were adquate return the empty set.
      (if (null? adequate-combos)
        '()
        ; Otherwise select the combos with fewest parts.
        (let* ([min-length (apply min (map length adequate-combos))])
            (set! adequate-combos (filter 
              (lambda (ell) (= min-length (length ell)))
              adequate-combos))
            ; Now select a combo with longest or shortest total size as desired.
            (let* ([lengths (map combo-len adequate-combos)]
                   [keep-len (apply (if (eq? preference 'short) min max)
                                    lengths)])
              (car (filter (lambda (c) (= keep-len (combo-len c)))
                           adequate-combos)) ) ) ) ) )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Logical formula type
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;
;;; General formation functions.
;;;
(define (lf-formula op . args)  (lf-apply op args))
(define (lf-apply op args)      (cons op args))

;;;
;;; Specific formation functions
;;;
(define (lf-true)               #t)
(define (lf-false)              #f)
(define (lf-const c)            c)

(define (lf-sym a)              a)
(define (lf-not a)              (lf-formula 'not   a))
(define (lf-impl  a b)          (lf-formula 'impl  a b))
(define (lf-equiv a b)          (lf-formula 'equiv a b))

;; N-ary 
(define (lf-and  . args)        (lf-apply   'and   args))
(define (lf-or   . args)        (lf-apply   'or    args))
(define (lf-nand . args)        (lf-apply   'nand  args)) ; Not associative!
(define (lf-nor  . args)        (lf-apply   'nor   args)) ; Not associative!
(define (lf-xor  . args)        (lf-apply   'xor   args))
(define (lf-xnor . args)        (lf-apply   'xnor  args))

(define (lf-forall x a)         (lf-formula (list 'forall x) a))
(define (lf-exists x a)         (lf-formula (list 'exists x) a))

;; Conversion between S-expressions and logical formulae.
(define (sexpr->lf e)  e)
(define (lf->sexpr lf) lf)

;;;
;;; Part extraction functions
;;;
(define (lf-op F)        (car   F)) ; E.g. 'and, '(forall x)
(define (lf-bound-var F) (cadar F)) ; only for forall or exists
(define (lf-op-sym F)                ; E.g. 'and, 'forall
  (cond
    [(not  (pair? F))         'none]
    [(memq (car F) '(and or not impl equiv nand nor xor xnor))
                              (car F)]
    [(lf-quantified? (car F)) (caar F)]
    [else                     'none] ) )

(define (lf-args F)       (if (pair? F) (cdr F) '()) )
(define (lf-nargs F)      (if (pair? F) (length (cdr F)) 0) )
(define (lf-arg F n)      (list-ref (cdr F) n))
(define (lf-first-arg F)  (cadr  F))
(define (lf-second-arg F) (caddr F))


;; Sub-formula at given path.  E.g. (lf-xarg '(and (or a b) c) '(0 2)) is b
(define (lf-xarg F path)
    (if (null? path) F (lf-xarg (lf-arg F (car path)) (cdr path))) )

;; Sub-formula at given path, collecting n siblings.
;; The siblings' parent's connective is used for the collection if span <> 1.
(define (lf-xarg-span F path span)
   (cond
      ;; Top-level
      [(null? path)
        (when (<> span 1) (error! "lf-xarg-span: bad span " span))
        F]

      ;; Interior node -- don't use span yet.
      [(list-length>? path 1)
        (lf-xarg-span (lf-arg F (car path)) (cdr path) span)]

      ;; At containing node.  Group span using containing node op.
      [else
        (lf-apply (lf-op F) (sub-list (car path) span (lf-args F)))] ))

;; Replacing argument of a formula
(define (lf-arg-subs F n G)
  (lf-apply (lf-op F) (list-replace (lf-args F) n G)))

;; Replacing part of a formula at a path
(define (lf-xarg-subs F path G)
  (if (null? path)
    G
    (let ([n (car path)] [tail (cdr path)])
      (lf-arg-subs F n (lf-xarg-subs (lf-arg F n) tail G))) ))

;; Replacing a span n siblings at a given path
(define (lf-xarg-span-subs F path span G)
   (cond
      ;; Top-level
      [(null? path)
        (when (<> span 1) (error! "lf-xarg-span-subs: bad span " span))
        G]

      ;; Interior node -- don't use span yet.
      [(list-length>? path 1)
        (let ([n (car path)])
          (lf-arg-subs F n (lf-xarg-span-subs (lf-arg F n) (cdr path) span G)))]

      ;; At containing node.  Group span using containing node op.
      [else
        (lf-apply (lf-op F) (sub-list-subs (car path) span (lf-args F) G)) ] ))

;;
;; Maps corresponding to the above
;;
(define (lf-arg-map F n fn)
  (lf-arg-subs F n (fn (lf-arg F n))))

(define (lf-xarg-map F path fn)
  (lf-xarg-subs F path (fn (lf-xarg F path))))

(define (lf-xarg-span-map F path span fn)
  (lf-xarg-span-subs F path span (fn (lf-xarg-span F path span))))

;; Parts satisfying a predicate. Satisfying parts aren't descended.
(define (lf-parts-satisfying pred F)
  (define (ok-parts f)
    (cond
      [(pred f)  (list f)]
      [(lf-atom? f) '()]
      [else (foldl lset-union '() (map ok-parts (lf-args f)))] ))
  (ok-parts F) )

(define (lf-atoms F)        (lf-parts-satisfying lf-atom? F))
(define (lf-prop-symbols F) (lf-parts-satisfying lf-prop-symbol? F))

;;
;; Dual operator: (and a b) --> or, ((forall x) A) --> (exists x), etc
;;
(define (lf-op-dual F)
  (let ([sym (lf-op-sym F)])
    (cond
      [(eq? sym 'and)   'or]
      [(eq? sym 'or)    'and]
      [(eq? sym 'not)   'not]
      [(eq? sym 'nand)  'nor]
      [(eq? sym 'nor)   'nand]
      [(eq? sym 'xor)   'xnor]
      [(eq? sym 'xnor)  'xor]
      [(eq? sym 'forall) (list 'exists (lf-bound-var F))]
      [(eq? sym 'exists) (list 'forall (lf-bound-var F))]
      [else (error! "No dual for operator ~a." sym)] ) ) )

;;;
;;; Operator properties
;;;
(define (lf-op-identity op-sym)
  (cond
    [(eq? op-sym 'and)  #t]
    [(eq? op-sym 'or)   #f]
    [(eq? op-sym 'xor)  #f]
    [(eq? op-sym 'xnor) #t]
    [else (error! "Operator ~a has no identity element." op-sym)] ) )

(define (lf-op-simplified-nullary op-sym)
  (cond
    [(eq? op-sym 'and)  #t]
    [(eq? op-sym 'or)   #f]
    [(eq? op-sym 'nand) #f]
    [(eq? op-sym 'nor)  #t]
    [(eq? op-sym 'xor)  #f]
    [(eq? op-sym 'xnor) #t]
    [else (error! "Operator ~a cannot be nullary." op-sym)] ) )

(define (lf-op-simplified-unary op-sym arg)
  (cond
    [(eq? op-sym 'not)  (lf-not arg)]
    [(eq? op-sym 'and)  arg]
    [(eq? op-sym 'or)   arg]
    [(eq? op-sym 'nand) (lf-not arg)]
    [(eq? op-sym 'nor)  (lf-not arg)]
    [(eq? op-sym 'xor)  arg]
    [(eq? op-sym 'xnor) (lf-not arg)]
    [else (error! "Operator ~a cannot be unary." op-sym)] ) )

;;;
;;; Error checking
;;;

(define (lf-check! F)
  (unless (lf-formula? F)  (error! "Bad formula ~a." F)))
(define (lf-check-nargs! F)
 (unless (lf-nargs-ok? F) (error! "Bad formula ~a." F)))
(define (lf-require! msg pred F)
 (unless (pred F) (error! "Bad formula ~a." F)))

(define (lf-nargs-ok? F)
  (let ([op (lf-op-sym F)] [args (lf-args F)])
    (cond
      [(lf-is-associative? F)         #t] ; Assoc lf ops all have identities.
      [(memq op '(not forall exists)) (list-length=? args 1)]
      [(memq op '(impl equiv))        (list-length=? args 2)]
      [else #f] ) ) )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Predicates
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (lf-const? F)       (boolean? F))
(define (lf-prop-symbol? F) (symbol? F))
(define (lf-atom? F)        (or (symbol? F) (boolean? F))) ;; TODO for now
(define (lf-op?  F op)      (equal? (car F) op))

(define (lf-not? F)         (eq-car?  F 'not))
(define (lf-and? F)         (eq-car?  F 'and))
(define (lf-or?  F)         (eq-car?  F 'or))
(define (lf-impl?  F)       (eq-car?  F 'impl))
(define (lf-equiv? F)       (eq-car?  F 'equiv))
(define (lf-nand?  F)       (eq-car?  F 'nand))
(define (lf-nor?   F)       (eq-car?  F 'nor))
(define (lf-xor?   F)       (eq-car?  F 'xor))
(define (lf-xnor?  F)       (eq-car?  F 'xnor))
(define (lf-forall? F)      (eq-caar? F 'forall))
(define (lf-exists? F)      (eq-caar? F 'exists))

;; Is it a form with the given connective?
(define (lf-op-sym? sym F) (eq? sym (lf-op-sym F)))

;; Is it an atom or negation of an atom?
(define (lf-literal? F)
  (or (lf-atom? F)
  (and (lf-not? F) (lf-atom? (lf-first-arg F))) ) )

;; Is formula a simple or indexed symbol?
(define (lf-var? F) (or (symbol? F) (eq-car? F 'var)))

;; Check for (forall var) or (exists var)
(define (lf-quantified? F)
   (and (list-length=? F 2)
        (memq (car F) '(forall exists))
        (lf-var? (cadr F)) ) )

(define (lf-proposition? F)
  (or
    (lf-const? F)
    (lf-prop-symbol? F)
    (and
      (not (lf-forall? F))
      (not (lf-exists? F))
      (andmap lf-proposition? (lf-args F)) )) )     

(define (lf-formula? F)
  (cond
    [(lf-const? F)                          #t]
    [(lf-var? F)                            #t]
    [(not (pair? F))                        #f]
    [(not (andmap lf-formula? (lf-args F))) #f]
    [else                                   (lf-nargs-ok? F)] ) )

;; E.g. dual of 'and is 'or.
(define (lf-has-dual? F)
  (memq (lf-op-sym F) '(and or not nand nor forall exists)) )

;;; Associativity and commutativity
(define (lf-is-associative? F) (lf-is-associative-op? (lf-op-sym F)))
(define (lf-is-commutative? F) (lf-is-commutative-op? (lf-op-sym F)))

(define (lf-is-associative-op? op)
  (pair? (memq op '(and or xor xnor))) )
(define (lf-is-commutative-op? op)
  (pair? (memq op '(and or nand nor xor xnor))) )

(define (lf-has-complementary-args? F)
  (if (or (lf-atom? F) (< (lf-nargs F) 2))
    #f
    (let ([args (lf-args F)])
      (ormap
        (lambda (lf) (and (lf-not? lf) (member? (lf-first-arg lf) args)))
        args) )))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Ordering
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (lf-atom<? a b) 
  (cond
    [(and (lf-const? a) (lf-const? b))   (and (not a) b)] ; #f < #t
    [(lf-const? a) #t]
    [(lf-const? b) #f]
    [else (symbol<? a b)]) )

(define (lf-op-sym<? sym-a sym-b) (symbol<? sym-a sym-b))

;; Return -1, 0, 1 according as <, =, >.
;;
;; TODO implement lf<? in terms of lf-cmp, not lf-cmp in terms of lf<?
(define (lf-cmp a b) (cond [(lf<? a b) -1] [(lf<? b a) 1] [else 0]))

(define (lf<? a b) 
  (cond
    [(and (lf-atom? a)  (lf-atom? b))  (lf-atom<? a b)]
    [(lf-atom? a)  #t]
    [(lf-atom? b)  #f]
    [else 
      ; Both have connectives
      (let ([sym-a   (lf-op-sym a)] [sym-b   (lf-op-sym b)]
            [nargs-a (lf-nargs  a)] [nargs-b (lf-nargs  b)])
        (cond
          [(lf-op-sym<? sym-a sym-b) #t]
          [(lf-op-sym<? sym-b sym-a) #f]
          [(< nargs-a nargs-b) #t]
          [(< nargs-b nargs-a) #f]
          [else
            ; Same connective and same number of arguments
            (do ([lt? 'unset]
                 [a-args (lf-args a) (cdr a-args)]
                 [b-args (lf-args b) (cdr b-args)])
                [(or (null? a-args) (not (eq? lt? 'unset)))
                 ; Note a-args and b-args have same length so if a-args is null
                 ; all corresponding args are equal, then a not < b.
                 (if (not (eq? lt? 'unset)) lt? #f) ]

                (let ([ai (car a-args)] [bi (car b-args)])
                  (cond
                    [(lf<? ai bi) (set! lt? #t)]
                    [(lf<? bi ai) (set! lt? #f)] ) ) )
          ] ) ) ] ) )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Valuations
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;
;;; Truth valuations
;;;
(define (tv-make alist) alist)
(define (tv-extend tv sym-val-pair)  (cons sym-val-pair tv))
(define (tv-lookup tv sym not-found) (lookq sym tv not-found))

(define tv-not not)
(define (tv-impl  a b)  (if a b #t))
(define (tv-equiv a b)  (eq? a b))
(define (tv-and . args)
  (if (null? args) #t (and (car args) (apply tv-and (cdr args)))) )
(define (tv-or . args)
  (if (null? args) #f (or  (car args) (apply tv-or  (cdr args)))) )
(define (tv-xor  . args)
  (if (null? args) #f (xor (car args) (apply tv-xor (cdr args)))) )
(define (tv-nand . args) (not (apply tv-and args)))
(define (tv-nor  . args) (not (apply tv-or  args)))
(define (tv-xnor . args) (not (apply tv-xor args)))

(define tv-ops (tv-make (list
   (cons 'not   tv-not)  (cons 'impl  tv-impl) (cons 'equiv tv-equiv)
   (cons 'and   tv-and)  (cons 'or    tv-or)   (cons 'xor   tv-xor)
   (cons 'nand  tv-nand) (cons 'nor   tv-nor)  (cons 'xnor  tv-xnor)
)))

(define (tv-apply tv F)
  (unless (lf-proposition? F)
    (error! "Truth valuation of non-proposition ~a." F))
  (define (tv-apply-inner F)
    (cond
      [(lf-const? F) F]
      [(lf-atom? F)
        (let ([v (tv-lookup tv F 'not-found)])
          (when (eq? v 'not-found) (error! "No truth value for symbol ~a." F))
          v ) ]
      [else 
        (let ([v (tv-lookup  tv-ops (lf-op F) 'not-found)])
          (when (eq? v 'not-found) (error! "No truth value for operator ~a." F))
          (apply v (map tv-apply-inner (lf-args F))) )]) )
  (tv-apply-inner F) )

;;
;; Make a list of all truth valuations for a set of propositional symbols.
;;
(define (tv-all-valuations sym-list)
  ;; Build from the right to give nice order.
  ;; Don't care about stack size since sym-list must be short.
  (define (extend-all tv-list sym-val-pair)
    (if (null? tv-list)
      '()
      (cons (tv-extend  (car tv-list) sym-val-pair)
            (extend-all (cdr tv-list) sym-val-pair) )) )

  (define (all-inner sym-list tv-list)
    (if (null? sym-list)
      tv-list
      (let ([rec-list (all-inner (cdr sym-list) tv-list)])
        (append (extend-all rec-list (cons (car sym-list) #f))
                (extend-all rec-list (cons (car sym-list) #t)) )) ))
  (all-inner sym-list (list (tv-make '()))) )

;;
;; Find all truth valuations under which two formulas differ.
;;
(define (lf-find-tv-differences F G)
  (unless (lf-proposition? F) (error! "Formula ~a is not a proposition." F))
  (unless (lf-proposition? G) (error! "Formula ~a is not a proposition." G))
  (let* ([sym-list (lset-union (lf-atoms F) (lf-atoms G))]
         [tv-list  (tv-all-valuations sym-list)]
         [differing-list '()])
    (for ([tv tv-list])
        (unless (eq? (tv-apply tv F) (tv-apply tv G))
           (set! differing-list (cons tv differing-list)) ))
    differing-list ))

;;
;; Simple function to determine whether propositions are equivalent.
;; Could quit after first difference.
(define (lf-are-propositions-equivalent? F G)
  (null? (lf-find-tv-differences F G)) )
     
     
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Higher-level operations on formulas
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   
;;;
;;; Argument lists of n-ary connectives for which (op arg) = arg
;;;
(define (lf-op-args op-pred F)  (if (op-pred F) (lf-args F) (list F)))
(define (lf-disjuncts F) (lf-op-args lf-or?  F))
(define (lf-conjuncts F) (lf-op-args lf-and? F))

;;;
;;; DNF and CNF
;;;

;; Check whether F is of the form (op1 (op2 leaf ...) ...)
;; If `explicit?` then op1 and op2 must be explicit.

(define (lf-op-op-general? op1-pred op2-pred leaf-pred F explicit?) 
  (and 
    (or (op1-pred F) (not explicit?))
    (andmap
      (lambda (op1-arg)
        (and
          (or (op2-pred F) (not explicit?))
          (andmap leaf-pred  (lf-op-args op2-pred op1-arg)) ) )
      (lf-op-args op1-pred F) ) ) )

(define (lf-dnf-general? F explicit?)
  (lf-op-op-general? lf-or?  lf-and? lf-literal? F explicit?))

(define (lf-cnf-general? F explicit?)
  (lf-op-op-general? lf-and? lf-or?  lf-literal? F explicit?))

(define (lf-dnf? F)        (lf-dnf-general? F #f))
(define (lf-cnf? F)        (lf-cnf-general? F #f))

(define (lf-dnf-strict? F) (lf-dnf-general? F #t))
(define (lf-cnf-strict? F) (lf-cnf-general? F #t))

(define (lf-simplify-and/or F)
  (define (remove-consts ell)
    ; Preserve order by not tail calling.
    (cond
      [(null? ell) '()]
      [(eq-car? ell #t) (remove-consts (cdr ell))]
      [(eq-car? ell #f) (remove-consts (cdr ell))]
      [else (cons (car ell) (remove-consts (cdr ell)))] ))

  (let ([newF (lf-push-nots-down F)])
    (if (or (lf-atom? newF) (lf-not?  newF))
      newF
      (let* ([op         (lf-op newF)]
             [argl       (map lf-simplify-and/or (lf-args F))]
             [argl-undup (sort (lset->list (list->lset argl)) lf<?)]
             [has-compl  (lf-has-complementary-args? (lf-apply op argl-undup))]
             [has-false  (member? #f argl-undup)]
             [has-true   (member? #t argl-undup)]
             [argl-new   (remove-consts argl-undup)]
             [is-nullary (null? argl-new)]
             [is-unary   (list-length=? argl-new 1)])
        (cond
          [(eq? op 'not)
            (cond
              [has-false #t]
              [has-true  #f]
              [(lf-not? (car argl)) (lf-first-arg (car argl))]
              [else (lf-apply op argl-new)])]
          [(eq? op 'and)
            (cond
              [(or has-compl has-false) #f]
              [is-nullary #t]
              [is-unary (car argl-new)]
              [else (lf-apply op argl-new)])]
          [(eq? op 'or)
            (cond
              [(or has-compl has-true) #t]
              [is-nullary #f]
              [is-unary (car argl-new)]
              [else (lf-apply op argl-new)])]
          [(eq? op 'nand)
            (cond
              [(or has-compl has-false) #t]
              [is-nullary #f]
              [is-unary (lf-not (car argl-new))]
              [else (lf-apply op argl-new)])]
          [(eq? op 'nor)
            (cond
              [(or has-compl has-true) #f]
              [is-nullary #t]
              [is-unary (lf-not (car argl-new))]
              [else (lf-formula op argl-new)])]
          [else
             (lf-apply op argl)] )) )))
;;;
;;; map, etc
;;;
(define (lf-map fn F)
  (if (lf-atom? F) (fn F) (lf-apply (lf-op F) (map fn (lf-args F)))) )

;; Apply a function at all levels of a logical formula.
;; E.g.  (lf-tree-map f '(and (or a b) c)) gives
;;       [f (and [f (or [f a] [f b])] [f c])]
(define (lf-tree-map fn F)
  (if (lf-atom? F)
    (fn F)
    (fn (lf-apply (lf-op F)
                  (map (lambda (a) (lf-tree-map fn a)) (lf-args F)))) ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Single rules (apply to the top-level only)
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; A --> A
(define (lf-rule-do-nothing A) A)

;; (not (not A)) --> A
(define (lf-rule-not-not F)
  (lf-require! "Need (not (not A))" lf-not? F)
  (lf-require! "Need (not (not A))" lf-not? (lf-first-arg F))
  (lf-first-arg (lf-first-arg F)) )

;; (impl A B) --> (or (not A) B)
(define (lf-rule-elim-impl F)
  (lf-require! "Need impl." lf-impl? F)
  (lf-or (lf-not (lf-first-arg F)) (lf-second-arg F)) )

;; (equiv A B) --> (or (and A B) (and (not A) (not B)))
(define (lf-rule-elim-equiv F)
  (lf-require! "Need equiv." lf-equiv? F)
  (let ([A (lf-first-arg F)] [B (lf-second-arg F)])
    (lf-or (lf-and A B) (lf-and (lf-not A) (lf-not B))) ) )

;; (xor A B) --> (or (and A (not B)) (and (not A) B))
(define (lf-rule-elim-xor-inner ell)
  (cond
    [(null? ell)       (lf-or)]
    [(null? (cdr ell)) (car ell)]
    [else
      (let ([xor-rest (lf-rule-elim-xor-inner (cdr ell))])
        (lf-or (lf-and (car ell) (lf-not xor-rest))
               (lf-and (lf-not (car ell)) xor-rest) ))]))

(define (lf-rule-elim-xor F)
  (lf-require! "Need xor." lf-xor? F)
  (lf-rule-elim-xor-inner (lf-args F)) )

;; (nand A B) --> (not (and A B))
(define (lf-rule-elim-nand F)
  (lf-require! "Need nand." lf-nand? F)
  (lf-not (apply lf-and (lf-args F))) )

;; (nor A B) --> (not (or A B))
(define (lf-rule-elim-nor F)
  (lf-require! "Need nor." lf-nor? F)
  (lf-not (apply lf-or (lf-args F))) )

;; (xnor A B) --> (not (xor A B))
(define (lf-rule-elim-xnor F)
  (lf-require! "Need xnor." lf-xnor? F)
  (lf-not (lf-rule-elim-xor-inner (lf-args F))) )

;; Demorgan down:
;;
;; (not (or  A1 ...))   --> (and  (not A1) ...)
;; (not (and A1 ...))   --> (or   (not A1) ...)
;; (not (nor A1 ...))   --> (nand (not A1) ...)
;; (not (nand A1 ...))  --> (nor  (not A1) ...)
;; (not ((exists x) A1) --> ((forall x) (not A1))
;; (not ((forall x) A1) --> ((exists x) (not A1))
(define (lf-rule-demorgan-down F)
  (lf-require! "Bad DeMorgan." lf-not? F)
  (let ([A (lf-first-arg F)])
    (lf-require! "Bad DeMorgan" lf-has-dual? A)
    (lf-apply (lf-op-dual A) (map lf-not (lf-args A))) ))

;; Combine n-ary connectives:
;;
;; (or (or a b) (or (or c d) (and e (or f g))) --> (or a b c d (and e (or g h)))
;;
;; sym is one of 'and  'or 'equiv.
(define (lf-rule-assoc-nary sym F)
  (cond
    [(not (memq sym '(and or xor equiv))) F]
    [(nequal? sym (lf-op-sym F))  F]
    [else
      (let ([op (lf-op F)] [rev-out '()])
        (for ([ai (lf-args F)])
          (set! rev-out (append
            (if (lf-op-sym? op ai)
              (reverse (lf-args (lf-rule-assoc-nary sym ai)))
              (list ai) )
            rev-out )) )
        (lf-apply op (reverse rev-out)) ) ] ) )

;; Modify n-ary connective to be left/right associative of binary connectives.
;; (or a b c d) --> (or (or (or a b) c) d) for left associative
;; (or a b c d) --> (or a (or b (or c d))) for right associative
;; (or a)       --> a
;; (or)         --> (or)
(define (lf-rule-assoc-sided sym F arg-prep binop) ; arg-l arg-r)
  (cond
    [(not (memq sym '(and or xor equiv))) F]
    [(nequal? sym (lf-op-sym F))  F]
    [else
      (let ([args (lf-args F)])
        (if (null? args)
          F
          (let ([args (arg-prep args)])
            (foldl binop (car args) (cdr args)) ) ) ) ] ) )

(define (lf-rule-assoc-left sym F)
  (lf-rule-assoc-sided sym F identity-fn (lambda (a b) (lf-formula sym b a))) )

(define (lf-rule-assoc-right sym F)
  (lf-rule-assoc-sided sym F reverse  (lambda (a b) (lf-formula sym a b))) )

;; Given (op2 (op1 a ...) ...) distribute to get (op1 (op1 r) ...)
;; Must have {op1, op2} = {and, or}, op1 dual of op2.  This is not checked.
;;
;; (op2 (op1 a b) (op1 c d)) --> (op1 (op2 a c) (op2 a d) (op2 b c) (op2 b d))
(define (lf-rule-distrib-swap-duals F op1 op2)
  (let ([top-lll (map (lambda (A) (map lf-args (lf-args A))) (lf-args F))])
    ; Now top-lll is a list of implied (op2 (op1 a ...) ...)
    (let ([result-ll (car top-lll)])
      ; Distribute over successive implied factors.
      (for ([tll (cdr top-lll)])
        ; Form new result-ll of appends of one from result-ll and one from tll.
        (let ([new-result-ll '()])
          (for ([rj result-ll])
            (for ([tk tll])
              (set! new-result-ll (cons (append rj tk) new-result-ll)) ) ) 
          (set! result-ll (reverse new-result-ll)) ) )
      ; Put operators back in.
      (lf-apply op1 (map (lambda (a) (lf-apply op2 a)) result-ll)) ) ) )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Transformations (applying deeply)
;;;+ 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Transformation to eliminate all impl and equiv.
(define (lf-not/and/or-only F)
  ;(lf-check! F)
  (cond
    [(lf-atom? F)  F]
    [(lf-impl? F)  (lf-rule-elim-impl  (lf-map lf-not/and/or-only F))]
    [(lf-equiv? F) (lf-rule-elim-equiv (lf-map lf-not/and/or-only F))]
    [(lf-xor? F)   (lf-rule-elim-xor   (lf-map lf-not/and/or-only F))]
    [(lf-nand? F)  (lf-rule-elim-nand  (lf-map lf-not/and/or-only F))]
    [(lf-nor? F)   (lf-rule-elim-nor   (lf-map lf-not/and/or-only F))]
    [(lf-xnor? F)  (lf-rule-elim-xnor  (lf-map lf-not/and/or-only F))]
    [else          (lf-map lf-not/and/or-only F)] ) )

;; Transformation to push all nots down to literals.
(define (lf-push-nots-down F)
  (lf-check! F)
  (cond
    [(lf-const? F)      F]
    [(lf-atom? F)       F]
    [(not (lf-not? F)) (lf-map lf-push-nots-down F)]
    [else ; not-case
      (let* ([A (lf-first-arg F)] [op (lf-op-sym A)] [nargs (lf-nargs A)])
        (cond
          [(lf-atom?  A) F]
          [(lf-const? A) F]
          [(= 0 nargs)
            (lf-const (not (lf-op-simplified-nullary op))) ]
          [(lf-not? A)
            (lf-push-nots-down (lf-first-arg A)) ]
          [(memq op '(and or forall exists))
            (lf-push-nots-down (lf-rule-demorgan-down F)) ]
          [(lf-nand? A)
            (lf-push-nots-down (apply lf-and (lf-args A))) ]
          [(lf-nor? A) 
            (lf-push-nots-down (apply lf-or  (lf-args A))) ]
          ; not (X -> Y) = not (not X or Y) = X and not Y
          [(lf-impl? A) (lf-push-nots-down
            (lf-and (lf-first-arg A) (lf-not (lf-second-arg A)))) ]
          ; not (X <-> Y) = (not X) <-> Y, etc
          [(memq op '(equiv xnor xor)) (lf-push-nots-down
            (lf-apply op (cons (lf-not (lf-first-arg A)) (cdr (lf-args A))))) ]
          [else
            (bug! "Unexpected operator" op)]) )]))

;; Transformation to make all associative operations n-ary.
;; TODO: xor xnor nand nor ??
(define (lf-assoc-nary F)
  (lf-check! F)
  (cond
    [(lf-atom? F) F]
    [(and (not (lf-or? F)) (not (lf-and? F)))
      (lf-map lf-assoc-nary F)]
    [else 
      ; This will not descend tree twice since lf-rule-s are shallow.
      (lf-map lf-assoc-nary (lf-rule-assoc-nary (lf-op F) F)) ] ) )

;; Transformation to DNF or CNF
(define ((lf-cnf-dnf op-outer op-inner) F)

  (define (nf F)
    (if (lf-literal? F)
      ; Base case
      (lf-formula op-outer (lf-formula op-inner F))

      ; Inductive case
      (let ([op (lf-op F)] [args (lf-args F)])
        (cond
          ; Errors if not nested ands and ors.
          [(and (not (eq? op 'and)) (not (eq? op 'or)))
            (error! "lf-cnf-dnf requires and and or connectives. Got ~a." op) ]
          ; Degenerate cases.
          [(null? args)
            (if (eq? op op-outer)
              (lf-formula op-outer)
              (lf-formula op-outer (lf-formula op-inner)) )]
          ; Only one arg. Use (and x) = x, (or x) = x.
          [(null? (cdr args))
            (nf (car args)) ]
          ; Join if F had op-outer
          [(eq? op op-outer)
            (lf-apply op-outer
              (apply append (map lf-args (map nf args)))) ]
          ; Distribute if F had op-inner
          [(eq? op op-inner)
            (lf-rule-distrib-swap-duals
              (lf-apply op (map nf args)) op-outer op-inner ) ]
          [else
            (bug! "Bug in lf-cnf-dnf.") ] ) ) ) )

  ;(lf-check! F)
  (nf (lf-push-nots-down (lf-not/and/or-only F))) )

(define lf-dnf (lf-cnf-dnf 'or 'and))
(define lf-cnf (lf-cnf-dnf 'and 'or))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Terms
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; This is a representation for conjunctions or disjunctions of literals.
;; It can be used with DNF, CNF, computing prime implicants, clauses, etc.
;;
;; In order to later allow these to be mixed with general logical formula
;; representation, they carry their sense and atom lists with them.
;; The atom lists should be eq? among all terms in a given problem.
;;
;; When computing a set of implicants, the terms are collected in a
;; (potentially unary or nullary) lf-or.
;;
;; When computing a set of clauses, the terms are collected in a
;; (potentially unary or nullary) lf-and.
;;
;; <term>     ::= #s( <op> <atoms> <literal vector> )
;;
;; <op>       ::= and | or
;; <atoms>    ::= list of atoms
;; <literal>  ::= tlit-pos | tlit-neg | tlit-none

;;;
;;; Literal indicators
;;;
(define tlit-none #\.)   ; atom     is not present
(define tlit-pos  #\+)   ; atom     is present (without negation)
(define tlit-neg  #\-)   ; not atom is present

;;;
;;; The structure
;;;
(struct term (op atoms lits)
    #:transparent
    #:methods gen:custom-write
    [(define (write-proc term port mode)
        (fprintf port "{~a}" (vector->string (term-lits term))) )] )

;;;
;;; Other functions
;;;
(define (term-copy T)   
    (term (term-op T) (term-atoms T) (vector-copy (term-lits T)) ))

(define (term-counts T)
  (let ([npos 0] [nneg 0] [nnone 0])
    (for ([lit (in-vector (term-lits T))])
      (cond [(equal? lit tlit-pos)  (set! npos  (+ 1 npos))]
            [(equal? lit tlit-neg)  (set! nneg  (+ 1 nneg))]
            [else                       (set! nnone (+ 1 nnone))]))
    (values npos nneg nnone) ))

(define (term-npos T) (let-values ([(npos nneg nnone) (term-counts T)]) npos))
(define (term-nneg T) (let-values ([(npos nneg nnone) (term-counts T)]) nneg))
(define (term-nnone T)(let-values ([(npos nneg nnone) (term-counts T)]) nnone))

;;; Vector view
(define (term-length T)      (vector-length (term-lits T)))
(define (term-ref  T ix)     (vector-ref    (term-lits T) ix))
(define (term-set! T ix val) (vector-set!   (term-lits T) ix val))

;; Copy of T with slot ix set to tlit-none.
(define (term-with-none-at T ix)
  (let ([new-T (term-copy T)]) (term-set! new-T ix tlit-none) new-T) )

;;;
;;; Conversion between terms and formulas.
;;;

;; Make an 'and or 'or term structure from a term formula.
;; Return #f or #t if given complementary literals for 'and or 'or respectively.

(define (make-term-with-lf op atoms lf)
  (unless (and (or (eq? op 'and) (eq? op 'or)) (eq? op (lf-op lf)))
    (error! "Formula ~a not suitable for making a term with ~a." lf op) )

  (let* ([v (make-vector (length atoms) tlit-none)]
         [return-value (term op atoms v)]
         [had-compl? #f])
    (for ([lfi (lf-args lf)])
      (let* ([atomi (if (lf-not? lfi) (lf-first-arg lfi) lfi)]
             [pos   (find-position atomi atoms eq?)])
        (when (= pos -1)
           (error! "Argument ~a unsuitable for term of atoms ~a." atomi atoms))
        (let ([vpos (vector-ref v pos)]
              [this-val (if (eq? atomi lfi) tlit-pos tlit-neg)])
          (cond
            [(equal? vpos tlit-none) (vector-set! v pos this-val)]
            [(equal? vpos this-val)] ; skip
            [else (set! had-compl? #t)] )) )) ; complementary literals
    (if had-compl? (eq? op 'or) return-value) ))

;; Convert a term back to a formula.
(define (term-formula T)
  (let ([args '()])
    (for ([i (in-range (term-length T))] [atomi (term-atoms T)])
      (let ([ti (term-ref T i)])
         (when (equal? ti tlit-pos)
            (set! args (cons atomi args)))
         (when (equal? ti tlit-neg)
            (set! args (cons (lf-not atomi) args)))))
    (lf-apply (term-op T) (reverse args)) ))

;;;
;;; Term numbers
;;;

;; Compute a term number:
;; sum(x_i * 2^i, i = 0..n-1) for x_0,...x_{n-1} each being 0 or 1.
;; Returns -1 if any of the values are tlit-none.

(define (term->termno term)
  (do ([tno 0] [ix 0 (+ 1 ix)] [twopow 1 (* 2 twopow)])
    [(>= ix (term-length term)) tno]
    (let* ([tix (term-ref term ix)]
           [pos? (equal? tix tlit-pos)] [neg? (equal? tix tlit-neg)])
      (unless (or pos? neg?) (set ix (term-length term)) (set! tno -1) )
      (set! tno (+ tno (* twopow (bool->zero-one pos?)))) )))

;;  Convert a term number back to a term.
(define (make-term-with-termno op atoms tno)
  (let ([term (make-term-with-lf op atoms (lf-apply op '()))] [tnoi tno])
    (for ([i (in-range (term-length term))])
      (term-set! term i (if (= (remainder tnoi 2) 1) tlit-pos tlit-neg))
      (set! tnoi (quotient tnoi 2)) )
    (unless (= tnoi 0) (error! "Term no. ~a too big for atoms ~a." tno atoms) )
    term ))   

;;;
;;; all-terms: compute minterms or maxterms.
;;;

;; Given one term, make a list of all possible terms with absent atoms
;; replaced by positive or negative values.
;;
;; E.g.  Writing terms as [ ] with + - n for positive, negative, absent,
;;
;; (all-terms [+])    --> (list [+])
;; (all-terms [n])    --> (list [+] [-])
;; (all-terms [+n-n]) --> (list [++-+] [++--] [+--+] [+---])
;;
;; For a list ell of "or" terms,  (apply and ell) = (apply and (all-terms ell).
;; For a list ell of "and" terms, (apply or  ell) = (apply or  (all-terms ell).

(define (all-terms T)
   ; Argument this-t is newly allocated and will be included in the result list.
   (define (do-index this-t ix list-so-far)
     (cond
       [(>= ix (term-length this-t))
         (cons this-t list-so-far)]
       [(nequal? (term-ref this-t ix) tlit-none)
         (do-index this-t (+ 1 ix) list-so-far)]
       [else
         (let ([tc (term-copy this-t)])
           (term-set! tc ix tlit-neg)
           (term-set! this-t  ix tlit-pos)
           (do-index this-t (+ 1 ix) (do-index tc (+ 1 ix) list-so-far)) )] ))
   (do-index (term-copy T) 0 '()) )

;; Like all-terms, but returns list of term numbers.

(define (all-termnos T)
   (define (do-index t ix tno pow2 list-so-far)
     (let ([ix+ (+ 1 ix)] [pow2* (* 2 pow2)])
       (cond
         [(>= ix (term-length t))
           (cons tno list-so-far)]
         [(not (equal? (term-ref t ix) tlit-none))
           (let ([tix (bool->zero-one (equal? (term-ref t ix) tlit-pos))])
             (do-index t ix+ (+ tno (* pow2 tix)) pow2* list-so-far))]
         [else
           (do-index t ix+ tno pow2* (do-index t ix+ (+ tno pow2) pow2*
             list-so-far )) ]) ))
   (do-index T 0 0 1 '()) )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Prime implicants
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (term-list-syms term-list)
  (sort (apply lset-union (map lf-prop-symbols term-list)) lf-atom<?) )

;; Find the prime implicants of a given logical formula.
;; The second, optional argument, is the method to use.
(define (lf-prime-implicants . args)
   (define F (lf-simplify-and/or (lf-dnf (car args))))
   (define method
     (if (list-length<? args 2) prime-implicants-from-dnf (cadr args)))
   (cond
     [(equal? F (lf-true))  (list (lf-and))] ; list of one empty conjunction
     [(equal? F (lf-false)) '()]             ; list of zero conjunctions
     [else
       (let* ([syms      (sort (lf-prop-symbols F) lf-atom<?)]
              [disjuncts (map (lambda (d) (lf-apply 'and (lf-conjuncts d)))
                           (lf-disjuncts F))]
              [terms     (filter non-null?
                           (map (lambda (d) (make-term-with-lf 'and syms d))
                             disjuncts)) ])
         (sort (map term-formula (method terms)) lf<?) )]))

;; Find the prime implicants given a term list.
(define (prime-implicants term-list)
  (prime-implicants-from-dnf term-list) )

;; Given a list of prime implicants and a list of dont-care minterms
;; return a list of essential prime implicants.
;; dc = don't care
(define (essential-prime-implicants pi-lset dc-minterm-lset)
    ;; 1. Get the min-terms for each prime-implicant
    ;; 2. Determine which min-terms appear in only one prime-implicant.
    ;; 3. Construct list of prime implicants giving those min-terms.
    (when *do-debug*
      (pretty-println "pi-lset    =     " pi-lset)
      (pretty-println "dc-mt-lset =     " dc-minterm-lset))
    (let* ([syms (term-list-syms (append pi-lset dc-minterm-lset))]
           [pi-disjuncts
             (map (lambda (d) (lf-apply 'and (lf-conjuncts d))) pi-lset)]
           [pi-terms (filter non-null?
             (map (lambda (d) (make-term-with-lf 'and syms d)) pi-disjuncts))]
           [pi-minterm-lists
             (map (lambda (pi) (cons pi (all-termnos pi))) pi-terms)]
           [pi-term-nos (apply lset-union (map cdr pi-minterm-lists))]

           [dc-disjuncts
             (map (lambda (d) (lf-apply 'and (lf-conjuncts d)))
                  dc-minterm-lset)]
           [dc-terms (filter term?
             (map (lambda (d) (make-term-with-lf 'and syms d))
                  dc-disjuncts)) ]
           [dc-minterm-lists 
             (map (lambda (pi) (cons pi (all-termnos pi))) dc-terms)]
           [dc-term-nos (apply lset-union (map cdr dc-minterm-lists))]
        )
        (when *do-debug*
          (pretty-println "syms =             " syms)
          (pretty-println "pi-disjuncts =     " pi-disjuncts)
          (pretty-println "pi-terms =         " pi-terms)
          (pretty-println "pi-minterm-lists = " pi-minterm-lists)
          (pretty-println "pi-term-nos =      " pi-term-nos)
          (pretty-println "dc-disjuncts =     " dc-disjuncts)
          (pretty-println "dc-terms =         " dc-terms)
          (pretty-println "dc-minterm-lists  =" dc-minterm-lists )
          (pretty-println "dc-term-nos =      " dc-term-nos) )
        (let ([essential-pis '()]
              [two-pow-n (expt 2 (length syms))])
          (do ([i 0 (+ 1 i)])
            [(= i two-pow-n)]
            (unless (member? i dc-term-nos)
              ; Count how many times minterm i occurs. Set i-implies-essential.
              (let ([i-implies-essential #f])
                (do ([count-mt-i 0] [mtl pi-minterm-lists (cdr mtl)])
                  [(null? mtl) (set! i-implies-essential (= count-mt-i 1)) ]
                  (let ([pi (caar mtl)] [mtl-mts (cdar mtl)])
                      (when (member? i mtl-mts)
                            (set! count-mt-i (+ 1 count-mt-i)))) )
                
                (when i-implies-essential
                   (do ([found? #f] [mtl pi-minterm-lists (cdr mtl)])
                     [(or found? (null? mtl))]
                     (let ([pi (caar mtl)] [mtl-mts (cdar mtl)])
                         (when (member? i mtl-mts)
                               (set! essential-pis (cons pi essential-pis))
                               (set! found? #t))))) ) ) ) 
            (map term-formula essential-pis) ) ))

(define (find-minimal-pi-cover pi-lset dc-minterm-lset)
    ;; 1. Find the set of all minterms needed.
    ;; 2. Remove all those covered by essential prime implicants
    ;; 3. Find a minimal set of non-essential prime implicants to cover rest.
    (let* (

           [syms (term-list-syms (append pi-lset dc-minterm-lset))]

           [pi-disjuncts
             (map (lambda (d) (lf-apply 'and (lf-conjuncts d))) pi-lset)]
           [pi-terms (filter term?
             (map (lambda (d) (make-term-with-lf 'and syms d)) pi-disjuncts)) ]

           [pi-minterm-lists
             (map (lambda (pi) (cons pi (all-termnos pi))) pi-terms)]
           [pi-term-nos (apply lset-union (map cdr pi-minterm-lists))]

           [dc-disjuncts
             (map (lambda (d) (lf-apply 'and (lf-conjuncts d)))
                  dc-minterm-lset)]
           [dc-terms (filter term?
             (map (lambda (d) (make-term-with-lf 'and syms d))
                  dc-disjuncts)) ]
           [dc-minterm-lists 
             (map (lambda (pi) (cons pi (all-termnos pi))) dc-terms)]
           [dc-term-nos (apply lset-union (map cdr dc-minterm-lists))]

           [essential-pis (essential-prime-implicants pi-lset dc-minterm-lset)]
           [epi-terms (map (lambda (d) (make-term-with-lf 'and syms d))
                           essential-pis)]
           [epi-term-nos 
             (apply lset-union (map all-termnos epi-terms))]
           [remaining-term-nos
             (lset-minus (lset-minus pi-term-nos dc-term-nos) epi-term-nos)]
           [non-essential-pis (lset-minus pi-lset essential-pis)]
           [ne-pi-terms (map (lambda (d) (make-term-with-lf 'and syms d))
                           non-essential-pis)]
           [ne-pi-minterm-lists 
             (map (lambda (pi) (cons pi (all-termnos pi))) ne-pi-terms)]
           [cover-remaining
             (find-minimal-cover remaining-term-nos ne-pi-minterm-lists 'short)]
           [minimal-pi-cover
             (append essential-pis 
                     (map term-formula (map car cover-remaining)))]
        )
     (when *do-debug*
       (pretty-println "FMC essential-pis         = " essential-pis)
       (pretty-println "FMC epi terms             = " epi-terms)
       (pretty-println "FMC epi term nos          = " epi-term-nos)
       (pretty-println "FMC pi minterm lists      = " pi-minterm-lists)
       (pretty-println "FMC all term nos          = " pi-term-nos)
       (pretty-println "FMC remaining term nos    = " remaining-term-nos)
       (pretty-println "FMC Non-essential-pis     = " non-essential-pis)
       (pretty-println "FMC N-e-pi term lists     = " ne-pi-minterm-lists)
       (pretty-println "FMC Cover remaining       = " cover-remaining)
       (pretty-println "FMC Minimal pi cover      = " minimal-pi-cover) )
     minimal-pi-cover) )

;; Find a minimal dnf for a logical formula.  
;; An optional second argument gives a list of dont-care minterms
(define (minimal-dnf lf . opt-args)
  (let* ([dc-minterms (if (null? opt-args) '() (car opt-args))]
         ;; TODO Fix to use abstract constructor
         [ok-lf (if (null? dc-minterms) lf (append (list 'or lf) dc-minterms))]
         [pis   (lf-prime-implicants ok-lf)]
         [cover (find-minimal-pi-cover pis dc-minterms)])
    ;; TODO Fix to use abstract constructor
    (cons 'or cover) ) ) 

;;;
;;; Reduce a pair of terms.
;;;
;;  A pair of terms can be reduced in one of four ways:
;;  * Complement:   abc. + ab'c.  = a.c.
;;  * Absorb:       ab.. + ab c.  = ab..
;;  * Generalize:   a... + a'b..  = a... + .b..
;;  * Fail:         a... + . b..  = a... + .b..
;;
(define (term-reduce-analyze A B)
  (let ([t-len (term-length A)]
        [A-absorbs #f] [B-absorbs #f] ; One absorbs the other at some index.
        [comp-ct  0]         ; Count of complementing literals.
        [comp-ix -1])        ; Index of last complementing literals.
    (debug "A = ~a, B= ~a~n" A B)
    (do ([i 0 (+ 1 i)])
      [(>= i t-len)]
      (let ([Ai (term-ref A i)] [Bi (term-ref B i)])
        (cond 
          [(and (equal?  Ai tlit-none) (nequal? Bi tlit-none))
            (set! A-absorbs #t)]
          [(and (nequal? Ai tlit-none) (equal?  Bi tlit-none))
            (set! B-absorbs #t)]
          [(and (equal?  Ai tlit-none) (equal?  Bi tlit-none)) ] ; skip
          [(equal?  Ai Bi)] ; skip
          [else
            ; Ai and Bi are complementary
            (set! comp-ct (+ 1 comp-ct))
            (set! comp-ix i) ] )))
    (values A-absorbs B-absorbs comp-ct comp-ix)))

;;
;; (term-reduce-pair A B) is one of
;;
;;    ('Complement T1)     T1 is a new term, replacing A and B.
;;    ('Absorb     T1 T2)  T1 is A or B. T2 is the absorbed other.
;;    ('Generalize T1 T2)  T1 is A or B. T2 is the generalized other.
;;    'Fail
(define (term-reduce-pair A B)
  (let-values
    ([(A-absorbs B-absorbs comp-ct comp-ix) (term-reduce-analyze A B)])
    (cond
      [(and A-absorbs (not B-absorbs))
        (cond 
          [(= comp-ct 0) (list 'Absorb A)]
          [(= comp-ct 1) (list 'Generalize A (term-with-none-at B comp-ix))]
          [else 'Fail] )]
      [(and (not A-absorbs) B-absorbs)
        (cond 
          [(= comp-ct 0) (list 'Absorb B)]
          [(= comp-ct 1) (list 'Generalize B (term-with-none-at A comp-ix))]
          [else 'Fail] )]
      [(and (not A-absorbs) (not B-absorbs))
        (cond
          [(= comp-ct 1) (list 'Complement   (term-with-none-at A comp-ix))]
          [else 'Fail] )]
      [else ; Both had a none where the other had pos or neg.
          'Fail] ) ))

;;;
;;; Try to reduce a pair of terms by complementation only.
;;; Special case of (term-reduce-pair A B).
;;
;; Can reduce if pair has exactly one coordinate with a positive and negative.
;; Returns (list 'Complement T) for reduced term T or 'Fail if can't reduce.
;; This function is symmetric.

(define (term-reduce-pair-by-complement A B)
  (if (or (<> 1 (abs (- (term-npos A) (term-npos B))))
          (<> 1 (abs (- (term-nneg A) (term-nneg B)))))
    'Fail ; return non-term
    (let-values
      ([(A-absorbs B-absorbs comp-ct comp-ix) (term-reduce-analyze A B)])
      (if (or A-absorbs B-absorbs (<> comp-ct 1))
        'Fail ; return non-term
        (list 'Complement (term-with-none-at A comp-ix))) )))

;;;
;;; Find prime implicants by critical pair completion.
;;;
;;  Merge pairs of potentially merge-able terms.
;;  For the Complement, Absorb and Generalize results, the terms T_i are
;;  retained for further reduction and the input arguments discarded.
;;  (For Absorb and Generalize, this means keeping one argument and
;;  replacing the other.)
;;
;;  In the Fail case, the arguments are noted irreducible and removed
;;  from consideration for further reduction.

(define (prime-implicants-pair-completion merge-fn terms)
  (let ([todo-terms   terms]
        [output-terms '()]
        [init-only-minterms? (andmap (lambda (t) (= 0 (term-nnone t))) terms)])

    (do ( )
      [(null? todo-terms) output-terms]
      (debug "Big iteration: todo-terms = ~a~n" todo-terms)
      (let ([new-terms    (lset-empty)]
            [killed-terms (lset-empty)])
        (do ([A-list todo-terms (cdr A-list)])
          [(null? A-list)]
          (let ([Ai (car A-list)])
            (do ([B-list (cdr A-list) (cdr B-list)])
              [(null? B-list)]
              (let* ([Bi (car B-list)] [R (merge-fn Ai Bi)])
                (debug "Merging ~a ~a to get ~a~n" Ai Bi
                       (if (eq? R 'Fail) 'Fail R))
                (cond
                  [(eq? R 'Fail)]    ; skip
                  [(eq-car? R 'Complement)
                    (let ([new-general (cadr R)])
                      (set! killed-terms
                        (lset-union1 Ai (lset-union1 Bi killed-terms)))
                      (set! new-terms
                        (lset-union1 new-general new-terms)) )]
                  [(eq-car? R 'Absorb)
                    (let* ([original (cadr R)]
                           [absorbee (if (neq? original Ai) Ai Bi)])
                      (set! killed-terms
                        (lset-union1 absorbee killed-terms)) )]
                  [(eq-car? R 'Generalize)
                    (let* ([original    (cadr R)]
                           [new-general (caddr R)]
                           [generalizee (if (neq? original Ai) Ai Bi)])
                      (set! killed-terms
                        (lset-union1 generalizee killed-terms))
                      (set! new-terms
                        (lset-union1 new-general new-terms)) )]
                  [else
                    (bug! "Unexpected case in prime-implicants.") ] )

                (debug "new-terms    = ~a~n"   new-terms)
                (debug "killed-terms = ~a~n~n" killed-terms)
        ))))
        (cond
          ;; If started with only minterms, anything not killed is prime.
          ;; Try combining the new terms with each other.
          [init-only-minterms?
            (set! output-terms (lset-union output-terms
              (lset-minus todo-terms killed-terms) ))
            (set! todo-terms new-terms)]

          ;; If there were no new terms, todo list is prime and we are done.
          [(null? new-terms)
            (set! output-terms (lset-union output-terms
              (lset-minus todo-terms killed-terms) ))
            (set! todo-terms '())]

          ;; There were some new terms, and these may potentially combine
          ;; with old ones.
          [else
            (set! todo-terms (lset-union new-terms
              (lset-minus todo-terms killed-terms) )) ]) )
        (debug "todo-terms   = ~a~n" todo-terms)
        (debug "output-terms = ~a~n" output-terms) )))

(define (prime-implicants-from-dnf terms)
  (prime-implicants-pair-completion
    term-reduce-pair
    terms ))

(define (quine-mccluskey-algorithm terms)
  ; Call with all minterms.
  (prime-implicants-pair-completion
    term-reduce-pair-by-complement
    (list->lset (foldr append '() (map all-terms terms))) ))

;;;
;;; Simplified Quine-McCluskey algorithm (not grouping by Hamming weight).
;;;
(define (simplified-quine-mccluskey-algorithm terms)
  ;; Iteratively merge until no merges possible.
  ;;
  ;; For each term try to merge it with all others it has not
  ;; already been tried with.  If it could merge, add it to list
  ;; of merged.  Otherwise, record it as un-mergeable.

  (define (merge-terms terms-list)
    (let ([un-mergeable '()])
      (do ( )
        [(null? terms-list)]

        (let ([merged  (lset-empty)] [mergees (lset-empty)])
          (do ([A-list terms-list (cdr A-list)])
            [(null? A-list)]
            (let ([Ai (car A-list)])
              (do ([B-list (cdr A-list) (cdr B-list)])
                [(null? B-list)]
                (let* ([Bi (car B-list)]
                       [AB (term-reduce-pair-by-complement Ai Bi)])
                  (when (term? AB)
                    (set! merged
                      (lset-union1 AB merged))
                    (set! mergees
                      (lset-union1 Ai (lset-union1 Bi mergees)) ) )) )))
          (set! un-mergeable
            (lset-union un-mergeable (lset-minus terms-list mergees)) )
          (set! terms-list merged) ))
      un-mergeable ))
  (if (null? terms)
    '()
    ; else merge, starting with min-terms
    (merge-terms (list->lset (foldr append '() (map all-terms terms) ))) ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Davis Putnam Procedure
;;;+ 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Resolve terms t1 and t2 on symbol with index ix.
;; To resolve, symbol ix must appear oppositely in t1 and t2.
;; If another symbol also appears oppositely, then the resolvent is #t.
;; If the terms don't resolve, return a non-term.
(define (resolve-terms ix t1 t2)
    (let ([atoms1 (term-atoms t1)] [atoms2 (term-atoms t2)])
      (when (not (equal? atoms1 atoms2))
        (error! "Cannot resolve terms with different atoms."))
      (let ([n (term-length t1)] [newt (term-copy t1)])
        (do ([i 0 (+ 1 i)]  [another-had-both? #f])
          [(or (= i n) another-had-both?)
           (if another-had-both? #t newt)]
          (let ([l1 (term-ref t1 i)] [l2 (term-ref t2 i)])
            (cond
              [(and (= i ix))
               (if (or (equal? l1 l2)
                       (equal? l1 tlit-none) (equal? l2 tlit-none))
                 (set! ok? #f)
                 (term-set! newt i tlit-none))]
              [(equal? l1 tlit-none) (term-set! newt i l2)]
              [(equal? l2 tlit-none) (term-set! newt i l1)]
              [(equal? l1 l2)        (term-set! newt i l1)]
              [else (set! another-had-both? #t)]) ))) ) )
    
;; Apply the Davis-Putnam procedure on the formulas in lf-list,
;; eliminating proposition symbols in the order given by sym-list.
(define (dpp sym-list lf-list #:verbose? [verbose? #f])
   (define (make-clause lf)     (make-term-with-lf 'or sym-list lf))
   (define ((has-pos? ix) term) (equal? tlit-pos (term-ref term ix)))
   (define ((has-neg? ix) term) (equal? tlit-neg (term-ref term ix)))

   (let* ([cnf-list  (map (compose lf-cnf lf-not/and/or-only) lf-list)]
          [conjuncts (apply lset-union (map lf-conjuncts cnf-list))]
          [clauses   (filter term? (map make-clause conjuncts))])
   (when verbose?
     (printf "Formulas:~n")  (pretty-print lf-list)
     (printf "Conjuncts:~n") (pretty-print conjuncts)
     (printf "Clauses:~n")   (pretty-print clauses))
   (do ([i 0 (+ 1 i)])
     [(= i (length sym-list))]
     (let* ([sym (list-ref sym-list i)]
            [pos-sym-clauses (filter (has-pos? i) clauses)]
            [neg-sym-clauses (filter (has-neg? i) clauses)]
            [sym-clauses (append pos-sym-clauses neg-sym-clauses)]
            [resolvents '()])
       (when verbose?
         (printf "Sym ~a pos: ~a~n" sym pos-sym-clauses)
         (printf "Sym ~a neg: ~a~n" sym neg-sym-clauses) )
       (for ([pos pos-sym-clauses])
         (for ([neg neg-sym-clauses])
           (let ([r (resolve-terms i pos neg)])
             (when verbose?
               (printf "Resolving ~a and ~a to get ~a~n" pos neg r))
             (when (term? r) ;; Exclude #t terms.
               (set! resolvents (lset-union1 r resolvents)) )) ))
       (set! clauses (lset-minus clauses sym-clauses))
       (set! clauses (lset-union clauses resolvents )) 
       (when verbose?
         (printf "Eliminated ~a clauses: ~a~n" sym clauses) )
   ))
   ;; At this point clauses list is either empty or has only the empty clause.
   (if (null? clauses) clauses (list (lf-or))) ))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Truth tables
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Construct a list of rows for a truth table with n symbols and m connectives.
;; The first is a list of logical formulas, the first n of which are symbols
;; and the remaining m of which are sub-formulas introduced by the connectives.
;; The next 2^n rows correspond to the different truth valuations.

(define (truth-table-of-formulas symbols formulas)
  (cons formulas
      (map (lambda (tv) (map (curry tv-apply tv) formulas))
           (tv-all-valuations symbols))) )
  
(define (truth-table-of-parts lf)
  (define (union-parts lf lset)
    (unless (lf-atom? lf)
      (for ((arg (lf-args lf)))
        (unless (lf-const? arg) (set! lset (union-parts arg lset))) ))
    (lset-union1 lf lset) )
       
  (let* ((rsyms (lf-prop-symbols lf))
         (syms  (reverse rsyms))
         (subforms (reverse (union-parts lf rsyms))))
    (truth-table-of-formulas syms subforms) ) )

;; The header of a truth table
(define (tt-headers tt)(unless (pair? tt) '(error! "Bad truth table")) (car tt))

;; The truth-valuation rows of a truth table
(define (tt-rows tt)   (unless (pair? tt) '(error! "Bad truth table")) (cdr tt))

;; The number of symbols in a truth table
(define (tt-nsyms tt)
  (do ([hdrs (tt-headers tt) (cdr hdrs)] [i 0 (+ 1 i)])
      [(or (null? hdrs) (not (lf-prop-symbol? (car hdrs)))) i] ))

;; The number of columngs  in a truth table
(define (tt-ncols tt) (length (tt-headers tt)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Logical Formula With Selection
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; A logical formula with selection is a list ('LFWS A B C), where
;;;   A is the 0-inexed path of child numbers to the start node,
;;;   B is the span, i.e. number of selected children,
;;;   C is a logical formula.
;;;
;;; The path and span have the same meaning as in path-op.


;;; The functions below return either a logical formula with selection or null
;;; if the operation was not possible.
;;; If the variable *lfws-verbose* is #t, then messages are given.

(define *lfws-verbose* #t)

(define (lf-with-selection lf [path '()] [span 1])
  (unless (lfws-path-ok? path span lf) (bug! "Bad call to lf-with-selection"))
  (list 'LFWS path span lf))
(define (lfws? x)  (and (eq-car? x 'LFWS) (= (length x) 4)))
(define (lfws-path  lfws) (cadr lfws))
(define (lfws-span  lfws) (caddr lfws))
(define (lfws-lf    lfws) (cadddr lfws))
(define (lfws-rpath lfws) (reverse (lfws-path lfws)))

(define (lfws-debug prefix lfws)
  (let ([path (lfws-path lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
    (printf "~a\n" prefix)
    (printf "lfws: ~a~n" lfws)
    (printf "path: ~a~n" path)
    (printf "span: ~a~n" span)
    (printf "lf:   ~a~n" lf))
  lfws)

(define (lfws-is-ok? lfws)
  (and (lfws? lfws)
       (lfws-path-ok? (lfws-path lfws) (lfws-span lfws) (lfws-lf lfws))) )

(define (lfws-show x) (lfws-lf (lfws-apply-to-selection (lambda (y) (list '>>>> y '<<<<)) x)))

(define (lfws-selection lfws)
  (let ([path (lfws-path lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
     (if (= span 1)
       (lf-xarg lf path)
       (lf-xarg-span lf path span))))

;; Apply f to the selection in lfws to create a new lfws.
(define (lfws-apply-to-selection f lfws)
  (let ([path (lfws-path lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
    (define newf
      (if (= span 1)
        (lf-xarg-subs      lf path      (f (lf-xarg      lf path)))
        (lf-xarg-span-subs lf path span (f (lf-xarg-span lf path span))) ))
    (lf-with-selection newf path 1) ))

;; Change selection to the n-th child or path of the selection, if possible.
(define (lfws-focus-down lfws where-to) 
  (when (integer? where-to) (set! where-to (list where-to)))
  (let ([path (lfws-path lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
    (lf-with-selection lf (append path where-to) 1) ))
     
;; Change selection to the n-th parent of current selection, if possible.
(define (lfws-focus-up lfws n)
  (let ([rpath (lfws-rpath lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
    (if (or (= n 0) (null? rpath))
      lfws
      (lfws-focus-up (lf-with-selection lf (reverse (cdr rpath)) 1) (- n 1)) )))

;; Change selection to n-th next child, if possible.
(define (lfws-focus-left  lfws n)
  (let ([rpath (lfws-rpath lfws)] [span  (lfws-span lfws)] [lf (lfws-lf lfws)])
    (if (and (<> n 0) (null? rpath))
        '()
        (lf-with-selection lf 
            (reverse (cons (- (car rpath) n) (cdr rpath))) 1 ) )))

;; Change selection to n-th previous child, if possible.
(define (lfws-focus-right  lfws n)
  (let ([rpath (lfws-rpath lfws)] [span  (lfws-span lfws)] [lf (lfws-lf lfws)])
    (if (and (<> n 0) (null? rpath))
        '()
        (lf-with-selection lf 
            (reverse (cons (+ (car rpath) n) (cdr rpath))) 1 ) )))

;; Grow selection by n toward left, if possible. Negative n means shrink.
(define (lfws-grow-left  lfws n)
  (let ([rpath (lfws-rpath lfws)] [span  (lfws-span lfws)] [lf (lfws-lf lfws)])
    (if (and (<> n 0) (null? rpath))
        '()
        (lf-with-selection lf 
            (reverse (cons (- (car rpath) n) (cdr rpath))) (+ span n) ) )))

;; Grow selection by n toward right, if possible. Negative n means shrink.
(define (lfws-grow-right lfws n)
  (let ([path (lfws-path lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
    (if (and (<> n 0) (null? path))
        '()
        (lf-with-selection lf path (+ span n)) )))

;; Move selection by n toward left, if possible.
(define (lfws-move-left lfws n) (lfws-move-right lfws (- n)))

;; Move selection by n toward right, if possible.
(define (lfws-move-right lfws n) (call/cc (lambda (return)
    (define (enforce! ok? . args)
      (unless ok? (when *lfws-verbose* (apply printf args)) (return '()) ))

    (when (= n 0) (return lfws))

    (let ([rpath (lfws-rpath lfws)] [span (lfws-span lfws)] [lf (lfws-lf lfws)])
      (enforce! (non-null? rpath) "Can't move whole expression.~n")

      (let* ([parent-path  (reverse (cdr rpath))]
             [parent       (lf-xarg lf parent-path)]
             [parent-op    (lf-op   parent)]
             [parent-args  (lf-args parent)]
             [parent-nargs (lf-nargs parent)]
             [child-no     (car rpath)]
             [commut?      (lf-is-commutative-op? parent-op)])

        (enforce! commut? "Cannot move within non-commutative ~a.~n" parent)

        ;; For parent  (op a[1] .. a[child_no]..a[child_no+span-1] .. a[M])
        (if (< n 0)
          (enforce! (<= 1 (+ child-no n))
                    "Can't move left ~a places.~n" (- n))
          (enforce! (<= (+ child-no span  n -1) parent-nargs)
                    "Can't move right ~a places.~n" n))
        (let* ([nbefore (- child-no 1)]
               [nafter  (- parent-nargs child-no span 1)]

               [args-before    (take parent-args nbefore)]
               [args-of-child  (take (drop parent-args nbefore) span)]
               [args-after     (drop parent-args (+ nbefore span))]

               [args-wo-child  (append args-before args-after)]
               [new-before     (take args-wo-child (+ nbefore n))]
               [new-after      (drop args-wo-child (+ nbefore n))]
               [new-all        (append new-before args-of-child new-after)]

               [new-parent     (lf-apply parent-op new-all)]
               [new-lf         (lf-carg-subs lf parent-path new-parent)]
               [new-path       (reverse (cons (+ child-no n) (cdr rpath)))])

            (lf-with-selection new-lf new-path span) ) ) )
)))


(define (lfws-path-ok? path0 span0 lf0)
  (define (check is-ok? . args)
    (when (and *lfws-verbose* (not is-ok?)) (apply printf args))
    is-ok? )
  (define (recursive-ok? path lf)  
    (if (null? path)
      ;; If no path, then need whole thing.
      (check (= span0 1) "Span = ~a <> 1 for path '().~n" span0)

      ;; Else if have path, then need start child to exist.
      (let* ([args (lf-args lf)]
             [ix (car path)] 
             [iok? (and (not (lf-atom? lf)) (>= ix 0) (list-length>? args ix))])
        (check iok? "Cannot take part ~a of ~a~n" ix lf)
        (if (not iok?)
          iok?
          (if (null? (cdr path))
            ;; If at end of path, check span.
            (let ([sok? (not (list-length<? args (+ ix span0)))]
                  [aok? (or (= span0 1) (lf-is-associative? lf))])
              (check sok? "Span = ~a at ~a not ok for ~a.~n" span0 ix lf)
              (check aok? "Span = ~a requires associative ~a.~n" span0 lf)
              (and sok? aok?) )

            ;; Else recurse
            (recursive-ok? (cdr path) (list-ref args ix)) )) )))

  (recursive-ok? path0 lf0) )

;;;
;;; A little editor
;;;

(define *lfws-expr* 'not-yet-initialized)

(define (l-set! lwfs)  (set! *lfws-expr* lwfs))
(define (l-get)        *lfws-expr*)
(define (l-show)       (lfws-show *lfws-expr*))
(define (l-selected)   (lfws-selection *lfws-expr*))

(define (l-use!   e) (l-set! (lf-with-selection e '() 1))         (l-show))
(define (l-do f   a) (l-set! (f (l-get) a))                       (l-show))
(define (l-apply  f) (l-set! (lfws-apply-to-selection f (l-get))) (l-show))

(define (l-up     [a 1]) (l-do lfws-focus-up    a))
(define (l-down   [a 0]) (l-do lfws-focus-down  a))
(define (l-left   [a 1]) (l-do lfws-focus-left  a))
(define (l-right  [a 1]) (l-do lfws-focus-right a))
(define (l-gleft  [a 1]) (l-do lfws-grow-left   a))
(define (l-gright [a 1]) (l-do lfws-grow-right  a))
(define (l-mleft  [a 1]) (l-do lfws-move-left   a))
(define (l-mright [a 1]) (l-do lfws-move-right  a))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Token I/O properties
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;;;
;;; Data structure forming operations for use by parser.
;;;
(define (parse-make-lf tok . args)
  (let ([nm (tok-lf-name tok)]) (if (boolean? nm) nm (lf-apply nm args))))

(define (parse-make-comma tok . args)  (cons 'comma args))

(define (parse-make-set   tok . args)  (cons 'set   args))

(define (parse-make-subs  tok id expr) (cons id expr))

(define (parse-make-fd-ent tok premises conclusion)
  (fd-ent (comma-or-item->list premises) conclusion))

(define (parse-make-collect tok elements)
  (cons tok (comma-or-item->list elements)))

(define (comma-or-item->list item)
  (if (and (pair? item) (eq-car? item 'comma)) (cdr item) (list item)))
    
;;;
;;; The operator information table
;;;

(define *tok-props* (list
  ;     token  null pre in post  lbp     rbp     term-former    term-or-head
  (list #\⊤    #t   #f  #f  #f   +inf.0  +inf.0  parse-make-lf  #t) 
  (list #\⊥    #t   #f  #f  #f   +inf.0  +inf.0  parse-make-lf  #f) 
  (list #\∀    #f   #t  #f  #f   +inf.0  60      parse-make-lf  'forall)
  (list #\∃    #f   #t  #f  #f   +inf.0  60      parse-make-lf  'exists)
  (list #\¬    #f   #t  #f  #f   +inf.0  60      parse-make-lf  'not)
  (list #\∧    #f   #f  #t  #f   50      50      parse-make-lf  'and)
  (list #\∨    #f   #f  #t  #f   50      50      parse-make-lf  'or)
  (list #\|    #f   #f  #t  #f   50      50      parse-make-lf  'nand)
  (list #\↓    #f   #f  #t  #f   50      50      parse-make-lf  'nor)
  (list #\⊕    #f   #f  #t  #f   50      50      parse-make-lf  'xor)
  (list #\→    #f   #f  #t  #f   40      39      parse-make-lf  'impl)
  (list #\↔    #f   #f  #t  #f   30      30      parse-make-lf  'equiv)

  (list #\'    #f   #f  #f  #t   60      +inf.0  parse-make-lf  'not)
  (list #\·    #f   #f  #t  #f   50      50      parse-make-lf  'and)
  (list #\+    #f   #f  #t  #f   45      45      parse-make-lf  'or)

  (list #\=    #f   #f  #t  #f   25      25      parse-make-subs    'subs)
  (list #\,    #f   #f  #t  #f   20      20      parse-make-comma   'comma)
  (list #\⊢    #f   #t  #t  #f   10      10      parse-make-fd-ent  'ignore)
))

;; Return one of the token property lists
(define (tok-prop tok n default)
  (let ([p (assoc tok *tok-props*)]) (if (pair? p) (list-ref p n) default)))

(define (tok-info-tok info)    (car info))
(define (tok-nullfix? tok)     (tok-prop tok 1 #f))
(define (tok-prefix?  tok)     (tok-prop tok 2 #f))
(define (tok-infix?   tok)     (tok-prop tok 3 #f))
(define (tok-postfix? tok)     (tok-prop tok 4 #f))
(define (tok-lbp tok err)  (or (tok-prop tok 5 #f) (err "Bad operator" tok)))
(define (tok-rbp tok err)  (or (tok-prop tok 6 #f) (err "Bad operator" tok)))
(define (tok-term-former tok)  (tok-prop tok 7 (lambda (x) x)))
(define (tok-lf-name tok)      (tok-prop tok 8 'xxnone))

(define (tok-kind tok)
  (cond 
    [(tok-nullfix? tok) 'nullfix]
    [(tok-prefix?  tok) 'prefix]
    [(tok-infix?   tok) 'infix]
    [(tok-postfix? tok) 'postfix]
    [else               'none] ))

(define (tok-bps tok) (cons (tok-lbp tok bug!) (tok-rbp tok bug!)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Parsing
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;
;;; Character and token streams
;;;

;; Pair an input port with a position for error reporting
(define (inp ip [cno 0]) (mcons ip cno))
(define (inp-pos  in) (mcdr in))
(define (inp-port in) (mcar in))

;; Character input
(define (inp-read-char in)
    (let ([ch (read-char (inp-port in))])
      (unless (eof-object? ch) (set-mcdr! in (+ 1 (mcdr in))))
      ch ))
(define (inp-peek-char in . rest)
    (apply peek-char (cons (inp-port in) rest)) )


;; Token streams -- allow push-back of tokens
(define (tok-stream in) (mcons '() in))

(define (tok-stream-get ts syntax-error) 
  (if (null? (mcar ts))
    (in-get-token (mcdr ts) syntax-error)
    (let ([tlist (mcar ts)]) (set-mcar! ts (cdr tlist)) (car tlist))))

(define (tok-stream-unget tok ts) 
  (set-mcar! ts (cons tok (mcar ts))))

(define (tok-stream-peek ts syntax-error) 
  (let ([peek-tok (tok-stream-get ts syntax-error)])
    (tok-stream-unget peek-tok ts)
    peek-tok))


;;;
;;; Token scanning -- Result is one of:
;;;
;;;    char?
;;;       Used in formulas
;;;       #\∧  #\∨  #\¬  #\→  #\↔  #\↓  #\⊕  #\· #\' #\∀  #\∃  #\⊤  #\⊥ 
;;;      
;;;       \land  \lor  \lnot  \lxor \limpl \lequiv  \lnand \lnor \lxnor
;;;       \rightarrow \leftrightarrow \downarrow
;;;       \forall  \exists  \oplus \cdot

;;;       /\    \/    ~    ->          <->    
;;;       &     |     ! 
;;;       *     !*    +    !+     ++  
;;;       #t    #f

;;;
;;;       Used in theorems
;;;       ⊢    |-    \vdash  ,   =
;;;      
;;;    symbol?                              for a-z  A-Z
;;;    number?                              for 0-9+
;;;    eof-object?                          end of input


(define (in-get-token in syntax-error)
    (let ([c0 (inp-read-char in)])
      ;; Skip white space
      (do ()
         [(or (not (char? c0)) (not (char-whitespace? c0)))]
         (set! c0 (inp-read-char in)) )

      (cond
        [(eof-object? c0) c0]
        ;; Single characters with special meaning.
        ;;
        ;; + | ! left out since we need to check for ++, ||, |-.

        [(string-contains? "()[]{}_¬'∧∨↓→↔⊕·∀∃⊤⊥⊢,=" (string c0)) c0]
        [(char=? c0 #\~) #\¬]
        [(char=? c0 #\*) #\·]

        ;; Alphabetic followed with alphanumerics give a symbol
        [(char-alphabetic? c0)
           (do ([chars (list c0)]
                [ci (inp-peek-char in) (inp-peek-char in)])
               [(or (not (char? ci)) (not (char-alphanumeric? ci)))
                (string->symbol (apply string (reverse chars)))]
             (set! chars (cons (inp-read-char in) chars)) )]

        ;; One or more digits gives an integer.
        [(char-numeric? c0) 
           (do ([digits (list c0)]
                [ci (inp-peek-char in) (inp-peek-char in)])
               [(or (not (char? ci)) (not (char-numeric? ci)))
                (string->number (apply string (reverse digits)))]
             (set! digits (cons (inp-read-char in) digits)) )]

        ;; Compound symbols.
        [(bite-if-can? "/\\"      c0 in) #\∧]
        [(bite-if-can? "\\/"      c0 in) #\∨]
        [(bite-if-can? "->"       c0 in) #\→]
        [(bite-if-can? "<->"      c0 in) #\↔]

        [(bite-if-can? "#t"       c0 in) #\⊤]
        [(bite-if-can? "#f"       c0 in) #\⊥]

        [(bite-if-can? "&&"       c0 in) #\∧]
        [(bite-if-can? "||"       c0 in) #\∨]  ; Must come before "|"
        [(bite-if-can? "|-"       c0 in) #\⊢]  ; Must come before "|"
        [(bite-if-can? "|"        c0 in) #\|]
        [(bite-if-can? "++"       c0 in) #\⊕]  ; Must come before "+"
        [(bite-if-can? "+"        c0 in) #\+]

        [(bite-if-can? "!*"       c0 in) #\|]
        [(bite-if-can? "!+"       c0 in) #\↓]
        [(bite-if-can? "!"        c0 in) #\¬]

        [(bite-if-can? "\\land"   c0 in) #\∧]
        [(bite-if-can? "\\lor"    c0 in) #\∨]
        [(bite-if-can? "\\lnot"   c0 in) #\¬]

        [(bite-if-can? "\\lnand"  c0 in) #\|]
        [(bite-if-can? "\\lnor"   c0 in) #\↓]
        [(bite-if-can? "\\limpl"  c0 in) #\→]
        [(bite-if-can? "\\lequiv" c0 in) #\↔]
        [(bite-if-can? "\\lxor"   c0 in) #\⊕]
        [(bite-if-can? "\\lxnor"  c0 in) #\↔]

        [(bite-if-can? "\\forall" c0 in) #\∀]
        [(bite-if-can? "\\exists" c0 in) #\∃]
        [(bite-if-can? "\\top"    c0 in) #\⊤]
        [(bite-if-can? "\\bot"    c0 in) #\⊥]

        [(bite-if-can? "\\rightarrow"     c0 in) #\→]
        [(bite-if-can? "\\leftrightarrow" c0 in) #\↔]
        [(bite-if-can? "\\downarrow"      c0 in) #\↓]

        [(bite-if-can? "\\vdash"  c0 in) #\⊢]

        (else (syntax-error c0 in)) )))

;; Return #t iff c0+chars from in have s as a prefix.  
;; If so,  then all the characters matching s will be read from in.
;; If not, then no additional characters will be read from in.
;; This relies on all the characters in s being single-byte characters.
(define (bite-if-can? s c0 in)
    (let ([slen (string-length s)])
      (cond
        [(= slen 0) #t]
        [(not (char=? (string-ref s 0) c0)) #f] 
        [(= slen 1) #t]
        [(not (char=? (string-ref s 1) (inp-peek-char in))) #f]
        [else
          ;; slen >= 2 and s[0] and s[1] match.
          (let ([matching? #t] [nmatch 2])

            ;; See whether the rest of s matches.
            (do ([i 2 (+ 1 i)])
              [(or (>= i slen) (not matching?))]
              (let ([peek-i (inp-peek-char in (- i 1))])
              (if (not (char=? (string-ref s i) (inp-peek-char in (- i 1))))
                (set! matching? #f)
                (set! nmatch (+ 1 nmatch))) ) )

             ;; If matched, read the characters.
             (unless (= nmatch slen) (set! matching? #f))
             (when matching?
               (do ([i 1 (+ 1 i)]) [(= i nmatch)] (inp-read-char in)) )

             ;; Return whether the string matched.
             matching? )] )))

;;;
;;; Parsing -- produces a logical formula, fd-ent or fd-subs
;;;

(define (parse-stream in-tok-stream tok-props err-thrower)

  (define (get-tok)     (tok-stream-get  in-tok-stream err-thrower))
  (define (peek-tok)    (tok-stream-peek in-tok-stream err-thrower))

  ; This should have some thought into arguments allowed.
  (define (syn-err . msg) (err-thrower in-tok-stream msg))

  (define (rbp tok) (tok-rbp tok syn-err))
  (define (lbp tok) (tok-lbp tok syn-err))

  ; These tree formers should come in as parameters.
  (define (make-leaf tok)          ((tok-term-former tok) tok))
  (define (make-prefix  tok E)     ((tok-term-former tok) tok E))
  (define (make-infix   tok E1 E2) ((tok-term-former tok) tok E1 E2))
  (define (make-postfix tok E)     ((tok-term-former tok) tok E))
  (define (make-nary    tok Elist) (apply (tok-term-former tok)
                                          (cons tok Elist)))

  (define (in-or-postfix? tok)     (or (tok-infix? tok) (tok-postfix? tok)))

  (define (parse-expr outer-bp)
    (parse-continue (parse-head outer-bp) outer-bp))

  (define (parse-match open close)
    (let* ([result (parse-expr 0)] [tok (get-tok)])
      (if (equal? tok close) result (syn-err (format "Missing '~a'" close))) ))

  (define (parse-head outer-bp)
    (let ([tok (get-tok)])
      (cond
        [(tok-nullfix? tok) ((tok-term-former tok) tok)]
        [(tok-prefix? tok)  (make-prefix tok (parse-expr (rbp tok))) ]
        [(symbol? tok)      (make-leaf tok) ]
        [(equal?  tok #\( ) (parse-match #\( #\)) ]
        [(equal?  tok #\{ ) (parse-make-collect 'set (parse-match #\{ #\})) ]
        [else (syn-err "Unexpected token." tok) ] )))

  (define (parse-continue lhs outer-bp)
    (do ([peeked (peek-tok) (peek-tok)])
        [(or (not (in-or-postfix? peeked)) (< (lbp peeked) outer-bp))  lhs]
      (let ([op (get-tok)])
        (cond
          [(tok-postfix? op)
           (set! lhs (make-postfix op lhs))]
  
          [(tok-infix? op)
           (let* ([roperands (list lhs)]   ; acumulate [rhsn .. rhs2 rhs1 lhs]
                  [rbp-op   (rbp op)]
                  [lbp-op   (lbp op)]
                  [n-ary?   (= lbp-op rbp-op)]
                  [rhs1     (tighten-right (parse-head outer-bp) rbp-op)])
             (set! roperands (cons rhs1 roperands))
  
             (when n-ary?
               (do ([next (peek-tok) (peek-tok)])
                   [(not (equal? next op)) 'void]
                 (get-tok)  ; consume op
                 (let ([rhs-i (tighten-right (parse-head outer-bp) rbp-op)])
                   (set! roperands (cons rhs-i roperands)) ) ))
  
             ;; Build n-ary if more than one rhs.
             (let ([operands (reverse roperands)])
               (if (list-length>=? operands 3)
                 (set! lhs (make-nary  op operands))
                 (set! lhs (make-infix op (car operands) (cadr operands))) ))) ]
        ))))

  ;; Tighten rhs with anything with lbp > stop-bp, postfix or stronger infix.
  (define (tighten-right rhs stop-bp)
    (do ([next-tok (peek-tok) (peek-tok)])
        [(or (not (in-or-postfix? next-tok)) (<= (lbp next-tok) stop-bp))
         rhs]
      (cond
        [(tok-postfix? next-tok)
         (set! rhs (make-postfix (get-tok) rhs))]
        [(tok-infix? next-tok)
         (set! rhs (parse-continue rhs (lbp next-tok)))]) ))

  (with-global (*tok-props* tok-props) (parse-expr 0)) )

(define (parse-string s [error-handler '()]) 
  (call/cc (lambda (throw-syntax-error)
    (when (null? error-handler) (set! error-handler throw-syntax-error))
    (define (syn-error . args) (error-handler args))

    (define ts (tok-stream (inp (open-input-string s))))
    (parse-stream ts *tok-props* syn-error))))

;; Conversion to/from strings
(define (string->lf s)   (parse-string s error!))
(define (string->fd-ent s) (parse-string s error!))

(define (string->fd-subs s)
  (let ([r (parse-string s error!)])
    (if (and (pair? r) (eq-car? r 'comma)) (cdr r) (list r)) ))

(define (fd-subs->string s)
  (define (comma-if i s)
    (if (= i 0) s (string-append ", " s)))

  (define (fmt-list fmt ell)
    (apply string-append
      (map comma-if (ints-upto (length ell)) (map fmt ell)) ))

  (define (fmt-subs-result f)
    (if (and (pair? f) (eq-car? f 'set))
      (string-append "{" (fmt-list lf->logic-string (cdr f)) "}")
      (lf->logic-string f)))

  (define (fmt-pair p)
    (format "~a = ~a" (car p) (fmt-subs-result (cdr p))))

  (if (null? s)
    "-empty-"
    (fmt-list fmt-pair s) ))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Formatting
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (lf->sexpr-string lf)
  (let ((out (open-output-string)))
     (write lf out)
     (get-output-string out) ))


;; The *-tokens lists are used to find the tok-info for precedence.
(define logic-tokens 
  '( (#t . #\⊤) (#f . #\⊥) (forall . #\∀) (exists . #\∃)
   (not . #\¬) (and . #\∧) (or . #\∨) (nand . #\|) (nor . #\↓) (xor . #\⊕)
   (impl . #\→) (equiv . #\↔) (xnor . #\↔)) )

(define boolalg-tokens
  '((#t . 1) (#f . 0) (not . #\') (and . #\·) (or . #\+) (xor . #\⊕)) )

;; The *-string-table lists give the text to insert in string output.
(define logic-string-table
  '((#t . "⊤")      (#f . "⊥")    (lparen . "(")  (rparen . ")")
    (not "¬" . "")  (and . "∧")   (or  . "∨")
    (impl . "→")    (equiv . "↔")
    (nand . "|")    (nor . "↓")   (xor . "⊕")     (xnor . "↔")) )

(define boolalg-string-table
  '((#t . "1")     (#f . "0")
    (lparen . "(") (rparen . ")")
    (not "" . "'") (and . "·") (or . "+") (xor . "⊕")) )

;; The *-latex-table lists give the text to insert in latex output.
(define logic-latex-table
  '((#t . "\\top")           (#f . "\\perp")
    (lparen . "\\left (")    (rparen . "\\right )")
    (not  "\\neg " . "")
    (and . "\\land ")        (or  . "\\lor ")
    (impl . "\\rightarrow ") (equiv . "\\leftrightarrow ")
    (nand . "|")             (nor . "\\downarrow ")
    (xor . "\\oplus ")       (xnor . "\\leftrightarrow ")) )

(define boolalg-latex-table
  '((#t . "1")               (#f . "0")
    (lparen . "\\left (")    (rparen . "\\right )")
    (not "\\overline{" . "}")
    (and . "\\cdot ")        (or . "+") (xor . "\\oplus ")) )

;; Construct message to use if an operator is not allowed.
(define (lf-op-error op-sym)
    (format "Operator ~a not allowed." op-sym))

(define (lf->logic-string lf [throw-syntax-err '()])
  (lf->string-general lf logic-tokens logic-string-table throw-syntax-err))

(define (lf->boolalg-string lf [throw-syntax-err '()]) 
  (lf->string-general lf boolalg-tokens boolalg-string-table throw-syntax-err))

(define (lf->logic-latex lf [throw-syntax-err '()])
  (lf->string-general lf logic-tokens logic-latex-table throw-syntax-err))

(define (lf->boolalg-latex lf [throw-syntax-err '()])
  (lf->string-general lf boolalg-tokens boolalg-latex-table throw-syntax-err))



(define lf->string-general (lambda args (apply lf->string-general-new args)))

(define (lf->string-general-new lf op-tokens op-strings
         [force-parens-on-equal? #t] [throw-syntax-error '()] )
  (call/cc
    (lambda (throw)
      (unless (null? throw-syntax-error) (set! throw throw-syntax-error))

      ;; Utilities
      (define (char->str c) (if (char? c) (string c) (format "~a" c)))
      (define lparen (lookq 'lparen op-strings "(")) 
      (define rparen (lookq 'rparen op-strings ")"))
      (when (or (null? lparen) (null? rparen))
         (bug! "No parentheses in string table"))
 
      ;; Operator info: (tok kind lbp rbp) with type one of null/pre/in/postfix.
      (define (op-info lf)
        (let ([tok  (lookq (lf-op lf) op-tokens 'not-found)])
          (when (eq? tok 'not-found)
            (throw (format "Operator ~a not allowed." (lf-op lf))))
          (let ([bps  (tok-bps tok)])
            (list tok (tok-kind tok) (car bps) (cdr bps)) )))
 
      (define (op-tok  info) (car info))
      (define (op-kind info) (cadr info))
      (define (op-lbp  info) (caddr info))
      (define (op-rbp  info) (cadddr info))
 
      (define (op-string info)
        (let ([tok (tok-info-tok info)])
          (if (eq? (op-kind info) 'infix)
            (lookq tok op-strings "¿infix?")
            (lookq tok op-strings '("¿pre?" . "¿post?")) )))
 
      ;; Decide if child-no of parent needs to be parenthesized
      (define (parens-needed? parent child-no)
        (let ([child (lf-arg parent child-no)])
          (if (or (lf-const? child) (lf-atom? child))
            #f
            (let* ([p-info     (op-info parent)]
                   [p-kind     (op-kind p-info)]
                   [c-info     (op-info child)]
                   [p-op-on-L? (or (eq? p-kind 'prefix)
                                   (and (eq? p-kind 'infix) (> child-no 0)))]
                   [p-op-on-R? (or (eq? p-kind 'postfix)
                                   (and (eq? p-kind 'infix)
                                        (< child-no (- (lf-nargs parent) 1))))])
             (or (and p-op-on-L? (>= (op-rbp p-info) (op-lbp c-info)))
                 (and p-op-on-R? (>= (op-lbp p-info) (op-rbp c-info)))) ))))
 
      ;; Convert form to string using the helpers above.
      (define (emit lf)
        ;; Output as pieces in reverse order
        (define routput '())
        (define (put s) (set! routput (cons s routput)))
 
        (define (emit0-parens-if parens? lf) 
         (when parens? (put lparen)) (emit0 lf) (when parens? (put rparen)))
 
        (define (emit0 lf)
          (cond
            [(lf-const? lf) (put (lookq lf op-strings "¿const?"))]
            [(lf-atom?  lf) (put (format "~a" lf))]
            [else
              (let* ([opstrs (lookq (lf-op lf) op-strings "¿op?")]
                     [info   (op-info lf)]
                     [tok    (op-tok  info)]
                     [kind   (op-kind info)]
                     [nargs  (lf-nargs lf)])
                (if (or (eq? kind 'prefix) (eq? kind 'postfix))
                  (let* ([arg (lf-arg lf 0)] [parens? (parens-needed? lf 0)])
                    (let ([pre-post opstrs])
                      (put (car pre-post))
                      (emit0-parens-if parens? arg)
                      (put (cdr pre-post)) ))
          ;       (cond
          ;         [(= nargs 0)
          ;           (lf-op-simplified-nullary (lf-op-sym lf))]
          ;         [(= nargs 1) 
          ;           (lf-op-simplified-unary (lf-op-sym lf) (lf-arg lf 0))]
          ;         [else
          ;           (for ([a (lf-args lf)] [i (in-range (lf-nargs lf))])
          ;             (when (> i 0) (put opstrs))
          ;             (emit0-parens-if (parens-needed? lf i) a) )]) ) )] )
                  (if (< nargs 2)
                    (emit0 (if (= nargs 0)
                      (lf-op-simplified-nullary (lf-op-sym lf))
                      (lf-op-simplified-unary   (lf-op-sym lf) (lf-arg lf 0)) ))
                    (for ([a (lf-args lf)] [i (in-range (lf-nargs lf))])
                      (when (> i 0) (put opstrs))
                      (emit0-parens-if (parens-needed? lf i) a) )) ))] )
          routput)
 
        (apply string-append (reverse (emit0 lf)) ) )

      ;; Do output
      (emit lf) )))


(define (lf->string-general-old lf op-precs op-strings throw-syntax-error)
  (call/cc (lambda (throw)
    (unless (null? throw-syntax-error) (set! throw throw-syntax-error))

    (define (lf-atom->string atom) (symbol->string atom))

    (define (op-prec op) (lookq op op-precs 999))
    (define not-prec     (op-prec 'not))

    (define (op-str op)  (lookq op op-strings "?"))
    (define not-pre-str  (op-str 'not-pre))
    (define not-post-str (op-str 'not-post))
    (define lpren-str    (op-str 'lparen))
    (define rpren-str    (op-str 'rparen))


    (define (lf->strings-rev lf outer-op outer-prec so-far)
      (cond
        [(lf-const? lf) (cons (op-str lf) so-far)]
        [(lf-atom? lf)  (cons (lf-atom->string lf) so-far)]
        [(lf-not? lf)
          (cons not-post-str
                (lf->strings-rev (lf-arg lf 0) 'not not-prec
                                 (cons not-pre-str so-far)))]
        [else
          (let* ([this-op   (lf-op-sym lf)]
                 [this-prec (op-prec this-op)]
                 [this-str  (op-str  this-op)]
                 [is-assoc? (lf-is-associative-op? this-op)])

            (when (eqv? this-str "?") (throw (lf-op-error this-op)) )

            (if (< (lf-nargs lf) 2)
              (lf->strings-rev
                (if (= (lf-nargs lf) 0)
                  (lf-op-simplified-nullary (lf-op-sym lf))
                  (lf-op-simplified-unary   (lf-op-sym lf) (lf-arg lf 0)) )
                outer-op outer-prec so-far)

              ;; We have an n-ary (n>=2) infix op
              (let ([skip-paren? (or (> this-prec outer-prec)
                                     (and is-assoc? (eq? this-op outer-op)))])
                (unless skip-paren? (set! so-far (cons lpren-str so-far)))
                (do ((first #t #f) (args (lf-args lf) (cdr args)))
                  [(null? args)]
                  (unless first (set! so-far (cons this-str so-far)))
                  (set! so-far 
                        (lf->strings-rev (car args) this-op this-prec so-far)) )
                (unless skip-paren? (set! so-far (cons rpren-str so-far)))
                so-far ) ))] ))

  (apply string-append
         (reverse (lf->strings-rev lf 'top (op-prec 'top) '())) ) )))
   



(define (cnf->clause-set-string cnf) x)
(define (boolalg-string->lf s)   x)
(define (logic-string->lf s)  x)
(define (clause-set-string->cnf s)   x)


;;;
;;; Formatting truth tables: results are lists of strings
;;;
(define (truth-table->strings ->string tt)
  (call/cc (lambda (throw-syntax-error)
    (define (err msg) (throw-syntax-error (list msg)))
    (define (spaces n) (make-string n #\Space))
    (let* ([hdrs (map (lambda (h) (->string h err)) (tt-headers tt))]
           [rows (tt-rows tt)]
           [lens (map string-length hdrs)]
           [ret  '()])
      (set! ret (cons (apply string-append (map (curry format "~a ") hdrs))
        ret))
      (for ([row rows])
        (set! ret (cons (apply string-append
          (map (lambda (v len) (format "~a~a" (if v 1 0) (spaces len)))
               row
               lens))
          ret)))
      (reverse ret) )) ))

(define (truth-table->latex ->latex tt sep)
  (call/cc (lambda (throw-syntax-error)
    (define (err msg) (throw-syntax-error (list msg)))
    (define (make-row ell) (prepend-with-seps " & " ell '("\\\\")))

    (let* ([hdrs   (map (lambda (h) (->latex h err)) (tt-headers tt))]
           [rows   (tt-rows  tt)]
           [ncols  (tt-ncols tt)]
           [nsyms  (tt-nsyms tt)]
           [nforms (- ncols nsyms)]
           [cspecs (lambda (n) (make-string n #\c))]
           [ret    '()])
      (set! ret (cons 
        (format "\\begin{tabular}{~a~a~a}" (cspecs nsyms) sep (cspecs nforms))
        ret))
      (set! ret (cons
        (apply string-append (make-row (map (curry format "$~a$") hdrs)))
        ret))
      (set! ret (cons
        "\\hline" 
        ret))
      (for ([row rows])
        (set! ret (cons
          (apply string-append (make-row (map (lambda (v) (if v "1" "0")) row)))
          ret)) )
      (set! ret (cons
        "\\end{tabular}"
        ret))
      (reverse ret) )) ))

(define (display-logic-strings-truth-table-of-parts lf)
  (display-strings
    (truth-table->strings lf->logic-string (truth-table-of-parts lf))))

(define (display-boolalg-strings-truth-table-of-parts lf)
  (display-strings
    (truth-table->strings lf->boolalg-string (truth-table-of-parts lf))))

(define (display-logic-strings-truth-table-of-formulas syms formulas)
  (display-strings
    (truth-table->strings lf->logic-string
                        (truth-table-of-formulas syms formulas))))

(define (display-boolalg-strings-truth-table-of-formulas syms formulas)
  (display-strings
    (truth-table->strings lf->boolalg-string
                        (truth-table-of-formulas syms formulas))))

(define (display-logic-latex-truth-table-of-parts lf)
  (display-strings
    (truth-table->latex lf->logic-latex (truth-table-of-parts lf) "||")))

(define (display-boolalg-latex-truth-table-of-parts lf)
  (display-strings
    (truth-table->latex lf->boolalg-latex (truth-table-of-parts lf) "||")))

(define (display-logic-latex-truth-table-of-formulas syms formulas)
  (display-strings
    (truth-table->latex lf->logic-latex
                        (truth-table-of-formulas syms formulas)
                        "")))

(define (display-boolalg-latex-truth-table-of-formulas syms formulas)
  (display-strings
    (truth-table->latex lf->boolalg-latex
                        (truth-table-of-formulas syms formulas)
                        "")))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Formal Deduction
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;
;;; Structure for formal deduction theorem statements, e.g. ¬B,A → B ⊢ ¬A.
;;;
;;; premises      a list of formulas or set symbols
;;; conclusion    a formula
(define (fd-ent premises conclusion) 
  (list 'fd-ent premises conclusion))
(define (fd-ent? ob)            (eq-car? ob 'fd-ent))
(define (fd-ent-premises ent)   (cadr  ent))
(define (fd-ent-conclusion ent) (caddr ent))

;; Determine whether premise symbols are for sets or formulas
(define *fd-symbols-for-sets* 
  '(Σ Σ1 Σ2 Σ3 Σ4 Σ5 Σ6 Σ7 Σ8 Σ9
    Sigma Sigma1 Sigma2 Sigma3 Sigma4 Sigma5 Sigma6 Sigma7 Sigma8 Sigma9))

(define (fd-symbol-for-set? sym) (memq sym *fd-symbols-for-sets*))

(define (fd-count-formula-premises premises)
  (- (length premises) (fd-count-set-premises premises)))

(define (fd-count-set-premises premises)
  (list-count fd-symbol-for-set? premises))

;; Canonicalize a theorem by sorting the premises
(define (fd-ent-canon ent)
  (fd-ent
    (sort (fd-ent-premises ent) lf<?)
    (fd-ent-conclusion ent) ))

;; A predicate to order theorems.
(define (fd-ent<? a b)
  (let ([a-prems (fd-ent-premises a)] [a-conc (fd-ent-conclusion a)]
        [b-prems (fd-ent-premises b)] [b-conc (fd-ent-conclusion b)])

    (let ([a-len (length a-prems)] [b-len (length b-prems)])
      (cond
        [(< a-len b-len) #t]
        [(> a-len b-len) #f]
        [else
          (do ([apl a-prems (cdr apl)] [bpl b-prems (cdr bpl)]
               [result 'unknown])
            [(or (null? apl) (boolean? result))
              (if (boolean? result) result (lf<? a-conc b-conc))]
            (let ([cmp (lf-cmp (car apl) (car bpl))])
              (cond
                [(= cmp -1) (set! result #t)]
                [(= cmp  1) (set! result #f)])) )] ))))

;;;
;;; Structure for formal deduction rules, e.g. If Σ,A ⊢ B then Σ ⊢ A → B.
;;;
;;; name          a symbol, the name of the rule
;;; kind          a symbol, one of: axiom, theorem, ...
;;; requirements  a list of required fd-ents (possibly empty)
;;; result        an fd-ent, true when the requirements are satisfied.
(define (fd-rule name kind requirements result) 
  (list 'fd-rule name kind requirements result)) 
(define (fd-rule? ob)               (eq-car? ob 'fd-rule))
(define (fd-rule-name rule)         (list-ref rule 1))
(define (fd-rule-kind rule)         (list-ref rule 2))
(define (fd-rule-requirements rule) (list-ref rule 3))
(define (fd-rule-result rule)       (list-ref rule 4))

(define (mk-fd-rule name kind requirement-string-list result-string)
  (let ([reqs (map string->fd-ent requirement-string-list)]
        [result (string->fd-ent result-string)])
    (fd-rule name kind reqs result)))

(define (mk-fd-axiom name requirement-string-list result-string)
  (mk-fd-rule name 'axiom requirement-string-list result-string))

(define (mk-fd-theorem name requirement-string-list result-string)
  (mk-fd-rule name 'theorem requirement-string-list result-string))

;;;
;;; Justifications
;;;
(define (fd-just rule-name step-names) (cons rule-name step-names))
(define (fd-just-rule-name  just) (car just))
(define (fd-just-step-names just) (cdr just))

;;;
;;; Proof step, e.g. Step7:  ¬B,A → B ⊢ ¬A  by (→ −, Step1, Step2).
;;;
(define (fd-step name entailment justifiction [subs 'auto])
  (list 'fd-step name entailment justifiction subs))

(define (mk-fd-step name entailment justification [subs 'auto])
  (when (neq? subs 'auto) (set! subs (string->fd-subs subs)))
  (fd-step name (string->fd-ent entailment) justification subs))

(define (fd-step? ob)                (eq-car? ob 'fd-step))
(define (fd-step-name rule)          (list-ref rule 1))
(define (fd-step-entailment rule)    (list-ref rule 2))
(define (fd-step-justification rule) (list-ref rule 3))
(define (fd-step-subs rule)          (list-ref rule 4))

;;;
;;; Proof object -- contains a list of steps.
;;;
(define (fd-proof step-list)   (cons 'fd-proof step-list))
(define (fd-proof? ob)         (eq-car? ob 'fd-proof))
(define (fd-proof-steps proof) (cdr proof))
(define (mk-fd-proof fancy-step-list)
  (fd-proof (map (lambda (fs) (apply mk-fd-step fs)) fancy-step-list)) )

;;
;; Find an object in a list, where the objects are of the form (x name x ...).
;; Applicable to fd-rules and fd-steps.
;;
(define (fd-find-by-name name ell)
  (cond [(null? ell) #f]
        [(eq? (cadar ell) name) (car ell)]
        [else (fd-find-by-name name (cdr ell))]))

;;;
;;; Expression symbols
;;;

;; Get all the non-special symbols in an expression
(define (fd-get-symbols syn-words expr) 
  (define (get-syms E syms)
    (cond
      [(symbol? E) (lset-union1 E syms)]
      [(pair? E)   (for ([e E]) (set! syms (get-syms e syms))) syms]
      [else        syms]))
  (lset-minus (get-syms expr (lset-empty)) syn-words) )

;;;
;;; Substitutions
;;;

;; Make a substitution for the symbols by gensyms.
(define (fd-gen-subs syn-words expr)
  (let* ([syms (fd-get-symbols syn-words expr)]
         [gens (map (lambda (x) (gensym)) syms)]
         [subs (map cons syms gens)])
    subs))

;; Invert a substitution
(define (fd-inverse-subs subs)
  (map (lambda (s) (cons (cdr s) (car s))) subs) )

;; Apply a substitution
(define (fd-apply-subs subs expr)
  (define (apply-it E) 
    (cond
      [(null? E) '()]
      [(symbol? E)
        (let ([r (assq E subs)]) (if (pair? r) (cdr r) E)) ]
      [(fd-rule? E)
        (fd-rule (fd-rule-name E) (fd-rule-kind E)
          (apply-it (fd-rule-requirements E))
          (apply-it (fd-rule-result E)))]
      [(fd-ent? E)
        (fd-ent
          ; The substitution might have given A -> (set X Y Z) so flatten.
          (fd-flatten-list (apply-it (fd-ent-premises E)) 'set)
          (apply-it (fd-ent-conclusion E)))]
      ; This needs to come after all the other type tests, in case they
      ; are implemented using pairs.
      ; TODO -- map should work here, but we somehow get dotted pairs.
      [(pair? E) (cons (apply-it (car E)) (apply-it (cdr E)))]
      [else E]))
  (apply-it expr) )

;; (A B (op C D) E (op) (op F)) -> (A B C D E F)
(define (fd-flatten-list ell op)
  (define (is-op? E) (and (pair? E) (eq-car? E op)))
  (define (rev-flatten E r)
     (if (null? E)
       r
       (let ([Hd (car E)] [Tl (cdr E)])
         (rev-flatten Tl
           (if (is-op? Hd) (rev-flatten (cdr Hd) r) (cons Hd r)) )) )) 
  (reverse (rev-flatten ell '())))

;; Return a substitution or #f if cannot match.
;;
;; Example 1:
;;   (fd-match '(and or) '(and A B) '(and (or A B) C))
;;   -> '((A . (and A B)) (B . C))
;; Example 2:
;;   (fd-match '(and or) '(and (or A B) '(or A C)) '(and (or X Y) (or X Z)))
;;   -> '((A . X) (B . Y) (C . Z))
;; Example 3:
;;   (fd-match '(and or) '(and A B) '(or (and A B) C))
;;   -> #f
;; Example 4:
;;   (fd-match '(and or) '(and (or A B) '(or A C)) '(and (or X Y) (or W Z)))
;;   -> #f
(define (fd-match syn-words pattern candidate)
  (call/cc (lambda (return)
    (define subs '())
    (define (match-part pat cand)
      (cond
        [(pair? pat)
         (if (or (not (pair? cand)) (<> (length pat) (length cand)))
           (return #f)
           (map match-part pat cand))]

        [(symbol? pat)
         (if (and (memq pat syn-words))
           (when (nequal? pat cand) (return #f))
           (let ([pp (assq pat subs)])
             (if (pair? pp)
               (when (nequal? (cdr pp) cand) (return #f))
               (set! subs (cons (cons pat cand) subs)))) )] ))
    (match-part pattern candidate)
    subs) ))

(define *fd-do-subs* #f)
(define *fd-keywords* '(fd-ent not and or xor nand nor xnor impl equiv))

;; If the client has not given a substitution to make the inference rule
;; of the justification match the cited steps, then we find all that apply.
;; It is good to find exactly one.  Zero or several are not good!
;;
;; To do this, we work with the following quantities:
;; * The justifiction of the step, step-just.
;; * The inference rule of the justification, just-rule.
;;
;; * The requirements for the inference rule to be applied, rule-reqs.
;; * The result of applying the inference rule, rule-result.
;;
;; * The theorems of the steps cited by the justifiction (which supposedly
;;     satisfy the requirements of the rule), step-reqs.
;; * The claimed theorem of the step, step-result.
;;
;; Before doing anything, the step-reqs and step-result are given fresh symbols
;; so nothing will conflict with what is in the rule.
;;
;; A match is a substitution for symbols in the rule-reqs and rule-result
;; such that when
;; - the substitution is applied to the rule-reqs and rule-result, and
;; - the substituted theorems have their premises "exploded" and sorted
;; - the substituted, exploded, sorted reqs and result are syntactically
;;   equal to the step reqs and result.
;;
;; "exploded" means that all (set ...) are appended into the containing list,
;; e.g.  '((set A B) C (and D E)) --> (A B C (and D E))

(define (fd-find-inference-match step rules prev-steps
                                 #:verbose? [verbose? #f]) 
  (call/cc (lambda (return)

  (let* ([step-just   (fd-step-justification step)]
         [just-rule   (or (fd-find-by-name (fd-just-rule-name step-just) rules)
                          (return #f))]

         ;; Get the requirements and result of the rule
         [rule-name   (fd-rule-name         just-rule)]
         [rule-kind   (fd-rule-kind         just-rule)]
         [rule-reqs   (fd-rule-requirements just-rule)]
         [rule-result (fd-rule-result       just-rule)]

         ;; Get what is supplied for the requirements, and the step result.
         [step-reqs
           (map (lambda (name) (fd-step-entailment
                  (or (fd-find-by-name name prev-steps) (return #f))))
                (fd-just-step-names step-just) )]
         [step-result (fd-step-entailment step)]

         ;; Make a substitution to put fresh variables in the step so they
         ;; won't conflicth with what is in the rule.
         [freshen-subs (if (not *fd-do-subs*) '()
           (fd-gen-subs *fd-keywords* (cons step-result step-reqs)))]

         [step-sreqs   (fd-apply-subs freshen-subs step-reqs)]
         [step-sresult (fd-apply-subs freshen-subs step-result)]
         [step-rule    (fd-rule rule-name rule-kind step-sreqs step-sresult)]

         [trace-me? (equal? step-just '(impl- 1 2))]

         [matches (apply append (map
            (lambda (step-rule-i)
              (fd-rule-premise-permutations step-rule-i just-rule))
            (fd-rule-requirement-permutations step-rule)))]

         [nmatches (length matches)])

    (when (= nmatches 0) (return #f))
    (when (> nmatches 1) (warning "More than one match for justification."))

    (car matches) ))))

;; Given a rule, return a list of rules with requirement permutations.
(define (fd-rule-requirement-permutations rule)
  (let ([name   (fd-rule-name rule)]
        [kind   (fd-rule-kind rule)]
        [reqs   (fd-rule-requirements rule)]
        [result (fd-rule-result rule)])
    (let ([perms  (permutations (ints-upto (length reqs)))])
      (map (lambda (p) (fd-rule name kind (list-multi-ref reqs p) result))
           perms) )))

;; Given a rule, return a list of substitutions for all applicable orders of 
;; premises for the required theorems and result theorem.
;;
;; We say "applicable" orders here because some of the premises may be
;; grouped together in a "(set ...)".  Whether this is so, and which argument
;; it pertains, is determined by the pattern-rule argument.
;;
;; Inputs are a candidate rule and a pattern rule to match.
(define (fd-rule-premise-permutations cand-rule pat-rule)
  (let* ([name          (fd-rule-name cand-rule)]
         [kind          (fd-rule-kind cand-rule)]  
         [cand-ents     (cons (fd-rule-result cand-rule)
                              (fd-rule-requirements cand-rule))]
         [pat-ents      (cons (fd-rule-result pat-rule)
                              (fd-rule-requirements pat-rule))]
         [perms-each    (map fd-ent-premise-permutations
                             cand-ents pat-ents)]
         [combos        (all-combos perms-each)]
         [maybe-matches (map (lambda (c) (fd-match *fd-keywords* pat-ents c))
                             combos)])
    (filter identity-fn maybe-matches) ))

;; Make a list of theorems with all permutations matching a pattern.
;; The pattern is a theorem with some premises (possibly 0) being formulas and
;; some (for now 0 or 1) being sets.  Sets in the pattern theorem are matched
;; to sorted sets of formulas, represented as "(set ...)", in the result.
;;
;; TODO:  We can limit permutations to ones where the formulas match structure.
;; TODO:  Allow more than one symbol representing a set.
(define (fd-ent-premise-permutations cand-entailment pat-entailment)
  ;; If any cand-rule premise represents a set, give the index of the first.
  ;; If there are none, return -1.
  ;; [Current limitation: we accept at most one symbol representing a set.]
  (define set-sym-index
    (let ([prems (fd-ent-premises pat-entailment)] [index -1])
      (for ([i (in-naturals)] [p prems])
        (when (fd-symbol-for-set? p) 
          (when (<> index -1)
            (error! "Can have at most one set symbol like Σ in premises."))
          (set! index i)))
      index) )

  (define count-pat-formulas
    (fd-count-formula-premises (fd-ent-premises pat-entailment)))

  (define (make-entailment premises conclusion)
    (let ([n-premises (length premises)])
      (cond
        [(< n-premises count-pat-formulas) #f]
        [(and (= n-premises count-pat-formulas) (= set-sym-index -1))
            (fd-ent premises conclusion) ]
        [else
          (if (= set-sym-index -1)
            #f
            (let ([p-before (take premises set-sym-index)]
                  [p-after  (take (drop premises set-sym-index)
                                  (- count-pat-formulas set-sym-index) )]
                  [p-in-set (drop premises count-pat-formulas)])
              (fd-ent (append p-before (list (cons 'set p-in-set)) p-after)
                          conclusion) )) ] )))

  ;; Permute from the candidate the number of formulas in the pattern.
  (let ([premises   (fd-ent-premises cand-entailment)]
        [conclusion (fd-ent-conclusion cand-entailment)])
    (filter identity-fn
      (map (lambda (p) (make-entailment (list-multi-ref premises p) conclusion))
           (permutations (ints-upto (length premises)) count-pat-formulas))) ))


;; Returns list of (ent-permut'n substitution) lists.
;; List may be emtpy.
(define (fd-find-inference-matches
           rule-inputs rule-output inst-inputs inst-output
         [trace-me? #f])
  (when trace-me?
    (printf "Rule inputs: ~a~n" rule-inputs)
    (printf "Rule output: ~a~n" rule-output)
    (printf "Inst inputs: ~a~n" inst-inputs)
    (printf "Inst output: ~a~n" inst-output))

  ;; Try all orders of instance inputs against rule inputs
  (let* ([matches '()]
         [input-permutations (permutations (ints-upto (length inst-inputs)))]
         [subs-so-far '()])
    (when trace-me?
      (printf "*** inst-inputs permutations: ***~n"))
    (for ([i (in-naturals)] [p input-permutations])
      (let ([inst-inputs-permuted (list-multi-ref inst-inputs p)])
        (when trace-me?
          (printf "~n>> ~a. Justification Permutation: ~a ~a~n"
            i p inst-inputs-permuted))
        (let ([new-ms (fd-find-entailment-match-all-premise-orders
                           rule-inputs rule-output
                           inst-inputs-permuted inst-output
                           subs-so-far)])
           (set! matches (append (map (curry cons p) new-ms) matches)) ) ))
    (when trace-me?
      (printf "*** Matches: ***~n")
      (for ([i (in-naturals)] [m matches])
        (printf "~a. ~a~n" i m) ))

     matches))

;; Returns list of (premise-permut'n substitution) lists pairs.
;; List may be emtpy.
(define (fd-find-entailment-match-all-premise-orders
           rule-inputs rule-output inst-inputs-permuted inst-output
           subs-so-far)
(printf "match theorem~n")
(printf "  In:   ~a~n  Out:  ~a~n  ::~n" rule-inputs rule-output)
(printf "  IIn:  ~a~n  IOut: ~a~n  /~n" inst-inputs-permuted inst-output)
(printf "  Subs: ~a~n" subs-so-far)
  
  ;; Make a list of premises in all the possible orders.
  (define (prep-premise-list prems n-formulas)
    (append (take prems n-formulas)
            (list (cons 'set (sort (drop prems n-formulas) lf<?)))))

  ;; Make list of inferences with premises in all possible orders.
  ;; I.e. list of (fd-rule requirement-list conclusion)
  (let* ([premises-of-inst-inputs
           (map fd-ent-premises inst-inputs-permuted)]
         [conclusions-of-inst-inputs
           (map fd-ent-conclusion inst-inputs-permuted)]
         [premises-of-rule-inputs (map fd-ent-premises rule-inputs)]
         [n-formula-of-each   
           (map fd-count-formula-premises premises-of-rule-inputs)]
         [permutations-of-each
           (map permutations premises-of-inst-inputs n-formula-of-each)])
    (for ([i     (in-naturals)]
          [nform n-formula-of-each]
          [plist premises-of-inst-inputs]
          [peach permutations-of-each]
          [c conclusions-of-inst-inputs])
(printf "~a. Premise list [~a] ~a~n" i nform plist) 
(printf "~   Conclusion: ~a~n" c)
(printf "~   Permutations:~n")
      (for ([j (in-naturals)] [p peach])
(printf "      <~a> ~a~n" j (fd-ent (prep-premise-list p nform) c))
        '(set! matches (cons (list 'yahoo i j) matches))
))
(printf "  Permutations of each: ~a~n" permutations-of-each)
      permutations-of-each))
         

;;; To verify a proof step,
;;; * the fd-rule is looked up 
;;; * the substitution is applied to it
;;; * the requirements and result parts of the fd-rule are checked to match
;;;   the theorems of the steps referred to (by name) in the justification.

(define (fd-check-step step rules prev-steps #:verbose? [verbose? #f]) 

  (define (find-step name) (fd-find-by-name name prev-steps))

  (when verbose? (printf "Checking step ~a: " (fd-step-name step)))

  (define ok? (call/cc (lambda (return)
    (let* ([st-ent    (fd-step-entailment step)]
           [st-subs   (fd-step-subs    step)]
           [st-just   (fd-step-justification step)]
           [just-rule (fd-find-by-name (fd-just-rule-name st-just) rules)]
           [just-args (map find-step (fd-just-step-names st-just))])

      ;; Need to have found the named rule and the justification arguments.
      (unless just-rule (return #f))
      (when (member? #f just-args) (return #f))

      ;; Take given substitution or try to find one.
      (if (neq? st-subs 'auto)
        (when verbose?
          (printf "Subst given. "))
        (let ([found-subs (fd-find-inference-match step rules prev-steps)])
          (when verbose? 
            (if found-subs
              (printf "Subst found ~a. " (fd-subs->string found-subs))
              (printf "No substitution works. ")))
          (if found-subs
            (set! st-subs found-subs)
            (return #f))))

      ;; Apply the substitution to the rule and see if it matches the step.
      (let* ([just-ents   (map fd-step-entailment   just-args)]
             [subs-rule   (fd-apply-subs st-subs just-rule)]
             [subs-reqs   (fd-rule-requirements  subs-rule)]
             [subs-result (fd-rule-result        subs-rule)])
        (cond
            [(not (fd-ent-list-match? subs-reqs just-ents))
              #f] ; req not met
            [(not (fd-ent-match? subs-result st-ent))
              #f] ; ent not obtained
            [else
              #t]) )))))
  (when verbose? (printf (if ok? "OK~n" "Failed~n")))
  ok?)

(define (fd-check-proof rules proof #:verbose? [verbose? #f])
  (let ([steps (fd-proof-steps proof)] [proven-steps '()] [ok? #t])
    (for ([step steps] #:break (not ok?))
      (set! ok?
        (fd-check-step step rules proven-steps #:verbose? verbose?))
      (if ok?
        (set! proven-steps (cons step proven-steps))
        (printf "Proof fails at step ~a.~n" (fd-step-name step)) ))
    (when verbose?
      (if ok? (printf "Proof OK!~n") (printf "Proof failed.~n")))
    ok? ))

(define (fd-ent-list-match? pat-list cand-list)
  (let ([pat-sort  (sort (map fd-ent-canon pat-list)  fd-ent<?)]
        [cand-sort (sort (map fd-ent-canon cand-list) fd-ent<?)])
    (equal? pat-sort cand-sort) ))

(define (fd-ent-match? lhs rhs)
  (equal? (fd-ent-canon lhs) (fd-ent-canon rhs)))


;;; When does a proven theorem satisfy the required theorem of a rule?
;;; E.g. When does a fd-ent from step 7 justify using an axiom in step 8?
;;;
;;; Method:
;;; * The formula-symbols (e.g. A, B) in the required theorem are
;;;   substituted with formulas or sub-formulas of the proven theorem.
;;; * Set-of-formula symbols (e.g. Σ, Σ1) in the required theorem are
;;;   substituted with sets of formulas in the premises of the proven theorem.
;;;   The premise list in the substituted required theorem is flattened.
;;; * The conclusions of the substituted required and proven theorems must 
;;;   be syntacitcally equal.
;;; * The sorted list of premises of the proven theorem must be syntactically
;;;   equal to the sorted premise list of the substituted required theorem.  
;;;   Notes:
;;;   -- Comparison is made after the substitution is applied.
;;;   -- Any total order on the set of formulas may be used.
;;;   -- Syntactic equality of lists means syntactic equality at each position.

(define (fd-match-entailment? lhs rhs)
  (let ([lhs-prems (sort (fd-premises lhs) lf<?)]
        [rhs-prems (sort (fd-premises rhs) lf<?)]
        [lhs-concl (fd-conclusion lhs)]
        [rhs-concl (fd-conclusion rhs)])
    (and (equal? lhs-concl rhs-concl)
         (for/and ([lp lhs-prems] [rp rhs-prems]) (equal? lp rp))) ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Formal Deduction Axioms
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define ax-ref     (mk-fd-axiom 'Ref      (list)                    "A⊢A"    ))
(define ax-+       (mk-fd-axiom '+        (list "Σ⊢A")              "Σ,B⊢A"  ))
(define ax-not-    (mk-fd-axiom 'not-     (list "Σ,¬A⊢B" "Σ,¬A⊢¬B") "Σ⊢A"    ))
(define ax-impl-   (mk-fd-axiom 'impl-    (list "Σ⊢A→B" "Σ⊢A")      "Σ⊢B"    ))
(define ax-impl+   (mk-fd-axiom 'impl+    (list "Σ,A⊢B")            "Σ⊢A→B"  ))
(define ax-and.L-  (mk-fd-axiom 'and.L-   (list "Σ⊢A∧B")            "Σ⊢A"    ))
(define ax-and.R-  (mk-fd-axiom 'and.R-   (list "Σ⊢A∧B")            "Σ⊢B"    ))
(define ax-and+    (mk-fd-axiom 'and+     (list "Σ⊢A" "Σ⊢B")        "Σ⊢A∧B"  ))
(define ax-or-     (mk-fd-axiom 'or-      (list "Σ,A⊢C" "Σ,B⊢C")    "Σ,A∨B⊢C"))
(define ax-or.L+   (mk-fd-axiom 'or.L+    (list "Σ⊢A")              "Σ⊢B∨A"  ))
(define ax-or.R+   (mk-fd-axiom 'or.R+    (list "Σ⊢A")              "Σ⊢A∨B"  ))
(define ax-equiv.L-(mk-fd-axiom 'equiv.L- (list "Σ,A↔B⊢A" "Σ⊢B")    "Σ⊢A"    ))
(define ax-equiv.R-(mk-fd-axiom 'equiv.R- (list "Σ,A↔B⊢B" "Σ⊢A")    "Σ⊢B"    ))
(define ax-equiv+  (mk-fd-axiom 'equiv+   (list "Σ,A⊢B" "Σ,B⊢A")    "Σ⊢A↔B"  ))

(define th-mem     (mk-fd-theorem 'mem    (list)                    "Σ,A⊢A"  ))
(define th-not+    (mk-fd-theorem 'not+   (list  "Σ,A⊢B" "Σ,A⊢ ¬B") "Σ⊢ ¬A"  ))

(define th-notnot-        (mk-fd-theorem 'notnot-        '() "¬ ¬A⊢A"         ))
(define th-and.assoc      (mk-fd-theorem 'and.assoc      '() "(A∧B)∧C⊢A∧(B∧C)"))
(define th-or.assoc       (mk-fd-theorem 'or.assoc       '() "(A∨B)∨C⊢A∨(B∨C)"))
(define th-demorgan.Aup   (mk-fd-theorem 'demorgan.Aup   '() "¬(A∧B) ⊢ ¬A∨¬B" ))
(define th-demorgan.Oup   (mk-fd-theorem 'demorgan.Oup   '() "¬(A∨B) ⊢ ¬A∧¬B" ))
(define th-demorgan.Adown (mk-fd-theorem 'demorgan.Adown '() "¬A∧¬B ⊢ ¬(A∨B)" ))
(define th-demorgan.Odown (mk-fd-theorem 'demorgan.Odown '() "¬A∨¬B ⊢ ¬(A∧B)" ))

(define axioms-Lp (list
  ax-ref ax-+ ax-not-
  ax-impl- ax-impl+
  ax-and.L- ax-and.R- ax-and+
  ax-or- ax-or.L+ ax-or.R+
  ax-equiv.L- ax-equiv.R- ax-equiv+))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Random formulas
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Select a random element from a list.
(define (lf-random-element ell) (list-ref ell (random (length ell))) )

;; Compute arity in [usual-min..usual-max] unless otherwise indicated.
(define *lf-random-arity-usual-min* 2)
(define *lf-random-arity-usual-max* 4)

(define (lf-random-arity op-sym alt-min-arity alt-max-arity)
  (cond
    [(eq? op-sym 'not)    1]
    [(eq? op-sym 'exists) 1]
    [(eq? op-sym 'forall) 1]
    [(eq? op-sym 'impl)   2]
    [(eq? op-sym 'equiv)  2]
    [else 
      (let ([m (max *lf-random-arity-usual-min* alt-min-arity)]
            [M (min *lf-random-arity-usual-max* alt-max-arity)]) 
        ; random integer in [m..M]
        (+ m (random (+ (- M m) 1))) ) ]))
        
;; Compute a random partion of N into k parts, each at least m.
(define (lf-random-partition N k m)
  (when (< N (* k m)) (error! "N = ~a is too small for random partition." N))
  (let ([v (make-vector k m)])
    (do ([n-left (- N (* k m)) (- n-left 1)])
         [(= n-left 0) v]
      (let ([i (random k)])
        (vector-set! v i (+ (vector-ref v i) 1)) ) ) ) )

(define (lf-random op-list atom-list n-nodes)
  (define op0-ok-list
    (lset-intersect op-list '(and or xor nand nor xnor)))
  (define op1-ok-list
    (lset-intersect op-list '(not and or xor nand nor xnor)))
  (define op2-ok-list
    (lset-intersect op-list '(not and or xor nand nor xnor impl equiv)))
    
  (define (random-inner n-nodes)
    (cond
      [(= n-nodes 1) (lf-random-element atom-list) ]
      [(= n-nodes 2) (lf-formula (lf-random-element op1-ok-list)
                                 (lf-random-element atom-list)   )]
      [else
        ; One node is taken by the operator.
        ; Take a random arity and partition node budget among the arguments.
        (let* ([nodes-left (- n-nodes 1)]
               [op         (lf-random-element op-list)]
               [arity      (lf-random-arity op 2 nodes-left)]
               [partition  (lf-random-partition nodes-left arity 1)])
          (do ([i 0 (+ 1 i)] [args '()])
            [(= i arity) (lf-apply op args) ]
            (set! args
              (cons (random-inner (vector-ref partition i)) args) ) ))] ))

  (when (<= n-nodes 0) (bug! "lf-random of zero nodes."))
  (random-inner n-nodes) )


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Testing utilities
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define grand-error-count 0)

;; Test whether (apply fn Flist) equals G. Returns number of errors.
(define (test-one fn Flist G)
  (let* ([fnF (apply fn Flist)] [ok? (equal? fnF G)])
    (unless ok?
       (pretty-print Flist)
       (printf "-->~n  *** WRONG ***~n  got~n")
       (pretty-print fnF)
       (printf " not ~n") 
       (pretty-print G)
       (printf " for ~n")
       (pretty-print Flist)
       (printf "  *************~n") )
    (if ok? 0 1) ))

;; Test for each pair whether fn of car equals cdr.  Returns number of errors.
(define (test-list title fn pairs)
  (printf "-- ~a --~n" title)
  (foldl (lambda (pr n) (+ n (test-one fn (car pr) (cdr pr)))) 0 pairs) )


(define (test-all)
  (printf "== Hand-made tests ==~n")
  (define error-count (+
    (test-list "Formula?" lf-formula? '(
        ([a]                          . #t)
        ([(and a b)]                  . #t)
        ([(and a b (or c d))]         . #t)
        ([(or a (equiv a b))]         . #t)
        ([(or a (equiv a b c))]       . #f)
        ([(impl hello #t)]            . #t)
        ([(or ((exists y) (and y (not y))) (and y))] . #t)
        ([(or ((forall y) (and y (not y))) (and y))] . #t)
        ([(or ((forall (not y)) (and y (not x))) (and z))] . #f)
    ))
    (test-list "Is Assoc?" lf-is-associative? '(
        ([(and  a b)]  . #t)
        ([(or   a b)]  . #t)
        ([(xor  a b)]  . #t)
        ([(nand a b)]  . #f)
        ([(nor  a b)]  . #f)
        ([(xnor a b)]  . #t)

        ([(impl  a b)] . #f)
        ([(equiv a b)] . #f)
        ([(not   a)]   . #f)
        ([a]           . #f)
    ))
    (test-list "Not/and/or only" lf-not/and/or-only '(
        ([a]                  . a)
        ([(and a b)]          . (and a b))
        ([(and a b (or c d))] . (and a b (or c d)))
        ([(or a (equiv a b))] . (or a (or (and a b) (and (not a) (not b)))))
        ([(impl hello (and))] . (or (not hello) (and)))
    ))
    (test-list "Push nots down" lf-push-nots-down '(
        ([a]                            . a)
        ([(and a b)]                    . (and a b))
        ([(and a b (or c d))]           . (and a  b (or c d)))
        ([(not (or a (not (and a b))))] . (and (not a) (and a b)))
        ([(not (or (not a) (not (and a b))))]
        .  (and a (and a b)) )
        ([(not ((exists y) (and y (not y))))]
        .  ((forall y) (or (not y) y)))
        ([(not (or (not ((forall y) (and y (not y)))) (and y)))]
        .  (and ((forall y) (and y (not y))) (or (not y))) )
        ([(or (and (not ((forall y) (or y (not x))))) (and z))]
        .  (or (and ((exists y) (and (not y) x))) (and z)) )
    ))
    (test-list "Assoc nary" lf-assoc-nary '(
        ([(or (and a (and b) (and) c) (or x y z) (impl u v) (or (or w)))]
        .  (or (and a b c) x y z (impl u v) w) )
        ([(or (or a (or b c) (or) (or (or d) (or e f))))]
        .  (or a b c d e f) )
    ))
    (test-list "Assoc left" (curry lf-rule-assoc-left  'or) '(
        ([(or a b c d)] . (or (or (or a b) c) d))
        ([(or a)]       . a)
        ([(or)]         . (or))
    ))
    (test-list "Assoc right" (curry lf-rule-assoc-right  'or) '(
        ([(or a b c d)] . (or a (or b (or c d))))
        ([(or a)]       . a)
        ([(or)]         . (or))
    ))
    (test-list "DNF" lf-dnf '(
        ([a]                        . (or (and a)))
        ([(not a)]                  . (or (and (not a))))
        ([(and a)]                  . (or (and a)))
        ([(or (and a))]             . (or (and a)))
        ([(or)]                     . (or))
        ([(and)]                    . (or (and)))
        ([(and (or a))]             . (or (and a)))
        ([(or a b)]                 . (or (and a) (and b)))
        ([(or a b c)]               . (or (and a) (and b) (and c)))
        ([(and a b)]                . (or (and a b)))
        ([(or (and a b) (and c d))] . (or (and a b) (and c d)))
        ([(or a (and b c))]         . (or (and a) (and b c)))
        ([(or a (and b c) d)]       . (or (and a) (and b c) (and d)))
        ([(and (or a b) c)]         . (or (and a c) (and b c)))
        ([(and a (or b c))]         . (or (and a b) (and a c)))
        ([(and (or a b) (or c d))]
        . (or (and a c) (and a d) (and b c) (and b d)) )
        ([(or (and a (or b c)) (and d e) a)]
        . (or (and a b) (and a c) (and d e) (and a)) )
        ([(or (and a (and b) (and) c)
              (impl (or (not x) (not y) z) (impl u v))
              (or (or w)) )]
        . (or (and a b c) (and x y (not z)) (and (not u)) (and v) (and w)) )
    ))
    (test-list "CNF" lf-cnf '(
        ([a]                        . (and (or a)))
        ([(not a)]                  . (and (or (not a))))
        ([(and a)]                  . (and (or a)))
        ([(or (and a))]             . (and (or a)))
        ([(or)]                     . (and (or)))
        ([(and)]                    . (and))
        ([(and (or a))]             . (and (or a)))
        ([(or a b)]                 . (and (or a b)))
        ([(or a b c)]               . (and (or a b c)))
        ([(and a b)]                . (and (or a) (or b)))
        ([(or (and a b) (and c d))] . (and (or a c) (or a d) (or b c) (or b d)))
        ([(or a (and b c))]         . (and (or a b) (or a c)))
        ([(or a (and b c) d)]       . (and (or a b d) (or a c d)))
        ([(and (or a b) c)]         . (and (or a b) (or c)))
        ([(and a (or b c))]         . (and (or a) (or b c)))
        ([(and (or a b) (or c d))]  . (and (or a b) (or c d)))
        ([(or (and a (or b c)) (and d e) a)]
        . (and (or a d a) (or a e a) (or b c d a) (or b c e a)) )
        ([(or (and a (and b) (and) c)
              (impl (or (not x) (not y) z) (impl u v))
              (or (or w)) )]
        . (and (or a x (not u) v w)
               (or a y (not u) v w)
               (or a (not z) (not u) v w) 
               (or b x (not u) v w) 
               (or b y (not u) v w) 
               (or b (not z) (not u) v w) 
               (or c x (not u) v w) 
               (or c y (not u) v w) 
               (or c (not z) (not u) v w) ) )
    ))
    (test-list "List sets"  list->lset '(
        ([()]                . ())
        ([(a)]               . (a))
        ([(a b)]             . (a b))
        ([(a b a)]           . (a b))
        ([(b a a)]           . (b a))
        ([(a a b)]           . (a b))
        ([(a l p h a b e t)] . (a l p h b e t))
    ))
    (test-list "List union" lset-union '(
        ([(a b c) (d e f)]   .  (a b c d e f))
        ([() (a b)]          .  (a b))
        ([(a b) ()]          .  (a b))
        ([(a b) (a c)]       .  (b a c))
    ))
    (test-list "List intersect" lset-intersect '(
        ([(a b c) (d e f)]             .  ())
        ([() (a b)]                    .  ())
        ([(a b) ()]                    .  ())
        ([(a b) (a c)]                 .  (a))
        ([(x a b) (b a c d) (b)]       .  (b))
        ([(b x a y) (a l p h a b e t)] .  (a b))
        ([(r x u y) (a l p h a b e t)] .  ())
    ))
    (test-list "List subset" lset-subset? '(
        ([() (a b)]      . #t)
        ([(a) (a b)]     . #t)
        ([(b) (a b)]     . #t)
        ([(a b) (a b)]   . #t)
        ([(c) (a b)]     . #f)
        ([(a b c) (a b)] . #f)
        ([(d e) (a b)]   . #f)
    ))
    (test-list "Order" lf<? '(
        ([a (and a b)]   . #t)
        ([(and a b) a]   . #f)
        ([a b]           . #t)
        ([a a]           . #f)
        ([b a]           . #f)
        ([(and (not a)) (and (not b))] . #t)
        ([(and (not b)) (and (not a))] . #f)
    ))
    (test-list "Sort" 
      (lambda (ell) (sort ell lf<?))
      '(([((and (not b)) b (and (not a)) a)] . 
          (a b (and (not a)) (and (not b))) )
    ))
    (test-list "LF xarg span" lf-xarg-span '(
        ([(and a b (or c (and s t u v w) (not y)) d)   ()      1] .
            (and a b (or c (and s t u v w) (not y)) d))
        ([(and a b (or c (and s t u v w) (not y)) d)   (2 1 1) 1] .
            (and t))
        ([(and a b (or c (and s t u v w) (not y)) d)   (2 1 1) 2] .
            (and t u))
    ))
    (test-list "LF xarg span subs" lf-xarg-span-subs '(
        ([(and a b (or c (and s t u v w) (not y)) d)   ()      1  xx] .
            xx)
        ([(and a b (or c (and s t u v w) (not y)) d)   (2 1 1) 1  xx] .
            (and a b (or c (and s xx u v w) (not y)) d))
        ([(and a b (or c (and s t u v w) (not y)) d)   (2 1 1) 2  xx] .
            (and a b (or c (and s xx v w) (not y)) d))
    ))
    (test-list "Truth tables" truth-table-of-parts
     '(
       ([#f]       . ((#f) (#f)) )
       ([#t]       . ((#t) (#t)) )
       ([(and #f)] . (((and #f)) (#f)) )
       ([(and #t)] . (((and #t)) (#t)) )

       ([(and )] . (((and )) (#t)) )
       ([(or  )] . (((or  )) (#f)) )
       ([(xor )] . (((xor )) (#f)) )
       ([(nand)] . (((nand)) (#f)) )
       ([(nor )] . (((nor )) (#t)) )
       ([(xnor)] . (((xnor)) (#t)) )

       ([p]        . ((p)         (#f) (#t)) )

       ([(not p)]  . ((p (not p)) (#f #t) (#t #f)) )

       ([(and  p)] . ((p (and  p)) (#f #f) (#t #t)) )
       ([(or   p)] . ((p (or   p)) (#f #f) (#t #t)) )
       ([(xor  p)] . ((p (xor  p)) (#f #f) (#t #t)) )
       ([(nand p)] . ((p (nand p)) (#f #t) (#t #f)) )
       ([(nor  p)] . ((p (nor  p)) (#f #t) (#t #f)) )
       ([(xnor p)] . ((p (xnor p)) (#f #t) (#t #f)) )

       ([(and p q)]  .
        ((p q (and  p q)) (#f #f #f) (#f #t #f) (#t #f #f) (#t #t #t)) )
       ([(or  p q)]  .
        ((p q (or   p q)) (#f #f #f) (#f #t #t) (#t #f #t) (#t #t #t)) )
       ([(xor p q)]  .
        ((p q (xor  p q)) (#f #f #f) (#f #t #t) (#t #f #t) (#t #t #f)) )
       ([(nand p q)] .
        ((p q (nand p q)) (#f #f #t) (#f #t #t) (#t #f #t) (#t #t #f)) )
       ([(nor  p q)] .
        ((p q (nor  p q)) (#f #f #t) (#f #t #f) (#t #f #f) (#t #t #f)) )
       ([(xnor p q)] .
        ((p q (xnor p q)) (#f #f #t) (#f #t #f) (#t #f #f) (#t #t #t)) )

       ([(impl p q)] .
        ((p q (impl p q)) (#f #f #t) (#f #t #t) (#t #f #f) (#t #t #t)) )
       ([(equiv p q)] .
        ((p q (equiv p q))(#f #f #t) (#f #t #f) (#t #f #f) (#t #t #t)) )

       ([(and p q r)]  .
        ((p q  r (and p q r))
         (#f #f #f #f) (#f #f #t #f) (#f #t #f #f) (#f #t #t #f)
         (#t #f #f #f) (#t #f #t #f) (#t #t #f #f) (#t #t #t #t)) )
       ([(or  p q r)]  .
        ((p q  r (or  p q r))  
         (#f #f #f #f) (#f #f #t #t) (#f #t #f #t) (#f #t #t #t)
         (#t #f #f #t) (#t #f #t #t) (#t #t #f #t) (#t #t #t #t)) )
       ([(xor p q r)]  .
        ((p  q  r (xor p q r))  
         (#f #f #f #f) (#f #f #t #t) (#f #t #f #t) (#f #t #t #f)
         (#t #f #f #t) (#t #f #t #f) (#t #t #f #f) (#t #t #t #t)) )
       ([(nand p q r)] .
        ((p  q  r (nand p q r)) 
         (#f #f #f #t) (#f #f #t #t) (#f #t #f #t) (#f #t #t #t)
         (#t #f #f #t) (#t #f #t #t) (#t #t #f #t) (#t #t #t #f)) )
       ([(nor  p q r)] .
        ((p  q  r (nor  p q r)) 
         (#f #f #f #t) (#f #f #t #f) (#f #t #f #f) (#f #t #t #f)
         (#t #f #f #f) (#t #f #t #f) (#t #t #f #f) (#t #t #t #f)) )
       ([(xnor p q r)] .
        ((p  q  r (xnor p q r)) 
         (#f #f #f #t) (#f #f #t #f) (#f #t #f #f) (#f #t #t #t)
         (#t #f #f #f) (#t #f #t #t) (#t #t #f #t) (#t #t #t #f)) )

       ([(equiv (impl p q) (or (not p) q))] .
        ((p  q (impl p q)(not p)(or (not p) q)(equiv (impl p q) (or (not p) q)))
         (#f #f #t       #t     #t            #t)
         (#f #t #t       #t     #t            #t)
         (#t #f #f       #f     #f            #t)
         (#t #t #t       #f     #t            #t)) )
    ))
    (test-list "Find minimal cover" find-minimal-cover '(
        ([(a b c d) ((l1 a) (l2 b c) (l3 a c) (l4 b d) (l5 d)) short]
        . ((l3 a c) (l4 b d)) )
        ([(a b c d) ((l1 a) (l2 b c) (l3 a c) (l4 b d) (l5 d)) long]
        . ((l3 a c) (l4 b d)) )
        ([(a b c d) ((l1 a b)(l2 b c)(l3 b c d)(l4 c d)(l5 c)(l6 d)) short]
        . ((l1 a b) (l4 c d)) )
        ([(a b c d) ((l1 a b)(l2 b c)(l3 b c d)(l4 c d)(l5 c)(l6 d)) long]
        . ((l1 a b) (l3 b c d)) )
    ))
    (test-list "Prime implicants"
      (lambda (ell)
        (let ([pi-dnf (lf-prime-implicants ell prime-implicants-from-dnf)]
              [pi-qmc (lf-prime-implicants ell quine-mccluskey-algorithm)])
          (if (equal? pi-dnf pi-qmc) pi-dnf (list 'Both pi-dnf pi-qmc)) ))
    '(
      ([#t]                    . ((and)) )
      ([#f]                    . () )
      ([(and a (not a))]       . () )
      ([(or (and a (not a)))]  . () )
      ([(or (and a (not a)) (and (not b) b))]  . () )
      ([a]                     . ((and a)) )
      ([(not a)]               . ((and (not a))) )
      ([(or a b)]              . ((and a) (and b)) )
      ([(and a b)]             . ((and a b)) )
     
      ([(or (and (not a) b (not c) (not d))
            (and a (not b) (not c) (not d))
            (and a (not b) c (not d))
            (and a (not b) c d)
            (and a b (not c) (not d))
            (and a b c d))] 
       .  ((and a c d)
           (and a (not b) c)
           (and a (not b) (not d))
           (and a (not c) (not d))
           (and b (not c) (not d)) ) )
      ([(or 
           (and a (not b) (not c) (not d))
           (and a (not b) (not c) d)
           (and a (not b) (not c))
           (and a (not b) (not d))
           (and a (not b) c (not d))
           (and a (not c) (not d))
           (and a (not c))
           (and a (not d))
           (and a b (not c) (not d))
           (and a b (not c) d)
           (and a b (not c))
           (and a b (not d))
           (and a b c (not d))
           (and a b c d)
           (and a b c)
           (and a b d)
           (and a b)
           (and a c (not d))
           (and a d (not c))
     
           (and (not a) (not b) (not c) d)
           (and (not a) (not b) c (not d))
           (and (not a) b c (not d))
           (and (not a) c (not d))
     
           (and b c (not d))
     
           (and (not b) (not c) d)
           (and (not b) c (not d))
     
           (and c (not d)) )] 
       . ((and a b)
          (and a (not c))
          (and a (not d))
          (and c (not d))
          (and (not b) (not c) d)) )
    ))
    (test-list "Essential prime implicants"
      (lambda (need-terms dc-minterms)
          (let* (
            [ok-lf (append '(or) need-terms dc-minterms)]
            [pis  (lf-prime-implicants ok-lf)]
            [epis (essential-prime-implicants pis dc-minterms)])
            epis)) 
      '(
       ; This example is from the Wikipedia article on Quine-McCluskey.
       ([((and (not za) yb (not xc) (not wd))
           (and za (not yb) (not xc) (not wd))
           (and za (not yb) xc (not wd))
           (and za (not yb) xc wd)
           (and za yb (not xc) (not wd))
           (and za yb xc wd))
         ((and za (not yb) (not xc) wd)
          (and za yb xc (not wd))) ]
        . ((and xc za) (and (not wd) (not xc) yb )) )
    ))
    (test-list "Minimal DNF" minimal-dnf '(
       ; This example is from the Wikipedia article on Quine-McCluskey.
       ([(or (and (not za) yb (not xc) (not wd))
           (and za (not yb) (not xc) (not wd))
           (and za (not yb) xc (not wd))
           (and za (not yb) xc wd)
           (and za yb (not xc) (not wd))
           (and za yb xc wd))
         ((and za (not yb) (not xc) wd)
          (and za yb xc (not wd))) ]
        . (or (and xc za) (and (not wd) (not xc) yb) (and (not yb) za)) )
    ))
    (test-list "Davis-Putnam Procedure" dpp
    '(
        ([(p1 p2 p3 p4 p5 p6)
          ((impl p1 p2)  (not p2)  (impl (not p1) (or p3 p4))
           (impl p3 p5)  (impl p6 (not p5))  p6  (or p6 (not p6))
           (not p4)
          ) ] . ((or)) )
        ([(p1 p2 p3 p4 p5 p6)
          ((impl p1 p2)  (not p2)  (impl (not p1) (or p3 p4))
           (impl p3 p5)  (impl p6 (not p5))  p6  (or p6 (not p6))
          ) ] . () )
    ))
    (test-list "Lexical Analysis 0"
      (lambda (s c0 ins)
        (let* ([in (inp (open-input-string ins) 0)]
               [bic (bite-if-can? s   c0 in)]
               [peek (inp-peek-char in)] )
          (list bic (if (eof-object? peek) 'eof peek)) ))
    '(
        (["<"      #\< "->"]     . (#t #\-))
        (["->"     #\- ">xyz"]   . (#t #\x))
        (["->"     #\- "]xyz"]   . (#f #\]))
        (["+>"     #\- ">xyz"]   . (#f #\>))
        (["<->"    #\< ">xyz"]   . (#f #\>))
        (["<->"    #\< "->xyz"]  . (#t #\x))
        (["<->"    #\< "->"]     . (#t eof))
        (["<->"    #\< ">"]      . (#f #\>))
        (["\\and"  #\\ "andor"]  . (#t #\o))
        (["\\land" #\\ "landor"] . (#t #\o))
    ))
    (test-list "Lexical Analysis 1" 
      (lambda (s)
        (call/cc (lambda (ret)
          (let* ([in (inp (open-input-string s) 0)]
                 [tok-list '()]
                 [syn-err (lambda (c0 in)
                   (list "Syntax error" c0 (inp-pos in))
                     (ret (reverse (cons (list (inp-pos in) "Syntax error" c0)
                           tok-list ))) ) ])
            (do ([tok (in-get-token in syn-err) (in-get-token in syn-err)])
                [(eof-object? tok) (reverse tok-list)]
              (set! tok-list (cons (list (inp-pos in) tok) tok-list)) ) ))))
    '( 
        (["(\\land a -> <-> b \\/ /\\ !b c' \\land \\lorp \\nox)" ] .
         ((1 #\() (6 #\∧) (8 a) (11 #\→) (15 #\↔) (17 b) (20 #\∨) (23 #\∧)
          (25 #\¬) (26 b) (28 c) (29 #\') (35 #\∧) (40 #\∨) (41 p)
          (43 "Syntax error" #\\) ))

        (["a ()[]{}_∧∨¬→↔⊕'3~902bc" ] .
         ((1 a) (3 #\() (4 #\)) (5 #\[) (6 #\]) (7 #\{) (8 #\}) (9 #\_)
          (10 #\∧) (11 #\∨) (12 #\¬) (13 #\→) (14 #\↔) (15 #\⊕) (16 #\')
          (17 3) (18 #\¬) (21 902) (23 bc)))

    ))
    (test-list "Parsing" (lambda (s)
      (define tok-props (list
        ;     name   null pre in post  lbp     rbp    term-former   lf-name
        (list #\'    #f   #f  #f #t    60      'undef list          'not)
        (list #\|    #f   #t  #f #f    'undef  50     list          'nand)
        (list #\→    #f   #f  #t #f    40      39     list          'impl)
        (list #\·    #f   #f  #t #f    30      31     list          'and)
        (list #\¬    #f   #t  #f #f    'undef  20     list          'neg)
        (list #\+    #f   #f  #t #f    10      11     list          'or)
        (list #\,    #f   #f  #f #t    1      'undef  list          'xor)
      ))
      (define op-tokens 
        '((nand . #\|) (impl . #\→)
          (and . #\·) (not . #\¬) (or . #\+) (xor . #\,)))
      (define op-strings
        '((#t . "1")     (#f . "0")
          (lparen . "(") (rparen . ")")
          (not "" . "'")
          (nand "|" "")
          (impl . "→")
          (and . "·")
          (neg "¬" . "")
          (or . "+") (xor "" . ",")))
      (call/cc (lambda (throw-syntax-error)
        (define ts (tok-stream (inp (open-input-string s))))
        (define (syn-error tok-stream msgl)
          (throw-syntax-error 
            ;(append (list 'syntax-error (mcdr (mcdr tok-stream))) msgl)))
            (append (list 'syntax-error tok-stream msgl))))
        (parse-stream ts tok-props syn-error)) ))
    '(
       (["¬x·y + z + | u→v→w·t" ] .
            (#\+ (#\+ (#\¬ (#\· x y)) z) (#\· (#\→ (#\| u) (#\→ v w)) t)) )
       (["¬x·y, + z + | u→v'→w·t" ] .
            (#\+ (#\+ (#\, (#\¬ (#\· x y))) z)
                 (#\· (#\→ (#\| u) (#\→ (#\' v) w)) t)) )
    ))
    (test-list "LF with selection paths" 
        (fn-with-global (*lfws-verbose* #f) lfws-path-ok?)
    '(
        ([()  1   (and a b)]  . #t)
        ([()  2   (and a b)]  . #f)  ; span too big
        ([(0) 1   (and a b)]  . #t)
        ([(1) 1   (and a b)]  . #t)
        ([(2) 1   (and a b)]  . #f)  ; start too big
        ([(0) 2   (and a b)]  . #t)
        ([(0) 3   (and a b)]  . #f)  ; span too big
        ([(0) 2   (impl a b)] . #f)  ; span != 1 when not assoc
        ([(0 1) 3 (impl (or u v w x y z) b)] . #t)
    ))
    (test-list "LF with selection"
      (lambda args (lfws-show (apply lf-with-selection args)))
    '(
       ([(and a (or b c d e) f)      ] .
        (>>>> (and a (or b c d e) f) <<<<))
       ([(and a (or b c d e) f) (0)  ] .
        (and (>>>> a <<<<) (or b c d e) f))
       ([(and a (or b c d e) f) (0) 1] .
        (and (>>>> a <<<<) (or b c d e) f))
       ([(and a (or b c d e) f) (0) 2] .
        (and (>>>> (and a (or b c d e)) <<<<) f))
       ([(and a (or b c d e) f)(1 2)1] .
        (and a (or b c (>>>> d <<<<) e) f))
       ([(and a (or b c d e) f)(1 2)2] .
        (and a (or b c (>>>> (or d e) <<<<)) f))
    ))
    (test-list "Logic Formatting"
      (lambda (lf) (list
        (lf->logic-string    lf)
        (lf->logic-latex     lf)))
    '(
       ([#f] . ("⊥" "\\perp"))
       ([#t] . ("⊤" "\\top" ))

       ([(and #f)] . ("⊥" "\\perp"))
       ([(and #t)] . ("⊤" "\\top" ))

       ([(and )] . ("⊤" "\\top" ))
       ([(or  )] . ("⊥" "\\perp"))
       ([(xor )] . ("⊥" "\\perp"))
       ([(nand)] . ("⊥" "\\perp"))
       ([(nor)]  . ("⊤" "\\top" ))
       ([(xnor)] . ("⊤" "\\top" ))

       ([p]        . ("p"  "p"      ))
       ([(not p)]  . ("¬p" "\\neg p"))

       ([(and  p)] . ("p"  "p"      ))
       ([(or   p)] . ("p"  "p"      ))
       ([(xor  p)] . ("p"  "p"      ))
       ([(nand p)] . ("¬p" "\\neg p"))
       ([(nor  p)] . ("¬p" "\\neg p"))
       ([(xnor p)] . ("¬p" "\\neg p"))

       ([(and  p q)] . ("p∧q" "p\\land q" ))
       ([(or   p q)] . ("p∨q" "p\\lor q"  ))
       ([(xor  p q)] . ("p⊕q" "p\\oplus q"))
       ([(nand p q)] . ("p|q" "p|q"       ))
       ([(nor  p q)] . ("p↓q" "p\\downarrow q"))
       ([(xnor p q)] . ("p↔q" "p\\leftrightarrow q"))


       ([(impl  p q)] .  ("p→q" "p\\rightarrow q"    ))
       ([(equiv p q)] .  ("p↔q" "p\\leftrightarrow q"))

       ([(and p q r)]  . ("p∧q∧r" "p\\land q\\land r"))
       ([(or  p q r)]  . ("p∨q∨r" "p\\lor q\\lor r"  ))
       ([(xor p q r)]  . ("p⊕q⊕r" "p\\oplus q\\oplus r"))
       ([(nand p q r)] . ("p|q|r" "p|q|r"))
       ([(nor  p q r)] . ("p↓q↓r" "p\\downarrow q\\downarrow r"))
       ([(xnor p q r)] . ("p↔q↔r" "p\\leftrightarrow q\\leftrightarrow r"))


       ([(and (and  a b) (and c d e))] .
        ("(a∧b)∧(c∧d∧e)" "\\left (a\\land b\\right )\\land \\left (c\\land d\\land e\\right )"))
       ([(and (or   a b) c)] .
        ("(a∨b)∧c" "\\left (a\\lor b\\right )\\land c"))
       ([(and (xor  a b) c)] .
        ("(a⊕b)∧c" "\\left (a\\oplus b\\right )\\land c"))
       ([(and (nand a b) c)] .
        ("(a|b)∧c" "\\left (a|b\\right )\\land c"))
       ([(and (nor  a b) c)] .
        ("(a↓b)∧c" "\\left (a\\downarrow b\\right )\\land c"))
       ([(and (xnor a b) c)] .
        ("(a↔b)∧c" "\\left (a\\leftrightarrow b\\right )\\land c"))
       ([(and (impl  a b) c)] .
        ("(a→b)∧c" "\\left (a\\rightarrow b\\right )\\land c"))
       ([(and (equiv a b) c)] .
        ("(a↔b)∧c" "\\left (a\\leftrightarrow b\\right )\\land c"))


       ([(or (and  a b) (and c d e))] .
        ("(a∧b)∨(c∧d∧e)" "\\left (a\\land b\\right )\\lor \\left (c\\land d\\land e\\right )"))
       ([(or (or   a b) c)] .
        ("(a∨b)∨c" "\\left (a\\lor b\\right )\\lor c"))
       ([(or (xor  a b) c)] .
        ("(a⊕b)∨c" "\\left (a\\oplus b\\right )\\lor c"))
       ([(or (nand a b) c)] .
        ("(a|b)∨c" "\\left (a|b\\right )\\lor c"))
       ([(or (nor  a b) c)] .
        ("(a↓b)∨c" "\\left (a\\downarrow b\\right )\\lor c"))
       ([(or (xnor a b) c)] .
        ("(a↔b)∨c" "\\left (a\\leftrightarrow b\\right )\\lor c"))
       ([(or (impl  a b) c)] .
        ("(a→b)∨c" "\\left (a\\rightarrow b\\right )\\lor c"))
       ([(or (equiv a b) c)] .
        ("(a↔b)∨c" "\\left (a\\leftrightarrow b\\right )\\lor c"))

       ([(xor (and  a b) (and c d e))] .
        ("(a∧b)⊕(c∧d∧e)" "\\left (a\\land b\\right )\\oplus \\left (c\\land d\\land e\\right )"))
       ([(xor (or   a b) c)] .
        ("(a∨b)⊕c" "\\left (a\\lor b\\right )\\oplus c"))
       ([(xor (xor  a b) c)] .
        ("(a⊕b)⊕c" "\\left (a\\oplus b\\right )\\oplus c"))
       ([(xor (nand a b) c)] .
        ("(a|b)⊕c" "\\left (a|b\\right )\\oplus c"))
       ([(xor (nor  a b) c)] .
        ("(a↓b)⊕c" "\\left (a\\downarrow b\\right )\\oplus c"))
       ([(xor (xnor a b) c)] .
        ("(a↔b)⊕c" "\\left (a\\leftrightarrow b\\right )\\oplus c"))
       ([(xor (impl  a b) c)] .
        ("(a→b)⊕c" "\\left (a\\rightarrow b\\right )\\oplus c"))
       ([(xor (equiv a b) c)] .
        ("(a↔b)⊕c" "\\left (a\\leftrightarrow b\\right )\\oplus c"))

       ([(nand (and  a b) (and c d e))] .
        ("(a∧b)|(c∧d∧e)" "\\left (a\\land b\\right )|\\left (c\\land d\\land e\\right )"))
       ([(nand (or   a b) c)] .
        ("(a∨b)|c" "\\left (a\\lor b\\right )|c"))
       ([(nand (xor  a b) c)] .
        ("(a⊕b)|c" "\\left (a\\oplus b\\right )|c"))
       ([(nand (nand a b) c)] .
        ("(a|b)|c" "\\left (a|b\\right )|c" ))
       ([(nand (nor  a b) c)] .
        ("(a↓b)|c" "\\left (a\\downarrow b\\right )|c"))
       ([(nand (xnor a b) c)] .
        ("(a↔b)|c" "\\left (a\\leftrightarrow b\\right )|c"))
       ([(nand (impl  a b) c)] .
        ("(a→b)|c" "\\left (a\\rightarrow b\\right )|c"))
       ([(nand (equiv a b) c)] .
        ("(a↔b)|c" "\\left (a\\leftrightarrow b\\right )|c"))

       ([(nor (and  a b) (and c d e))] .
        ("(a∧b)↓(c∧d∧e)" "\\left (a\\land b\\right )\\downarrow \\left (c\\land d\\land e\\right )"))
       ([(nor (or   a b) c)] .
        ("(a∨b)↓c" "\\left (a\\lor b\\right )\\downarrow c"))
       ([(nor (xor  a b) c)] .
        ("(a⊕b)↓c" "\\left (a\\oplus b\\right )\\downarrow c"))
       ([(nor (nand a b) c)] .
        ("(a|b)↓c" "\\left (a|b\\right )\\downarrow c"))
       ([(nor (nor  a b) c)] .
        ("(a↓b)↓c"   "\\left (a\\downarrow b\\right )\\downarrow c"))
       ([(nor (xnor a b) c)] .
        ("(a↔b)↓c" "\\left (a\\leftrightarrow b\\right )\\downarrow c"))
       ([(nor (impl  a b) c)] .
        ("(a→b)↓c" "\\left (a\\rightarrow b\\right )\\downarrow c"))
       ([(nor (equiv a b) c)] .
        ("(a↔b)↓c" "\\left (a\\leftrightarrow b\\right )\\downarrow c"))

       ([(xnor (and  a b) (and c d e))] .
        ("a∧b↔c∧d∧e" "a\\land b\\leftrightarrow c\\land d\\land e"))
       ([(xnor (or   a b) c)] .
        ("a∨b↔c" "a\\lor b\\leftrightarrow c"))
       ([(xnor (xor  a b) c)] .
        ("a⊕b↔c" "a\\oplus b\\leftrightarrow c"))
       ([(xnor (nand a b) c)] .
        ("a|b↔c" "a|b\\leftrightarrow c"))
       ([(xnor (nor  a b) c)] .
        ("a↓b↔c" "a\\downarrow b\\leftrightarrow c"))
       ([(xnor (xnor a b) c)] .
        ("(a↔b)↔c" "\\left (a\\leftrightarrow b\\right )\\leftrightarrow c"))
       ([(xnor (impl  a b) c)] .
        ("a→b↔c" "a\\rightarrow b\\leftrightarrow c"))
       ([(xnor (equiv a b) c)] .
        ("(a↔b)↔c" "\\left (a\\leftrightarrow b\\right )\\leftrightarrow c"))

       ([(impl (and  a b) (and c d e))] .
        ("a∧b→c∧d∧e" "a\\land b\\rightarrow c\\land d\\land e"))
       ([(impl (or   a b) c)] .
        ("a∨b→c" "a\\lor b\\rightarrow c"))
       ([(impl (xor  a b) c)] .
        ("a⊕b→c" "a\\oplus b\\rightarrow c"))
       ([(impl (nand a b) c)] .
        ("a|b→c" "a|b\\rightarrow c"))
       ([(impl (nor  a b) c)] .
        ("a↓b→c" "a\\downarrow b\\rightarrow c"))
       ([(impl (xnor a b) c)] .
        ("(a↔b)→c" "\\left (a\\leftrightarrow b\\right )\\rightarrow c"))
       ([(impl (impl  a b) c)] .
        ("(a→b)→c" "\\left (a\\rightarrow b\\right )\\rightarrow c"))
       ([(impl (equiv a b) c)] .
        ("(a↔b)→c" "\\left (a\\leftrightarrow b\\right )\\rightarrow c"))

       ([(equiv (and  a b) (and c d e))] .
        ("a∧b↔c∧d∧e" "a\\land b\\leftrightarrow c\\land d\\land e"))
       ([(equiv (or   a b) c)] .
        ("a∨b↔c" "a\\lor b\\leftrightarrow c"))
       ([(equiv (xor  a b) c)] .
        ("a⊕b↔c" "a\\oplus b\\leftrightarrow c"))
       ([(equiv (nand a b) c)] .
        ("a|b↔c" "a|b\\leftrightarrow c"))
       ([(equiv (nor  a b) c)] .
        ("a↓b↔c" "a\\downarrow b\\leftrightarrow c"))
       ([(equiv (xnor a b) c)] .
        ("(a↔b)↔c" "\\left (a\\leftrightarrow b\\right )\\leftrightarrow c"))
       ([(equiv (impl  a b) c)] .
        ("a→b↔c" "a\\rightarrow b\\leftrightarrow c"))
       ([(equiv (equiv a b) c)] .
        ("(a↔b)↔c" "\\left (a\\leftrightarrow b\\right )\\leftrightarrow c"))

       ([(and #f a b (and g h) 
              (or (and #t A B) (or (not y) z) (not (and (impl U V) v))))] .
        ("⊥∧a∧b∧(g∧h)∧((⊤∧A∧B)∨(¬y∨z)∨¬((U→V)∧v))"

          "\\perp\\land a\\land b\\land \\left (g\\land h\\right )\\land \\left (\\left (\\top\\land A\\land B\\right )\\lor \\left (\\neg y\\lor z\\right )\\lor \\neg \\left (\\left (U\\rightarrow V\\right )\\land v\\right )\\right )"

          ))
     ))
    (test-list "Boolean Algebra Formatting"
      (lambda (lf) (list
        (lf->boolalg-string lf)
        (lf->boolalg-latex  lf) ))
    '(
       ([#f] . ("0" "0"))
       ([#t] . ("1" "1"))

       ([p]           . ("p"  "p" ))
       ([(not p)]     . ("p'" "\\overline{p}"))

       ([(and #f)]    . ("0"     "0"))
       ([(and #t)]    . ("1"     "1"))
       ([(and)]       . ("1"     "1"))
       ([(and p)]     . ("p"     "p" ))
       ([(and p q)]   . ("p·q"   "p\\cdot q"))
       ([(and p q r)] . ("p·q·r" "p\\cdot q\\cdot r"))

       ([(or #f)]     . ("0"     "0"))
       ([(or #t)]     . ("1"     "1"))
       ([(or)]        . ("0"     "0"))
       ([(or p)]      . ("p"     "p" ))
       ([(or p q)]    . ("p+q"   "p+q"))
       ([(or p q r)]  . ("p+q+r" "p+q+r"))

       ([(and (and a b) c)] . ("(a·b)·c" "\\left (a\\cdot b\\right )\\cdot c"))
       ([(and (or  a b) c)] . ("(a+b)·c" "\\left (a+b\\right )\\cdot c"))
       ([(or  (and a b) c)] . ("a·b+c"   "a\\cdot b+c"))
       ([(or  (or  a b) c)] . ("(a+b)+c" "\\left (a+b\\right )+c"))

       ([(impl (and  a b) c)] .
        ("Operator impl not allowed." "Operator impl not allowed."))
     ))
     (test-list "Formatting truth tables"
       (lambda (lf) 
         (let ([tt (truth-table-of-parts lf)]) (append
           (truth-table->strings  lf->logic-string   tt)
           (truth-table->strings  lf->boolalg-string tt)
           (truth-table->latex    lf->logic-latex    tt "||")
           (truth-table->latex    lf->boolalg-latex  tt "||") )) )
     '(
        ([#f] .
        ("⊥ " "0 "
         "0 " "0 "
         "\\begin{tabular}{||c}"
           "$\\perp$\\\\" "\\hline" "0\\\\"
         "\\end{tabular}"
         "\\begin{tabular}{||c}"
           "$0$\\\\" "\\hline" "0\\\\"
         "\\end{tabular}" ))

        ([(and #f)] .
        ("⊥ " "0 "
         "0 " "0 "
         "\\begin{tabular}{||c}"
           "$\\perp$\\\\" "\\hline" "0\\\\"
         "\\end{tabular}"
         "\\begin{tabular}{||c}"
           "$0$\\\\" "\\hline" "0\\\\"
         "\\end{tabular}" ))

        ([p] .
        ("p " "0 " "1 "
         "p " "0 " "1 "
         "\\begin{tabular}{c||}"
           "$p$\\\\" "\\hline" "0\\\\" "1\\\\"
         "\\end{tabular}"
         "\\begin{tabular}{c||}"
           "$p$\\\\" "\\hline" "0\\\\" "1\\\\"
         "\\end{tabular}" ))

        ([(not p)] .
        ("p ¬p " "0 1  " "1 0  "
         "p p' " "0 1  " "1 0  "
         "\\begin{tabular}{c||c}"
           "$p$ & $\\neg p$\\\\" "\\hline" "0 & 1\\\\" "1 & 0\\\\"
         "\\end{tabular}"
         "\\begin{tabular}{c||c}"
           "$p$ & $\\overline{p}$\\\\" "\\hline" "0 & 1\\\\" "1 & 0\\\\"
         "\\end{tabular}" ))

        ([(and (or (not p) q) (not (or (not p) q)))] .
        ("p q ¬p ¬p∨q ¬(¬p∨q) (¬p∨q)∧¬(¬p∨q) "
         "0 0 1  1    0       0              "
         "0 1 1  1    0       0              "
         "1 0 0  0    1       0              "
         "1 1 0  1    0       0              "
         "p q p' p'+q (p'+q)' (p'+q)·(p'+q)' "
         "0 0 1  1    0       0              "
         "0 1 1  1    0       0              "
         "1 0 0  0    1       0              "
         "1 1 0  1    0       0              "
         "\\begin{tabular}{cc||cccc}"
         "$p$ & $q$ & $\\neg p$ & $\\neg p\\lor q$ & $\\neg \\left (\\neg p\\lor q\\right )$ & $\\left (\\neg p\\lor q\\right )\\land \\neg \\left (\\neg p\\lor q\\right )$\\\\"
         "\\hline"
         "0 & 0 & 1 & 1 & 0 & 0\\\\"
         "0 & 1 & 1 & 1 & 0 & 0\\\\"
         "1 & 0 & 0 & 0 & 1 & 0\\\\"
         "1 & 1 & 0 & 1 & 0 & 0\\\\"
         "\\end{tabular}"
         "\\begin{tabular}{cc||cccc}"
         "$p$ & $q$ & $\\overline{p}$ & $\\overline{p}+q$ & $\\overline{\\left (\\overline{p}+q\\right )}$ & $\\left (\\overline{p}+q\\right )\\cdot \\overline{\\left (\\overline{p}+q\\right )}$\\\\"
         "\\hline"
         "0 & 0 & 1 & 1 & 0 & 0\\\\"
         "0 & 1 & 1 & 1 & 0 & 0\\\\"
         "1 & 0 & 0 & 0 & 1 & 0\\\\"
         "1 & 1 & 0 & 1 & 0 & 0\\\\"
         "\\end{tabular}" ))

        ([(impl (or (not p) q) (not (or (not p) q)))] .
        ("p q ¬p ¬p∨q ¬(¬p∨q) ¬p∨q→¬(¬p∨q) "
         "0 0 1  1    0       0            "
         "0 1 1  1    0       0            "
         "1 0 0  0    1       1            "
         "1 1 0  1    0       0            "
         "p q p' p'+q (p'+q)' Operator impl not allowed. "
         "0 0 1  1    0       0                          "
         "0 1 1  1    0       0                          "
         "1 0 0  0    1       1                          "
         "1 1 0  1    0       0                          "
         "\\begin{tabular}{cc||cccc}"
         "$p$ & $q$ & $\\neg p$ & $\\neg p\\lor q$ & $\\neg \\left (\\neg p\\lor q\\right )$ & $\\neg p\\lor q\\rightarrow \\neg \\left (\\neg p\\lor q\\right )$\\\\"
         "\\hline"
         "0 & 0 & 1 & 1 & 0 & 0\\\\"
         "0 & 1 & 1 & 1 & 0 & 0\\\\"
         "1 & 0 & 0 & 0 & 1 & 1\\\\"
         "1 & 1 & 0 & 1 & 0 & 0\\\\"
         "\\end{tabular}"
         "\\begin{tabular}{cc||cccc}"
         "$p$ & $q$ & $\\overline{p}$ & $\\overline{p}+q$ & $\\overline{\\left (\\overline{p}+q\\right )}$ & $Operator impl not allowed.$\\\\"
         "\\hline"
         "0 & 0 & 1 & 1 & 0 & 0\\\\"
         "0 & 1 & 1 & 1 & 0 & 0\\\\"
         "1 & 0 & 0 & 0 & 1 & 1\\\\"
         "1 & 1 & 0 & 1 & 0 & 0\\\\"
         "\\end{tabular}")
       )
    ))
    (test-list "FD symbols" fd-get-symbols
    '(
        ([(impl)  (V (impl X Y) U)] . (U Y X V))
    ))
    (test-list "FD subs" 
      (lambda (syn-syms E)
        (let* ([s  (fd-gen-subs syn-syms E)]
               [si (fd-inverse-subs s)]
               [F  (fd-apply-subs s E)]
               [Fi (fd-apply-subs si F)])
          (list (equal? E F) (equal? E Fi))))
    '(
        ([(impl)  (V (impl X Y) U)] . (#f #t))
    ))
    (test-list "FD match" fd-match
    '(
        ([(and or) (and A B) (and (or A B) C)] .
         ((B . C) (A . (or A B))))
        ([(and or) (and (or A B) (or A C)) (and (or X Y) (or X Z))] .
         ((C . Z) (B . Y) (A . X)))
        ([(and or) (and A B) '(or (and A B) C) ] .
         #f)
        ([(and or) (and (or A B) '(or A C)) '(and (or X Y) (or W Z)) ] .
         #f)
    ))
    (test-list "FD theorem premise permutations" fd-ent-premise-permutations
    '(
       ([(fd-ent (S T U V) C) (fd-ent (D Σ (or A B)) C)] .
         ((fd-ent (S (set U V) T) C)
          (fd-ent (S (set T V) U) C)
          (fd-ent (S (set T U) V) C)
          (fd-ent (T (set U V) S) C)
          (fd-ent (T (set S V) U) C)
          (fd-ent (T (set S U) V) C)
          (fd-ent (U (set T V) S) C)
          (fd-ent (U (set S V) T) C)
          (fd-ent (U (set S T) V) C)
          (fd-ent (V (set T U) S) C)
          (fd-ent (V (set S U) T) C)
          (fd-ent (V (set S T) U) C)))
       ([(fd-ent (S T U V) C) (fd-ent (Σ D (or A B)) C)] .
         ((fd-ent ((set U V) S T) C)
          (fd-ent ((set T V) S U) C)
          (fd-ent ((set T U) S V) C)
          (fd-ent ((set U V) T S) C)
          (fd-ent ((set S V) T U) C)
          (fd-ent ((set S U) T V) C)
          (fd-ent ((set T V) U S) C)
          (fd-ent ((set S V) U T) C)
          (fd-ent ((set S T) U V) C)
          (fd-ent ((set T U) V S) C)
          (fd-ent ((set S U) V T) C)
          (fd-ent ((set S T) V U) C)))
       ([(fd-ent (S T U V) C) (fd-ent (D (or A B) Σ) C)] .
         ((fd-ent (S T (set U V)) C)
          (fd-ent (S U (set T V)) C)
          (fd-ent (S V (set T U)) C)
          (fd-ent (T S (set U V)) C)
          (fd-ent (T U (set S V)) C)
          (fd-ent (T V (set S U)) C)
          (fd-ent (U S (set T V)) C)
          (fd-ent (U T (set S V)) C)
          (fd-ent (U V (set S T)) C)
          (fd-ent (V S (set T U)) C)
          (fd-ent (V T (set S U)) C)
          (fd-ent (V U (set S T)) C)))
       ([(fd-ent (S T U) C) (fd-ent (D (or A B) Σ) C)] .
         ((fd-ent (S T (set U)) C)
          (fd-ent (S U (set T)) C)
          (fd-ent (T S (set U)) C)
          (fd-ent (T U (set S)) C)
          (fd-ent (U S (set T)) C)
          (fd-ent (U T (set S)) C)))
       ([(fd-ent (S T) C) (fd-ent (D (or A B) Σ) C)] .
         ((fd-ent (S T (set)) C) (fd-ent (T S (set)) C)))
       ([(fd-ent (S) C) (fd-ent (D (or A B) Σ) C)] .
         ())
       ([(fd-ent (S T U V) C) (fd-ent (D (or A B) E) C)] .
         ())
       ([(fd-ent (S T U) C) (fd-ent (D (or A B) E) C)] .
         ((fd-ent (S T U) C)
          (fd-ent (S U T) C)
          (fd-ent (T S U) C)
          (fd-ent (T U S) C)
          (fd-ent (U S T) C)
          (fd-ent (U T S) C)))
       ([(fd-ent (S T) C) (fd-ent (D (or A B) E) C)] .
         ())
  ))
  ))
  (if (= error-count 0)
      (printf "--- All OK! ---~n")
      (printf "--- *** ~a ERRORS *** ---~n" error-count))
  error-count
)

(when *do-specific-tests?*
  (set! grand-error-count (+ grand-error-count (test-all))))

(define (show-me F1 #:verbose? [verbose? #f])
  (let ([nerrs 0])
    (define (pp1 msg ob)
      (when verbose? (printf "~a~n" msg) (pretty-print ob) (newline)) )

    (when verbose? (printf "==============================================~n"))
    (printf "F ") (pretty-print  F1)
    (when verbose? (printf "==============================================~n"))
    (define A1 (lf-not/and/or-only F1))
    (pp1 "A"    A1)
    (define D1 (lf-dnf A1))
    (unless (lf-dnf? D1) (printf "Expected dnf, but got ~a.~n" D1))
    (pp1 "DNF" D1)
    (define dD1 (lf-simplify-and/or D1))
    (unless (lf-dnf? dD1) (printf "Expected dnf, but got ~a.~n" dD1))
    (pp1 "dDNF" dD1)
    (define C1 (lf-cnf A1))
    (unless (lf-cnf? C1) (printf "Expected cnf, but got ~a.~n" C1))
    (pp1 "CNF" C1)
    (define dC1 (lf-simplify-and/or C1))
    (unless (lf-cnf? dC1) (printf "Expected cnf, but got ~a.~n" dC1))
    (pp1 "dCNF" dC1)
    (define pi1 (lf-prime-implicants dD1))
    (pp1 "pi"   pi1)
    (define at1 (foldl lset-union '() (map lf-atoms pi1)))
    (pp1 "atoms of pi" at1)
    (define t1 (map (lambda (lf) (make-term-with-lf 'and at1 lf)) pi1))
    (pp1 "t1" t1)
    (define allt1 (map all-terms t1))
    (pp1 "all t1" allt1)
    (define allt2 (foldl lset-union '() allt1))
    (pp1 "all t2" allt2)
    (define allt3 (map term->termno allt2))
    (pp1 "all t3" allt3)
    (define allt4 (map
        (lambda (tno) (term-formula (make-term-with-termno 'and at1 tno)))
        allt3 ))
    (pp1 "all t4" allt4)
    (define F-reprise (lf-apply 'or allt4))

    (map 
      (lambda (E) 
         (let ([is-equiv?  (lf-are-propositions-equivalent? E F1)])
            (unless is-equiv?
              (printf "Inequivalent~n~a~nand~n~a~n" E F1)
              (set! nerrs (+ 1 nerrs)) )))
         (list A1 D1 dD1 C1 dC1 F-reprise) )
    (if (= nerrs 0)
      (when verbose? (printf "OK~n"))
      (printf "*** Not OK *** ~a errors~n" nerrs) )
    nerrs ))


(when *do-random-tests?*
  (printf "== Random formula tests ==~n")
  (let ([nerrs (+
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 5));  'verbose)
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 6));  'verbose)
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 7));  'verbose)
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 7));  'verbose)
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 10))
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 20))
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 30))
    (show-me (lf-random '(and or not nand nor) '(a b c d e f g) 30))
    (show-me '(not
      (and (not (and d (or (not (and g e)) e)))
           (or (or c (and g)) (or g) (not (or c)) (not (or g))))))
    (show-me '(and (or (not a) b (not c) (not d))
                   (or a (not b) (not c) (not d))
                   (or a (not b) c (not d))
                   (or a c d)
                   (or a b (not c) (not d)) ))
  )])
  (if (= nerrs 0)
    (printf "--- All OK! ---~n")
    (printf "--- *** ~a ERRORS *** ---~n" nerrs))
  (set! grand-error-count (+ grand-error-count nerrs))
))


(when (or *do-specific-tests?* *do-random-tests?*)
  (if (= grand-error-count 0)
    (printf "+++ Grand total OK! +++~n")
    (printf "+++ Grand total *** ~a ERRORS *** +++" grand-error-count)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;+
;;;+ Tests with output
;;;+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(when *do-tests-with-output?*
(printf "DPP Examples =======~n")
(printf "~a~n~a~n~a~n~n~n"
(dpp
  '(p1 p2 p3 p4 p5 p6)
  (map string->lf 
    '("p1→p2" "¬p2" "¬p1→p3∨p4" "p3→p5" "p6→ ¬p5" "p6" "p6∨¬p6" "¬p4"))
  #:verbose? #t)
(dpp
  '(p1 p2 p3 p4 p5 p6)
  (map string->lf 
    '("p1→p2" "¬p2" "¬p1→p3∨p4" "p3→p5" "p6→ ¬p5" "p6" "p6∨¬p6"))
  #:verbose? #t)
(dpp '(p q r s)
  (map string->lf '("p→q" "¬q∨¬r∨s" "p∧r∧¬s"))
  #:verbose? #t))

(define Hyp-proof-subs1 (fd-proof  (list
  (mk-fd-step 1 "A→B, B→C, A ⊢ A→B"   '(mem)       "A=A→B, Σ={B→C, A}"        )
  (mk-fd-step 2 "A→B, B→C, A ⊢ A"     '(mem)       "A=A, Σ={A→B, B→C}"        )
  (mk-fd-step 3 "A→B, B→C, A ⊢ B"     '(impl- 1 2) "A=A, B=B, Σ={A→B, B→C, A}")
  (mk-fd-step 4 "A→B, B→C, A ⊢ B→C"   '(mem)       "A=B→C, Σ={A→B, A}"        )
  (mk-fd-step 5 "A→B, B→C, A ⊢ C"     '(impl- 4 3) "A=B, B=C, Σ={A→B, B→C, A}")
  (mk-fd-step 6 "A→B, B→C ⊢ A→C"      '(impl+ 5)   "A=A, B=C, Σ={A→B, B→C}"   )
)))
(define Hyp-proof-auto1 (fd-proof  (list
  (mk-fd-step 1 "A→B, B→C, A ⊢ A→B"   '(mem))
  (mk-fd-step 2 "A→B, B→C, A ⊢ A"     '(mem))
  (mk-fd-step 3 "A→B, B→C, A ⊢ B"     '(impl- 1 2))
  (mk-fd-step 4 "A→B, B→C, A ⊢ B→C"   '(mem))
  (mk-fd-step 5 "A→B, B→C, A ⊢ C"     '(impl- 4 3))
  (mk-fd-step 6 "A→B, B→C ⊢ A→C"      '(impl+ 5))
)))
(define Hyp-proof-subs2 (mk-fd-proof '(
  [1 "A→B, B→C, A ⊢ A→B"  (mem)       "A=A→B, Σ={B→C, A}"        ]
  [2 "A→B, B→C, A ⊢ A"    (mem)       "A=A, Σ={A→B, B→C}"        ]
  [3 "A→B, B→C, A ⊢ B"    (impl- 1 2) "A=A, B=B, Σ={A→B, B→C, A}"]
  [4 "A→B, B→C, A ⊢ B→C"  (mem)       "A=B→C, Σ={A→B, A}"        ]
  [5 "A→B, B→C, A ⊢ C"    (impl- 4 3) "A=B, B=C, Σ={A→B, B→C, A}"]
  [6 "A→B, B→C ⊢ A→C"     (impl+ 5)   "A=A, B=C, Σ={A→B, B→C}"   ]
)))
(define Hyp-proof-auto2 (mk-fd-proof  '(
  [1 "A→B, B→C, A ⊢ A→B"   (mem)      ]
  [2 "A→B, B→C, A ⊢ A"     (mem)      ]
  [3 "A→B, B→C, A ⊢ B"     (impl- 1 2)]
  [4 "A→B, B→C, A ⊢ B→C"   (mem)      ]
  [5 "A→B, B→C, A ⊢ C"     (impl- 4 3)]
  [6 "A→B, B→C ⊢ A→C"      (impl+ 5)  ]
)))
(define Bad-proof-subs (mk-fd-proof '(
  [S1 "A→B, B→C, A ⊢ A→B" (mem)         "A=A→B, Σ={B→C, A}"      ]
  [S2 "A→B, B→C, A ⊢ B"   (mem)         "A=A, Σ={A→B,B→C}"       ]
  [S3 "A→B, B→C, A ⊢ B"   (impl- S1 S2) "A=A, B=B, Σ={A→B,B→C,A}"]
  [S4 "A→B, B→C, A ⊢ B→C" (mem)         "A=B→C, Σ={A→B,A}"       ]
  [S5 "A→B, B→C, A ⊢ C"   (impl- S4 S3) "A=B, B=C, Σ={A→B,B→C,A}"]
  [S6 "A→B, B→C ⊢ A→C"    (impl+ S5)    "A=A, B=C, Σ={A→B,B→C}"  ]
)))
(define Bad-proof-auto (mk-fd-proof '(
  [S1 "A→B, B→C, A ⊢ A→B" (mem)        ]
  [S2 "A→B, B→C, A ⊢ B"   (mem)        ]
  [S3 "A→B, B→C, A ⊢ B"   (impl- S1 S2)]
  [S4 "A→B, B→C, A ⊢ B→C" (mem)        ]
  [S5 "A→B, B→C, A ⊢ C"   (impl- S4 S3)]
  [S6 "A→B, B→C ⊢ A→C"    (impl+ S5)   ]
)))
       
(define (test-proof-and-report name proof expected)
  (printf "Checking ~a ========~n" name)
  (let ([result (fd-check-proof (cons th-mem axioms-Lp) proof #:verbose? #t)])
    (if (equal? result expected)
      (printf "As expected!~n")
      (printf "***** Not Expected *****~n"))))

(test-proof-and-report "Checking Hyp-proof-subs" Hyp-proof-subs1 #t)
(test-proof-and-report "Checking Hyp-proof-auto" Hyp-proof-auto1 #t)
(test-proof-and-report "Checking Hyp-proof-subs" Hyp-proof-subs2 #t)
(test-proof-and-report "Checking Hyp-proof-auto" Hyp-proof-auto2 #t)
(test-proof-and-report "Checking Bad-proof-subs" Bad-proof-subs  #f)
(test-proof-and-report "Checking Bad-proof-auto" Bad-proof-auto  #f)
)