;
; Support for reducing terms via context-rewriting
; 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.

;
; Given a rule (a pair of a pattern and a map of replacements,)
; apply the rule to the given subject.  If the pattern part of
; the rule matches the subject, replace the subterms that matched
; named subpatterns with the expanded replacement whose key in
; the map is that name.
;
(define apply-rule
  (lambda (subject pattern replacements generation-id)
    (let* ((unifier (match subject subject pattern (mk-empty-unifier) (mk-base-index))))
      (if unifier
        (apply-unifier subject subject unifier unifier replacements generation-id)
        #f))))

;
; Helper function for apply-rule.  For each substitution in the unifier whose
; name is present in some replacement, expand that replacement with values from
; the unifier, and graft it into the subject at the position given in the unifier.
;
(define apply-unifier
  (lambda (complete-subject subject complete-unifier unifier replacements generation-id)
    (if (null? unifier)
      subject
      (let* ((unif-pair         (car unifier))
             (rest-of-unif      (cdr unifier))
             (name              (car unif-pair))
             (index             (cdr unif-pair))
             (repl-pair         (assq name replacements)))
        (if repl-pair
          (let* ((replacement   (cdr repl-pair))
                 (expanded-repl (expand-vars complete-subject replacement complete-unifier generation-id))
                 (new-subject   (term-index-store subject index expanded-repl)))
            (apply-unifier complete-subject new-subject complete-unifier rest-of-unif replacements generation-id))
          (apply-unifier complete-subject subject complete-unifier rest-of-unif replacements generation-id))))))

;
; Given a set of rules, apply repeatedly to subject until none apply.
;
(define reduce
  (lambda (subject complete-rules rules generation-id)
    (if (null? rules)
      subject
      (let* ((rule-pair     (car rules))
             (rest-of-rules (cdr rules))
             (pattern       (car rule-pair))
             (replacements  (cdr rule-pair))
             (new-gen-id    (+ generation-id 1))
             (new-subject   (apply-rule subject pattern replacements generation-id)))
        (if new-subject
          (reduce new-subject complete-rules complete-rules new-gen-id)
          (reduce subject complete-rules rest-of-rules new-gen-id))))))

;
; Useful shortcut for calling reduce.
;
(define toplevel-reduce
  (lambda (subject complete-rules)
    (reduce subject complete-rules complete-rules 0)))