Skip to main content

🗿 Legacy_script_patches.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.

Module t.
  Record record : Set := Build {
    addresses : list string;
    hash : Script_expr_hash.t;
    patched_code : Micheline.canonical Michelson_v1_primitives.prim;
  }.
  Definition with_addresses addresses (r : record) :=
    Build addresses r.(hash) r.(patched_code).
  Definition with_hash hash (r : record) :=
    Build r.(addresses) hash r.(patched_code).
  Definition with_patched_code patched_code (r : record) :=
    Build r.(addresses) r.(hash) patched_code.
End t.
Definition t := t.record.

Definition script_hash (function_parameter : t) : Script_expr_hash.t :=
  let '{| t.hash := hash_value |} := function_parameter in
  hash_value.

Definition code (function_parameter : t)
  : Micheline.canonical Michelson_v1_primitives.prim :=
  let '{| t.patched_code := patched_code |} := function_parameter in
  patched_code.

Definition bin_expr_exn (hex : string) : Script_repr.expr :=
  match
    Option.bind (Hex.to_bytes (Hex.Hex hex))
      (fun (bytes_value : bytes) ⇒
        Data_encoding.Binary.of_bytes_opt Script_repr.expr_encoding bytes_value)
    with
  | Some exprexpr
  | None
    Pervasives.raise
      (Build_extensible "Failure" string "Decoding script failed.")
  end.

Definition patches {A : Set} : list A := nil.

Definition addresses_to_patch
  : list
    (string × Script_expr_hash.t ×
      Micheline.canonical Michelson_v1_primitives.prim) :=
  List.concat_map
    (fun (function_parameter : t) ⇒
      let '{|
        t.addresses := addresses;
          t.hash := hash_value;
          t.patched_code := patched_code
          |} := function_parameter in
      List.map (fun (addr : string) ⇒ (addr, hash_value, patched_code))
        addresses) patches.