This structure defines the command monad for communicating with the
program environment. See structure ComCompose for
sequential composition of commands.
List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Seq
See Void
SIGNATURE Com[data:SORT]
$Date: 2011-09-22 20:53:06 +0200 (Do, 22. Sep 2011) $ ($Revision: 682 $)
SORT data IMPORT Nat ONLY nat
The data type of answers represents all kinds of execution results of
commands. An answer may be either okay, in which case it
holds the computed data of the command, or it may be a fail,
in which case it holds a description of the failure as a denotation.
TYPE ans ==
okay(data: data)
fail(error: denotation)
The data type of commands is opaque to the user. Here, two
fundamental constructors for commands are provided. The
yield function constructs a command which just returns the given
answer. The exit function constructs a command which terminates
program execution with the given code. Many other constructor functions
for commands are defined elsewhere in the OPAL library.
SORT com FUN yield : ans -> com FUN exit : nat -> com
For the frequent occurence of the term yield(okay(Data))
the abbreviation succeed(Data) is provided. The counterpart
for the term yield(fail(Message)) is break(Message).
FUN succeed : data -> com FUN break : denotation -> com
The following function provides a crutch until the initialization of global constants by commands is supported explicitly by the language. It executes the given command (with side-effects!) as a pure function. If command execution returns a failure, program execution is terminated prompting the description of the failure.
This function may only be used as the outermost call of the right-hand-side of a definition of a global constant. Any other use may result in undefined and even nondeterministic behaviour.
When OpalWindows is used, it must not be used at all!
FUN EXEC : com -> data
next node: ComCompose,
prev node: Subsystem Commands,
up to node: Subsystem Commands