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

;;; File converted on 28-Oct-87 14:27:32 from source UNIFIER
;;; Original source {DSK}<LISPFILES>LOGIC>MEDLEY>UNIFIER.;1 created  1-Aug-88 11:37:03

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


(DEFUN BINDING (PREDICATE THEORY-NAME &OPTIONAL WINDOW)
       (COND ((EQ THEORY-NAME '*BACKGROUND-THEORY*)
              (COND ((EQ (CHAR-CODE (CHAR (SYMBOL-NAME PREDICATE)
                                          0))
                         33)
                     
                     ;; CUT is handled in a very particular way!! 
                     (GETHASH '! (GET 'THEORY '*BACKGROUND-THEORY*)))
                    (T (GETHASH PREDICATE (GET 'THEORY 
                                               '*BACKGROUND-THEORY*))))
              )
             (T (GETHASH PREDICATE (GET-THEORY THEORY-NAME WINDOW)))))
(DEFUN BUILD-NEW-ENV (PAT DAT ENV)
       
       ;;  It is better to make a distinction between the null value
       ;; of a variable  and the variables unbound
       (COND ((NULL DAT)
              (ACONS PAT '*NULL* ENV))
             (T (ACONS PAT DAT ENV))))
(DEFUN CREATE-NEW-VARIABLE NIL
       (PROGN (SETF *VARIABLES-COUNTER* (+ 1 *VARIABLES-COUNTER*))
              (OR (GETHASH *VARIABLES-COUNTER* *VARIABLES-TABLE*)
                  (SETF (GETHASH *VARIABLES-COUNTER* *VARIABLES-TABLE*)
                        (MAKE-SYMBOL (FORMAT NIL "?~A" 
                                            *VARIABLES-COUNTER*))))))
(DEFUN CREATE-VARIABLES NIL (DEFVAR *VARIABLES-TABLE* (MAKE-HASH-TABLE)
                                   )
       
       ;; all the variables used are cached in a hash-table: this is
       ;; also for not generating a lot of symbols that will fill up
       ;; the symbol table of the system 
       
       ;; This function must be called before starting to work with
       ;; Logic
       (DO ((X 0 (+ X 1)))
           ((= X 4095)
            T)
         (SETF (GETHASH X *VARIABLES-TABLE*)
               (MAKE-SYMBOL (FORMAT NIL "?~A" X)))))
(DEFUN FIND-IF-MEMBER (ELT LST)
       (COND ((NULL LST)
              NIL)
             ((LISTP LST)
              (OR (FIND-IF-MEMBER ELT (CAR LST))
                  (FIND-IF-MEMBER ELT (CDR LST))))
             ((ATOM LST)
              (EQ LST ELT))
             (T (MEMBER ELT LST))))
(DEFUN FIND-VALUES (ELT ENV)
       (COND ((NULL ELT)
              NIL)
             ((LISTP ELT)
              (CONS (FIND-VALUES (CAR ELT)
                           ENV)
                    (FIND-VALUES (CDR ELT)
                           ENV)))
             ((VARIABLEP ELT)
              (FIND-VARIABLE-VALUE ELT ENV))
             (T ELT)))
(DEFUN FIND-VARIABLE-VALUE (VAR ENV)
       (LET ((VAL (CDR (ASSOC VAR ENV))))
            (COND ((VARIABLEP VAL)
                   (FIND-VARIABLE-VALUE VAL ENV))
                  ((NULL VAL)
                   
                   ;; The variable is unbound, so the variable itself
                   ;; is returned
                   VAR)
                  ((NULLP VAL)
                   
                   ;; NULLP checks is the value is *NULL*
                   NIL)
                  (T 
                     ;; This is the statement for a partial occur 
                     ;; check
                     (OR (AND (NOT (FIND-IF-MEMBER VAR VAL))
                              (FIND-VALUES VAL ENV))
                         VAL)))))
(DEFUN LOOKUP (EXPR ENV)
       (COND ((NUMBERP EXPR)
              EXPR)
             ((SYMBOLP EXPR)
              (FIND-VALUES EXPR ENV))
             (T (CONS (FIND-VALUES (CAR EXPR)
                             ENV)
                      (FIND-VALUES (CDR EXPR)
                             ENV)))))
(DEFMACRO NULLP (ATOM)
       `(EQ ,ATOM '*NULL*))
(DEFUN RENAME (EXPR)
       (LET ((VARSTABLE (MAKE-HASH-TABLE)))
            (DECLARE (SPECIAL VARSTABLE))
            (RENAME-VARS EXPR)))
(DEFUN RENAME-VARS (EXPR)
       (COND ((NULL EXPR)
              NIL)
             ((LISTP EXPR)
              (CONS (RENAME-VARS (CAR EXPR))
                    (RENAME-VARS (CDR EXPR))))
             ((VARIABLEP EXPR)
              (LET ((ALREADY-RENAMED (GETHASH EXPR VARSTABLE)))
                   (COND (ALREADY-RENAMED ALREADY-RENAMED)
                         (T (LET ((NEW (CREATE-NEW-VARIABLE)))
                                 (SETF (GETHASH EXPR VARSTABLE)
                                       NEW)
                                 NEW)))))
             (T EXPR)))
(DEFUN UNIFY (PATT DAT ENV &OPTIONAL WINDOW)
       
       ;; This is a very fast implementation of unifier: no stack
       ;; frames are generated. The tecnique used here is that of
       ;; save-rest argument: the unifier is not a true-recursive
       ;; procedure, in the sense that it does not require a full
       ;; stack for its implementation: in fact, when failure occurs,
       ;; the value FAILED must be immediately returned 
       (PROG ((DEBUGFLG (AND WINDOW (TRACINGP WINDOW 'UNIFY)))
              (REST-PAT)
              (REST-DAT)
              TEMP)
             HERE
             (AND DEBUGFLG (UNIFY-DEBUGGER PATT DAT ENV WINDOW))
                                           ; debugging stuff
             (COND ((AND (NULL PATT)
                         (NULL DAT))
                    (COND ((AND (NULL REST-DAT)
                                REST-PAT)
                           (RETURN 'FAILED))
                          ((AND (NULL REST-PAT)
                                REST-DAT)
                           (RETURN 'FAILED))
                          ((AND (NULL REST-PAT)
                                (NULL REST-DAT))
                           (RETURN ENV))
                          (T (SETF PATT (CAR REST-PAT))
                             (SETF DAT (CAR REST-DAT))
                             (SETF REST-PAT (CDR REST-PAT))
                             (SETF REST-DAT (CDR REST-DAT))
                             (GO HERE))))
                   ((EQ ENV 'FAILED)
                    (RETURN 'FAILED))
                   ((EQ PATT DAT)
                    (GO OUT))
                   ((VARIABLEP DAT)
                    (SETF TEMP (CDR (ASSOC DAT ENV)))
                    (COND ((NULL TEMP)
                           (SETF ENV (BUILD-NEW-ENV DAT PATT ENV))
                           (GO OUT))
                          (T (SETF DAT TEMP)
                             (GO HERE))))
                   ((VARIABLEP PATT)
                    (SETF TEMP (CDR (ASSOC PATT ENV)))
                    (COND ((NULL TEMP)
                           (SETF ENV (BUILD-NEW-ENV PATT DAT ENV))
                           (GO OUT))
                          (T (SETF PATT TEMP)
                             (GO HERE))))
                   ((NULL PATT)
                    (COND ((NULLP DAT)
                           (GO OUT))
                          (T (RETURN 'FAILED))))
                   ((NULL DAT)
                    (COND ((NULLP PATT)
                           (GO OUT))
                          (T (RETURN 'FAILED))))
                   ((LISTP PATT)
                    (COND ((LISTP DAT)
                           (SETF REST-PAT (CONS (REST PATT)
                                                REST-PAT))
                           (SETF REST-DAT (CONS (REST DAT)
                                                REST-DAT))
                           (SETF PATT (CAR PATT))
                           (SETF DAT (CAR DAT))
                           (GO HERE))
                          (T (RETURN 'FAILED))))
                   (T (RETURN 'FAILED)))
             OUT
             
             ;; a check is made for the end of the procedure
             (COND ((AND (NULL REST-PAT)
                         (NULL REST-DAT))
                    (RETURN ENV))
                   (T (SETF DAT NIL)
                      (SETF PATT NIL)
                      (GO HERE)))))
(DEFMACRO VARIABLEP (ITEM)
       `(AND (SYMBOLP ,ITEM)
             (EQ (CHAR-CODE (CHAR (SYMBOL-NAME ,ITEM)
                                  0))
                 63)))