1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
\documentclass{article}
\usepackage{axiom}
\begin{document}
\title{src/algebra void.spad}
\author{Stephen M. Watt}
\maketitle
\begin{abstract}
\end{abstract}
\tableofcontents
\eject
\section{domain VOID Void}
<<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: CoercibleTo OutputForm with
void: () -> % ++ void() produces a void object.
== add
Rep := String
void() == voidValue()$Lisp
coerce(v:%) == coerce(v)$Rep
@
\section{domain EXIT Exit}
<<domain EXIT Exit>>=
import SetCategory
)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}
<<package RESLATC ResolveLatticeCompletion>>=
import Void
import Exit
)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}
<<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.
@
<<*>>=
<<license>>
<<domain VOID Void>>
<<domain EXIT Exit>>
<<package RESLATC ResolveLatticeCompletion>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}
|
