Skip to main content

🗂️ Indexable.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.Cache_memory_helpers.

Inductive index_only : Set :=
| Index_only : index_only.

Inductive value_only : Set :=
| Value_only : value_only.

Inductive unknown : Set :=
| Unknown : unknown.

Inductive t (a : Set) : Set :=
| Value : a t a
| Hidden_value : a t a
| Index : int32 t a
| Hidden_index : int32 t a.

Arguments Value {_}.
Arguments Hidden_value {_}.
Arguments Index {_}.
Arguments Hidden_index {_}.

Init function; without side-effects in Coq
Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "indexable.index_cannot_be_negative" "Index of values cannot be negative"
    "A negative integer cannot be used as an index for a value."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (wrong_id : int32) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.No_precision
                (CamlinternalFormatBasics.String_literal
                  " cannot be used as an index because it is negative."
                  CamlinternalFormatBasics.End_of_format))
              "%ld cannot be used as an index because it is negative.") wrong_id))
    (Data_encoding.obj1
      (Data_encoding.req None None "wrong_index" Data_encoding.int32_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Index_cannot_be_negative" then
          let wrong_id := cast int32 payload in
          Some wrong_id
        else None
      end)
    (fun (wrong_id : int32) ⇒
      Build_extensible "Index_cannot_be_negative" int32 wrong_id).

Definition value (a : Set) : Set := t a.

Definition index (a : Set) : Set := t a.

Definition either (a : Set) : Set := t a.

Definition value_value {a : Set} (v_value : a) : value a := Value v_value.

Definition from_value {a : Set} (v_value : a) : either a :=
  Hidden_value v_value.

Definition index_value {a : Set} (i_value : int32) : M? (index a) :=
  if 0 i32 i_value then
    return? (Index i_value)
  else
    Error_monad.error_value
      (Build_extensible "Index_cannot_be_negative" int32 i_value).

Definition from_index {a : Set} (i_value : int32) : M? (either a) :=
  if 0 i32 i_value then
    return? (Hidden_index i_value)
  else
    Error_monad.error_value
      (Build_extensible "Index_cannot_be_negative" int32 i_value).

Definition index_exn {a : Set} (i_value : int32) : index a :=
  match index_value i_value with
  | Pervasives.Ok x_valuex_value
  | Pervasives.Error _
    Pervasives.raise
      (Build_extensible "Invalid_argument" string "Indexable.index_exn")
  end.

Definition from_index_exn {a : Set} (i_value : int32) : either a :=
  match from_index i_value with
  | Pervasives.Ok x_valuex_value
  | Pervasives.Error _
    Pervasives.raise
      (Build_extensible "Invalid_argument" string "Indexable.from_index_exn")
  end.

Definition destruct {a : Set} (function_parameter : t a)
  : Either.t (index a) a :=
  match function_parameter with
  | (Hidden_value x_value | Value x_value) ⇒ Either.Right x_value
  | (Hidden_index x_value | Index x_value) ⇒ Either.Left (Index x_value)
  end.

Definition forget {a : Set} (function_parameter : t a) : t a :=
  match function_parameter with
  | (Hidden_value x_value | Value x_value) ⇒ Hidden_value x_value
  | (Hidden_index x_value | Index x_value) ⇒ Hidden_index x_value
  end.

Definition to_int32 {A : Set} (function_parameter : t A) : int32 :=
  match function_parameter with
  | Index x_valuex_value
  | _unreachable_gadt_branch
  end.

Definition to_value {A : Set} (function_parameter : t A) : A :=
  match function_parameter with
  | Value x_valuex_value
  | _unreachable_gadt_branch
  end.

Definition is_value_e {trace a : Set} (error_value : trace) (v_value : t a)
  : Pervasives.result a trace :=
  match destruct v_value with
  | Either.Left _Result.error_value error_value
  | Either.Right v_valueResult.ok v_value
  end.

Definition compact {A : Set} (val_encoding : Data_encoding.encoding A)
  : Data_encoding.Compact.t (t A) :=
  Data_encoding.Compact.conv None
    (fun (function_parameter : t A) ⇒
      match function_parameter with
      | Hidden_index x_valueEither.Left x_value
      | Hidden_value x_valueEither.Right x_value
      | _unreachable_gadt_branch
      end)
    (fun (function_parameter : Either.t int32 A) ⇒
      match function_parameter with
      | Either.Left x_valueHidden_index x_value
      | Either.Right x_valueHidden_value x_value
      end) (Data_encoding.Compact.or_int32 "index" "value" None val_encoding).

Definition encoding {a : Set} (val_encoding : Data_encoding.t a)
  : Data_encoding.t (either a) :=
  Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
    (compact val_encoding).

Definition pp {a : Set}
  (ppv : Format.formatter a unit) (fmt : Format.formatter)
  (function_parameter : t a) : unit :=
  match function_parameter with
  | (Hidden_index x_value | Index x_value) ⇒
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Char_literal "" % char
          (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            CamlinternalFormatBasics.End_of_format)) "#%ld") x_value
  | (Hidden_value x_value | Value x_value) ⇒
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
        "%a") ppv x_value
  end.

Definition in_memory_size {a : Set}
  (ims : a Cache_memory_helpers.sint) (function_parameter : t a)
  : Cache_memory_helpers.sint :=
  match function_parameter with
  | (Hidden_value x_value | Value x_value) ⇒
    Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
        Cache_memory_helpers.word_size) (ims x_value)
  | (Hidden_index _ | Index _) ⇒
    Cache_memory_helpers.op_plusexclamation
      (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
        Cache_memory_helpers.word_size) Cache_memory_helpers.int32_size
  end.

Definition size_value {a : Set} (s_value : a int) (function_parameter : t a)
  : int :=
  match function_parameter with
  | (Hidden_value x_value | Value x_value) ⇒ 1 +i (s_value x_value)
  | (Hidden_index _ | Index _) ⇒ 1 +i 4
  end.

Definition compare {a : Set}
  (c_value : a a int) (x_value : t a) (y_value : t a) : int :=
  match (x_value, y_value) with
  |
    ((Hidden_index x_value | Index x_value),
      (Hidden_index y_value | Index y_value))
    Compare.Int32.(Compare.S.compare) x_value y_value
  |
    ((Hidden_value x_value | Value x_value),
      (Hidden_value y_value | Value y_value))c_value x_value y_value
  | ((Hidden_index _ | Index _), (Hidden_value _ | Value _)) ⇒ (-1)
  | ((Hidden_value _ | Value _), (Hidden_index _ | Index _)) ⇒ 1
  end.

Definition compare_values {a : Set}
  (c_value : a a int) (x_value : value a) (y_value : value a) : int :=
  match (x_value, y_value) with
  | (Value x_value, Value y_value)c_value x_value y_value
  | _unreachable_gadt_branch
  end.

Definition compare_indexes {a : Set} (x_value : index a) (y_value : index a)
  : int :=
  match (x_value, y_value) with
  | (Index x_value, Index y_value)
    Compare.Int32.(Compare.S.compare) x_value y_value
  | _unreachable_gadt_branch
  end.

Module VALUE.
  Record signature {t : Set} : Set := {
    t := t;
    encoding : Data_encoding.t t;
    compare : t t int;
    pp : Format.formatter t unit;
  }.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.

Module INDEXABLE.
  Record signature {v_t : Set} : Set := {
    v_t := v_t;
    t := t v_t;
    index := index v_t;
    value := value v_t;
    either := either v_t;
    value_value : v_t value;
    index_value : int32 M? index;
    index_exn : int32 index;
    compact : Data_encoding.Compact.t either;
    encoding : Data_encoding.t either;
    index_encoding : Data_encoding.t index;
    value_encoding : Data_encoding.t value;
    compare : t t int;
    compare_values : value value int;
    compare_indexes : index index int;
    pp : Format.formatter t unit;
  }.
End INDEXABLE.
Definition INDEXABLE := @INDEXABLE.signature.
Arguments INDEXABLE {_}.

Module Make.
  Class FArgs {V_t : Set} := {
    V : VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_}.

  Definition t `{FArgs} : Set := t V.(VALUE.t).

  Definition index `{FArgs} : Set := index V.(VALUE.t).

  Definition value `{FArgs} : Set := value V.(VALUE.t).

  Definition either `{FArgs} : Set := either V.(VALUE.t).

  Definition value_value `{FArgs} : V.(VALUE.t) value := value_value.

  Definition index_value `{FArgs} : int32 M? index := index_value.

  Definition index_exn `{FArgs} : int32 index := index_exn.

  Definition compact `{FArgs} : Data_encoding.Compact.t either :=
    compact V.(VALUE.encoding).

  Definition encoding `{FArgs} : Data_encoding.t either :=
    encoding V.(VALUE.encoding).

  Definition index_encoding `{FArgs} : Data_encoding.t index :=
    Data_encoding.conv
      (fun (function_parameter : index) ⇒
        match function_parameter with
        | Index x_valuex_value
        | _unreachable_gadt_branch
        end) (fun (x_value : int32) ⇒ Index x_value) None
      Data_encoding.int32_value.

  Definition value_encoding `{FArgs} : Data_encoding.t value :=
    Data_encoding.conv
      (fun (function_parameter : value) ⇒
        match function_parameter with
        | Value x_valuex_value
        | _unreachable_gadt_branch
        end) (fun (x_value : V.(VALUE.t)) ⇒ Value x_value) None
      V.(VALUE.encoding).

  Definition pp `{FArgs} (fmt : Format.formatter) (x_value : t) : unit :=
    pp V.(VALUE.pp) fmt x_value.

  Definition compare_values `{FArgs} : value value int :=
    compare_values V.(VALUE.compare).

  Definition compare_indexes `{FArgs} : index index int :=
    compare_indexes.

  Definition compare `{FArgs} (x_value : t) (y_value : t) : int :=
    compare V.(VALUE.compare) x_value y_value.

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      INDEXABLE.value_value := value_value;
      INDEXABLE.index_value := index_value;
      INDEXABLE.index_exn := index_exn;
      INDEXABLE.compact := compact;
      INDEXABLE.encoding := encoding;
      INDEXABLE.index_encoding := index_encoding;
      INDEXABLE.value_encoding := value_encoding;
      INDEXABLE.compare := compare;
      INDEXABLE.compare_values := compare_values;
      INDEXABLE.compare_indexes := compare_indexes;
      INDEXABLE.pp := pp
    |}.
End Make.
Definition Make {V_t : Set} (V : VALUE (t := V_t))
  : INDEXABLE (v_t := V.(VALUE.t)) :=
  let '_ := Make.Build_FArgs V in
  Make.functor.