Module AcgData.Error

type lex_error =
| Unstarted_comment
| Unstarted_bracket
| Mismatch_parentheses of char
| Unclosed_comment
| Expect of string
| Bad_token

The type for errors raised by the lexer. Names should be explicit

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 string

The 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

type lexicon_error =
| Missing_interpretations of string * string * string list

The types for errors raised by lexicons

type env_error =
| Duplicated_signature of string
| Duplicated_lexicon of string
| Duplicated_entry of string

The types for errors raised by the environment. Names should be explicit

type version_error =
| Outdated_version of string * string
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 string

The type for errors

type warning =
| Variable_or_constant of string * (Stdlib.Lexing.position * Stdlib.Lexing.position)

The type for warnings

exception Error of error

The exception that should be raised when an error occur

val update_loc : Stdlib.Lexing.lexbuf -> string option -> unit

update_loc lexbuf name update the position informations for the lexer

val set_infix : (string * (Stdlib.Lexing.position * Stdlib.Lexing.position)) -> unit

set_infix sym declares sym as a prefix symbol used in an infix position

val unset_infix : unit -> unit

unset_infix () unset the current use of a prefix symbol used in an infix position

val error_msg : error -> string -> string

error_msg e filename returns a string describing the error e while the file filename is being processed

val warnings_to_string : string -> warning list -> string

warnings_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.position

get_loc_error e returns the starting and ending position of an error

val compute_comment_for_position : Stdlib.Lexing.position -> Stdlib.Lexing.position -> string