ComCheck

The structure ComCheck defines several command monad combinators which deal with failures.

Signature of ComCheck

List of Import References :
See BOOL
See Com
See DENOTATION
See Nat
See Option
See Seq
See Void

SIGNATURE ComCheck[data]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

SORT data

IMPORT  Void            ONLY void
        Com[void]       ONLY com
        Com[data]       ONLY com

Com1 | Com2 executes Com1. If Com1 fails, Com2 is executed, otherwise the answer of Com1 is yielded. Com1 breaks Com2 is an alternative notation for Com2 | Com1.

FUN |           : com[data] ** com[data] -> com[data]
FUN breaks      : com[data] ** com[data] -> com[data]

section(Enter, Exit, Com) ensures that the execution of Com is surrounded by the execution of Enter and Exit. It first executes Enter. If Enter succeeds Com is executed. Afterwards Exit is executed, independent of the result of Com. The answer is either the failure of Enter, or, if there wasn't any, the failure of Com, or, if there wasn't any, the failure of Exit, or finally, if no failure at all occured, the success of Com.

section(Enter, Exit, Com) == 
    Enter & (Com ; (\\Ans. IF okay?(Ans) THEN Exit & yield(Ans)
					 ELSE Exit ; yield(Ans) FI))

FUN section: com[void] ** com[void] ** com[data] -> com[data]

Aug check Com executes the given command Com. If Com fails, the error description of the failure is augmented by Aug (which usually is just the identity \\X.X), the result together with the program name is printed to stdErr, and program execution is terminated with result code 1. Otherwise the answer is yielded.

FUN check : (denotation -> denotation) ** com[data] -> com[data]

next node: ComMap,
prev node: ComAction,
up to node: Subsystem Commands