Error Handling for Parsing and Validation

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

def Validator.countLines {s : String} (pos : s.Pos) : ℕ

Equations

• Validator.countLines pos = String.Slice.foldl (fun (n : ℕ) (d : Char) => if d = '\n' then n + 1 else n) 0 (s.sliceTo pos)

def Validator.positionInfo (s : String.Slice) : ℕ × ℕ × String

Equations

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

inductive Validator.Error : Type

• parseUnexpected : String.Slice → Error
• unvalid : String → Error
• addMessage : Error → Option String.Slice → String → Error

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

Equations

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

def Validator.Error.toString : Error → String

Equations

• One or more equations did not get rendered due to their size.
• (Validator.Error.unvalid msg).toString = toString " " ++ toString msg ++ toString "\n"
• (e.addMessage none msg).toString = toString " " ++ toString msg ++ toString "\n" ++ e.toString

instance Validator.Error.instToString : ToString Error

Equations

• Validator.Error.instToString = { toString := Validator.Error.toString }

@[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.Result' (p : Prop) : Type

Equations

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

def Validator.throwUnvalid (msg : String) {α : Type u_1} {p : α → Prop} : Result α p

Equations

• Validator.throwUnvalid msg = throw (Validator.Error.unvalid msg)

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)