🍬 Script_big_map.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Definition empty {a b : Set}
(key_type : Script_typed_ir.comparable_ty) (value_type : Script_typed_ir.ty)
: Script_typed_ir.big_map :=
Script_typed_ir.Big_map
{| Script_typed_ir.big_map.Big_map.id := None;
Script_typed_ir.big_map.Big_map.diff :=
({|
Script_typed_ir.big_map_overlay.map :=
Script_typed_ir.Big_map_overlay.(Map.S.empty);
Script_typed_ir.big_map_overlay.size := 0; |} :
Script_typed_ir.big_map_overlay a b);
Script_typed_ir.big_map.Big_map.key_type := key_type;
Script_typed_ir.big_map.Big_map.value_type := value_type; |}.
Definition mem {A : Set}
(ctxt : Alpha_context.context) (key_value : A)
(function_parameter : Script_typed_ir.big_map)
: M? (bool × Alpha_context.context) :=
let
'Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.id := id;
Script_typed_ir.big_map.Big_map.diff := diff_value;
Script_typed_ir.big_map.Big_map.key_type := key_type
|} := function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
match
((Script_typed_ir.Big_map_overlay.(Map.S.find) key_hash
diff_value.(Script_typed_ir.big_map_overlay.map)), id) with
| (None, None) ⇒ return? (false, ctxt)
| (None, Some id) ⇒
let? '(ctxt, res) := Alpha_context.Big_map.mem ctxt id key_hash in
return? (res, ctxt)
| (Some (_, None), _) ⇒ return? (false, ctxt)
| (Some (_, Some _), _) ⇒ return? (true, ctxt)
end.
Definition get_by_hash {A B : Set}
(ctxt : Alpha_context.context) (key_value : Script_expr_hash.t)
(big_map : Script_typed_ir.big_map) : M? (option A × Alpha_context.context) :=
let
'Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.id := id;
Script_typed_ir.big_map.Big_map.diff := diff_value;
Script_typed_ir.big_map.Big_map.value_type := value_type
|} := big_map in
let '[value_type, diff_value, id] :=
cast
[Script_typed_ir.ty ** Script_typed_ir.big_map_overlay B A **
option Alpha_context.Big_map.Id.t] [value_type, diff_value, id] in
match
((Script_typed_ir.Big_map_overlay.(Map.S.find) key_value
diff_value.(Script_typed_ir.big_map_overlay.map)), id) with
| (Some (_, x_value), _) ⇒ return? (x_value, ctxt)
| (None, None) ⇒ return? (None, ctxt)
| (None, Some id) ⇒
let? function_parameter := Alpha_context.Big_map.get_opt ctxt id key_value
in
match function_parameter with
| (ctxt, None) ⇒ return? (None, ctxt)
| (ctxt, Some value_value) ⇒
let? '(x_value, ctxt) :=
Script_ir_translator.parse_data
(Script_ir_translator_config.make None None true tt) ctxt true
value_type (Micheline.root_value value_value) in
return? ((Some x_value), ctxt)
end
end.
Definition get {A B : Set}
(ctxt : Alpha_context.context) (key_value : A)
(function_parameter : Script_typed_ir.big_map)
: M? (option B × Alpha_context.context) :=
let
'(Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.key_type := key_type |}) as map :=
function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
(get_by_hash (B := A)) ctxt key_hash map.
Definition update_by_hash {A B : Set}
(key_hash : Script_expr_hash.t) (key_value : A) (value_value : option B)
(big_map : Script_typed_ir.big_map) : Script_typed_ir.big_map :=
let 'Script_typed_ir.Big_map map := big_map in
let map := cast (Script_typed_ir.big_map.Big_map A B) map in
let contains :=
Script_typed_ir.Big_map_overlay.(Map.S.mem) key_hash
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.map)
in
Script_typed_ir.Big_map
(Script_typed_ir.big_map.Big_map.with_diff
{|
Script_typed_ir.big_map_overlay.map :=
Script_typed_ir.Big_map_overlay.(Map.S.add) key_hash
(key_value, value_value)
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.map);
Script_typed_ir.big_map_overlay.size :=
if contains then
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.size)
else
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.size)
+i 1; |} map).
Definition update {A B : Set}
(ctxt : Alpha_context.context) (key_value : A) (value_value : option B)
(function_parameter : Script_typed_ir.big_map)
: M? (Script_typed_ir.big_map × Alpha_context.context) :=
let
'(Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.key_type := key_type |}) as map :=
function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
let map := update_by_hash key_hash key_value value_value map in
return? (map, ctxt).
Definition get_and_update {A B : Set}
(ctxt : Alpha_context.context) (key_value : A) (value_value : option B)
(function_parameter : Script_typed_ir.big_map)
: M? ((option B × Script_typed_ir.big_map) × Alpha_context.context) :=
let
'(Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.key_type := key_type |}) as map :=
function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
let new_map := update_by_hash key_hash key_value value_value map in
let? '(old_value, ctxt) := (get_by_hash (B := A)) ctxt key_hash map in
return? ((old_value, new_map), ctxt).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Definition empty {a b : Set}
(key_type : Script_typed_ir.comparable_ty) (value_type : Script_typed_ir.ty)
: Script_typed_ir.big_map :=
Script_typed_ir.Big_map
{| Script_typed_ir.big_map.Big_map.id := None;
Script_typed_ir.big_map.Big_map.diff :=
({|
Script_typed_ir.big_map_overlay.map :=
Script_typed_ir.Big_map_overlay.(Map.S.empty);
Script_typed_ir.big_map_overlay.size := 0; |} :
Script_typed_ir.big_map_overlay a b);
Script_typed_ir.big_map.Big_map.key_type := key_type;
Script_typed_ir.big_map.Big_map.value_type := value_type; |}.
Definition mem {A : Set}
(ctxt : Alpha_context.context) (key_value : A)
(function_parameter : Script_typed_ir.big_map)
: M? (bool × Alpha_context.context) :=
let
'Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.id := id;
Script_typed_ir.big_map.Big_map.diff := diff_value;
Script_typed_ir.big_map.Big_map.key_type := key_type
|} := function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
match
((Script_typed_ir.Big_map_overlay.(Map.S.find) key_hash
diff_value.(Script_typed_ir.big_map_overlay.map)), id) with
| (None, None) ⇒ return? (false, ctxt)
| (None, Some id) ⇒
let? '(ctxt, res) := Alpha_context.Big_map.mem ctxt id key_hash in
return? (res, ctxt)
| (Some (_, None), _) ⇒ return? (false, ctxt)
| (Some (_, Some _), _) ⇒ return? (true, ctxt)
end.
Definition get_by_hash {A B : Set}
(ctxt : Alpha_context.context) (key_value : Script_expr_hash.t)
(big_map : Script_typed_ir.big_map) : M? (option A × Alpha_context.context) :=
let
'Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.id := id;
Script_typed_ir.big_map.Big_map.diff := diff_value;
Script_typed_ir.big_map.Big_map.value_type := value_type
|} := big_map in
let '[value_type, diff_value, id] :=
cast
[Script_typed_ir.ty ** Script_typed_ir.big_map_overlay B A **
option Alpha_context.Big_map.Id.t] [value_type, diff_value, id] in
match
((Script_typed_ir.Big_map_overlay.(Map.S.find) key_value
diff_value.(Script_typed_ir.big_map_overlay.map)), id) with
| (Some (_, x_value), _) ⇒ return? (x_value, ctxt)
| (None, None) ⇒ return? (None, ctxt)
| (None, Some id) ⇒
let? function_parameter := Alpha_context.Big_map.get_opt ctxt id key_value
in
match function_parameter with
| (ctxt, None) ⇒ return? (None, ctxt)
| (ctxt, Some value_value) ⇒
let? '(x_value, ctxt) :=
Script_ir_translator.parse_data
(Script_ir_translator_config.make None None true tt) ctxt true
value_type (Micheline.root_value value_value) in
return? ((Some x_value), ctxt)
end
end.
Definition get {A B : Set}
(ctxt : Alpha_context.context) (key_value : A)
(function_parameter : Script_typed_ir.big_map)
: M? (option B × Alpha_context.context) :=
let
'(Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.key_type := key_type |}) as map :=
function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
(get_by_hash (B := A)) ctxt key_hash map.
Definition update_by_hash {A B : Set}
(key_hash : Script_expr_hash.t) (key_value : A) (value_value : option B)
(big_map : Script_typed_ir.big_map) : Script_typed_ir.big_map :=
let 'Script_typed_ir.Big_map map := big_map in
let map := cast (Script_typed_ir.big_map.Big_map A B) map in
let contains :=
Script_typed_ir.Big_map_overlay.(Map.S.mem) key_hash
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.map)
in
Script_typed_ir.Big_map
(Script_typed_ir.big_map.Big_map.with_diff
{|
Script_typed_ir.big_map_overlay.map :=
Script_typed_ir.Big_map_overlay.(Map.S.add) key_hash
(key_value, value_value)
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.map);
Script_typed_ir.big_map_overlay.size :=
if contains then
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.size)
else
map.(Script_typed_ir.big_map.Big_map.diff).(Script_typed_ir.big_map_overlay.size)
+i 1; |} map).
Definition update {A B : Set}
(ctxt : Alpha_context.context) (key_value : A) (value_value : option B)
(function_parameter : Script_typed_ir.big_map)
: M? (Script_typed_ir.big_map × Alpha_context.context) :=
let
'(Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.key_type := key_type |}) as map :=
function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
let map := update_by_hash key_hash key_value value_value map in
return? (map, ctxt).
Definition get_and_update {A B : Set}
(ctxt : Alpha_context.context) (key_value : A) (value_value : option B)
(function_parameter : Script_typed_ir.big_map)
: M? ((option B × Script_typed_ir.big_map) × Alpha_context.context) :=
let
'(Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.key_type := key_type |}) as map :=
function_parameter in
let? '(key_hash, ctxt) :=
Script_ir_translator.hash_comparable_data ctxt key_type key_value in
let new_map := update_by_hash key_hash key_value value_value map in
let? '(old_value, ctxt) := (get_by_hash (B := A)) ctxt key_hash map in
return? ((old_value, new_map), ctxt).