;    The top-level function CONVERT of this program takes a representation
;of a sentence in predicate logic, of a form described below, and returns
;a representation in clause form, with sets represented by lists.

;    It is assumed that the input has no free variables, that the only
;connectives are AND, OR, IMPLIES, and NOT.  You may assume that nested
;quantifiers never quantify variables of the same name.  You needn't check
;for ill-formed input sentences.


; This program uses the algorithm of p.145 of Rich & Knight, 2d edition
; After their step 4, scope information has been lost.  This may result in
;   extra arguments to Skolem functions.  This isn't wrong, really, but
;   just awkward.

; It is assumed that there are no nested quantifiers with same name
;   this condition could be detected with a little effort

; Assume the following grammar for statements, where
;      variables are symbols beginning with a question mark
;      other symbols are constants or relation names, depending
;        upon their position


;  Sentence -> QuantifiedSentence | CompoundSentence | PrimitiveSentence
;  QuantifiedSentence -> ( Quantifier Sentence )
;  Quantifier -> (forall Variable) | (exists Variable)
;  CompoundSentence -> (not Sentence) (and Sentence Sentence) |
;                      (or Sentence Sentence) (implies Sentence Sentence)
;  PrimitiveSentence -> ( PredicateConstant Terms )
;  Variables ->  Variable | Variable Variables


;  For ease of implementation, this program distinguishes unary
;    compound sentences (i.e., negations) from the rest


;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TEST DATA ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define d1 '((forall ?x) (implies (implies (p ?x) (q ?x)) (r ?x))))
(define d2 '((forall ?x) (implies (p ?x) (implies (q ?x) (r ?x)))))
(define d3 '(or ((forall ?x) (male ?x)) ((forall ?x) (female ?x))))
(define d4 '((forall ?z) (not ((forall ?y) (implies (p ?y ?z) (q ?y ?z))))))
(define d5 '(implies ((forall ?x) (implies (not (p ?x)) (not (q ?x))))
                     ((forall ?x) (implies (p ?x) (q ?x)))))
(define d6 '(and ((forall ?x) (implies (p ?x) ((exists ?y) (q ?x ?y))))
                 ((forall ?x) (implies ((exists ?y) (q ?x ?y)) (p ?x)))))
(define d7 '(or (not ((forall ?x) (implies (p ?x) ((exists ?y) (q ?x ?y)))))
                (not ((forall ?x) (implies ((exists ?y) (q ?x ?y)) (p ?x))))))
(define d8 '((forall ?a)
             ((forall ?b)
              ((forall ?c)
               (not ((forall ?d) (implies (p ?a ?b) (or (q ?c) (r ?d)))))))))
(define d9 '((exists ?a)
             ((forall ?b)
              ((exists ?c)
               ((forall ?d)
                ((exists ?e)
                 (and (and (p ?a ?b) (q ?c ?d)) (r ?e f))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TYPES ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Four types are assumed:  QUANTIFIED-SENTENCE (with subtypes EXISTENTIAL
;   and UNIVERSAL), NEGATED-SENTENCE, COMPOUND-SENTENCE (with subtypes
;   DISJUNCTION, CONJUNCTION, and IMPLICATION; note that NEGATED-SENTENCE,
;   being unary, is not considered a subtype), and ATOM


;;;;;;;;;;;;;;;;;;;; SELECTORS AND CONSTRUCTORS ;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;; for QUANTIFIED-SENTENCES ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Quantified sentences consist of a QUANTIFIER (itself consisting of
;   a QUANTIFIER-TYPE and a VARIABLE) and a QUANTIFIED sentence
; No type checking is done on the arguments to the selectors

(define (quantifier s) (car s))
(define (quantified s) (cadr s))
(define (quantifier-type s) (caar s))

(define (variable s) (cadar s))
(define (build-quantifier qt v) (list qt v))
(define (build-quantified q s) (list q s))

(define (quantified-sentence? s)
  (and (pair? s) (pair? (car s)) (member (caar s) '(forall exists))))
(define (existential? s)
  (and (quantified-sentence? s) (eq? (car (quantifier s)) 'exists)))


;;;;;;;;;;;;;;;;;;;; for COMPOUND-SENTENCES ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Compound sentences consist of a connective (AND, OR, or IMPLIES)
;   and two arguments ARG1 and ARG2, which are sentences

(define (connective s) (car s))
(define (arg1 s) (cadr s))
(define (arg2 s) (caddr s))

(define (build-compound c a1 a2) (list c a1 a2))

(define (compound-sentence? s)
  (and (pair? s) (member (car s) '(and or implies))))
(define (implication? s)
  (and (compound-sentence? s) (eq? (connective s) 'implies)))
(define (conjunction? s)
  (and (compound-sentence? s) (eq? (connective s) 'and)))
(define (disjunction? s)
  (and (compound-sentence? s) (eq? (connective s) 'or)))


;;;;;;;;;;;;;;;;;;;;;;;;; for NEGATIONS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Negations have an argument ARG, which is a sentence, and a
;   CONNECTIVE, which always has value NOT and is used only
;   by the predicate NEGATION? (and already has the proper definition)
; Rather than a constructor, an operator NEGATE is provided that
;   removes a negation if one is already present, and adds one if not

(define (arg s) (cadr s))

(define (negation? s)
  (and (pair? s) (eq? (connective s) 'not)))

(define (negate s)
  (if (negation? s)
      (arg s)
      (list 'not s)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;; for ATOMS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; ATOMS consist of a RELATION-NAME and an ARG-LIST of terms
; No predicate is given for testing atomhood; it is assumed that
;  a sentence that is not a negation, a compound sentence, or a
;  quantified sentence is an atom
; This type is also used for Skolem functions.

(define (relation-name s) (car s))
(define (arg-list s) (cdr s))

(define (build-atom r a) (cons r a))


;;;;;;;;;;;;;;;;;;;;;;;;;; UTILITY FUNCTIONS ;;;;;;;;;;;;;;;;;;;;;

; SWITCH is used inside DeMorgan's laws

(define (switch x)
  (cond ((eq? x 'and) 'or)
        ((eq? x 'or) 'and)
        ((eq? (car x) 'forall) (cons 'exists (cdr x)))
        ((eq? (car x) 'exists) (cons 'forall (cdr x)))))


; This predicate tests whether its argument, assumed to be a symbol,
;   is a variable.

(define (variable? x) (eq? (car (explode x)) '?))

; This function creates a new symbol based on an old symbol NAME
; It is used in standardizing & standardizing apart.

(define (get-new-name name)
  (implode
    (cons
      '?
      (explode
        (gensym (implode (append (cdr (explode name)) '(_))))))))


; SUBSTITUTE takes a list of pairs and a variable VAR and returns the
;   CDR of the first pair whose CAR is EQUAL? to the variable.
; It is essentially a lookup function for association lists

(define (substitute var new-names)
  (cond ((null? new-names) var)
        ((equal? var (caar new-names)) (cdar new-names))
        (else (substitute var (cdr new-names)))))


;;;;;;;;;;;;;;;;;; CONVERSION TO CLAUSE FORM ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; The top-level function CONVERT for conversion to clause form faithfully
;   reflects the algorithm of p. 145 of the text.  The names of the 9
;   functions corresponding to the steps of this algorithm can be seen
;   in its body.  Most of these functions merely consider all possible
;   input types and handle them as appropriate.  Each function assumes
;   that its input has been normalized by the previous functions

(define (convert s)
  (standardize-apart
    (make-set
      (distribute
        (remove-quantifiers
          (skolemize
            (move-quantifiers-left
              (standardize
                (move-negation-in
                  (remove-implies s))))))))))



;;;;;;;;;;;;;;;; REMOVE-IMPLIES ;;;;;;;;; STEP 1 OF TEXT ;;;;;;;;;;;;;;;;;;

; To remove implications, REMOVE-IMPLIES merely processes the arguments
;   of the sentence recursively, except in the case of implications,
;   which it converts to a disjunction of the same arguments (with
;   implication removed), with the first argument negated.

(define (remove-implies s)
  (cond ((quantified-sentence? s)
         (build-quantified (quantifier s) (remove-implies (quantified s))))
        ((compound-sentence? s)
         (if (implication? s)
             (build-compound 'or
                             (negate (remove-implies (arg1 s)))
                             (remove-implies (arg2 s)))
             (build-compound (connective s)
                             (remove-implies (arg1 s))
                             (remove-implies (arg2 s)))))
        ((negation? s)
         (negate (remove-implies (arg s))))
        (else s)))


;;;;;;;;;;;;;;;; MOVE-NEGATION-IN ;;;;;;;;; STEP 2 OF TEXT ;;;;;;;;;;;;;;;

; To move negation for sentences that aren't negations, all that is
;   needed is to do so recursively for arguments.  Atoms may be left
;   alone.  Negations need to consider the type of the argument, and
;   use the appropriate version of DeMorgan's law.

(define (move-negation-in s)
  (cond ((quantified-sentence? s)
         (build-quantified (quantifier s) (move-negation-in (quantified s))))
        ((compound-sentence? s)
         (build-compound (connective s)
                         (move-negation-in (arg1 s))
                         (move-negation-in (arg2 s))))
        ((negation? s)
         (let ((a (arg s)))
           (cond ((quantified-sentence? a)
                  (build-quantified
                    (switch (quantifier a))
                    (move-negation-in (negate (quantified a)))))
                 ((negation? a)
                  (move-negation-in (arg a)))
                 ((compound-sentence? a)
                  (build-compound
                    (switch (connective a))
                    (move-negation-in (negate (arg1 a)))
                    (move-negation-in (negate (arg2 a)))))
                 (else s))))
        ; atoms are left alone
        (else s)))


;;;;;;;;;;;;;;;;; STANDARDIZE ;;;;;;;;;;; STEP 3 OF TEXT ;;;;;;;;;;;;;;;

; This function maintains an association list NEW-NAMES of pairs of
;   the form (old-name new-name), for all variables OLD-NAME currently
;   in scope.  Each time a new scope is entered, a new name is generated
;   for the new quantified variable.  For negations and compound
;   statements, the function is simply called recursively.  When an atom
;   is reached, all old names are replaced by the corresponding new names.
; The function STANDARDIZE merely initializes the association list
;   to NIL, and passes it to STANDARDIZE-REC, which does all the work.
; It is assumed that there are no nested quantifiers with same name
;   this condition could be detected with a little effort

(define (standardize s)
  (define (standardize-rec s new-names)
    (cond ((quantified-sentence? s)
           (let ((new-name (get-new-name (variable s))))
             (build-quantified (build-quantifier
                                 (quantifier-type s)
                                 new-name)
                           (standardize-rec
                             (quantified s)
                             (cons (cons (variable s) new-name)
                                   new-names)))))
          ((negation? s)
           (negate (standardize-rec (arg s) new-names)))
          ((compound-sentence? s)
           (build-compound (connective s)
                           (standardize-rec (arg1 s) new-names)
                           (standardize-rec (arg2 s) new-names)))
          (else (build-atom (relation-name s)
                            (map (lambda (x) (substitute x new-names))
                                 (arg-list s))))))
  (standardize-rec s '()))

; could use a map function to filter?
(define (get-variables2 s)
  (define (filter args)
    (cond ((null? args) '())
          (else (let ((vars (filter (cdr args))))
                  (if (and (variable? (car args))
                           (not (member (car args) vars)))
                      (cons (car args) vars)
                      vars)))))
  (define (union s1 s2)
    (cond ((null? s1) s2)
          ((member (car s1) s2) (union (cdr s1) s2))
          (else (cons (car s1) (union (cdr s1) s2)))))
  (cond ((quantified-sentence? s)
         (let ((vars (get-variables2 (quantified s))))
           (if (member (variable s) vars)
               vars
               (cons (variable s) vars))))
        ((compound-sentence? s)
         (union (get-variables2 (arg1 s))
                (get-variables2 (arg2 s))))
        (else (filter (arg-list s)))))


;;;;;;;;;;;;;; MOVE-QUANTIFIERS-LEFT ;;;;;;;;; STEP 4 OF TEXT ;;;;;;;;;;;;;;;

; This algorithm is complicated slightly by the representation of
;   the input as a binary tree.  Thus for compound sentences there
;   are 3 cases.  Each case assumes that quantifiers have been
;   moved leftward (i.e., upward) for the 2 arguments.
;         (1) if the 1st arg is quantified, return its quantifier
;             applied to its quantified and to the full 2nd arg
;         (2) else if the 2nd arg is quantified, return its
;             quantifier applied to the full 1st arg and the
;             2nd arg's quantified
;         (3) otherwise leave the input alone.
; Note that negations, like atoms, may be left alone, since they
;   can no longer have quantifiers inside them after step 2.
; Quantified sentences just need their quantified processed recursively.

(define (move-quantifiers-left s)
  (cond ((quantified-sentence? s)
         (build-quantified (quantifier s)
                           (move-quantifiers-left (quantified s))))
        ((compound-sentence? s)
         (let ((a1 (move-quantifiers-left (arg1 s)))
               (a2 (move-quantifiers-left (arg2 s))))
           (cond ((quantified-sentence? a1)
                  (build-quantified (quantifier a1)
                                    (move-quantifiers-left
                                      (build-compound (connective s)
                                                      (quantified a1)
                                                      a2))))
                 ((quantified-sentence? a2)
                  (build-quantified (quantifier a2)
                                    (move-quantifiers-left
                                      (build-compound (connective s)
                                                      a1
                                                      (quantified a2)))))
                 (else s))))
        (else s)))


;;;;;;;;;;;;;;;; SKOLEMIZE ;;;;;;;;;;;;;;;; STEP 5 OF TEXT ;;;;;;;;;;;;;;;

; Recursive, one-pass skolemization requires keeping track of
;   (1) a list of those universally quantified variables already encountered
;   (2) a list of the variables to be skolemized and the arguments for each
; This is handled by passing two corresponding arguments ARGS and
;   DEPENDENCIES to a recursive SKOLEMIZE-REC function that does all
;   the work.  Initially both arguments are empty
; Quantified sentences are handled differently depending on their quantifier.
;   For existentially quantified sentences, the variable needs to be
;     added, together with its arguments, to the list of DEPENDENCIES
;     before the quantified is processed recursively.  For universally
;     quantified sentences, the variable needs to be added to the list
;     ARGS of universally quantified arguments before recursive processing
;     of the quantified.
; Compound sentences and negations merely process their arguments recursively.
; For atoms, each existentially quantified variable (i.e., each variable
;   appearing as the CAR of a member of DEPENDENCIES) must be replaced
;   by a functional expression whose function name depends on the variable
;   name, and whose arguments are those given by lookup in DEPENDENCIES.
; This substitution is handled one term at a time by the auxiliary function
;   SUBSTITUTE-SK.  It uses its own auxiliary function CONVERT-NAME to
;   create the names of Skolem functions.

(define (skolemize s)
  (define (substitute-sk args dependencies)
    (define (convert-name var)
      (implode (append '(s k _) (cdr (explode var)))))
    (cond ((null? args) '())
          (else (let ((dependency (substitute (car args) dependencies)))
                  (if (eq? dependency (car args))
                      (cons (car args) (substitute-sk (cdr args) dependencies))
                      (cons (build-atom (convert-name (car args)) dependency)
                            (substitute-sk (cdr args) dependencies)))))))
  (define (skolemize-rec s universals dependencies)
    (cond ((quantified-sentence? s)
           (build-quantified
             (quantifier s)
             (if (existential? s)
                 (skolemize-rec
                   (quantified s)
                   universals
                   (cons (cons (variable s) universals) dependencies))
                 (skolemize-rec
                   (quantified s)
                   (cons (variable s) universals)
                   dependencies))))
          ((compound-sentence? s)
           (build-compound (connective s)
                           (skolemize-rec (arg1 s) universals dependencies)
                           (skolemize-rec (arg2 s) universals dependencies)))
          ((negation? s)
           (negate (skolemize-rec (arg s) universals dependencies)))
          (else (build-atom (relation-name s)
                            (substitute-sk (arg-list s) dependencies)))))
  (skolemize-rec s '() '()))



;;;;;;;;;;;;;;; REMOVE-QUANTIFIERS ;;;;;;;;; STEP 6 OF TEXT ;;;;;;;;;;;;;;;

; This step is easy, since by now all quantifers trail down linearly from
;   the root.  So quantifiers are just stripped from the top until a
;   non-quantified sentence is encountered.

(define (remove-quantifiers s)
  (if (quantified-sentence? s)
      (remove-quantifiers (quantified s))
      s))


;;;;;;;;;;;;;;;;;; DISTRIBUTE ;;;;;;;;;;;;; STEP 7 OF TEXT ;;;;;;;;;;;;;;;

; The goal of this operation is to have all ANDs appear outside (i.e., above)
;   all ORs.  It is also slightly complicated by the binary tree
;   representation.
; Note that no quantifiers remain after step 6, and that if a negation
;   or an atom is encountered, processing may stop, since neither can
;   contain a compound sentence after step 2.
; Conjunctions already have an AND at the top level, so they just need
;   to have their arguments processed recursively.
; Disjunctions need to care about the form of their arguments, and to
;   have these arguments already processed recursively.
; If both arguments are conjunctions after being processed,
;   then there is the possibility of combinatorial explosion.
;   This is handled by keeping the first disjunct intact, distributing
;     over the second (to give two ORs at the 2nd level), and applying
;     DISTRIBUTE recursively to these two ORs.
; If just one argument is a conjunction, then the distributive law is
;   applied to this argument.  If no argument is a conjunction, then
;   there were no conjunctions in all of S, and S may be returned
;   unchanged.

(define (distribute s)
  (cond ((negation? s) s)
        ((conjunction? s)
         (build-compound 'and (distribute (arg1 s)) (distribute (arg2 s))))
        ((disjunction? s)
         (let ((a1 (distribute (arg1 s)))
               (a2 (distribute (arg2 s))))
           (if (conjunction? a1)
               (if (conjunction? a2)
                   (build-compound
                     'and
                     (distribute (build-compound 'or a1 (arg1 a2)))
                     (distribute (build-compound 'or a1 (arg2 a2))))
                   (build-compound
                     'and
                     (build-compound 'or (arg1 a1) a2)
                     (build-compound 'or (arg2 a1) a2)))
               (if (conjunction? a2)
                   (build-compound
                     'and
                     (build-compound 'or a1 (arg1 a2))
                     (build-compound 'or a1 (arg2 a2)))
                   s))))
        ; atom
        (else s)))


;;;;;;;;;;;;;;;; MAKE-SET ;;;;;;;;; STEP 8 OF TEXT ;;;;;;;;;;;;;;;

; This function takes a conjunction of disjunctions of literals and
;   returns a list of the clauses (i.e., the conjuncts), where each
;   clause is represented as a list of literals.
; Disjunctions are represented as lists of length 1, where the sole
;   element is a list of literals.  This list must be obtained by
;   appending the sole member of their argument lists.  Literals
;   are trivial disjunctions, so they must be enclosed in 2 pairs
;   of parentheses.

(define (make-set s)
  (cond ((negation? s) (list (list s)))
        ((disjunction? s) (list (append (car (make-set (arg1 s)))
                                        (car (make-set (arg2 s))))))
        ((conjunction? s) (append (make-set (arg1 s))
                                  (make-set (arg2 s))))
        (else (list (list s)))))


;;;;;;;;;;;;;; STANDARDIZE-APART ;;;;;;;;;;;;;; STEP 9 OF TEXT ;;;;;;;;;;;;;

; This function works one clause at a time, making a list of all
;   variables that appear in the clause, constructing new names
;   for them, and substituting the new names for the old.
; These 3 steps are handled respectively by GET-VARIABLES,
;   GET-NEW-NAMES, and SUBSTITUTE-ALL

(define (standardize-apart clause-list)
  (cond ((null? clause-list) '())
        (else (let ((var-list (get-variables (car clause-list))))
                (let ((new-names (get-new-names var-list)))
                  (cons (substitute-all (car clause-list) new-names)
                        (standardize-apart (cdr clause-list))))))))

; these 3 could be subordinate to standardize-apart

; This function just calls the utility function GET-NEW-NAME for
;   every member of the list VAR-LIST of variables

(define (get-new-names var-list)
  (cond ((null? var-list) '())
        (else
          (cons (cons (car var-list) (get-new-name (car var-list)))
                (get-new-names (cdr var-list))))))


; This function takes a clause -- a list of literals -- and a list
;   NEW-NAMES of pairs of the form (variable  new-name-of-variable)
;   and substitutes the CDR of the pair for the CAR for every occurence
;   of every CAR.  For each literal, it copies NOT if present, copies
;   the relation name, and calls SUBSTITUTE-VAR-LIST to make all
;   substitutions in the argument list.
; SUBSTITUTE-VAR-LIST just traverses the list of arguments, substituting
;   for each (perhaps with the identity substitution).  It needs to be
;   able to handle skolemized variables, thus requiring a test of
;   the form (PAIR? (CAR VAR-LIST)).

(define (substitute-all clause new-names)
  (define (substitute-var-list var-list new-names)
    (cond ((null? var-list) '())
          ((pair? (car var-list))
           (cons (cons (caar var-list)
                       (substitute-var-list (cdar var-list) new-names))
                 (substitute-var-list (cdr var-list) new-names)))
          (else (cons (substitute (car var-list) new-names)
                      (substitute-var-list (cdr var-list) new-names)))))
  (cond ((null? clause) '())
        ((negation? (car clause))
         (cons (negate (build-atom (relation-name (arg (car clause)))
                                   (substitute-var-list
                                     (arg-list (arg (car clause)))
                                     new-names)))
               (substitute-all (cdr clause) new-names)))
        (else (cons (build-atom (relation-name (car clause))
                                (substitute-var-list
                                  (arg-list (car clause))
                                  new-names))
                    (substitute-all (cdr clause) new-names)))))

; Here in step 9 each member of a clause is a literal.  If it's a negation
;   then the variables are just the variables of the clause with the
;   NOT of the first member discarded.  Otherwise the first element of
;   a clause is added to the output list iff it is a variable that
;   is not duplicated elsewhere in the output.  To check this, the
;   output for the clause with this element deleted is computed and
;   stored in VARIABLES.
; Note that this deletion may yield a clause with an empty first literal.
;   Thus a separate test has to be made for whether the CAR of a clause
;   is NULL.

(define (get-variables clause)
   (cond ((null? clause) '())
         ((negation? (car clause))
          (get-variables (cons (arg (car clause)) (cdr clause))))
         ((null? (car clause)) (get-variables (cdr clause)))
         (else (let ((variables
                       (get-variables
                         ; handle skolemized variable
                         (if (pair? (caar clause))
                             (cons (cdaar clause)
                                   (cons (cdar clause) (cdr clause)))
                             (cons (cdar clause) (cdr clause))))))
                 (cond ((and (variable? (caar clause))
                             (not (member (caar clause) variables)))
                        (cons (caar clause) variables))
                       (else variables))))))