Fix incorrect parenthesis

base-packages.lisp

@@ -39,6 +39,7 @@
    #:*operator-unicode-lookup-alist*
    #:*operator-latex-lookup-alist*
    #:latex-var-name-transform
+   #:flatten-proposition
    #:typeset-proposition
    #:convert-truth-table-to-latex
    #:convert-truth-table-to-html

eval.lisp

@@ -29,6 +29,21 @@
   (:documentation "Condition representing an error that occurred during
 evaluation for a proposition."))
 
+(defun operator-argument-count (oper)
+  "Return the minimum number of arguments that OPER takes as the first value,
+and the maximum number (or nil for infinity) as a second value."
+  (case oper
+    (and (values 1 nil))
+    (or (values 1 nil))
+    (xor (values 1 nil))
+    (not (values 1 1))
+    (implies (values 2 2))
+    (converse (values 2 2))
+    (iff (values 2 2))
+    (nand (values 1 nil))
+    (nor (values 1 nil))
+    (t (error "unknown operator: ~S" oper))))
+
 (defun logical-xor (&rest args)
   "Logical xor (not equal) each argument in turn with its following argument.
 NOTE: This is NOT a macro, there is no short circuit evaluation (all arguments

parse.lisp

@@ -108,26 +108,9 @@ proposition."))
     (open-paren most-positive-fixnum)
     (t nil)))
 
-(defun operator-argument-count (oper)
-  "Return the minimum number of arguments that OPER takes as the first value,
-and the maximum number (or nil for infinity) as a second value."
-  (case oper
-    (and (values 2 nil))
-    (or (values 2 nil))
-    (xor (values 2 nil))
-    (not (values 1 1))
-    (implies (values 2 2))
-    (converse (values 2 2))
-    (iff (values 2 2))
-    (nand (values 2 nil))
-    (nor (values 2 2))
-    (open-paren (values 0 0))
-    (t (error "unknown operator: ~S" oper))))
-
 (defun unary-p (oper)
   "Return whether OPER is a unary operator or not."
-  (when oper
+  (eq oper 'not))
-    (= 1 (operator-argument-count oper))))
 
 (defun interpret-operand (oper-str)
   "Return a symbol representing OPER-STR, or the string itself if it represents
@@ -267,7 +250,7 @@ found variables."
                    (error 'proposition-parse-error :message "no more operators"
                                                    :position pos
                                                    :proposition prop-str))
-                 (let ((oper-args (operator-argument-count oper))
+                 (let ((oper-args (if (unary-p oper) 1 2))
                        (cur-operands (list (pop operands))))
                    (when (not (car cur-operands))
                      (error 'proposition-parse-error

typeset.lisp

@@ -117,11 +117,41 @@
                              else
                                collect char)))
 
+(defun flattenable-p (oper)
+  "Return t if OPER is able to be flattened. That is, it does not care a bout
+argument ordering."
+  (multiple-value-bind (min max)
+      (operator-argument-count oper)
+    (declare (ignorable min))
+    ;; currently, all unordered operators take any number of arguments max, and
+    ;; all ordered operators have some max number of arguments (as a
+    ;; proposition: an operator is unordered if and only if it takes any number
+    ;; of arguments)
+    (not max)))
+
+(defun flatten-proposition (prop)
+  "Flatten PROP, such that adjacent operators with the same precedence and with
+no ordering (such as \"and\" or \"or\") are not surrounded by parenthesis when
+typeset."
+  (if (consp prop)
+      (loop with my-oper = (car prop)
+            for raw-sub-expr in (cdr prop)
+            for sub-expr = (flatten-proposition raw-sub-expr)
+            when (and (flattenable-p my-oper)
+                      (consp sub-expr)
+                      (eq (car sub-expr) my-oper))
+              append (cdr sub-expr) into out-args
+            else
+              collect sub-expr into out-args
+            finally (return (cons my-oper out-args)))
+      prop))
+
 (defun typeset-proposition (expr &key
                                    (lookup-table *operator-ascii-lookup-alist*)
                                    var-name-transform
                                    (parent-prec most-positive-fixnum)
-                                   latin-truths)
+                                   latin-truths
+                                   (flatten-prop t))
   "Typeset the propositional expression EXPR to plain text.  LOOKUP-TABLE should
 be a table mapping operators to their textual representation. VAR-NAME-TRANSFORM
 (if non-nil) should take a single string argument which is a variable name and
@@ -147,10 +177,13 @@ use (it controls when parentheses are applied.)"
          (cdr (assoc 'false lookup-table))))
     ;; expr is a compound expression
     (t
-     (destructuring-bind (oper first-arg &rest args) expr
+     (destructuring-bind (oper first-arg &rest args)
+         (if flatten-prop
+             (flatten-proposition expr)
+             expr)
        (let* ((our-prec (operator-precedence oper))
               (oper-ascii (cdr (assoc oper lookup-table)))
-              (prefix-suffix (if (< parent-prec our-prec)
+              (prefix-suffix (if (<= parent-prec our-prec)
                                  (cons (cdr (assoc 'open-paren lookup-table))
                                        (cdr (assoc 'close-paren lookup-table)))
                                  '("" . ""))))
@@ -161,7 +194,8 @@ use (it controls when parentheses are applied.)"
                                           :lookup-table lookup-table
                                           :var-name-transform var-name-transform
                                           :latin-truths latin-truths
-                                          :parent-prec our-prec)
+                                          :parent-prec our-prec
+                                          :flatten-prop nil)
                      (cdr prefix-suffix))
              ;; we have many arguments
              (loop for arg in args
@@ -171,19 +205,20 @@ use (it controls when parentheses are applied.)"
                                         :lookup-table lookup-table
                                         :var-name-transform var-name-transform
                                         :latin-truths latin-truths
-                                        :parent-prec our-prec)
+                                        :parent-prec our-prec
+                                        :flatten-prop nil)
                      into output
                    finally
                       (push (typeset-proposition first-arg
                                                  :lookup-table lookup-table
                                                  :var-name-transform var-name-transform
                                                  :latin-truths latin-truths
-                                                 :parent-prec our-prec)
+                                                 :parent-prec our-prec
+                                                 :flatten-prop nil)
                             output)
                       (return (format nil "~A~{~A~^ ~}~A" (car prefix-suffix)
                                       output (cdr prefix-suffix))))))))))
 
-
 (defun convert-truth-table-to-latex (table &key pretty-print latin-truths)
   "Convert TABLE, which should be a truth table as returned by
 `create-truth-table' to latex. If PRETTY-PRINT, add newlines to make the