error.mli 5.21 KB
Newer Older
1 2 3 4
(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
5
(*                  Copyright 2008-2018 INRIA                             *)
6
(*                                                                        *)
7
(*  More information on "http://acg.gforge.inria.fr/"                     *)
8 9 10 11 12 13 14 15 16 17 18 19
(*  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           *)
(*                                                                        *)
(**************************************************************************)

20 21 22 23 24 25
(** 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
*)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
26
type lex_error =
27 28
  | Unstarted_comment
  | Unstarted_bracket
29
  | Mismatch_parentheses of char
30 31
  | Unclosed_comment
  | Expect of string
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
32
  | Bad_token
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
33

34 35
(** The type for errors raised by the parser. Names should be explicit
*)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
36
type parse_error =
37
  | Syntax_error of string
38 39 40 41
  | Duplicated_term of string
  | Duplicated_type of string
  | Binder_expected of string
  | Unknown_constant of string
42
  | Not_def_as_infix of string
43 44
  | Unknown_constant_nor_variable of string
  | Unknown_constant_nor_type of string
45 46
  | Unknown_type of string
  | Missing_arg_of_Infix of string
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
47
  | No_such_signature of string
48
  | No_such_lexicon of string
49 50 51 52 53
  | 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
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
54

55
(** The types for errors raised by the typechecker. Names should be
56
    explicit *)
57
type type_error =
58 59 60
  | Already_defined_var of string
  | Not_defined_var of string
  | Not_defined_const of string
Sarah Maarek's avatar
Sarah Maarek committed
61
  | Not_well_typed_term of string * string
Sarah Maarek's avatar
Sarah Maarek committed
62
  | Not_well_typed_term_plus of string * string * string
63
  | Not_well_kinded_type of string
Sarah Maarek's avatar
Sarah Maarek committed
64 65
  | Non_linear_var of string
  | Linear_var of string
66
  | Other
67 68
  | Is_Used of string * string
  | Two_occurrences_of_linear_variable of (Lexing.position * Lexing.position)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
69
  | Non_empty_context of (string*(Lexing.position * Lexing.position)*(Lexing.position * Lexing.position)*string)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
70 71
  | Not_normal
  | Vacuous_abstraction of (string * (Lexing.position * Lexing.position))
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
72

73

74 75 76 77
(** The types for errors raised by lexicons *)
type lexicon_error =
  | Missing_interpretations of (string * string * (string list))

78
(** The types for errors raised by the environment. Names should be
79
    explicit *)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
80
type env_error =
81 82 83 84 85 86
| Duplicated_signature of string
| Duplicated_lexicon of string
| Duplicated_entry of string
    
type version_error =  Outdated_version of (string*string)
    
87
(** The type for errors *)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
88
type error = 
89 90 91 92 93 94 95 96
| 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
    
97
(** The type for warnings *)
98
type warning =
99
  | Variable_or_constant of (string * (Lexing.position * Lexing.position))
100

101
(** The exception that should be raised when an error occur *)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
102 103
exception Error of error

104 105 106
(** [update_loc lexbuf name] update the position informations for the
    lexer *)
val update_loc : Lexing.lexbuf -> string option -> unit
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
107

108 109 110 111 112 113 114 115
(** [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

116 117
(** [error_msg e filename] returns a string describing the error [e]
    while the file [filename] is being processed *)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
118
val error_msg : error -> string -> string
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
119

120 121
(** [dyp_error lexbuf] returns an exception {!Error.Error} so
    that it can be caught in a uniform way. [lexbuf] is
122
    used to set correctly the location information of the parse error *)
123
(* val dyp_error : Lexing.lexbuf -> exn *)
124

125
(** [warnings_to_string filname ws] returns a string describing the
126
    warnings and their location for the file [filename] *)
127
val warnings_to_string : string -> warning list -> string
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
128 129 130 131

(** [get_loc_error e] returns the starting and ending position of an
error *)
val get_loc_error : error -> (Lexing.position * Lexing.position)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
132 133

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