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 (defmfun mark (x)
  89   (putprop x t 'mark))
  90
  91 (defmfun markp (x)
  92   (and (symbolp x) (zl-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 (defmfun 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 (defmfun 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 (defmfun 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 (defmfun 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 (defmfun falsep (pat)
 384   (clear)
 385   (cond ((eq (car pat) 'kind)
 386          (beg (cadr pat) 1)
 387          (beg (caddr pat) 1)
 388          (propg))))
 389
 390 (defmfun isp (pat)
 391   (let ((isp 'unknown))
 392     (ignore-errors
 393       (setq isp
 394             (cond ((truep pat))
 395                   ((falsep pat) nil)
 396                   (t 'unknown))))
 397     isp))
 398
 399 (defmfun kindp (x y)
 400   (unless (symbolp x)
 401     (merror (intl:gettext "declare: argument must be a symbol; found ~M") x))
 402   (clear)
 403   (beg x 1)
 404   (do ((p (dq+) (dq+)))
 405       ((null p))
 406     (if (eq y p)
 407         (return t)
 408         (mark+ p (+labs p)))))
 409
 410 (defmfun true* (pat)
 411   (let ((dum (semant pat)))
 412     (if dum
 413         (cntxt (ind (ncons dum)) context))))
 414
 415 (defmfun fact (fun arg val)
 416   (cntxt (ind (datum (list fun arg val))) context))
 417
 418 (defmfun kind (x y &aux #+kcl (y y))
 419   (setq y (datum (list 'kind x y)))
 420   (cntxt y context)
 421   (addf y x))
 422
 423 (defmfun par (s y)
 424   (setq y (datum (list 'par s y)))
 425   (cntxt y context)
 426   (mapc #'(lambda (lis) (addf y lis)) s))
 427
 428 (defmfun datum (pat)
 429   (ncons pat))
 430
 431 (defun ind (dat)
 432   (mapc #'(lambda (lis) (ind1 dat lis)) (cdar dat))
 433   (mapc #'ind2 (cdar dat))
 434   dat)
 435
 436 (defun ind1 (dat pat)
 437   (cond ((not (nodep pat))
 438          (mapc #'(lambda (lis) (ind1 dat lis)) pat))
 439         ((or (markp pat) (eq 'unknown pat)))
 440         (t
 441          (addf dat pat) (mark pat))))
 442
 443 (defun ind2 (nd)
 444   (if (nodep nd)
 445       (unmrk nd)
 446       (mapc #'ind2 nd)))
 447
 448 (defmfun addf (dat nd)
 449   (push+sto (sel nd data) (cons dat (sel nd data))))
 450
 451 (defmfun maxima-remf (dat nd)
 452   (push+sto (sel nd data) (fdel dat (sel nd data))))
 453
 454 (defun fdel (fact data)
 455   (cond ((and (eq (car fact) (caaar data))
 456               (eq (cadr fact) (cadaar data))
 457               (eq (caddr fact) (caddar (car data))))
 458          (cdr data))
 459         (t
 460          (do ((ds data (cdr ds))
 461               (d))
 462              ((null (cdr ds)))
 463            (setq d (caadr ds))
 464            (cond ((and (eq (car fact) (car d))
 465                        (eq (cadr fact) (cadr d))
 466                        (eq (caddr fact) (caddr d)))
 467                   (push+sto (sel d con data) (delete d (sel d con data) :test #'eq))
 468                   (rplacd ds (cddr ds)) (return t))))
 469          data)))
 470
 471 (defun semantics (pat)
 472   (if (atom pat)
 473       pat
 474       (list (semant pat))))
 475
 476 (defun db-mnump (x)
 477   (or (numberp x)
 478       (and (not (atom x))
 479            (not (atom (car x)))
 480            (member (caar x) '(rat bigfloat) :test #'eq))))
 481
 482 (defun semant (pat)
 483   (cond ((symbolp pat) (or (zl-get pat 'var) pat))
 484         ((db-mnump pat) (dintnum pat))
 485         (t (mapcar #'semant pat))))
 486
 487 (defmfun dinternp (x)
 488   (cond ((mnump x) (dintnum x))
 489         ((atom x) x)
 490         ((assol x dobjects))))
 491
 492 (defmfun dintern (x)
 493   (cond ((mnump x) (dintnum x))
 494         ((atom x) x)
 495         ((assol x dobjects))
 496         (t (setq dobjects (cons (dbnode x) dobjects))
 497            (car dobjects))))
 498
 499 (defun dintnum (x &aux foo)
 500   (cond ((assol x *nobjects*))
 501         ((progn (setq x (dbnode x)) nil))
 502         ((null *nobjects*)
 503          (setq *nobjects* (list x))
 504          x)
 505         ((eq '$zero (setq foo (rgrp (car x) (caar *nobjects*))))
 506          (let ((context 'global))
 507            (fact 'meqp x (car *nobjects*)))
 508          (push x *nobjects*)
 509          x)
 510         ((eq '$pos foo)
 511          (let ((context 'global))
 512            (fact 'mgrp x (car *nobjects*)))
 513          (push x *nobjects*)
 514          x)
 515         (t
 516          (do ((lis *nobjects* (cdr lis))
 517               (context '$global))
 518              ((null (cdr lis))
 519               (let ((context 'global))
 520                 (fact 'mgrp (car lis) x))
 521               (rplacd lis (list x)) x)
 522            (cond ((eq '$zero (setq foo (rgrp (car x) (caadr lis))))
 523               (let ((context 'global))
 524                 (fact 'meqp (cadr lis) x))
 525               (rplacd lis (cons x (cdr lis)))
 526               (return x))
 527          ((eq '$pos foo)
 528                   (let ((context 'global))
 529                     (fact 'mgrp (car lis) x)
 530                     (fact 'mgrp x (cadr lis)))
 531                   (rplacd lis (cons x (cdr lis)))
 532                   (return x)))))))
 533
 534 (defmfun doutern (x)
 535   (if (atom x) x (car x)))
 536
 537 (defmfun untrue (pat)
 538   (kill (car pat) (semant (cadr pat)) (semant (caddr pat))))
 539
 540 (defmfun kill (fun arg val)
 541   (kill2 fun arg val arg)
 542   (kill2 fun arg val val))
 543
 544 (defun kill2 (fun arg val cl)
 545   (cond ((not (atom cl)) (mapc #'(lambda (lis) (kill2 fun arg val lis)) cl))
 546         ((numberp cl))
 547         (t (push+sto (sel cl data) (kill3 fun arg val (sel cl data))))))
 548
 549 (defun kill3 (fun arg val data)
 550   (cond ((and (eq fun (caaar data))
 551               (eq arg (cadaar data))
 552               (eq val (caddar (car data))))
 553          (cdr data))
 554         (t
 555          (do ((ds data (cdr ds))
 556               (d))
 557              ((null (cdr ds)))
 558          (setq d (caadr ds))
 559          (cond ((not (and (eq fun (car d))
 560                           (eq arg (cadr d))
 561                           (eq val (caddr d))))
 562                 t)
 563                (t (push+sto (sel d con data) (delete d (sel d con data) :test #'eq))
 564                   (rplacd ds (cddr ds)) (return t))))
 565          data)))
 566
 567 (defmfun unkind (x y)
 568   (setq y (car (datum (list 'kind x y))))
 569   (kcntxt y context)
 570   (maxima-remf y x))
 571
 572 (defmfun remov (fact)
 573   (remov4 fact (cadar fact))
 574   (remov4 fact (caddar fact)))
 575
 576 (defun remov4 (fact cl)
 577   (cond ((or (symbolp cl)               ;if CL is a symbol or
 578              (and (consp cl)            ;an interned number, then we want to REMOV4 FACT
 579                   (mnump (car cl))))    ;from its property list.
 580          (push+sto (sel cl data) (delete fact (sel cl data) :test #'eq)))
 581         ((or (atom cl) (atom (car cl)))) ;if CL is an atom (not a symbol)
 582                                         ;or its CAR is an atom then we don't want to do
 583                                         ;anything to it.
 584         (t
 585          (mapc #'(lambda (lis) (remov4 fact lis))
 586                (cond ((atom (caar cl)) (cdr cl)) ;if CL's CAAR is
 587                                         ;an atom, then CL is an expression, and
 588                                         ;we want to REMOV4 FACT from the parts
 589                                         ;of the expression.
 590                      ((atom (caaar cl)) (cdar cl)))))))
 591                                         ;if CL's CAAAR is an atom, then CL is a
 592                                         ;fact, and we want to REMOV4 FACT from
 593                                         ;the parts of the fact.
 594
 595 (defmfun killframe (cl)
 596   (mapc #'remov (sel cl data))
 597   (zl-remprop cl '+labs)
 598   (zl-remprop cl '-labs)
 599   (zl-remprop cl 'obj)
 600   (zl-remprop cl 'var)
 601   (zl-remprop cl 'fact)
 602   (zl-remprop cl 'wn))
 603
 604 (defmfun activate (&rest l)
 605   (dolist (e l)
 606     (cond ((member e contexts :test #'eq) nil)
 607           (t (push e contexts)
 608              (cmark e)))))
 609
 610 (defmfun deactivate (&rest l)
 611   (dolist (e l)
 612     (cond ((not (member e contexts :test #'eq))
 613            nil)
 614           (t
 615            (cunmrk e)
 616            (setq contexts (delete e contexts :test #'eq))))))
 617
 618 (defun gccon ()
 619   (gccon1)
 620   (when (> *conindex* *connumber*)
 621     #+gc (gc)
 622     (gccon1)
 623     (when (> *conindex* *connumber*)
 624       (merror (intl:gettext "context: too many contexts.")))))
 625
 626 (defun gccon1 ()
 627   (setq *conindex* 0)
 628   (do ((i 0 (1+ i)))
 629       ((> i *connumber*))
 630     (cond ((not (eq (aref conmark i) (cdr (aref conunmrk i))))
 631            (killc (aref conmark i)))
 632           (t
 633            (setf (aref conunmrk *conindex*) (aref conunmrk i))
 634            (setf (aref conmark *conindex*) (aref conmark i))
 635            (incf *conindex*)))))
 636
 637 (defmfun cntxt (dat con)
 638   (unless (atom con)
 639     (setq con (cdr con)))
 640   (putprop con (cons dat (zl-get con 'data)) 'data)
 641   (unless (eq 'global con)
 642     (putprop dat con 'con))
 643   dat)
 644
 645 (defmfun kcntxt (fact con)
 646   (unless (atom con)
 647     (setq con (cdr con)))
 648   (putprop con (fdel fact (zl-get con 'data)) 'data)
 649   (unless (eq 'global con)
 650     (zl-remprop fact 'con))
 651   fact)
 652
 653 (defun cntp (f)
 654   (cond ((not (setq f (sel f con))))
 655         ((setq f (zl-get f 'cmark))
 656          (> f 0))))
 657
 658 (defmfun contextmark ()
 659   (let ((con context))
 660     (unless (eq current con)
 661       (cunmrk current)
 662       (setq current con)
 663       (cmark con))))
 664
 665 (defun cmark (con)
 666   (unless (atom con)
 667     (setq con (cdr con)))
 668   (let ((cm (zl-get con 'cmark)))
 669     (putprop con (if cm (1+ cm) 1) 'cmark)
 670     (mapc #'cmark (zl-get con 'subc))))
 671
 672 (defun cunmrk (con)
 673   (if (not (atom con))
 674       (setq con (cdr con)))
 675   (let ((cm (zl-get con 'cmark)))
 676     (cond (cm (putprop con (1- cm) 'cmark)))
 677     (mapc #'cunmrk (zl-get con 'subc))))
 678
 679 (defmfun killc (con)
 680   (contextmark)
 681   (unless (null con)
 682     (mapc #'remov (zl-get con 'data))
 683     (zl-remprop con 'data)
 684     (zl-remprop con 'cmark)
 685     (zl-remprop con 'subc))
 686   t)
 687
 688 (defun propg ()
 689   (do ((x)
 690        (lab))
 691       (nil)
 692     (cond ((setq x (dq+))
 693            (setq lab (+labs x))
 694            (if (zerop (logand (unlab lab) (unlab (-labz x))))
 695                (mark+ x lab)
 696                (return t)))
 697           ((setq x (dq-))
 698            (setq lab (-labs x))
 699            (if (zerop (logand (unlab lab) (unlab (+labz x))))
 700                (mark- x lab)
 701                (return t)))
 702           (t (return nil)))))
 703
 704 (defun mark+ (cl lab)
 705   (when dbtrace
 706     (incf *marks*)
 707     (format *trace-output* "~%MARK+: marking ~A +" cl)
 708     (prlab lab))
 709   (mapc #'(lambda (lis) (mark+0 cl lab lis)) (sel cl data)))
 710
 711 (defun mark+3 (dat)
 712   (if (/= 0 (logand (unlab (+labz (caddar dat)))
 713                     (unlab (dbv (+labz (cadar dat)) (-labz (caar dat))))))
 714       (beg- (sel dat wn) *world*)))
 715
 716 (defun mark+0 (cl lab fact)
 717   (when *dbcheck*
 718     (format *trace-output* "~%MARK+0: checking ~a from ~A+" (car fact) cl)
 719     (prlab lab))
 720   (cond ((onpu lab fact))
 721         ((not (cntp fact)))
 722         ((null (sel fact wn)) (mark+1 cl lab fact))
 723         ((onp (sel fact wn) *world*) (mark+1 cl lab fact))
 724         ((offp (sel fact wn) *world*) nil)
 725         (t (mark+3 fact))))
 726
 727 (defun mark+1 (cl lab dat)
 728   (cond ((eq (caar dat) 'kind)
 729          (if (eq (cadar dat) cl) (mid (caddar dat) lab))) ; E1
 730         ((eq (caar dat) 'par)
 731          (if (not (eq (caddar dat) cl))
 732              (progn
 733                (cancel lab dat)         ; PR1
 734                (mid (caddar dat) lab)
 735                (do ((lis (cadar dat) (cdr lis)))
 736                    ((null lis))
 737                  (if (not (eq (car lis) cl))
 738                      (mid- (car lis) lab))))))
 739         ((eq (cadar dat) cl)
 740          (if (+labs (caar dat))         ; V1
 741              (end (caddar dat) (dbv lab (+labs (caar dat)))))
 742          (if (-labs (caddar dat))       ; F4
 743              (end- (caar dat) (lpr lab (-labs (caddar dat))))))))
 744
 745 (defun mark- (cl lab)
 746   (when dbtrace
 747     (incf *marks*)
 748     (format *trace-output* "~%MARK-: marking ~A -" cl)
 749     (prlab lab))
 750   (mapc #'(lambda (lis) (mark-0 cl lab lis)) (sel cl data)))
 751
 752 (defun mark-0 (cl lab fact)
 753   (when *dbcheck*
 754     (format *trace-output* "~%MARK-0: checking ~A from ~A-" (car fact) cl)
 755     (prlab lab))
 756   (cond ((onpu lab fact))
 757         ((not (cntp fact)))
 758         ((null (sel fact wn)) (mark-1 cl lab fact))
 759         ((onp (sel fact wn) *world*) (mark-1 cl lab fact))
 760         ((offp (sel fact wn) *world*) nil)))
 761
 762 (defun mark-1 (cl lab dat)
 763   (cond ((eq (caar dat) 'kind)
 764          (if (not (eq (cadar dat) cl)) (mid- (cadar dat) lab))) ; E4
 765         ((eq (caar dat) 'par)
 766          (if (eq (caddar dat) cl)
 767              (prog2
 768                  (cancel lab dat)       ; S4
 769                  (do ((lis (cadar dat) (cdr lis)))
 770                      ((null lis))
 771                    (mid- (car lis) lab)))
 772              (progn
 773                (setq lab (unlab lab))   ; ALL4
 774                (do ((lis (cadar dat) (cdr lis)))
 775                    ((null lis))
 776                  (setq lab (logand (unlab (-labz (car lis))) lab)))
 777                (setq lab (copyn lab))
 778                (cancel lab dat)
 779                (mid- (caddar dat) lab))))
 780         ((eq (caddar dat) cl)
 781          (if (+labs (caar dat))         ; A2
 782              (end- (cadar dat) (dba (+labs (caar dat)) lab)))
 783          (if (+labs (cadar dat))        ; F6
 784              (end- (caar dat) (lpr (+labs (cadar dat)) lab))))))
 785
 786 ;;           in out                    in out                  ins  in out
 787 ;;      -----------             -------------             ----------------
 788 ;;      E1 |     +              INV1 |     +              AB1 |(+)  +   +
 789 ;;      E2 |     -              INV2 |     -              AB2 |(+)  -   +
 790 ;;      E3 | +                  INV3 | +                  AB3 |(+)  +   -
 791 ;;      E4 | -                  INV4 | -                  AB4 |(+)  -   -
 792 ;;                                                         AB5 |(-)  +   +
 793 ;;            in out                    in out             AB6 |(-)  -   +
 794 ;;       -----------             -------------             AB7 |(-)  +   -
 795 ;;       S1 |    (+)             ALL1 |(+)  +              AB8 |(-)  -   -
 796 ;;       S2 |    (-)             ALL2 |(+)  -
 797 ;;       S3 |(+)                 ALL3 |(-)  +
 798 ;;       S4 |(-)                 ALL4 |(-)  -
 799
 800
 801
 802 ;;           in rel out          in rel out          in rel out
 803 ;;      ---------------     ---------------     ---------------
 804 ;;      V1 |    (+)  +      A1 | +  (+)         F1 |     +  (+)
 805 ;;      V2 |    (+)  -      A2 | -  (+)         F2 |     +  (-)
 806 ;;      V3 |    (-)  +      A3 | +  (-)         F3 |     -  (+)
 807 ;;      V4 |    (-)  -      A4 | -  (-)         F4 |     -  (-)
 808 ;;                                              F5 |(+)  +
 809 ;;                                              F6 |(+)  -
 810 ;;                                              F7 |(-)  +
 811 ;;                                              F8 |(-)  -
 812
 813 (defun uni (p1 p2 al)
 814   (cond ((dbvarp p1) (dbunivar p1 p2 al))
 815         ((nodep p1)
 816          (cond ((dbvarp p2) (dbunivar p2 p1 al))
 817                ((nodep p2) (if (eq p1 p2) al))))
 818         ((dbvarp p2) (dbunivar p2 p1 al))
 819         ((nodep p2) nil)
 820         ((setq al (uni (car p1) (car p2) al))
 821          (uni (cdr p1) (cdr p2) al))))
 822
 823 (defun dbunivar (p v al)
 824   (let ((dum (assoc p al :test #'eq)))
 825     (if (null dum)
 826         (cons (cons p v) al)
 827         (uni (cdr dum) v al))))