;;; $Id: relax-type-checking.scm,v 1.2 2006/01/30 03:13:29 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.
;;;
;;; The procedures in this module are useful for making the type checker
;;; shut up when you know what you are doing.  Use them wisely.

(module relax-type-checking (lib "typedscm.ss" "typedscm")

  (provide ignore true? make-pair pair-first pair-second)
  
  (deftype ignore (-> (datum) void))
  (deftype true? (-> (datum) boolean))
  (deftype make-pair (forall (S T) (-> (S T) (pair-of S T))))
  (deftype pair-first (forall (S T) (-> ((pair-of S T)) S)))
  (deftype pair-second (forall (S T) (-> ((pair-of S T)) T)))

  ;; Ignore applied to an expression makes the type checker shut up
  ;; about that expression not being of type void.  This is useful
  ;; when you are using a value as a statement that you know you are
  ;; ignoring.
  (define ignore
    (lambda (x) (void)))

  ;; True? applied to an expression makes the type checker shut
  ;; up about that expression not being of type boolean.  This is
  ;; useful when you are using a value in a context where anything but
  ;; #f counts as true, as in Scheme if-expressions.
  (define true?
    (lambda (x)
      (has-type-trusted boolean x)))

    ;; Let the type checker know you are making a pair, not a list...
  (define make-pair
    (has-type-trusted
      (forall (S T) (-> (S T) (pair-of S T)))
      (lambda (x y)
	(cons x y))))

  ;; Let the type checker know you are working on a pair, not a list
  (define pair-first
    (has-type-trusted
      (forall (S T) (-> ((pair-of S T)) S))
      (lambda (x)
	(car x))))

  ;; Let the type checker know you are working on a pair, not a list
  (define pair-second
    (has-type-trusted
      (forall (S T) (-> ((pair-of S T)) T))
      (lambda (x)
	(cdr x))))

) ;; end module