Parser (nholz)

Parser Module

Namespace: HOL
Assembly: nholz.dll

This module implements syntax analysis and top-level parsing of type/term quotations into internal types/terms. The syntax analysis functions take a list of lexical tokens as their source, and return a pretype/preterm that gets passed on to type analysis. Lexical analysis is implemented in the 'Lexer' module, and type analsyis (actually common to parsing and printing) is implemented in the 'TypeAnal' module.

Types

Type	Description
'a, 'b infix_elem

Functions and values

Function or value	Description
`(/!) parse_fn msg src` Full Usage: `(/!) parse_fn msg src` Parameters: parse_fn : `'a -> 'b` msg : `string` src : `'a` Returns: `'b`	parse_fn : `'a -> 'b` msg : `string` src : `'a` Returns: `'b`
`parse_fn /\|/! err_fn` Full Usage: `parse_fn /\|/! err_fn` Parameters: parse_fn : `'a -> 'b * 'a` err_fn : `'a -> string` Returns: `'a -> 'b * 'a`	parse_fn : `'a -> 'b * 'a` err_fn : `'a -> string` Returns: `'a -> 'b * 'a`
`build_infix_expr mk_bin_fn ys` Full Usage: `build_infix_expr mk_bin_fn ys` Parameters: mk_bin_fn : `'a * 'b * 'b -> 'b` ys : `('a, 'b)infix_elem list` Returns: `'b * ('a, 'b)infix_elem list`	mk_bin_fn : `'a * 'b * 'b -> 'b` ys : `('a, 'b)infix_elem list` Returns: `'b * ('a, 'b)infix_elem list`
`build_revpolish (form, name_fn) expr0 fexprs` Full Usage: `build_revpolish (form, name_fn) expr0 fexprs` Parameters: form : `string` name_fn : `'a -> string` expr0 : `'b` fexprs : `(('a * 'c * assochand) * 'b) list` Returns: `('a, 'b)infix_elem list`	form : `string` name_fn : `'a -> string` expr0 : `'b` fexprs : `(('a * 'c * assochand) * 'b) list` Returns: `('a, 'b)infix_elem list`
`build_revpolish_step (form, name_fn) (elems, fnhs) (arg5, expr)` Full Usage: `build_revpolish_step (form, name_fn) (elems, fnhs) (arg5, expr)` Parameters: form : `string` name_fn : `'a -> string` elems : `('a, 'b)infix_elem list` fnhs : `('a * 'c * assochand) list` arg4 : `'a * 'c * assochand` expr : `'b` Returns: `('a, 'b)infix_elem list * ('a * 'c * assochand) list`	form : `string` name_fn : `'a -> string` elems : `('a, 'b)infix_elem list` fnhs : `('a * 'c * assochand) list` arg4 : `'a * 'c * assochand` expr : `'b` Returns: `('a, 'b)infix_elem list * ('a * 'c * assochand) list`
`early_resword_err rws item` Full Usage: `early_resword_err rws item` Parameters: rws : `string list` item : `unit -> string` Returns: `token list -> string`	rws : `string list` item : `unit -> string` Returns: `token list -> string`
`end_of_qtn_err items` Full Usage: `end_of_qtn_err items` Parameters: items : `(unit -> string) list` Returns: `token list -> string`	items : `(unit -> string) list` Returns: `token list -> string`
`expand_hol_quotation x` Full Usage: `expand_hol_quotation x` Parameters: x : `string` Returns: `string`	x : `string` Returns: `string`
`hit_const_err eqkwd items` Full Usage: `hit_const_err eqkwd items` Parameters: eqkwd : `bool` items : `(unit -> string) list` Returns: `token list -> string`	eqkwd : `bool` items : `(unit -> string) list` Returns: `token list -> string`
`hit_infix_err items` Full Usage: `hit_infix_err items` Parameters: items : `(unit -> string) list` Returns: `token list -> string`	items : `(unit -> string) list` Returns: `token list -> string`
`hit_numeral_err items` Full Usage: `hit_numeral_err items` Parameters: items : `(unit -> string) list` Returns: `token list -> string`	items : `(unit -> string) list` Returns: `token list -> string`
`hit_prefix_err items` Full Usage: `hit_prefix_err items` Parameters: items : `(unit -> string) list` Returns: `token list -> string`	items : `(unit -> string) list` Returns: `token list -> string`
`hit_resword_err rws context` Full Usage: `hit_resword_err rws context` Parameters: rws : `string list` context : `unit -> string` Returns: `token list -> string`	rws : `string list` context : `unit -> string` Returns: `token list -> string`
`hit_resword_instead_err rws items` Full Usage: `hit_resword_instead_err rws items` Parameters: rws : `string list` items : `(unit -> string) list` Returns: `token list -> string`	rws : `string list` items : `(unit -> string) list` Returns: `token list -> string`
`is_binder_token tok` Full Usage: `is_binder_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_const_token tok` Full Usage: `is_const_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_eqkwd_token tok` Full Usage: `is_eqkwd_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_infix_token tok` Full Usage: `is_infix_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_infix_tyconst_token tok` Full Usage: `is_infix_tyconst_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_nonfix_token tok` Full Usage: `is_nonfix_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_nonfix_tyconst_token tok` Full Usage: `is_nonfix_tyconst_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_nonfix_var_token tok` Full Usage: `is_nonfix_var_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_numeral_token tok` Full Usage: `is_numeral_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_postfix_token tok` Full Usage: `is_postfix_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_prefix_token tok` Full Usage: `is_prefix_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_resword_token tok` Full Usage: `is_resword_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_resword_token_in xs0 tok` Full Usage: `is_resword_token_in xs0 tok` Parameters: xs0 : `string list` tok : `token` Returns: `bool`	xs0 : `string list` tok : `token` Returns: `bool`
`is_resword_token_not_in xs0 tok` Full Usage: `is_resword_token_not_in xs0 tok` Parameters: xs0 : `string list` tok : `token` Returns: `bool`	xs0 : `string list` tok : `token` Returns: `bool`
`is_resword_token_with p tok` Full Usage: `is_resword_token_with p tok` Parameters: p : `string -> bool` tok : `token` Returns: `bool`	p : `string -> bool` tok : `token` Returns: `bool`
`is_tyvar_token tok` Full Usage: `is_tyvar_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`is_var_token tok` Full Usage: `is_var_token tok` Parameters: tok : `token` Returns: `bool`	tok : `token` Returns: `bool`
`leading_term_reswords ()` Full Usage: `leading_term_reswords ()` Parameters: () : `unit` Returns: `string list`	() : `unit` Returns: `string list`
`leading_type_reswords` Full Usage: `leading_type_reswords` Returns: `string list`	Returns: `string list`
`no_close_err (rw1, rw2)` Full Usage: `no_close_err (rw1, rw2)` Parameters: rw1 : `string` rw2 : `string` Returns: `token list -> string`	rw1 : `string` rw2 : `string` Returns: `token list -> string`
`no_close_err0 n (rw1, rw2) src` Full Usage: `no_close_err0 n (rw1, rw2) src` Parameters: n : `int` rw1 : `string` rw2 : `string` src : `token list` Returns: `unit * token list`	n : `int` rw1 : `string` rw2 : `string` src : `token list` Returns: `unit * token list`
`ored items` Full Usage: `ored items` Parameters: items : `(unit -> string) list` Returns: `unit -> string`	items : `(unit -> string) list` Returns: `unit -> string`
`parse_atom_with test_fn src` Full Usage: `parse_atom_with test_fn src` Parameters: test_fn : `token -> bool` src : `token list` Returns: `preterm * token list`	test_fn : `token -> bool` src : `token list` Returns: `preterm * token list`
`parse_end` Full Usage: `parse_end` Returns: `token list -> unit * token list`	Returns: `token list -> unit * token list`
`parse_equals_kwd` Full Usage: `parse_equals_kwd` Returns: `token list -> string * token list`	Returns: `token list -> string * token list`
`parse_infix_expr (form, name_fn) (parse_fn, parse_op_fn, mk_bin_fn) e0 src` Full Usage: `parse_infix_expr (form, name_fn) (parse_fn, parse_op_fn, mk_bin_fn) e0 src` Parameters: form : `string` name_fn : `'a -> string` parse_fn : `token list -> 'b * token list` parse_op_fn : `token list -> ('a * 'c * assochand) * token list` mk_bin_fn : `'a * 'b * 'b -> 'b` e0 : `'b` src : `token list` Returns: `'b * token list`	form : `string` name_fn : `'a -> string` parse_fn : `token list -> 'b * token list` parse_op_fn : `token list -> ('a * 'c * assochand) * token list` mk_bin_fn : `'a * 'b * 'b -> 'b` e0 : `'b` src : `token list` Returns: `'b * token list`
`parse_infix_expr0 (form, name_fn) (parse_fn, parse_op_fn)` Full Usage: `parse_infix_expr0 (form, name_fn) (parse_fn, parse_op_fn)` Parameters: form : `string` name_fn : `'a -> string` parse_fn : `token list -> 'b * token list` parse_op_fn : `token list -> ('a * 'c * 'd) * token list` Returns: `token list -> (('a * 'c * 'd) * 'b) list * token list`	form : `string` name_fn : `'a -> string` parse_fn : `token list -> 'b * token list` parse_op_fn : `token list -> ('a * 'c * 'd) * token list` Returns: `token list -> (('a * 'c * 'd) * 'b) list * token list`
`parse_infix_op` Full Usage: `parse_infix_op` Returns: `token list -> (preterm * int * assochand) * token list`	Returns: `token list -> (preterm * int * assochand) * token list`
`parse_infix_tyconst` Full Usage: `parse_infix_tyconst` Returns: `token list -> (string * int * assochand) * token list`	Returns: `token list -> (string * int * assochand) * token list`
`parse_itemA item rws parse_fn` Full Usage: `parse_itemA item rws parse_fn` Parameters: item : `unit -> string` rws : `string list` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`	item : `unit -> string` rws : `string list` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`
`parse_itemB item parse_fn` Full Usage: `parse_itemB item parse_fn` Parameters: item : `unit -> string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`	item : `unit -> string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`
`parse_itemC item (br1, br2) parse_fn` Full Usage: `parse_itemC item (br1, br2) parse_fn` Parameters: item : `unit -> string` br1 : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`	item : `unit -> string` br1 : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`
`parse_itemD item (br1, sep, br2) parse_fn` Full Usage: `parse_itemD item (br1, sep, br2) parse_fn` Parameters: item : `unit -> string` br1 : `string` sep : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`	item : `unit -> string` br1 : `string` sep : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a * token list`
`parse_list` Full Usage: `parse_list` Returns: `int -> (token list -> 'a * token list) -> token list -> 'a list * token list`	Returns: `int -> (token list -> 'a * token list) -> token list -> 'a list * token list`
`parse_listA item rw parse_fn1` Full Usage: `parse_listA item rw parse_fn1` Parameters: item : `unit -> string` rw : `string` parse_fn1 : `(unit -> string) list -> token list -> 'a * token list` Returns: `token list -> 'a list * token list`	item : `unit -> string` rw : `string` parse_fn1 : `(unit -> string) list -> token list -> 'a * token list` Returns: `token list -> 'a list * token list`
`parse_listD n item (br1, sep, br2) parse_fn` Full Usage: `parse_listD n item (br1, sep, br2) parse_fn` Parameters: n : `int` item : `unit -> string` br1 : `string` sep : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a list * token list`	n : `int` item : `unit -> string` br1 : `string` sep : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a list * token list`
`parse_listD0 n item (br1, sep, br2) parse_fn` Full Usage: `parse_listD0 n item (br1, sep, br2) parse_fn` Parameters: n : `int` item : `unit -> string` br1 : `string` sep : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a list * token list`	n : `int` item : `unit -> string` br1 : `string` sep : `string` br2 : `string` parse_fn : `token list -> 'a * token list` Returns: `token list -> 'a list * token list`
`parse_name_with test_fn` Full Usage: `parse_name_with test_fn` Parameters: test_fn : `token -> bool` Returns: `token list -> string * token list`	test_fn : `token -> bool` Returns: `token list -> string * token list`
`parse_nonfix_tyconst` Full Usage: `parse_nonfix_tyconst` Returns: `token list -> string * token list`	Returns: `token list -> string * token list`
`parse_nonfix_var eqkwd items` Full Usage: `parse_nonfix_var eqkwd items` Parameters: eqkwd : `bool` items : `(unit -> string) list` Returns: `token list -> preterm * token list`	eqkwd : `bool` items : `(unit -> string) list` Returns: `token list -> preterm * token list`
`parse_preterm src` Full Usage: `parse_preterm src` Parameters: src : `token list` Returns: `preterm`	src : `token list` Returns: `preterm`
`parse_preterm0 src` Full Usage: `parse_preterm0 src` Parameters: src : `token list` Returns: `preterm * token list`	src : `token list` Returns: `preterm * token list`
`parse_preterm1 src` Full Usage: `parse_preterm1 src` Parameters: src : `token list` Returns: `preterm * token list`	src : `token list` Returns: `preterm * token list`
`parse_preterm2 src` Full Usage: `parse_preterm2 src` Parameters: src : `token list` Returns: `preterm * token list`	src : `token list` Returns: `preterm * token list`
`parse_preterm3 src` Full Usage: `parse_preterm3 src` Parameters: src : `token list` Returns: `preterm * token list`	src : `token list` Returns: `preterm * token list`
`parse_preterm4 src` Full Usage: `parse_preterm4 src` Parameters: src : `token list` Returns: `preterm * token list`	src : `token list` Returns: `preterm * token list`
`parse_preterm5 src` Full Usage: `parse_preterm5 src` Parameters: src : `token list` Returns: `preterm * token list`	src : `token list` Returns: `preterm * token list`
`parse_pretype src` Full Usage: `parse_pretype src` Parameters: src : `token list` Returns: `pretype`	src : `token list` Returns: `pretype`
`parse_pretype0 src` Full Usage: `parse_pretype0 src` Parameters: src : `token list` Returns: `pretype * token list`	src : `token list` Returns: `pretype * token list`
`parse_pretype1 src` Full Usage: `parse_pretype1 src` Parameters: src : `token list` Returns: `pretype * token list`	src : `token list` Returns: `pretype * token list`
`parse_pretype2 src` Full Usage: `parse_pretype2 src` Parameters: src : `token list` Returns: `pretype * token list`	src : `token list` Returns: `pretype * token list`
`parse_resword x` Full Usage: `parse_resword x` Parameters: x : `string` Returns: `token list -> string * token list`	x : `string` Returns: `token list -> string * token list`
`parse_reswordA rw` Full Usage: `parse_reswordA rw` Parameters: rw : `string` Returns: `token list -> string * token list`	rw : `string` Returns: `token list -> string * token list`
`parse_reswordD (br1, sep, br2) x` Full Usage: `parse_reswordD (br1, sep, br2) x` Parameters: br1 : `string` sep : `string` br2 : `string` x : `string` Returns: `token list -> string * token list`	br1 : `string` sep : `string` br2 : `string` x : `string` Returns: `token list -> string * token list`
`parse_resword_in xs` Full Usage: `parse_resword_in xs` Parameters: xs : `string list` Returns: `token list -> string * token list`	xs : `string list` Returns: `token list -> string * token list`
`parse_resword_not_in xs` Full Usage: `parse_resword_not_in xs` Parameters: xs : `string list` Returns: `token list -> string * token list`	xs : `string list` Returns: `token list -> string * token list`
`parse_start` Full Usage: `parse_start` Returns: `token list -> unit * token list`	Returns: `token list -> unit * token list`
`parse_term x` Full Usage: `parse_term x` Parameters: x : `string` Returns: `term`	This takes a string and parses it into an internal term. The type analysis stage first detypes the preterm before inferring types (in 'resolve_preterm'), since the syntax analysis stage gives all variables and constants the null pretype. Note that type inference is capable of handling overloaded variables. x : `string` Returns: `term`
`parse_type x` Full Usage: `parse_type x` Parameters: x : `string` Returns: `hol_type`	x : `string` Returns: `hol_type`
`skip_space x i` Full Usage: `skip_space x i` Parameters: x : `string` i : `int` Returns: `int`	x : `string` i : `int` Returns: `int`
`string_tail x i` Full Usage: `string_tail x i` Parameters: x : `string` i : `int` Returns: `string`	x : `string` i : `int` Returns: `string`
`syntax_err x` Full Usage: `syntax_err x` Parameters: x : `string` Returns: `'a`	x : `string` Returns: `'a`
`wrong_resword_err rws` Full Usage: `wrong_resword_err rws` Parameters: rws : `string list` Returns: `token list -> string`	rws : `string list` Returns: `token list -> string`