;; 
;; Generalized variable substitution semantics.
;;
;; Copyright 2008-2009 Ivan Raikov and the Okinawa Institute of Science and Technology.
;;
;; This program is free software: you can redistribute it and/or
;; modify it under the terms of the GNU General Public License as
;; published by the Free Software Foundation, either version 3 of the
;; License, or (at your option) any later version.
;;
;; This program is distributed in the hope that it will be useful, but
;; WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;; General Public License for more details.
;;
;; A full copy of the GPL license can be found at
;; <http://www.gnu.org/licenses/>.
;;



(module varsubst

   (subst? subst-empty subst-empty?
	   subst-includes? subst-lookup subst-extend
	   subst-map subst-compose
	   subst-driver)

   (import scheme chicken data-structures srfi-1)

(define subst? list?)

(define subst-empty (list))
(define subst-empty? null?)

(define (subst-includes? k subst)
  (and (subst? subst) (any (lambda (p) 
			     (equal? (->string k) (->string (car p)))) subst)))

(define (subst-lookup k subst)
  (and (subst? subst)
       (let ((v (find (lambda (p) (equal? (->string k) (->string (car p)))) subst)))
	 (cadr v))))

(define (subst-extend k v subst)
  (and (subst? subst) (cons (list k v) subst)))

(define (subst-map proc subst)
  (and (subst? subst)
       (map (lambda (p) (list (car p) (proc (cadr p)))) subst)))

;; compose a new substitution and an existing substitution environment
(define (subst-compose a v subst var subst-term)
  (if (subst-includes? a subst)
      (let* ((v1 (subst-lookup a subst))
	     (tsubst  (subst-extend a (var v) subst-empty)))
	(let* ((subst1 (subst-map (lambda (t) (subst-term t tsubst)) subst))
	       (subst2 (subst-extend a (var v) subst1)))
	  (subst-extend v v1 subst2)))
      (subst-extend a (var v) subst)))

(define (subst-driver var? bind? var bind subst-term . rest)
  (let-optionals rest ((prefix "v"))
   (letrec 
       ((k (lambda (t subst)
	     (cond ((var? t)  => (lambda (a) 
				   (if (subst-includes? a subst) (subst-lookup a subst) t)))
		   ((bind? t) => 
		    (lambda (be) 
		      (let ((bnds (car be)) (expr (cadr be)))
			(let-values (((as us) (unzip2 bnds)))
			  (let* ((vs (list-tabulate (length as) (lambda (x) (gensym prefix))))
				 (ksubst-term  (lambda (t tsubst) (subst-term t tsubst k)))
				 (subst1 (fold (lambda (a v subst) (subst-compose a v subst var ksubst-term)) 
					       subst as vs)))
			    (bind vs (map (lambda (u) (subst-term u  subst1 k)) us) (subst-term expr subst1 k)))))))
		   (else (subst-term t subst k))))))
     k)))
)