Skip to main content

🍃 RPC_arg.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Pervasives.

Module t.
  Record record {a : Set} : Set := Build {
    descr : option string;
    name : string;
    destruct : string Pervasives.result a string;
    construct : a string;
  }.
  Arguments record : clear implicits.
End t.
Definition t := t.record.

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

Definition make {a : Set}
  (descr : option string) (name : string)
  (destruct : string Pervasives.result a string) (construct : a string)
  (_ : unit) : arg a :=
  t.Build _ descr name destruct construct.

Module descr.
  Record record : Set := Build {
    name : string;
    descr : option string }.
  Definition with_name name (r : record) :=
    Build name r.(descr).
  Definition with_descr descr (r : record) :=
    Build r.(name) descr.
End descr.
Definition descr := descr.record.

Definition descr_value {a : Set} (x : arg a) : descr :=
  {|
    descr.name := x.(t.name);
    descr.descr := x.(t.descr);
  |}.

Parameter bool_value : arg bool.

Parameter int_value : arg int.

Parameter uint : arg int.

Parameter int32_value : arg int32.

Parameter uint31 : arg int32.

Parameter int64_value : arg int64.

Parameter uint63 : arg int64.

Parameter string_value : arg string.

Parameter option_value : {a : Set}, arg a arg (option a).

Parameter list_value : {a : Set}, arg a arg (list a).

Parameter like : {a : Set}, arg a option string string arg a.

Inductive eq (a : Set) : Set :=
| Eq : eq a.

Arguments Eq {_}.

Parameter eq_value : {a b : Set}, arg a arg b option (eq a).