🗿 Legacy_script_patches.v
Translated 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 expr ⇒ expr
| 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.
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 expr ⇒ expr
| 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.