;;; $Id: tc-ignore-types-at-runtime.scm,v 1.4 2006/01/18 23:17:27 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.

;;; Use this file if you aren't using the type checker but are working with
;;; Scheme files that have deftypes and defreps in them

;;; The following is specialized to Chez Scheme version
;;; See ../drscheme/tc-ignore-types-at-runtime.scm for the MzScheme version.

;;; The following are R5RS macros.

(define-syntax has-type
    (syntax-rules ()
      ((has-type type-exp expression)
       expression)))

(define-syntax has-type-trusted
    (syntax-rules ()
      ((has-type-trusted type-exp expression)
       expression)))

(define-syntax test-type
  (lambda (x)
    (syntax-case x ( -> list-of vector-of pair-of all-of)
      ((test-type (-> (arg-pred ...) res-pred) expression)
       (with-syntax (((arg ...) (generate-temporaries (syntax (arg-pred ...)))))
		    (syntax (let ((val expression))
			      (if (procedure? val)
				  (lambda (arg ...)
				    (test-type
				     res-pred
				     (val (test-type arg-pred arg) ...)))
				  (eopl:error
				   'test-type
				   "Testing type with procedure? failed for ~s"
				   val))))))
      ((test-type (list-of elem-pred) expression)
       (syntax (let ((val expression))
		 (if (list? val)
		     (do ((ls val (cdr ls)))
			 ((null? ls) val)
		       (set-car! ls (test-type elem-pred (car ls))))
		     (eopl:error
		      'test-type
		      "Testing type with list? failed for ~s"
		      val)))))
      ((test-type (vector-of elem-pred) expression)
       (syntax (let ((val expression))
		 (if (vector? val)
		     (do ((i (- (vector-length val) 1) (- i 1)))
			 ((negative? i) val)
		       (vector-set! val i
				    (test-type elem-pred (vector-ref val i))))
		     (eopl:error
		      'test-type
		      "Testing type with vector? failed for ~s"
		      val)))))
      ((test-type (pair-of pred1 pred2) expression)
       (syntax (let ((val expression))
		 (if (pair? val)
		     (begin
		       (set-car! val (test-type pred1 (car val)))
		       (set-cdr! val (test-type pred2 (cdr val)))
		       val)
		     (eopl:error
		      'test-type
		      "Testing type with pair? failed for ~s"
		      val)))))
      ((test-type type-pred expression)
       (syntax (let ((val expression))
		 (if (type-pred val)
		     val
		     (eopl:error
		      'test-type
		      "Testing type with ~s failed for ~s"
		      'type-pred
		      val))))))))

;; The <- procedure is defined in type-predicates.scm
(define-syntax ->
  (syntax-rules ()
    ((-> (argument-predicate ...) result-predicate)
     (<- result-predicate argument-predicate ...))))

(define-syntax forall
  (syntax-rules ()
    ((forall type-predicate-formals predicate-expression)
     (lambda type-predicate-formals predicate-expression))))

;; The following relies on syntax-case and generate-temporaries.
;; These are supposed to be in both MzScheme and Chez Scheme.
;; See below if these don't work for you.
;; However, the more complex translation is preferred, as it makes
;; deftype be a definition form.
(define-syntax deftype
  (lambda (x)
    (syntax-case x ()
      ((deftype name type-exp)
       (with-syntax (((gname) (generate-temporaries (syntax (name)))))
	  (syntax (define gname #f)))))))

;; Use the following if you can't get the above definition of deftype to work
;; in your Scheme system.
; (define-syntax deftype
;   (syntax-rules ()
;     ((deftype name type-exp)
;      (void)))) ; should be a definition form, technically

(define-syntax defrep
  (syntax-rules (forall)
    ((defrep (forall (type-var ...) abstract-type concrete-type))
     (begin))
    ((defrep (abstract-type concrete-type))
     (begin))
    ((defrep (forall (type-var ...) abstract-type concrete-type)
       abs-conc-pair ...)
     (defrep abs-conc-pair ...))
    ((defrep (abstract-type concrete-type) abs-conc-pair ...)
     (defrep abs-conc-pair ...))
    ))

(define datum? (lambda (x) #t))
(define ... datum?)

(define void? (lambda (x) #f))
(define poof? void?)

;;; Type predicate transformers that the type checker "understands"

(define pair-of
  (forall (S? T?)
    (if (not (procedure? S?))
	(eopl:error 'pair-of
		    "Expecting type predicates as left argument, not ~s"
		    S?)
	(if (not (procedure? T?))
	    (eopl:error 'pair-of
			"Expecting type predicates as right argument, not ~s"
			T?)
	    (lambda (obj)
	      (and (pair? obj)
		   (S? (car obj))
		   (T? (cdr obj))))))))

(define vector-of
  (letrec ((check-all-elems
	    (lambda (T? vec i)
	      (or (< i 0)
		  (and (T? (vector-ref vec i))
		       (check-all-elems T? vec (- i 1)))))))
    (forall (T?)
      (if (not (procedure? T?))
	  (eopl:error 'vector-of
		      "Expecting a type predicate as argument, not ~s"
		      T?)
	  (lambda (obj)
	    (and (vector? obj)
		 (check-all-elems T? obj (- (vector-length obj) 1))))))))

;;; The predicate transformer <- doesn't do anything with its arguments,
;;; but they are used by the -> syntax in the type checker.
;;; See type-check-ignore-types-at-runtime for the -> syntax.
(define <-
  (forall (result-pred . arg-preds)
    (if (not ((list-of procedure?) arg-preds))
	(eopl:error
	 '<-
	 "Expecting a list of type predicates as first argument, not ~s"
	 arg-preds)
	(if (not (procedure? result-pred))
	    (eopl:error
	     '<-
	     "Expecting a type predicate as second argument, not ~s"
	     result-pred)
	    (lambda (obj)
	      (procedure? obj))))))

;;; Type predicate for type predicates
(define type-predicate-for
  (forall (T?)
    (<- boolean? T?)))
  
;;; adapted from EOPL 2e, p. 45 (these are homogeneous lists)
(define list-of
  (forall (T?)
    (if (not (procedure? T?))
	(eopl:error 'list-of
		    "Expecting a type predicate as argument, not ~s"
		    T?)
	(lambda (val)
	  (or (null? val)
	      (and (pair? val)
		   (T? (car val))
		   ((list-of T?) (cdr val))))))))

(define all-of
  (forall (predicate-1 . predicates)
    (if (not (procedure? predicate-1))
	(eopl:error 'all-of
		    "Expecting a type predicate as argument, not ~s"
		    predicate-1)
	(if (not ((list-of procedure?) predicates))
	    (eopl:error 'all-of
			"Expecting type predicate arguments")
	    (lambda (val)
	      (letrec ((test-all
			(lambda (preds)
			  (or (null? preds)
			      (and ((car preds) val)
				   (test-all (cdr preds)))))))
		(test-all (cons predicate-1 predicates))))))))