Documentation

Init.System.IOError

inductive IO.Error :

Type

alreadyExists: Option String → UInt32 → String → IO.Error
otherError: UInt32 → String → IO.Error
resourceBusy: UInt32 → String → IO.Error
resourceVanished: UInt32 → String → IO.Error
unsupportedOperation: UInt32 → String → IO.Error
hardwareFault: UInt32 → String → IO.Error
unsatisfiedConstraints: UInt32 → String → IO.Error
illegalOperation: UInt32 → String → IO.Error
protocolError: UInt32 → String → IO.Error
timeExpired: UInt32 → String → IO.Error
interrupted: String → UInt32 → String → IO.Error
noFileOrDirectory: String → UInt32 → String → IO.Error
invalidArgument: Option String → UInt32 → String → IO.Error
permissionDenied: Option String → UInt32 → String → IO.Error
resourceExhausted: Option String → UInt32 → String → IO.Error
inappropriateType: Option String → UInt32 → String → IO.Error
noSuchThing: Option String → UInt32 → String → IO.Error
unexpectedEof: IO.Error
userError: String → IO.Error

instance IO.instInhabitedError :

Inhabited IO.Error

Equations

IO.instInhabitedError = { default := IO.Error.alreadyExists default default default }

def IO.userError (s : String) :

Equations

IO.userError s = IO.Error.userError s

instance instCoeStringError :

Coe String IO.Error

Equations

instCoeStringError = { coe := IO.userError }

def IO.Error.mkAlreadyExistsFile :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkAlreadyExistsFile = IO.Error.alreadyExists ∘ some

def IO.Error.mkEofError :

Unit → IO.Error

Equations

IO.Error.mkEofError x = IO.Error.unexpectedEof

def IO.Error.mkInappropriateTypeFile :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkInappropriateTypeFile = IO.Error.inappropriateType ∘ some

def IO.Error.mkInterrupted :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkInterrupted = IO.Error.interrupted

def IO.Error.mkInvalidArgumentFile :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkInvalidArgumentFile = IO.Error.invalidArgument ∘ some

def IO.Error.mkNoFileOrDirectory :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkNoFileOrDirectory = IO.Error.noFileOrDirectory

def IO.Error.mkNoSuchThingFile :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkNoSuchThingFile = IO.Error.noSuchThing ∘ some

def IO.Error.mkPermissionDeniedFile :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkPermissionDeniedFile = IO.Error.permissionDenied ∘ some

def IO.Error.mkResourceExhaustedFile :

String → UInt32 → String → IO.Error

Equations

IO.Error.mkResourceExhaustedFile = IO.Error.resourceExhausted ∘ some

def IO.Error.mkUnsupportedOperation :

UInt32 → String → IO.Error

Equations

IO.Error.mkUnsupportedOperation = IO.Error.unsupportedOperation

def IO.Error.mkResourceExhausted :

UInt32 → String → IO.Error

Equations

IO.Error.mkResourceExhausted = IO.Error.resourceExhausted none

def IO.Error.mkAlreadyExists :

UInt32 → String → IO.Error

Equations

IO.Error.mkAlreadyExists = IO.Error.alreadyExists none

def IO.Error.mkInappropriateType :

UInt32 → String → IO.Error

Equations

IO.Error.mkInappropriateType = IO.Error.inappropriateType none

def IO.Error.mkNoSuchThing :

UInt32 → String → IO.Error

Equations

IO.Error.mkNoSuchThing = IO.Error.noSuchThing none

def IO.Error.mkResourceVanished :

UInt32 → String → IO.Error

Equations

IO.Error.mkResourceVanished = IO.Error.resourceVanished

def IO.Error.mkResourceBusy :

UInt32 → String → IO.Error

Equations

IO.Error.mkResourceBusy = IO.Error.resourceBusy

def IO.Error.mkInvalidArgument :

UInt32 → String → IO.Error

Equations

IO.Error.mkInvalidArgument = IO.Error.invalidArgument none

def IO.Error.mkOtherError :

UInt32 → String → IO.Error

Equations

IO.Error.mkOtherError = IO.Error.otherError

def IO.Error.mkPermissionDenied :

UInt32 → String → IO.Error

Equations

IO.Error.mkPermissionDenied = IO.Error.permissionDenied none

def IO.Error.mkHardwareFault :

UInt32 → String → IO.Error

Equations

IO.Error.mkHardwareFault = IO.Error.hardwareFault

def IO.Error.mkUnsatisfiedConstraints :

UInt32 → String → IO.Error

Equations

IO.Error.mkUnsatisfiedConstraints = IO.Error.unsatisfiedConstraints

def IO.Error.mkIllegalOperation :

UInt32 → String → IO.Error

Equations

IO.Error.mkIllegalOperation = IO.Error.illegalOperation

def IO.Error.mkProtocolError :

UInt32 → String → IO.Error

Equations

IO.Error.mkProtocolError = IO.Error.protocolError

def IO.Error.mkTimeExpired :

UInt32 → String → IO.Error

Equations

IO.Error.mkTimeExpired = IO.Error.timeExpired

def IO.Error.fopenErrorToString (gist : String) (fn : String) (code : UInt32) :

Option String → String

Equations

IO.Error.fopenErrorToString gist fn code _fun_discr = match _fun_discr with | some details => IO.Error.downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ IO.Error.downCaseFirst details ++ ")\n file: " ++ fn | none => IO.Error.downCaseFirst gist ++ " (error code: " ++ toString code ++ ")\n file: " ++ fn

def IO.Error.otherErrorToString (gist : String) (code : UInt32) :

Option String → String

Equations

IO.Error.otherErrorToString gist code _fun_discr = match _fun_discr with | some details => IO.Error.downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ IO.Error.downCaseFirst details ++ ")" | none => IO.Error.downCaseFirst gist ++ " (error code: " ++ toString code ++ ")"

def IO.Error.toString :

IO.Error → String

Equations

IO.Error.toString _fun_discr = match _fun_discr with | IO.Error.unexpectedEof => "end of file" | IO.Error.inappropriateType (some fn) code details => IO.Error.fopenErrorToString "inappropriate type" fn code (some details) | IO.Error.inappropriateType none code details => IO.Error.otherErrorToString "inappropriate type" code (some details) | IO.Error.interrupted fn code details => IO.Error.fopenErrorToString "interrupted system call" fn code (some details) | IO.Error.invalidArgument (some fn) code details => IO.Error.fopenErrorToString "invalid argument" fn code (some details) | IO.Error.invalidArgument none code details => IO.Error.otherErrorToString "invalid argument" code (some details) | IO.Error.noFileOrDirectory fn code details => IO.Error.fopenErrorToString "no such file or directory" fn code none | IO.Error.noSuchThing (some fn) code details => IO.Error.fopenErrorToString "no such thing" fn code (some details) | IO.Error.noSuchThing none code details => IO.Error.otherErrorToString "no such thing" code (some details) | IO.Error.permissionDenied (some fn) code details => IO.Error.fopenErrorToString details fn code none | IO.Error.permissionDenied none code details => IO.Error.otherErrorToString details code none | IO.Error.resourceExhausted (some fn) code details => IO.Error.fopenErrorToString "resource exhausted" fn code (some details) | IO.Error.resourceExhausted none code details => IO.Error.otherErrorToString "resource exhausted" code (some details) | IO.Error.alreadyExists none code details => IO.Error.otherErrorToString "already exists" code (some details) | IO.Error.alreadyExists (some fn) code details => IO.Error.fopenErrorToString "already exists" fn code (some details) | IO.Error.otherError code details => IO.Error.otherErrorToString details code none | IO.Error.resourceBusy code details => IO.Error.otherErrorToString "resource busy" code (some details) | IO.Error.resourceVanished code details => IO.Error.otherErrorToString "resource vanished" code (some details) | IO.Error.hardwareFault code details => IO.Error.otherErrorToString "hardware fault" code none | IO.Error.illegalOperation code details => IO.Error.otherErrorToString "illegal operation" code (some details) | IO.Error.protocolError code details => IO.Error.otherErrorToString "protocol error" code (some details) | IO.Error.timeExpired code details => IO.Error.otherErrorToString "time expired" code (some details) | IO.Error.unsatisfiedConstraints code details => IO.Error.otherErrorToString "directory not empty" code none | IO.Error.unsupportedOperation code details => IO.Error.otherErrorToString "unsupported operation" code (some details) | IO.Error.userError msg => msg

instance IO.Error.instToStringError :

ToString IO.Error

Equations

IO.Error.instToStringError = { toString := IO.Error.toString }