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