🍃 RPC_service.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.RPC_path.
Require TezosOfOCaml.Environment.Structs.V0.RPC_query.
Inductive meth : Set :=
| PUT : meth
| GET : meth
| DELETE : meth
| POST : meth
| PATCH : meth.
Module t.
Record record {prefix params query input output : Set} : Set := Build {
method : meth;
description : option string;
query_rpc : RPC_query.t query;
input_encoding : Data_encoding.t input;
output_encoding : Data_encoding.t output;
path : RPC_path.t prefix params;
}.
Arguments record : clear implicits.
End t.
Definition t := t.record.
Definition service (prefix params query input output : Set) : Set :=
t prefix params query input output.
Definition get_service {output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(output_encoding : Data_encoding.t output) (path : RPC_path.t prefix params)
: service prefix params query unit output :=
t.Build _ _ _ _ _
GET description query_rpc Data_encoding.unit_value output_encoding path.
Definition post_service {input output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(input_encoding : Data_encoding.t input)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query input output :=
t.Build _ _ _ _ _
POST description query_rpc input_encoding output_encoding path.
Definition delete_service {output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query unit output :=
t.Build _ _ _ _ _
DELETE description query_rpc Data_encoding.unit_value output_encoding path.
Definition patch_service {input output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(input_encoding : Data_encoding.t input)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query input output :=
t.Build _ _ _ _ _
PATCH description query_rpc input_encoding output_encoding path.
Definition put_service {input output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(input_encoding : Data_encoding.t input)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query input output :=
t.Build _ _ _ _ _
PUT description query_rpc input_encoding output_encoding path.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.RPC_path.
Require TezosOfOCaml.Environment.Structs.V0.RPC_query.
Inductive meth : Set :=
| PUT : meth
| GET : meth
| DELETE : meth
| POST : meth
| PATCH : meth.
Module t.
Record record {prefix params query input output : Set} : Set := Build {
method : meth;
description : option string;
query_rpc : RPC_query.t query;
input_encoding : Data_encoding.t input;
output_encoding : Data_encoding.t output;
path : RPC_path.t prefix params;
}.
Arguments record : clear implicits.
End t.
Definition t := t.record.
Definition service (prefix params query input output : Set) : Set :=
t prefix params query input output.
Definition get_service {output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(output_encoding : Data_encoding.t output) (path : RPC_path.t prefix params)
: service prefix params query unit output :=
t.Build _ _ _ _ _
GET description query_rpc Data_encoding.unit_value output_encoding path.
Definition post_service {input output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(input_encoding : Data_encoding.t input)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query input output :=
t.Build _ _ _ _ _
POST description query_rpc input_encoding output_encoding path.
Definition delete_service {output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query unit output :=
t.Build _ _ _ _ _
DELETE description query_rpc Data_encoding.unit_value output_encoding path.
Definition patch_service {input output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(input_encoding : Data_encoding.t input)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query input output :=
t.Build _ _ _ _ _
PATCH description query_rpc input_encoding output_encoding path.
Definition put_service {input output params prefix query : Set}
(description : option string) (query_rpc : RPC_query.t query)
(input_encoding : Data_encoding.t input)
(output_encoding : Data_encoding.t output)
(path : RPC_path.t prefix params)
: service prefix params query input output :=
t.Build _ _ _ _ _
PUT description query_rpc input_encoding output_encoding path.