1;;; -*- Mode: Lisp; Package: Maxima; Syntax: Common-Lisp; Base: 10 -*- ;;;; 2;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 3;;; The data in this file contains enhancments. ;;;;; 4;;; ;;;;; 5;;; Copyright (c) 1984,1987 by William Schelter,University of Texas ;;;;; 6;;; All rights reserved ;;;;; 7;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 8;;; (c) Copyright 1982 Massachusetts Institute of Technology ;;; 9;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 10 11(in-package :maxima) 12 13(macsyma-module db) 14 15(load-macsyma-macros mrgmac) 16 17;; This file uses its own special syntax which is set up here. The function 18;; which does it is defined in LIBMAX;MRGMAC. It sets up <, >, and : for 19;; structure manipulation. A major bug with this package is that the code is 20;; almost completely uncommented. Someone with nothing better to do should go 21;; through it, figure out how it works, and write it down. 22 23;; External specials 24 25(defvar context 'global) 26(defvar contexts nil) 27(defvar current 'global) 28(defvar dbtrace nil) 29(defvar dobjects nil) 30 31;; Internal specials 32 33(defvar *nobjects* nil) 34(defvar *dbcheck* nil) 35(defvar +l) 36(defvar -l) 37 38(defvar *conindex* 0) 39(defvar *connumber* 50) 40 41(defconstant +lab-high-bit+ most-negative-fixnum) 42 43;; One less than the number of bits in a fixnum. 44(defconstant +labnumber+ (1- (integer-length +lab-high-bit+))) 45 46;; A cell with the high bit turned on. 47(defvar *lab-high-lab* (list +lab-high-bit+)) 48 49;; Variables that are set by (clear) 50(defvar +s) 51(defvar +sm) 52(defvar +sl) 53(defvar -s) 54(defvar -sm) 55(defvar -sl) 56(defvar *labs*) 57(defvar *lprs*) 58(defvar *labindex*) 59(defvar *lprindex*) 60(defvar *marks* 0) 61(defvar +labs nil) 62(defvar -labs nil) 63(defvar ulabs nil) 64 65 66(defvar *world*) 67(defvar *db*) 68 69;; Macro for indirecting through the contents of a cell. 70 71(defmacro unlab (cell) 72 `(car ,cell)) 73 74(defmacro copyn (n) 75 `(list ,n)) 76 77(defmacro iorm (cell n) 78 `(rplaca ,cell (logior (car ,cell) (car ,n)))) 79 80(defmacro xorm (cell n) 81 `(rplaca ,cell (logxor (car ,cell) (car ,n)))) 82 83(defprop global 1 cmark) 84 85(defvar conunmrk (make-array (1+ *connumber*) :initial-element nil)) 86(defvar conmark (make-array (1+ *connumber*) :initial-element nil)) 87 88(defun mark (x) 89 (putprop x t 'mark)) 90 91(defun markp (x) 92 (and (symbolp x) (get x 'mark))) 93 94(defun zl-remprop (sym indicator) 95 (if (symbolp sym) 96 (remprop sym indicator) 97 (unless (atom sym) 98 (remf (cdr sym) indicator)))) 99 100(defun unmrk (x) 101 (zl-remprop x 'mark)) 102 103(defun marks (x) 104 (cond ((numberp x)) 105 ((atom x) (mark x)) 106 (t (mapc #'marks x)))) 107 108(defun unmrks (x) 109 (cond ((numberp x)) 110 ((or (atom x) (numberp (car x))) (unmrk x)) 111 (t (mapc #'unmrks x)))) 112 113(defmode type () 114 (atom (selector +labs) (selector -labs) (selector data)) 115 selector) 116 117(defmode indv () 118 (atom (selector =labs) (selector nlabs) (selector data) (selector in)) 119 selector) 120 121(defmode univ () 122 (atom (selector =labs) (selector nlabs) (selector data) (selector un)) 123 selector) 124 125(defmode datum () 126 (atom (selector ulabs) (selector con) (selector wn)) 127 selector) 128 129(defmode context () 130 (atom (selector cmark fixnum 0) (selector subc) (selector data))) 131 132(defmacro +labz (x) 133 `(cond ((+labs ,x)) 134 (t '(0)))) 135 136(defmacro -labz (x) 137 `(cond ((-labs ,x)) 138 (t '(0)))) 139 140(defmacro =labz (x) 141 `(cond ((=labs ,x)) 142 (t '(0)))) 143 144(defmacro nlabz (x) 145 `(cond ((nlabs ,x)) 146 (t '(0)))) 147 148(defmacro ulabz (x) 149 `(cond ((ulabs ,x)) 150 (t '(0)))) 151 152(defmacro subp (&rest x) 153 (setq x (mapcar #'(lambda (form) `(unlab ,form)) x)) 154 `(= ,(car x) (logand ,@x))) 155 156(defun dbnode (x) 157 (if (symbolp x) x (list x))) 158 159(defun nodep (x) 160 (or (atom x) (mnump (car x)))) 161 162(defun dbvarp (x) 163 (getl x '(un ex))) 164 165(defun lab (n) 166 (ash 1 (1- n))) 167 168(defun lpr (m n) 169 (cond ((do ((l *lprs* (cdr l))) 170 ((null l)) 171 (if (and (labeq m (caaar l)) (labeq n (cdaar l))) 172 (return (cdar l))))) 173 ((= (decf *lprindex*) *labindex*) 174 (break)) 175 (t 176 (push (cons (cons m n) (ash 1 *lprindex*)) *lprs*) 177 (cdar *lprs*)))) 178 179(defun labeq (x y) 180 (= (logior x +lab-high-bit+) (logior y +lab-high-bit+))) 181 182(defun marknd (nd) 183 (cond ((+labs nd)) 184 ((= *lprindex* (incf *labindex*)) 185 (break)) 186 (t (push (cons nd (lab *labindex*)) *labs*) 187 (beg nd (lab *labindex*)) 188 (cdar *labs*)))) 189 190(defun dbv (x r) 191 (do ((l *lprs* (cdr l)) 192 (y 0)) 193 ((null l) y) 194 (unless (or (zerop (logand r (cdar l))) (zerop (logand x (caaar l)))) 195 (setq y (logior (cdaar l) y))))) 196 197(defun dba (r y) 198 (do ((l *lprs* (cdr l)) 199 (x 0)) 200 ((null l) x) 201 (unless (or (zerop (logand r (cdar l))) (zerop (logand (cdaar l) y))) 202 (setq x (logior x (caaar l)))))) 203 204(defun prlab (x) 205 (setq x (unlab x)) 206 (when x 207 (format t " ~,,' ,3:B" (logandc1 +lab-high-bit+ x)))) 208 209(defun onp (cl lab) 210 (subp lab (+labz cl))) 211 212(defun offp (cl lab) 213 (subp lab (-labz cl))) 214 215(defun onpu (lab fact) 216 (subp lab (ulabz fact))) 217 218(defun visiblep (dat) 219 (and (not (ulabs dat)) (cntp dat))) 220 221(defun cancel (lab dat) 222 (cond ((setq *db* (ulabs dat)) 223 (iorm *db* lab)) 224 (t 225 (push dat ulabs) 226 (setq lab (unlab lab)) 227 (putprop dat (copyn lab) 'ulabs)))) 228 229(defun queue+p (nd lab) 230 (cond ((null (setq *db* (+labs nd))) 231 (push nd +labs) 232 (setq lab (unlab lab)) 233 (putprop nd (copyn (logior +lab-high-bit+ lab)) '+labs)) 234 ((subp lab *db*) 235 nil) 236 ((subp *lab-high-lab* *db*) 237 (iorm *db* lab) 238 nil) 239 (t 240 (iorm *db* (copyn (logior +lab-high-bit+ (unlab lab))))))) 241 242(defun beg (nd lab) 243 (setq lab (copyn lab)) 244 (if (queue+p nd lab) 245 (if (null +s) 246 (setq +s (ncons nd) 247 +sm +s 248 +sl +s) 249 (push nd +s)))) 250 251(defun queue-p (nd lab) 252 (cond ((null (setq *db* (-labs nd))) 253 (push nd -labs) 254 (setq lab (unlab lab)) 255 (putprop nd (copyn (logior +lab-high-bit+ lab)) '-labs)) 256 ((subp lab *db*) 257 nil) 258 ((subp *lab-high-lab* *db*) 259 (iorm *db* lab) 260 nil) 261 (t 262 (iorm *db* (copyn (logior +lab-high-bit+ (unlab lab))))))) 263 264(defun beg- (nd lab) 265 (setq lab (copyn lab)) 266 (if (queue-p nd lab) 267 (if (null -s) 268 (setq -s (ncons nd) 269 -sm -s 270 -sl -s) 271 (setq -s (cons nd -s))))) 272 273(defun mid (nd lab) 274 (if (queue+p nd lab) 275 (cond ((null +sm) 276 (setq +s (ncons nd) 277 +sm +s 278 +sl +s)) 279 (t 280 (rplacd +sm (cons nd (cdr +sm))) 281 (if (eq +sm +sl) 282 (setq +sl (cdr +sl))) 283 (setq +sm (cdr +sm)))))) 284 285(defun mid- (nd lab) 286 (if (queue-p nd lab) 287 (cond ((null -sm) 288 (setq -s (ncons nd) 289 -sm -s 290 -sl -s)) 291 (t 292 (rplacd -sm (cons nd (cdr -sm))) 293 (when (eq -sm -sl) 294 (setq -sl (cdr -sl))) 295 (setq -sm (cdr -sm)))))) 296 297(defun end (nd lab) 298 (if (queue+p nd lab) 299 (cond ((null +sl) 300 (setq +s (ncons nd) 301 +sm +s 302 +sl +s)) 303 (t 304 (rplacd +sl (ncons nd)) 305 (setq +sl (cdr +sl)))))) 306 307(defun end- (nd lab) 308 (if (queue-p nd lab) 309 (cond ((null -sl) 310 (setq -s (ncons nd) 311 -sm -s 312 -sl -s)) 313 (t 314 (rplacd -sl (ncons nd)) 315 (setq -sl (cdr -sl)))))) 316 317(defun dq+ () 318 (if +s 319 (prog2 320 (xorm (zl-get (car +s) '+labs) *lab-high-lab*) 321 (car +s) 322 (cond ((not (eq +s +sm)) 323 (setq +s (cdr +s))) 324 ((not (eq +s +sl)) 325 (setq +s (cdr +s) 326 +sm +s)) 327 (t 328 (setq +s nil 329 +sm nil 330 +sl nil)))))) 331 332(defun dq- () 333 (if -s 334 (prog2 335 (xorm (-labs (car -s)) *lab-high-lab*) 336 (car -s) 337 (cond ((not (eq -s -sm)) 338 (setq -s (cdr -s))) 339 ((not (eq -s -sl)) 340 (setq -s (cdr -s) 341 -sm -s)) 342 (t 343 (setq -s nil 344 -sm nil 345 -sl nil)))))) 346 347(defun clear () 348 (when dbtrace 349 (format *trace-output* "~%CLEAR: clearing ~A" *marks*)) 350 (mapc #'(lambda (sym) (push+sto (sel sym +labs) nil)) +labs) 351 (mapc #'(lambda (sym) (push+sto (sel sym -labs) nil)) -labs) 352 (mapc #'(lambda (sym) (zl-remprop sym 'ulabs)) ulabs) 353 (setq +s nil 354 +sm nil 355 +sl nil 356 -s nil 357 -sm nil 358 -sl nil 359 *labs* nil 360 *lprs* nil 361 *labindex* 0 362 *lprindex* +labnumber+ 363 *marks* 0 364 +labs nil 365 -labs nil 366 ulabs nil) 367 (contextmark)) 368 369(defun truep (pat) 370 (clear) 371 (cond ((atom pat) pat) 372 ((prog2 (setq pat (mapcar #'semant pat)) nil)) 373 ((eq (car pat) 'kind) 374 (beg (cadr pat) 1) 375 (beg- (caddr pat) 1) 376 (propg)) 377 (t 378 (beg (cadr pat) 1) 379 (beg- (caddr pat) 2) 380 (beg (car pat) (lpr 1 2)) 381 (propg)))) 382 383(defun falsep (pat) 384 (clear) 385 (cond ((eq (car pat) 'kind) 386 (beg (cadr pat) 1) 387 (beg (caddr pat) 1) 388 (propg)))) 389 390(defun isp (pat) 391 (let ((isp 'unknown) #+ccl (err t)) 392 (ignore-errors 393 (setq isp 394 (cond ((truep pat)) 395 ((falsep pat) nil) 396 (t 'unknown))) 397 #+ccl (setq err nil)) 398 #+ccl 399 (when err 400 (setq +labs nil)) 401 isp)) 402 403(defun kindp (x y) 404 (unless (symbolp x) 405 (merror (intl:gettext "declare: argument must be a symbol; found ~M") x)) 406 (clear) 407 (beg x 1) 408 (do ((p (dq+) (dq+))) 409 ((null p)) 410 (if (eq y p) 411 (return t) 412 (mark+ p (+labs p))))) 413 414(defun true* (pat) 415 (let ((dum (semant pat))) 416 (if dum 417 (cntxt (ind (ncons dum)) context)))) 418 419(defun fact (fun arg val) 420 (cntxt (ind (datum (list fun arg val))) context)) 421 422(defun kind (x y &aux #+kcl (y y)) 423 (setq y (datum (list 'kind x y))) 424 (cntxt y context) 425 (addf y x)) 426 427(defun par (s y) 428 (setq y (datum (list 'par s y))) 429 (cntxt y context) 430 (mapc #'(lambda (lis) (addf y lis)) s)) 431 432(defun datum (pat) 433 (ncons pat)) 434 435(defun ind (dat) 436 (mapc #'(lambda (lis) (ind1 dat lis)) (cdar dat)) 437 (mapc #'ind2 (cdar dat)) 438 dat) 439 440(defun ind1 (dat pat) 441 (cond ((not (nodep pat)) 442 (mapc #'(lambda (lis) (ind1 dat lis)) pat)) 443 ((or (markp pat) (eq 'unknown pat))) 444 (t 445 (addf dat pat) (mark pat)))) 446 447(defun ind2 (nd) 448 (if (nodep nd) 449 (unmrk nd) 450 (mapc #'ind2 nd))) 451 452(defun addf (dat nd) 453 (push+sto (sel nd data) (cons dat (sel nd data)))) 454 455(defun maxima-remf (dat nd) 456 (push+sto (sel nd data) (fdel dat (sel nd data)))) 457 458(defun fdel (fact data) 459 (cond ((and (eq (car fact) (caaar data)) 460 (eq (cadr fact) (cadaar data)) 461 (eq (caddr fact) (caddar (car data)))) 462 (cdr data)) 463 (t 464 (do ((ds data (cdr ds)) 465 (d)) 466 ((null (cdr ds))) 467 (setq d (caadr ds)) 468 (cond ((and (eq (car fact) (car d)) 469 (eq (cadr fact) (cadr d)) 470 (eq (caddr fact) (caddr d))) 471 (push+sto (sel d con data) (delete d (sel d con data) :test #'eq)) 472 (rplacd ds (cddr ds)) (return t)))) 473 data))) 474 475(defun semantics (pat) 476 (if (atom pat) 477 pat 478 (list (semant pat)))) 479 480(defun db-mnump (x) 481 (or (numberp x) 482 (and (not (atom x)) 483 (not (atom (car x))) 484 (member (caar x) '(rat bigfloat) :test #'eq)))) 485 486(defun semant (pat) 487 (cond ((symbolp pat) (or (get pat 'var) pat)) 488 ((db-mnump pat) (dintnum pat)) 489 (t (mapcar #'semant pat)))) 490 491(defun dinternp (x) 492 (cond ((mnump x) (dintnum x)) 493 ((atom x) x) 494 ((assol x dobjects)))) 495 496(defun dintern (x) 497 (cond ((mnump x) (dintnum x)) 498 ((atom x) x) 499 ((assol x dobjects)) 500 (t (setq dobjects (cons (dbnode x) dobjects)) 501 (car dobjects)))) 502 503(defun dintnum (x &aux foo) 504 (cond ((assol x *nobjects*)) 505 ((progn (setq x (dbnode x)) nil)) 506 ((null *nobjects*) 507 (setq *nobjects* (list x)) 508 x) 509 ((eq '$zero (setq foo (rgrp (car x) (caar *nobjects*)))) 510 (let ((context 'global)) 511 (fact 'meqp x (car *nobjects*))) 512 (push x *nobjects*) 513 x) 514 ((eq '$pos foo) 515 (let ((context 'global)) 516 (fact 'mgrp x (car *nobjects*))) 517 (push x *nobjects*) 518 x) 519 (t 520 (do ((lis *nobjects* (cdr lis)) 521 (context '$global)) 522 ((null (cdr lis)) 523 (let ((context 'global)) 524 (fact 'mgrp (car lis) x)) 525 (rplacd lis (list x)) x) 526 (cond ((eq '$zero (setq foo (rgrp (car x) (caadr lis)))) 527 (let ((context 'global)) 528 (fact 'meqp (cadr lis) x)) 529 (rplacd lis (cons x (cdr lis))) 530 (return x)) 531 ((eq '$pos foo) 532 (let ((context 'global)) 533 (fact 'mgrp (car lis) x) 534 (fact 'mgrp x (cadr lis))) 535 (rplacd lis (cons x (cdr lis))) 536 (return x))))))) 537 538(defun doutern (x) 539 (if (atom x) x (car x))) 540 541(defun untrue (pat) 542 (kill (car pat) (semant (cadr pat)) (semant (caddr pat)))) 543 544(defun kill (fun arg val) 545 (kill2 fun arg val arg) 546 (kill2 fun arg val val)) 547 548(defun kill2 (fun arg val cl) 549 (cond ((not (atom cl)) (mapc #'(lambda (lis) (kill2 fun arg val lis)) cl)) 550 ((numberp cl)) 551 (t (push+sto (sel cl data) (kill3 fun arg val (sel cl data)))))) 552 553(defun kill3 (fun arg val data) 554 (cond ((and (eq fun (caaar data)) 555 (eq arg (cadaar data)) 556 (eq val (caddar (car data)))) 557 (cdr data)) 558 (t 559 (do ((ds data (cdr ds)) 560 (d)) 561 ((null (cdr ds))) 562 (setq d (caadr ds)) 563 (cond ((not (and (eq fun (car d)) 564 (eq arg (cadr d)) 565 (eq val (caddr d)))) 566 t) 567 (t (push+sto (sel d con data) (delete d (sel d con data) :test #'eq)) 568 (rplacd ds (cddr ds)) (return t)))) 569 data))) 570 571(defun unkind (x y) 572 (setq y (car (datum (list 'kind x y)))) 573 (kcntxt y context) 574 (maxima-remf y x)) 575 576(defun remov (fact) 577 (remov4 fact (cadar fact)) 578 (remov4 fact (caddar fact))) 579 580(defun remov4 (fact cl) 581 (cond ((or (symbolp cl) ;if CL is a symbol or 582 (and (consp cl) ;an interned number, then we want to REMOV4 FACT 583 (mnump (car cl)))) ;from its property list. 584 (push+sto (sel cl data) (delete fact (sel cl data) :test #'eq))) 585 ((or (atom cl) (atom (car cl)))) ;if CL is an atom (not a symbol) 586 ;or its CAR is an atom then we don't want to do 587 ;anything to it. 588 (t 589 (mapc #'(lambda (lis) (remov4 fact lis)) 590 (cond ((atom (caar cl)) (cdr cl)) ;if CL's CAAR is 591 ;an atom, then CL is an expression, and 592 ;we want to REMOV4 FACT from the parts 593 ;of the expression. 594 ((atom (caaar cl)) (cdar cl))))))) 595 ;if CL's CAAAR is an atom, then CL is a 596 ;fact, and we want to REMOV4 FACT from 597 ;the parts of the fact. 598 599(defun killframe (cl) 600 (mapc #'remov (sel cl data)) 601 (zl-remprop cl '+labs) 602 (zl-remprop cl '-labs) 603 (zl-remprop cl 'obj) 604 (zl-remprop cl 'var) 605 (zl-remprop cl 'fact) 606 (zl-remprop cl 'wn)) 607 608(defun activate (&rest l) 609 (dolist (e l) 610 (cond ((member e contexts :test #'eq) nil) 611 (t (push e contexts) 612 (cmark e))))) 613 614(defun deactivate (&rest l) 615 (dolist (e l) 616 (cond ((not (member e contexts :test #'eq)) 617 nil) 618 (t 619 (cunmrk e) 620 (setq contexts (delete e contexts :test #'eq)))))) 621 622(defun gccon () 623 (gccon1) 624 (when (> *conindex* *connumber*) 625 #+gc (gc) 626 (gccon1) 627 (when (> *conindex* *connumber*) 628 (merror (intl:gettext "context: too many contexts."))))) 629 630(defun gccon1 () 631 (setq *conindex* 0) 632 (do ((i 0 (1+ i))) 633 ((> i *connumber*)) 634 (cond ((not (eq (aref conmark i) (cdr (aref conunmrk i)))) 635 (killc (aref conmark i))) 636 (t 637 (setf (aref conunmrk *conindex*) (aref conunmrk i)) 638 (setf (aref conmark *conindex*) (aref conmark i)) 639 (incf *conindex*))))) 640 641(defun cntxt (dat con) 642 (unless (atom con) 643 (setq con (cdr con))) 644 (putprop con (cons dat (zl-get con 'data)) 'data) 645 (unless (eq 'global con) 646 (putprop dat con 'con)) 647 dat) 648 649(defun kcntxt (fact con) 650 (unless (atom con) 651 (setq con (cdr con))) 652 (putprop con (fdel fact (zl-get con 'data)) 'data) 653 (unless (eq 'global con) 654 (zl-remprop fact 'con)) 655 fact) 656 657(defun cntp (f) 658 (cond ((not (setq f (sel f con)))) 659 ((setq f (zl-get f 'cmark)) 660 (> f 0)))) 661 662(defun contextmark () 663 (let ((con context)) 664 (unless (eq current con) 665 (cunmrk current) 666 (setq current con) 667 (cmark con)))) 668 669(defun cmark (con) 670 (unless (atom con) 671 (setq con (cdr con))) 672 (let ((cm (zl-get con 'cmark))) 673 (putprop con (if cm (1+ cm) 1) 'cmark) 674 (mapc #'cmark (zl-get con 'subc)))) 675 676(defun cunmrk (con) 677 (if (not (atom con)) 678 (setq con (cdr con))) 679 (let ((cm (zl-get con 'cmark))) 680 (cond (cm (putprop con (1- cm) 'cmark))) 681 (mapc #'cunmrk (zl-get con 'subc)))) 682 683(defun killc (con) 684 (contextmark) 685 (unless (null con) 686 (mapc #'remov (zl-get con 'data)) 687 (zl-remprop con 'data) 688 (zl-remprop con 'cmark) 689 (zl-remprop con 'subc)) 690 t) 691 692(defun propg () 693 (do ((x) 694 (lab)) 695 (nil) 696 (cond ((setq x (dq+)) 697 (setq lab (+labs x)) 698 (if (zerop (logand (unlab lab) (unlab (-labz x)))) 699 (mark+ x lab) 700 (return t))) 701 ((setq x (dq-)) 702 (setq lab (-labs x)) 703 (if (zerop (logand (unlab lab) (unlab (+labz x)))) 704 (mark- x lab) 705 (return t))) 706 (t (return nil))))) 707 708(defun mark+ (cl lab) 709 (when dbtrace 710 (incf *marks*) 711 (format *trace-output* "~%MARK+: marking ~A +" cl) 712 (prlab lab)) 713 (mapc #'(lambda (lis) (mark+0 cl lab lis)) (sel cl data))) 714 715(defun mark+3 (dat) 716 (if (/= 0 (logand (unlab (+labz (caddar dat))) 717 (unlab (dbv (+labz (cadar dat)) (-labz (caar dat)))))) 718 (beg- (sel dat wn) *world*))) 719 720(defun mark+0 (cl lab fact) 721 (when *dbcheck* 722 (format *trace-output* "~%MARK+0: checking ~a from ~A+" (car fact) cl) 723 (prlab lab)) 724 (cond ((onpu lab fact)) 725 ((not (cntp fact))) 726 ((null (sel fact wn)) (mark+1 cl lab fact)) 727 ((onp (sel fact wn) *world*) (mark+1 cl lab fact)) 728 ((offp (sel fact wn) *world*) nil) 729 (t (mark+3 fact)))) 730 731(defun mark+1 (cl lab dat) 732 (cond ((eq (caar dat) 'kind) 733 (if (eq (cadar dat) cl) (mid (caddar dat) lab))) ; E1 734 ((eq (caar dat) 'par) 735 (if (not (eq (caddar dat) cl)) 736 (progn 737 (cancel lab dat) ; PR1 738 (mid (caddar dat) lab) 739 (do ((lis (cadar dat) (cdr lis))) 740 ((null lis)) 741 (if (not (eq (car lis) cl)) 742 (mid- (car lis) lab)))))) 743 ((eq (cadar dat) cl) 744 (if (+labs (caar dat)) ; V1 745 (end (caddar dat) (dbv lab (+labs (caar dat))))) 746 (if (-labs (caddar dat)) ; F4 747 (end- (caar dat) (lpr lab (-labs (caddar dat)))))))) 748 749(defun mark- (cl lab) 750 (when dbtrace 751 (incf *marks*) 752 (format *trace-output* "~%MARK-: marking ~A -" cl) 753 (prlab lab)) 754 (mapc #'(lambda (lis) (mark-0 cl lab lis)) (sel cl data))) 755 756(defun mark-0 (cl lab fact) 757 (when *dbcheck* 758 (format *trace-output* "~%MARK-0: checking ~A from ~A-" (car fact) cl) 759 (prlab lab)) 760 (cond ((onpu lab fact)) 761 ((not (cntp fact))) 762 ((null (sel fact wn)) (mark-1 cl lab fact)) 763 ((onp (sel fact wn) *world*) (mark-1 cl lab fact)) 764 ((offp (sel fact wn) *world*) nil))) 765 766(defun mark-1 (cl lab dat) 767 (cond ((eq (caar dat) 'kind) 768 (if (not (eq (cadar dat) cl)) (mid- (cadar dat) lab))) ; E4 769 ((eq (caar dat) 'par) 770 (if (eq (caddar dat) cl) 771 (prog2 772 (cancel lab dat) ; S4 773 (do ((lis (cadar dat) (cdr lis))) 774 ((null lis)) 775 (mid- (car lis) lab))) 776 (progn 777 (setq lab (unlab lab)) ; ALL4 778 (do ((lis (cadar dat) (cdr lis))) 779 ((null lis)) 780 (setq lab (logand (unlab (-labz (car lis))) lab))) 781 (setq lab (copyn lab)) 782 (cancel lab dat) 783 (mid- (caddar dat) lab)))) 784 ((eq (caddar dat) cl) 785 (if (+labs (caar dat)) ; A2 786 (end- (cadar dat) (dba (+labs (caar dat)) lab))) 787 (if (+labs (cadar dat)) ; F6 788 (end- (caar dat) (lpr (+labs (cadar dat)) lab)))))) 789 790;; in out in out ins in out 791;; ----------- ------------- ---------------- 792;; E1 | + INV1 | + AB1 |(+) + + 793;; E2 | - INV2 | - AB2 |(+) - + 794;; E3 | + INV3 | + AB3 |(+) + - 795;; E4 | - INV4 | - AB4 |(+) - - 796;; AB5 |(-) + + 797;; in out in out AB6 |(-) - + 798;; ----------- ------------- AB7 |(-) + - 799;; S1 | (+) ALL1 |(+) + AB8 |(-) - - 800;; S2 | (-) ALL2 |(+) - 801;; S3 |(+) ALL3 |(-) + 802;; S4 |(-) ALL4 |(-) - 803 804 805 806;; in rel out in rel out in rel out 807;; --------------- --------------- --------------- 808;; V1 | (+) + A1 | + (+) F1 | + (+) 809;; V2 | (+) - A2 | - (+) F2 | + (-) 810;; V3 | (-) + A3 | + (-) F3 | - (+) 811;; V4 | (-) - A4 | - (-) F4 | - (-) 812;; F5 |(+) + 813;; F6 |(+) - 814;; F7 |(-) + 815;; F8 |(-) - 816 817(defun uni (p1 p2 al) 818 (cond ((dbvarp p1) (dbunivar p1 p2 al)) 819 ((nodep p1) 820 (cond ((dbvarp p2) (dbunivar p2 p1 al)) 821 ((nodep p2) (if (eq p1 p2) al)))) 822 ((dbvarp p2) (dbunivar p2 p1 al)) 823 ((nodep p2) nil) 824 ((setq al (uni (car p1) (car p2) al)) 825 (uni (cdr p1) (cdr p2) al)))) 826 827(defun dbunivar (p v al) 828 (let ((dum (assoc p al :test #'eq))) 829 (if (null dum) 830 (cons (cons p v) al) 831 (uni (cdr dum) v al)))) 832