This module gives some types and some utilities to mange, emit and display messages
type parse_error = | Syntax_error of string| Duplicated_term of string| Duplicated_type of string| Binder_expected of string| Unknown_constant of string| Not_def_as_infix of string| Unknown_constant_nor_variable of string| Unknown_constant_nor_type of string| Unknown_type of string| Missing_arg_of_Infix of string| No_such_signature of string| No_such_lexicon of string| Not_associative of string| Not_infix of string| Prefix_missing_arg of string| Infix_missing_first_arg of string| Infix_missing_second_arg of stringThe type for errors raised by the parser. Names should be explicit
type type_error = | Already_defined_var of string| Not_defined_var of string| Not_defined_const of string| Not_well_typed_term of string * string| Not_well_typed_term_plus of string * string * string| Not_well_kinded_type of string| Non_linear_var of string| Linear_var of string| Other| Is_Used of string * string| Two_occurrences_of_linear_variable of Stdlib.Lexing.position
* Stdlib.Lexing.position| Non_empty_context of string
* (Stdlib.Lexing.position * Stdlib.Lexing.position)
* (Stdlib.Lexing.position * Stdlib.Lexing.position)
* string| Not_normal| Vacuous_abstraction of string
* (Stdlib.Lexing.position * Stdlib.Lexing.position)The types for errors raised by the typechecker. Names should be explicit
The types for errors raised by lexicons
type error = | Parse_error of parse_error * Stdlib.Lexing.position * Stdlib.Lexing.position| Lexer_error of lex_error * Stdlib.Lexing.position * Stdlib.Lexing.position| Type_error of type_error * Stdlib.Lexing.position * Stdlib.Lexing.position| Env_error of env_error * Stdlib.Lexing.position * Stdlib.Lexing.position| Version_error of version_error| Lexicon_error of lexicon_error
* Stdlib.Lexing.position * Stdlib.Lexing.position| System_error of stringThe type for errors
The type for warnings
exception Error of errorThe exception that should be raised when an error occur
update_loc lexbuf name update the position informations for the lexer
set_infix sym declares sym as a prefix symbol used in an infix position
unset_infix () unset the current use of a prefix symbol used in an infix position
val error_msg : error -> string -> stringerror_msg e filename returns a string describing the error e while the file filename is being processed
dyp_error lexbuf returns an exception Error.Error so that it can be caught in a uniform way. lexbuf is used to set correctly the location information of the parse error
val warnings_to_string : string -> warning list -> stringwarnings_to_string filname ws returns a string describing the warnings and their location for the file filename
val get_loc_error : error -> Stdlib.Lexing.position * Stdlib.Lexing.positionget_loc_error e returns the starting and ending position of an error