| 74 | 74 |
|
| 75 | 75 |
;;; SORT DECLARATION
|
| 76 | 76 |
(defun print-sort-decl (ast &optional (stream *standard-output*))
|
|
77 |
(declare (type stream stream))
|
| 77 | 78 |
(format stream "(%sort-decl ~s ~s)" (%sort-decl-name ast)
|
| 78 | 79 |
(%sort-decl-hidden ast)))
|
| 79 | 80 |
|
| 80 | 81 |
;;; SUBSORT DECLARATION
|
| 81 | 82 |
(defun print-subsort-decl (ast &optional (stream *standard-output*))
|
|
83 |
(declare (type %subsort-decl ast)
|
|
84 |
(type stream stream))
|
| 82 | 85 |
(fresh-line)
|
| 83 | 86 |
(let ((s-seq (remove nil (mapcar #'(lambda (x)
|
| 84 | 87 |
(if (atom x)
|
|
| 89 | 92 |
|
| 90 | 93 |
;;; BSORT DECLARATION
|
| 91 | 94 |
(defun print-bsort-decl (ast &optional (stream *standard-output*))
|
|
95 |
(declare (type %bsort-decl)
|
|
96 |
(type stream stream))
|
| 92 | 97 |
(let ((tp (%bsort-decl-token-predicate ast))
|
| 93 | 98 |
(tc (%bsort-decl-term-creator ast))
|
| 94 | 99 |
(tpr (%bsort-decl-term-printer ast))
|
|
| 99 | 104 |
|
| 100 | 105 |
;;; PRINCIPAL-SORT-DECLARATION
|
| 101 | 106 |
(defun print-psort-decl (ast &optional (stream *standard-output*))
|
|
107 |
(declare (type %psort-decl ast)
|
|
108 |
(type stream stream))
|
| 102 | 109 |
(format stream "~&(%psort-decl ~s)" (%psort-decl-sort ast)))
|
| 103 | 110 |
|
| 104 | 111 |
;;; Operator Reference
|
| 105 | 112 |
;;;-----------------------------------------------------------------------------
|
| 106 | 113 |
(defun print-opref (ast &optional (stream *standard-output*))
|
|
114 |
(declare (type %opref ast)
|
|
115 |
(type stream stream))
|
| 107 | 116 |
(format stream "~s ~s ~s" (%opref-name ast)
|
| 108 | 117 |
(%opref-module ast)
|
| 109 | 118 |
(%opref-num-args ast)))
|
| 110 | 119 |
|
| 111 | 120 |
(defun print-opref-simple (ast &optional (stream *standard-output*))
|
|
121 |
(declare (type %opref ast)
|
|
122 |
(type stream stream))
|
| 112 | 123 |
(let ((*standard-output* stream)
|
| 113 | 124 |
(name (%opref-name ast))
|
| 114 | 125 |
(module (%opref-module ast)))
|
|
| 122 | 133 |
;;; Operator Declaration *TODO*
|
| 123 | 134 |
;;;-----------------------------------------------------------------------------
|
| 124 | 135 |
(defun print-op-decl-ast (ast &optional (stream *standard-output*))
|
|
136 |
(declare (type %op-decl ast)
|
|
137 |
(type stream stream))
|
| 125 | 138 |
(let ((*standard-output* stream)
|
| 126 | 139 |
(name (%op-decl-name ast))
|
| 127 | 140 |
(arity (%op-decl-arity ast))
|
|
| 148 | 161 |
;;; Operator Attribute declarations
|
| 149 | 162 |
;;;-----------------------------------------------------------------------------
|
| 150 | 163 |
(defun print-opattrs-ast (ast &optional (stream *standard-output*))
|
|
164 |
(declare (type %opattrs ast)
|
|
165 |
(type stream stream))
|
| 151 | 166 |
(let ((theory (%opattrs-theory ast))
|
| 152 | 167 |
(assoc (%opattrs-assoc ast))
|
| 153 | 168 |
(prec (%opattrs-prec ast))
|
|
| 169 | 184 |
(when constr
|
| 170 | 185 |
(format stream "~& - constr is specified"))
|
| 171 | 186 |
(when coherent
|
| 172 | |
(format stream "~& - coherent is specified"))
|
| 173 | |
))
|
|
187 |
(format stream "~& - coherent is specified"))))
|
| 174 | 188 |
|
| 175 | 189 |
;;; Variable Declaration
|
| 176 | 190 |
;;;-----------------------------------------------------------------------------
|
| 177 | 191 |
(defun print-var-decl (ast &optional (stream *standard-output*))
|
|
192 |
(declare (type %var-decl ast)
|
|
193 |
(type stream stream))
|
| 178 | 194 |
(let* ((*standard-output* stream)
|
| 179 | 195 |
(names (%var-decl-names ast))
|
| 180 | 196 |
(sort-ref (%var-decl-sort ast))
|
| 181 | 197 |
(sort-name (%sort-ref-name sort-ref))
|
| 182 | 198 |
(sort-qual (%sort-ref-qualifier sort-ref)))
|
|
199 |
(declare (type list names)
|
|
200 |
(type %sort-ref sort-ref)
|
|
201 |
(type simple-string sort-name))
|
| 183 | 202 |
(format t "~%Variable declaration : names =~{ ~a~}" names)
|
| 184 | 203 |
(format t "~& Sort = ~a" sort-name)
|
| 185 | 204 |
(when sort-qual
|
|
| 187 | 206 |
(print-modexp sort-qual stream t t))))
|
| 188 | 207 |
|
| 189 | 208 |
(defun print-pvar-decl (ast &optional (stream *standard-output*))
|
|
209 |
(declare (type %pvar-decl ast)
|
|
210 |
(type stream stream))
|
| 190 | 211 |
(let* ((*standard-output* stream)
|
| 191 | 212 |
(names (%pvar-decl-names ast))
|
| 192 | 213 |
(sort-ref (%pvar-decl-sort ast))
|
|
| 201 | 222 |
;;; LET DECLARATOIN
|
| 202 | 223 |
;;;-----------------------------------------------------------------------------
|
| 203 | 224 |
(defun print-let-decl (ast &optional (stream *standard-output*))
|
|
225 |
(declare (type %let ast)
|
|
226 |
(type stream stream))
|
| 204 | 227 |
(let ((sym (%let-sym ast))
|
| 205 | 228 |
(value (%let-value ast)))
|
| 206 | 229 |
(format stream "~%let declaration: ")
|
|
| 210 | 233 |
;;; MACRO DECLARATION
|
| 211 | 234 |
;;;-----------------------------------------------------------------------------
|
| 212 | 235 |
(defun print-macro-decl (ast &optional (stream *standard-output*))
|
|
236 |
(declare (type %macro ast)
|
|
237 |
(type stream stream))
|
| 213 | 238 |
(let ((lhs (%macro-lhs ast))
|
| 214 | 239 |
(rhs (%macro-rhs ast)))
|
| 215 | 240 |
(format stream "~%macro declaration:")
|
|
| 219 | 244 |
;;; AXIOM DECLARATION
|
| 220 | 245 |
;;;-----------------------------------------------------------------------------
|
| 221 | 246 |
(defun print-axiom-decl-form (ast &optional (stream *standard-output*))
|
|
247 |
(declare (type %axiom-decl ast)
|
|
248 |
(type stream stream))
|
| 222 | 249 |
(let ((type (%axiom-decl-type ast))
|
| 223 | 250 |
(labels (%axiom-decl-labels ast))
|
| 224 | 251 |
(lhs (%axiom-decl-lhs ast))
|
|
| 235 | 262 |
;;; IMPORT-DECLARATION
|
| 236 | 263 |
;;;-----------------------------------------------------------------------------
|
| 237 | 264 |
(defun print-import-decl (ast &optional (stream *standard-output*))
|
|
265 |
(declare (type %import ast)
|
|
266 |
(type stream stream))
|
| 238 | 267 |
(let ((mode (%import-mode ast))
|
| 239 | 268 |
(mod (%import-module ast))
|
| 240 | 269 |
(as (%import-alias ast)))
|
|
| 249 | 278 |
;;; MODULE NAME
|
| 250 | 279 |
;;;-----------------------------------------------------------------------------
|
| 251 | 280 |
(defun get-module-print-name (module)
|
| 252 | |
(unless (module-p module) (break "internal error, get-module-print-name"))
|
|
281 |
(declare (type module module))
|
| 253 | 282 |
(let ((name (module-name module)))
|
| 254 | 283 |
(if (modexp-is-simple-name name)
|
| 255 | 284 |
name
|
| 256 | |
(or (module-decl-form module) name))))
|
| 257 | |
|
| 258 | |
(defun make-module-print-name (mod &optional (abbrev t))
|
| 259 | |
(with-output-to-string (name-string)
|
| 260 | |
(print-mod-name mod name-string abbrev)
|
| 261 | |
name-string))
|
|
285 |
(or (module-decl-form module) name))))
|
|
286 |
|
|
287 |
(defun print-mod-name-internal (val abbrev &optional (no-param nil))
|
|
288 |
(declare (type (or null (not null)) abbrev no-param))
|
|
289 |
(if (stringp val)
|
|
290 |
(princ val)
|
|
291 |
(if (and (consp val) (not (chaos-ast? val)))
|
|
292 |
(if (modexp-is-parameter-theory val)
|
|
293 |
;; parameter theory
|
|
294 |
(if abbrev
|
|
295 |
(progn
|
|
296 |
(format t "~a" (car val))
|
|
297 |
(princ ".")
|
|
298 |
(print-mod-name (car (last val))
|
|
299 |
*standard-output*
|
|
300 |
abbrev
|
|
301 |
no-param))
|
|
302 |
(let ((cntxt (fourth val)))
|
|
303 |
(if (and cntxt
|
|
304 |
(not (eq (get-context-module) cntxt)))
|
|
305 |
(progn (format t "~a." (car val))
|
|
306 |
(print-mod-name cntxt *standard-output* t t)
|
|
307 |
(princ " :: "))
|
|
308 |
(format t "~a :: " (car val)))
|
|
309 |
(print-mod-name (caddr val) *standard-output* nil t)))
|
|
310 |
(print-chaos-object val))
|
|
311 |
(print-modexp val *standard-output* abbrev no-param))))
|
| 262 | 312 |
|
| 263 | 313 |
(defun print-mod-name (arg &optional
|
| 264 | 314 |
(stream *standard-output*)
|
| 265 | 315 |
(abbrev nil)
|
| 266 | 316 |
(no-param nil))
|
| 267 | |
(declare (values t))
|
| 268 | 317 |
(let ((*standard-output* stream))
|
| 269 | 318 |
(if (module-p arg)
|
| 270 | 319 |
(let ((modname (get-module-print-name arg)))
|
|
| 276 | 325 |
(let ((params (get-module-parameters arg)))
|
| 277 | 326 |
(when (and params (not no-param))
|
| 278 | 327 |
(let ((flg nil))
|
| 279 | |
;; (princ "[")
|
| 280 | 328 |
(princ "(")
|
| 281 | 329 |
(dolist (param params)
|
| 282 | 330 |
(let ((theory (get-parameter-theory
|
|
| 287 | 335 |
(eq arg (parameter-context param)))
|
| 288 | 336 |
(princ (parameter-arg-name param))
|
| 289 | 337 |
(progn
|
| 290 | |
;; (format t "~a@" (parameter-arg-name param))
|
| 291 | 338 |
(format t "~a." (parameter-arg-name param))
|
| 292 | 339 |
(print-mod-name (parameter-context param)
|
| 293 | 340 |
stream
|
| 294 | 341 |
abbrev
|
| 295 | 342 |
t)))
|
| 296 | |
;; patch-begin
|
| 297 | |
;; (princ "::")
|
| 298 | |
;; (print-mod-name theory stream abbrev t)
|
| 299 | |
;; patch-end
|
| 300 | 343 |
(setq flg t)))
|
| 301 | |
;; (princ "]")
|
| 302 | |
(princ ")")
|
| 303 | |
))))
|
| 304 | |
(print-chaos-object arg)
|
| 305 | |
)))
|
| 306 | |
|
| 307 | |
(defun print-mod-name-internal (val abbrev
|
| 308 | |
&optional
|
| 309 | |
(no-param nil))
|
| 310 | |
(declare (values t))
|
| 311 | |
(if (stringp val)
|
| 312 | |
(princ val)
|
| 313 | |
(if (and (consp val) (not (chaos-ast? val)))
|
| 314 | |
(if (modexp-is-parameter-theory val)
|
| 315 | |
;; (equal "::" (cadr val))
|
| 316 | |
;; parameter theory
|
| 317 | |
(if abbrev
|
| 318 | |
(progn
|
| 319 | |
(format t "~a" (car val))
|
| 320 | |
(princ ".")
|
| 321 | |
(print-mod-name (car (last val))
|
| 322 | |
*standard-output*
|
| 323 | |
abbrev
|
| 324 | |
no-param))
|
| 325 | |
;;
|
| 326 | |
(let ((cntxt (fourth val)))
|
| 327 | |
(if (and cntxt
|
| 328 | |
(not (eq *current-module* cntxt)))
|
| 329 | |
(progn (format t "~a." (car val))
|
| 330 | |
(print-mod-name cntxt *standard-output* t t)
|
| 331 | |
(princ " :: "))
|
| 332 | |
(format t "~a :: " (car val)))
|
| 333 | |
(print-mod-name (caddr val) *standard-output* nil t)))
|
| 334 | |
(print-chaos-object val))
|
| 335 | |
(print-modexp val *standard-output* abbrev no-param))))
|
|
344 |
(princ ")")))))
|
|
345 |
(print-chaos-object arg))))
|
|
346 |
|
|
347 |
(defun make-module-print-name (mod &optional (abbrev t))
|
|
348 |
(declare (type module mod)
|
|
349 |
(type (or null (not null)) abbrev))
|
|
350 |
(with-output-to-string (name-string)
|
|
351 |
(print-mod-name mod name-string abbrev)
|
|
352 |
name-string))
|
| 336 | 353 |
|
| 337 | 354 |
(defun print-simple-mod-name (module &optional (stream *standard-output*))
|
|
355 |
(declare (type stream stream))
|
| 338 | 356 |
(if (and *open-module*
|
| 339 | 357 |
(equal "%" (get-module-print-name module)))
|
| 340 | 358 |
(progn
|
| 341 | 359 |
(princ "%" stream)
|
| 342 | 360 |
(print-mod-name *open-module* stream t nil))
|
| 343 | 361 |
(print-mod-name module stream t nil)))
|
| 344 | |
|
| 345 | |
(defun make-module-print-name2 (mod)
|
| 346 | |
(with-output-to-string (name-string)
|
| 347 | |
(print-mod-name2 mod name-string t)
|
| 348 | |
name-string))
|
| 349 | 362 |
|
| 350 | 363 |
(defun print-mod-name2 (arg &optional
|
| 351 | 364 |
(stream *standard-output*)
|
|
| 357 | 370 |
(let ((info (getf (module-infos arg) 'rename-mod)))
|
| 358 | 371 |
(print-mod-name2 (car info) stream no-param)
|
| 359 | 372 |
(princ "*DUMMY"))
|
| 360 | |
(print-mod-name-internal2 modname no-param))
|
|
373 |
(print-mod-name-internal2 modname no-param))
|
| 361 | 374 |
(let ((params (get-module-parameters arg)))
|
| 362 | 375 |
(when (and params (not no-param))
|
| 363 | 376 |
(let ((flg nil))
|
|
| 368 | 381 |
(if flg (princ ", "))
|
| 369 | 382 |
(if (eq arg (parameter-context param))
|
| 370 | 383 |
(princ (parameter-arg-name param))
|
| 371 | |
(progn
|
| 372 | |
(format t "~a." (parameter-arg-name param))
|
| 373 | |
(print-mod-name2 (parameter-context param)
|
| 374 | |
stream
|
| 375 | |
t)))
|
|
384 |
(progn
|
|
385 |
(format t "~a." (parameter-arg-name param))
|
|
386 |
(print-mod-name2 (parameter-context param)
|
|
387 |
stream
|
|
388 |
t)))
|
| 376 | 389 |
(setq flg t)))
|
| 377 | |
(princ ")")
|
| 378 | |
))))
|
| 379 | |
;; unknown object ...
|
| 380 | |
(print-chaos-object arg)
|
| 381 | |
)))
|
|
390 |
(princ ")")))))
|
|
391 |
;; unknown object ...
|
|
392 |
(print-chaos-object arg))))
|
| 382 | 393 |
|
| 383 | 394 |
(defun print-mod-name-internal2 (val &optional (no-param nil))
|
| 384 | 395 |
(if (stringp val)
|
|
| 392 | 403 |
*standard-output*
|
| 393 | 404 |
no-param))
|
| 394 | 405 |
(print-chaos-object val))
|
| 395 | |
(print-modexp val *standard-output* nil no-param))))
|
|
406 |
(print-modexp val *standard-output* nil no-param))))
|
|
407 |
|
|
408 |
(defun make-module-print-name2 (mod)
|
|
409 |
(with-output-to-string (name-string)
|
|
410 |
(print-mod-name2 mod name-string t)
|
|
411 |
name-string))
|
| 396 | 412 |
|
| 397 | 413 |
(defun get-parameter-theory (mod)
|
| 398 | 414 |
(cond ((module-p mod)
|
|
| 430 | 446 |
(defun print-parameter-theory-name (mod &optional (stream *standard-output*)
|
| 431 | 447 |
(abbrev t)
|
| 432 | 448 |
(no-param t))
|
|
449 |
(declare (type module mod)
|
|
450 |
(type stream stream)
|
|
451 |
(type (or null (not null)) abbrev no-param))
|
| 433 | 452 |
(let ((theory (get-parameter-theory mod)))
|
| 434 | 453 |
(cond ((module-p theory)
|
| 435 | 454 |
(print-mod-name theory stream abbrev no-param))
|
|
| 442 | 461 |
;;; they may include internal objects (not AST).
|
| 443 | 462 |
;;;
|
| 444 | 463 |
(defun print-modexp-simple (me &optional (stream *standard-output*))
|
|
464 |
(declare (type modexp me)
|
|
465 |
(type stream stream))
|
| 445 | 466 |
(print-modexp me stream t t))
|
| 446 | 467 |
|
| 447 | 468 |
;;; top level modexp printer ---------------------------------------------------
|
| 448 | 469 |
|
| 449 | 470 |
(declaim (inline get-context-name))
|
| 450 | 471 |
(defun get-context-name (obj)
|
|
472 |
(declare (type object obj))
|
| 451 | 473 |
(let ((context-mod (get-object-context obj)))
|
| 452 | 474 |
(if context-mod
|
| 453 | 475 |
(get-module-print-name context-mod)
|
| 454 | 476 |
nil)))
|
| 455 | 477 |
|
| 456 | 478 |
(defun get-context-name-extended (obj &optional (context (get-context-module)))
|
|
479 |
(declare (type object obj)
|
|
480 |
(type module context))
|
| 457 | 481 |
(let ((cmod (object-context-mod obj)))
|
| 458 | 482 |
(declare (type (or null module) cmod))
|
| 459 | 483 |
(unless cmod (return-from get-context-name-extended nil))
|
|
| 476 | 500 |
(stream *standard-output*)
|
| 477 | 501 |
(simple t)
|
| 478 | 502 |
(no-param nil))
|
|
503 |
(declare (type modexp me)
|
|
504 |
(type stream stream)
|
|
505 |
(type (or null (not null)) simple no-param))
|
| 479 | 506 |
(let ((.file-col. .file-col.)
|
| 480 | 507 |
(*standard-output* stream))
|
| 481 | 508 |
(if me
|
| 482 | 509 |
(cond
|
| 483 | |
;;
|
| 484 | 510 |
;; The modexp internal..
|
| 485 | 511 |
((int-plus-p me) (pr-int-plus me stream simple no-param))
|
| 486 | 512 |
((int-rename-p me) (pr-int-rename me stream simple no-param))
|
|
| 519 | 545 |
((modexp-is-parameter-theory me)
|
| 520 | 546 |
(let ((cntxt (fourth me)))
|
| 521 | 547 |
(princ (car me))
|
| 522 | |
(when (and cntxt (not (eq *current-module* cntxt)))
|
|
548 |
(when (and cntxt (not (eq (get-context-module) cntxt)))
|
| 523 | 549 |
(princ ".")
|
| 524 | 550 |
(print-mod-name cntxt stream t t)
|
| 525 | 551 |
(print-check .file-col. 0 stream))))
|
|
| 546 | 572 |
|
| 547 | 573 |
;;; *** PLUS ****
|
| 548 | 574 |
|
| 549 | |
(defun print-plus-modexp (me &optional stream simple no-param)
|
|
575 |
(defun print-plus-modexp (me &optional (stream *standard-output*) simple no-param)
|
|
576 |
(declare (type %+ me)
|
|
577 |
(type stream stream)
|
|
578 |
(type (or null (not null)) simple no-param))
|
| 550 | 579 |
(let ((flg nil))
|
| 551 | 580 |
(do* ((args (reverse (%plus-args me)) (cddr args))
|
| 552 | 581 |
(l (car args) (car args))
|
|
| 566 | 595 |
(print-modexp r stream simple no-param)
|
| 567 | 596 |
(princ ")" stream)
|
| 568 | 597 |
(decf .file-col.))
|
| 569 | |
(print-modexp r stream simple no-param))))))
|
|
598 |
(print-modexp r stream simple no-param))))))
|
| 570 | 599 |
|
| 571 | 600 |
;;; *** RENAME ***
|
| 572 | 601 |
|
| 573 | |
(defun print-rename-modexp (me &optional stream simple no-param)
|
|
602 |
(defun print-rename-modexp (me &optional (stream *standard-output*) simple no-param)
|
|
603 |
(declare (type modexp me)
|
|
604 |
(type stream stream)
|
|
605 |
(type (or null (not null)) simple no-param))
|
| 574 | 606 |
(print-modexp (%rename-module me) stream simple no-param) (princ " * {")
|
| 575 | 607 |
(print-check .file-col. 0 stream)
|
| 576 | 608 |
(if simple
|
| 577 | 609 |
(princ " ... " stream)
|
| 578 | |
(print-rename-map (%rename-map me) stream)
|
| 579 | |
)
|
|
610 |
(print-rename-map (%rename-map me) stream))
|
| 580 | 611 |
(princ "}" stream))
|
| 581 | 612 |
|
| 582 | 613 |
;;; *** INSTANTIATION ***
|
| 583 | 614 |
|
| 584 | |
(defun print-instantiation-modexp (me &optional stream simple no-param)
|
|
615 |
(defun print-instantiation-modexp (me &optional (stream *standard-output*)
|
|
616 |
simple
|
|
617 |
no-param)
|
|
618 |
(declare (type %! me)
|
|
619 |
(type stream stream)
|
|
620 |
(type (or null (not null)) simple no-param))
|
| 585 | 621 |
(if (or (stringp (%instantiation-module me))
|
| 586 | 622 |
(and (module-p (%instantiation-module me))
|
| 587 | 623 |
(stringp (module-name (%instantiation-module me)))))
|
| 588 | 624 |
(progn
|
| 589 | 625 |
(print-modexp (%instantiation-module me) stream simple no-param))
|
| 590 | 626 |
(progn
|
| 591 | |
;; (princ "(" stream)
|
| 592 | 627 |
(print-modexp (%instantiation-module me) stream simple no-param)))
|
| 593 | 628 |
(princ "(" stream)
|
| 594 | 629 |
(incf .file-col.)
|
| 595 | 630 |
(let ((flg nil)
|
| 596 | 631 |
(pos-arg nil))
|
|
632 |
(declare (type (or null (not null)) flg pos-arg))
|
| 597 | 633 |
(dolist (arg (%instantiation-args me))
|
| 598 | 634 |
(let ((arg-name (%!arg-name arg))
|
| 599 | 635 |
(view (%!arg-view arg)))
|
|
| 601 | 637 |
(progn (princ ", " stream)
|
| 602 | 638 |
(print-check .file-col. 0 stream))
|
| 603 | 639 |
(setq flg t))
|
| 604 | |
;;
|
| 605 | 640 |
(cond ((stringp arg-name) (princ arg-name stream))
|
| 606 | 641 |
((and (consp arg-name) (cdr arg-name))
|
| 607 | 642 |
;; (format t "~a@" (car arg-name))
|
|
| 619 | 654 |
(unless pos-arg
|
| 620 | 655 |
(princ " <= " stream))
|
| 621 | 656 |
(print-view-modexp-abbrev view stream simple))))
|
| 622 | |
;; (princ "]" stream)
|
| 623 | 657 |
(princ ")" stream)
|
| 624 | 658 |
(decf .file-col.))
|
| 625 | 659 |
|
| 626 | 660 |
;;; *** Sort renaming ***
|
| 627 | 661 |
|
| 628 | 662 |
(defun print-ren-sort (ast &optional (stream *standard-output*) pretty)
|
|
663 |
(declare (type %ren-sort ast)
|
|
664 |
(type stream stream)
|
|
665 |
(type (or null (not null)) pretty))
|
| 629 | 666 |
(let ((*standard-output* stream)
|
| 630 | 667 |
(p-flg nil))
|
|
668 |
(declare (type (or null (not null)) p-flg))
|
| 631 | 669 |
(dolist (elt (%ren-sort-maps ast))
|
| 632 | 670 |
(if p-flg
|
| 633 | 671 |
(progn (princ ",")
|
|
| 643 | 681 |
;;; *** Operator renaming ***
|
| 644 | 682 |
|
| 645 | 683 |
(defun print-ren-op (ast &optional (stream *standard-output*) pretty)
|
|
684 |
(declare (type %ren-op ast)
|
|
685 |
(type stream stream)
|
|
686 |
(type (or null (not null)) pretty))
|
| 646 | 687 |
(let ((*standard-output* stream)
|
| 647 | 688 |
(p-flg nil))
|
| 648 | 689 |
(dolist (elt (%ren-op-maps ast))
|
|
| 651 | 692 |
(princ "op ")
|
| 652 | 693 |
(if (%is-opref (car elt))
|
| 653 | 694 |
(print-opref-simple (car elt))
|
| 654 | |
(print-simple-princ-open (car elt)))
|
|
695 |
(print-simple-princ-open (car elt)))
|
| 655 | 696 |
(print-check .file-col. 0 stream)
|
| 656 | 697 |
(princ " -> ")
|
| 657 | 698 |
(if (%is-opref (cadr elt))
|
| 658 | 699 |
(print-opref-simple (cadr elt))
|
| 659 | |
(print-simple-princ-open (cadr elt))))))
|
|
700 |
(print-simple-princ-open (cadr elt))))))
|
| 660 | 701 |
|
| 661 | 702 |
;;; Parameter renaming
|
| 662 | 703 |
|
| 663 | 704 |
(defun print-ren-param (ast &optional (stream *standard-output*))
|
|
705 |
(declare (type %ren-param ast)
|
|
706 |
(type stream stream))
|
| 664 | 707 |
(let ((*standard-output* stream)
|
| 665 | 708 |
source
|
| 666 | 709 |
target)
|
|
| 674 | 717 |
;;; vars in mapping
|
| 675 | 718 |
|
| 676 | 719 |
(defun print-vars-ast (ast &optional (stream *standard-output*) pretty)
|
|
720 |
(declare (type %vars ast)
|
|
721 |
(type stream stream)
|
|
722 |
(type (or null (not null)) pretty))
|
| 677 | 723 |
(let ((p-flg nil))
|
|
724 |
(declare (type (or null (not null)) p-flg))
|
| 678 | 725 |
(dolist (elt (%vars-elements ast))
|
| 679 | 726 |
(let ((var-names (car elt))
|
| 680 | 727 |
(sort (cadr elt)))
|
|
| 689 | 736 |
;;; *** RENAME MAP ***
|
| 690 | 737 |
|
| 691 | 738 |
(defun print-rename-map (rn &optional (stream *standard-output*) simple no-param pretty)
|
| 692 | |
(declare (ignore simple no-param))
|
|
739 |
(declare (type stream stream)
|
|
740 |
(ignore simple no-param))
|
| 693 | 741 |
(let ((*standard-output* stream))
|
| 694 | 742 |
(cond ((null rn) (princ " ## EMPTY RENAME MAP ##")) ; for debugging.
|
| 695 | 743 |
((%is-rmap rn)
|
|
| 709 | 757 |
|
| 710 | 758 |
;;; RENAME
|
| 711 | 759 |
(defun pr-int-rename (obj &optional (stream *standard-output*) simple no-param)
|
| 712 | |
;; (declare (ignore simple no-param))
|
| 713 | |
(declare (ignore no-param))
|
|
760 |
(declare (type stream stream)
|
|
761 |
(type (or null (not null)) simple)
|
|
762 |
(ignore no-param))
|
| 714 | 763 |
(let ((*standard-output* stream))
|
| 715 | 764 |
(print-modexp (int-rename-module obj) stream t t)
|
| 716 | 765 |
(princ " *{ " stream)
|
|
| 743 | 792 |
|
| 744 | 793 |
;;; PLUS
|
| 745 | 794 |
(defun pr-int-plus (obj &optional (stream *standard-output*) simple no-param)
|
| 746 | |
(declare (ignore simple no-param))
|
|
795 |
(declare (type stream stream)
|
|
796 |
(ignore simple no-param))
|
| 747 | 797 |
(let ((*standard-output* stream))
|
| 748 | 798 |
(let ((*print-indent* (+ *print-indent* 4))
|
| 749 | 799 |
(flg nil))
|
| 750 | 800 |
(dolist (mod (int-plus-args obj))
|
| 751 | 801 |
(print-check)
|
| 752 | 802 |
(when flg (princ " + "))
|
| 753 | |
;; (print-modexp mod stream simple no-param)
|
| 754 | 803 |
(print-modexp mod stream t t)
|
| 755 | 804 |
(setq flg t)))))
|
| 756 | 805 |
|
|
| 758 | 807 |
(defun pr-int-instantiation (obj &optional
|
| 759 | 808 |
(stream *standard-output*)
|
| 760 | 809 |
simple no-param)
|
| 761 | |
(declare (ignore simple no-param))
|
|
810 |
(declare (type stream stream)
|
|
811 |
(ignore simple no-param))
|
| 762 | 812 |
(let ((*standard-output* stream))
|
| 763 | 813 |
(let ((*print-indent* (+ *print-indent* 4)))
|
| 764 | |
;; (print-modexp (int-instantiation-module obj) stream simple no-param)
|
| 765 | 814 |
(print-modexp (int-instantiation-module obj) stream t t)
|
| 766 | |
;; (princ "[ ")
|
| 767 | 815 |
(princ "(")
|
| 768 | 816 |
(let ((flg nil))
|
| 769 | 817 |
(dolist (arg (int-instantiation-args obj))
|
|
| 772 | 820 |
(pos-arg nil))
|
| 773 | 821 |
(cond ((stringp arg-name) (princ arg-name stream))
|
| 774 | 822 |
((and (consp arg-name) (cdr arg-name))
|
| 775 | |
;; (format t "~a@" (car arg-name))
|
| 776 | 823 |
(format t "~a." (car arg-name))
|
| 777 | 824 |
(print-chaos-object (cdr arg-name) stream))
|
| 778 | 825 |
((consp arg-name) (princ (car arg-name) stream))
|
|
| 788 | 835 |
(unless pos-arg
|
| 789 | 836 |
(princ " <= "))
|
| 790 | 837 |
(let ((*print-indent* (+ *print-indent* 4)))
|
| 791 | |
;; (print-view (%!arg-view arg) stream simple no-param)
|
| 792 | |
(print-view (%!arg-view arg) stream t t)
|
| 793 | |
))
|
|
838 |
(print-view (%!arg-view arg) stream t t)))
|
| 794 | 839 |
(print-check)))
|
| 795 | |
;; (princ " ]")
|
| 796 | 840 |
(princ ")"))))
|
| 797 | 841 |
|
| 798 | 842 |
;;;-----------------------------------------------------------------------------
|
|
| 800 | 844 |
;;;-----------------------------------------------------------------------------
|
| 801 | 845 |
|
| 802 | 846 |
(defun print-view-internal (vw &optional (stream *standard-output*) &rest ignore)
|
| 803 | |
(declare (ignore ignore))
|
|
847 |
(declare (type stream stream)
|
|
848 |
(ignore ignore))
|
| 804 | 849 |
(print-view vw stream))
|
| 805 | 850 |
|
| 806 | 851 |
(defun print-view (vw &optional (stream *standard-output*) simple no-param
|
| 807 | 852 |
(syntax *show-mode*))
|
|
853 |
(declare (type stream stream)
|
|
854 |
(type symbol syntax)
|
|
855 |
(type (or null (not null)) simple no-param))
|
| 808 | 856 |
(if (eq syntax :cafeobj)
|
| 809 | 857 |
(print-view-in-cafeobj-mode vw
|
| 810 | 858 |
stream simple
|
|
| 815 | 863 |
no-param)))
|
| 816 | 864 |
|
| 817 | 865 |
(defun print-view-in-cafeobj-mode (vw stream simple no-param)
|
|
866 |
(declare (type stream stream)
|
|
867 |
(type (or null (not null)) simple no-param))
|
| 818 | 868 |
(cond ((and (not (stringp vw))
|
| 819 | 869 |
(chaos-ast? vw)
|
| 820 | 870 |
(memq (ast-type vw)
|
|
| 854 | 904 |
;;
|
| 855 | 905 |
((and (consp vw) (stringp (car vw))) (princ vw stream))
|
| 856 | 906 |
((atom vw) (princ vw stream))
|
| 857 | |
(t (print-modexp vw stream simple no-param))
|
| 858 | |
))
|
|
907 |
(t (print-modexp vw stream simple no-param))))
|
| 859 | 908 |
|
| 860 | 909 |
(defun print-view-in-chaos-mode (vw stream &rest ignore)
|
| 861 | |
(declare (ignore ignore))
|
|
910 |
(declare (type stream stream)
|
|
911 |
(ignore ignore))
|
| 862 | 912 |
(let ((*print-pretty* t))
|
| 863 | 913 |
(format stream "~%~s" (object-decl-form vw))))
|
| 864 | 914 |
|
| 865 | 915 |
(defun print-view-struct-maps (view stream &rest ignore)
|
| 866 | |
(declare (ignore ignore))
|
|
916 |
(declare (type stream stream)
|
|
917 |
(ignore ignore))
|
| 867 | 918 |
(let ((*print-indent* (+ *print-indent* 2))
|
| 868 | 919 |
(sort-maps (view-sort-maps view))
|
| 869 | 920 |
(op-maps (view-op-maps view))
|
|
| 888 | 939 |
(princ "(")(print-chaos-object (term-head (cadr pm)))(princ ")"))))
|
| 889 | 940 |
|
| 890 | 941 |
(defun print-abs-view-mapping (map stream simple no-param pretty)
|
| 891 | |
(declare (ignore simple no-param))
|
|
942 |
(declare (type stream stream)
|
|
943 |
(ignore simple no-param))
|
| 892 | 944 |
(unless map (return-from print-abs-view-mapping nil))
|
| 893 | 945 |
(let ((rmap (if (%is-rmap map)
|
| 894 | 946 |
(%rmap-map map)
|
|
| 906 | 958 |
(print-ren-op opmaps stream pretty)))))
|
| 907 | 959 |
|
| 908 | 960 |
(defun print-view-modexp (me &optional (stream *standard-output*) simple no-param)
|
|
961 |
(declare (type %view me)
|
|
962 |
(type stream stream)
|
|
963 |
(type (or null (not null)) simple no-param))
|
| 909 | 964 |
(when (%view-map me)
|
| 910 | 965 |
(if simple
|
| 911 | 966 |
(princ "{ ... }" stream)
|
|
| 926 | 981 |
|
| 927 | 982 |
(defun print-view-modexp-abbrev (me &optional
|
| 928 | 983 |
(stream *standard-output*) simple no-param)
|
|
984 |
(declare (type stream stream)
|
|
985 |
(type (or null (not null)) simple no-param))
|
| 929 | 986 |
(let ((target (if (view-p me)
|
| 930 | 987 |
(view-target me)
|
| 931 | 988 |
(if (modexp-is-view me)
|
|
| 937 | 994 |
(with-output-panic-message ()
|
| 938 | 995 |
(format t "print-view, given invalid view : ")
|
| 939 | 996 |
(prin1 me))))
|
| 940 | |
;; (chaos-error 'invalid-view))))
|
| 941 | 997 |
(when (stringp me)
|
| 942 | 998 |
(return-from print-view-modexp-abbrev nil))
|
| 943 | 999 |
(when (and (not (view-p me)) (%view-map me))
|
|
| 954 | 1010 |
(defun print-view-mapping (vwmap &optional
|
| 955 | 1011 |
(stream *standard-output*) simple no-param
|
| 956 | 1012 |
pretty)
|
|
1013 |
(declare (type stream stream)
|
|
1014 |
(type (or null (not null)) simple no-param pretty))
|
| 957 | 1015 |
(unless vwmap (return-from print-view-mapping nil))
|
| 958 | 1016 |
(print-rename-map vwmap stream simple no-param pretty))
|
| 959 | 1017 |
|
|
| 964 | 1022 |
;;; OPERATOR **********
|
| 965 | 1023 |
|
| 966 | 1024 |
(defun print-operator-internal (op &optional (stream *standard-output*))
|
|
1025 |
(declare (type operator op)
|
|
1026 |
(type stream stream))
|
| 967 | 1027 |
(format stream "~a/~a."
|
| 968 | 1028 |
(operator-symbol op)
|
| 969 | 1029 |
(operator-num-args op))
|
| 970 | 1030 |
(print-mod-name (operator-module op) stream))
|
| 971 | 1031 |
|
| 972 | 1032 |
(defun print-op-name (op)
|
|
1033 |
(declare (type operator op))
|
| 973 | 1034 |
(format t "~a/~a" (operator-symbol op) (operator-num-args op)))
|
| 974 | 1035 |
|
| 975 | 1036 |
;;; SORT **************
|
| 976 | 1037 |
|
| 977 | 1038 |
(defun print-sort-internal (sort &optional (stream *standard-output*) ignore)
|
| 978 | |
(declare (ignore ignore))
|
|
1039 |
(declare (type sort* sort)
|
|
1040 |
(type stream stream)
|
|
1041 |
(ignore ignore))
|
| 979 | 1042 |
(print-sort-name sort (get-object-context sort) stream))
|
| 980 | 1043 |
|
| 981 | |
(defun print-record-internal (sort &optional (stream *standard-output*) ignore)
|
| 982 | |
(declare (ignore ignore))
|
|
1044 |
(defun print-bsort-internal (sort &optional (stream *standard-output*) ignore)
|
|
1045 |
(declare (type bsort sort)
|
|
1046 |
(type stream stream)
|
|
1047 |
(ignore ignore))
|
| 983 | 1048 |
(print-sort-name sort (get-object-context sort) stream))
|
| 984 | 1049 |
|
| 985 | |
(defun print-class-internal (sort &optional (stream *standard-output*) ignore)
|
| 986 | |
(declare (ignore ignore))
|
|
1050 |
(defun print-and-sort-internal (sort &optional (stream *standard-output*) ignore)
|
|
1051 |
(declare (type and-sort sort)
|
|
1052 |
(type stream stream)
|
|
1053 |
(ignore ignore))
|
| 987 | 1054 |
(print-sort-name sort (get-object-context sort) stream))
|
| 988 | 1055 |
|
| 989 | |
(defun print-bsort-internal (sort &optional (stream *standard-output*) ignore)
|
| 990 | |
(declare (ignore ignore))
|
|
1056 |
(defun print-or-sort-internal (sort &optional (stream *standard-output*) ignore)
|
|
1057 |
(declare (type or-sort sort)
|
|
1058 |
(type stream stream)
|
|
1059 |
(ignore ignore))
|
| 991 | 1060 |
(print-sort-name sort (get-object-context sort) stream))
|
| 992 | 1061 |
|
| 993 | |
(defun print-and-sort-internal (sort &optional (stream *standard-output*) ignore)
|
| 994 | |
(declare (ignore ignore))
|
|
1062 |
(defun print-err-sort-internal (sort &optional (stream *standard-output*) ignore)
|
|
1063 |
(declare (type err-sort sort)
|
|
1064 |
(type stream stream)
|
|
1065 |
(ignore ignore))
|
| 995 | 1066 |
(print-sort-name sort (get-object-context sort) stream))
|
| 996 | 1067 |
|
| 997 | |
(defun print-or-sort-internal (sort &optional (stream *standard-output*) ignore)
|
| 998 | |
(declare (ignore ignore))
|
| 999 | |
(print-sort-name sort (get-object-context sort) stream))
|
| 1000 | |
|
| 1001 | |
(defun print-err-sort-internal (sort &optional (stream *standard-output*) ignore)
|
| 1002 | |
(declare (ignore ignore))
|
| 1003 | |
(print-sort-name sort (get-object-context sort) stream))
|
| 1004 | |
|
| 1005 | 1068 |
;;; MODULE ************
|
| 1006 | 1069 |
|
| 1007 | 1070 |
(defun print-module-internal (module &optional (stream *standard-output*) ignore)
|
| 1008 | |
(declare (ignore ignore))
|
|
1071 |
(declare (type module module)
|
|
1072 |
(type stream stream)
|
|
1073 |
(ignore ignore))
|
| 1009 | 1074 |
(print-mod-name module stream t nil))
|
| 1010 | 1075 |
|
| 1011 | 1076 |
;;; AXIOM *************
|
| 1012 | 1077 |
|
| 1013 | 1078 |
(defun print-axiom-internal (ax &optional (stream *standard-output*) ignore)
|
| 1014 | |
(declare (ignore ignore))
|
|
1079 |
(declare (type rewrite-rule ax)
|
|
1080 |
(type stream stream)
|
|
1081 |
(ignore ignore))
|
| 1015 | 1082 |
(print-axiom-brief ax stream))
|
| 1016 | 1083 |
|
| 1017 | 1084 |
;;; REWRITE RULE *****
|
| 1018 | 1085 |
(defun print-rule-internal (rule &optional (stream *standard-output*) ignore)
|
| 1019 | |
(declare (ignore ignore))
|
|
1086 |
(declare (type rewrite-rule rule)
|
|
1087 |
(type stream stream)
|
|
1088 |
(ignore ignore))
|
| 1020 | 1089 |
(let ((cnd (not (term-is-similar? *BOOL-true* (rule-condition rule))))
|
| 1021 | 1090 |
(.printed-vars-so-far. nil))
|
| 1022 | 1091 |
(when (rule-labels rule)
|
|
| 1050 | 1119 |
;;; METHOD ************
|
| 1051 | 1120 |
|
| 1052 | 1121 |
(defun print-method-internal (meth &optional (stream *standard-output*) ignore)
|
| 1053 | |
(declare (ignore ignore))
|
|
1122 |
(declare (type method meth)
|
|
1123 |
(type stream stream)
|
|
1124 |
(ignore ignore))
|
| 1054 | 1125 |
(let ((mod (get-object-context meth))
|
| 1055 | 1126 |
(.file-col. .file-col.))
|
|
1127 |
(declare (type module mod))
|
| 1056 | 1128 |
(format stream "~{~A~} :" (method-symbol meth))
|
| 1057 | 1129 |
(setq .file-col. (file-column stream))
|
| 1058 | 1130 |
(mapc #'(lambda (x)
|
|
| 1072 | 1144 |
;;;-----------------------------------------------------------------------------
|
| 1073 | 1145 |
|
| 1074 | 1146 |
(defun print-modmorph (mppg)
|
|
1147 |
(declare (type modmorph mppg))
|
| 1075 | 1148 |
(format t "~%Module morphism:")
|
| 1076 | 1149 |
(format t "~& name: ") (print-chaos-object (modmorph-name mppg))
|
| 1077 | 1150 |
(format t "~& sort: ")
|
|
| 1098 | 1171 |
;;;
|
| 1099 | 1172 |
(defun print-sort-name (s &optional (module (get-object-context s))
|
| 1100 | 1173 |
(stream *standard-output*))
|
| 1101 | |
(unless (sort-struct-p s) (break "print-sort-name: given non sort: ~s" s))
|
|
1174 |
(declare (type sort* s)
|
|
1175 |
(type module module)
|
|
1176 |
(type stream stream))
|
| 1102 | 1177 |
(let ((*standard-output* stream)
|
| 1103 | 1178 |
(mod-name (get-module-print-name (sort-module s))))
|
| 1104 | 1179 |
(cond ((and module
|
|
| 1111 | 1186 |
(print-mod-name cntxt stream t t)))
|
| 1112 | 1187 |
(progn
|
| 1113 | 1188 |
(format t "~a." (string (sort-id s)))
|
| 1114 | |
;; (print-simple-mod-name (sort-module s))
|
| 1115 | 1189 |
(print-mod-name (sort-module s) stream t t))))
|
| 1116 | 1190 |
(t (format t "~a" (string (sort-id s)))))))
|
| 1117 | 1191 |
|
| 1118 | |
(defun sort-print-name (sort &optional (with-mod-qualifier))
|
|
1192 |
(defun sort-print-name (sort &optional with-mod-qualifier)
|
|
1193 |
(declare (type sort* sort)
|
|
1194 |
(type (or null (not null)) with-mod-qualifier))
|
| 1119 | 1195 |
(with-output-to-string (str)
|
| 1120 | 1196 |
(let ((*standard-output* str))
|
| 1121 | 1197 |
(if with-mod-qualifier
|
|
| 1128 | 1204 |
;;; PRINT-SORT-LIST
|
| 1129 | 1205 |
;;;
|
| 1130 | 1206 |
(defun print-sort-list (lst &optional
|
| 1131 | |
(module *current-module*)
|
|
1207 |
(module (get-context-module))
|
| 1132 | 1208 |
(stream *standard-output*))
|
|
1209 |
(declare (type list lst)
|
|
1210 |
(type module module)
|
|
1211 |
(type stream stream))
|
| 1133 | 1212 |
(let ((*standard-output* stream))
|
| 1134 | 1213 |
(let ((flag nil))
|
| 1135 | 1214 |
(dolist (s lst)
|
|
| 1137 | 1216 |
(if flag (princ " ") (setq flag t))
|
| 1138 | 1217 |
(print-sort-name s module)))))
|
| 1139 | 1218 |
|
| 1140 | |
(defun print-sort-name2 (sort &optional (module *current-module*)
|
| 1141 | |
(stream *standard-output*))
|
|
1219 |
(defun print-sort-name2 (sort &optional (module (get-context-module))
|
|
1220 |
(stream *standard-output*))
|
|
1221 |
(declare (type sort* sort)
|
|
1222 |
(type module module)
|
|
1223 |
(stream stream))
|
| 1142 | 1224 |
(let ((*standard-output* stream)
|
| 1143 | 1225 |
(*current-sort-order* (module-sort-order module)))
|
| 1144 | 1226 |
(let ((subs (subsorts sort))
|
|
| 1177 | 1259 |
(print-simple-princ (cadr qop))
|
| 1178 | 1260 |
(princ ".")
|
| 1179 | 1261 |
(print-qual-sort-name (caddr qop)))
|
| 1180 | |
(if (consp qop)
|
| 1181 | |
(let ((flag nil))
|
| 1182 | |
(dolist (x qop)
|
| 1183 | |
(if flag (princ " ") (setq flag t))
|
| 1184 | |
(if (consp x) (print-qual-sort-name x)
|
|
1262 |
(if (consp qop)
|
|
1263 |
(let ((flag nil))
|
|
1264 |
(dolist (x qop)
|
|
1265 |
(if flag (princ " ") (setq flag t))
|
|
1266 |
(if (consp x) (print-qual-sort-name x)
|
| 1185 | 1267 |
(princ x))))
|
| 1186 | 1268 |
(print-simple-princ-open qop))))
|
| 1187 | 1269 |
|
|
| 1194 | 1276 |
(equal l (append iota '(0))))))
|
| 1195 | 1277 |
|
| 1196 | 1278 |
(defun print-check-bu-meth (method l)
|
|
1279 |
(declare (type method method))
|
| 1197 | 1280 |
(let ((iota (make-list-1-n (length (method-arity method)))))
|
| 1198 | 1281 |
(or (equal l iota)
|
| 1199 | 1282 |
(equal l (append iota '(0))))))
|
| 1200 | 1283 |
|
| 1201 | 1284 |
(defun print-method-brief (meth)
|
| 1202 | |
(unless (method-p meth)
|
| 1203 | |
(format t "[print-method-brief]: Illegal method given ~a" meth)
|
| 1204 | |
(return-from print-method-brief nil))
|
|
1285 |
(declare (type method meth))
|
| 1205 | 1286 |
(let* ((*print-indent* (+ 4 *print-indent*))
|
| 1206 | 1287 |
(.file-col. *print-indent*)
|
| 1207 | 1288 |
(is-predicate (method-is-predicate meth)))
|
|
| 1217 | 1298 |
(setq .file-col. (1- (file-column *standard-output*)))
|
| 1218 | 1299 |
(when (method-arity meth)
|
| 1219 | 1300 |
(dolist (ar (method-arity meth))
|
| 1220 | |
(print-sort-name ar *current-module*)
|
|
1301 |
(print-sort-name ar (get-context-module))
|
| 1221 | 1302 |
(princ " ")
|
| 1222 | 1303 |
(print-check .file-col. 0)))
|
| 1223 | 1304 |
(unless is-predicate
|
| 1224 | 1305 |
(princ "-> ")
|
| 1225 | |
(print-sort-name (method-coarity meth) *current-module*))
|
|
1306 |
(print-sort-name (method-coarity meth) (get-context-module)))
|
| 1226 | 1307 |
(print-check .file-col. 0)
|
| 1227 | 1308 |
(print-method-attrs meth)))
|
| 1228 | 1309 |
|
| 1229 | 1310 |
(defun operator-decl-form-string (op)
|
|
1311 |
(declare (type method op))
|
| 1230 | 1312 |
(with-output-to-string (stream nil)
|
| 1231 | 1313 |
(let ((*standard-output* stream))
|
| 1232 | 1314 |
(print-method-brief op))
|
|
| 1234 | 1316 |
|
| 1235 | 1317 |
;;; PRINT-OP-BRIEF operator
|
| 1236 | 1318 |
;;;
|
| 1237 | |
(defun print-op-brief (op &optional (module *current-module*)
|
|
1319 |
(defun print-op-brief (op &optional (module (get-context-module))
|
| 1238 | 1320 |
(all t)
|
| 1239 | 1321 |
(every nil)
|
| 1240 | 1322 |
(show-context nil))
|
|
1323 |
(declare (type operator op)
|
|
1324 |
(type module module)
|
|
1325 |
(type (or null (not null)) all every show-context))
|
| 1241 | 1326 |
(let* ((*print-indent* *print-indent*)
|
| 1242 | 1327 |
(opinfo (get-operator-info op (module-all-operators module)))
|
| 1243 | 1328 |
(methods (if all
|
|
| 1262 | 1347 |
;;; PRINT-OP-METH
|
| 1263 | 1348 |
;;;
|
| 1264 | 1349 |
(defun print-op-meth (op-meth mod &optional (all t))
|
|
1350 |
(declare (type module mod)
|
|
1351 |
(type list op-meth))
|
| 1265 | 1352 |
(let ((op (car op-meth))
|
| 1266 | 1353 |
(methods (if all
|
| 1267 | 1354 |
(cadr op-meth)
|
|
| 1280 | 1367 |
(print-method-brief meth)))))))
|
| 1281 | 1368 |
|
| 1282 | 1369 |
(defun print-op-meth2 (op-meth mod &optional (all t))
|
|
1370 |
(declare (type list op-meth)
|
|
1371 |
(type module mod)
|
|
1372 |
(type (or null (not null)) all))
|
| 1283 | 1373 |
(with-in-module (mod)
|
| 1284 | 1374 |
(let ((op (car op-meth))
|
| 1285 | 1375 |
(methods (if all
|
|
| 1311 | 1401 |
;;; PRINT-TERM-HEAD : term module stream -> void
|
| 1312 | 1402 |
;;;
|
| 1313 | 1403 |
(defun print-term-head (term &optional
|
| 1314 | |
(module *current-module*)
|
|
1404 |
(module (get-context-module))
|
| 1315 | 1405 |
(stream *standard-output*))
|
|
1406 |
(declare (type term term)
|
|
1407 |
(type module module)
|
|
1408 |
(type stream stream))
|
| 1316 | 1409 |
(if (operator-method-p term)
|
| 1317 | 1410 |
(print-method term module stream)
|
| 1318 | |
(if (term-is-builtin-constant? term)
|
| 1319 | |
(print-bi-constant-method term module stream)
|
| 1320 | |
(print-method (term-head term) module stream))))
|
|
1411 |
(if (term-is-builtin-constant? term)
|
|
1412 |
(print-bi-constant-method term module stream)
|
|
1413 |
(print-method (term-head term) module stream))))
|
| 1321 | 1414 |
|
| 1322 | 1415 |
;;; PRINT-METHOD : method module stream -> void
|
| 1323 | 1416 |
;;;
|
| 1324 | 1417 |
(defun print-method (method &optional
|
| 1325 | |
(module *current-module*)
|
|
1418 |
(module (get-context-module))
|
| 1326 | 1419 |
(stream *standard-output*))
|
|
1420 |
(declare (type method method)
|
|
1421 |
(type module module)
|
|
1422 |
(type stream stream))
|
| 1327 | 1423 |
(format stream "~{~a~} : " (method-symbol method))
|
| 1328 | 1424 |
(print-sort-list (method-arity method) module stream)
|
| 1329 | 1425 |
(princ " -> " stream)
|
|
| 1331 | 1427 |
|
| 1332 | 1428 |
;;; METHOD-PRINT-STRING
|
| 1333 | 1429 |
;;;
|
| 1334 | |
(defun method-print-string (meth &optional (module *current-module*))
|
|
1430 |
(defun method-print-string (meth &optional (module (get-context-module)))
|
|
1431 |
(declare (type method meth)
|
|
1432 |
(type module module))
|
| 1335 | 1433 |
(with-output-to-string (str)
|
| 1336 | 1434 |
(print-method meth module str)
|
| 1337 | 1435 |
str))
|
|
| 1339 | 1437 |
;;; PRINT-BI-CONSTANT-METHOD (term &optional module stream)
|
| 1340 | 1438 |
;;;
|
| 1341 | 1439 |
(defun print-bi-constant-method (term &optional
|
| 1342 | |
(module *current-module*)
|
|
1440 |
(module (get-context-module))
|
| 1343 | 1441 |
(stream *standard-output*))
|
|
1442 |
(declare (type term term)
|
|
1443 |
(type module module)
|
|
1444 |
(type stream stream))
|
| 1344 | 1445 |
(princ (term-builtin-value term) stream)
|
| 1345 | 1446 |
(princ " : -> ")
|
| 1346 | 1447 |
(print-sort-name (term-sort term) module stream))
|
| 1347 | 1448 |
|
| 1348 | 1449 |
|
| 1349 | |
;;; BI-METHOD-PRINT-STRING (term &optional (module *current-module*))
|
|
1450 |
;;; BI-METHOD-PRINT-STRING
|
| 1350 | 1451 |
;;;
|
| 1351 | |
(defun bi-method-print-string (term &optional (module *current-module*))
|
|
1452 |
(defun bi-method-print-string (term &optional (module (get-context-module)))
|
|
1453 |
(declare (type term term)
|
|
1454 |
(type module module))
|
| 1352 | 1455 |
(with-output-to-string (str)
|
| 1353 | 1456 |
(print-bi-constant-method term module)))
|
| 1354 | 1457 |
|
|
| 1357 | 1460 |
;;;-----------------------------------------------------------------------------
|
| 1358 | 1461 |
|
| 1359 | 1462 |
(defun print-op-attrs (op)
|
|
1463 |
(declare (type operator op))
|
| 1360 | 1464 |
;; print "attributes" -- for the moment ignore purely syntactic
|
| 1361 | 1465 |
;; -- i.e. precedence and associativity .
|
| 1362 | 1466 |
(let ((strat (let ((val (operator-strategy op)))
|
|
| 1386 | 1490 |
(princ " }")))))
|
| 1387 | 1491 |
|
| 1388 | 1492 |
(defun print-method-attrs (method &optional header)
|
|
1493 |
(declare (type method method))
|
| 1389 | 1494 |
(let ((strat (let ((val (method-rewrite-strategy method)))
|
| 1390 | 1495 |
(if (print-check-bu-meth method val) nil val)))
|
| 1391 | 1496 |
(constr (method-constructor method))
|
|
| 1465 | 1570 |
(defun print-id-condition (x stream) (print-id-cond x 10) stream)
|
| 1466 | 1571 |
|
| 1467 | 1572 |
(defun print-id-cond (x p &optional (stream *standard-output*))
|
| 1468 | |
(declare (type fixnum p))
|
|
1573 |
(declare (type fixnum p)
|
|
1574 |
(type stream stream))
|
| 1469 | 1575 |
(let ((*standard-output* stream))
|
| 1470 | 1576 |
(cond ((eq 'and (car x))
|
| 1471 | 1577 |
(let ((paren (< p 4)))
|
|
| 1501 | 1607 |
(print-id-cond c r))))
|
| 1502 | 1608 |
|
| 1503 | 1609 |
(defun print-rule-labels (rul)
|
|
1610 |
(declare (type axiom rul))
|
| 1504 | 1611 |
(let ((labels (axiom-labels rul)))
|
| 1505 | 1612 |
(unless *chaos-verbose*
|
| 1506 | 1613 |
;; (format t "~%~{~s~^ ~}" labels)
|
|
| 1518 | 1625 |
(full-stop nil))
|
| 1519 | 1626 |
(declare (type axiom rul)
|
| 1520 | 1627 |
(type stream stream)
|
| 1521 | |
(type (or null t) no-type no-label meta))
|
|
1628 |
(type (or null (not null)) no-type no-label meta full-stop))
|
| 1522 | 1629 |
(let ((type (axiom-type rul))
|
| 1523 | 1630 |
(cnd (not (term-is-similar? *BOOL-true* (axiom-condition rul))))
|
| 1524 | 1631 |
(.printed-vars-so-far. nil)
|
|
| 1613 | 1720 |
(princ " ."))))
|
| 1614 | 1721 |
|
| 1615 | 1722 |
(defun print-rule-id-inf (x)
|
|
1723 |
(declare (type list x))
|
| 1616 | 1724 |
(print-axiom-brief (nth 0 x)) (terpri)
|
| 1617 | 1725 |
(print-substitution (nth 1 x))
|
| 1618 | 1726 |
(when (cddr x)
|
| 1619 | 1727 |
(progn (print-chaos-object (nth 2 x) nil) (terpri))))
|
| 1620 | 1728 |
|
| 1621 | 1729 |
(defun print-rule (rul)
|
|
1730 |
(declare (type axiom rul))
|
| 1622 | 1731 |
(let ((type (axiom-type rul))
|
| 1623 | 1732 |
(cond (not (term-is-similar? *bool-true* (axiom-condition rul))))
|
| 1624 | 1733 |
(rul-rhs (axiom-rhs rul))
|
|
| 1628 | 1737 |
(if cond
|
| 1629 | 1738 |
(if (axiom-is-behavioural rul)
|
| 1630 | 1739 |
(princ "- conditional behavioural equation ")
|
| 1631 | |
(princ "- conditional equation "))
|
| 1632 | |
(if (axiom-is-behavioural rul)
|
| 1633 | |
(princ "- behavioural equation ")
|
| 1634 | |
(princ "- equation "))))
|
|
1740 |
(princ "- conditional equation "))
|
|
1741 |
(if (axiom-is-behavioural rul)
|
|
1742 |
(princ "- behavioural equation ")
|
|
1743 |
(princ "- equation "))))
|
| 1635 | 1744 |
(:rule
|
| 1636 | 1745 |
(if cond
|
| 1637 | 1746 |
(if (axiom-is-behavioural rul)
|
| 1638 | 1747 |
(princ "- conditional behavioural transition ")
|
| 1639 | |
(princ "- conditional transition "))
|
| 1640 | |
(if (axiom-is-behavioural rul)
|
| 1641 | |
(princ "- behavioural transition ")
|
| 1642 | |
(princ "- transition "))))
|
|
1748 |
(princ "- conditional transition "))
|
|
1749 |
(if (axiom-is-behavioural rul)
|
|
1750 |
(princ "- behavioural transition ")
|
|
1751 |
(princ "- transition "))))
|
| 1643 | 1752 |
(:pignose-axiom
|
| 1644 | 1753 |
(if (axiom-is-behavioural rul)
|
| 1645 | 1754 |
(princ "- behavioural FOPL axiom ")
|
|
| 1680 | 1789 |
(print-next)
|
| 1681 | 1790 |
(princ "* lhs is a variable."))
|
| 1682 | 1791 |
(t
|
| 1683 | |
(let ((head (term-head lhs)))
|
|
1792 |
(let ((head (term-head lhs))
|
|
1793 |
(cntxt (get-context-module)))
|
| 1684 | 1794 |
(print-next)
|
| 1685 | 1795 |
(princ "top operator : ")
|
| 1686 | 1796 |
(when (method-arity head)
|
| 1687 | |
(print-sort-list (method-arity head) *current-module*)
|
|
1797 |
(print-sort-list (method-arity head) cntxt)
|
| 1688 | 1798 |
(princ " "))
|
| 1689 | 1799 |
(princ "-> ")
|
| 1690 | |
(print-sort-name (method-coarity head) *current-module*)))
|
| 1691 | |
)
|
| 1692 | |
;;
|
|
1800 |
(print-sort-name (method-coarity head) cntxt))))
|
| 1693 | 1801 |
(when (axiom-id-condition rul)
|
| 1694 | 1802 |
(print-next)
|
| 1695 | 1803 |
(princ "id condition : ")
|
|
| 1742 | 1850 |
|
| 1743 | 1851 |
;;; *TODO*
|
| 1744 | 1852 |
(defun print-rules-detail (mod)
|
|
1853 |
(declare (type module mod))
|
| 1745 | 1854 |
(let ((rules (module-rules mod)))
|
| 1746 | 1855 |
(dolist (r rules)
|
| 1747 | 1856 |
(print-chaos-object r) (terpri))))
|
|
| 1749 | 1858 |
;;; axiom-declaration-string : axiom -> string
|
| 1750 | 1859 |
;;;
|
| 1751 | 1860 |
(defun axiom-declaration-string (axiom &optional (mod (get-context-module)))
|
|
1861 |
(declare (type axiom axiom)
|
|
1862 |
(type module mod))
|
| 1752 | 1863 |
(with-output-to-string (stream)
|
| 1753 | 1864 |
(with-in-module (mod)
|
| 1754 | 1865 |
(let ((*term-print-depth* nil)
|
|
| 1770 | 1881 |
;;;-----------------------------------------------------------------------------
|
| 1771 | 1882 |
|
| 1772 | 1883 |
(defun print-mapping (mppg &optional (stream *standard-output*))
|
|
1884 |
(declare (type modmorph mppg)
|
|
1885 |
(type stream stream))
|
| 1773 | 1886 |
(let ((*standard-output* stream)
|
| 1774 | 1887 |
(*print-indent* (1+ *print-indent*))
|
| 1775 | 1888 |
(*print-array* nil)
|
|
| 1817 | 1930 |
(print-mod-name (method-module head)
|
| 1818 | 1931 |
*standard-output*
|
| 1819 | 1932 |
t t)
|
| 1820 | |
(princ ")")))
|
| 1821 | |
)
|
|
1933 |
(princ ")"))))
|
| 1822 | 1934 |
(decf *print-indent* 2)
|
| 1823 | 1935 |
(print-next)
|
| 1824 | 1936 |
(princ "module mappings: ")
|
|
| 1834 | 1946 |
;;;-----------------------------------------------------------------------------
|
| 1835 | 1947 |
|
| 1836 | 1948 |
(defun print-rule-ring (rr &optional (stream *standard-output*))
|
|
1949 |
(declare (type rule-ring rr)
|
|
1950 |
(type stream stream))
|
| 1837 | 1951 |
(princ "rule ring: " stream)
|
| 1838 | 1952 |
(do ((rule (initialize-rule-ring rr) (rule-ring-next rr)))
|
| 1839 | 1953 |
;; avoid end-test so can trace it
|
|
| 1847 | 1961 |
;;; SUBSTITUTION
|
| 1848 | 1962 |
|
| 1849 | 1963 |
(defun print-substitution (subst &optional (stream *standard-output*))
|
|
1964 |
(declare (type substitution subst)
|
|
1965 |
(type stream stream))
|
| 1850 | 1966 |
(let ((.file-col. .file-col.))
|
| 1851 | 1967 |
(if (or (substitution-is-empty subst)
|
| 1852 | 1968 |
(null (car subst)))
|
|
| 1871 | 1987 |
;;; PARSE DICTIONARY
|
| 1872 | 1988 |
|
| 1873 | 1989 |
(defun show-parse-dict (dict)
|
|
1990 |
(declare (type parse-dictionary dict))
|
| 1874 | 1991 |
(format t "~%Parse Dictionary:")
|
| 1875 | 1992 |
(maphash #'(lambda (key val)
|
| 1876 | 1993 |
(format t "~% -- key = ~s" key)
|
|
| 1891 | 2008 |
;;; SORT ORDER
|
| 1892 | 2009 |
|
| 1893 | 2010 |
(defun pp-sort-order (&optional (sort-order *current-sort-order*))
|
|
2011 |
(declare (type sort-order sort-order))
|
| 1894 | 2012 |
(maphash #'(lambda (sort sort-rel)
|
| 1895 | 2013 |
(format t "~%[Sort : ~A](~a)" (sort-print-name sort) sort)
|
| 1896 | 2014 |
(format t "~% Subsorts : ~{ ~A~}(~{ ~a~})"
|
|
| 1907 | 2025 |
|
| 1908 | 2026 |
(defun pp-sort-order-raw (module &optional
|
| 1909 | 2027 |
(sort-order (module-sort-order module)))
|
|
2028 |
(declare (type module module)
|
|
2029 |
(type sort-order sort-order))
|
| 1910 | 2030 |
(with-in-module (module)
|
| 1911 | 2031 |
(maphash #'(lambda (sort sort-rel)
|
| 1912 | 2032 |
(format t "~%[Sort : ~A](~a)" (sort-print-name sort) sort)
|
|
| 1924 | 2044 |
|
| 1925 | 2045 |
;;; MODULE INSTANCE DB
|
| 1926 | 2046 |
|
| 1927 | |
(defun print-instance-db (&optional (module *current-module*))
|
|
2047 |
(defun print-instance-db (&optional (module (get-context-module)))
|
|
2048 |
(declare (type module module))
|
| 1928 | 2049 |
(let ((db (module-instance-db module)))
|
| 1929 | 2050 |
(unless db
|
| 1930 | 2051 |
(format t "~%module ")
|