2024-09-04 03:14:57 -07:00
|
|
|
|
;; parse.lisp -- Proposition string parsing subroutines
|
|
|
|
|
;; 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)
|
|
|
|
|
|
|
|
|
|
(defun whitespace-p (char)
|
|
|
|
|
"Return nil unless CHAR is whitespace."
|
|
|
|
|
(member char '(#\newline #\space) :test 'eq))
|
|
|
|
|
|
|
|
|
|
(defun paren-p (char)
|
|
|
|
|
"Return nil unless CHAR is a parenthesis."
|
|
|
|
|
(member char '(#\( #\))))
|
|
|
|
|
|
|
|
|
|
(defun delim-p (char)
|
|
|
|
|
"Return nil unless CHAR is either whitespace or a parenthesis."
|
|
|
|
|
(or (whitespace-p char) (paren-p char)))
|
|
|
|
|
|
|
|
|
|
(defun symbol-char-p (char)
|
|
|
|
|
"Return nil until CHAR is a valid character for use in proposition variable
|
|
|
|
|
names."
|
|
|
|
|
(or (alpha-char-p char) (eq char #\_) (digit-char-p char)))
|
|
|
|
|
|
|
|
|
|
(defun replace-in-string (str chars new-char)
|
|
|
|
|
"Replace all instances of any of CHARS in STR with NEW-CHAR."
|
|
|
|
|
(coerce (loop with lchars = (if (atom chars)
|
|
|
|
|
(list chars)
|
|
|
|
|
chars)
|
|
|
|
|
for char across str
|
|
|
|
|
when (member char lchars)
|
|
|
|
|
collect new-char
|
|
|
|
|
else
|
|
|
|
|
collect char)
|
|
|
|
|
'string))
|
|
|
|
|
|
|
|
|
|
(define-condition proposition-parse-error (error)
|
|
|
|
|
((position :initarg :position
|
|
|
|
|
:accessor parse-error-position
|
|
|
|
|
:initform nil)
|
|
|
|
|
(proposition :initarg :proposition
|
|
|
|
|
:accessor parse-error-proposition
|
|
|
|
|
:initform nil)
|
|
|
|
|
(message :initarg :message
|
|
|
|
|
:accessor parse-error-message
|
|
|
|
|
:initform nil))
|
|
|
|
|
(:report (lambda (con stream)
|
|
|
|
|
(with-slots (position proposition message) con
|
|
|
|
|
(format stream
|
|
|
|
|
"parse error~@[ at column ~d~]~@[: ~a~]~
|
|
|
|
|
~@[:~% ~a~@[~% ~a^~]~]"
|
|
|
|
|
(when position
|
|
|
|
|
(1+ position))
|
|
|
|
|
message
|
|
|
|
|
(when proposition
|
|
|
|
|
(replace-in-string proposition
|
|
|
|
|
'(#\newline #\return)
|
|
|
|
|
#\space))
|
|
|
|
|
(when position
|
|
|
|
|
(make-string position
|
|
|
|
|
:initial-element #\space))))))
|
|
|
|
|
(:documentation "Condition representing an error during parsing of a
|
|
|
|
|
proposition."))
|
|
|
|
|
|
|
|
|
|
(defparameter *operator-symbol-table*
|
|
|
|
|
'((open-paren "(")
|
|
|
|
|
(close-paren ")")
|
|
|
|
|
(and "/\\" "and" "&&" "&" "∧" ".")
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(nand "nand" "↑" "⊼" "~&" "~&&" "!&" "!&&")
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(or "\\/" "or" "||" "|" "∥" "+" "∨")
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(nor "nor" "↓" "⊽" "~|" "~||" "!|" "!||")
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(xor "xor" "⊕" "⊻" "↮" "≢" "^" "!=")
|
|
|
|
|
(not "¬" "~" "!" "not")
|
|
|
|
|
(implies "->" ">" "=>" "⇒" "⟹" "→" "⊃" "implies")
|
|
|
|
|
(converse "<-" "<" "<=" "←" "⇐" "⟸" "⊂" "converse")
|
|
|
|
|
(iff "<->" "<>" "<=>" "⇔" "↔" "≡" "iff" "=" "==" "xnor" "⊙"))
|
|
|
|
|
"Alist table of operator symbols and their possible string representations.")
|
|
|
|
|
|
2024-09-16 03:08:29 -07:00
|
|
|
|
(defun alpha-string-p (str)
|
|
|
|
|
"Return t if STR is only alphabetical characters."
|
|
|
|
|
(not (find-if-not 'alpha-char-p str)))
|
|
|
|
|
|
|
|
|
|
(defparameter *longest-non-alpha-operator*
|
|
|
|
|
(apply 'max (mapcar
|
|
|
|
|
(lambda (entry)
|
|
|
|
|
(apply 'max
|
|
|
|
|
(mapcar 'length
|
|
|
|
|
(remove-if 'alpha-string-p (cdr entry)))))
|
|
|
|
|
*operator-symbol-table*))
|
|
|
|
|
"The longest operator in `*operator-symbol-table*' such that `alpha-string-p'
|
|
|
|
|
returns t.")
|
|
|
|
|
|
2024-09-16 02:38:09 -07:00
|
|
|
|
(defparameter *operator-descriptions* ;; noindent 30
|
|
|
|
|
`((open-paren ("open parenthesis")
|
|
|
|
|
,(format nil "Used in combination with a close parenthesis to denote ~
|
|
|
|
|
some terms to be evaluated before the surrounding terms.")
|
|
|
|
|
(((and (or true true) false) . false)
|
|
|
|
|
((or true (and true false)) . true)))
|
|
|
|
|
(close-paren ("close parenthesis")
|
|
|
|
|
"Used to close a group started with an open parenthesis."
|
|
|
|
|
()) ;; no examples for closed paren
|
|
|
|
|
(and ("and" "conjunction")
|
|
|
|
|
,(format nil "Evaluate to true only if the expressions to the left and ~
|
|
|
|
|
right evaluate to true.")
|
|
|
|
|
(((and true true) . true)
|
|
|
|
|
((and true false) . false)))
|
|
|
|
|
(nand ("nand" "non-conjunction")
|
|
|
|
|
,(format nil "Evaluate to true unless the expressions to the left and ~
|
|
|
|
|
right are both true. This is the negation of the 'and' operator.")
|
|
|
|
|
(((nand true true) . false)
|
|
|
|
|
((nand true false) . true)
|
|
|
|
|
((nand false false) . true)))
|
|
|
|
|
(or ("or" "disjunction")
|
|
|
|
|
,(format nil "Evaluate to true if the expression to the left is true, the ~
|
|
|
|
|
expression to the right is true, or both the left and right expressions are ~
|
|
|
|
|
true.")
|
|
|
|
|
(((or true true) . true)
|
|
|
|
|
((or true false) . true)
|
|
|
|
|
((or false false) . false)))
|
|
|
|
|
(nor ("nor" "non-disjunction")
|
|
|
|
|
,(format nil "Evaluate to true if the expressions to the left and right ~
|
|
|
|
|
are both false. This is the negation of the 'or' operator.")
|
|
|
|
|
(((nor true true) . false)
|
|
|
|
|
((nor true false) . false)
|
|
|
|
|
((nor false false) . true)))
|
|
|
|
|
(xor ("exclusive or" "exclusive disjunction") ;; noindent 30
|
|
|
|
|
,(format nil "Evaluate to true if the expression to the left is true or ~
|
|
|
|
|
if the expression to the right is true, but not if both of them are true.")
|
|
|
|
|
(((xor true true) . false)
|
|
|
|
|
((xor true false) . true)))
|
|
|
|
|
(not ("not" "negation")
|
|
|
|
|
,(format nil "Evaluate to false if the expression to the left evaluates ~
|
|
|
|
|
to true, and evaluate to true if the expression to the left evaluates to ~
|
|
|
|
|
false. This is a unary operator (it only applies to the expression following ~
|
|
|
|
|
it).")
|
|
|
|
|
(((not true) . false)
|
|
|
|
|
((not false) . true)))
|
|
|
|
|
(implies ("implies" "conditional")
|
|
|
|
|
,(format nil "Evaluate to false if the expression to the left evaluates ~
|
|
|
|
|
to true and the expressions to the right evaluates to false. Otherwise, ~
|
|
|
|
|
evaluate to true.")
|
|
|
|
|
(((implies true true) . true)
|
|
|
|
|
((implies true false) . false)
|
|
|
|
|
((implies false true) . true)
|
|
|
|
|
((implies false false) . true)))
|
|
|
|
|
(converse ("converse")
|
|
|
|
|
,(format nil "Evaluate to false if the expression to the right evaluates ~
|
|
|
|
|
to true and the expression to the left evaluates to false. Otherwise, evaluate ~
|
|
|
|
|
to true. This is the 'implies' operator with its arguments flipped.")
|
|
|
|
|
(((implies true true) . true)
|
|
|
|
|
((implies true false) . true)
|
|
|
|
|
((implies false true) . false)
|
|
|
|
|
((implies false false) . true)))
|
|
|
|
|
(iff ("biconditional" "equivalent")
|
|
|
|
|
,(format nil "Evaluate to true if the expressions to the left and rigt ~
|
|
|
|
|
evaluate to the same value. That is, they are both true or both false.")
|
|
|
|
|
(((iff true true) . true)
|
|
|
|
|
((iff true false) . false)
|
|
|
|
|
((iff false false) . true))))
|
|
|
|
|
"Alist table of operator symbols and their descriptions. The format of this
|
|
|
|
|
list is SYMBOL NAMES DESCRIPTION (&rest (EXAMPLE LEFT . EXAMPLE RIGHT)). These
|
|
|
|
|
are useful for use in things like syntax explanation messages.")
|
|
|
|
|
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(defun operator-symbol (oper-str)
|
|
|
|
|
"Return the symbol for OPER-STR, or nil if it is not a know operator."
|
|
|
|
|
(loop for (oper-sym . strs) in *operator-symbol-table*
|
|
|
|
|
when (member oper-str strs :test 'equalp)
|
|
|
|
|
do (return oper-sym)))
|
|
|
|
|
|
|
|
|
|
(defun operator-precedence (oper)
|
|
|
|
|
"Return the precedence for OPER."
|
|
|
|
|
(case oper
|
|
|
|
|
(not 1)
|
|
|
|
|
(and 2)
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(implicit-and 2)
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(nand 2)
|
|
|
|
|
(xor 3)
|
|
|
|
|
(or 4)
|
|
|
|
|
(nor 4)
|
|
|
|
|
(implies 5)
|
|
|
|
|
(converse 5)
|
|
|
|
|
(iff 6)
|
|
|
|
|
(open-paren most-positive-fixnum)
|
|
|
|
|
(t nil)))
|
|
|
|
|
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(defun unary-p (oper)
|
|
|
|
|
"Return whether OPER is a unary operator or not."
|
2024-09-10 23:05:14 -07:00
|
|
|
|
(eq oper 'not))
|
2024-09-06 14:20:13 -07:00
|
|
|
|
|
2024-09-16 04:17:24 -07:00
|
|
|
|
(defparameter *operand-symbol-table*
|
|
|
|
|
'((true "t" "true" "⊤" "1")
|
|
|
|
|
(false "f" "false" "⊥" "0"))
|
|
|
|
|
"Alist mapping operand symbols (true and false) to their textual
|
|
|
|
|
representations.")
|
|
|
|
|
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(defun interpret-operand (oper-str)
|
|
|
|
|
"Return a symbol representing OPER-STR, or the string itself if it represents
|
|
|
|
|
a variable."
|
2024-09-16 04:17:24 -07:00
|
|
|
|
(dolist (entry *operand-symbol-table*)
|
|
|
|
|
(when (member oper-str (cdr entry) :test 'equalp)
|
|
|
|
|
(return-from interpret-operand (car entry))))
|
|
|
|
|
;; check if OPER-STR is a valid variable name
|
|
|
|
|
(if (or (zerop (length oper-str))
|
|
|
|
|
(find-if-not 'symbol-char-p oper-str))
|
|
|
|
|
nil
|
|
|
|
|
oper-str))
|
2024-09-04 03:14:57 -07:00
|
|
|
|
|
|
|
|
|
(defun string-first-char-safe (str)
|
|
|
|
|
"Return the first character of STR, or nil if it is empty."
|
|
|
|
|
(unless (zerop (length str))
|
|
|
|
|
(elt str 0)))
|
|
|
|
|
|
2024-09-16 03:08:29 -07:00
|
|
|
|
(defun try-find-operator-for-token (token)
|
|
|
|
|
"Return the operator symbol for TOKEN, if it is an operator. As a second
|
|
|
|
|
value, return the matched portion of TOKEN. If no match is found, return
|
|
|
|
|
(values nil nil)."
|
|
|
|
|
(loop for len downfrom (min *longest-non-alpha-operator* (length token)) to 1
|
|
|
|
|
for cur-test = (subseq token 0 len)
|
|
|
|
|
for oper-sym = (operator-symbol cur-test)
|
|
|
|
|
when oper-sym do
|
|
|
|
|
(return-from try-find-operator-for-token
|
|
|
|
|
(values oper-sym cur-test)))
|
|
|
|
|
(values nil nil))
|
|
|
|
|
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(defun next-symbol-token (str &key multi-char-names)
|
|
|
|
|
"Return the next token from STR that is not a paren. If MULTI-CHAR-NAMES is
|
|
|
|
|
non-nil, allow names to be more than one character long."
|
|
|
|
|
(loop with mode = (if (symbol-char-p (elt str 0))
|
|
|
|
|
'alpha
|
|
|
|
|
'sym)
|
|
|
|
|
for char across str
|
|
|
|
|
for chari from 0
|
|
|
|
|
while (or (and (eq mode 'alpha) (symbol-char-p char))
|
|
|
|
|
(and (eq mode 'sym) (not (symbol-char-p char))
|
|
|
|
|
(not (delim-p char))))
|
|
|
|
|
collect char into token
|
|
|
|
|
finally
|
|
|
|
|
(let ((str (coerce token 'string)))
|
|
|
|
|
(return
|
2024-09-06 14:58:47 -07:00
|
|
|
|
(string
|
|
|
|
|
(cond
|
2024-09-16 03:08:29 -07:00
|
|
|
|
;; operator
|
|
|
|
|
((multiple-value-bind (sym match)
|
|
|
|
|
(try-find-operator-for-token str)
|
|
|
|
|
(declare (ignorable sym))
|
|
|
|
|
match))
|
|
|
|
|
;; multi-char variable, constant (true or false)
|
2024-09-06 14:58:47 -07:00
|
|
|
|
((or multi-char-names
|
2024-09-04 03:14:57 -07:00
|
|
|
|
(symbolp (interpret-operand str)))
|
2024-09-06 14:58:47 -07:00
|
|
|
|
str)
|
|
|
|
|
;; single letter variable (multi-char-names is off)
|
|
|
|
|
(t (first token))))))))
|
2024-09-04 03:14:57 -07:00
|
|
|
|
|
|
|
|
|
(defun next-token (str &key multi-char-names)
|
|
|
|
|
"Return a list of the next token in STR and how much whitespace it had."
|
|
|
|
|
(let ((whitespace-chars 0))
|
|
|
|
|
(loop for char across str
|
|
|
|
|
while (whitespace-p char) do
|
|
|
|
|
(setq whitespace-chars (1+ whitespace-chars)))
|
|
|
|
|
(setq str (subseq str whitespace-chars))
|
|
|
|
|
(let ((next-char (string-first-char-safe str)))
|
|
|
|
|
(cond
|
|
|
|
|
((not next-char)
|
|
|
|
|
(list nil whitespace-chars))
|
|
|
|
|
((paren-p next-char)
|
|
|
|
|
(list (string next-char) whitespace-chars))
|
|
|
|
|
(t
|
|
|
|
|
(let ((token (next-symbol-token str :multi-char-names multi-char-names)))
|
|
|
|
|
(list token whitespace-chars)))))))
|
|
|
|
|
|
|
|
|
|
(defmacro dotokens ((var pos-var str &optional (retval nil retvalp))
|
|
|
|
|
(&key multi-char-names &allow-other-keys)
|
|
|
|
|
&body body)
|
|
|
|
|
"Execute BODY once with VAR bound to each token in STR. Optionally, return
|
|
|
|
|
RETVAL. The position of each token will be stored in POS-VAR. If
|
|
|
|
|
MULTI-CHAR-NAMES is enabled, allow multiple characters in variable names."
|
|
|
|
|
(let ((stream-var (gensym))
|
|
|
|
|
(token-start-var (gensym))
|
|
|
|
|
(token-var (gensym))
|
|
|
|
|
(read-chars-var (gensym))
|
|
|
|
|
(whitespace-var (gensym)))
|
|
|
|
|
`(loop for ,stream-var = ,str then (subseq ,str ,read-chars-var)
|
|
|
|
|
for (,token-var ,whitespace-var)
|
|
|
|
|
= (next-token ,stream-var :multi-char-names ,multi-char-names)
|
|
|
|
|
for ,token-start-var = ,whitespace-var
|
|
|
|
|
then (+ ,read-chars-var ,whitespace-var)
|
|
|
|
|
for ,read-chars-var = (+ ,whitespace-var (length ,token-var))
|
|
|
|
|
then (+ ,read-chars-var ,whitespace-var (length ,token-var))
|
|
|
|
|
while ,token-var do
|
|
|
|
|
(let ((,var ,token-var)
|
|
|
|
|
(,pos-var ,token-start-var))
|
|
|
|
|
(declare (ignorable ,pos-var))
|
|
|
|
|
,@body)
|
|
|
|
|
finally
|
|
|
|
|
(return ,(when retvalp
|
|
|
|
|
retval)))))
|
|
|
|
|
|
|
|
|
|
(defun interpret-token (token)
|
|
|
|
|
"Return a list of the form (type value), where type is one of: `operator' or
|
|
|
|
|
`operand', and value is the tokens value, as returned by `operator-symbol' or
|
|
|
|
|
`interpret-operand'. If the token is of an unknown type, return a list of (nil
|
|
|
|
|
nil)."
|
|
|
|
|
(let ((operator-value (operator-symbol token)))
|
|
|
|
|
(if operator-value
|
|
|
|
|
(list 'operator operator-value)
|
|
|
|
|
(let ((operand-value (interpret-operand token)))
|
|
|
|
|
(if operand-value
|
|
|
|
|
(list 'operand operand-value)
|
|
|
|
|
(list nil nil))))))
|
|
|
|
|
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(defun parse-proposition-string (prop-str &key (implicit-and t) multi-char-names)
|
|
|
|
|
"Parse PROP-STR, which is a proposition string.
|
2024-09-04 03:14:57 -07:00
|
|
|
|
The return value is the values set of the parsed string, and the list of all
|
|
|
|
|
found variables."
|
|
|
|
|
(let ((found-vars '())
|
|
|
|
|
(operators '())
|
|
|
|
|
(operands '())
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(paren-operands (list 0)))
|
|
|
|
|
(labels ((peek-operator ()
|
|
|
|
|
(destructuring-bind (&optional value . pos) (car operators)
|
|
|
|
|
(values value pos)))
|
|
|
|
|
(pop-operator ()
|
|
|
|
|
(destructuring-bind (&optional value . pos) (pop operators)
|
|
|
|
|
(values value pos)))
|
|
|
|
|
(convert-implicit-and (this-name pos)
|
|
|
|
|
(multiple-value-bind (value top-pos) (peek-operator)
|
|
|
|
|
(when (eq value 'implicit-and)
|
|
|
|
|
(unless implicit-and
|
|
|
|
|
(cerror "Insert implicit AND operator"
|
|
|
|
|
'proposition-parse-error
|
|
|
|
|
:position pos
|
|
|
|
|
:proposition prop-str
|
|
|
|
|
:message
|
|
|
|
|
(format nil "expected binary operator, found ~a"
|
|
|
|
|
this-name)))
|
|
|
|
|
(pop-operator)
|
|
|
|
|
(push (cons 'and top-pos) operators))))
|
|
|
|
|
(apply-one-operator ()
|
|
|
|
|
(multiple-value-bind (oper pos) (pop-operator)
|
|
|
|
|
(when (not oper)
|
|
|
|
|
(error 'proposition-parse-error :message "no more operators"
|
|
|
|
|
:position pos
|
|
|
|
|
:proposition prop-str))
|
2024-09-10 23:05:14 -07:00
|
|
|
|
(let ((oper-args (if (unary-p oper) 1 2))
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(cur-operands (list (pop operands))))
|
|
|
|
|
(when (not (car cur-operands))
|
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
:position pos
|
|
|
|
|
:proposition prop-str
|
|
|
|
|
:message
|
|
|
|
|
(format nil "~A expects ~D arguments, found none"
|
|
|
|
|
oper oper-args)))
|
|
|
|
|
(when (= oper-args 2)
|
|
|
|
|
(push (pop operands) cur-operands)
|
|
|
|
|
(when (not (car cur-operands))
|
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
:position pos
|
|
|
|
|
:proposition prop-str
|
|
|
|
|
:message
|
|
|
|
|
(format nil "~A expects ~D arguments, found 1"
|
|
|
|
|
oper oper-args))))
|
|
|
|
|
(push (cons oper cur-operands) operands))))
|
|
|
|
|
(apply-lower-precedent (prec)
|
|
|
|
|
(loop for top-oper = (peek-operator)
|
|
|
|
|
while (and top-oper
|
|
|
|
|
(<= (or (operator-precedence top-oper)
|
|
|
|
|
most-positive-fixnum)
|
|
|
|
|
prec)
|
|
|
|
|
(not (unary-p top-oper)))
|
|
|
|
|
do (apply-one-operator)))
|
|
|
|
|
(apply-all-unary ()
|
|
|
|
|
(loop while (unary-p (peek-operator))
|
|
|
|
|
do
|
|
|
|
|
(apply-one-operator)))
|
|
|
|
|
(push-operator (oper token-pos)
|
|
|
|
|
(apply-lower-precedent (operator-precedence oper))
|
|
|
|
|
(push (cons oper token-pos) operators)))
|
|
|
|
|
(dotokens (token-str token-pos prop-str)
|
2024-09-05 14:46:05 -07:00
|
|
|
|
(:multi-char-names multi-char-names)
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(destructuring-bind (type value) (interpret-token token-str)
|
2024-09-05 14:46:05 -07:00
|
|
|
|
(cond
|
2024-09-06 14:20:13 -07:00
|
|
|
|
;; unknown token
|
2024-09-05 14:46:05 -07:00
|
|
|
|
((not type)
|
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
:position token-pos
|
2024-09-06 14:20:13 -07:00
|
|
|
|
:proposition prop-str
|
2024-09-05 14:46:05 -07:00
|
|
|
|
:message "unknown token"))
|
|
|
|
|
;; operand
|
|
|
|
|
((eq type 'operand)
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(convert-implicit-and "operand" token-pos)
|
2024-09-05 14:46:05 -07:00
|
|
|
|
(unless (member value '(true false))
|
|
|
|
|
(pushnew value found-vars :test 'equal))
|
|
|
|
|
(push value operands)
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(incf (car paren-operands))
|
|
|
|
|
(apply-all-unary)
|
|
|
|
|
(convert-implicit-and "operand" token-pos)
|
|
|
|
|
(push-operator 'implicit-and token-pos))
|
|
|
|
|
;; open parenthesis
|
2024-09-05 14:46:05 -07:00
|
|
|
|
((eq value 'open-paren)
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(convert-implicit-and "open parenthesis" token-pos)
|
|
|
|
|
(push (cons value token-pos) operators)
|
|
|
|
|
(push 0 paren-operands))
|
|
|
|
|
;; close parenthesis
|
2024-09-05 14:46:05 -07:00
|
|
|
|
((eq value 'close-paren)
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(when (eq (peek-operator) 'implicit-and)
|
|
|
|
|
(pop-operator))
|
|
|
|
|
(loop while (not (eq (peek-operator) 'open-paren))
|
2024-09-05 14:46:05 -07:00
|
|
|
|
when (null operators) do
|
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
:position token-pos
|
2024-09-06 14:20:13 -07:00
|
|
|
|
:proposition prop-str
|
2024-09-05 14:46:05 -07:00
|
|
|
|
:message "no matching open parenthesis")
|
2024-09-06 14:20:13 -07:00
|
|
|
|
do (apply-one-operator))
|
|
|
|
|
(when (zerop (pop paren-operands))
|
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
;; open paren position
|
|
|
|
|
:position (cdr (pop operators))
|
|
|
|
|
:proposition prop-str
|
|
|
|
|
:message "empty parenthesis"))
|
|
|
|
|
;; remove open paren
|
|
|
|
|
(pop-operator)
|
|
|
|
|
(apply-all-unary)
|
|
|
|
|
(convert-implicit-and "close parenthesis" token-pos)
|
|
|
|
|
(push-operator 'implicit-and token-pos))
|
2024-09-05 14:46:05 -07:00
|
|
|
|
;; operator
|
|
|
|
|
(t
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(if (eq (peek-operator) 'implicit-and)
|
|
|
|
|
(if (unary-p value)
|
|
|
|
|
(convert-implicit-and "unary operator" token-pos)
|
|
|
|
|
(pop-operator))
|
|
|
|
|
(unless (unary-p value)
|
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
:position token-pos
|
|
|
|
|
:proposition prop-str
|
|
|
|
|
:message "expected operand, found operator")))
|
|
|
|
|
(push-operator value token-pos)))))
|
|
|
|
|
;; remove implicit-and
|
|
|
|
|
(when (eq 'implicit-and (peek-operator))
|
|
|
|
|
(pop-operator))
|
|
|
|
|
(loop for (top-oper . top-pos) = (car operators)
|
|
|
|
|
while top-oper
|
|
|
|
|
when (eq top-oper 'open-paren) do
|
2024-09-05 14:46:05 -07:00
|
|
|
|
(error 'proposition-parse-error
|
|
|
|
|
:message "no matching closing parenthesis"
|
2024-09-06 14:20:13 -07:00
|
|
|
|
:proposition prop-str
|
|
|
|
|
:position top-pos)
|
2024-09-05 14:46:05 -07:00
|
|
|
|
do
|
2024-09-06 14:20:13 -07:00
|
|
|
|
(apply-one-operator))
|
2024-09-05 14:46:05 -07:00
|
|
|
|
;; return variables in the order we found them
|
|
|
|
|
(values (car operands) (nreverse found-vars)))))
|