Portability	mostly portable (deriving extensions)
Stability	experimental
Maintainer	rhymoid@gmail.com
Safe Haskell	Safe-Inferred

Language.GuardedCommands

Contents

Abstract syntax
Parsing

Description

A language with guarded commands, heavily based on:

Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (August 1975), 453–457. DOI=10.1145/360933.360975

With regards to the above source, the following assumptions were made:

Guarded command sets may be empty, and __skip__ and __abort__ are keywords.
The __while__ guard __do__ stmts... __od__ notation used on page 457 is allowed and is syntactic sugar for __do__ guard __→__stmts... __od__.

Furthermore, the language is extended so that the blocks denoted by __do__ ... __od__ may be preceded by zero or more loop invariants (written: __invariant__ guard).

Synopsis

Abstract syntax

data GCL stmt guard Source

Guarded statements

Constructors

Alternative [GC stmt guard]	Alternative statement. If none of the guards is true, the command diverges; otherwise, an arbitrary guarded list with a true guard is executed.
Repetitive [guard] [GC stmt guard]	Repetitive statement. If none of the guards is true, the command terminates; otherwise, an arbitrary guarded list with a true guard is executed (the 'iteration'), after which the entire repetitive statement is executed again. Before and after every iteration, all loop invariants must hold.
Statement stmt	Some user-defined statement.

Instances

Typeable2 GCL
Bifunctor GCL
Functor (GCL stmt)
Foldable (GCL stmt)
Traversable (GCL stmt)
(Eq stmt, Eq guard) => Eq (GCL stmt guard)
(Data stmt, Data guard) => Data (GCL stmt guard)
(Show stmt, Show guard) => Show (GCL stmt guard)

data GC stmt guard Source

Guarded commands

Constructors

GC guard [GCL stmt guard]

Instances

Typeable2 GC
Bifunctor GC
Functor (GC stmt)
Foldable (GC stmt)
Traversable (GC stmt)
(Eq stmt, Eq guard) => Eq (GC stmt guard)
(Data stmt, Data guard) => Data (GC stmt guard)
(Show stmt, Show guard) => Show (GC stmt guard)

Parsing

Parsers based on the TokenParsing class.

By overriding token appropriately, the keywords (words "⫾ → if fi do od abort skip invariant while ") may take on different forms or even be forbidden.

pGCL :: TokenParsing m => m stmt -> m guard -> m (GCL stmt guard)Source

Parse a guarded statement, given parsers for user-defined statments and for guards.

pGuardedCommandSet :: TokenParsing m => m guard -> m (GCL stmt guard) -> m [GC stmt guard]Source

Parse a guarded command set, given parsers for guards and guarded statements.

The guarded commands are separated by a 'white vertical bar' (U+2AFE) symbol, a.k.a. 'Dijkstra choice'.

pGuardedCommand :: TokenParsing m => m guard -> m (GCL stmt guard) -> m (GC stmt guard)Source

Parse a guarded command, given parsers for guards and guarded statements.

The guard and the guarded list are separated by a 'rightwards arrow' (U+2192) symbol.

pGuardedList :: TokenParsing m => m (GCL stmt guard) -> m [GCL stmt guard]Source

Parse a guarded list, given a parser for guarded statements.

The guarded statements are separated by a semicolon. This function is equal to a type-restricted semiSep1.