🐾 Path_encoding.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.

Module S.
  Record signature {t : Set} : Set := {
    t := t;
    to_path : t → list string → list string;
    of_path : list string → M? (option t);
    path_length : M? int;
  }.
End S.
Definition S := @S.signature.
Arguments S {_}.

Module ENCODING.
  Record signature {t : Set} : Set := {
    t := t;
    to_bytes : t → bytes;
    of_bytes_opt : bytes → option t;
  }.
End ENCODING.
Definition ENCODING := @ENCODING.signature.
Arguments ENCODING {_}.

Module Make_hex.
  Class FArgs {H_t : Set} := {
    H : ENCODING (t := H_t);
  }.
  Arguments Build_FArgs {_}.

  Definition path_length `{FArgs} : M? int := return? 1.

  Definition to_path `{FArgs} (t_value : H.(ENCODING.t)) (l_value : list string)
    : list string :=
    let 'Hex.Hex key_value := Hex.of_bytes None (H.(ENCODING.to_bytes) t_value)
      in
    cons key_value l_value.

  Definition of_path `{FArgs} (function_parameter : list string)
    : M? (option H.(ENCODING.t)) :=
    match function_parameter with
    | cons path [] ⇒
      return?
        (Option.bind (Hex.to_bytes (Hex.Hex path)) H.(ENCODING.of_bytes_opt))
    | _ ⇒ return? None
    end.

  (* Make_hex *)
  Definition functor `{FArgs} :=
    {|
      S.path_length := path_length;
      S.to_path := to_path;
      S.of_path := of_path
    |}.
End Make_hex.
Definition Make_hex {H_t : Set} (H : ENCODING (t := H_t)) :=
  let '_ := Make_hex.Build_FArgs H in
  Make_hex.functor.