🍃 RPC_query.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.RPC_arg.

Parameter t : ∀ (a : Set), Set.

Definition query (a : Set) : Set := t a.

Parameter empty : query unit.

Module field.
  Record record {a b : Set} : Set := Build {
    description : option string;
    name : string;
    ty : RPC_arg.t b;
    default : b;
    get : a → b;
  }.
  Arguments record : clear implicits.
End field.
Definition field := field.record.

Definition field_value {a b : Set}
  (description : option string) (name : string) (ty : RPC_arg.t a) (default : a)
  (get : b → a) : field b a :=
  {|
    field.description := description;
    field.name := name;
    field.ty := ty;
    field.default := default;
    field.get := get;
  |}.

Definition opt_field {a b : Set}
  (description : option string) (name : string) (ty : RPC_arg.t a)
  (get : b → option a) : field b (option a) :=
  {|
    field.description := description;
    field.name := name;
    field.ty := RPC_arg.option_value ty;
    field.default := None;
    field.get := get;
  |}.

Definition flag {a : Set}
  (description : option string) (name : string) (get : a → bool) :
  field a bool :=
  {|
    field.description := description;
    field.name := name;
    field.ty := RPC_arg.bool_value;
    field.default := false;
    field.get := get;
  |}.

Definition multi_field {a b : Set}
  (description : option string) (name : string) (ty : RPC_arg.t a)
  (get : b → list a) : field b (list a) :=
  {|
    field.description := description;
    field.name := name;
    field.ty := RPC_arg.list_value ty;
    field.default := [];
    field.get := get;
  |}.

Parameter open_query : ∀ (a b c : Set), Set.

Parameter query_value : ∀ {a b : Set}, b → open_query a b b.

Parameter op_pipeplus : ∀ {a b c d : Set},
  open_query a b (c → d) → field a c → open_query a b d.

Parameter seal : ∀ {a b : Set}, open_query a b a → t a.

Definition untyped : Set := list (string × string).

Parameter parse : ∀ {a : Set}, query a → untyped → a.