-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathprolog.lisp
209 lines (142 loc) · 5.29 KB
/
prolog.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
;;;; -*- Mode: Lisp; Syntax: Common-Lisp -*-
;;;; Code from Paradigms of AI Programming
;;;; Copyright (c) 1991 Peter Norvig
;;;; File prolog.lisp: prolog from (11.3), with interactive backtracking.
(tao:common-lisp)
(in-package :tao.logic)
(defvar *negation-as-failure* nil)
(defun tao:negation-as-failure (&optional (negation-as-failure? nil negation-as-failure?-sup?))
(if negation-as-failure?-sup?
(setq *negation-as-failure* negation-as-failure?)
*negation-as-failure*))
(define-compiler-macro tao:negation-as-failure (&whole w &optional (negation-as-failure? nil negation-as-failure?-sup?))
(declare (ignore negation-as-failure?))
(if negation-as-failure?-sup?
*negation-as-failure*
w))
;;;; does not include destructive unification (11.6); see prologc.lisp
;; clauses are represented as (head . body) cons cells
(defun clause-head (clause) (first clause))
(defun clause-body (clause) (rest clause))
;; clauses are stored on the predicate's plist
(defun get-clauses (pred) (get pred 'clauses))
(defun (setf get-clauses) (val pred) (setf (get pred 'clauses) val))
(defun predicate (relation)
(if (atom relation)
relation
(first relation)))
#|(defun args (x)
"The arguments of a relation"
(if (atom x)
nil
(rest x)))|#
(defvar *db-predicates* nil
"a list of all predicates stored in the database.")
(defun add-clause (clause)
"add a clause to the data base, indexed by head's predicate."
;; the predicate must be a non-variable symbol.
(let ((pred (predicate (clause-head clause))))
(assert (and (symbolp pred) (not (variable-p pred))))
(pushnew pred *db-predicates*)
(setf (get pred 'clauses)
(nconc (get-clauses pred) (list clause)))
pred))
(defun clear-db ()
"remove all clauses (for all predicates) from the data base."
(mapc #'clear-predicate *db-predicates*))
(defun clear-predicate (predicate)
"remove the clauses for a single predicate."
(setf (get predicate 'clauses) nil))
(defun rename-variables (x)
"replace all variables in x with new ones."
(sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))
(variables-in x))
x))
;; cf. unique-find-if-anywhere
(defun unique-find-anywhere-if (predicate tree &optional found-so-far)
(unique-find-if-anywhere predicate tree found-so-far))
;; cf. find-if-anywhere
(defun find-anywhere-if (predicate tree)
(find-if-anywhere predicate tree))
(defmacro ?- (&rest goals) `(top-level-prove ',(replace-_-vars goals)))
(defmacro ?-all (&rest goals) `(top-level-prove-all ',(replace-_-vars goals)))
(defun prove-all (goals bindings)
"Find a solution to the conjunction of goals."
(cond ((eq bindings fail) fail)
((null goals) bindings)
(t (prove (first goals) bindings (rest goals)))))
(defun prove (goal bindings other-goals)
"Return a list of possible solutions to goal."
(let ((clauses (get-clauses (predicate goal))))
(if (listp clauses)
(some
#'(lambda (clause)
(let ((new-clause (rename-variables clause)))
(prove-all
(append (clause-body new-clause) other-goals)
(unify goal (clause-head new-clause) bindings))))
clauses)
;; The predicate's "clauses" can be an atom:
;; a primitive function to call
(funcall clauses (rest goal) bindings
other-goals))))
(defun top-level-prove (goals)
(prove-all `(,@goals (show-prolog-vars ,@(variables-in// goals)))
no-bindings)
(format t "~&no")
(values))
(defun top-level-prove-all (goals)
(prove-all `(,@goals (show-all-prolog-vars ,@(variables-in// goals)))
no-bindings)
'tao::that\'s-all)
(defun show-prolog-vars (vars bindings other-goals)
"Print each variable with its binding.
Then ask the user if more solutions are desired."
(if (null vars)
(format t "~&Yes")
(dolist (var vars)
(format t "~&~a = ~a" var
(subst-bindings bindings var))))
(force-output)
(if (continue-p)
fail
(prove-all other-goals bindings)))
(defun show-all-prolog-vars (vars bindings other-goals)
(declare (ignore other-goals))
(if (null vars)
(format t "~&Yes")
(dolist (var vars)
(format t "~&~a = ~a" var
(subst-bindings bindings var))))
(force-output)
fail)
(setf (get 'show-prolog-vars 'clauses) 'show-prolog-vars)
(setf (get 'show-all-prolog-vars 'clauses) 'show-all-prolog-vars)
(defun continue-p ()
"Ask user if we should continue looking for solutions."
(case (read-char)
(#\; t)
(#\. nil)
(#\newline (continue-p))
(otherwise
(format t " Type ; to see more or . to stop")
(continue-p))))
(defun variables-in (exp)
"Return a list of all the variables in EXP."
(variables-in/ exp))
(defun variables-in// (exp)
"Return a list of all the variables in EXP."
(unique-find-anywhere-if #'non-anon-variable-p exp))
(defun variables-in/ (exp)
(declare (ignore exp))
'())
(defun non-anon-variable-p (x)
(and (variable-p x) (not (eq x '_))))
(defun replace-_-vars (exp)
"Replace any _ within exp with a var of the form _123."
(cond ((eq exp '_) (gensym "_"))
((atom exp) exp)
(t (reuse-cons (replace-_-vars (first exp))
(replace-_-vars (rest exp))
exp))))
;;; *EOF*