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.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Carbonated_map_costs.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.

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

Module GAS.
  Record signature {context : Set} : Set := {
    context := context;
    consume : context Saturation_repr.t M? context;
  }.
End GAS.
Definition GAS := @GAS.signature.
Arguments GAS {_}.

Module COMPARABLE.
  Record signature {t : Set} : Set := {
    t := t;
    compare : t t int;
    
[compare_cost k] returns the cost of comparing the given key [k] with another value of the same type.
    compare_cost : t Saturation_repr.t;
  }.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.

Module S_builder.
  Record signature {t : Set Set} {key : Set} : Set := {
    t := t;
    key := key;
    Make :
       {G_context : Set},
       (G : GAS (context := G_context)),
      S (t := fun (a : Set) ⇒ t a) (key := key) (context := G.(GAS.context));
  }.
End S_builder.
Definition S_builder := @S_builder.signature.
Arguments S_builder {_ _}.

Module Make_builder.
  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.

  Module Make.
    Class FArgs `{FArgs} {G_context : Set} := {
      G : GAS (context := G_context);
    }.
    Arguments Build_FArgs {_ _ _}.

    Definition key `{FArgs} : Set := C.(COMPARABLE.t).

    Definition context `{FArgs} : Set := G.(GAS.context).

    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)
      : Carbonated_map_costs.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)
      : Carbonated_map_costs.cost :=
      Carbonated_map_costs.update_cost (C.(COMPARABLE.compare_cost) key_value)
        size_value.

    Definition find `{FArgs} {A : Set}
      (ctxt : G.(GAS.context)) (key_value : C.(COMPARABLE.t))
      (function_parameter : t A) : M? (option A × G.(GAS.context)) :=
      let '{| t.map := map; t.size := size_value |} := function_parameter in
      let? ctxt := G.(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 : G.(GAS.context)) (key_value : C.(COMPARABLE.t))
      (f_value : G.(GAS.context) option A M? (option A × G.(GAS.context)))
      (function_parameter : t A) : M? (t A × G.(GAS.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 := G.(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 := G.(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 := G.(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 := G.(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 : G.(GAS.context)) (function_parameter : t A)
      : M? (list (C.(COMPARABLE.t) × A) × G.(GAS.context)) :=
      let '{| t.map := map; t.size := size_value |} := function_parameter in
      let? ctxt :=
        G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
      return? ((M.(Map.S.bindings) map), ctxt).

    Definition add `{FArgs} {A : Set}
      (ctxt : G.(GAS.context))
      (merge_overlap : G.(GAS.context) A A M? (A × G.(GAS.context)))
      (key_value : C.(COMPARABLE.t)) (value_value : A)
      (function_parameter : t A) : M? (t A × G.(GAS.context)) :=
      let '{| t.map := map; t.size := size_value |} := function_parameter in
      let? ctxt := G.(GAS.consume) ctxt (find_cost key_value size_value) in
      let? ctxt := G.(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 : G.(GAS.context))
      (merge_overlap : G.(GAS.context) A A M? (A × G.(GAS.context)))
      (map : t A) (key_values : list (C.(COMPARABLE.t) × A))
      : M? (t A × G.(GAS.context)) :=
      let accum (function_parameter : t A × G.(GAS.context))
        : C.(COMPARABLE.t) × A M? (t A × G.(GAS.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 : G.(GAS.context))
      (merge_overlap : G.(GAS.context) A A M? (A × G.(GAS.context)))
      : list (C.(COMPARABLE.t) × A) M? (t A × G.(GAS.context)) :=
      add_key_values_to_map ctxt merge_overlap empty.

    Definition merge `{FArgs} {A : Set}
      (ctxt : G.(GAS.context))
      (merge_overlap : G.(GAS.context) A A M? (A × G.(GAS.context)))
      (map1 : t A) (function_parameter : t A) : M? (t A × G.(GAS.context)) :=
      let '{| t.map := map; t.size := size_value |} := function_parameter in
      let? ctxt :=
        G.(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 × G.(GAS.context)) ⇒
              let '(map, ctxt) := function_parameter in
              add ctxt merge_overlap key_value value_value map) map (map1, ctxt).

    Definition fold_e `{FArgs} {A B : Set}
      (ctxt : G.(GAS.context))
      (f_value :
        G.(GAS.context) A C.(COMPARABLE.t) B
        M? (A × G.(GAS.context))) (empty : A) (function_parameter : t B)
      : M? (A × G.(GAS.context)) :=
      let '{| t.map := map; t.size := size_value |} := function_parameter in
      let? ctxt :=
        G.(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 × G.(GAS.context)) ⇒
              let '(acc_value, ctxt) := function_parameter in
              f_value ctxt acc_value key_value value_value) map (empty, ctxt).

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

    Definition map_e `{FArgs} {A B : Set}
      (ctxt : G.(GAS.context))
      (f_value :
        G.(GAS.context) C.(COMPARABLE.t) A M? (B × G.(GAS.context)))
      (function_parameter : t A) : M? (t B × G.(GAS.context)) :=
      let '{| t.map := map; t.size := size_value |} := function_parameter in
      let? '(map, ctxt) :=
        fold_e ctxt
          (fun (ctxt : G.(GAS.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 :=
                    G.(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_e _ _ := map_e;
        S.fold_e _ _ := fold_e;
        S.fold_es _ _ := fold_es
      |}.
  End Make.
  Definition Make `{FArgs} {G_context : Set} (G : GAS (context := G_context))
    : S (t := fun (a : Set) ⇒ t a) (key := C.(COMPARABLE.t))
      (context := G.(GAS.context)) :=
    let '_ := Make.Build_FArgs G in
    Make.functor.

  (* Make_builder *)
  Definition functor `{FArgs} :=
    {|
      S_builder.Make _ := Make
    |}.
End Make_builder.
Definition Make_builder {C_t : Set} (C : COMPARABLE (t := C_t))
  : S_builder (t := _) (key := C.(COMPARABLE.t)) :=
  let '_ := Make_builder.Build_FArgs C in
  Make_builder.functor.

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

  Definition M `{FArgs} := Make_builder C.

  Definition t `{FArgs} (a : Set) : Set := M.(S_builder.t) a.

  Definition M_Make_include `{FArgs} := M.(S_builder.Make) G.

Inclusion of the module [M_Make_include]
  Definition key `{FArgs} := M_Make_include.(S.key).

  Definition context `{FArgs} := M_Make_include.(S.context).

  Definition empty `{FArgs} {a : Set} := M_Make_include.(S.empty) (a := a).

  Definition singleton `{FArgs} {a : Set} :=
    M_Make_include.(S.singleton) (a := a).

  Definition size_value `{FArgs} {a : Set} :=
    M_Make_include.(S.size_value) (a := a).

  Definition find `{FArgs} {a : Set} := M_Make_include.(S.find) (a := a).

  Definition update `{FArgs} {a : Set} := M_Make_include.(S.update) (a := a).

  Definition to_list `{FArgs} {a : Set} := M_Make_include.(S.to_list) (a := a).

  Definition of_list `{FArgs} {a : Set} := M_Make_include.(S.of_list) (a := a).

  Definition merge `{FArgs} {a : Set} := M_Make_include.(S.merge) (a := a).

  Definition map_e `{FArgs} {a b : Set} :=
    M_Make_include.(S.map_e) (a := a) (b := b).

  Definition fold_e `{FArgs} {state value : Set} :=
    M_Make_include.(S.fold_e) (state := state) (value := value).

  Definition fold_es `{FArgs} {state value : Set} :=
    M_Make_include.(S.fold_es) (state := state) (value := value).

  (* 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_e _ _ := map_e;
      S.fold_e _ _ := fold_e;
      S.fold_es _ _ := fold_es
    |}.
End Make.
Definition Make {G_context C_t : Set}
  (G : GAS (context := G_context)) (C : COMPARABLE (t := C_t))
  : S (t := _) (key := C.(COMPARABLE.t)) (context := G.(GAS.context)) :=
  let '_ := Make.Build_FArgs G C in
  Make.functor.