inheritance.scm 16.7 KB
Newer Older
1 2
(define-module (logic guile-log inheritance)
  #:use-module (logic guile-log dynlist)
3
  #:use-module (ice-9 pretty-print)
4
  #:use-module (ice-9 match)
5 6 7
  #:export 
  (
   bits-to-is get-high-bit get-rest-bits
8

9
   make-set-theory
10 11
   *current-set-theory*

12 13
   new-set a->b a->b-o set->f
   print-theory print-set
14
   compile-sup-sub
15
   compile-set-representation
16
   mktree 
17 18
   find-matching-sets
   fold-matching-sets
19 20
   get-translation-data
   order-the-set
21 22 23 24
   inh-comb
   mk-get-set
   mk-get-set!
   set<
25
   assoc=>tree
26 27 28

   lookup
   reverse-lookup
29
   ))
30

31 32 33
;; Syntax helpers
(define-syntax-rule (aif (v) p x y)
  (let ((v p)) (if v x y)))
34

35 36 37 38 39
(define-syntax alet* 
  (syntax-rules ()
    ((_ ((a b) . q) code e)
     (aif (a) b (alet* q code e) e))
    ((_ () code e) code)))
40

41 42 43
#|
  Bit twiggling framework
|#
44

45 46
(define-inlinable (bits-to-is set)
  (let lp ((ih set))
47 48 49
      (if (= ih 0)
	  '()
	  (let ((high (get-high-bit ih)))
50 51 52 53 54 55 56 57 58 59 60 61 62 63
	    (cons high (lp (logand ih (lognot high))))))))

(define-inlinable (get-high-bit x) 
  (ash 1 (- (integer-length x) 1)))

(define-inlinable (get-rest-bits x)
  (logand x (lognot (get-high-bit x))))


#|
 - The set theory infrastructure -

This is prepared to make it functional, but currently we mutate
|#
64 65 66 67 68 69 70 71 72 73 74
(define make-set-theory
  (case-lambda
    (() (make-set-theory #f))
    ((super)
     (vector 0 
	     1
	     (make-hash-table)
	     (make-hash-table)
	     (make-hash-table)
	     (make-hash-table)
	     '()
75
	     super
76
	     (make-hash-table)
77
	     (make-hash-table)))))
78 79 80 81

(define-inlinable (get-set     x)     (vector-ref  x 0))
(define-inlinable (get-new     x)     (vector-ref  x 1))
(define-inlinable (get-set->i  x)     (vector-ref  x 2))
82
(define-inlinable (get-i->j    x)     (vector-ref  x 2))
83
(define-inlinable (get-i->set  x)     (vector-ref  x 3))
84
(define-inlinable (get-j->i    x)     (vector-ref  x 3))
85 86
(define-inlinable (get-i->subs x)     (vector-ref  x 4))
(define-inlinable (get-i->sups x)     (vector-ref  x 5))
87
(define-inlinable (get-parent  x)     (vector-ref  x 7))
88
(define-inlinable (get-i->i    x)     (vector-ref  x 8))
89
(define-inlinable (get-i->f    x)     (vector-ref  x 9))
90 91 92 93 94 95 96 97 98 99 100 101 102 103
(define-inlinable (set-set     x v) (vector-set! x 0 v))
(define-inlinable (set-new     x v) (vector-set! x 1 v))
(define-inlinable (set-set->i  x v) (vector-set! x 2 v))
(define-inlinable (set-i->set  x v) (vector-set! x 3 v))
(define-inlinable (set-i->subs x v) (vector-set! x 4 v))

(define-inlinable (put-set->i x k v)
  (hash-set! (get-set->i x) k v))
(define-inlinable (put-i->set x k v)
  (hash-set! (get-i->set x) k v))
(define-inlinable (put-i->subs x k v)
  (hash-set! (get-i->subs x) k v))
(define-inlinable (put-i->sups x k v)
  (hash-set! (get-i->sups x) k v))
104

105
(define-inlinable (get-i    ->i i)   (hash-ref  ->i i #f))
106
(define-inlinable (get-0    ->i i)   (hash-ref  ->i i 0))
107 108
(define-inlinable (get-list ->i i)   (hash-ref  ->i i '()))
(define-inlinable (update   ->i i v) (begin (hash-set! ->i i v) ->i))
109

110 111 112 113 114 115 116 117 118
(define-syntax-rule (update-set-theory th . l)
  (let ((ll (list . l)))
    (aif (r) (member #:set ll)
	 (set-set th (cadr r))
	 #f)
    (aif (r) (member #:new ll)
	 (set-new th (cadr r))
	 #f)
    th))
119 120

#|
121 122 123 124 125
  Enable a current-set-theory interface
|#

(define *current-set-theory* (make-fluid (make-set-theory)))
(define (get-current-set-theory) (fluid-ref *current-set-theory*))
126

127 128 129 130
(define-syntax-rule (mk-get-set set)
  (if set
      (lambda (s)
	(let* ((i (get-i (get-set->i (fluid-ref *current-set-theory*)) s)))
131
	  (set! set (logior set i))
132 133 134 135 136 137 138
	  i))
      (lambda (s) 0)))

(define-syntax-rule (mk-get-set! set)
  (if set
      (lambda (s)
	(let* ((i (get-i (get-set->i (fluid-ref *current-set-theory*)) s)))
139
	  (set! set (logior set i))
140 141 142
	  i))
      (lambda (s) 0)))

143 144 145
#|
Basic construction and removal of set and set graph relationship,
|#
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161

(define print-set
  (case-lambda 
    (() (print-set (fluid-ref *current-set-theory*)))
    ((theory)
     (define (tr x)
       (let lp ((x x) (th theory))
	 (aif (it) (get-parent th)
	      (lp (get-i (get-j->i th) x) it)
	      (get-i (get-i->set th) x))))
     (pk
      (let lp ((l (bits-to-is (- (get-new theory) 1))))
	(if (pair? l)
	    (cons (tr (car l)) (lp (cdr l)))
	    '()))))))

162 163 164 165 166
(define print-theory
  (case-lambda 
    (() (print-theory (fluid-ref *current-set-theory*)))
    ((theory)
     (define out '())
167 168 169 170 171 172
     (define (tr x)
       (let lp ((x x) (th theory))
	 (aif (it) (get-parent th)
	    (lp (get-i (get-j->i th) x) it)
	    (get-i (get-i->set th) x))))

173 174 175 176 177
     (hash-for-each
      (lambda (i s)
	(define target '())
	(set! out
	  (cons
178
	   (list (tr i) '->
179 180 181
		 (let lp ((l (bits-to-is (get-i (get-i->subs theory) i))))
		   (if (pair? l)
		       (cons
182
			(tr (car l))
183 184 185 186 187 188
			(lp (cdr l)))
		       '())))
	   out)))
      (get-i->set theory))
     (pretty-print out))))

189 190 191 192 193 194 195 196 197
(define set->f 
  (case-lambda
    ((set f) (set->f (fluid-ref *current-set-theory*) set f))
    ((theory set f)
     (update-set-theory theory
       #:i->f (update (get-i->f theory) 
		      (get-i (get-set->i theory) set) 
		      f)))))

198 199 200 201 202 203 204 205 206 207 208 209 210 211
(define new-set 
  (case-lambda
    ((set)
     (fluid-set! *current-set-theory*
		 (new-set (fluid-ref *current-set-theory*) set)))
    ((theory set)
     (let ((j (get-new theory)))
       (update-set-theory theory
	 #:set (logior (get-set theory) j)
         #:new (* 2 j)
	 #:->i   (put-set->i  theory set j)
	 #:->set (put-i->set  theory j   set)
	 #:subs  (put-i->subs theory j   j)
	 #:sups  (put-i->sups theory j   j))))))
212

213 214 215 216 217
(define a->b
  (case-lambda*
    ((set-a set-b)
     (fluid-set! *current-set-theory*
		 (a->b (fluid-ref *current-set-theory*) set-a set-b)))
218

219 220 221 222 223 224 225 226 227
    ((theory set-a set-b)
     (let* ((set->i (get-set->i theory))
	    (i->i   (get-i->i   theory))
	    (a      (get-i set->i set-a))
	    (b      (get-i set->i set-b)))
       (update-set-theory theory
	  #:i->i (update i->i a (cons b (get-i i->i a))))))))

(define a->b-o 
228 229 230 231
  (case-lambda*
    ((set-a set-b)
     (fluid-set! *current-set-theory*
		 (a->b (fluid-ref *current-set-theory*) set-a set-b)))
232

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260
    ((theory set-a set-b)
     (let* ((->i     (get-set->i  theory))
	    (->subs  (get-i->subs theory))
	    (->sups  (get-i->sups theory)))
       (alet* ((a  (get-i ->i    set-a))
	       (b  (get-i ->i    set-b))
	       (ah (get-i ->subs a))
	       (bh (get-i ->subs b))
	       (ap (get-i ->sups a)))
	 (begin
	   (when (not (= (logand bh a) 0))
	     (error (format #f "(a->b ~a ~a) created a circle" set-a set-b)))
	   (let lp ((l (bits-to-is ap)) (->subs ->subs))
	     (if (pair? l)
		 (let ((c (car l)))
		   (aif (ch) (get-i ->subs c)
			(lp (cdr l) (update ->subs c (logior bh ch)))
			(error "a->b set is not locatable in hash")))
		 (let lp ((l (bits-to-is bh)) (->sups ->sups))
		   (if (pair? l)
		       (let ((c (car l)))
			 (aif (cp) (get-i ->sups c)
			      (lp (cdr l) (update ->sups c (logior ap cp)))
			      (error "a->b set is not locatable in hash")))
		       (update-set-theory theory
					  #:subs ->subs
					  #:sups ->sups))))))
	 (error "a->b set is not locatable in hash"))))))
261
     
262 263 264 265 266 267
#|
Each function has it's own subspace of to how do we know that a set s is 
if S->S', then we just move on with S'
S->IH IH n World, so this works but is really less efficient, but we would of
cause cache this set for later faster lookup
|#
268

269 270 271
#|
This function introduce a new coding which order the sets and also introduce
a natural generational mapping to help in constructing a match tree.
272
|#
273

274 275 276
(define compile-sup-sub
  (case-lambda 
    (()
277 278
     (fluid-set! *current-set-theory*
		 (compile-sup-sub (fluid-ref *current-set-theory*))))
279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
    ((theory)
     (let ((i->subs (get-i->subs theory))
	   (i->sups (get-i->sups theory))
	   (i->i    (get-i->i    theory)))

       (define (find-leafs)
	 (let lp ((l (bits-to-is (get-set theory))) (leafs 0))
	   (if (pair? l)
	       (if (null? (get-list i->i (car l)))
		   (lp (cdr l) (logior leafs (car l)))
		   (lp (cdr l) leafs))		 
	       leafs)))

       (define (new-generation old)
	 (let lp ((l (bits-to-is (get-set theory))) (new 0))
	   (if (pair? l)
	       (if (= (car l) (logand (car l) old))
		   (lp (cdr l) new)
		   (if (let lp2 ((ll (get-list i->i (car l))))
			 (if (pair? ll)
			     (if (= (car ll) (logand (car ll) old))
				 (lp2 (cdr ll))
				 #f)
			     #t))
		       (lp (cdr l) (logior new (car l)))
		       (lp (cdr l) new)))
	       new)))
       
       (let ((leafs (find-leafs)))
308 309 310 311 312
	 (define (init ->)
	   (let lp ((l (bits-to-is leafs)) (-> ->))
	     (if (pair? l)
		 (lp (cdr l) (update -> (car l) (car l)))
		 ->)))
313
	 (let lp ((new leafs) (subs leafs) 
314
		  (i->subs (init i->subs)) (i->sups (init i->sups)))
315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
	   (if (not (= new 0))
	       (let lp2 ((l (bits-to-is new)) 
			 (i->subs i->subs) (i->sups i->sups))
		 (if (pair? l)
		     (let lp3 ((ll      (get-list i->i (car l))) 
			       (i->subs i->subs) 
			       (i->sups i->sups))
		       (if (pair? ll)
			   (lp3 (cdr ll)
				(update i->subs (car l)
					(logior (get-i i->subs (car l))
						(get-i i->subs (car ll))))
				(update i->sups (car ll)
					(logior (get-i i->sups (car ll))
						(car l))))

			   (lp2 (cdr l) i->subs i->sups)))
		     (let ((subs (logior new subs)))
		       (lp (new-generation subs) subs i->subs i->sups))))

	       (update-set-theory theory
		  #:i->subs i->subs
		  #:i->sups i->sups))))))))

339
(define compile-set-representation 
340 341 342 343 344 345 346 347 348 349 350 351
  (case-lambda
    (()
     (compile-set-representation (fluid-ref *current-set-theory*) ))

    ((setbits-or-theory)
     (if (number? setbits-or-theory)
	 (compile-set-representation (fluid-ref *current-set-theory*) 
				     setbits-or-theory)
	 (compile-set-representation setbits-or-theory
				     (- (get-new setbits-or-theory)
					1))))
     
352
    ((theory setbits)
353 354 355 356 357 358 359 360 361 362 363 364 365 366
     (if (= setbits 0)
	 #f
	 (let ((deps (get-i->subs theory))
	       (sups (get-i->sups theory)))
	   (define (find-all-leafs)
	     (let lp ((ss (bits-to-is setbits)) (leafs 0))
	       (if (pair? ss)
		   (let ((i (car ss)))
		     (aif (ih) (get-i deps i)
			  (if (= i (logand setbits ih))
			      (lp (cdr ss) (logior leafs i))
			      (lp (cdr ss) leafs))
	  (error "compile-set-representatoin has nonmatched bit")))
		   leafs)))
367

368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388
       (define (find-all-newcombers downbits new-downbits)
	 (let lp1 ((ss (bits-to-is new-downbits)) (news 0))
	   (if (pair? ss)
	       (let ((i (car ss)))
		 (aif (hi) (get-i sups i)
		      (let lp2 ((js   (bits-to-is (logand setbits hi)))
				(news news))
			(if (pair? js)
			    (let ((j (car js)))	   
			      (if (and (not (= j i)) (= (logand j downbits) 0))
				  (aif (jh) (get-i deps j)
				       (if (= (logand jh setbits)
					      (logand (logand jh setbits) 
						      (logior j downbits)))
					   (lp2 (cdr js) (logior j news))
					   (lp2 (cdr js) news))
				       (error "missing set registratoin in"))
				  (lp2 (cdr js) news)))
			    (lp1 (cdr ss) news)))
		      (error "missing set registratoin in")))
	       news)))
389
  
390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416
       (define new-theory (make-set-theory theory))
       (define (register-new newbits)
	 (let ((l (bits-to-is newbits))
	       (s (get-set  new-theory)))
	   (let lp ((ss   l)
		    (m    (get-new  new-theory))
		    (i->j (get-i->j new-theory)) 
		    (j->i (get-j->i new-theory)))
	     (if (pair? ss)
		 (let ((i (car ss)))
		   (let ((j m))
		     (lp (cdr ss)
			 (* 2 m)
			 (update i->j i j)
			 (update j->i j i))))
		   (update-set-theory new-theory
		      #:set (logior s newbits)
		      #:new m
		      #:i->j i->j
		      #:j->i j->i)))))
       
       (let ((leafs (find-all-leafs)))
	 (let lp ((downbits leafs) (new-downbits leafs))
	   (if (not (= new-downbits 0))
	       (begin
		 (set! new-theory (register-new new-downbits))
		 (let ((newcoms (find-all-newcombers downbits new-downbits)))
417
		   (lp (logior newcoms downbits) newcoms))))))
418
       
419
       (let ((s       (get-set     new-theory))
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
	     (i->j    (get-i->j    new-theory))
	     (j->subs (get-i->subs new-theory))
	     (j->sups (get-i->sups new-theory))
	     (p->subs (get-i->subs theory))
	     (p->sups (get-i->sups theory)))
	 (let lp ((l (bits-to-is s)) (j->subs j->subs) (j->sups j->sups))
	   (if (pair? l)
	       (let lp2 ((ll (bits-to-is (logand s (get-i p->subs (car l)))))
			 (sub 0))
		 (if (pair? ll)
		     (lp2 (cdr ll) (logior (get-i i->j (car ll)) sub))
		     (let lp3 ((ll 
				(bits-to-is (logand s (get-i p->sups (car l)))))
			       (sup 0))
		       (if (pair? ll)
			   (lp3 (cdr ll) (logior (get-i i->j (car ll)) sup))
			   (lp (cdr l) 
			       (update j->subs (get-i i->j (car l)) sub)
			       (update j->sups (get-i i->j (car l)) sup))))))
	       (set! new-theory
		 (update-set-theory new-theory
			  #:subs j->subs
			  #:sups j->sups)))))
		     
444
       new-theory)))))
445
  
446
#|
447 448 449
    Balanced binary tree compilation

    You take a set i, finds it's subs sub and if sub | m, then dive
450 451 452 453

    each if we have a set s and would like to lookup the matches
  
    
454
|#	 
455 456 457 458 459 460 461 462 463

(define (inh-comb i->f)
  (case-lambda
    ((x)
     (values x 
	     (vector x (get-i i->f x))))
    ((x y)
     (logior x y))
    (() 0)))
464
	
465 466 467 468 469 470
(define (assoc=>tree theory a)
  (let ((p      (get-parent theory))
	(set->i (get-set->i theory))
	(i->j   (get-i->j   theory)))
    (let lp ((a a) (i->f (make-hash-table)))
      (if (pair? a)
471 472 473
	  (let ((key (get-i i->j (caar a))))
	    (lp (cdr a) (update i->f key
				(logior (cdar a) (get-0 i->f key)))))
474
	  (mktree theory i->f)))))
475

476 477
(define mktree 
  (case-lambda* 
478 479 480
    ((i->f #:key (setbits (- (get-new (fluid-ref *current-set-theory*)) 1)))
     (mktree (fluid-ref *current-set-theory*) i->f #:setbits setbits))
    ((theory i->f #:key (setbits (- (get-new theory) 1)))
481 482 483 484 485 486
     (define (clusterize setbits)
       (let ((i->subs  (get-i->subs theory)))
	 (let lp ((ss (bits-to-is setbits)) (done 0))
	   (if (pair? ss)
	       (let* ((i  (car ss)))
		 (if (= (logand done i) 0)
487
		     (let ((ih (logand setbits (get-i i->subs i))))
488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
		       (cons ih (lp (cdr ss) (logior done ih))))
		     (lp (cdr ss) done)))
	       '()))))

     (define (mktree1 setbits)
       (if (= setbits 0)
	   '()
	   (let ((cls (clusterize setbits)))
	     (map 
	      (lambda (cluster-bits)
		(let ((a (get-high-bit  cluster-bits))
		      (t (get-rest-bits cluster-bits)))
		  (cons a (mktree1 t))))
	      cls))))

     (define (linearize tree)
       (let lp ((r tree))
	 (match r
	   ((x . y) (append (linearize x) (linearize y)))
	   (()      '())
	   (x       (list x)))))

510
     (define (p x)
511
       (pk 'revlockup (map (lambda (x) (reverse-lookup theory x)) x))
512 513
       x)

514
     (define setlist (linearize (mktree1 setbits)))
515

516
     (define comb (inh-comb i->f))
517
     (define tree
518 519 520 521
       (let lp ((l (reverse setlist)) (tree (make-dynlist)))
	 (if (pair? l)
	     (let ((i (car l)))
	       (lp (cdr l)
522
		   (dynlist-add tree i comb)))
523
	     tree)))
524
     tree)))
525
     
526 527 528 529
#|
Algorithm to lookup the matching sets iiis, preliminary this will be called
from c-land in the indexer.
|#
530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563

(define reverse-lookup
  (case-lambda
    ((set)
     (lookup (fluid-ref *current-set-theory*) set))
    ((theory set)
     (define (tr x)
       (let lp ((x x) (th theory))
	 (aif (it) (get-parent th)
	      (lp (get-i (get-j->i th) x) it)
	      (get-i (get-i->set th) x))))
     (tr set))))

(define lookup
  (case-lambda
    ((set)
     (lookup (fluid-ref *current-set-theory*) set))
    ((theory set)
     (aif (it) (get-parent theory)
	  (get-i (get-i->j theory) (lookup it set))
	  (get-i (get-set->i theory) set)))))


(define (find-matching-sets theory set tree)
  (let ((ih (get-i (get-i->subs theory) (lookup theory set))))
    (let lp ((l (bits-to-is (fold-dynlist-lr 
			     (lambda (x seed)
			       (logior (vector-ref x 0) seed))
			     tree 0  
			     (lambda (x)
			       (not (= (logand x ih) 0)))))))
      (if (pair? l)
	  (cons (reverse-lookup theory (car l)) (lp (cdr l)))
	  '()))))
564

565 566 567
(define fold-matching-sets
  (case-lambda
    ((f seed set tree)
568
     (fold-matching-sets f seed (fluid-ref *current-set-theory*) set tree))
569 570 571 572 573 574 575 576 577 578
    ((f seed theory set tree)
     (let ((ih (get-i (get-i->subs theory) (lookup theory set))))
       (fold-dynlist-lr 
	(lambda (x seed)
	  (f (reverse-lookup theory (vector-ref x 0))
	     (vector-ref x 1) seed))
	tree 0  
	(lambda (x)
	  (not (= (logand x ih) 0))))))))

579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597
(define get-translation-data
  (case-lambda 
    (() (get-translation-data (fluid-ref *current-set-theory*)))
    ((theory)
     (let lp ((theory theory) (l '()))
       (let ((p (get-parent theory)))
	 (if p
	     (lp p (cons* (get-set theory) (get-i->j theory) 
			  (get-i->subs theory) l))
	     (cons (get-set->i theory) l)))))))
	     

(define order-the-set
  (case-lambda
    (()
     (fluid-set! *current-set-theory*
		 (order-the-set (fluid-ref *current-set-theory*)))) 
    ((theory)
     (compile-set-representation theory))))
598 599 600 601 602 603 604 605 606 607 608

(define set<
  (case-lambda
    ((x y)
     (set< (fluid-ref *current-set-theory*) x y))
    ((theory x y)
     (let ((set->i  (get-set->i  theory))
	   (i->subs (get-i->subs theory)))
       (> (logand (get-i i->subs (get-i set->i y))
		  (get-i set->i x))
	  0)))))