Source file errors.ml

open UtilsLib.Error

module Environment_l =
  struct
    type t =
      | EntryNotFound of string
      | NotALexicon of string
      | NotASignature of string
      | DuplicatedEntry of string
      | Other

    let kind = "ACG"

    let pp fmt = function
      | EntryNotFound e -> Format.fprintf fmt "Entry@ \"%s\"@ not@ found@ in@ current@ environment" e
      | NotALexicon e -> Format.fprintf fmt "Entry@ \"%s\"@ is@ not@ a@ lexicon,@ but@ a@ lexicon@ is@ required" e
      | NotASignature e -> Format.fprintf fmt "Entry@ \"%s\"@ is@ not@ a@ signature,@ but@ a@ signature@ is@ required" e
      | DuplicatedEntry e -> Format.fprintf fmt "Entry@ \"%s\"@ already@ exists@ in@ the@ environment" e
      | Other -> Format.fprintf fmt "Unknown@ error"

    
  end

module EnvironmentErrors = ErrorManager(Environment_l)

module Lexicon_l =
  struct
    type t =
      | MissingInterpretations of string * string * string list
      | BadInterpretationOfMacro of string * string * string
      | NotComposable of string * string * string
      | UnavailableSignature of (string * string * string)
      | NotCompatibleSignature of (string * string * string * string)

    let kind = "Lexicon"

    let pp fmt err =
      match err with
      | MissingInterpretations (lex_name, abs_name, lst) ->
        UtilsLib.Utils.(
          Format.fprintf fmt
            "Lexicon@ \"%a\"@ is@ missing@ the@ interpretations@ of@ \
             the@ following@ terms@ of@ the@ abstract@ signature@ \
             \"%a\":@[<v2>@,@[%a@]@]"
            lex_pp lex_name
            sig_pp abs_name
            (pp_list Format.pp_print_string)
            lst)
      | BadInterpretationOfMacro (lex_name, sig_name, macro_name) ->
        UtilsLib.Utils.(
          Format.fprintf fmt
            "The@ term@ \"%s\"@ is@ not@ a@ constant@ but@ a@ macro@ \
             of@ the@ abstract@ signature@ \"%a\".@ It@ thus@ should@ \
             not@ be@ given@ an@ interpretation@ by@ the@ lexicon@ \
             \"%a\""
            macro_name
            sig_pp sig_name
            lex_pp lex_name)
        | NotComposable (lex_name, l1_name, l2_name) ->
          UtilsLib.Utils.(
            Format.fprintf
              fmt
              "Lexicon@ \"%a\"@ is@ defined@ using@ the@ composition@ \
               \"%a∘%a\".@ However,@ the@ abstract@ vocabulary@ of@ \
               \"%a\"@ is@ not@ the@ same@ as@ the@ object@ \
               vocabulary@ of@ \"%a\""
              lex_pp lex_name
              lex_pp l2_name
              lex_pp l1_name
              lex_pp l2_name
              lex_pp l1_name)
      | UnavailableSignature (lex_name, sig_name, file_name) ->
        UtilsLib.Utils.(
          Format.fprintf
            fmt
            "No@ signature@ \"%a\"@ available@ for@ lexicon@ \"%a\"@ defined@ in@ the@ object@ file@ \"%s\".@ Maybe@ an@ object@ file@ defining@ \"%a\"@ is@ missing"
            sig_pp
            sig_name
            lex_pp
            lex_name
            file_name
            sig_pp
            sig_name)
      | NotCompatibleSignature (lex_name, lex_filename, sig_name, sig_filename) ->
        UtilsLib.Utils.(
          Format.fprintf
            fmt
            "A@ signature@ \"%a\"@ is@ available@ for@ lexicon@ \
             \"%a\"@ defined@ in@ the@ object@ file@ \"%s\".@ \
             However,@ it@ seems@ it@ is@ not@ against@ that@ \
             signature@ (from@ file@ \"%s\",@ or@ possibly@ a@ later@ \
             version)@ that@ lexicon@ \"%a\"@ was@ compiled"
            sig_pp
            sig_name
            lex_pp
            lex_name
            lex_filename
            sig_filename
            lex_pp
            lex_name)
  end

module LexiconErrors = ErrorManager(Lexicon_l)

module Type_l =
  struct
    type t =
      | AlreadyDefinedVar of string
      | NotDefinedVar of string
      | NotDefinedConst of string
      | NotWellTypedTerm of string * string
      | NotWellTypedTermPlus of string * string * string
      | NotWellKindedType of string
      | NonLinearVar of string
      | LinearVar of string
      | IsUsed of string * string
      | TwoOccurrencesOfLinearVariable of UtilsLib.Error.pos
      | NonEmptyContext of string * UtilsLib.Error.pos * UtilsLib.Error.pos * string
      | NotNormal
      | VacuousAbstraction of string * UtilsLib.Error.pos
      | Other

    let kind = "Type"

    let pp fmt err =
      match err with
      | AlreadyDefinedVar s -> Format.fprintf fmt "Var@ \"%s\"@ is@ already@ defined" s
      | NotDefinedVar s -> Format.fprintf fmt "Var@ \"%s\"@ is@ not@ defined" s
      | NotDefinedConst s -> Format.fprintf fmt "Const@ \"%s\"@ is@ not@ defined" s
      | NotWellTypedTerm (s, typ) ->
          Format.fprintf fmt "Term@ \"%s\"@ not@ well@ typed.@;Expected@ type:@ %s" s typ
      | NotWellTypedTermPlus (s, typ, wrong_typ) ->
          Format.fprintf fmt
            "Term@ \"%s\"@ not@ well@ typed.@;\"%s\"@ is@ of@ type@ %s@ but@ is@ here@ used@ with@ type@ %s"
            s s typ wrong_typ
      | NotWellKindedType s -> Format.fprintf fmt "Type@ \"%s\"@ not@ well@ kinded" s
      | NonLinearVar s ->
          Format.fprintf fmt "Var@ \"%s\"@ is@ supposed@ to@ be@ non-linear" s
      | LinearVar s -> Format.fprintf fmt "Var@ \"%s\"@ is@ supposed@ to@ be@ linear" s
      | IsUsed (s1, s2) ->
          Format.fprintf fmt
            "The@ type@ of@ this@ expression@ is@ \"%s\"@ but@ is@ used@ with@ type@ %s" s1 s2
      | TwoOccurrencesOfLinearVariable (s, e) ->
          Format.fprintf fmt "This@ linear@ variable@ was@ already@ used:@ %s"
            (UtilsLib.Error.compute_comment_for_location (s, e))
      | NonEmptyContext (x, (s, e), funct_pos, funct_type) ->
          Format.fprintf fmt
            "This@ term@ contains@ a@ free@ linear@ variable@ \"%s\"@ at@ %s@ and@ is@ \
             argument@ of@ the@ term@ of@ type@ \"%s\"@ at@ %s"
            x
            (UtilsLib.Error.compute_comment_for_location (s, e))
            funct_type
            (UtilsLib.Error.compute_comment_for_location funct_pos)
      | NotNormal -> Format.fprintf fmt "This@ term@ is@ not@ in@ normal@ form"
      | VacuousAbstraction (x, (s, e)) ->
          Format.fprintf fmt
            "This@ linear@ variable@ \"%s\"@ is@ abstracted@ over@ but@ not@ used@ in@ term@ %s"
            x
            (UtilsLib.Error.compute_comment_for_location (s, e))
      | Other -> Format.fprintf fmt "Not@ yet@ implemented"

  end

module TypeErrors = ErrorManager(Type_l)


module Cmd_l =
struct
  type t =
    | TypeMismatch of (Format.formatter -> unit) * (Format.formatter -> unit) * (Format.formatter -> unit) * (Format.formatter -> unit)
                      
  let kind = ""
    
  let pp fmt = function
    | TypeMismatch (obj, abs, inter_abs, lex) ->
      Format.fprintf
        fmt
        "The@ object@ type@ \"%t\"@ is@ not@ the@ interpretation@ of@ the@ abstract@ type@ \"%t\"@ by@ the@ lexicon@ %t@ (type@ \"%t\"@ was@ expected)"
        obj
        abs
        lex
        inter_abs
end

module CmdErrors = ErrorManager(Cmd_l)