Skip to main content

🔥 Carbonated_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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Carbonated_map_costs.

Module S.
  Record signature {t : Set Set} {key : Set} : Set := {
    t := t;
    key := key;
    empty : {a : Set}, t a;
    singleton : {a : Set}, key a t a;
    size_value : {a : Set}, t a int;
    find :
       {a : Set},
      Alpha_context.context key t a
      M? (option a × Alpha_context.context);
    update :
       {a : Set},
      Alpha_context.context key
      (Alpha_context.context option a
      M? (option a × Alpha_context.context)) t a
      M? (t a × Alpha_context.context);
    to_list :
       {a : Set},
      Alpha_context.context t a
      M? (list (key × a) × Alpha_context.context);
    of_list :
       {a : Set},
      Alpha_context.context
      (Alpha_context.context a a M? (a × Alpha_context.context))
      list (key × a) M? (t a × Alpha_context.context);
    merge :
       {a : Set},
      Alpha_context.context
      (Alpha_context.context a a M? (a × Alpha_context.context))
      t a t a M? (t a × Alpha_context.context);
    map :
       {a b : Set},
      Alpha_context.context
      (Alpha_context.context key a M? (b × Alpha_context.context))
      t a M? (t b × Alpha_context.context);
    fold :
       {state value : Set},
      Alpha_context.context
      (Alpha_context.context state key value
      M? (state × Alpha_context.context)) state t value
      M? (state × Alpha_context.context);
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _}.

Module COMPARABLE.
  Record signature {t : Set} : Set := {
    t := t;
    compare : t t int;
    compare_cost : t Alpha_context.Gas.cost;
  }.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.

Module Make.
  Class FArgs {C_t : Set} := {
    C : COMPARABLE (t := C_t);
  }.
  Arguments Build_FArgs {_}.

  Definition M `{FArgs} :=
    Map.Make
      {|
        Compare.COMPARABLE.compare := C.(COMPARABLE.compare)
      |}.

  Module t.
    Record record `{FArgs} {a : Set} : Set := Build {
      map : M.(Map.S.t) a;
      size : int;
    }.
    Arguments record {_ _}.
    Definition with_map `{FArgs} {t_a} map (r : record t_a) :=
      Build _ _ t_a map r.(size).
    Definition with_size `{FArgs} {t_a} size (r : record t_a) :=
      Build _ _ t_a r.(map) size.
  End t.
  Definition t `{FArgs} := t.record.

  Definition empty `{FArgs} {A : Set} : t A :=
    {| t.map := M.(Map.S.empty); t.size := 0; |}.

  Definition singleton `{FArgs} {A : Set}
    (key_value : C.(COMPARABLE.t)) (value_value : A) : t A :=
    {| t.map := M.(Map.S.singleton) key_value value_value; t.size := 1; |}.

  Definition size_value `{FArgs} {A : Set} (function_parameter : t A) : int :=
    let '{| t.size := size_value |} := function_parameter in
    size_value.

  Definition find_cost `{FArgs}
    (key_value : C.(COMPARABLE.t)) (size_value : int)
    : Alpha_context.Gas.cost :=
    Carbonated_map_costs.find_cost (C.(COMPARABLE.compare_cost) key_value)
      size_value.

  Definition update_cost `{FArgs}
    (key_value : C.(COMPARABLE.t)) (size_value : int)
    : Alpha_context.Gas.cost :=
    Carbonated_map_costs.update_cost (C.(COMPARABLE.compare_cost) key_value)
      size_value.

  Definition find `{FArgs} {A : Set}
    (ctxt : Alpha_context.context) (key_value : C.(COMPARABLE.t))
    (function_parameter : t A) : M? (option A × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let? ctxt := Alpha_context.Gas.consume ctxt (find_cost key_value size_value)
      in
    return? ((M.(Map.S.find) key_value map), ctxt).

  Definition update `{FArgs} {A : Set}
    (ctxt : Alpha_context.context) (key_value : C.(COMPARABLE.t))
    (f_value :
      Alpha_context.context option A M? (option A × Alpha_context.context))
    (function_parameter : t A) : M? (t A × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let find_cost := find_cost key_value size_value in
    let update_cost := update_cost key_value size_value in
    let? ctxt := Alpha_context.Gas.consume ctxt find_cost in
    let old_val_opt := M.(Map.S.find) key_value map in
    let? '(new_val_opt, ctxt) := f_value ctxt old_val_opt in
    match (old_val_opt, new_val_opt) with
    | (Some _, Some new_val)
      let? ctxt := Alpha_context.Gas.consume ctxt update_cost in
      return?
        ({| t.map := M.(Map.S.add) key_value new_val map; t.size := size_value;
          |}, ctxt)
    | (Some _, None)
      let? ctxt := Alpha_context.Gas.consume ctxt update_cost in
      return?
        ({| t.map := M.(Map.S.remove) key_value map; t.size := size_value -i 1;
          |}, ctxt)
    | (None, Some new_val)
      let? ctxt := Alpha_context.Gas.consume ctxt update_cost in
      return?
        ({| t.map := M.(Map.S.add) key_value new_val map;
          t.size := size_value +i 1; |}, ctxt)
    | (None, None)return? ({| t.map := map; t.size := size_value; |}, ctxt)
    end.

  Definition to_list `{FArgs} {A : Set}
    (ctxt : Alpha_context.context) (function_parameter : t A)
    : M? (list (C.(COMPARABLE.t) × A) × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let? ctxt :=
      Alpha_context.Gas.consume ctxt (Carbonated_map_costs.fold_cost size_value)
      in
    return? ((M.(Map.S.bindings) map), ctxt).

  Definition add `{FArgs} {A : Set}
    (ctxt : Alpha_context.context)
    (merge_overlap :
      Alpha_context.context A A M? (A × Alpha_context.context))
    (key_value : C.(COMPARABLE.t)) (value_value : A) (function_parameter : t A)
    : M? (t A × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let? ctxt := Alpha_context.Gas.consume ctxt (find_cost key_value size_value)
      in
    let? ctxt :=
      Alpha_context.Gas.consume ctxt (update_cost key_value size_value) in
    match M.(Map.S.find) key_value map with
    | Some old_val
      let? '(new_value, ctxt) := merge_overlap ctxt old_val value_value in
      return?
        ({| t.map := M.(Map.S.add) key_value new_value map;
          t.size := size_value; |}, ctxt)
    | None
      Pervasives.Ok
        ({| t.map := M.(Map.S.add) key_value value_value map;
          t.size := size_value +i 1; |}, ctxt)
    end.

  Definition add_key_values_to_map `{FArgs} {A : Set}
    (ctxt : Alpha_context.context)
    (merge_overlap :
      Alpha_context.context A A M? (A × Alpha_context.context))
    (map : t A) (key_values : list (C.(COMPARABLE.t) × A))
    : M? (t A × Alpha_context.context) :=
    let accum (function_parameter : t A × Alpha_context.context)
      : C.(COMPARABLE.t) × A M? (t A × Alpha_context.context) :=
      let '(map, ctxt) := function_parameter in
      fun (function_parameter : C.(COMPARABLE.t) × A) ⇒
        let '(key_value, value_value) := function_parameter in
        add ctxt merge_overlap key_value value_value map in
    List.fold_left_e accum (map, ctxt) key_values.

  Definition of_list `{FArgs} {A : Set}
    (ctxt : Alpha_context.context)
    (merge_overlap :
      Alpha_context.context A A M? (A × Alpha_context.context))
    : list (C.(COMPARABLE.t) × A) M? (t A × Alpha_context.context) :=
    add_key_values_to_map ctxt merge_overlap empty.

  Definition merge `{FArgs} {A : Set}
    (ctxt : Alpha_context.context)
    (merge_overlap :
      Alpha_context.context A A M? (A × Alpha_context.context))
    (map1 : t A) (function_parameter : t A)
    : M? (t A × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let? ctxt :=
      Alpha_context.Gas.consume ctxt (Carbonated_map_costs.fold_cost size_value)
      in
    M.(Map.S.fold_e)
      (fun (key_value : C.(COMPARABLE.t)) ⇒
        fun (value_value : A) ⇒
          fun (function_parameter : t A × Alpha_context.context) ⇒
            let '(map, ctxt) := function_parameter in
            add ctxt merge_overlap key_value value_value map) map (map1, ctxt).

  Definition fold `{FArgs} {A B : Set}
    (ctxt : Alpha_context.context)
    (f_value :
      Alpha_context.context A C.(COMPARABLE.t) B
      M? (A × Alpha_context.context)) (empty : A) (function_parameter : t B)
    : M? (A × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let? ctxt :=
      Alpha_context.Gas.consume ctxt (Carbonated_map_costs.fold_cost size_value)
      in
    M.(Map.S.fold_e)
      (fun (key_value : C.(COMPARABLE.t)) ⇒
        fun (value_value : B) ⇒
          fun (function_parameter : A × Alpha_context.context) ⇒
            let '(acc_value, ctxt) := function_parameter in
            f_value ctxt acc_value key_value value_value) map (empty, ctxt).

  Definition map `{FArgs} {A B : Set}
    (ctxt : Alpha_context.context)
    (f_value :
      Alpha_context.context C.(COMPARABLE.t) A
      M? (B × Alpha_context.context)) (function_parameter : t A)
    : M? (t B × Alpha_context.context) :=
    let '{| t.map := map; t.size := size_value |} := function_parameter in
    let? '(map, ctxt) :=
      fold ctxt
        (fun (ctxt : Alpha_context.context) ⇒
          fun (map : M.(Map.S.t) B) ⇒
            fun (key_value : C.(COMPARABLE.t)) ⇒
              fun (value_value : A) ⇒
                let? '(value_value, ctxt) := f_value ctxt key_value value_value
                  in
                let? ctxt :=
                  Alpha_context.Gas.consume ctxt
                    (update_cost key_value size_value) in
                return? ((M.(Map.S.add) key_value value_value map), ctxt))
        M.(Map.S.empty) {| t.map := map; t.size := size_value; |} in
    return? ({| t.map := map; t.size := size_value; |}, ctxt).

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      S.empty _ := empty;
      S.singleton _ := singleton;
      S.size_value _ := size_value;
      S.find _ := find;
      S.update _ := update;
      S.to_list _ := to_list;
      S.of_list _ := of_list;
      S.merge _ := merge;
      S.map _ _ := map;
      S.fold _ _ := fold
    |}.
End Make.
Definition Make {C_t : Set} (C : COMPARABLE (t := C_t))
  : S (t := _) (key := C.(COMPARABLE.t)) :=
  let '_ := Make.Build_FArgs C in
  Make.functor.