Lean.Server.Rpc.Basic

class Lean.Server.MonadRpcSession (m : Type → Type) :

Type

rpcStoreRef : Lean.Name → NonScalar → m Lean.Lsp.RpcRef
rpcGetRef : Lean.Lsp.RpcRef → m (Option (Lean.Name × NonScalar))
rpcReleaseRef : Lean.Lsp.RpcRef → m Bool

Instances

instance Lean.Server.instMonadRpcSession {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : Lean.Server.MonadRpcSession m] :

Lean.Server.MonadRpcSession n

Equations

Lean.Server.instMonadRpcSession = { rpcStoreRef := fun typeName obj => liftM (Lean.Server.rpcStoreRef typeName obj), rpcGetRef := fun r => liftM (Lean.Server.rpcGetRef r), rpcReleaseRef := fun r => liftM (Lean.Server.rpcReleaseRef r) }

source

class Lean.Server.RpcEncoding (α : Type) (β : outParam Type) :

Type 1

rpcEncode : {m : Type → Type} → [inst : Monad m] → [inst : Lean.Server.MonadRpcSession m] → α → m β
rpcDecode : {m : Type → Type} → [inst : Monad m] → [inst : Lean.Server.MonadRpcSession m] → β → ExceptT String m α

Instances

source

instance Lean.Server.instRpcEncoding {α : Type} [inst : Lean.FromJson α] [inst : Lean.ToJson α] :

Lean.Server.RpcEncoding α α

Equations

Lean.Server.instRpcEncoding = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => pure, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => pure }

source

instance Lean.Server.instRpcEncodingOption {α : Type} {β : outParam Type} [inst : Lean.Server.RpcEncoding α β] :

Lean.Server.RpcEncoding (Option α) (Option β)

Equations

Lean.Server.instRpcEncodingOption = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] v => match v with | none => pure none | some v => some <$> Lean.Server.rpcEncode v, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] v => match v with | none => pure none | some v => some <$> Lean.Server.rpcDecode v }

source

instance Lean.Server.instRpcEncodingArray {α : Type} {β : outParam Type} [inst : Lean.Server.RpcEncoding α β] :

Lean.Server.RpcEncoding (Array α) (Array β)

Equations

Lean.Server.instRpcEncodingArray = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => Array.mapM Lean.Server.rpcEncode a, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] b => Array.mapM Lean.Server.rpcDecode b }

source

instance Lean.Server.instRpcEncodingProd {α : Type} {α' : outParam Type} {β : Type} {β' : outParam Type} [inst : Lean.Server.RpcEncoding α α'] [inst : Lean.Server.RpcEncoding β β'] :

Lean.Server.RpcEncoding (α × β) (α' × β')

Equations

Lean.Server.instRpcEncodingProd = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] x => match x with | (a, b) => do let a' ← Lean.Server.rpcEncode a let b' ← Lean.Server.rpcEncode b pure (a', b'), rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] x => match x with | (a', b') => do let a ← Lean.Server.rpcDecode a' let b ← Lean.Server.rpcDecode b' pure (a, b) }

source

structure Lean.Server.RpcEncoding.DerivingParams :

Type

withRef : Bool

source

structure Lean.Server.WithRpcRef (α : Type u) :

Type u

val : α

source

instance Lean.Server.instInhabitedWithRpcRef :

{a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.Server.WithRpcRef a)

Equations

Lean.Server.instInhabitedWithRpcRef = { default := { val := default } }

source

unsafe def Lean.Server.WithRpcRef.encodeUnsafe {m : Type → Type} [inst : Lean.Server.MonadRpcSession m] {α : Type u_1} [inst : Monad m] (typeName : Lean.Name) (r : Lean.Server.WithRpcRef α) :

m Lean.Lsp.RpcRef

Equations

Lean.Server.WithRpcRef.encodeUnsafe typeName r = let obj := unsafeCast r.val; Lean.Server.rpcStoreRef typeName obj

source

unsafe def Lean.Server.WithRpcRef.decodeUnsafeAs {m : Type → Type} [inst : Monad m] [inst : Lean.Server.MonadRpcSession m] (α : Type) (typeName : Lean.Name) (r : Lean.Lsp.RpcRef) :

ExceptT String m (Lean.Server.WithRpcRef α)

Equations

Lean.Server.WithRpcRef.decodeUnsafeAs α typeName r = do let a ← Lean.Server.rpcGetRef r match a with | none => throw (toString "RPC reference '" ++ toString r ++ toString "' is not valid") | some (nm, obj) => let _do_jp := fun y => pure { val := unsafeCast obj }; if (nm != typeName) = true then do let y ← throw (toString "RPC call type mismatch in reference '" ++ toString r ++ toString "'\nexpected '" ++ toString typeName ++ toString "', got '" ++ toString nm ++ toString "'") _do_jp y else do let y ← pure PUnit.unit _do_jp y