Skip to main content

🍃 RPC_context.v

Environment

Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Updater.

Definition t : Set := Updater.rpc_context.

Module simple.
  Record record {pr : Set} : Set := Build {
    call_proto_service0 :
       {q i o : Set},
        RPC_service.t t t q i o pr q i
        Error_monad.shell_tzresult o;
    call_proto_service1 :
       {a q i o : Set},
        RPC_service.t t (t × a) q i o pr a q i
        Error_monad.shell_tzresult o;
    call_proto_service2 :
       {a b q i o : Set},
        RPC_service.t t ((t × a) × b) q i o pr a b q i
        Error_monad.shell_tzresult o;
    call_proto_service3 :
       {a b c q i o : Set},
        RPC_service.t t (((t × a) × b) × c) q i o pr a b c q
        i Error_monad.shell_tzresult o }.
  Arguments record : clear implicits.
End simple.
Definition simple := simple.record.

Parameter make_call0 : {i o pr q : Set},
  RPC_service.t t t q i o simple pr pr q i
  Error_monad.shell_tzresult o.

Parameter make_call1 : {a i o pr q : Set},
  RPC_service.t t (t × a) q i o simple pr pr a q i
  Error_monad.shell_tzresult o.

Parameter make_call2 : {a b i o pr q : Set},
  RPC_service.t t ((t × a) × b) q i o simple pr pr a b q
  i Error_monad.shell_tzresult o.

Parameter make_call3 : {a b c i o pr q : Set},
  RPC_service.t t (((t × a) × b) × c) q i o simple pr pr a b
  c q i Error_monad.shell_tzresult o.

Parameter make_opt_call0 : {i o pr q : Set},
  RPC_service.t t t q i o simple pr pr q i
  Error_monad.shell_tzresult (option o).

Parameter make_opt_call1 : {a i o pr q : Set},
  RPC_service.t t (t × a) q i o simple pr pr a q i
  Error_monad.shell_tzresult (option o).

Parameter make_opt_call2 : {a b i o pr q : Set},
  RPC_service.t t ((t × a) × b) q i o simple pr pr a b q
  i Error_monad.shell_tzresult (option o).

Parameter make_opt_call3 : {a b c i o pr q : Set},
  RPC_service.t t (((t × a) × b) × c) q i o simple pr pr a b
  c q i Error_monad.shell_tzresult (option o).