Error Handling for Parsing and Validation

This file implements error handling for the parsers and the validator.

inductive Validator.IndexType : Type

• Action : IndexType
• ActionSet : IndexType
• StateSet : IndexType
• Knowledge : IndexType
• Bdd : IndexType

@[implicit_reducible]

instance Validator.instToStringIndexType : ToString IndexType

Equations

• One or more equations did not get rendered due to their size.

inductive Validator.Error : Type

The type of errors used in the certificate parser and checker.

• invalidId (T : IndexType) (Eᵢ : ℕ) : Error

  The certificate is invalid because there is no identifier Eᵢ for type T.

• invalidIds (T : IndexType) (ids : List ℕ) : Error

  The certificate is invalid because the given identifers are invalid for type T.

• unexpectedId (T : IndexType) (expected found : ℕ) : Error

  The certificate is invalid because some id in the certificat did not match the expected id.

• unexpected (T : IndexType) (Eᵢ : ℕ) (expected found : String) : Error

  The certificate is invalid because the expression with Eᵢ was used when an expression with a different format was expected.

• notSubset (T : IndexType) (E1ᵢ E2ᵢ : ℕ) : Error
• unsupportedB4 (R R' : StateSetFormalism) : Error
• noUnsolvability : Error
• bddError (path : System.FilePath) (e : IO.Error) : Error

  An error occured while parsing the given bdd file.

• parseUnexpected (s : String) (pos : String.Pos.Raw) : Error

  An unexpected character was found at the given position while parsing the string s.

• addMessage (e : Error) (pos : Option (String × String.Pos.Raw)) (msg : String) : Error

  Add an error message to the error e, with the possibility of specifiying the position in case of a parsing error.

@[implicit_reducible]

instance Validator.Error.instErrorSliceChar : Parser.Error Error String.Slice Char

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.Error.instToFormat : Std.ToFormat Error

Equations

• Validator.Error.instToFormat = { format := Validator.Error.format✝ }

@[reducible, inline]

abbrev Validator.Result (α : Type u) (p : α → Prop) : Type u

Equations

• Validator.Result α p = Except Validator.Error { a : α // p a }

@[reducible, inline]

abbrev Validator.ResultProp (p : Prop) : Type

Equations

• Validator.ResultProp p = Validator.Result Unit fun (x : Unit) => p

def Validator.withErrorMessage {α : Type u_1} {p : α → Prop} : Option String → Result α p → Result α p

Equations

• Validator.withErrorMessage none x✝ = x✝
• Validator.withErrorMessage (some msg) x✝ = tryCatch x✝ fun (e : Validator.Error) => throw (e.addMessage none msg)