#|
;;; Patterns

;;; Rewriting rules (match and substitute).

   a * (b + c) <==> a * b  +  a * c


      (* (? a) (+ (? b) (? c)))

 (+ (* (? a) (? b)) (* (? a) (? c)))


;;; Pattern-directed invocation

 (goal (= (* (? x) (? x)) (? y)))

 (goal (and (on (? a) (? b))
            (on (? b) (? c))))


;;; Logic

 (can-derive ((? a)
              (implies (? a) (? b)))
             (? b))
|#

;;; Recursive Equality of s-expressions.

(define (equal? a b)
  (cond ((pair? a)
	 (if (pair? b)
	     (and (equal? (car a) (car b))
		  (equal? (cdr a) (cdr b)))
	     #f))
	((pair? b) #f)
	(else (eqv? a b))))

;;; Adding in don't cares

(define (match? a b)
  (cond ((variable? a) #t)
	((pair? a)
	 (if (pair? b)
	     (and (match? (car a) (car b))
		  (match? (cdr a) (cdr b)))
	     #f))
	((pair? b) #f)
	(else (eqv? a b))))

(define (variable? x)
  (and (pair? x)
       (eq? (car x) '?)))

#|
(match? '(a (?) c) '(a b c))
;Value: #t

(match? '(a (?) c) '(a d c))
;Value: #t

(match? '(a (?) c) '(a (b d) c))
;Value: #t

(match? '(a (?) c) '(a (b d) d))
;Value: #f
|#

;;; Named variables collect values

(define (match? a b)
  (define (walk a b dict)
    (cond ((variable? a)
	   (if (named-variable? a)
	       (bind a b
		     dict)
	       dict))
	  ((pair? a)
	   (if (pair? b)
	       (let ((ndict
		      (walk (car a) (car b)
			    dict)))
		 (and ndict
		      (walk (cdr a) (cdr b)
			    ndict)))
	       #f))
	  ((pair? b) #f)
	  ((eqv? a b) dict)
	  (else #f)))
  (walk a b '()))

(define (named-variable? a)
  (and (pair? (cdr a))
       (symbol? (cadr a))))

(define (variable-name a)
  (cadr a))

(define (bind var value dict)
  (cons (list (variable-name var) value)
	dict))

#|
(match? '(a ((? b) 2 3) 1 c)
	'(a (1 2 3) 1 c))
;Value: ((b 1))

(match? '(a (? b) 1 c)
	'(a (1 2 3) 1 c))
;Value: ((b (1 2 3)))


;;; But!

(match? '(a ((? b) 2 3) (? b) c)
	'(a (1 2 3) 1 c))
;Value: ((b 1) (b 1))


(match? '(a ((? b) 2 3) (? b) c)
	'(a (1 2 3) 2 c))
;Value: ((b 2) (b 1))
|#

;;; Two instances of the same named variable 
;;;  must have the same value.

;;; Let's assume all variables are named...

(define (match? a b)
  (define (walk a b dict)
    (cond ((variable? a)
	   (let ((vcell
		  (lookup a dict)))
	     (if vcell
		 (if (equal? (value vcell) b)
		     dict
		     #f)
		 (bind a b dict))))
	  ((pair? a)
	   (if (pair? b)
	       (let ((ndict
		      (walk (car a) (car b)
			    dict)))
		 (and ndict
		      (walk (cdr a) (cdr b)
			    ndict)))
	       #f))
	  ((pair? b) #f)
	  ((eqv? a b) dict)
	  (else #f)))
  (walk a b '()))

(define (value vcell) (cadr vcell))

(define (lookup var dict)
  (assq (variable-name var) dict))

#|
(match? '(a ((? b) 2 3) (? b) c)
	'(a (1 2 3) 1 c))
;Value: ((b 1))


(match? '(a ((? b) 2 3) (? b) c)
	'(a (1 2 3) 2 c))
;Value: #f
|#

;;; Break up into pieces

(define (match? a b)
  (define (walk a b dict)
    (cond ((variable? a)
	   (match-variable a b dict))
	  ((pair? a)
	   (if (pair? b)
	       (let ((ndict
		      (walk (car a) (car b)
			    dict)))
		 (and ndict
		      (walk (cdr a) (cdr b)
			    ndict)))
	       #f))
	  ((pair? b) #f)
	  ((eqv? a b) dict)
	  (else #f)))
  (walk a b '()))

(define (match-variable a b dict)
  (let ((vcell
	 (lookup a dict)))
    (if vcell
	(if (equal? (value vcell) b)
	    dict
	    #f)
	(bind a b dict))))

;;; Matching lists rather than pairs

(define (match? a b)
  (define (walk a b dict)
    (cond ((variable? a)
	   (match-variable a b dict))
	  ((pair? a)
	   (if (pair? b)
	       (let lp ((a a) (b b) (dict dict))
		 (cond ((and (null? a)
			     (null? b))
			dict)
		       ((or (null? a) (null? b))
			#f)
		       (else
			(let ((ndict
			       (walk (car a)
				     (car b)
				     dict)))
			  (and ndict
			       (lp (cdr a)
				   (cdr b)
				   ndict))))))
	       #f))
	  ((pair? b) #f)
	  ((eqv? a b) dict)
	  (else #f)))
  (walk a b '()))

;;; Segment Variables eat many elements.  
;;; Need continuations to do search.
;;; First transform to lists at all levels.

(define (match? a b)
  (define (walk a b dict cont)
    (cond ((variable? a)
	   (match-variable a b dict cont))
	  ((pair? a)
	   (if (pair? b)
	       (let lp ((p a)
			(items (car b))
			(dict dict))
		 (cond ((pair? p)
			(walk (car p) items dict
			    (lambda (ndict rest)
			      (lp (cdr p)
				  rest
				  ndict))))
		       ((pair? items) #f)
		       (else
			(cont dict (cdr b)))))
	       #f))
	  ((and (pair? b) (eqv? a (car b)))
	   (cont dict (cdr b)))
	  (else #f)))
  (walk a (list b) '()
	(lambda (dict rest)
	  (and (null? rest)
	       dict))))

(define (match-variable a b dict cont)
  (let ((vcell
	 (lookup a dict)))
    (if vcell
	(if (equal? (value vcell) (car b))
	    (cont dict (cdr b))
	    #f)
	(cont (bind a (car b) dict)
		  (cdr b)))))

;;; Abstract out list matcher.
;;; Add in segment matcher.

(define (match? a b)
  (define (walk a b dict cont)
    (cond ((variable? a)
	   (match-variable a b dict cont))
	  ((segment? a)
	   (match-segment a b dict cont))
	  ((pair? a)
	   (match-pair a b dict walk cont))
	  ((and (pair? b) (eqv? a (car b)))
	   (cont dict (cdr b)))
	  (else #f)))
  (walk a (list b) '()
	(lambda (dict rest)
	  (and (null? rest)
	       dict))))

(define (match-pair a b dict walk cont)
  (if (pair? b)
      (let lp ((p a)
	       (items (car b))
	       (dict dict))
	(cond ((pair? p)
	       (walk (car p) items dict
		     (lambda (ndict rest)
		       (lp (cdr p)
			   rest
			   ndict))))
	      ((pair? items) #f)
	      (else
	       (cont dict (cdr b)))))
      #f))

(define (match-segment a b dict cont)
  (and (or (pair? b) (null? b))
       (let try-seg ((end b))
	 (or (cont
	      (bind a
		    (make-segment b end)
		    dict)
	      end)
	     (and (pair? end)
		  (try-seg (cdr end)))))))

(define (segment? x)
  (and (pair? x)
       (eq? (car x) '??)))

(define (make-segment start end)
  (vector start end))

#|
(pp (match? '(a (?? x) b (?? y) c)
	    '(a a b b b b b b c)))
((y #((b b b b b c) (c)))
 (x #((a b b b b b b c) (b b b b b b c))))
|#

;;; Segments with same name have same value.

(define (match-segment a b dict cont)
  (and (or (pair? b) (null? b))
       (let ((vcell (lookup a dict)))
	 (if vcell
	     (let ((v (value vcell)))
	       (let ((end (segment-end v)))
		 (let scan
		     ((vptr (segment-beg v))
		      (dptr b))
		   (cond ((eq? vptr end)
			  (cont dict dptr))
			 ((not (pair? dptr)) #f)
			 ((equal? (car vptr)
				  (car dptr))
			  (scan (cdr vptr)
				(cdr dptr)))
			 (else #f)))))
	     (try-seg a b dict cont)))))

(define (try-seg a b dict cont)
  (let lp ((end b))
    (or (cont
	 (bind a
	       (make-segment b end)
	       dict)
	 end)
	(and (pair? end)
	     (lp (cdr end))))))

(define (segment-beg v)
  (vector-ref v 0))

(define (segment-end v)
  (vector-ref v 1))

;;; Get other matches

(define (match? a b #!optional cont)
  (define (walk a b dict cont)
    (cond ((variable? a)
	   (match-variable a b dict cont))
	  ((segment? a)
	   (match-segment a b dict cont))
	  ((pair? a)
	   (match-pair a b dict walk cont))
	  ((and (pair? b) (eqv? a (car b)))
	   (cont dict (cdr b)))
	  (else #f)))
  (if (default-object? cont)
      (walk a (list b) '()
	    (lambda (dict rest)
	      (and (null? rest)
		   dict)))
      (walk a (list b) '()
	    (lambda (dict rest)
	      (and (null? rest)
		   (cont dict))))))

#|
(match? '(a (?? x) (?? y) (?? x) c)
        '(a b b b b b b c)
	(lambda (dict)
	  (display "#|\n ")
	  (pp dict)
	  (display "|#\n")
	  #f))
#|
 ((y #((b b b b b b c) (c)))
  (x #((b b b b b b c) (b b b b b b c))))
|#
#|
 ((y #((b b b b b c) (b c)))
   (x #((b b b b b b c) (b b b b b c))))
|#
#|
 ((y #((b b b b c) (b b c)))
   (x #((b b b b b b c) (b b b b c))))
|#
#|
 ((y #((b b b c) (b b b c)))
  (x #((b b b b b b c) (b b b c))))
|#
 
;Value: #f
|#