🍬 Script_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.Gas_comparable_input_size.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Definition make {A B : Set}
  (x_value :
    {OPS_t : Set → Set @
      Script_typed_ir.Boxed_map (key := A) (value := B)
        (OPS_t := OPS_t)}) : Script_typed_ir.map A B :=
  Script_typed_ir.Map_tag x_value.

Definition get_module {A B : Set} (function_parameter : Script_typed_ir.map A B)
  : {OPS_t : Set → Set @
    Script_typed_ir.Boxed_map (key := A) (value := B)
      (OPS_t := OPS_t)} :=
  let 'Script_typed_ir.Map_tag x_value := function_parameter in
  x_value.

Definition empty_from {a b c : Set}
  (function_parameter : Script_typed_ir.map a b) : Script_typed_ir.map a c :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Script_typed_ir.Map_tag
    (existS (A := Set → Set) _ _
      (let key : Set := a in
      let value : Set := c in
      let OPS := Box.(Script_typed_ir.Boxed_map.OPS) in
      let boxed {D : Set}
        : Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.t)
          D :=
        OPS.(Script_typed_ir.Boxed_map_OPS.empty) in
      let size_value := 0 in
      let boxed_map_tag := tt in
      {|
        Script_typed_ir.Boxed_map.OPS := OPS;
        Script_typed_ir.Boxed_map.boxed := boxed;
        Script_typed_ir.Boxed_map.size_value := size_value;
        Script_typed_ir.Boxed_map.boxed_map_tag := boxed_map_tag
      |})).

Definition empty {a b : Set} (ty_value : Script_typed_ir.comparable_ty)
  : Script_typed_ir.map a b :=
  let OPS :=
    let key_size := Gas_comparable_input_size.size_of_comparable_value ty_value
      in
    let Map :=
      Map.Make
        (let t : Set := a in
        let compare := Script_comparable.compare_comparable ty_value in
        {|
          Compare.COMPARABLE.compare := compare
        |}) in
    let t (a : Set) : Set := Map.(Map.S.t) a in
    let key : Set := a in
    let empty {C : Set} : Map.(Map.S.t) C :=
      Map.(Map.S.empty) in
    let add {C : Set} : a → C → Map.(Map.S.t) C → Map.(Map.S.t) C :=
      Map.(Map.S.add) in
    let remove {C : Set} : a → Map.(Map.S.t) C → Map.(Map.S.t) C :=
      Map.(Map.S.remove) in
    let find {C : Set} : a → Map.(Map.S.t) C → option C :=
      Map.(Map.S.find) in
    let fold {C D : Set} : (a → C → D → D) → Map.(Map.S.t) C → D → D :=
      Map.(Map.S.fold) in
    let fold_es {C D E : Set}
      : (a → C → D → Pervasives.result D E) → Map.(Map.S.t) C → D →
      Pervasives.result D E :=
      Map.(Map.S.fold_es) in
    {|
      Script_typed_ir.Boxed_map_OPS.key_size := key_size;
      Script_typed_ir.Boxed_map_OPS.empty _ := empty;
      Script_typed_ir.Boxed_map_OPS.add _ := add;
      Script_typed_ir.Boxed_map_OPS.remove _ := remove;
      Script_typed_ir.Boxed_map_OPS.find _ := find;
      Script_typed_ir.Boxed_map_OPS.fold _ _ := fold;
      Script_typed_ir.Boxed_map_OPS.fold_es _ _ := fold_es
    |} in
  Script_typed_ir.Map_tag
    (existS (A := Set → Set) _ _
      (let key : Set := a in
      let value : Set := b in
      let OPS := OPS in
      let boxed {C : Set} : OPS.(Script_typed_ir.Boxed_map_OPS.t) C :=
        OPS.(Script_typed_ir.Boxed_map_OPS.empty) in
      let size_value := 0 in
      let boxed_map_tag := tt in
      {|
        Script_typed_ir.Boxed_map.OPS := OPS;
        Script_typed_ir.Boxed_map.boxed := boxed;
        Script_typed_ir.Boxed_map.size_value := size_value;
        Script_typed_ir.Boxed_map.boxed_map_tag := boxed_map_tag
      |})).

Definition get {key value : Set}
  (k_value : key) (function_parameter : Script_typed_ir.map key value)
  : option value :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.find)
    k_value Box.(Script_typed_ir.Boxed_map.boxed).

Definition update {a b : Set}
  (k_value : a) (v_value : option b)
  (function_parameter : Script_typed_ir.map a b) : Script_typed_ir.map a b :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  let '(boxed, size_value) :=
    let contains :=
      match
        Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.find)
          k_value Box.(Script_typed_ir.Boxed_map.boxed) with
      | None ⇒ false
      | _ ⇒ true
      end in
    match v_value with
    | Some v_value ⇒
      ((Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.add)
        k_value v_value Box.(Script_typed_ir.Boxed_map.boxed)),
        (Box.(Script_typed_ir.Boxed_map.size_value) +i
        (if contains then
          0
        else
          1)))
    | None ⇒
      ((Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.remove)
        k_value Box.(Script_typed_ir.Boxed_map.boxed)),
        (Box.(Script_typed_ir.Boxed_map.size_value) -i
        (if contains then
          1
        else
          0)))
    end in
  Script_typed_ir.Map_tag
    (existS (A := Set → Set) _ _
      (let key : Set := a in
      let value : Set := b in
      let OPS := Box.(Script_typed_ir.Boxed_map.OPS) in
      let boxed_map_tag := tt in
      {|
        Script_typed_ir.Boxed_map.OPS := OPS;
        Script_typed_ir.Boxed_map.boxed := boxed;
        Script_typed_ir.Boxed_map.size_value := size_value;
        Script_typed_ir.Boxed_map.boxed_map_tag := boxed_map_tag
      |})).

Definition mem {key value : Set}
  (k_value : key) (function_parameter : Script_typed_ir.map key value) : bool :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  match
    Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.find)
      k_value Box.(Script_typed_ir.Boxed_map.boxed) with
  | None ⇒ false
  | _ ⇒ true
  end.

Definition fold {key value acc : Set}
  (f_value : key → value → acc → acc)
  (function_parameter : Script_typed_ir.map key value) : acc → acc :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.fold)
    f_value Box.(Script_typed_ir.Boxed_map.boxed).

Definition fold_es {key value acc : Set}
  (f_value : key → value → acc → M? acc)
  (function_parameter : Script_typed_ir.map key value) : acc → M? acc :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.fold_es)
    f_value Box.(Script_typed_ir.Boxed_map.boxed).

Definition size_value {key value : Set}
  (function_parameter : Script_typed_ir.map key value) : Script_int.num :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  Script_int.abs (Script_int.of_int Box.(Script_typed_ir.Boxed_map.size_value)).

Definition map_es_in_context {context key value value' : Set}
  (f_value : context → key → value → M? (value' × context)) (ctxt : context)
  (function_parameter : Script_typed_ir.map key value)
  : M? (Script_typed_ir.map key value' × context) :=
  let 'Script_typed_ir.Map_tag Box := function_parameter in
  let 'existS _ _ Box := Box in
  let? '(map, ctxt) :=
    Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.fold_es)
      (fun (key_value : key) ⇒
        fun (value_value : value) ⇒
          fun (function_parameter :
            Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.t)
              value' × context) ⇒
            let '(map, ctxt) := function_parameter in
            let? '(value_value, ctxt) := f_value ctxt key_value value_value in
            return?
              ((Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.add)
                key_value value_value map), ctxt))
      Box.(Script_typed_ir.Boxed_map.boxed)
      (Box.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.empty),
        ctxt) in
  return?
    ((Script_typed_ir.Map_tag
      (existS (A := Set → Set) _ _
        (let key : Set := key in
        let value : Set := value' in
        let OPS := Box.(Script_typed_ir.Boxed_map.OPS) in
        let boxed := map in
        let size_value := Box.(Script_typed_ir.Boxed_map.size_value) in
        let boxed_map_tag := tt in
        {|
          Script_typed_ir.Boxed_map.OPS := OPS;
          Script_typed_ir.Boxed_map.boxed := boxed;
          Script_typed_ir.Boxed_map.size_value := size_value;
          Script_typed_ir.Boxed_map.boxed_map_tag := boxed_map_tag
        |}))), ctxt).