;;; $Id: maybe.scm,v 1.13 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.
;;; tagged, discriminated union types
(module maybe (lib "typedscm.ss" "typedscm")
(provide maybe-of make-something make-nothing maybe-something? maybe-nothing?
something->value maybe-test)
(deftype maybe-of
(forall (T)
(-> ((type-predicate-for T)) (type-predicate-for (maybe-of T)))))
(deftype make-something (forall (T) (-> (T) (maybe-of T))))
(deftype make-nothing (forall (T) (-> () (maybe-of T))))
(deftype maybe-something? (forall (T) (-> ((maybe-of T)) boolean)))
(deftype maybe-nothing? (forall (T) (-> ((maybe-of T)) boolean)))
(deftype something->value (forall (T) (-> ((maybe-of T)) T)))
(deftype maybe-test (forall (T U) (-> ((maybe-of T) (-> (T) U) (-> () U)) U)))
(defrep (forall (T) (maybe-of T) (vector-of datum)))
(define *maybe:maybe-tag* (has-type datum 'maybe))
(define maybe-of
(has-type-trusted
(forall (T)
(-> ((type-predicate-for T)) (type-predicate-for (vector-of datum))))
(forall (T?)
(lambda (d)
(and (vector? d)
(<= 2 (vector-length d))
(let ((d-as-vector d))
(and (eq? (vector-ref d-as-vector 0) *maybe:maybe-tag*)
(or (and (eq? (vector-ref d-as-vector 1) 'nothing)
(= (vector-length d) 3))
(and (eq? (vector-ref d-as-vector 1) 'something)
(= (vector-length d) 3)
(T? (vector-ref d-as-vector 2)))))))))))
(define make-something
(lambda (d)
(vector *maybe:maybe-tag* 'something d)))
(define make-nothing
(lambda ()
(vector *maybe:maybe-tag* 'nothing)))
(define maybe-something?
(lambda (o)
(eq? (vector-ref o 1) (has-type datum 'something))))
(define maybe-nothing?
(lambda (o)
(eq? (vector-ref o 1) (has-type datum 'nothing))))
(define something->value
(lambda (o)
(if (maybe-something? o)
(vector-ref o 2)
(error "something->value passed nothing"))))
(define maybe-test
(lambda (o something-fun nothing-fun)
(if (maybe-something? o)
(something-fun (vector-ref o 2))
(nothing-fun))))
) ; end module