;;       
;; 
;; Utility procedures for manipulating arithmetic expressions. 
;;
;; Copyright 2008-2012 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/>.
;;


(define symbolic-constants `(false true))


(define (sexp->value sexp)
  (cond
	((and (pair? sexp) (eq? 'if (car sexp)))
	 (V:Ifv (sexp->value (cadr sexp)) 
		(sexp->value (caddr sexp))
		(sexp->value (cadddr sexp))))
	((and (pair? sexp) (symbol? (car sexp)))
	 (V:Op (car sexp) (map sexp->value (cdr sexp))))
	((number? sexp)
	 (V:C (exact->inexact sexp)))
	((symbol? sexp)
	 (V:Var sexp))
	(else 
	 (error 'sexp->value "invalid value s-expression" sexp))))


(define (function->expr name fd)
  (let ((r (sexp->value (function-body fd))))
    (if (pair? (function-formals fd))
	(E:Val name (V:Fn (function-formals fd) (E:Ret r)))
	(E:Val name r))
    ))


(define (enum-freevars expr bnds ax)
  (cond ((pair? expr)
	 (case (car expr)
	   ((if) (let ((es (cdr expr))) 
		   (fold (lambda (x ax) (enum-freevars x bnds ax)) ax es)))
	   ((let)
	    (let ((lbnds (cadr expr))
		  (body (caddr expr)))
	      (let ((bnds1 (append (map first lbnds) bnds)))
		(enum-freevars body bnds1 
			       (fold (lambda (x ax) (enum-freevars x bnds ax)) ax
				     (map second lbnds))))))
	   (else
	    (let ((s (car expr)) (es (cdr expr)))
	      (if (symbol? s)  (fold (lambda (x ax) (enum-freevars x bnds ax)) ax es) ax)))
	   ))
	(else
	 (let ((id expr))
	   (if (and (symbol? id) (not (member id bnds)))  (cons id ax) ax)))))


#|


(define (enum-bnds expr ax)
  (match expr 
	 (('if . es)        (fold enum-bnds ax es))
	 (('let bnds body)  (enum-bnds body (append (map car bnds) (fold enum-bnds ax (map cadr bnds)))))
	 ((s . es)          (if (symbol? s)  (fold enum-bnds ax es) ax))
	 (else ax)))


(define (enum-freevars expr bnds ax)
  (match expr 
	 (('if . es)  
	  (fold (lambda (x ax) (enum-freevars x bnds ax)) ax es))
	 (('let lbnds body)  
	  (let ((bnds1 (append (map first lbnds) bnds)))
	    (enum-freevars body bnds1 
	     (fold (lambda (x ax) (enum-freevars x bnds ax)) ax 
		   (map second lbnds)))))
	 ((s . es)    (if (symbol? s)  (fold (lambda (x ax) (enum-freevars x bnds ax)) ax es) ax))
	 (id          (if (and (symbol? id) (not (member id bnds)))  (cons id ax) ax))))


(define (if-convert expr)
  (match expr 
	 (('if c t e) 
	  (let ((r (gensym "if")))
	    `(let ((,r (if ,(if-convert c) ,(if-convert t) ,(if-convert e))))  
	       ,r)))
	 (('let bs e)
	  `(let ,(map (lambda (b) `(,(car b) ,(if-convert (cadr b)))) bs) ,(if-convert e)))
	 ((f . es)
	  (cons f (map if-convert es)))
	 ((? atom? ) expr)))

	 
(define (let-enum expr ax)
  (match expr
	 (('let ((x ('if c t e))) y)
	  (let ((ax (fold let-enum ax (list c ))))
	    (if (eq? x y)  (append ax (list (list x `(if ,c ,t ,e)))) ax)))

	 (('let bnds body)  (append ax bnds))

	 (('if c t e)  (let-enum c ax))

	 ((f . es)  (fold let-enum ax es))

	 (else ax)))


(define (let-elim expr)
  (match expr
	 (('let ((x ('if c t e))) y)
	  (if (eq? x y)  y expr))

	 (('let bnds body) body)

	 (('if c t e)  `(if ,(let-elim c) ,(let-lift t) ,(let-lift e)))

	 ((f . es)  `(,f . ,(map let-elim es)))

	 (else expr)))
  

(define (let-lift expr)
  (define (fbnds bnds)
    (let ((bnds0 
	   (fold (lambda (b ax) 
		   (let ((bexpr  (cadr b)))
		     (match bexpr
			    (('let bnds expr) (append bnds ax))
			    (else (append (let-enum bexpr (list)) ax)))))
		 '() bnds)))
      bnds0))
  (let ((expr1
	 (match expr
		(('let bnds expr) 
		 (let ((bnds0 (fbnds bnds))
		       (expr1 
			`(let  ,(map (lambda (b) (list (car b) (let-elim (cadr b)))) bnds)
			   ,(let-lift expr))))
		     (if (null? bnds0) expr1 `(let ,bnds0 ,expr1))))

		(else 
		 (let ((bnds (let-enum expr (list))))
		   (if (null? bnds) 
		       (let-elim expr)
		       (let ((bnds0 (fbnds bnds))
			     (expr1 `(let ,(map (lambda (b) (list (car b) (let-elim (cadr b)))) bnds)
				       ,(let-elim expr))))
			 (if (null? bnds0) expr1 `(let ,bnds0 ,expr1))))))
		)))
    (if (equal? expr expr1) expr1 
	(let-lift expr1))))


(define (lookup-def k lst . rest)
  (let-optionals rest ((default #f))
    (let ((k (->string k))) 
     (let recur ((kv #f) (lst lst))
       (if (or kv (null? lst))
	(if (not kv) default
 	    (match kv ((k v) v) (else (cdr kv))))
        (let ((kv (car lst)))
          (recur (and (string=? (->string (car kv)) k) kv)
		 (cdr lst)) ))))))


(define (subst-term t subst k)
  (assert (every symbol? (map car subst)))
  (match t
	 (('if c t e)
	  `(if ,(k c subst) ,(k t subst) ,(k e subst)))
		  
	 (('let bs e)
	  (let ((r `(let ,(map (lambda (b) `(,(car b) ,(k (cadr b) subst))) bs) ,(k e subst))))
	    (k r subst)))
		  
	 ((f . es)
	  (cons (k f subst) (map (lambda (e) (k e subst)) es)))
	 
	 ((? symbol? )  (lookup-def t subst t))
	 
	 ((? atom? ) t)))
    

(define (binding? t) 
  (and (list? t) (eq? 'let (car t)) (cdr t)))

(define (bind ks vs e) `(let ,(zip ks vs) ,e))

(define (canonicalize-expr expr)
  (let ((subst-convert  (subst-driver (lambda (x) (and (symbol? x) x)) binding? identity bind subst-term)))
    (let* ((expr1 (if-convert expr))
	   (expr2 (subst-convert expr1 subst-empty))
	   (expr3 (let-lift expr2)))
      expr3)))

|#