Copyright	(c) Stijn van Drongelen, 2014
License	MIT
Maintainer	rhymoid@gmail.com
Stability	experimental
Portability	mostly portable (deriving extensions)
Safe Haskell	None
Language	Haskell2010

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

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)
Typeable (* -> * -> *) GCL

data GC stmt guard Source

Guarded commands

Constructors

GC guard [GCL stmt guard]

Instances

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)
Typeable (* -> * -> *) GC

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 box' (U+25A1) symbol, although one might argue that Dijkstra used a 'white vertical rectangle' (U+25AF).

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.