inductive LeanRedis.Protocol.Phase : Type

• disconnected : Phase
• connecting (attempt : Nat) : Phase
• bootstrapping (isReconnect : Bool) : Phase
• ready (version : Version) (selectedDb? : Option UInt32) : Phase
• reconnecting (attempt : Nat) : Phase
• closing : Phase
• failed (error : String) : Phase

def LeanRedis.Protocol.instBEqPhase.beq : Phase → Phase → Bool

Equations

• LeanRedis.Protocol.instBEqPhase.beq LeanRedis.Protocol.Phase.disconnected LeanRedis.Protocol.Phase.disconnected = true
• LeanRedis.Protocol.instBEqPhase.beq (LeanRedis.Protocol.Phase.connecting a) (LeanRedis.Protocol.Phase.connecting b) = (a == b)
• LeanRedis.Protocol.instBEqPhase.beq (LeanRedis.Protocol.Phase.bootstrapping a) (LeanRedis.Protocol.Phase.bootstrapping b) = (a == b)
• LeanRedis.Protocol.instBEqPhase.beq (LeanRedis.Protocol.Phase.ready a a_1) (LeanRedis.Protocol.Phase.ready b b_1) = (a == b && a_1 == b_1)
• LeanRedis.Protocol.instBEqPhase.beq (LeanRedis.Protocol.Phase.reconnecting a) (LeanRedis.Protocol.Phase.reconnecting b) = (a == b)
• LeanRedis.Protocol.instBEqPhase.beq LeanRedis.Protocol.Phase.closing LeanRedis.Protocol.Phase.closing = true
• LeanRedis.Protocol.instBEqPhase.beq (LeanRedis.Protocol.Phase.failed a) (LeanRedis.Protocol.Phase.failed b) = (a == b)
• LeanRedis.Protocol.instBEqPhase.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqPhase : BEq Phase

Equations

• LeanRedis.Protocol.instBEqPhase = { beq := LeanRedis.Protocol.instBEqPhase.beq }

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedPhase : Inhabited Phase

Equations

• LeanRedis.Protocol.instInhabitedPhase = { default := LeanRedis.Protocol.instInhabitedPhase.default }

def LeanRedis.Protocol.instInhabitedPhase.default : Phase

Equations

• LeanRedis.Protocol.instInhabitedPhase.default = LeanRedis.Protocol.Phase.disconnected

def LeanRedis.Protocol.instReprPhase.repr : Phase → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.Protocol.instReprPhase : Repr Phase

Equations

• LeanRedis.Protocol.instReprPhase = { reprPrec := LeanRedis.Protocol.instReprPhase.repr }

structure LeanRedis.Protocol.Session : Type

• phase : Phase
• lastReply? : Option Resp.Value

def LeanRedis.Protocol.instBEqSession.beq : Session → Session → Bool

Equations

• LeanRedis.Protocol.instBEqSession.beq { phase := a, lastReply? := a_1 } { phase := b, lastReply? := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.Protocol.instBEqSession.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqSession : BEq Session

Equations

• LeanRedis.Protocol.instBEqSession = { beq := LeanRedis.Protocol.instBEqSession.beq }

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedSession : Inhabited Session

Equations

• LeanRedis.Protocol.instInhabitedSession = { default := LeanRedis.Protocol.instInhabitedSession.default }

def LeanRedis.Protocol.instInhabitedSession.default : Session

Equations

• LeanRedis.Protocol.instInhabitedSession.default = { phase := default, lastReply? := default }

inductive LeanRedis.Protocol.Action : Type

• requestConnect : Action
• transportOpened : Action
• transportFailed (error : String) : Action
• bootstrapComplete (replies : Array Resp.Value) : Action
• replyReceived (request? : Option CommandRequest) (reply : Resp.Value) : Action
• remoteDisconnect : Action
• reconnectTick : Action
• reconnectExhausted : Action
• requestDisconnect : Action
• closeComplete : Action

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqAction : BEq Action

Equations

• LeanRedis.Protocol.instBEqAction = { beq := LeanRedis.Protocol.instBEqAction.beq }

def LeanRedis.Protocol.instBEqAction.beq : Action → Action → Bool

Equations

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

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedAction : Inhabited Action

Equations

• LeanRedis.Protocol.instInhabitedAction = { default := LeanRedis.Protocol.instInhabitedAction.default }

def LeanRedis.Protocol.instInhabitedAction.default : Action

Equations

• LeanRedis.Protocol.instInhabitedAction.default = LeanRedis.Protocol.Action.requestConnect

inductive LeanRedis.Protocol.EventTag : Type

• initialConnectFailed : EventTag
• remoteDisconnected : EventTag
• reconnectAttemptStarted : EventTag
• reconnectAttemptFailed : EventTag
• reconnected : EventTag
• reconnectStopped : EventTag
• explicitlyDisconnected : EventTag

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqEventTag : BEq EventTag

Equations

• LeanRedis.Protocol.instBEqEventTag = { beq := LeanRedis.Protocol.instBEqEventTag.beq }

def LeanRedis.Protocol.instBEqEventTag.beq : EventTag → EventTag → Bool

Equations

• LeanRedis.Protocol.instBEqEventTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def LeanRedis.Protocol.instInhabitedEventTag.default : EventTag

Equations

• LeanRedis.Protocol.instInhabitedEventTag.default = LeanRedis.Protocol.EventTag.initialConnectFailed

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedEventTag : Inhabited EventTag

Equations

• LeanRedis.Protocol.instInhabitedEventTag = { default := LeanRedis.Protocol.instInhabitedEventTag.default }

inductive LeanRedis.Protocol.Effect : Type

• sendBootstrapRequests : Effect
• closeTransport : Effect
• emit (tag : EventTag) : Effect

def LeanRedis.Protocol.instBEqEffect.beq : Effect → Effect → Bool

Equations

• LeanRedis.Protocol.instBEqEffect.beq LeanRedis.Protocol.Effect.sendBootstrapRequests LeanRedis.Protocol.Effect.sendBootstrapRequests = true
• LeanRedis.Protocol.instBEqEffect.beq LeanRedis.Protocol.Effect.closeTransport LeanRedis.Protocol.Effect.closeTransport = true
• LeanRedis.Protocol.instBEqEffect.beq (LeanRedis.Protocol.Effect.emit a) (LeanRedis.Protocol.Effect.emit b) = (a == b)
• LeanRedis.Protocol.instBEqEffect.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqEffect : BEq Effect

Equations

• LeanRedis.Protocol.instBEqEffect = { beq := LeanRedis.Protocol.instBEqEffect.beq }

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedEffect : Inhabited Effect

Equations

• LeanRedis.Protocol.instInhabitedEffect = { default := LeanRedis.Protocol.instInhabitedEffect.default }

def LeanRedis.Protocol.instInhabitedEffect.default : Effect

Equations

• LeanRedis.Protocol.instInhabitedEffect.default = LeanRedis.Protocol.Effect.sendBootstrapRequests

def LeanRedis.Protocol.Session.isReady (session : Session) : Bool

Equations

• session.isReady = match session.phase with | LeanRedis.Protocol.Phase.ready version selectedDb? => true | x => false

def LeanRedis.Protocol.Session.isDisconnected (session : Session) : Bool

Equations

• session.isDisconnected = match session.phase with | LeanRedis.Protocol.Phase.disconnected => true | x => false

def LeanRedis.Protocol.Session.protocol? (session : Session) : Option Version

Equations

• session.protocol? = match session.phase with | LeanRedis.Protocol.Phase.ready v selectedDb? => some v | x => none

def LeanRedis.Protocol.Session.selectedDb? (session : Session) : Option UInt32

Equations

• session.selectedDb? = match session.phase with | LeanRedis.Protocol.Phase.ready version db => db | x => none

def LeanRedis.Protocol.Session.step (session : Session) (action : Action) (config : Config) : Session × Array Effect

Equations

• One or more equations did not get rendered due to their size.
• session.step LeanRedis.Protocol.Action.requestConnect config = ({ phase := LeanRedis.Protocol.Phase.connecting 0, lastReply? := session.lastReply? }, #[])
• session.step (LeanRedis.Protocol.Action.replyReceived none reply) config = ({ phase := LeanRedis.Protocol.Phase.ready v (none.orElse fun (x : Unit) => db), lastReply? := some reply }, #[])
• session.step LeanRedis.Protocol.Action.reconnectExhausted config = ({ lastReply? := session.lastReply? }, #[LeanRedis.Protocol.Effect.emit LeanRedis.Protocol.EventTag.reconnectStopped])
• session.step LeanRedis.Protocol.Action.closeComplete config = ({ lastReply? := session.lastReply? }, #[])
• session.step action✝ config = (session, #[])