diff --git a/base-packages.lisp b/base-packages.lisp index dfc33a4..05d0068 100644 --- a/base-packages.lisp +++ b/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 diff --git a/eval.lisp b/eval.lisp index 13f1058..db5092b 100644 --- a/eval.lisp +++ b/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 diff --git a/parse.lisp b/parse.lisp index 9ab80f7..74ae3cb 100644 --- a/parse.lisp +++ b/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 - (= 1 (operator-argument-count oper)))) + (eq oper 'not)) (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 diff --git a/typeset.lisp b/typeset.lisp index 743b42a..e4f4e8f 100644 --- a/typeset.lisp +++ b/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