Codebase list cafeobj / 23ef61a
Search predicate should use plain old hash mechanisms for treating terms with operator theory properly. Toshimi Sawada 5 years ago
2 changed file(s) with 338 addition(s) and 519 deletion(s). Raw diff Collapse all Expand all
+0
-309
chaos/cafein/apply-rule.lisp less more
0 ;;;-*-Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp -*-
1 ;;;
2 ;;; Copyright (c) 2000-2018, Toshimi Sawada. All rights reserved.
3 ;;;
4 ;;; Redistribution and use in source and binary forms, with or without
5 ;;; modification, are permitted provided that the following conditions
6 ;;; are met:
7 ;;;
8 ;;; * Redistributions of source code must retain the above copyright
9 ;;; notice, this list of conditions and the following disclaimer.
10 ;;;
11 ;;; * Redistributions in binary form must reproduce the above
12 ;;; copyright notice, this list of conditions and the following
13 ;;; disclaimer in the documentation and/or other materials
14 ;;; provided with the distribution.
15 ;;;
16 ;;; THIS SOFTWARE IS PROVIDED BY THE AUTHOR 'AS IS' AND ANY EXPRESSED
17 ;;; OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
18 ;;; WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
19 ;;; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
20 ;;; DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
21 ;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
22 ;;; GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
23 ;;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
24 ;;; WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
25 ;;; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
26 ;;; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27 ;;;
28 (in-package :chaos)
29 #|=============================================================================
30 System:CHAOS
31 Module:cafein
32 File:apply-rule.lisp
33 =============================================================================|#
34 #-:chaos-debug
35 (declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
36 #+:chaos-debug
37 (declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
38
39 ;;;*****************************************************************************
40 ;;; BASIC PROCS for REWRITE RULE APPLICATION ***********************************
41 ;;;*****************************************************************************
42 ;;; (defvar *rewrite-debug* nil)
43
44 ;;; APPLY-RULE : rule term -> Bool
45 ;;;-----------------------------------------------------------------------------
46 ;;; Returns true iff the rule has been sucessfully apply. Note that in this case
47 ;;; "term" is also modified.
48 ;;; The associative extensions are automatiquely generated and applied if needed.
49 ;;;
50 (defun apply-rule (rule term)
51 (declare (type axiom rule)
52 (type term term)
53 (values (or null t)))
54 (let ((is-applied nil))
55 (tagbody
56 (when (rule-is-rule rule)
57 (if *rewrite-exec-mode*
58 (go do-apply)
59 (return-from apply-rule nil)))
60 ;; rule is equation
61 (when (and (not *cexec-normalize*)
62 (term-is-applform? term)
63 (method-has-trans-rule (term-head term)))
64 (return-from apply-rule nil))
65 ;;----
66 do-apply
67 ;;----
68 ;;
69 ;; first apply the given rule.
70 (setq is-applied (apply-one-rule rule term))
71
72 ;; then there may be some extensions.
73 (when (and (not is-applied) (term-is-applform? term))
74 (let ((top (term-head term)))
75 (declare (type method top))
76 (unless (let ((val (axiom-kind rule)))
77 (and val
78 (not (eq :id-theorem val))
79 (not (eq :idem-theory val))))
80 (when (method-is-associative top)
81 (if (method-is-commutative top)
82 (setq is-applied
83 (or (apply-AC-extension rule term top)
84 is-applied))
85 ;; the operator is only associative,
86 (setq is-applied
87 (or (apply-A-extensions rule term top)
88 is-applied))
89 )))))
90 )
91 ;; return t iff the rule is applied.
92 is-applied))
93
94 ;;;
95 ;;; APPLY-ONE-RULE
96 ;;;
97 (defun apply-one-rule (rule term)
98 (declare (ignore rule term))
99 (format t "~%APPLY-ONE-RULE : INTERNAL ERROR, SPECIFIC REWRITEING ENGINE ISN'T SPECIFIED.")
100 (break))
101
102 (declaim (inline term-replace-dd-simple))
103 #-gcl
104 (defun term-replace-dd-simple (old new)
105 (declare (type term old new)
106 (values term))
107 (incf *rule-count*)
108 (term-replace old new))
109
110 #+gcl
111 (si::define-inline-function term-replace-dd-simple (old new)
112 (incf *rule-count*)
113 (term-replace old new))
114
115 (defmacro beh-context-ok? (rule)
116 ` (if *rewrite-semantic-reduce*
117 (if (axiom-is-behavioural ,rule)
118 (check-beh-context)
119 t)
120 t))
121
122 (defun apply-one-rule-simple (rule term)
123 (declare (type axiom rule)
124 (type term term)
125 (values (or null t)))
126 (declare (inline term-replace-dd-simple))
127 ;;
128 (block the-end
129 (let* ((condition nil)
130 next-match-method
131 (*self* term))
132 (multiple-value-bind (global-state subst no-match E-equal)
133 (funcall (rule-first-match-method rule) (rule-lhs rule) term)
134 (incf $$matches)
135 (when no-match (return-from the-end nil))
136
137 ;;
138 (unless (beh-context-ok? rule)
139 (return-from the-end nil))
140 ;;
141 ;; technical assignation related to substitution-image.
142 (when E-equal (setq subst nil))
143
144 ;; match success -------------------------------------
145 ;; then, the condition must be checked
146 (block try-rule
147 (catch 'rule-failure
148 ;;
149 (when (and (is-true? (setq condition (rule-condition rule)))
150 (null (rule-id-condition rule)))
151 ;; there is no condition --
152 ;; rewrite term.
153 (term-replace-dd-simple
154 term
155 ;; note that the computation of the substitution
156 ;; made a copy of the rhs.
157 (substitution-image-simplifying subst
158 (rule-rhs rule)))
159 (return-from the-end t))))
160
161 ;; if the condition is not trivial, we enter in a loop
162 ;; where one try to find a match such that the condition
163 ;; is satisfied.
164 (setf next-match-method (rule-next-match-method rule))
165 (loop (when no-match (return))
166 (unless (beh-context-ok? rule)
167 (return-from the-end nil))
168 (block try-rule
169 (catch 'rule-failure
170 (if (and (or (null (rule-id-condition rule))
171 (rule-eval-id-condition subst
172 (rule-id-condition rule)))
173 (is-true?
174 (let (($$cond (substitution-image subst condition))
175 (*rewrite-exec-mode*
176 (if *rewrite-exec-condition*
177 *rewrite-exec-mode*
178 nil)))
179 ;; no simplyfing since probably wouldn't pay
180 (if *rewrite-semantic-reduce*
181 (normalize-term-with-bcontext $$cond)
182 (normalize-term $$cond))
183 $$cond)))
184 ;; the condition is satisfied
185 (progn
186 (term-replace-dd-simple
187 term
188 (substitution-image-simplifying subst
189 (rule-rhs rule)))
190 (return-from the-end t))
191 nil)))
192
193 ;; else, try another ...
194 (multiple-value-setq (global-state subst no-match)
195 (progn
196 (incf $$matches)
197 (funcall next-match-method global-state)
198 ))
199
200 );; end loop
201
202 ;; In this case there is no match at all and the rule does not apply.
203 (return-from the-end nil)))))
204
205 ;;; INIT
206 (eval-when (:execute :load-toplevel)
207 (setf (symbol-function 'apply-one-rule)
208 (symbol-function 'apply-one-rule-simple)))
209
210 ;;; APPLY-A-EXTENSIONS : rule term method -> Bool
211 ;;;-----------------------------------------------------------------------------
212 ;;; Apply the associative-extensions. returns true iff the some rule is applied.
213 ;;;
214 (defun apply-A-extensions (rule term top)
215 (declare (type axiom rule)
216 (type term term)
217 (type method top)
218 (values (or null t)))
219 ;; (declare (optimize (speed 3) (safety 0)))
220 (let ((listext (!axiom-a-extensions rule))
221 (a-ext nil)
222 (is-applied nil))
223 (when (null listext)
224 ;; then need to pre-compute the extensions and store then
225 (setq listext (compute-A-extensions rule top)))
226 (when (setq a-ext (car listext))
227 ;; the first extension exists
228 (setq is-applied (apply-one-rule a-ext term)))
229 (setq listext (cdr listext))
230 (when (setq a-ext (car listext))
231 ;; the second extension exists
232 (setq is-applied (or (apply-one-rule a-ext term)
233 is-applied)))
234 (setq listext (cdr listext))
235 (when (setq a-ext (car listext))
236 ;; the third extension exists
237 (setq is-applied (or (apply-one-rule a-ext term)
238 is-applied)))
239 ;;
240 is-applied))
241
242 ;;; APPLY-AC-EXTENSION : rule term method -> Bool
243 ;;;-----------------------------------------------------------------------------
244 ;;; Apply the associative-commutative-extension. returns t iff the rule is applied.
245 ;;;
246 (defun apply-AC-extension (rule term top)
247 (declare (type axiom rule)
248 (type term term)
249 (type method top)
250 (values (or null t)))
251 (let ((listext (give-AC-extension rule))
252 (is-applied nil))
253 (when (car listext)
254 ;; the extension exists
255 (setq is-applied (apply-one-rule (car listext) term)))
256 is-applied))
257
258 ;;; RULE-EVAL-ID-CONDITION : substitution condition ->
259 ;;;-----------------------------------------------------------------------------
260 ;;; really not not want to use normalize -- perhaps could use normal expressions.
261 (defun rule-eval-id-condition (subst cond)
262 (declare (type list subst cond)
263 (values (or null t)))
264 (cond ((eq 'and (car cond))
265 (dolist (sc (cdr cond) t)
266 (unless (rule-eval-id-condition subst sc) (return nil))))
267 ((eq 'not-equal (car cond))
268 (not (term-is-similar?
269 (rule-eval-term subst (cadr cond))
270 (rule-eval-term subst (caddr cond)))))
271 ((eq 'equal (car cond))
272 (term-is-similar?
273 (rule-eval-term subst (cadr cond))
274 (rule-eval-term subst (caddr cond))))
275 ((eq 'or (car cond))
276 (dolist (sc (cdr cond) nil)
277 (when (rule-eval-id-condition subst sc) (return t))))
278 ((eq 'not (car cond))
279 (not (rule-eval-id-condition subst (cadr cond))))
280 ((eq 'xor (car cond)) ;@@ remove?
281 (let ((res nil))
282 (dolist (sc (cdr cond))
283 (setq res (if (rule-eval-id-condition subst sc) (not res) res)))
284 res))
285 (t (break "rule-eval-id-condition: illegal condition"))
286 ))
287
288 ;;; RULE-EVAL-TERM : teta term -> term'
289 ;;;
290 (defun rule-eval-term (teta term)
291 (declare (type list teta)
292 (type term term)
293 (values list))
294 (macrolet ((assoc% (_x _y)
295 `(let ((*_lst ,_y))
296 (loop
297 (when (null *_lst) (return nil))
298 (when (eq ,_x (caar *_lst)) (return (car *_lst)))
299 (setq *_lst (cdr *_lst))))))
300 (cond ((term-is-variable? term)
301 (let ((im (cdr (assoc% term teta))))
302 (if im;; i.e. im = teta(term)
303 im
304 ;; if variable doesn't have a binding, it evaluates to itself
305 term)))
306 (t term))))
307
308 ;;; EOF
+338
-210
thstuff/cexec.lisp less more
00 ;;;-*-Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp -*-
11 ;;;
2 ;;; Copyright (c) 2000-2015, Toshimi Sawada. All rights reserved.
2 ;;; Copyright (c) 2000-2018, Toshimi Sawada. All rights reserved.
33 ;;;
44 ;;; Redistribution and use in source and binary forms, with or without
55 ;;; modification, are permitted provided that the following conditions
3939 ;;;
4040 (declaim (special $$cexec-term)) ; the target term
4141
42 ;;; Basic Data Structures
43
44
4245 ;;; *****
4346 ;;; RULEs
4447 ;;; *****
6164 (defvar .rules-so-far. 0)
6265
6366 (defun print-rule-pattern (rpat &optional (stream *standard-output*) &rest ignore)
67 (declare (type rule-pat rpat)
68 (type stream stream)
69 (ignore ignore))
6470 (format stream "~%-- rule pattern: ~d" (rule-pat-num rpat))
6571 (format stream "~% posisition: ~a" (rule-pat-pos rpat))
6672 (format stream "~& rule :")(print-chaos-object (rule-pat-rule rpat))
6874 (format stream "~& cond-ok :~a" (rule-pat-cond-ok rpat))
6975 (format stream "~& condition :")(term-print (rule-pat-condition rpat)))
7076
71 (defun make-rule-pat-with-check (pos rule subst sch-context)
72 (when (rule-non-exec rule)
73 ;; the rule is marked as non-executable
74 (return-from make-rule-pat-with-check nil))
75 (let ((condition (rule-condition rule)))
76 ;; pre check whether the condition part is satisfied or not
77 (when (and (is-true? condition)
78 (null (rule-id-condition rule)))
79 ;; rule is not conditional
80 (return-from make-rule-pat-with-check
81 (make-rule-pat :pos pos :rule rule :subst subst :num (incf .rules-so-far.))))
82 ;; check the condition
83 (let (($$term nil)
84 ($$cond (set-term-color (substitution-image-cp subst condition))))
85
86 (when *cexec-debug*
87 (format t "~%rule: cond ") (term-print-with-sort $$cond)
88 (format t "~% subst") (print-substitution subst)
89 (let ((vars (term-variables $$cond)))
90 (dolist (v vars)
91 (format t "~% var ") (term-print-with-sort v))))
92
93 (catch 'rule-failure
94 (if (and (or (null (rule-id-condition rule))
95 (rule-eval-id-condition subst
96 (rule-id-condition rule)
97 :slow))
98 (is-true? (progn (normalize-term $$cond) $$cond)))
99 ;; the condition is satisfied
100 (return-from make-rule-pat-with-check
101 (make-rule-pat :pos pos :rule rule :subst subst :cond-ok t :condition $$cond :num (incf .rules-so-far.)))
102 (if (rwl-sch-context-if sch-context)
103 ;; rule condition fail & there exists 'if'
104 (return-from make-rule-pat-with-check
105 (make-rule-pat :pos pos :rule rule :subst subst :cond-ok nil :condition $$cond :num (incf .rules-so-far.)))
106 (return-from make-rule-pat-with-check nil))))
107 nil)))
108
109 (defun rule-pat-equal (pat1 pat2)
110 (and (equal (rule-pat-pos pat1) (rule-pat-pos pat2))
111 (eq (rule-pat-rule pat1) (rule-pat-rule pat2))
112 (substitution-equal (rule-pat-subst pat1) (rule-pat-subst pat2))))
113
114 ;;; *****
115 ;;; STATE
116 ;;; *****
117
77 ;;; *********
11878 ;;; RWL-STATE
79 ;;; *********
11980 ;;; represents a state
12081 ;;;
12182 (defstruct (rwl-state
12283 (:print-function pr-rwl-state))
123 (state 0 :type fixnum) ; fixnum value identifying this state
124 (term nil) ; a term
125 (trans-rules nil) ; applicable rules to this state
126 (rule-pat nil) ; the rule-pat which derived this state
127 (subst nil) ; list of substitution !!
128 (is-final nil) ; t iff the state is a final state
129 (loop nil) ; t iff the same state occurs more than once
130 (condition nil) ;
131 (depth 0 :type fixnum) ; nesting depth of rwl-search*
84 (state 0 :type fixnum) ; fixnum value identifying this state
85 (term nil :type (or null term)) ; a term
86 (trans-rules nil :type list) ; applicable rules to this state
87 (rule-pat nil :type (or null rule-pat)) ; the rule-pat which derived this state
88 (subst nil :type list) ; list of substitution !!
89 (is-final nil :type (or null t)) ; t iff the state is a final state
90 (loop nil :type (or null t)) ; t iff the same state occurs more than once
91 (condition nil) ;
92 (depth 0 :type fixnum) ; nesting depth of rwl-search*
13293 )
13394
134 (defun state-is-valid-transition (state)
135 (let ((cond (rwl-state-condition state)))
136 (and (not (rwl-state-loop state))
137 (or (null cond)
138 (is-true? cond)))))
139
140 (defun pr-rwl-state (state &optional (stream *standard-output*) &rest ignore)
141 (declare (ignore ignore))
142 (let ((*standard-output* stream))
143 (format t "#<rwl-state(~D):" (rwl-state-state state))
144 (term-print (rwl-state-term state))
145 (princ ", ")
146 (dolist (sub (rwl-state-subst state))
147 (print-substitution sub))
148 (when (rwl-state-is-final state)
149 (princ " ,final"))
150 (princ ">")))
151
152 (declaim (special .rwl-search-depth.))
153 (defvar .rwl-search-depth. -1)
154
155 (defun print-rwl-state (state &optional (stream *standard-output*) &rest ignore)
156 (declare (ignore ignore)
157 (type rwl-state state)
158 (type stream stream))
159 (let ((*standard-output* stream))
160 (format t "~%[state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
161 (let ((*print-indent* (+ 4 *print-indent*)))
162 (term-print-with-sort (rwl-state-term state))
163 (when *cexec-trace*
164 (format t "~& matched with the substitution "))
165 (let ((*print-indent* (+ 4 *print-indent*)))
166 (dolist (subst (rwl-state-subst state))
167 (print-next)
168 (print-substitution subst)))
169 (flush-all))))
170
171 (defun print-state-transition (state sub-states &optional (stream *standard-output*))
172 (declare (type rwl-state state)
173 (type list sub-states)
174 (type stream stream))
175 (let ((*standard-output* stream)
176 (arc-num 0))
177 (declare (type fixnum arc-num))
178 (format t "~%[state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
179 (term-print-with-sort (rwl-state-term state))
180 (dolist (sub sub-states)
181 (format t "~& arc ~D --> [state ~D-~D] " arc-num (rwl-state-depth state) (rwl-state-state sub))
182 (let ((*print-indent* (+ 4 *print-indent*)))
183 (print-next)
184 (print-axiom-brief (rule-pat-rule (rwl-state-rule-pat sub))))
185 (incf arc-num))))
186
18795 ;;; ***********
188 ;;; SEARCH TREE
96 ;;; Search tree
18997 ;;; ***********
190
191 ;;; Search tree
19298 ;;; - bi-directional dag (see comlib/dag.lisp)
19399 ;;; - datum contains an instance of rwl-state.
194100 ;;;
205111 (declare (ignore ignore))
206112 (let ((*standard-output* stream))
207113 (format t "SCH-NODE:~A" (dag-node-datum node))))
208
209 ;;; ******************
210 ;;; RWL-SCH-NODE utils
211 ;;; ******************
212
213 ;;; print the rule & state
214 ;;;
215 (defun show-rwl-sch-state (dag &optional (path? t) (bind-pattern nil))
216 (declare (type rwl-sch-node dag))
217 (let* ((st (dag-node-datum dag))
218 (term (rwl-state-term st))
219 (rule-pat (rwl-state-rule-pat st))
220 (rl (if rule-pat (rule-pat-rule rule-pat)
221 nil)))
222 (when (and rl path?)
223 (print-next)
224 (princ " ")
225 (let ((*print-indent* (+ 8 *print-indent*)))
226 (print-chaos-object rl) ; (print-axiom-brief rl)
227 ))
228 (format t "~%[state ~D-~D] " (rwl-state-depth st) (rwl-state-state st))
229 (term-print-with-sort term)
230 (dolist (sub (rwl-state-subst st))
231 (format t "~& ")
232 (print-substitution sub)
233 (when bind-pattern
234 (let ((bimage (substitution-image-simplifying sub bind-pattern)))
235 (normalize-term bimage)
236 (format t "~% => ")
237 (term-print-with-sort bimage))))))
238
239 ;;; print the label of a rule which derived a state
240 ;;; that denode contains.
241 ;;;
242 (defun show-rwl-sch-label (dnode)
243 (declare (type rwl-sch-node dnode))
244 (let* ((dt (dag-node-datum dnode))
245 (rl (rule-pat-rule (rwl-state-rule-pat dt)))
246 (label (car (rule-labels rl))))
247 (if label
248 (format t "~&[~a]" label)
249 (format t "~&NONE"))))
250
251 ;;; **************
252 ;;; SEARCH CONTEXT
253 ;;; **************
254114
255115 ;;; RWL-SCH-CONTEXT
256116 ;;;
279139 (bind nil) ; ....
280140 (if nil) ;
281141 (pr-out? nil) ;
282 (term-hash nil :type hash-table) ; term hash table for catching loop
283142 )
284143
285144 (defun print-sch-context (ctxt &optional (stream *standard-output*) &rest ignore)
320179 (format t "~% if: ")
321180 (term-print-with-sort (rwl-sch-context-if ctxt))))))
322181
323 ;;; .RWL-SCH-CONTEXT.
324 ;;; moved to comlib/globals.lisp
325 ;;; (defvar .rwl-sch-context. nil)
182 ;;; **********************
183 ;;; RULE related unilities
184 ;;; **********************
185 (defun make-rule-pat-with-check (pos rule subst sch-context)
186 (declare (type list pos)
187 (type axiom rule)
188 (type substitution subst)
189 (type rwl-sch-context sch-context))
190 (when (rule-non-exec rule)
191 ;; the rule is marked as non-executable
192 (return-from make-rule-pat-with-check nil))
193 (let ((condition (rule-condition rule)))
194 ;; pre check whether the condition part is satisfied or not
195 (when (and (is-true? condition)
196 (null (rule-id-condition rule)))
197 ;; rule is not conditional
198 (return-from make-rule-pat-with-check
199 (make-rule-pat :pos pos :rule rule :subst subst :num (incf .rules-so-far.))))
200 ;; check the condition
201 (let (($$term nil)
202 ($$cond (set-term-color (substitution-image-cp subst condition))))
203
204 (when *cexec-debug*
205 (format t "~%rule: cond ") (term-print-with-sort $$cond)
206 (format t "~% subst") (print-substitution subst)
207 (let ((vars (term-variables $$cond)))
208 (dolist (v vars)
209 (format t "~% var ") (term-print-with-sort v))))
210
211 (catch 'rule-failure
212 (if (and (or (null (rule-id-condition rule))
213 (rule-eval-id-condition subst
214 (rule-id-condition rule)
215 :slow))
216 (is-true? (progn (normalize-term $$cond) $$cond)))
217 ;; the condition is satisfied
218 (return-from make-rule-pat-with-check
219 (make-rule-pat :pos pos :rule rule :subst subst :cond-ok t :condition $$cond :num (incf .rules-so-far.)))
220 (if (rwl-sch-context-if sch-context)
221 ;; rule condition fail & there exists 'if'
222 (return-from make-rule-pat-with-check
223 (make-rule-pat :pos pos :rule rule :subst subst :cond-ok nil :condition $$cond :num (incf .rules-so-far.)))
224 (return-from make-rule-pat-with-check nil))))
225 nil)))
226
227 (defun rule-pat-equal (pat1 pat2)
228 (and (equal (rule-pat-pos pat1) (rule-pat-pos pat2))
229 (eq (rule-pat-rule pat1) (rule-pat-rule pat2))
230 (substitution-equal (rule-pat-subst pat1) (rule-pat-subst pat2))))
231
232 ;;; *****
233 ;;; STATE utils
234 ;;; *****
235
236 (defun state-is-valid-transition (state)
237 (declare (type rwl-state state))
238 (let ((cond (rwl-state-condition state)))
239 (and (not (rwl-state-loop state))
240 (or (null cond)
241 (is-true? cond)))))
242
243 (defun pr-rwl-state (state &optional (stream *standard-output*) &rest ignore)
244 (declare (ignore ignore)
245 (type rwl-state state)
246 (type stream stream))
247 (let ((*standard-output* stream))
248 (format t "#<rwl-state(~D):" (rwl-state-state state))
249 (term-print (rwl-state-term state))
250 (princ ", ")
251 (dolist (sub (rwl-state-subst state))
252 (print-substitution sub))
253 (when (rwl-state-is-final state)
254 (princ " ,final"))
255 (princ ">")))
256
257 (declaim (special .rwl-search-depth.))
258 (defvar .rwl-search-depth. -1)
259
260 (defun print-rwl-state (state &optional (stream *standard-output*) &rest ignore)
261 (declare (ignore ignore)
262 (type rwl-state state)
263 (type stream stream))
264 (let ((*standard-output* stream))
265 (format t "~%[state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
266 (let ((*print-indent* (+ 4 *print-indent*)))
267 (term-print-with-sort (rwl-state-term state))
268 (when *cexec-trace*
269 (format t "~& matched with the substitution "))
270 (let ((*print-indent* (+ 4 *print-indent*)))
271 (dolist (subst (rwl-state-subst state))
272 (print-next)
273 (print-substitution subst)))
274 (flush-all))))
275
276 (defun print-state-transition (state sub-states &optional (stream *standard-output*))
277 (declare (type rwl-state state)
278 (type list sub-states)
279 (type stream stream))
280 (let ((*standard-output* stream)
281 (arc-num 0))
282 (declare (type fixnum arc-num))
283 (format t "~%[state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
284 (term-print-with-sort (rwl-state-term state))
285 (dolist (sub sub-states)
286 (format t "~& arc ~D --> [state ~D-~D] " arc-num (rwl-state-depth state) (rwl-state-state sub))
287 (let ((*print-indent* (+ 4 *print-indent*)))
288 (print-next)
289 (print-axiom-brief (rule-pat-rule (rwl-state-rule-pat sub))))
290 (incf arc-num))))
291
292 ;;; ******************
293 ;;; RWL-SCH-NODE utils
294 ;;; ******************
295
296 ;;; print the rule & state
297 ;;;
298 (defun show-rwl-state (dag &optional (path? t) (bind-pattern nil))
299 (declare (type rwl-sch-node dag)
300 (type (or null t) path? bind-pattern))
301 (let* ((st (dag-node-datum dag))
302 (term (rwl-state-term st))
303 (rule-pat (rwl-state-rule-pat st))
304 (rl (if rule-pat (rule-pat-rule rule-pat)
305 nil)))
306 (when (and rl path?)
307 (print-next)
308 (princ " ")
309 (let ((*print-indent* (+ 8 *print-indent*)))
310 (print-chaos-object rl) ; (print-axiom-brief rl)
311 ))
312 (format t "~%[state ~D-~D] " (rwl-state-depth st) (rwl-state-state st))
313 (term-print-with-sort term)
314 (dolist (sub (rwl-state-subst st))
315 (format t "~& ")
316 (print-substitution sub)
317 (when bind-pattern
318 (let ((bimage (substitution-image-simplifying sub bind-pattern)))
319 (normalize-term bimage)
320 (format t "~% => ")
321 (term-print-with-sort bimage))))))
322
323 ;;; print the label of a rule which derived a state
324 ;;; that denode contains.
325 ;;;
326 (defun show-rwl-sch-label (dnode)
327 (declare (type rwl-sch-node dnode))
328 (let* ((dt (dag-node-datum dnode))
329 (rl (rule-pat-rule (rwl-state-rule-pat dt)))
330 (label (car (rule-labels rl))))
331 (if label
332 (format t "~&[~a]" label)
333 (format t "~&NONE"))))
326334
327335 ;;; *********************
328336 ;;; SEARCH CONTEXT UTILS
369377 (dag-node-datum sd))
370378 (dag-node-subnodes d))))))))))))
371379
372 (defun find-rwl-sch-state (num &optional (sch-context .rwl-sch-context.))
373 (declare (type fixnum num))
380 (defun find-rwl-state (num &optional (sch-context .rwl-sch-context.))
381 (declare (type fixnum num)
382 (type (or null rwl-sch-context) sch-context))
374383 (unless sch-context
375384 (with-output-chaos-error ('no-root-node)
376385 (format t "no search result exists")))
379388 (catch 'dag-found
380389 (dag-wfs (rwl-sch-context-root sch-context)
381390 #'(lambda (d)
391 (declare (type dag-node d))
382392 (let ((st (dag-node-datum d)))
383393 (when (= (rwl-state-state st) num)
384394 (throw 'dag-found d)))))
385395 nil))
386396 dag))
387397
388 (defun find-rwl-sch-state-globally (num)
398 (defun find-rwl-state-globally (num)
389399 (declare (type fixnum num))
390400 (dolist (context .rwl-context-stack.)
391 (let ((st (find-rwl-sch-state num context)))
392 (when st (return-from find-rwl-sch-state-globally (values context st))))))
401 (declare (type rwl-sch-context context))
402 (let ((st (find-rwl-state num context)))
403 (when st (return-from find-rwl-state-globally (values context st))))))
393404
394405 (defun show-rwl-sch-path (num-tok &optional (label? nil)
395406 (sch-context .rwl-sch-context.)
405416 (with-output-chaos-error ()
406417 (format t "state must be a positive integer value.")))
407418 (multiple-value-bind (sch-context dag)
408 (find-rwl-sch-state-globally num)
419 (find-rwl-state-globally num)
409420 (unless dag
410421 (with-output-chaos-error ('no-state)
411422 (format t "no such state ~D" num)))
415426 (with-output-chaos-warning ()
416427 (format t "the context(module) of search result is different from the current module.")))
417428 (with-in-module (mod)
418 (cond (state-only? (show-rwl-sch-state dag nil (rwl-sch-context-bind sch-context)))
429 (cond (state-only? (show-rwl-state dag nil (rwl-sch-context-bind sch-context)))
419430 (t (let ((parents (get-bdag-parents dag)))
420431 (cond (label?
421432 (dolist (p (cdr parents)) ;root has no transition
422433 (show-rwl-sch-label p))
423434 (show-rwl-sch-label dag))
424435 (t (dolist (p parents)
425 (show-rwl-sch-state p t (rwl-sch-context-bind sch-context)))
426 (show-rwl-sch-state dag t (rwl-sch-context-bind sch-context))))))))))))
436 (show-rwl-state p t (rwl-sch-context-bind sch-context)))
437 (show-rwl-state dag t (rwl-sch-context-bind sch-context))))))))))))
427438
428439
429440 ;;; *************
433444 ;;; finds all transition rules possibly applicable to the given target term
434445 ;;;
435446 (defun find-matching-rules-for-exec (target sch-context &optional start-pos)
447 (declare (type term target)
448 (type rwl-sch-context sch-context)
449 (type (or null fixnum) start-pos))
436450 (let ((module (rwl-sch-context-module sch-context)))
451 (declare (type module module))
437452 (when start-pos
438453 (setq target (get-target-subterm target start-pos)))
439454 (with-in-module (module)
441456 (rules (get-module-axioms *current-module* t))
442457 (rls nil)
443458 (res nil))
459 (declare (type list rules rls res))
444460 (dolist (rule rules)
445461 (when (rule-is-rule rule)
446462 (push rule rls)))
458474 res ))))
459475
460476 (defun find-matching-rules-for-exec* (target rules pos sch-context)
477 (declare (type term target)
478 (type list rules pos)
479 (type rwl-sch-context sch-context))
461480 (when *cexec-debug*
462481 (format t "~%find matching rules. ")
463482 (term-print target)
525544 ;;; ****************
526545
527546 (defun if-binding-should-be-printed (sch-context)
547 (declare (type rwl-sch-context sch-context))
528548 (and (rwl-sch-context-if sch-context)
529549 ;; (not *rwl-search-no-state-report*)
530550 (<= (rwl-sch-context-cur-depth sch-context) (rwl-sch-context-max-depth sch-context))))
537557 (declare (type rwl-sch-node node)
538558 (type rwl-sch-context sch-context))
539559 (flet ((condition-check-ok (subst)
560 (declare (type substitution subst))
540561 (let ((cond (rwl-sch-context-condition sch-context))
541562 ($$term nil)
542563 ($$cond nil)
633654 (not (null (rwl-state-subst state))))))
634655
635656 (defun pr-used-rule (state)
657 (declare (type rwl-state state))
636658 (let ((rule-pat (rwl-state-rule-pat state))
637659 (rule nil))
638660 (unless rule-pat (return-from pr-used-rule nil))
646668 t))
647669
648670 (defun print-subst-if-binding-result (state sub sch-context)
649 (declare (ignore state))
671 (declare (ignore state)
672 (type substitution sub)
673 (type rwl-sch-context sch-context))
650674 (setf (rwl-sch-context-pr-out? sch-context) t)
651675 (format t "~% ") (print-substitution sub)
652676 (when (rwl-sch-context-bind sch-context)
665689 ;;; returns a subterm at position 'pos'
666690 ;;;
667691 (defun get-target-subterm (term pos)
692 (declare (type term term)
693 (type list pos))
668694 (let ((cur term))
695 (declare (type term cur))
669696 (when pos
670697 (dolist (p pos)
671698 (setq cur (term-arg-n cur p))
679706 cur))
680707
681708 ;;; *********
682 ;;; TERM HASH
709 ;;; TERM HASH : used for loop check
683710 ;;; *********
684 (declaim (special .cexec-term-hash.))
711 (deftype term-hash-key () '(unsigned-byte 29))
712 (defconstant term-hash-mask #x1FFFFFFF)
713 (defconstant term-hash-size 9001)
714
715 (declaim (inline term-hash-equal))
716 #-CMU
717 (defun term-hash-equal (x)
718 (declare (optimize (speed 3) (safety 0)))
719 (logand term-hash-mask (sxhash x)))
720
721 #+CMU
722 (defun term-hash-equal (x)
723 (sxhash x))
724
725 (declaim (inline term-hash-eq))
726 (defun term-hash-eq (object)
727 (declare (optimize (speed 3) (safety 0)))
728 (ash (+ (the term-hash-key
729 (logand term-hash-mask
730 (the (unsigned-byte 32) (addr-of object))))
731 3)
732 -3))
733
734 (declaim (inline term-hash-comb))
735 (defun term-hash-comb (x y)
736 (declare (optimize (speed 3) (safety 0)))
737 (the term-hash-key (logand term-hash-mask (logand term-hash-mask (+ x y)))))
738
739 (defun cexec-hash-term (term)
740 (declare (type term term)
741 (optimize (speed 3) (safety 0)))
742 (cond ((term-is-applform? term)
743 (let ((res (sxhash (the symbol (method-id-symbol (term-head term))))))
744 (dolist (subterm (term-subterms term))
745 (setq res (term-hash-comb res (cexec-hash-term subterm))))
746 res))
747 ((term-is-builtin-constant? term)
748 (term-hash-comb (sxhash (the symbol (sort-id (term-sort term))))
749 (term-hash-equal (term-builtin-value term))))
750 ((term-is-variable? term) (term-hash-eq term))))
751
752 (defun dump-cexec-term-hash (term-hash &optional (size term-hash-size))
753 (dotimes (x size)
754 (let ((ent (svref term-hash x)))
755 (when ent
756 (format t "~%[~3d]: ~d entrie(s)" x (length ent))
757 (dotimes (y (length ent))
758 (let ((e (nth y ent)))
759 (format t "~%(~d)" y)
760 (let ((*print-indent* (+ 2 *print-indent*)))
761 (term-print (car e))
762 (print-next)
763 (princ "==>")
764 (print-next)
765 (term-print (cdr e)))))))))
766
685767 (defvar .cexec-term-hash. nil)
686768
769 (declaim (inline init-rwl-term-hash))
770 (defun init-rwl-term-hash (depth)
771 (declare (type fixnum depth)
772 (optimize (speed 3) (safety 0)))
773 (unless .cexec-term-hash.
774 (setq .cexec-term-hash. (alloc-svec term-hash-size)))
775 (when (zerop depth)
776 (dotimes (x term-hash-size)
777 (setf (svref .cexec-term-hash. x) nil))))
778
687779 (declaim (inline get-sch-hashed-term))
688
689 (defun get-sch-hashed-term (term-id term-hash)
690 (if term-id
691 (gethash term-id term-hash)
692 nil))
780 (defun get-sch-hashed-term (term term-hash)
781 (declare (type term term)
782 (type simple-vector term-hash)
783 (optimize (speed 3) (safety 0)))
784 (let ((val (cexec-hash-term term)))
785 (let* ((ent (svref term-hash
786 (mod val term-hash-size)))
787 (val (cdr (assoc term ent :test #'term-equational-equal))))
788 (when val (incf (the fixnum *term-memo-hash-hit*)))
789 val)))
693790
694791 (declaim (inline set-sch-hashed-term))
695
696 (defun set-sch-hashed-term (term-id term-hash value)
697 (when term-id
698 (setf (gethash term-id term-hash) value)))
792 (defun set-sch-hashed-term (term term-hash value)
793 (declare (type term term)
794 (type simple-vector term-hash)
795 (type fixnum value)
796 (optimize (speed 3) (safety 0)))
797 (let ((val (cexec-hash-term term)))
798 (let ((ind (mod val term-hash-size)))
799 (let ((ent (svref term-hash ind)))
800 (let ((pr (assoc term ent :test #'term-equational-equal)))
801 (if pr (rplacd pr value)
802 (setf (svref term-hash ind) (cons (cons term value) ent))))))))
803
804 (defmacro cexec-get-hashed-term (term)
805 `(get-sch-hashed-term ,term .cexec-term-hash.))
806
807 (defmacro cexec-set-hashed-term (term state-num)
808 `(set-sch-hashed-term ,term .cexec-term-hash. ,state-num))
699809
700810 (defun cexec-sch-check-predicate (term t1 pred-pat)
811 (declare (type term term t1)
812 (type list pred-pat)
813 (optimize (speed 3) (safety 0)))
701814 (let ((pred (car pred-pat))
702815 (vars (cdr pred-pat))
703816 (subst nil)
736849 (format t "~%** state predicate returned `true'."))
737850 res))
738851
739 (defun cexec-loop-check (term-id term sch-context)
740 (or (get-sch-hashed-term term-id .cexec-term-hash.)
852 (declaim (inline cexec-loop-check))
853 (defun cexec-loop-check (term sch-context)
854 (declare (type term term)
855 (type rwl-sch-context sch-context)
856 (optimize (safety 0) (speed 3)))
857 (or (cexec-get-hashed-term term)
741858 (let ((pred-pat (rwl-sch-context-state-predicate sch-context)))
742859 (if pred-pat
743 (maphash #'(lambda (key e)
744 (declare (ignore key))
745 (let ((t1 (car e)))
746 (when (cexec-sch-check-predicate term t1 pred-pat)
747 (return-from cexec-loop-check (cdr e)))))
748 .cexec-term-hash.)
860 (dotimes (x term-hash-size nil)
861 (let ((ent (svref .cexec-term-hash. x)))
862 (dolist (e ent)
863 (let ((t1 (car e)))
864 (when (cexec-sch-check-predicate term t1 pred-pat)
865 (return-from cexec-loop-check (cdr e)))))))
749866 nil))))
750867
751868 ;;;
752869 ;;; MAKE-RWL-STATE-WITH-HASH
753870 ;;;
754871 (defun make-rwl-state-with-hash (target rule-pat sch-context)
755 (let* ((term-id (term-id target))
756 (ostate-num (cexec-loop-check term-id target sch-context))
872 (declare (type term target)
873 (type rule-pat rule-pat)
874 (type rwl-sch-context sch-context)
875 (optimize (speed 3) (safety 0)))
876 (let* ((ostate-num (cexec-loop-check target sch-context))
757877 (condition (rule-pat-condition rule-pat))
758878 (new-state nil))
759879 (cond (ostate-num
764884 :term target
765885 :rule-pat rule-pat
766886 :subst nil
767 :condition condition
768 :depth .rwl-search-depth.))
887 :condition condition))
769888 (when (or *cexec-trace* *chaos-verbose*)
770889 (format t "~%* loop"))
771890 (setf (rwl-state-loop new-state) t))
774893 :term target
775894 :rule-pat rule-pat
776895 :subst nil
777 :condition condition
778 :depth .rwl-search-depth.))
896 :condition condition))
779897 ;; register the term
780898 (when *cexec-debug*
781899 (format t "~%** hashing state ~D" state-num))
782 (set-sch-hashed-term term-id .cexec-term-hash. state-num))))
900 (cexec-set-hashed-term target state-num))))
783901 ;;
784902 new-state))
903
785904
786905 ;;; *******************
787906 ;;; ONE STEP TRANSITION
790909 ;;; RWL-STATE-SET-TRANSITION-RULES
791910 ;;;
792911 (defun rwl-state-set-transition-rules (state sch-context)
912 (declare (type rwl-state state)
913 (type rwl-sch-context sch-context))
793914 (let ((rule-pats (find-matching-rules-for-exec (rwl-state-term state) sch-context)))
794915 (setf (rwl-state-trans-rules state) rule-pats)
795916 (unless rule-pats
799920 ;;; APPLY-RULE-CEXEC: rule target -> Bool
800921 ;;;
801922 (defun apply-rule-cexec (rule term subst)
923 (declare (type rewrite-rule rule)
924 (type term term)
925 (type substitution subst))
802926 (catch 'rule-failure
803927 (progn
804928 (term-replace-dd-simple
818942 ;;; - returns the list of substates which derived from the given state.
819943 ;;; - NOTE: term of the given state is NOT modified.
820944 ;;;
821 (defun cexec-term-1 (dag sch-context) ; node-num ...
945 (defun cexec-term-1 (dag sch-context)
822946 (declare (type rwl-sch-node dag)
823947 (type rwl-sch-context sch-context)
824 ; (type fixnum node-num)
825 )
826 ;;
948 (optimize (speed 3) (safety 0)))
827949 (let* ((state (dag-node-datum dag))
828950 (term (rwl-state-term state)))
829951 (flet ((no-more-transition ()
9741096 ;;; each `last-siblings' & check if derived terms match to `pattern'.
9751097 ;;;
9761098 (defun rwl-step-forward-1 (sch-context)
977 (declare (type rwl-sch-context sch-context))
1099 (declare (type rwl-sch-context sch-context)
1100 (optimize (speed 3) (safety 0)))
9781101 ;; check # of transitions
9791102 (when (>= (rwl-sch-context-trans-so-far sch-context)
9801103 *cexec-limit*)
10751198 ;;; *********
10761199 ;;; TOP LEVEL functions
10771200 ;;; *********
1201 (declaim (inline make-anything-is-ok-term))
10781202 (defun make-anything-is-ok-term ()
10791203 (make-variable-term *cosmos* (gensym "Univ")))
10801204
10841208 module
10851209 bind
10861210 if)
1211 (declare (type term t1 t2)
1212 (type fixnum max-result max-depth)
1213 (type (or null t) zero?))
10871214 (with-in-module (module)
10881215 (unless t2
10891216 (setq t2 (make-anything-is-ok-term)))
11481275 :max-depth max-depth
11491276 :state-predicate nil
11501277 :bind bind
1151 :if if
1152 :term-hash (make-hash-table :test #'equal
1153 :rehash-size 1.5
1154 :rehash-threshold 0.7)))
1278 :if if))
11551279 (root nil)
11561280 (res nil)
11571281 (no-more nil)
11891313 ;; state equality predicate
11901314 (setf (rwl-sch-context-state-predicate sch-context) (make-state-pred-pat))
11911315 (let ((.rwl-sch-context. sch-context)
1192 (.cexec-term-hash. (rwl-sch-context-term-hash sch-context))
11931316 (.rwl-search-depth. (1+ .rwl-search-depth.))
11941317 (.ignore-term-id-limit. t))
11951318 (declare (special .rwl-sch-context. .cexec.term-hash. .ignore-term-id-limit.))
11961319 (push sch-context .rwl-context-stack.)
1320 (init-rwl-term-hash .rwl-search-depth.)
11971321 ;; the first state is 0
1198 (set-sch-hashed-term (term-id t1) .cexec-term-hash. 0)
1322 (set-sch-hashed-term t1 .cexec-term-hash. 0)
11991323 ;;
12001324 ;; do the search
12011325 ;;
13161440 (bind nil)
13171441 ;; the followings are experimental
13181442 (if nil))
1443 (declare (type term term pattern)
1444 (type fixnum max-result max-depth)
1445 (type (or null t) zero? final?))
13191446 (let ((module (get-context-module))
13201447 max-r
13211448 max-d)
1449 (declare (type module module))
13221450 (if (integerp max-result)
13231451 (setq max-r max-result)
13241452 (if (term-is-builtin-constant? max-result)