Skip to main content

🍃 RPC_service.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Data_encoding.
Require Proto_alpha.Environment.RPC_path.
Require Proto_alpha.Environment.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.