(**************************************************************************) (* *) (* ACG development toolkit *) (* *) (* Copyright 2008-2018 INRIA *) (* *) (* More information on "http://acg.gforge.inria.fr/" *) (* License: CeCILL, see the LICENSE file or "http://www.cecill.info" *) (* Authors: see the AUTHORS file *) (* *) (* *) (* *) (* *) (* $Rev:: $: Revision of last commit *) (* $Author:: $: Author of last commit *) (* $Date:: $: Date of last commit *) (* *) (**************************************************************************) (** This module gives some types and some utilities to mange, emit and display messages *) (** The type for errors raised by the lexer. Names should be explicit *) 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 parser. 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 types for errors raised by the typechecker. 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 (Lexing.position * Lexing.position) | Non_empty_context of (string*(Lexing.position * Lexing.position)*(Lexing.position * Lexing.position)*string) | Not_normal | Vacuous_abstraction of (string * (Lexing.position * Lexing.position)) (** The types for errors raised by lexicons *) type lexicon_error = | Missing_interpretations of (string * string * (string list)) (** The types for errors raised by the environment. Names should be explicit *) type env_error = | Duplicated_signature of string | Duplicated_lexicon of string | Duplicated_entry of string type version_error = Outdated_version of (string*string) (** The type for errors *) type error = | Parse_error of parse_error * (Lexing.position * Lexing.position) | Lexer_error of lex_error * (Lexing.position * Lexing.position) | Type_error of type_error * (Lexing.position * Lexing.position) | Env_error of env_error * (Lexing.position * Lexing.position) | Version_error of version_error | Lexicon_error of lexicon_error * (Lexing.position * Lexing.position) | System_error of string (** The type for warnings *) type warning = | Variable_or_constant of (string * (Lexing.position * Lexing.position)) (** The exception that should be raised when an error occur *) exception Error of error (** [update_loc lexbuf name] update the position informations for the lexer *) val update_loc : Lexing.lexbuf -> string option -> unit (** [set_infix sym] declares sym as a prefix symbol used in an infix position *) val set_infix : string * (Lexing.position * Lexing.position) -> unit (** [unset_infix ()] unset the current use of a prefix symbol used in an infix position *) val unset_infix : unit -> unit (** [error_msg e filename] returns a string describing the error [e] while the file [filename] is being processed *) val error_msg : error -> string -> string (** [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 dyp_error : Lexing.lexbuf -> exn *) (** [warnings_to_string filname ws] returns a string describing the warnings and their location for the file [filename] *) val warnings_to_string : string -> warning list -> string (** [get_loc_error e] returns the starting and ending position of an error *) val get_loc_error : error -> (Lexing.position * Lexing.position) val compute_comment_for_position : Lexing.position -> Lexing.position -> string