Reader (nholz)

Reader Module

Namespace: HOL
Assembly: nholz.dll

This module provides library support for generic reader functions that process data from a given source and return a read item and the source correspondingly advanced, ready for the next item to be read. This gets used in the HOL quotation lexer and parsers (see 'Lexer' and 'Parser' modules respectively).

Types

Type	Description
ReadFail	This exception is dedicated to non-fatal failures in reader functions, and is used for simple control flow between reader connectives. This allows simple implementation of reader connectives that trap non-fatal failures and act accordingly, whilst allowing other exceptions to propagate.

Functions and values

Function or value	Description
`(>>) read_fn1 read_fn2 src` Full Usage: `(>>) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b * 'a` read_fn2 : `'a -> 'c * 'a` src : `'a` Returns: `'c * 'a`	read_fn1 : `'a -> 'b * 'a` read_fn2 : `'a -> 'c * 'a` src : `'a` Returns: `'c * 'a`
`(@>) read_fn1 read_fn2 src` Full Usage: `(@>) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b * 'a` read_fn2 : `'b -> 'a -> 'c * 'a` src : `'a` Returns: `'c * 'a`	read_fn1 : `'a -> 'b * 'a` read_fn2 : `'b -> 'a -> 'c * 'a` src : `'a` Returns: `'c * 'a`
`(>>) read_fn1 read_fn2 src` Full Usage: `(>>) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b * 'a` read_fn2 : `'a -> 'd * 'a` src : `'a` Returns: `'b * 'a`	read_fn1 : `'a -> 'b * 'a` read_fn2 : `'a -> 'd * 'a` src : `'a` Returns: `'b * 'a`
`(!>>>) read_fn1 read_fn2 src` Full Usage: `(!>>>) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b * 'a` read_fn2 : `'a -> 'c * 'a` src : `'a` Returns: `('b * 'c) * 'a`	The first reader function reads an initial part, and the second reader function reads the next part, with a ReadFail raised if either reader raises one. The '>>>' connective returns the combined results as a pair read_fn1 : `'a -> 'b * 'a` read_fn2 : `'a -> 'c * 'a` src : `'a` Returns: `('b * 'c) * 'a`
`(!\|\|\|) read_fn1 read_fn2 src` Full Usage: `(!\|\|\|) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b` read_fn2 : `'a -> 'b` src : `'a` Returns: `'b`	This is for alternation. The first reader function is tried, and if this produces a ReadFail then the second reader function is tried from the same starting point. read_fn1 : `'a -> 'b` read_fn2 : `'a -> 'b` src : `'a` Returns: `'b`
`(>@>) read_fn1 read_fn2 src` Full Usage: `(>@>) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b * 'a` read_fn2 : `'b -> 'a -> 'c * 'a` src : `'a` Returns: `('b * 'c) * 'a`	read_fn1 : `'a -> 'b * 'a` read_fn2 : `'b -> 'a -> 'c * 'a` src : `'a` Returns: `('b * 'c) * 'a`
`(@!\|) f read_fn src` Full Usage: `(@!\|) f read_fn src` Parameters: f : `'b -> 'c` read_fn : `'a -> 'b * 'a` src : `'a` Returns: `'c`	These functions are for performing post-processing on the result of a reader function. The LHS is a function that produces a string to get raised as an error message if the RHS succeeds. f : `'b -> 'c` read_fn : `'a -> 'b * 'a` src : `'a` Returns: `'c`
`(@\|) f read_fn src` Full Usage: `(@\|) f read_fn src` Parameters: f : `'b -> 'c` read_fn : `'a -> 'b * 'a` src : `'a` Returns: `'c * 'a`	Thise functions is for performing post-processing on the result of a reader function. The LHS is a function that reformulates the result of the RHS. f : `'b -> 'c` read_fn : `'a -> 'b * 'a` src : `'a` Returns: `'c * 'a`
`(\|@\|) read_fn1 read_fn2 src` Full Usage: `(\|@\|) read_fn1 read_fn2 src` Parameters: read_fn1 : `'a -> 'b * 'a` read_fn2 : `'b -> 'a -> 'b * 'a` src : `'a` Returns: `'b * 'a`	read_fn1 : `'a -> 'b * 'a` read_fn2 : `'b -> 'a -> 'b * 'a` src : `'a` Returns: `'b * 'a`
`lookahead read_fn src` Full Usage: `lookahead read_fn src` Parameters: read_fn : `'a -> 'b * 'a` src : `'a` Returns: `'b * 'a`	read_fn : `'a -> 'b * 'a` src : `'a` Returns: `'b * 'a`
`read_elem src` Full Usage: `read_elem src` Parameters: src : `'a list` Returns: `'a * 'a list`	src : `'a list` Returns: `'a * 'a list`
`read_elem_in es src` Full Usage: `read_elem_in es src` Parameters: es : `'a list` src : `'a list` Returns: `'a * 'a list`	es : `'a list` src : `'a list` Returns: `'a * 'a list`
`read_elem_not_in es src` Full Usage: `read_elem_not_in es src` Parameters: es : `'a list` src : `'a list` Returns: `'a * 'a list`	es : `'a list` src : `'a list` Returns: `'a * 'a list`
`read_elem_with test_fn src` Full Usage: `read_elem_with test_fn src` Parameters: test_fn : `'a -> bool` src : `'a list` Returns: `'a * 'a list`	test_fn : `'a -> bool` src : `'a list` Returns: `'a * 'a list`
`read_end src` Full Usage: `read_end src` Parameters: src : `'a list` Returns: `unit * 'a list`	src : `'a list` Returns: `unit * 'a list`
`read_list n read_fn src` Full Usage: `read_list n read_fn src` Parameters: n : `int` read_fn : `'b -> 'c * 'b` src : `'b` Returns: `'c list * 'b`	n : `int` read_fn : `'b -> 'c * 'b` src : `'b` Returns: `'c list * 'b`
`read_start src` Full Usage: `read_start src` Parameters: src : `'a list` Returns: `unit * 'a list`	src : `'a list` Returns: `unit * 'a list`
`read_with (read_fn, test_fn) src` Full Usage: `read_with (read_fn, test_fn) src` Parameters: read_fn : `'a -> 'b * 'a` test_fn : `'b -> bool` src : `'a` Returns: `'b * 'a`	read_fn : `'a -> 'b * 'a` test_fn : `'b -> bool` src : `'a` Returns: `'b * 'a`