Skip to main content

🍬 Script_big_map.v

Translated OCaml

See proofs, 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.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).