Module ParseArc

module ParseArc: sig .. end

Contains the bottom-up chart-based parser that uses syntax definitions and checks if terms are well-typed when closing arcs. *

type parser_elem =

`\|`	`Token of string`
`\|`	`PTerm of Term.term * Term.isubsts * int`	`(*`	From `parsed_elems`, `cstrn` and `endpos` of `ParseArc.parser_arc`.	`*)`

The type of elements created during parsing. Tokens come just from lexer and terms are created during parsing. term does not have substitution applied.

val elem_str : parser_elem -> string

Print a parser elem.

val reset_fresh_count : unit -> unit

Reset the variable suffix count.

type parser_arc = {

`sd_n :string;`	`(*`	The parsed definition's unique name.	`*)`
`sd_res :SyntaxDef.sdef_result;`	`(*`	Its supertypes and whether it's a variable.	`*)`
`rem_elems :SyntaxDef.syntax_elem list;`	`(*`	Its remaining elements.	`*)`
`parsed_elems :parser_elem list;`	`(*`	Useful elements parsed so far in rev. order (all will be arguments).	`*)`
`spos :int;`	`(*`	Start position of the arc.	`*)`
`endpos :int;`	`(*`	The current end position of the arc.	`*)`
`cstrn :Term.isubsts;`	`(*`	Constraint for the arc.	`*)`

}

Incomplete arcs that appear during parsing. parsed_elems do not have cstrn applied.

Parsing, done by adding arcs

val create_arc : SyntaxDef.syntax_def -> string -> int -> parser_arc

val extend_arc_list : Term.decls_set ->
       parser_elem -> parser_arc list -> parser_arc list

Extends all the arcs in the given list that can be extended and removes all other arcs.

val close_arc : Term.decls_set -> parser_arc -> (parser_elem * int) option

Closes an arc when it is completed: returns the corresponding term parser element together with the starting position of the arc.

val parse_to_array : Term.decls_set ->
       (string * SyntaxDef.syntax_def) list ->
       string list -> (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 -> 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