package acgtk

  1. Overview
  2. Docs

This module gives some types and some utilities to mange, emit and display messages

type lex_error =
  1. | Unstarted_comment
  2. | Unstarted_bracket
  3. | Mismatch_parentheses of char
  4. | Unclosed_comment
  5. | Expect of string
  6. | Bad_token

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

type parse_error =
  1. | Syntax_error of string
  2. | Duplicated_term of string
  3. | Duplicated_type of string
  4. | Binder_expected of string
  5. | Unknown_constant of string
  6. | Not_def_as_infix of string
  7. | Unknown_constant_nor_variable of string
  8. | Unknown_constant_nor_type of string
  9. | Unknown_type of string
  10. | Missing_arg_of_Infix of string
  11. | No_such_signature of string
  12. | No_such_lexicon of string
  13. | Not_associative of string
  14. | Not_infix of string
  15. | Prefix_missing_arg of string
  16. | Infix_missing_first_arg of string
  17. | Infix_missing_second_arg of string

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

type type_error =
  1. | Already_defined_var of string
  2. | Not_defined_var of string
  3. | Not_defined_const of string
  4. | Not_well_typed_term of string * string
  5. | Not_well_typed_term_plus of string * string * string
  6. | Not_well_kinded_type of string
  7. | Non_linear_var of string
  8. | Linear_var of string
  9. | Other
  10. | Is_Used of string * string
  11. | Two_occurrences_of_linear_variable of Stdlib.Lexing.position * Stdlib.Lexing.position
  12. | Non_empty_context of string * (Stdlib.Lexing.position * Stdlib.Lexing.position) * (Stdlib.Lexing.position * Stdlib.Lexing.position) * string
  13. | Not_normal
  14. | 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 =
  1. | Missing_interpretations of string * string * string list

The types for errors raised by lexicons

type env_error =
  1. | Duplicated_signature of string
  2. | Duplicated_lexicon of string
  3. | Duplicated_entry of string

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

type version_error =
  1. | Outdated_version of string * string
type error =
  1. | Parse_error of parse_error * Stdlib.Lexing.position * Stdlib.Lexing.position
  2. | Lexer_error of lex_error * Stdlib.Lexing.position * Stdlib.Lexing.position
  3. | Type_error of type_error * Stdlib.Lexing.position * Stdlib.Lexing.position
  4. | Env_error of env_error * Stdlib.Lexing.position * Stdlib.Lexing.position
  5. | Version_error of version_error
  6. | Lexicon_error of lexicon_error * Stdlib.Lexing.position * Stdlib.Lexing.position
  7. | System_error of string

The type for errors

type warning =
  1. | 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 get_string_error : error -> string * (Stdlib.Lexing.position * Stdlib.Lexing.position)

get_string_error e returns the string describing the error and its position

val change_loc : error -> (Stdlib.Lexing.position * Stdlib.Lexing.position) -> error
val compute_comment_for_position : Stdlib.Lexing.position -> Stdlib.Lexing.position -> string