;; 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 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
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, 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 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 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)))))))))