src/db.lisp

   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))))