Skip to main content

🍃 RPC_query.v

Environment

See proofs, Gitlab , OCaml

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

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