📄 prolog.lsp
字号:
;;Rules are represented as (head bodys) list,
;; stored in the predicate's plist
;; for example,
;; R1=(Head Bodys)
;; =((p ...)(q ...)(r ...)...)
;; Append R into (get p 'rules)
(defvar *prolog-rules* nil)
(defun add-index (index)
(setf *prolog-rules* (adjoin index *prolog-rules*)) )
(defun clear-index (index)
(setf (get index 'rules) nil))
(defun get-index (rule) (caar rule))
(defmacro <-- (rule) `(add-rule ',rule))
(defmacro fact (&rest facts) `(add-rule ',facts))
(defmacro rule (head sign &rest rules)
`(<-- (,head ,@rules)))
(defun add-rule (rule)
(let* ((index (get-index rule))
(oldrules (get index 'rules)))
(add-index index)
(setf (get index 'rules)
(nconc oldrules (list rule)))
(format t "~&Add ~a to ~a --> ~a " rule index (get index 'rules))
) )
(defun clear-rules ()
(dolist (x *prolog-rules*)
(clear-index x))
(setf *prolog-rules* nil)
)
(defun my-prove (goal binds)
;(format t "~&Prove ~a" (get (get-index goal) 'rules))
(let ((result nil))
(dolist (rule (get (get-index goal) 'rules) result)
(let* ((nr (rename-var rule))
(tmp (my-prove-all (cdr nr)
(unify-binds (car goal)(car nr) binds)
)) )
(setf result (append tmp result))
) ) ) )
(defun my-prove-all (goals binds)
(cond
((null binds) nil)
((null goals) (list binds))
(t (let ((result nil))
(dolist (x (my-prove goals binds) result)
(setf result
(append (my-prove-all (rest goals) x) result)
) ) ) )) )
(defun my-prove-one-by-one (goals binds)
(cond
((null binds) nil)
((null goals) binds)
(t (my-prove-one (first goals) binds (rest goals))
) ) )
(defun my-prove-one (goal binds rest-goals)
(let ((clauses (get (first goal) 'rules)))
(cond
((listp clauses)
(some #'(lambda (rule)
(format t "~&Try rule ~a" rule)
(let ((nr (rename-var rule)))
(my-prove-one-by-one
(append (rest nr) rest-goals)
(unify-binds goal (first nr) binds)
)) )
clauses
))
((eql '! clauses) nil)
((eql '$ clauses)
(show-result (rest goal) binds)
(if (continue-p)
nil
(my-prove-one-by-one rest-goals binds)
))
) ) )
(defun one-by-one-with-cut (goals binds)
(cond
((null binds) (values nil nil))
((null goals) (values binds nil))
(t (multiple-value-bind (bs cut?)
(one-with-cut (first goals) binds (rest goals))
(values bs cut?)
) ) ) )
(defun one-with-cut (goal binds rest-goals)
(let ((clauses (get (first goal) 'rules)))
(cond
((listp clauses)
(let ((cutvalue nil)(bs2 nil))
(dolist (rule clauses)
(format t "~&Try rule ~a" rule)
(let ((nr (rename-var rule)))
(multiple-value-bind (bs cut?)
(one-by-one-with-cut
(append (rest nr) rest-goals)
(unify-binds goal (first nr) binds)
)
(setf cutvalue cut?)
(setf bs2 bs)
) )
(when cutvalue (return))
)
(values bs2 cutvalue)
))
((eql '! clauses)
(format t "~&* Cut here! *")
(multiple-value-bind (bs cut?)
(one-by-one-with-cut rest-goals binds)
(values bs t)
))
((eql '$ clauses)
; (format t "~&$..binds= ~a" binds)
(show-result (rest goal) binds)
(if (continue-p)
(values nil nil)
(multiple-value-bind (bs cut?)
(one-by-one-with-cut rest-goals binds)
(values bs cut?)
) )
)
) ) )
(defun continue-p ()
(case (read-char)
(#\; t)
(#\. nil)
(#\newline (continue-p))
(otherwise
(format t " Enter ; to see more or . to stop")
(continue-p)
) ) )
(defun rename-var (x)
"replace all variables in x with new ones."
(sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))
(vars-in x))
x
) )
(defun vars-in (exp)
(let* ((tmp1 (DF-search exp))
(tmp2 (remove-if-not #'var-p tmp1))
(result nil))
(dolist (x tmp2 result)
(setf result (adjoin x result))
) ) )
(defun DF-search (L)
(cond ((null L) ())
((atom L) (list L))
(t `(,@(DF-search (car L))
,@(DF-search (cdr L)))
) ) )
;(defmacro ?- (&rest goals) `(my-prove-all ',goals '(())))
(defmacro ?? (&rest goals) `(top-level-prove ',goals))
(defmacro ?1 (&rest goals) `(top-level-prove-one-by-one ',goals))
(defmacro ?1c (&rest goals) `(top-level-one-by-one-with-cut ',goals))
(defun unify-binds (x y binds)
(cond
((and (null x)(null y))
(if (null binds) t binds ))
((or (null x)(null y)) nil)
((eql x y) binds)
((eql (car x)(car y))
(unify-binds (cdr x)(cdr y) binds))
((header-p (car x) #\?)
(let ((new-binds (extend-binds (car x) (car y) binds)))
(if (null new-binds)
nil
(unify-binds (cdr x)(cdr y) new-binds)
)) )
((header-p (car y) #\?)
(let ((new-binds (extend-binds (car y) (car x) binds)))
(if (null new-binds)
nil
(unify-binds (cdr x)(cdr y) new-binds)
)) )
) )
(defun header-p (x head)
(and (symbolp x)
(char= (char (symbol-name x) 0) head )))
(defun extend-binds (x y b)
(let ((xpair (assoc x b))
(ypair (assoc y b)))
(cond
((eql x y) b)
;binding of x exist
((not (null xpair))
(extend-binds (second xpair) y b))
;binding of x not exist
((and (var-p y) ypair)
(extend-binds x (second ypair) b))
;neither x nor y is variable
((and (not (var-p x))(not (var-p y)))
(if (eql x y) b nil))
(t (if (var-p x)
(cons (list x y) b)
(cons (list y x) b)))
) ) )
(defun do-binds (binds x)
"Replace all bindings of variables in x"
(cond
((null binds) x)
((and (var-p x)(assoc x binds))
(do-binds binds (second (assoc x binds))))
((atom x) x)
(t (cons (do-binds binds (car x))
(do-binds binds (cdr x))
) ) ) )
(defun var-p (x) (header-p x #\?))
(defun unify (x y)
(let ((bindings nil))
(do-binds (unify-binds x y bindings) y)
) )
(defun top-level-prove (goals)
"Prove the goals, and print variables readably."
(let ((solutions (my-prove-all goals '(()) ))
(vars (vars-in goals)) )
(cond
((null solutions) (format t "~&No."))
(t (dolist (x solutions)
(show-result vars x))
) )
)
(values)
)
(defun top-level-prove-one-by-one (goals)
(my-prove-one-by-one `(,@goals ($ ,@(vars-in goals))) '(()) )
(format t "~&No.")
(values)
)
(defun top-level-one-by-one-with-cut (goals)
(one-by-one-with-cut `(,@goals ($ ,@(vars-in goals))) '(()) )
(format t "~&No.")
(values)
)
(defun show-result (vars binds)
"Print each variable with its binding."
(if (null vars)
(format t "~&Yes")
(dolist (x vars)
(format t " ~a = ~a" x (do-binds binds x)
) ) )
(format t ";~&")
)
(setf (get '$ 'rules) '$)
(setf (get '! 'rules) '!)
(clear-rules)
(fact (girl mary))
(fact (girl joy))
(fact (boy john))
(fact (boy tom))
(fact (pet cat))
(fact (pet dog))
(fact (love john mary))
(fact (like john dog))
(fact (like tom car))
(fact (like mary cat))
(rule (like joy ?x) if (pet ?x))
(rule (love mary ?x) if (boy ?x)(like ?x ?y)(pet ?y))
(rule (like ?x car) if (boy ?x))
(rule (like ?x ?y) if (boy ?x)(girl ?y))
(rule (like ?x ?y) if (girl ?x)(boy ?y))
;Occur-check!!
;(rule (like ?x ?y) if (like ?x ?z)(like ?y ?z))
(fact (smaller 0 3))
(fact (smaller 1 3))
(fact (smaller 2 3))
(fact (smaller 6 8))
(fact (smaller 6 9))
(rule (smaller ?x 6) if (smaller ?x 3))
(rule (f ?x 0) if (smaller ?x 3) (!))
(rule (f ?x 2) if (smaller ?x 6) (!))
(rule (f ?x 4) if (smaller 6 ?x))
(rule (g ?x 0) if (smaller ?x 3))
(rule (g ?x 2) if (smaller ?x 6))
(rule (g ?x 4) if (smaller 6 ?x))
(fact (u 1)) (fact (u 2)) (fact (u 3))
(fact (v 4)) (fact (v 5))
(fact (w 6)) (fact (w 7)) (fact (w 8))
(rule (combin ?x ?y ?z) if (u ?x)(v ?y)(w ?z))
(rule (combin-cut2 ?x ?y ?z) if (u ?x)(v ?y)(!)(w ?z))
(rule (combin-cut1 ?x ?y ?z) if (u ?x)(!)(v ?y)(w ?z))
;(defun prove (goal binds)
; (format t "~&Prove ~a" (get (get-index goal) 'rules))
; (mapcan #'(lambda (rule)
; (let ((nr (rename-var rule)))
; (prove-all (cdr nr)
; (unify-binds (car goal) (car nr) binds)
; ) ) )
; (get (get-index goal) 'rules)
;) )
;(defun prove-all (goals binds)
; (cond
; ((null binds) nil)
; ((null goals) (list binds))
; (t (mapcan #'(lambda (one-solution)
; (prove-all (rest goals) one-solution))
; (prove goals binds)
;) ) ) )
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -