Errors

Cvc.Error is what every failing operation of this library throws, Res/ResT the result types carrying one, and throwUser and friends the ways to throw one.

inductive Cvc.Error : Type

The error type of this library.

• internal (msg : String) : Error

  A failure inside this library.

• unsupported (msg : String) : Error

  Unsupported feature.

• user (msg : String) : Error

  A misuse of the library or of cvc5, including every error cvc5 reports.

• io (msg : String) : Error

  Input/output error.

@[instance_reducible]

instance Cvc.instInhabitedError : Inhabited Error

Equations

• Cvc.instInhabitedError = { default := Cvc.instInhabitedError.default }

def Cvc.Error.mapMsg (f : String → String) : Error → Error

Maps over an error's message.

Equations

• Cvc.Error.mapMsg f (Cvc.Error.internal msg) = Cvc.Error.internal (f msg)
• Cvc.Error.mapMsg f (Cvc.Error.unsupported msg) = Cvc.Error.unsupported (f msg)
• Cvc.Error.mapMsg f (Cvc.Error.user msg) = Cvc.Error.user (f msg)
• Cvc.Error.mapMsg f (Cvc.Error.io msg) = Cvc.Error.io (f msg)

def Cvc.Error.append (self : Error) (txt : String) (newline : Bool := true) : Error

Appends some text to an error's internal message.

Equations

• self.append txt newline = Cvc.Error.mapMsg (fun (x : String) => x ++ if newline = true then "\n" ++ txt else txt) self

def Cvc.Error.toString : Error → String

String representation.

Equations

• (Cvc.Error.user msg).toString = msg
• (Cvc.Error.internal msg).toString = toString "[internal] " ++ toString msg
• (Cvc.Error.unsupported msg).toString = toString "[unsupported] " ++ toString msg
• (Cvc.Error.io msg).toString = toString "[io] " ++ toString msg

@[instance_reducible]

instance Cvc.Error.instToString : ToString Error

Equations

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

def Cvc.Error.throwUser {m : Type u_1 → Type u_2} [MonadExcept Error m] (msg : String) {α : Type u_1} : m α

Throws an Error.user.

Equations

• Cvc.throwUser msg = throw (Cvc.Error.user msg)

def Cvc.Error.someOrThrowUser {m : Type u_1 → Type u_2} [Monad m] [MonadExcept Error m] (msg : String) {α : Type u_1} : Option α → m α

Unwraps an Option, throwing an Error.user on none.

Equations

• Cvc.someOrThrowUser msg (some a) = pure a
• Cvc.someOrThrowUser msg none = Cvc.throwUser msg

def Cvc.Error.throwInternal {m : Type u_1 → Type u_2} [MonadExcept Error m] (msg : String) {α : Type u_1} : m α

Throws an Error.internal.

Equations

• Cvc.throwInternal msg = throw (Cvc.Error.internal msg)

def Cvc.Error.throwTodo {m : Type u_1 → Type u_2} [MonadExcept Error m] (msg : String) {α : Type u_1} : m α

Throws an Error.internal with an unsupported-feature message.

Equations

• Cvc.throwTodo msg = throw (Cvc.Error.internal (toString "[unsupported] " ++ toString msg))

def Cvc.Error.throwUnreachable {m : Type u_1 → Type u_2} [MonadExcept Error m] {α : Type u_1} (msg : String := "") : m α

Throws an Error.internal reporting that unreachable code was reached.

Equations

• Cvc.throwUnreachable msg = throw (Cvc.Error.internal (toString "reached unreachable code" ++ toString (if msg.isEmpty = true then "" else ": ") ++ toString msg))

def Cvc.Error.throwIO {m : Type u_1 → Type u_2} [MonadExcept Error m] {α : Type u_1} (e : IO.Error) : m α

Throws an Error.io.

Equations

• Cvc.throwIO e = throw (Cvc.Error.io (toString e))

def Cvc.Error.explainError {m : Type u_1 → Type u_2} [MonadExcept Error m] {α : Type u_1} (code : m α) (explain : Unit → Option String) : m α

code, failing with the user error explain gives, if it gives one, when code fails.

Equations

• Cvc.explainError code explain = tryCatch code fun (e : Cvc.Error) => match explain () with | some msg => throw (Cvc.Error.user msg) | none => throw e

def Cvc.errorContext {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Error m] (s : Unit → String) (code : m α) : m α

Sets an error context as a lazy string to newline-append after code's error, if any.

Equations

• Cvc.errorContext s code = tryCatch code fun (e : Cvc.Error) => throw (Cvc.Error.mapMsg (fun (x : String) => toString x ++ toString "\n" ++ toString (s ())) e)

@[reducible, inline]

abbrev Cvc.ResT (m : Type → Type) (α : Type) : Type

Error-result monad transformer.

Equations

• Cvc.ResT m α = ExceptT Cvc.Error m α

@[reducible, inline]

abbrev Cvc.Res (α : Type) : Type

Error monad.

Equations

• Cvc.Res α = Cvc.ResT Id α

@[reducible, inline]

abbrev Cvc.Res.ok {α : Type} (a : α) : Res α

A success value of type α

Equations

• Cvc.Res.ok a = pure a

@[reducible, inline]

abbrev Cvc.Res.error {α : Type} (e : Error) : Res α

A failure value of type ε

Equations

• Cvc.Res.error e = throw e

@[instance_reducible]

instance Cvc.Res.instMonadLiftResTOfMonad {m : Type → Type} [Monad m] : MonadLift Res (ResT m)

Equations

• Cvc.Res.instMonadLiftResTOfMonad = { monadLift := fun {α : Type} (x : Cvc.Res α) => match x with | Except.ok a => pure a | Except.error e => throw e }