sig
type parser_elem =
Token of string
| PTerm of Term.term * Term.isubsts * int
val elem_str : ParseArc.parser_elem -> string
val reset_fresh_count : unit -> unit
type parser_arc = {
sd_n : string;
sd_res : SyntaxDef.sdef_result;
rem_elems : SyntaxDef.syntax_elem list;
parsed_elems : ParseArc.parser_elem list;
spos : int;
endpos : int;
cstrn : Term.isubsts;
}
val create_arc :
SyntaxDef.syntax_def -> string -> int -> ParseArc.parser_arc
val extend_arc_list :
Term.decls_set ->
ParseArc.parser_elem ->
ParseArc.parser_arc list -> ParseArc.parser_arc list
val close_arc :
Term.decls_set ->
ParseArc.parser_arc -> (ParseArc.parser_elem * int) option
val parse_to_array :
Term.decls_set ->
(string * SyntaxDef.syntax_def) list ->
string list -> (ParseArc.parser_elem * int) list array
val parsing_postprocess : ?builtin_sd:bool -> Term.term -> Term.term
val builtin_decls :
unit -> (string * SyntaxDef.syntax_def) list * Term.decls_set
val parse :
Term.decls_set ->
(string * SyntaxDef.syntax_def) list ->
string list -> ParseArc.parser_elem list
val split_input_string : string -> string list
val parse_with_sdefs :
Term.decls_set ->
(string * SyntaxDef.syntax_def) list -> string -> Term.term list
val last_no_parse_message : unit -> string
end