Skip to main content

🎯 Destination_repr.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.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Inductive t : Set :=
| Contract : Contract_repr.t t
| Tx_rollup : Tx_rollup_repr.t t.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (l1 : t) (l2 : t) : int :=
      match (l1, l2) with
      | (Contract k1, Contract k2)Contract_repr.compare k1 k2
      | (Tx_rollup k1, Tx_rollup k2)Tx_rollup_repr.compare k1 k2
      | (Contract _, _) ⇒ (-1)
      | (_, Contract _) ⇒ 1
      end in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "destination_repr.invalid_b58check" "Destination decoding failed"
    "Failed to read a valid destination from a b58check_encoding data" None
    (Data_encoding.obj1
      (Data_encoding.req None None "input" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_destination_b58check" then
          let x_value := cast string payload in
          Some x_value
        else None
      end)
    (fun (x_value : string) ⇒
      Build_extensible "Invalid_destination_b58check" string x_value).

Definition of_b58check (s_value : string) : M? t :=
  match Contract_repr.of_b58check s_value with
  | Pervasives.Ok s_valuePervasives.Ok (Contract s_value)
  | Pervasives.Error _
    match Tx_rollup_repr.of_b58check s_value with
    | Pervasives.Ok s_valuePervasives.Ok (Tx_rollup s_value)
    | Pervasives.Error _
      Error_monad.error_value
        (Build_extensible "Invalid_destination_b58check" string s_value)
    end
  end.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.def "transaction_destination"
    (Some "A destination of a transaction")
    (Some
      "A destination notation compatible with the contract notation as given to an RPC or inside scripts. Can be a base58 implicit contract hash, a base58 originated contract hash, or a base58 originated transaction rollup.")
    (Data_encoding.splitted
      (Data_encoding.conv to_b58check
        (fun (s_value : string) ⇒
          match of_b58check s_value with
          | Pervasives.Ok s_values_value
          | Pervasives.Error _
            Data_encoding.Json.cannot_destruct
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid destination notation."
                  CamlinternalFormatBasics.End_of_format)
                "Invalid destination notation.")
          end) None Data_encoding.string_value)
      (Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
        (Pervasives.op_at
          (Contract_repr.cases
            (fun (function_parameter : t) ⇒
              match function_parameter with
              | Contract x_valueSome x_value
              | _None
              end) (fun (x_value : Contract_repr.contract) ⇒ Contract x_value))
          [
            Data_encoding.case_value "Tx_rollup" None (Data_encoding.Tag 2)
              (Data_encoding.Fixed.add_padding Tx_rollup_repr.encoding 1)
              (fun (function_parameter : t) ⇒
                match function_parameter with
                | Tx_rollup k_valueSome k_value
                | _None
                end)
              (fun (k_value : Tx_rollup_repr.t) ⇒ Tx_rollup k_value)
          ]))).

Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Contract k_valueContract_repr.pp fmt k_value
  | Tx_rollup k_valueTx_rollup_repr.pp fmt k_value
  end.

Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
  match function_parameter with
  | Contract k_value
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      (Contract_repr.in_memory_size k_value)
  | Tx_rollup k_value
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      (Tx_rollup_repr.in_memory_size k_value)
  end.