;;;
;;; This file contains the data access functions for
;;; the logical formulas of the propositional calculus as a
;;; symbolic data domain as described in chapter 4 of the text.
;;;
;;; -------------------------------------
;;; The recognizers.
;;;
proposition-p[formula] = symbolp[formula]

negation-p[formula] =
  [symbolp[formula] --> F;
   otherwise --> endp[rest[rest[formula]]]]

conjunction-p[formula] =
  [symbolp[formula] --> F;
   endp[rest[rest[formula]]] --> F;
   otherwise --> eq[second[formula]; "AND"]]

disjunction-p[formula] =
  [symbolp[formula] --> F;
   endp[rest[rest[formula]]] --> F;
   otherwise --> eq[second[formula]; "OR"]]

implication-p[formula] =
  [symbolp[formula] --> F;
   endp[rest[rest[formula]]] --> F;
   otherwise --> eq[second[formula]; "IMPLIES"]]

equivalence-p[formula] =
  [symbolp[formula] --> F;
   endp[rest[rest[formula]]] --> F;
   otherwise --> eq[second[formula]; "EQUIV"]]

;;;
;;; The selector and constructor for negations.
;;;
negend[formula] = second[formula]

make-negation[negend] = list2["NOT"; negend]

;;;
;;; Selectors and constructor for conjunctions.
;;;
conjunct1[formula] = first[formula]

conjunct2[formula] = third[formula]

make-conjunction[conj1; conj2] = list3[conj1; "AND"; conj2]

;;;
;;; Selectors and constructor for disjunctions.
;;;
disjunct1[formula] = first[formula]

disjunct2[formula] = third[formula]

make-disjunction[disj1; disj2] = list3[disj1; "OR"; disj2]

;;;
;;; Selectors and constructor for implications.
;;;
antecedent[formula] = first[formula]

consequent[formula] = third[formula]

make-implication[ante; conseq] = list3[ante; "IMPLIES"; conseq]

;;;
;;; Selectors and constructor for conditionals.
;;;
condition1[formula] = first[formula]

condition2[formula] = third[formula]

make-equivalence[cond1; cond2] = list3[cond1; "EQUIV"; cond2]

;;;
;;; Converter functions for propositions.
;;;
prop-name[proposition] = proposition

make-proposition[symbolic-atom] = symbolic-atom