From ab8cc85adde879fb963c94d15675783f2cf4b183 Mon Sep 17 00:00:00 2001 From: dos-reis Date: Tue, 14 Aug 2007 05:14:52 +0000 Subject: Initial population. --- src/algebra/void.spad.pamphlet | 145 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 145 insertions(+) create mode 100644 src/algebra/void.spad.pamphlet (limited to 'src/algebra/void.spad.pamphlet') diff --git a/src/algebra/void.spad.pamphlet b/src/algebra/void.spad.pamphlet new file mode 100644 index 00000000..1a27a5fb --- /dev/null +++ b/src/algebra/void.spad.pamphlet @@ -0,0 +1,145 @@ +\documentclass{article} +\usepackage{axiom} +\begin{document} +\title{\$SPAD/src/algebra void.spad} +\author{Stephen M. Watt} +\maketitle +\begin{abstract} +\end{abstract} +\eject +\tableofcontents +\eject +\section{domain VOID Void} +<>= +)abbrev domain VOID Void +-- These types act as the top and bottom of the type lattice +-- and are known to the compiler and interpreter for type resolution. +++ Author: Stephen M. Watt +++ Date Created: 1986 +++ Date Last Updated: May 30, 1991 +++ Basic Operations: +++ Related Domains: ErrorFunctions, ResolveLatticeCompletion, Exit +++ Also See: +++ AMS Classifications: +++ Keywords: type, mode, coerce, no value +++ Examples: +++ References: +++ Description: +++ This type is used when no value is needed, e.g., in the \spad{then} +++ part of a one armed \spad{if}. +++ All values can be coerced to type Void. Once a value has been coerced +++ to Void, it cannot be recovered. + +Void: with + void: () -> % ++ void() produces a void object. + coerce: % -> OutputForm ++ coerce(v) coerces void object to outputForm. + == add + Rep := String + void() == voidValue()$Lisp + coerce(v:%) == coerce(v)$Rep + +@ +\section{domain EXIT Exit} +<>= +)abbrev domain EXIT Exit +++ Author: Stephen M. Watt +++ Date Created: 1986 +++ Date Last Updated: May 30, 1991 +++ Basic Operations: +++ Related Domains: ErrorFunctions, ResolveLatticeCompletion, Void +++ Also See: +++ AMS Classifications: +++ Keywords: exit, throw, error, non-local return +++ Examples: +++ References: +++ Description: +++ A function which does not return directly to its caller should +++ have Exit as its return type. +++ +++ Note: It is convenient to have a formal \spad{coerce} into each type from +++ type Exit. This allows, for example, errors to be raised in +++ one half of a type-balanced \spad{if}. +Exit: SetCategory == add + coerce(n:%) == error "Cannot use an Exit value." + n1 = n2 == error "Cannot use an Exit value." + +@ +\section{package RESLATC ResolveLatticeCompletion} +<>= +)abbrev package RESLATC ResolveLatticeCompletion +++ Author: Stephen M. Watt +++ Date Created: 1986 +++ Date Last Updated: May 30, 1991 +++ Basic Operations: +++ Related Domains: ErrorFunctions, Exit, Void +++ Also See: +++ AMS Classifications: +++ Keywords: mode, resolve, type lattice +++ Examples: +++ References: +++ Description: +++ This package provides coercions for the special types \spadtype{Exit} +++ and \spadtype{Void}. +ResolveLatticeCompletion(S: Type): with + coerce: S -> Void + ++ coerce(s) throws all information about s away. + ++ This coercion allows values of any type to appear + ++ in contexts where they will not be used. + ++ For example, it allows the resolution of different types in + ++ the \spad{then} and \spad{else} branches when an \spad{if} + ++ is in a context where the resulting value is not used. + coerce: Exit -> S + ++ coerce(e) is never really evaluated. This coercion is + ++ used for formal type correctness when a function will not + ++ return directly to its caller. + == add + coerce(s: S): Void == void() + coerce(e: Exit): S == + error "Bug: Should not be able to obtain value of type Exit" + +@ +\section{License} +<>= +--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. +--All rights reserved. +-- +--Redistribution and use in source and binary forms, with or without +--modification, are permitted provided that the following conditions are +--met: +-- +-- - Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- +-- - Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in +-- the documentation and/or other materials provided with the +-- distribution. +-- +-- - Neither the name of The Numerical ALgorithms Group Ltd. nor the +-- names of its contributors may be used to endorse or promote products +-- derived from this software without specific prior written permission. +-- +--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +@ +<<*>>= +<> + +<> +<> +<> +@ +\eject +\begin{thebibliography}{99} +\bibitem{1} nothing +\end{thebibliography} +\end{document} -- cgit v1.2.3