161 lines
6.5 KiB
Common Lisp
161 lines
6.5 KiB
Common Lisp
|
;; eval.lisp -- Evaluate parsed proposition strings
|
||
|
|
;; Copyright (C) 2024 Alexander Rosenberg
|
||
|
|
;;
|
||
|
|
;; This program is free software: you can redistribute it and/or modify
|
||
|
|
;; it under the terms of the GNU General Public License as published by
|
||
|
|
;; the Free Software Foundation, either version 3 of the License, or
|
||
|
|
;; (at your option) any later version.
|
||
|
|
;;
|
||
|
|
;; This program is distributed in the hope that it will be useful,
|
||
|
|
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||
|
|
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||
|
|
;; GNU General Public License for more details.
|
||
|
|
;;
|
||
|
|
;; You should have received a copy of the GNU General Public License
|
||
|
|
;; along with this program. If not, see <https://www.gnu.org/licenses/>.
|
||
|
|
(in-package :truth-table/base)
|
||
|
|
|
||
|
|
(define-condition proposition-eval-error (error)
|
||
|
|
((message :initarg :message
|
||
|
|
:accessor proposition-eval-error-message)
|
||
|
|
(proposition :initarg :proposition
|
||
|
|
:accessor proposition-eval-error-proposition
|
||
|
|
:initform nil))
|
||
|
|
(:report (lambda (con stream)
|
||
|
|
(with-slots (message proposition)
|
||
|
|
con
|
||
|
|
(format stream "~a~@[:~% ~a~]"
|
||
|
|
message proposition))))
|
||
|
|
(: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 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))
|
||
|
|
(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, so all arguments, so there is no short circuit
|
||
|
|
evaluation (all arguments are evaluated no matter what)."
|
||
|
|
(loop with result = nil
|
||
|
|
for arg in args do
|
||
|
|
(setq result (not (eq result arg)))
|
||
|
|
finally (return result)))
|
||
|
|
|
||
|
|
(defun logical-and (&rest args)
|
||
|
|
"Logical and (all true).
|
||
|
|
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
|
||
|
|
evaluation (all arguments are evaluated no matter what)."
|
||
|
|
(not (member nil args)))
|
||
|
|
|
||
|
|
(defun logical-or (&rest args)
|
||
|
|
"Logical or (one or more true).
|
||
|
|
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
|
||
|
|
evaluation (all arguments are evaluated no matter what)."
|
||
|
|
(not (not (member t args))))
|
||
|
|
|
||
|
|
(defun logical-implies (prop1 prop2)
|
||
|
|
"Evaluate the logical implies operation on PROP1 and PROP2. That is \"if
|
||
|
|
PROP1, then PROP2\".
|
||
|
|
NOTE: This is NOT a macro, so all arguments, so there is no short circuit
|
||
|
|
evaluation (all arguments are evaluated no matter what)."
|
||
|
|
(if prop1 ;; only if first is true
|
||
|
|
prop2 ;; eval second
|
||
|
|
t)) ;; otherwise, just return true
|
||
|
|
|
||
|
|
(defun check-operator-argument-count (oper args)
|
||
|
|
"Raise an error if OPER cannot be called with ARGS."
|
||
|
|
(multiple-value-bind (min max) (operator-argument-count oper)
|
||
|
|
(let ((arg-count (length args)))
|
||
|
|
(cond
|
||
|
|
((< arg-count min)
|
||
|
|
(error 'proposition-eval-error
|
||
|
|
:message
|
||
|
|
(format nil "~s ~[takes no arguments~;requires one argument~:;~
|
||
|
|
requires at least ~:*~d arguments~], ~
|
||
|
|
but got ~[none~:;~:*~d~]"
|
||
|
|
oper min arg-count)))
|
||
|
|
((and max (> arg-count max))
|
||
|
|
(error 'proposition-eval-error
|
||
|
|
:message
|
||
|
|
(format nil "~s can take at most ~d argument~:p, but got ~d"
|
||
|
|
oper max arg-count)))))))
|
||
|
|
|
||
|
|
(defun keep-unique-expressions (mapping)
|
||
|
|
"Keep only unique expressions from MAPPING, which is an alist as returned by
|
||
|
|
`eval-proposition'."
|
||
|
|
(loop for entry in mapping
|
||
|
|
unless (assoc (car entry) output :test 'equal)
|
||
|
|
collect entry into output
|
||
|
|
finally (return output)))
|
||
|
|
|
||
|
|
(defun eval-proposition (prop vars)
|
||
|
|
"Evaluate the proposition PROP, with the alist VARS mapping variables to their
|
||
|
|
values. Return the result of the proposition as the first value, and an alist
|
||
|
|
mapping sub expressions to their results as the second value.
|
||
|
|
NOTE: the second value does not include individual variables, literal values
|
||
|
|
(true and false)."
|
||
|
|
(cond
|
||
|
|
;; prop is a variable name
|
||
|
|
((stringp prop)
|
||
|
|
(let ((entry (assoc prop vars :test 'equal)))
|
||
|
|
(unless entry
|
||
|
|
(error 'proposition-eval-error
|
||
|
|
:message (format nil "unknown variable: ~S~%" prop)))
|
||
|
|
(values (cdr entry) '())))
|
||
|
|
;; prop is true or false
|
||
|
|
((eq prop 'true)
|
||
|
|
(values t '()))
|
||
|
|
((eq prop 'false)
|
||
|
|
(values nil '()))
|
||
|
|
;; prop is a compound expression
|
||
|
|
(t
|
||
|
|
(loop with (oper . args) = prop
|
||
|
|
for arg in args
|
||
|
|
for (value sub-map) = (multiple-value-list
|
||
|
|
(eval-proposition arg vars))
|
||
|
|
nconc sub-map into mapping
|
||
|
|
collect value into arg-values
|
||
|
|
finally
|
||
|
|
(check-operator-argument-count oper args)
|
||
|
|
(let ((result
|
||
|
|
(case oper
|
||
|
|
;; avoid using the macros `and' and `or' so we can avoid
|
||
|
|
;; using `eval'
|
||
|
|
(and
|
||
|
|
(apply 'logical-and arg-values))
|
||
|
|
(nand
|
||
|
|
(not (apply 'logical-and arg-values)))
|
||
|
|
(or
|
||
|
|
(apply 'logical-or arg-values))
|
||
|
|
(nor
|
||
|
|
(not (apply 'logical-or arg-values)))
|
||
|
|
(xor
|
||
|
|
(apply 'logical-xor arg-values))
|
||
|
|
(not
|
||
|
|
(not (car arg-values)))
|
||
|
|
(implies
|
||
|
|
(logical-implies (car arg-values)
|
||
|
|
(second arg-values)))
|
||
|
|
(converse
|
||
|
|
;; this is just implies with the arguments flipped
|
||
|
|
(logical-implies (second arg-values)
|
||
|
|
(car arg-values)))
|
||
|
|
(iff
|
||
|
|
(eq (car arg-values) ;; both must have the same value
|
||
|
|
(second arg-values))))))
|
||
|
|
(return (values result
|
||
|
|
(keep-unique-expressions
|
||
|
|
(cons (cons prop result) mapping)))))))))
|