Skip to main content

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

Module S.
  Record signature {t : Set} : Set := {
    t := t;
    to_path : t list string list string;
    of_path : list string option t;
    path_length : 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} : int := 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)
    : option H.(ENCODING.t) :=
    match function_parameter with
    | cons path []
      Option.bind (Hex.to_bytes (Hex.Hex path)) H.(ENCODING.of_bytes_opt)
    | _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.