;;; $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