Lexer (nholz)

Lexer Module

Namespace: HOL
Assembly: nholz.dll

This module implements the lexical analysis stage, common to both HOL type and term quotation parsing. The top-level type and term parsers are implemented in the 'Parser' module. The classification of characters, used to determine how lexical tokens are formed, is implemented in the 'Names' module.

Types

Type	Description
token
varmark

Functions and values

Function or value	Description
`(/+) read_fn msg src` Full Usage: `(/+) read_fn msg src` Parameters: read_fn : `'a -> 'b` msg : `string` src : `'a` Returns: `'b`	read_fn : `'a -> 'b` msg : `string` src : `'a` Returns: `'b`
`funcAlphanumeric (dfx, vmrk)` Full Usage: `funcAlphanumeric (dfx, vmrk)` Parameters: dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`	dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`
`funcNumeric (dfx, vmrk)` Full Usage: `funcNumeric (dfx, vmrk)` Parameters: dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`	dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`
`funcPunct (dfx, vmrk)` Full Usage: `funcPunct (dfx, vmrk)` Parameters: dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`	dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`
`funcSymbolic (dfx, vmrk)` Full Usage: `funcSymbolic (dfx, vmrk)` Parameters: dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`	dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`
`lex src` Full Usage: `lex src` Parameters: src : `char list` Returns: `token list`	src : `char list` Returns: `token list`
`lex_char_in` Full Usage: `lex_char_in` Returns: `char list -> char list -> char * char list`	Returns: `char list -> char list -> char * char list`
`lex_char_not_in` Full Usage: `lex_char_not_in` Returns: `char list -> char list -> char * char list`	Returns: `char list -> char list -> char * char list`
`lex_char_with` Full Usage: `lex_char_with` Returns: `(char -> bool) -> char list -> char * char list`	Returns: `(char -> bool) -> char list -> char * char list`
`lex_end` Full Usage: `lex_end` Returns: `char list -> unit * char list`	Returns: `char list -> unit * char list`
`lex_err x` Full Usage: `lex_err x` Parameters: x : `string` Returns: `'a`	x : `string` Returns: `'a`
`lex_list` Full Usage: `lex_list` Returns: `int -> (char list -> 'a * char list) -> char list -> 'a list * char list`	Returns: `int -> (char list -> 'a * char list) -> char list -> 'a list * char list`
`lex_token` Full Usage: `lex_token` Returns: `char list -> token * char list`	Returns: `char list -> token * char list`
`lex_token0 (dfx, vmrk)` Full Usage: `lex_token0 (dfx, vmrk)` Parameters: dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`	dfx : `bool` vmrk : `varmark` Returns: `char list -> token * char list`
`lex_whitespace` Full Usage: `lex_whitespace` Returns: `char list -> char list * char list`	Returns: `char list -> char list * char list`
`token_name tok` Full Usage: `token_name tok` Parameters: tok : `token` Returns: `string`	tok : `token` Returns: `string`