| Safe Haskell | Safe |
|---|---|
| Language | GHC2021 |
LambdaUC.UC
Synopsis
- type EnvProcess down res = ExecBuilder ExecIndexInit (ExecIndexSome '[PingRecvPort, down] (InitPresent res)) ()
- data SubRespTree (up :: Port) where
- MkSubRespTree :: ExecBuilder ExecIndexInit (ExecIndexSome (PingSendPort : (PortDual (x :> y) : down)) InitAbsent) () -> HList SubRespTree down -> SubRespTree (x :> y)
- subRespEval :: SubRespTree iface -> ExecBuilder ExecIndexInit (ExecIndexSome '[PingSendPort, PortDual iface] InitAbsent) ()
Documentation
type EnvProcess down res = ExecBuilder ExecIndexInit (ExecIndexSome '[PingRecvPort, down] (InitPresent res)) () #
data SubRespTree (up :: Port) where #
A tree of subroutine-respecting protocols.
A `SubRespTree m up` is either an ideal functionality or a protocol where the required subroutine interfaces were filled with actual implementations (and, therefore, are not required and not exposed by a type parameter anymore).
Constructors
| MkSubRespTree :: ExecBuilder ExecIndexInit (ExecIndexSome (PingSendPort : (PortDual (x :> y) : down)) InitAbsent) () -> HList SubRespTree down -> SubRespTree (x :> y) |
Arguments
| :: SubRespTree iface | The called protocol with its subroutines composed-in |
| -> ExecBuilder ExecIndexInit (ExecIndexSome '[PingSendPort, PortDual iface] InitAbsent) () |
Run environment with a given protocol (no adversary yet).