home *** CD-ROM | disk | FTP | other *** search
- ; Prolog-Interpreter: eXPerimental-Prolog
- ; Bruno Haible 21.04.1988-22.04.1988
-
- (setq *print-pretty* t)
- (setq *print-circle* t)
- (defvar prologpackage
- (or (find-package "_") (make-package "_" :nicknames '("PROLOGVARS")))
- )
- (defun c ()
- (compile-file "PROLOG.LSP" :output-file "PROLOG.FAS")
- (load "PROLOG.FAS")
- )
-
- #| Unifikation: nach Robinson, mit Zyklen |#
-
- ; Variablen sind Symbole.
- ; Sie werden dadurch an etwas gebunden, daß ihre Wertzelle diesen Wert
- ; enthält.
-
- ; Generierung einer Variablen mit vorgegebenem Namensanfang:
- (defun make-var (name)
- (let ((var (gentemp (string name) prologpackage)))
- (set var var)
- var
- ) )
-
- ; Test auf Variable
- (defun varp (term)
- (and (symbolp term) (eq (symbol-package term) prologpackage))
- )
-
- ; Test auf gebundene Variable
- (defun boundvarp (term)
- (and (varp term) (not (eq (symbol-value term) term)))
- )
-
- ; Generierung einer Bindung
- (defun bind (var term)
- (set var term)
- )
-
- ; Substitution = Menge aller Paare (X . W), wo X eine gebundene Variable
- ; und W der Inhalt ihrer Wertzelle ist.
-
- (defun check-circularity (var)
- ; liefert T, falls var (evtl. über andere Variablen hinweg)
- ; an sich selbst gebunden ist.
- (let ((step1 var) ; Vorgehen wie bei list-length
- (step2 var))
- (loop
- (if (eq (symbol-value step2) step2) ; Variable ungebunden?
- (return T))
- (setq step2 (symbol-value step2)) ; eins weiterrücken
- (if (not (varp step2)) ; Ende der Liste ?
- (return NIL))
- (if (eq step1 step2) ; in Zyklus gelaufen?
- (return T))
- (if (eq (symbol-value step2) step2) ; Variable ungebunden?
- (return T))
- (setq step2 (symbol-value step2)) ; wieder eins weiterrücken
- (if (not (varp step2)) ; Ende der Liste ?
- (return NIL))
- (if (eq step1 step2) ; in Zyklus gelaufen?
- (return T))
- (setq step1 (symbol-value step1))
- ; step1 folgt mit halber Geschwindigkeit nach.
- ) ) )
-
- (defun make-lispterm (term)
- ; wandelt einen Prolog-Term durch Ausschaltung von Zwischenvariablen
- ; zu einem reinen Lisp-Term um und liefert diesen.
- (let ((markedvars nil))
- (labels ((unmarked (var)
- (eq (get var 'newreference '%default%) '%default%)
- )
- (mark (var)
- ; markiert die Variable var, indem es in die Propertyliste
- ; von var das einträgt, worauf jede Referenz
- ; auf var zu zeigen haben wird.
- (when (unmarked var) ; schon markiert -> nichts tun.
- (push var markedvars)
- (let ((val (symbol-value var)))
- (setf (get var 'newreference)
- (cond ((varp val) (mark val)) ; bei Variablen: rekursiv
- ((consp val) ; neue CONS-Zelle anlegen:
- (cons (car val) (cdr val)) )
- (t val) ; Atome: Wert selbst
- ) ) ) )
- (get var 'newreference)
- )
- (lispterm (term) ; der eigentliche Umwandler
- (cond ((varp term)
- (if (check-circularity term)
- (error "Ungebundene Variable ~S kann nicht in ~
- LISP-Objekt umgewandelt werden." term
- ) )
- (if (unmarked term)
- (let ((newval (mark term)))
- (when (consp newval)
- (setf (car newval) (lispterm (car newval)))
- (setf (cdr newval) (lispterm (cdr newval)))
- )
- newval
- )
- (get term 'newreference)
- ))
- ((consp term)
- (cons (lispterm (car term)) (lispterm (cdr term)))
- )
- (t term)
- )) )
- (prog1
- (lispterm term)
- (dolist (v markedvars) ; alle Markierungen rückgängig machen
- (remprop v 'newreference)
- ) )
- ) ) )
-
- ; Damit die PRINT-CIRCLE-Markierungen in den verschiedenen Teilen der
- ; Ausgabe dieselben Nummern tragen, muß man die Teile per DEFSTRUCT
- ; zusammenfassen und mit einer eigenen PRINT-FUNCTION ausgeben:
- (defstruct (vars-and-vals (:print-function print-vars-and-vals) (:conc-name "VV-"))
- (vars nil :type list)
- (vals nil :type list)
- )
- (defun print-vars-and-vals (obj stream depth)
- (declare (ignore depth))
- (format stream "~{~W = ~W~^, ~}" (mapcan #'list (vv-vars obj) (vv-vals obj)))
- )
-
- (defun print-bindings (varnames newvars)
- ; gibt die Werte der Variablen in newvars aus, dabei dienen die Symbole
- ; in varnames als Namen.
- (let ((markedvars nil))
- (labels ((unmarked (var)
- (eq (get var 'newreference '%default%) '%default%)
- )
- (mark (var)
- ; markiert die Variable var, indem es in die Propertyliste
- ; von var dasjenige Objekt einträgt, worauf jede Referenz
- ; auf var zu zeigen haben wird. Liefert dieses Objekt.
- (when (unmarked var) ; schon markiert -> nichts tun.
- (push var markedvars)
- (let ((val (symbol-value var)))
- (setf (get var 'newreference)
- (cond ((varp val) (mark val)) ; bei Variablen: rekursiv
- ((consp val) ; neue CONS-Zelle anlegen:
- (cons (car val) (cdr val)) )
- (t val) ; Atome: Wert selbst
- ) ) ) )
- (get var 'newreference)
- )
- (markcircular (var)
- ; markiert var (noch nicht markiert) und alle mit var
- ; geshareten Variablen mit demselben Symbol,
- ; liefert dieses Symbol.
- ; 1. Schritt: Suchen, ob eine der Variablen bereits markiert.
- (let ((markingvar
- (do ((step1 var) (step2 var))
- (nil)
- (setq step2 (symbol-value step2))
- (unless (unmarked step2)
- (return (get step2 'newreference)))
- (if (eq step1 step2) (return var))
- (setq step2 (symbol-value step2))
- (unless (unmarked step2)
- (return (get step2 'newreference)))
- (if (eq step1 step2) (return var))
- (setq step1 (symbol-value step1))
- )) )
- ; 2. Schritt: diese Markierung überall unterbringen.
- (do ((step1 var) (step2 var))
- (nil)
- (pushnew step2 markedvars)
- (setf (get step2 'newreference) markingvar)
- (setq step2 (symbol-value step2))
- (if (eq step1 step2) (return))
- (pushnew step2 markedvars)
- (setf (get step2 'newreference) markingvar)
- (setq step2 (symbol-value step2))
- (if (eq step1 step2) (return))
- (setq step1 (symbol-value step1))
- )
- markingvar
- ) )
- (lispterm (term) ; der eigentliche Umwandler
- (cond ((varp term)
- (if (check-circularity term)
- (if (unmarked term)
- (markcircular term)
- (get term 'newreference)
- )
- (if (unmarked term)
- (let ((newval (mark term)))
- (when (consp newval)
- (setf (car newval) (lispterm (car newval)))
- (setf (cdr newval) (lispterm (cdr newval)))
- )
- newval
- )
- (get term 'newreference)
- )) )
- ((consp term)
- (cons (lispterm (car term)) (lispterm (cdr term)))
- )
- (t term)
- )) )
- (let ((values (mapcar #'lispterm newvars)))
- (print (make-vars-and-vals :vars varnames :vals values))
- (dolist (v markedvars) ; alle Markierungen rückgängig machen
- (remprop v 'newreference)
- ) )
- ) ) )
-
-
- ; unifiziert mehrere Terme, erweitert dabei die (globale) Substitution:
- ; Hier: Unifikation nach Robinson.
- ; Ergebnis: 'IMPOSSIBLE oder
- ; eine Liste ((X1 . T1) ... (Xj . Tj)) der alten Werte der bei der
- ; Unifikation veränderten Variablen.
- (defun unify (termpairlist &aux (oldvaluelist nil))
- ; termpairlist = ((T1a T1b) ... (Tka Tkb)), wobei Tia mit Tib zu unifizieren
- ; ist.
- (loop
- (if (null termpairlist) (return oldvaluelist))
- (let ((Ta (first (first termpairlist)))
- (Tb (second (first termpairlist))))
- (setq termpairlist (cdr termpairlist))
- (cond ((eq Ta Tb)) ; gleich -> OK
- ((varp Ta)
- (let ((oldvalue (symbol-value Ta)))
- (push (cons Ta oldvalue) oldvaluelist)
- (bind Ta Tb)
- (push (list oldvalue Tb) termpairlist)
- ))
- ((varp Tb)
- (let ((oldvalue (symbol-value Tb)))
- (push (cons Tb oldvalue) oldvaluelist)
- (bind Tb Ta)
- (push (list Ta oldvalue) termpairlist)
- ))
- ((and (consp Ta) (consp Tb))
- (push (list (cdr Ta) (cdr Tb)) termpairlist)
- (push (list (car Ta) (car Tb)) termpairlist)
- )
- (t
- (undobinds oldvaluelist)
- (return 'impossible)
- )
- ) ) ) )
-
- (defun undobinds (oldvaluelist)
- (dolist (pair oldvaluelist) (set (car pair) (cdr pair)))
- )
-
- #| Kontrollstruktur: Box
- +----------+
- ----CALL---->| |-----RETURN---->
- | |
- <---FAIL-----| |<----REDO-------
- +----------+
-
- Bei CALL und RETURN wächst der Stack, bei FAIL und REDO schrumpft er.
- CALL ist ein normaler Prozedur-Aufruf,
- FAIL ist ein normaler Prozedur-Rücksprung, der beim Aufrufer als REDO wirkt.
- RETURN ist (da der Stack wachsen muß) auch ein Aufruf!
- |#
-
- (defstruct (hornclause :constructor
- (:constructor make-clause (vars head &optional body)))
- vars ; Liste von Variablen, die in head und body zu instantiieren sind
- head ; Der Kopf der Klause, mit ihr ist zu unifizieren
- body ; Die zu erfüllende Form, meist (and form1 ... formk)
- ; nil [für Klausen 'fact.'] bedeutet soviel wie (and) : sofort erfüllt.
- )
-
- ; Prädikate, die Lisp-Funktionen sind, werden als Primitives angesehen.
- (defun primitivep (pred)
- (and (null (get pred 'prolog)) (fboundp pred))
- )
-
- ; versucht alle Lösungen des Goals form zu bestimmen, liefert die
- ; Lösungen einzeln mit Aufruf von returnfun, und führt bei einem Fail
- ; einen normalen Rücksprung aus.
- (defun prolog-form (form returnfun &optional cut-tag)
- (let ((pred (first form)))
- (cond ((eq pred 'fail)) ; sofort return-> fail, Ignorierung von returnfun
- ((eq pred 'is)
- (unless (varp (second form))
- (error "Zuweisung an ~S mit IS unmöglich, da keine Variable")
- )
- (let* ((var (second form))
- (oldvaluelist
- (unify (list (list
- var
- (eval (make-lispterm (third form)))
- )) ) ) )
- (if (listp oldvaluelist)
- (unwind-protect
- (funcall returnfun)
- (undobinds oldvaluelist)
- )) ) )
- ((eq pred 'and)
- (funcall
- (reduce
- #'(lambda (formi fun)
- (function (lambda () (prolog-form formi fun cut-tag)))
- )
- (cdr form)
- :from-end t :initial-value returnfun
- )) )
- ((eq pred 'or)
- (dolist (subform (cdr form))
- (prolog-form subform returnfun cut-tag)
- ; nach fail die nächste Subform probieren
- ))
- ((eq pred '!) ;cut
- (funcall returnfun) ; eine Lösung suchen
- (throw cut-tag nil) ; danach das ganze Prädikat abbrechen
- ; (Bindungen rückgängig machen nicht vergessen!)
- )
- ((eq pred 'call)
- (prolog-form (make-lispterm (second form)) returnfun cut-tag)
- )
- ((get pred 'prolog)
- (if (get pred 'prologtraced)
- (print-bindings '(call) (list form))
- )
- (let* ((new-cut-tag (gensym))
- (clauses (get pred 'prolog)))
- (catch new-cut-tag
- (dolist (clause clauses)
- (let* ((oldvars (hornclause-vars clause))
- (head (hornclause-head clause))
- (body (hornclause-body clause)))
- (if (/= (length form) (length head))
- (error "Bad number of arguments to ~S, wanted ~S, ~
- received ~S" pred (length head) (length form)
- ) )
- (dolist (var oldvars)
- (let ((newvar (make-var var)))
- (setq head (subst newvar var head))
- (setq body (subst newvar var body))
- ) )
- (let* ((returnfun1
- (if (get pred 'prologtraced)
- (function
- (lambda ()
- (print-bindings '(return) (list form))
- (funcall returnfun)
- (print-bindings '(redo) (list form))
- ) )
- returnfun
- ) )
- (oldvaluelist (unify (list (list form head)))))
- (if (listp oldvaluelist)
- (unwind-protect
- (if body
- (prolog-form body returnfun1 new-cut-tag)
- (funcall returnfun1)
- )
- (undobinds oldvaluelist)
- ) ) ) ; bei IMPOSSIBLE sofort FAIL für diese Clause.
- ) ) ) )
- (if (get pred 'prologtraced)
- (print-bindings '(fail) (list form))
- ))
- ((primitivep pred)
- (apply pred (mapcar #'make-lispterm (cdr form)))
- (funcall returnfun) ; ein REDO ergibt automatisch ein FAIL.
- )
- (t (cerror "It will fail." "Undefined predicate ~S" pred))
- ) ) )
-
-
- ; Definition eines Prolog-Prädikates
- (defmacro deflog (name &rest clauses)
- `(setf (get ',name 'prolog)
- ',(mapcar #'(lambda (clause) (apply #'make-clause clause))
- clauses
- ) )
- )
-
- (defmacro prologtrace (name)
- `(setf (get ',name 'prologtraced) T)
- )
-
- (defmacro prologuntrace (name)
- `(remprop ',name 'prologtraced)
- )
-
-
- (defun goal1 (vars form &aux (newvars nil)) ; löst form nach vars auf.
- (if (null vars)
- (block maingoal
- (catch 'main-cut-tag
- (prolog-form form
- #'(lambda () (format t "~%Yes.") (return-from maingoal nil))
- 'main-cut-tag
- )
- (format t "~%No.")
- ) )
- (prog ((foundsome nil))
- (dolist (var vars)
- (let ((newvar (make-var var)))
- (setq form (subst newvar var form))
- (push newvar newvars)
- ) )
- (setq newvars (nreverse newvars))
- (catch 'main-cut-tag
- (prolog-form form
- #'(lambda () (setq foundsome t) (print-bindings vars newvars))
- 'main-cut-tag
- ) )
- (format t "~%No ~:[~;other ~]solutions." foundsome)
- ) )
- (values)
- )
-
- (defmacro goal (vars form)
- `(time (goal1 ',vars ',form))
- )
-
-