;;; -*- Package: User; Syntax: Common-Lisp; Mode: Lisp; Base: 10 -*-

;;; File converted on 28-Oct-87 14:27:32 from source LOGIC
;;; Original source {DSK}<LISPFILES>LOGIC>LOGIC.;3 created 26-Apr-88 09:10:49

; Copyright (c) 1988 by Roberto Ghislanzoni.  All rights reserved.



(DEFUN ADD-OR-LEVEL (WFF CLAUSES TREE &OPTIONAL CUTNAME) 
       
       ;; Adds a new or-node to the list of the nodes. The new
       ;; node is put in front of the old ones
 (COND
    ((NULL CLAUSES)
     TREE)
    (T (LET* ((LEVEL (AND-LEVEL TREE))
              (NEW-OR-NODE (MAKE-OR-NODE WFF CLAUSES (CONJ LEVEL)
                                  (UNIFICATION-ENV LEVEL)
                                  (GET-AND-NODE-THEORIES LEVEL)
                                  CUTNAME)))
             (MAKE-TREE LEVEL (APPEND (LIST NEW-OR-NODE)
                                     (OR-LEVELS TREE)))))))


(DEFUN ALL (VARS CONJ THS)
   (PROG (RESULTING-TREE
          (TREE (MAKE-TREE (MAKE-AND-NODE CONJ NIL
                                  (APPEND (LIST '*BACKGROUND-THEORY*)
                                         THS))
                       NIL))
          COLLECTED-RESULTS NEXT-OR)
     HERE
         (SETF RESULTING-TREE (LOGIC-PROVE TREE))
         (COND
            ((NULL RESULTING-TREE)
             (RETURN COLLECTED-RESULTS))
            (T (SETF COLLECTED-RESULTS
                     (APPEND COLLECTED-RESULTS
                            (LIST (LOOKUP VARS (UNIFICATION-ENV
                                                (AND-LEVEL 
                                                       RESULTING-TREE))
                                         ))))
               (SETF NEXT-OR (FIRST (OR-LEVELS RESULTING-TREE)))
               (SETF TREE (SOLVE (NEW-TREE RESULTING-TREE NEXT-OR)
                                 (FORMULA-OR NEXT-OR)
                                 (CLAUSES-OR NEXT-OR)))
               (GO HERE)))))


(DEFUN ALL-PREDICATES (THEORY-NAME) (ALL-PREDS (GET-THEORY THEORY-NAME)
                                           ))


(DEFUN ALL-PREDS (THEORY) 
       
       ;; The presence of VAL in the AND body is necessary
       ;; because it is correct to test if the predicates has
       ;; not  been erased: in such a case its value is NIL
 (PROG (PRNAMES)
   LABEL
       (MAPHASH #'(LAMBDA (KEY VAL)
                         (AND (NOT (SEMANTIC-ATTACHMENT-P VAL))
                              VAL
                              (SETF PRNAMES (APPEND PRNAMES
                                                   (LIST KEY))))) 
              THEORY)
       (RETURN PRNAMES)))


(DEFUN ALL-SAS (THEORY)
   (PROG (SANAMES)
     LABEL
         (MAPHASH #'(LAMBDA (KEY VAL)
                           (AND (SEMANTIC-ATTACHMENT-P VAL)
                                VAL
                                (SETF SANAMES (APPEND SANAMES
                                                     (LIST KEY))))) 
                THEORY)
         (RETURN SANAMES)))


(DEFUN ALL-SEMANTIC-ATTACHMENTS (THEORY-NAME) (ALL-SAS (GET-THEORY
                                                        THEORY-NAME)))


(DEFMACRO AND-LEVEL (TREE) (IL:BQUOTE (CAR (IL:\\\, TREE))))


(DEFMACRO ANTEC (WFF) (IL:BQUOTE (CDDR (IL:\\\, WFF))))


(DEFUN ANY (HOW-MANY VARS CONJ THS)
   (PROG (RESULTING-TREE
          (COUNTER 0)
          (TREE (MAKE-TREE (MAKE-AND-NODE CONJ NIL
                                  (APPEND (LIST '*BACKGROUND-THEORY*)
                                         THS))
                       NIL))
          COLLECTED-RESULTS NEXT-OR)
     HERE
         (SETF RESULTING-TREE (LOGIC-PROVE TREE))
         (COND
            ((OR (NULL RESULTING-TREE)
                 (EQ COUNTER HOW-MANY))
             (RETURN COLLECTED-RESULTS))
            (T (SETF COLLECTED-RESULTS
                     (APPEND COLLECTED-RESULTS
                            (LIST (LOOKUP VARS (UNIFICATION-ENV
                                                (AND-LEVEL 
                                                       RESULTING-TREE))
                                         ))))
               (SETF NEXT-OR (FIRST (OR-LEVELS RESULTING-TREE)))
               (SETF TREE (SOLVE (NEW-TREE RESULTING-TREE NEXT-OR)
                                 (FORMULA-OR NEXT-OR)
                                 (CLAUSES-OR NEXT-OR)))
               (INCF COUNTER)
               (GO HERE)))))


(DEFMACRO ATOMIC-FORMULAP (WFF)
   (IL:BQUOTE (AND (LISTP (IL:\\\, WFF))
                   (NULL (SECOND (IL:\\\, WFF))))))


(DEFUN ATTACH (SA-NAME DEFINITION THEORY-NAME &OPTIONAL WINDOW)
   (SETF (GETHASH SA-NAME (GET-THEORY THEORY-NAME WINDOW))
         (CONS 'SA DEFINITION))
   'ATTACHED)


(DEFMACRO CLAUSES-OR (OR-NODE) (IL:BQUOTE (SECOND (IL:\\\, OR-NODE))))


(DEFUN CLEAR-AND-LEVEL (TREE) (PROGN (SETF (CAR TREE)
                                           NIL)
                                     TREE))


(DEFMACRO CONJ (AND-LEVEL) (IL:BQUOTE (CAR (IL:\\\, AND-LEVEL))))


(DEFUN CONSEQ (WFF) (CAR WFF))


(DEFMACRO CONSEQP (C) (IL:BQUOTE (AND (LISTP (IL:\\\, C))
                                      (SYMBOLP (CAR (IL:\\\, C))))))


(DEFUN CREATE-BACKGROUND-THEORY
   NIL (PROGN (IN-PACKAGE 'USER)
              (CREATE-THEORY '*BACKGROUND-THEORY*)
              (WITH-OPEN-FILE (FILE (MERGE-PATHNAMES
                                     (MAKE-PATHNAME :NAME 'MAIN :TYPE
                                            'LGC))
                                    :DIRECTION :INPUT)
                     (PROG (NAME)
                       LABEL
                           (AND (EQ (SETF NAME (READ FILE))
                                    'THEORY-END)
                                (RETURN))
                           (LOGIC-ASSERT NAME (CONS '
                                                   DIRECTLY-IMPLEMENTED
                                                    (READ FILE))
                                  '*BACKGROUND-THEORY*)
                           (GO LABEL)))))


(DEFUN CREATE-THEORY (THEORY-NAME) (SETF (GET 'THEORY THEORY-NAME)
                                         (MAKE-HASH-TABLE))
                                   THEORY-NAME)


(DEFUN DELETE-OR-NODE (TAGNODE NODES) (DELETE TAGNODE NODES :TEST
                                             #'EQUAL :COUNT 1))


(DEFUN DELETE-OR-NODE-WITH-CUT (CUTNAME OR-LEVELS) 
       
       ;; This function is called every time a cut is proven:
       ;; all the alternatives for that clause MUST be erased.
       ;; Remember that every cut has a unique identifier
 (PROG ((NODES OR-LEVELS))
   LABEL
       (COND
          ((NULL NODES)
           OR-LEVELS)
          ((EQ (GET-CUT (CAR NODES))
               CUTNAME)
           (RETURN (DELETE-OR-NODE (CAR NODES)
                          OR-LEVELS)))
          (T (SETF NODES (CDR NODES))
             (GO LABEL)))))


(DEFMACRO DIRECTLY-IMPLEMENTED (CLAUSES)
   (IL:BQUOTE (EQ (CAR (IL:\\\, CLAUSES))
                  'DIRECTLY-IMPLEMENTED)))


(DEFMACRO FAILEDP (ENV) (IL:BQUOTE (EQ (IL:\\\, ENV)
                                       'FAILED)))


(DEFUN FIND-CLAUSES (PREDICATE-NAME THEORY-NAMES &OPTIONAL WINDOW)
   (PROG NIL
     LABEL
         (COND
            ((NULL THEORY-NAMES)
             (RETURN NIL))
            (T (LET* ((TH (FIRST THEORY-NAMES))
                      (CLAUSES (BINDING PREDICATE-NAME TH WINDOW)))
                     (COND
                        ((NULL CLAUSES)
                         (SETF THEORY-NAMES (CDR THEORY-NAMES))
                         (GO LABEL))
                        (T (RETURN CLAUSES))))))))


(DEFMACRO FORMULA-OR (OR-LEVEL) (IL:BQUOTE (CAR (IL:\\\, OR-LEVEL))))


(DEFMACRO GET-AND-NODE-THEORIES (AND-NODE) (IL:BQUOTE
                                            (THIRD (IL:\\\, AND-NODE))))


(DEFMACRO GET-CUT (OR-NODE) (IL:BQUOTE (SIXTH (IL:\\\, OR-NODE))))


(DEFMACRO GET-OR-NODE-THEORIES (OR-NODE) (IL:BQUOTE (FIFTH (IL:\\\,
                                                            OR-NODE))))


(DEFMACRO GET-THEORY (THEORY-NAME &OPTIONAL WINDOW)
   (IL:BQUOTE (OR (AND (IL:\\\, WINDOW)
                       (GET-THEORY-INTERNAL (IL:\\\, THEORY-NAME)
                              (IL:\\\, WINDOW)))
                  (GET 'THEORY (IL:\\\, THEORY-NAME)))))


(DEFMACRO IMPLICATIONP (WFF)
   (IL:BQUOTE (LET ((SEPARATOR (SECOND (IL:\\\, WFF))))
                   (AND (EQ SEPARATOR ':-)
                        (NOT (NULL (CDDR (IL:\\\, WFF))))))))


(DEFUN IS-THERE-CUT (CONJS)
   (OR (MEMBER '! CONJS)
       (PROG ((ELTS CONJS))
         LABEL
             (COND
                ((NULL ELTS)
                 NIL)
                ((AND (SYMBOLP (CAR ELTS))
                      (EQ (CHAR-CODE (CHAR (SYMBOL-NAME (CAR ELTS))
                                           0))
                          33))
                 (RETURN T))
                (T (SETF ELTS (CDR ELTS))
                   (GO LABEL))))))


(DEFUN LIST-ALL-THEORIES (&OPTIONAL WINDOW)
   (OR (AND WINDOW (LIST-ALL-THEORIES-INTERNAL WINDOW))
       (DO ((LL (SYMBOL-PLIST 'THEORY)
                (CDDR LL))
            (RESULT NIL))
           ((NULL LL)
            RESULT)
           (SETF RESULT (APPEND RESULT (LIST (CAR LL)))))))


(DEFUN LOAD-THEORY (THEORY-NAME &OPTIONAL WINDOW)
   (LET
    ((THEORY-FILE (MERGE-PATHNAMES (MAKE-PATHNAME :NAME THEORY-NAME 
                                          :TYPE 'LGC))))
    (OR
     (AND WINDOW (LOAD-DEVEL-THEORY WINDOW THEORY-NAME))
     (OR (AND (PROBE-FILE THEORY-FILE)
              (WITH-OPEN-FILE
               (FILE THEORY-FILE :DIRECTION :INPUT)
               (PROG (THEORY-NAME PRED-NUMBER SAS-NUMBER)
                     (SETF THEORY-NAME (READ FILE))
                     (CREATE-THEORY THEORY-NAME)
                     (SETF SAS-NUMBER (READ FILE))
                     (DO ((SAS SAS-NUMBER (DECF SAS)))
                         ((EQ SAS 0)
                          NIL)
                         (SETF (GETHASH (READ FILE)
                                      (GET 'THEORY THEORY-NAME))
                               (READ FILE)))
                     (SETF PRED-NUMBER (READ FILE))
                     (DO ((PREDS PRED-NUMBER (DECF PREDS)))
                         ((EQ PREDS 0)
                          NIL)
                         (SETF (GETHASH (READ FILE)
                                      (GET 'THEORY THEORY-NAME))
                               (READ FILE)))
                     (RETURN 'LOADED))))
         (FORMAT T "Theory not found")))))


(DEFUN LOGIC-ADD (PRED CLAUSES THEORY &OPTIONAL WINDOW)
   (PROGN (SETF (GETHASH PRED (GET-THEORY THEORY WINDOW))
                (APPEND (GETHASH PRED (GET-THEORY THEORY WINDOW))
                       CLAUSES))
          'ADDED))


(DEFUN LOGIC-ASSERT (PREDICATE-NAME CLAUSES THEORY-NAME &OPTIONAL 
                           WINDOW) (SETF (GETHASH PREDICATE-NAME
                                                (GET-THEORY THEORY-NAME 
                                                       WINDOW))
                                         CLAUSES)
                                   'ASSERTED)


(DEFUN LOGIC-DELETE (PRED-OR-SA THEORY-NAME &OPTIONAL WINDOW)
   (PROGN (SETF (GETHASH PRED-OR-SA (GET-THEORY THEORY-NAME WINDOW))
                NIL)
          'DELETED))


(DEFUN LOGIC-PROVE (TREE &OPTIONAL WINDOW)
   (PROG NIL
     JUMP
         (COND
            ((NULL-TREEP TREE)
             (RETURN NIL))
            ((NULL-AND-LEVELP TREE)
             (LET ((NEXT-OR (FIRST (OR-LEVELS TREE))))
       
       ;; Gets the next or-node: we have now no strategy for
       ;; choosing it; maybe later...

                  (COND
                     ((NULL NEXT-OR)
                      (SETF TREE (LIST NIL NIL))
                      (GO JUMP))
                     (T (SETF TREE (SOLVE (NEW-TREE TREE NEXT-OR)
                                          (FORMULA-OR NEXT-OR)
                                          (CLAUSES-OR NEXT-OR)
                                          NIL WINDOW))
                        (GO JUMP)))))
            (T
             (LET ((NEXT-LEVEL (AND-LEVEL TREE)))
                  (COND
                     ((NULL (CONJ NEXT-LEVEL))
                      (RETURN TREE))
                     (T (LET* ((TO-PROVE (FIRST (CONJ NEXT-LEVEL)))
                               (THS (GET-AND-NODE-THEORIES NEXT-LEVEL))
                               (CLAUSES (FIND-CLAUSES (PREDICATE 
                                                             TO-PROVE)
                                               THS WINDOW))
                               (CUT? (IS-THERE-CUT (REST (CONJ 
                                                             NEXT-LEVEL
                                                               )))))
                              (SETF TREE (SOLVE (UPDATE-TREE
                                                 (UPDATE-LEVEL 
                                                        NEXT-LEVEL 
                                                        TO-PROVE)
                                                 TREE)
                                                TO-PROVE CLAUSES CUT? 
                                                WINDOW))
                              (GO JUMP)))))))))


(DEFUN MAKE-AND-NODE (CONJ UNIF-ENV THEORIES) (LIST CONJ UNIF-ENV 
                                                    THEORIES))


(DEFUN MAKE-OR-NODE (WFF CLAUSES BORDER UNIF-ENV THEORIES &OPTIONAL 
                         CUTNAME) (LIST WFF CLAUSES BORDER UNIF-ENV 
                                        THEORIES CUTNAME))


(DEFUN MAKE-TREE (AND-LEVEL OR-LEVELS) (LIST AND-LEVEL OR-LEVELS))


(DEFUN MERGE-INTERNAL (NEW-THEORY-NAME THEORIES &OPTIONAL WINDOW)
   (PROGN
       
       ;; Merges the specified theories in to a new-brand theory

    (LET ((ACTUAL-THEORY (GET-THEORY NEW-THEORY-NAME WINDOW)))
         (DO ((THS THEORIES (CDR THS)))
             ((NULL THS)
              'MERGED)
             (AND (THEORYP (CAR THS)
                         WINDOW)
                  (MAPHASH #'(LAMBDA (KEY VAL)
                                    (AND VAL (SETF (GETHASH KEY 
                                                          ACTUAL-THEORY
                                                          )
                                                   VAL)))
                         (GET-THEORY (CAR THS)
                                WINDOW)))))))


(DEFUN MERGE-THEORIES (NEW-THEORY-NAME &REST LIST-OF-THEORIES)
   (PROGN (CREATE-THEORY NEW-THEORY-NAME)
          (MERGE-INTERNAL NEW-THEORY-NAME LIST-OF-THEORIES)
          'MERGED))


(DEFUN NEW-TREE (TREE OR-NODE) (MAKE-TREE (MAKE-AND-NODE (THIRD OR-NODE
                                                                )
                                                 (UNIF-ENV-OR OR-NODE)
                                                 (GET-OR-NODE-THEORIES
                                                  OR-NODE))
                                      (DELETE-OR-NODE OR-NODE
                                             (OR-LEVELS TREE))))


(DEFMACRO NULL-AND-LEVELP (TREE) (IL:BQUOTE (NULL (CAR (IL:\\\, TREE)))
                                        ))


(DEFMACRO NULL-OR-LEVELP (TREE) (IL:BQUOTE (NULL (SECOND (IL:\\\,
                                                          TREE)))))


(DEFMACRO NULL-TREEP (TREE) (IL:BQUOTE (AND (NULL-AND-LEVELP
                                             (IL:\\\, TREE))
                                            (NULL-OR-LEVELP
                                             (IL:\\\, TREE)))))


(DEFMACRO OR-LEVELS (TREE) (IL:BQUOTE (SECOND (IL:\\\, TREE))))


(DEFUN PREDICATE (WFF) (COND
                          ((LISTP WFF)
                           (CAR WFF))
                          (T WFF)))


(DEFUN PROVE (CONJ THS)
   (LET ((RESULT (LOGIC-PROVE (MAKE-TREE
                               (MAKE-AND-NODE
                                CONJ NIL (APPEND (LIST '
                                                    *BACKGROUND-THEORY*
                                                       )
                                                THS))
                               NIL))))
        (COND
           ((NULL RESULT)
            NIL)
           (T T))))


(DEFUN RENAME-CUT (ANTECS) 
       
       ;; This function returns a CONS with CAR as the renamed
       ;; cut and CDR as the list of antecs with the cut
       ;; renamed
 (DO ((TEMPVAR ANTECS (CDR TEMPVAR))
      (RESULTS NIL)
      (CUT-RENAMED NIL))
     ((NULL TEMPVAR)
      (CONS CUT-RENAMED RESULTS))
     (COND
        ((EQ (CAR TEMPVAR)
             '!)
         (SETF CUT-RENAMED (GENSYM "!"))
         (SETF RESULTS (APPEND RESULTS (LIST CUT-RENAMED))))
        (T (SETF RESULTS (APPEND RESULTS (LIST (CAR TEMPVAR))))))))


(DEFUN SAVE-THEORY (THEORY-NAME &OPTIONAL WINDOW)
   (LET ((THEORY (GET-THEORY THEORY-NAME WINDOW)))
        (COND
           ((NOT (THEORYP THEORY))
            'ERROR)
           (T (WITH-OPEN-FILE
               (FILE (MERGE-PATHNAMES (MAKE-PATHNAME :NAME THEORY-NAME 
                                             :TYPE 'LGC))
                     :DIRECTION :OUTPUT :IF-EXISTS :NEW-VERSION 
                     :IF-DOES-NOT-EXIST :CREATE)
               (LET ((PREDS (ALL-PREDS THEORY))
                     (SAS (ALL-SAS THEORY)))
                    (PROGN (FORMAT FILE "~S~%" THEORY-NAME)
                           (FORMAT FILE "~D~%" (LENGTH SAS))
                           (DO ((SA-NAME SAS (CDR SA-NAME)))
                               ((NULL SA-NAME)
                                NIL)
                               (FORMAT FILE "~S ~S ~%" (CAR SA-NAME)
                                      (GETHASH (CAR SA-NAME)
                                             THEORY)))
                           (FORMAT FILE "~D~%" (LENGTH PREDS))
                           (DO ((PRED-NAME PREDS (CDR PRED-NAME)))
                               ((NULL PRED-NAME)
                                NIL)
                               (FORMAT FILE "~S ~S ~%" (CAR PRED-NAME)
                                      (GETHASH (CAR PRED-NAME)
                                             THEORY)))
                           'SAVED)))))))


(DEFMACRO SEMANTIC-ATTACHMENT-P (SA) (IL:BQUOTE
                                      (EQ (CAR (IL:\\\, SA))
                                          'SA)))


(DEFUN SHOW-DEFINITION (ELEMENT THEORY-NAME &OPTIONAL WINDOW)
   (FORMAT (OR (AND WINDOW *TRACE-OUTPUT*)
               T)
          "~S~%"
          (PROG ((DEF (GETHASH ELEMENT (GET-THEORY THEORY-NAME WINDOW))
                      ))
                (OR (AND (SEMANTIC-ATTACHMENT-P DEF)
                         (RETURN (CDR DEF)))
                    (RETURN DEF)))))


(DEFUN SHOW-THEORY (THEORY-NAME &OPTIONAL VERBOSE WINDOW)
   (LET*
    ((THEORY (GET-THEORY THEORY-NAME))
     (PREDICATES (ALL-PREDS THEORY))
     (SAS (ALL-SAS THEORY))
     (STREAM (OR (AND WINDOW *TRACE-OUTPUT*)
                 T)))
    (OR
     (AND SAS
          (PROGN (FORMAT STREAM "Semantic attachments: ~%")
                 (DO ((PP SAS (CDR PP)))
                     ((NULL PP)
                      NIL)
                     (PROGN (FORMAT T "~%~S ~% " (CAR PP))
                            (AND VERBOSE
                                 (FORMAT T "Definition: ~S ~%"
                                        (CDR (GETHASH (CAR PP)
                                                    THEORY))
                                        " "))))
                 (FORMAT STREAM "~% ~%"))))
    (OR (AND PREDICATES
             (PROGN (FORMAT STREAM "Predicates: ~%")
                    (DO ((PP PREDICATES (CDR PP)))
                        ((NULL PP)
                         NIL)
                        (PROGN (FORMAT T "~%~S ~%" (CAR PP))
                               (AND VERBOSE (FORMAT STREAM 
                                                   "Clauses: ~S ~%"
                                                   (GETHASH
                                                    (CAR PP)
                                                    THEORY)
                                                   " "))))
                    (FORMAT STREAM "~% ~%"))))))


(DEFUN SOLVE (TREE FORMULA CLAUSES &OPTIONAL CUT WINDOW)
   (PROG NIL
     JUMP
         (AND WINDOW (SOLVE-DEBUGGER TREE FORMULA CLAUSES WINDOW))
         (COND
            ((NULL CLAUSES)                ; demo is failed

             (RETURN (CLEAR-AND-LEVEL TREE)))
            ((DIRECTLY-IMPLEMENTED CLAUSES); clauses from the main
                                           ; theory

             (RETURN (FUNCALL (CDR CLAUSES)
                            TREE FORMULA CLAUSES WINDOW)))
            ((SEMANTIC-ATTACHMENT-P CLAUSES)
                                           ; Semantic attachment
                                           ; defined by the user

             (LET ((EXPANDED-FORMULA (LOOKUP FORMULA
                                            (UNIFICATION-ENV
                                             (AND-LEVEL TREE)))))
                  (COND
                     ((APPLY (CDR CLAUSES)
                             (CDR EXPANDED-FORMULA))
                      (RETURN TREE))
                     (T (RETURN (CLEAR-AND-LEVEL TREE))))))
            (T
             (LET* ((CANDIDATE (FIRST CLAUSES))
                    (ASSERT (RENAME CANDIDATE))
                    (NEWENV (UNIFY FORMULA (CONSEQ ASSERT)
                                   (UNIFICATION-ENV (AND-LEVEL TREE))
                                   WINDOW)))
                   (COND
                      ((FAILEDP NEWENV)
                       (SETF CLAUSES (REST CLAUSES))
                       (GO JUMP))
                      ((ATOMIC-FORMULAP ASSERT)
       
       ;; If a cut has been discovered in the previous
       ;; procedure, it is necessary not to instantiate
       ;; alternatives for the clause in a or-level

                       (RETURN (UPDATE-ENV NEWENV
                                      (OR (AND CUT TREE)
                                          (ADD-OR-LEVEL FORMULA
                                                 (REST CLAUSES)
                                                 TREE)))))
                      ((IMPLICATIONP ASSERT)
       
       ;; If there is a cut, it is necessary to mark the
       ;; alternatives for that clause; if the cut will be
       ;; proved, then these alternatives will be eliminated  

                       (RETURN (COND
                                  ((IS-THERE-CUT (ANTEC ASSERT))
                                   (LET* ((RENAMED-STRUCTURE
                                           (RENAME-CUT (ANTEC ASSERT)))
                                          (RENAMED-CUT (CAR 
                                                      RENAMED-STRUCTURE
                                                            ))
                                          (RENAMED-ASSERT (CDR 
                                                      RENAMED-STRUCTURE
                                                               )))
                                         (SUBSTITUTE-LEVEL
                                          NEWENV RENAMED-ASSERT
                                          (ADD-OR-LEVEL FORMULA
                                                 (REST CLAUSES)
                                                 TREE RENAMED-CUT))))
                                  (T (SUBSTITUTE-LEVEL
                                      NEWENV
                                      (ANTEC ASSERT)
                                      (ADD-OR-LEVEL FORMULA
                                             (REST CLAUSES)
                                             TREE))))))))))))


(DEFUN SUBSTITUTE-LEVEL (ENV ANTECS TREE)
   (PROGN (RPLACA TREE (MAKE-AND-NODE (APPEND ANTECS
                                             (CONJ (AND-LEVEL TREE)))
                              ENV
                              (GET-AND-NODE-THEORIES (AND-LEVEL TREE)))
                 )
          TREE))


(DEFMACRO THEORYP (THEORY &OPTIONAL WINDOW)
   (IL:BQUOTE (OR (AND (GET-THEORY (IL:\\\, THEORY)
                              (IL:\\\, WINDOW))
                       T)
                  (HASH-TABLE-P (IL:\\\, THEORY)))))


(DEFMACRO UNIF-ENV-OR (OR-NODE) (IL:BQUOTE (FOURTH (IL:\\\, OR-NODE))))


(DEFMACRO UNIFICATION-ENV (AND-NODE) (IL:BQUOTE (SECOND (IL:\\\, 
                                                               AND-NODE
                                                               ))))


(DEFUN UPDATE-ENV (ENV TREE) (SETF (SECOND (AND-LEVEL TREE))
                                   ENV)
                             TREE)


(DEFUN UPDATE-LEVEL (LEVEL FORMULA) (MAKE-AND-NODE (CDR (CONJ LEVEL))
                                           (UNIFICATION-ENV LEVEL)
                                           (GET-AND-NODE-THEORIES
                                            LEVEL)))


(DEFUN UPDATE-TREE (LEVEL TREE) (MAKE-TREE LEVEL (OR-LEVELS TREE)))

(IL:FILESLOAD UNIFIER)