;
; Support for matching context-rewriting patterns (names, wildcards, holes)
; Chris Pressey, March 2008
;

; Copyright (c)2008 Cat's Eye Technologies.  All rights reserved.
;
; Redistribution and use in source and binary forms, with or without
; modification, are permitted provided that the following conditions
; are met:
;
; 1. Redistributions of source code must retain the above copyright
;    notices, this list of conditions and the following disclaimer.
; 2. Redistributions in binary form must reproduce the above copyright
;    notices, this list of conditions, and the following disclaimer in
;    the documentation and/or other materials provided with the
;    distribution.
; 3. Neither the names of the copyright holders nor the names of their
;    contributors may be used to endorse or promote products derived
;    from this software without specific prior written permission. 
;
; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
; ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES INCLUDING, BUT NOT
; LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
; FOR A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE
; COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
; INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
; BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
; CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
; ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
; POSSIBILITY OF SUCH DAMAGE.

;
; Shorthand for common usage of match.
;
(define toplevel-match
  (lambda (subject pattern)
    (match subject subject pattern (mk-empty-unifier) (mk-base-index))))

;
; Attempt to find a unifier (list of substitutions) which makes
; the given pattern equal to the given term, and return it.
; Return #f if the pattern does not match.
;
; Note that match, upon matching a hole, calls search-match.
; This is mutually recursive, since search-match also calls match.
;
(define match
  (lambda (subject term pattern unifier index)
    (cond ((is-wildcard? pattern)
            unifier)
          ((is-named? pattern)
            (let* ((name     (get-name pattern))
                   (subpat   (get-named-subpat pattern))
                   (submatch (match subject term subpat unifier index)))
              (cond (submatch
                      ; note that we pass the whole subject here
                      (bind-name subject (reverse index) name submatch))
                    (else
                      #f))))
          ((is-hole? pattern)
            (let* ((order  (get-hole-order pattern))
                   (subpat (get-hole-subpat pattern)))
              (cond ((eq? order 'innermost)
                      (search-match-innermost subject term subpat unifier index))
                    ((eq? order 'outermost)
                      (search-match-outermost subject term subpat unifier index))
                    (else
                      #f))))
          ((and (list? term) (list? pattern))
            (match-lists subject term pattern unifier (descend-index index)))
          ((eqv? term pattern)
            unifier)
          (else
            #f))))

;
; Helper function for match.
; Given a term and a pattern, where we know both are lists,
; fold over both of them, matching all the corresponding elements.
;
(define match-lists
  (lambda (subject term pattern unifier index)
    (cond ((and (null? term) (null? pattern))  ; end of both
            unifier)
          ((or (null? term) (null? pattern))   ; end of one but not the other
            #f)
          (else
            (let ((new-unifier (match subject (car term) (car pattern) unifier index))
                  (new-index   (next-index index)))
              (if new-unifier
                (match-lists subject (cdr term) (cdr pattern) new-unifier new-index)
                #f))))))

;
; Match the given pattern to any subterm of the given term, if possible.
; Give priority to the leftmost outermost subterm that matches.
; Returns a new unifier, or #f.
;
; While searching, this tracks a term index which points to the subterm
; that matches.  We pass this back in the returned unifier.
;
(define search-match-outermost
  (lambda (subject term pattern unifier index)
    (let* ((new-unifier (match subject term pattern unifier index)))
      (cond (new-unifier
              new-unifier)
            ((list? term)
              (search-match-list-outermost subject term pattern unifier (descend-index index)))
            (else
              #f)))))

;
; Helper function.  Try to match the given pattern to each term in the
; given list, left to right.  Return new unifier on first successful
; match, or #f is there is none.
;
(define search-match-list-outermost
  (lambda (subject terms pattern unifier index)
    (cond ((null? terms)
            #f)
          (else
            (let* ((new-unifier (search-match-outermost subject (car terms) pattern unifier index))
                   (new-index   (next-index index)))
              (if new-unifier
                new-unifier
                (search-match-list-outermost subject (cdr terms) pattern unifier new-index)))))))

;
; Match the given pattern to any subterm of the given term, if possible.
; Give priority to the leftmost innermost subterm that matches.
; Returns a new unifier, or #f.
;
; While searching, this tracks a term index which points to the subterm
; that matches.  We return this in the returned unifier.
;
(define search-match-innermost
  (lambda (subject term pattern unifier index)
    (cond ((list? term)
            (let* ((new-unifier (search-match-list-innermost subject term pattern unifier (descend-index index))))
              (if new-unifier
                new-unifier
                (match subject term pattern unifier index))))
          (else
            (match subject term pattern unifier index)))))

;
; Helper function.  Try to match the given pattern to each term in the
; given list, left to right.  Return new unifier on first successful
; match, or #f is there is none.
;
(define search-match-list-innermost
  (lambda (subject terms pattern unifier index)
    (cond ((null? terms)
            #f)
          (else
            (let* ((new-unifier (search-match-innermost subject (car terms) pattern unifier index))
                   (new-index   (next-index index)))
              (if new-unifier
                new-unifier
                (search-match-list-innermost subject (cdr terms) pattern unifier new-index)))))))