;;; -*- 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>SIMPLELOGIC>UNIFIER.;7 created  1-Mar-88 10:38:52

; 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 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 (GENSYM "?")))
                       (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)))