(DEFINE-FILE-INFO READTABLE "INTERLISP" PACKAGE "USER" BASE 10)
(IL:FILECREATED "14-Sep-94 18:48:27" ("compiled on " IL:{DSK}<lispcore>lispusers>UNIFIER.;1) 
"28-Jul-94 17:28:46" IL:bcompl'd IL:in "Medley 25-Aug-94 ..." IL:dated "25-Aug-94 10:02:49")
(IL:FILECREATED " 1-Aug-88 11:37:03" IL:{DSK}<LISPFILES>LOGIC>MEDLEY>UNIFIER.;1 7425 IL:previous 
IL:date%: "13-Jul-88 15:26:58" IL:{DSK}<LISPFILES>LOGIC>UNIFIER.;1)
(IL:PRETTYCOMPRINT IL:UNIFIERCOMS)
(IL:RPAQQ IL:UNIFIERCOMS ((IL:FUNCTIONS BINDING BUILD-NEW-ENV CREATE-NEW-VARIABLE CREATE-VARIABLES 
FIND-IF-MEMBER FIND-VALUES FIND-VARIABLE-VALUE LOOKUP NULLP RENAME RENAME-VARS UNIFY VARIABLEP)))
(DEFUN BINDING (PREDICATE THEORY-NAME &OPTIONAL WINDOW) (COND ((EQ THEORY-NAME (QUOTE 
*BACKGROUND-THEORY*)) (COND ((EQ (CHAR-CODE (CHAR (SYMBOL-NAME PREDICATE) 0)) 33) (IL:* IL:;; 
"CUT is handled in a very particular way!! ") (GETHASH (QUOTE !) (GET (QUOTE THEORY) (QUOTE 
*BACKGROUND-THEORY*)))) (T (GETHASH PREDICATE (GET (QUOTE THEORY) (QUOTE *BACKGROUND-THEORY*)))))) (T 
(GETHASH PREDICATE (GET-THEORY THEORY-NAME WINDOW)))))
(DEFUN BUILD-NEW-ENV (PAT DAT ENV) (IL:* IL:;; 
" It is better to make a distinction between the null value of a variable  and the variables unbound")
 (COND ((NULL DAT) (ACONS PAT (QUOTE *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)) (IL:* IL:;; 
"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 "
) (IL:* IL:;; "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) (IL:* IL:;; 
"The variable is unbound, so the variable itself is returned") VAR) ((NULLP VAL) (IL:* IL:;; 
"NULLP checks is the value is *NULL*") NIL) (T (IL:* IL:;; 
"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) (IL:BQUOTE (EQ (IL:\, ATOM) (QUOTE *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) (IL:* IL:;; 
"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 (QUOTE UNIFY)))) (REST-PAT) (REST-DAT) TEMP) HERE (AND
 DEBUGFLG (UNIFY-DEBUGGER PATT DAT ENV WINDOW)) (IL:* IL:; "debugging stuff") (COND ((AND (NULL PATT) 
(NULL DAT)) (COND ((AND (NULL REST-DAT) REST-PAT) (RETURN (QUOTE FAILED))) ((AND (NULL REST-PAT) 
REST-DAT) (RETURN (QUOTE 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 (QUOTE FAILED)) (RETURN (QUOTE 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 (QUOTE FAILED))))) ((NULL DAT) (COND ((NULLP PATT) (GO 
OUT)) (T (RETURN (QUOTE 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 (QUOTE FAILED))))) (T (RETURN (QUOTE FAILED)))) OUT (IL:* IL:;; 
"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) (IL:BQUOTE (AND (SYMBOLP (IL:\, ITEM)) (EQ (CHAR-CODE (CHAR (SYMBOL-NAME (
IL:\, ITEM)) 0)) 63))))
(IL:PUTPROPS IL:UNIFIER IL:COPYRIGHT ("Roberto Ghislanzoni" 1987 1988))
NIL