;;; $Id: tc-util.scm,v 1.31 2006/01/29 01:50:01 leavens Exp $
;;; Copyright (C) 2006 Iowa State University
;;;
;;; This file is part of Typedscm.
;;;
;;; This library is free software; you can redistribute it and/or
;;; modify it under the terms of the GNU Lesser General Public License
;;; as published by the Free Software Foundation; either version 2.1,
;;; of the License, or (at your option) any later version.
;;;
;;; This library 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
;;; Lesser General Public License for more details.
;;;
;;; You should have received a copy of the GNU Lesser General Public
;;; License along with Typedscm; see the file LesserGPL.txt.  If not,
;;; write to the Free Software Foundation, Inc., 51 Franklin St, Fifth
;;; Floor, Boston, MA 02110-1301 USA.

;;; Handy procedures that are used in the type checker.
;;;
;;; AUTHOR: Brian Dorn and Gary T. Leavens

(module tc-util (lib "typedscm.ss" "typedscm")

(provide tc:nl-indent tc:max-list tc:intersect
	 tc:no-duplicates? tc:find-duplicates tc:duplicate
	 tc:filter tc:list-split tc:last-item tc:some tc:all
	 tc:force-if-promise
	 tc:string-replace tc:add-slashes tc:extract-name
	 tc:set-one-elem tc:set-rest tc:set-empty? tc:set-member?
	 tc:set-equal? tc:set-subset?)

(deftype tc:nl-indent string)

(deftype tc:max-list (-> ((list-of number)) number))
(deftype tc:intersect (forall (T) (-> ((list-of T) (list-of T)) (list-of T))))
(deftype tc:no-duplicates? (forall (T) (-> ((list-of T)) boolean)))
(deftype tc:find-duplicates (forall (T) (-> ((list-of T)) (list-of T))))
(deftype tc:filter
  (forall (T) (-> ((-> (T) boolean) (list-of T)) (list-of T))))
(deftype tc:list-split
  (forall (T) (-> ((list-of T) number) (pair-of (list-of T) (list-of T)))))
(deftype tc:last-item (forall (T) (-> ((list-of T)) T)))
(deftype tc:some (forall (T) (-> ((-> (T) boolean) (list-of T)) boolean)))
(deftype tc:all (forall (T) (-> ((-> (T) boolean) (list-of T)) boolean)))

(deftype tc:force-if-promise
  (forall (T)
    (all-of (-> ((promise-of T)) T)
	    (-> (T) T))))

(deftype tc:string-replace (-> (string char char) string))
(deftype tc:add-slashes (-> ((list-of string)) string))
(deftype tc:extract-name (-> (string) symbol))

;; a string used in several places
(define tc:nl-indent
  (string-append (string #\newline) "  "))

;;; List utilties

(define tc:max-list
  (lambda (lon)
    ;; REQUIRES: lon contains at least one item
    ;; ENSURES: result is equal to the largest element in lon
    (apply max lon)))

(define tc:intersect
  (lambda (x y)
    ;; ENSURES: result contains all elements
    ;;          that are members of both x and y
    (cond
     ((or (null? y) (null? x)) '())
     ((member (car x) y) (cons (car x) (tc:intersect (cdr x) y)))
     (else (tc:intersect (cdr x) y)))))

(define tc:filter
  (lambda (pred ls)
    ;; ENSURES: result is a list like ls, but
    ;; without the elements of ls that do not pass pred.
    (cond
     ((null? ls) '())
     ((pred (car ls)) (cons (car ls) (tc:filter pred (cdr ls))))
     (else (tc:filter pred (cdr ls))))))
      
(define tc:no-duplicates?
  (lambda (ls)
    (null? (tc:find-duplicates ls))))

(define tc:find-duplicates
  (letrec ((look-for-dups
	    (lambda (ls dups)
	      (cond
	       ((null? ls) dups)
	       ((member (car ls) (cdr ls))
		(look-for-dups (cdr ls) (cons (car ls) dups)))
	       (else (look-for-dups (cdr ls) dups))))))
    (lambda (ls)
      ;; ENSURES: result is a list of all duplicate elements in ls
      (look-for-dups ls '()))))

(define tc:list-split
  (letrec ((iter
	    (lambda (front rear k)
	      ;; REQUIRES: 0 <= k and k <= (length rear)
	      ;;          and (length front) = k
	      (if (zero? k)
		  (cons (reverse front) rear)
		  (iter
		   (cons (car rear) front)
		   (cdr rear)
		   (- k 1))))))
    (lambda (ls n)
      ;; REQUIRES: 0 <= n and n <= (length ls)
      ;; ENSURES: result is a pair of lists, of which the car
      ;;          is n elements long, and the cdr is (length ls) - n long
      ;;          and such that (append (car result) (cdr result)) is ls.
      (iter '() ls n))))

(define tc:last-item
  (lambda (ls)
    ;; REQUIRES: ls is not empty
    ;; ENSURES: result is the last item of ls
    (cond
      ((null? (cdr ls)) (car ls))
      (else (tc:last-item (cdr ls))))))


(define tc:some
  (lambda (pred ls)
    ;; ENSURES: result is true when pred is true for any item in ls.
    (and (not (null? ls))
	 (or (pred (car ls))
	     (tc:some pred (cdr ls))))))

(define tc:all
  (lambda (pred ls)
    ;; ENSURES: result is true just when pred is true for each item in ls.
    (or (null? ls)
	(and (pred (car ls))
	     (tc:all pred (cdr ls))))))

;; Promises

(define tc:force-if-promise
  (has-type-trusted
    (forall (T)
      (all-of (-> ((promise-of T)) T)
	      (-> (T) T)))
    (lambda (e)
      (if (promise? e)
	  (force e) e))))

;; Path manipulation

(define tc:string-replace
  (lambda (str oldc newc)
    ;; ENSURES: result is a new string with all occurrences of oldc
    ;;          replaced with newc.
    (let ((str (string-copy str)))
      (letrec ((iter!
		(lambda (i)
		  (if (not (negative? i))
		      (begin
			(if (eqv? oldc (string-ref str i))
			    (string-set! str i newc))
			(iter! (- i 1)))))))
      (iter! (- (string-length str) 1))
      str))))
		   
(define tc:add-slashes
  (letrec
      ((iter
        (lambda (los ans)
          (if (null? los)
              ans
              (iter (cdr los) (string-append ans (car los) "/"))))))
    (lambda (los)
      ;; ENSURES: result is a string with the strings in los, in
      ;; order, terminated by a slash "/" character.
      (iter los ""))))

(define tc:extract-name
  (letrec ((trim-extension
            (lambda (str)
              (let ((dot-pos (last-pos str #\. (- (string-length str) 1))))
                (if (= dot-pos -1)
                    str
                    (substring str 0 dot-pos)))))
           (trim-directory
            (lambda (str)
              (let* ((len (string-length str))
                     (slash-pos (last-pos str #\/ (- len 1)))
                     (bs-pos (last-pos str #\\ (- len 1))))
                (substring str (+ (max slash-pos bs-pos) 1) len))))
           (last-pos
            (lambda (str ch pos)
              (if (< pos 0)
                  -1
                  (if (char=? ch (string-ref str pos))
                      pos
                      (last-pos str ch (- pos 1)))))))
    (lambda (str)
      ;; ENSURES: result is a module name taken from the filename part
      ;; of the given string without the suffix.
      (string->symbol (trim-extension (trim-directory str))))))

(deftype tc:set-one-elem (forall (T) (-> ((list-of T)) T)))
(define tc:set-one-elem car)

(deftype tc:set-rest (forall (T) (-> ((list-of T)) (list-of T))))
(define tc:set-rest cdr)

(deftype tc:set-empty? (forall (T) (-> ((list-of T)) boolean)))
(define tc:set-empty? null?)

(deftype tc:set-member? (forall (T) (-> (T (list-of T)) boolean)))
(define tc:set-member?
  (lambda (e S)
    (and (not (tc:set-empty? S))
	 (or (equal? e (tc:set-one-elem S))
	     (tc:set-member? e (tc:set-rest S))))))

(deftype tc:set-equal? (forall (T) (-> ((list-of T) (list-of T)) boolean)))
(define tc:set-equal?
  (letrec
      ((set-subset?
	(has-type
	 (forall (T) (-> ((list-of T) (list-of T)) boolean))
	 (lambda (S1 S2)
	   (or (tc:set-empty? S1)
	       (and (tc:set-member? (tc:set-one-elem S1) S2)
		    (set-subset? (tc:set-rest S1) S2)))))))
    (lambda (S1 S2)
      (and (set-subset? S1 S2)
	   (set-subset? S2 S1)))))

(deftype tc:set-subset? (forall (T) (-> ((list-of T) (list-of T)) boolean)))
(define tc:set-subset?
  (lambda (S1 S2)
	   (or (tc:set-empty? S1)
	       (and (tc:set-member? (tc:set-one-elem S1) S2)
		    (tc:set-subset? (tc:set-rest S1) S2)))))

(define tc:duplicate
  (lambda (val len)
    (letrec ((duplicate-maker
	      (lambda (val len accum)
		(if (= len 0)
		    accum
		    (duplicate-maker val (- len 1) (cons val accum))))))
      (duplicate-maker val len '()))))

) ;; end module