Skip to main content

πŸƒΒ Data_encoding.v

Environment

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.Variant.

Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Either.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require TezosOfOCaml.Environment.Structs.V0.Z.

Inductive json : Set :=
| Bool : bool β†’ json
| Null : json
| O : list (string Γ— json) β†’ json
| Float : float β†’ json
| String : string β†’ json
| A : list json β†’ json.

Parameter json_schema : Set.

Parameter t : βˆ€ (a : Set), Set.

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

Inductive string_json_repr : Set :=
| Hex : string_json_repr
| Plain : string_json_repr.

Parameter classify : βˆ€ {a : Set}, encoding a β†’ Variant.t.

Parameter splitted : βˆ€ {a : Set}, encoding a β†’ encoding a β†’ encoding a.

Parameter null : encoding unit.

Parameter empty : encoding unit.

Parameter unit_value : encoding unit.

Parameter constant : string β†’ encoding unit.

Parameter int8 : encoding int.

Parameter uint8 : encoding int.

Parameter int16 : encoding int.

Parameter uint16 : encoding int.

Parameter int31 : encoding int.

Parameter int32_value : encoding int32.

Parameter int64_value : encoding int64.

Parameter ranged_int : int β†’ int β†’ encoding int.

Parameter z_value : encoding Z.t.

Parameter n_value : encoding Z.t.

Parameter uint_like_n : option int β†’ unit β†’ encoding int.

Parameter int_like_z : option int β†’ option int β†’ unit β†’ encoding int.

Parameter bool_value : encoding bool.

Parameter string' : option Variant.t β†’ string_json_repr β†’ encoding string.

Parameter bytes' : option Variant.t β†’ string_json_repr β†’ encoding Bytes.t.

Parameter string_value : encoding string.

Parameter bytes_value : encoding bytes.

Parameter option_value : βˆ€ {a : Set},
  encoding a β†’ encoding (option a).

Parameter result_value : βˆ€ {a b : Set},
  encoding a β†’ encoding b β†’ encoding (Pervasives.result a b).

Parameter array_value : βˆ€ {a : Set},
  option int β†’ encoding a β†’ encoding (array a).

Parameter list_value : βˆ€ {a : Set},
  option int β†’ encoding a β†’ encoding (list a).

Parameter list_with_length : βˆ€ {a : Set},
  option int β†’ Variant.t β†’ encoding a β†’ encoding (list a).

Parameter conv : βˆ€ {a b : Set},
  (a β†’ b) β†’ (b β†’ a) β†’ option json_schema β†’ encoding b β†’ encoding a.

Parameter conv_with_guard : βˆ€ {a b : Set},
  (a β†’ b) β†’ (b β†’ Pervasives.result a string) β†’ option json_schema β†’
  encoding b β†’ encoding a.

Parameter with_decoding_guard : βˆ€ {a : Set},
  (a β†’ Pervasives.result unit string) β†’ encoding a β†’ encoding a.

Parameter assoc : βˆ€ {a : Set},
  encoding a β†’ encoding (list (string Γ— a)).

Parameter dynamic_size : βˆ€ {a : Set},
  option Variant.t β†’ encoding a β†’ encoding a.

Parameter json_value : encoding json.

Parameter json_schema_value : encoding json_schema.

Parameter field : βˆ€ (a : Set), Set.

Parameter req : βˆ€ {t : Set},
  option string β†’ option string β†’ string β†’ encoding t β†’ field t.

Parameter opt : βˆ€ {t : Set},
  option string β†’ option string β†’ string β†’ encoding t β†’ field (option t).

Parameter varopt : βˆ€ {t : Set},
  option string β†’ option string β†’ string β†’ encoding t β†’ field (option t).

Parameter dft : βˆ€ {t : Set},
  option string β†’ option string β†’ string β†’ encoding t β†’ t β†’ field t.

Parameter obj1 : βˆ€ {f1 : Set}, field f1 β†’ encoding f1.

Parameter obj2 : βˆ€ {f1 f2 : Set},
  field f1 β†’ field f2 β†’ encoding (f1 Γ— f2).

Parameter obj3 : βˆ€ {f1 f2 f3 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ encoding (f1 Γ— f2 Γ— f3).

Parameter obj4 : βˆ€ {f1 f2 f3 f4 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4).

Parameter obj5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

Parameter obj6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

Parameter obj7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
  field f7 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

Parameter obj8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
  field f7 β†’ field f8 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

Parameter obj9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
  field f7 β†’ field f8 β†’ field f9 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

Parameter obj10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
  field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
  field f7 β†’ field f8 β†’ field f9 β†’ field f10 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

Parameter merge_objs : βˆ€ {o1 o2 : Set},
  encoding o1 β†’ encoding o2 β†’ encoding (o1 Γ— o2).

Module With_field_name_duplicate_checks.
  Parameter obj1 : βˆ€ {f1 : Set}, field f1 β†’ encoding f1.

  Parameter obj2 : βˆ€ {f1 f2 : Set},
    field f1 β†’ field f2 β†’ encoding (f1 Γ— f2).

  Parameter obj3 : βˆ€ {f1 f2 f3 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ encoding (f1 Γ— f2 Γ— f3).

  Parameter obj4 : βˆ€ {f1 f2 f3 f4 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4).

  Parameter obj5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

  Parameter obj6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

  Parameter obj7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

  Parameter obj8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

  Parameter obj9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ field f9 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

  Parameter obj10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ field f9 β†’ field f10 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

  Parameter merge_objs : βˆ€ {o1 o2 : Set},
    encoding o1 β†’ encoding o2 β†’ encoding (o1 Γ— o2).
End With_field_name_duplicate_checks.

Parameter tup1 : βˆ€ {f1 : Set}, encoding f1 β†’ encoding f1.

Parameter tup2 : βˆ€ {f1 f2 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding (f1 Γ— f2).

Parameter tup3 : βˆ€ {f1 f2 f3 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding (f1 Γ— f2 Γ— f3).

Parameter tup4 : βˆ€ {f1 f2 f3 f4 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4).

Parameter tup5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

Parameter tup6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
  encoding f6 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

Parameter tup7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
  encoding f6 β†’ encoding f7 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

Parameter tup8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
  encoding f6 β†’ encoding f7 β†’ encoding f8 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

Parameter tup9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
  encoding f6 β†’ encoding f7 β†’ encoding f8 β†’ encoding f9 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

Parameter tup10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
  encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
  encoding f6 β†’ encoding f7 β†’ encoding f8 β†’ encoding f9 β†’ encoding f10 β†’
  encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

Parameter merge_tups : βˆ€ {a1 a2 : Set},
  encoding a1 β†’ encoding a2 β†’ encoding (a1 Γ— a2).

Parameter case : βˆ€ (t : Set), Set.

Inductive case_tag : Set :=
| Tag : int β†’ case_tag
| Json_only : case_tag.

Parameter match_result : Set.

Definition matching_function (a : Set) : Set := a β†’ match_result.

Parameter matched : βˆ€ {a : Set},
  option Variant.t β†’ int β†’ encoding a β†’ a β†’ match_result.

Parameter case_value : βˆ€ {a t : Set},
  string β†’ option string β†’ case_tag β†’ encoding a β†’ (t β†’ option a) β†’
  (a β†’ t) β†’ case t.

Parameter matching : βˆ€ {t : Set},
  option Variant.t β†’ matching_function t β†’ list (case t) β†’ encoding t.

Parameter union : βˆ€ {t : Set},
  option Variant.t β†’ list (case t) β†’ encoding t.

Module With_JSON_discriminant.
  Inductive case_tag : Set :=
  | Tag : int Γ— string β†’ case_tag.

  Parameter case : βˆ€ (t : Set), Set.

  Parameter case_value : βˆ€ {a t : Set},
    string β†’ option string β†’ case_tag β†’ encoding a β†’ (t β†’ option a) β†’
    (a β†’ t) β†’ case t.

  Parameter matched : βˆ€ {a : Set},
    option Variant.t β†’ int Γ— string β†’ encoding a β†’ a β†’ match_result.

  Parameter matching : βˆ€ {t : Set},
    option Variant.t β†’ matching_function t β†’ list (case t) β†’ encoding t.

  Parameter union : βˆ€ {t : Set},
    option Variant.t β†’ list (case t) β†’ encoding t.
End With_JSON_discriminant.

Parameter string_enum : βˆ€ {a : Set}, list (string Γ— a) β†’ encoding a.

Module Fixed.
  Parameter string_value : int β†’ encoding string.

  Parameter string' : string_json_repr β†’ int β†’ encoding string.

  Parameter bytes_value : int β†’ encoding Bytes.t.

  Parameter bytes' : string_json_repr β†’ int β†’ encoding Bytes.t.

  Parameter add_padding : βˆ€ {a : Set}, encoding a β†’ int β†’ encoding a.

  Parameter list_value : βˆ€ {a : Set},
    int β†’ encoding a β†’ encoding (list a).

  Parameter array_value : βˆ€ {a : Set},
    int β†’ encoding a β†’ encoding (array a).
End Fixed.

Module _Variable.
  Parameter string_value : encoding string.

  Parameter string' : string_json_repr β†’ encoding string.

  Parameter bytes_value : encoding Bytes.t.

  Parameter bytes' : string_json_repr β†’ encoding Bytes.t.

  Parameter array_value : βˆ€ {a : Set},
    option int β†’ encoding a β†’ encoding (array a).

  Parameter list_value : βˆ€ {a : Set},
    option int β†’ encoding a β†’ encoding (list a).
End _Variable.

Module Bounded.
  Parameter string' :
    option Variant.t β†’ string_json_repr β†’ int β†’ encoding string.

  Parameter string_value : int β†’ encoding string.

  Parameter bytes' :
    option Variant.t β†’ string_json_repr β†’ int β†’ encoding Bytes.t.

  Parameter bytes_value : int β†’ encoding Bytes.t.
End Bounded.

Inductive tag_size : Set :=
| Uint16 : tag_size
| Uint8 : tag_size.

Parameter def : βˆ€ {t : Set},
  string β†’ option string β†’ option string β†’ encoding t β†’ encoding t.

Parameter mu : βˆ€ {a : Set},
  string β†’ option string β†’ option string β†’ (encoding a β†’ encoding a) β†’
  encoding a.

Module Lazy.
  Inductive t (a : Set) : Set :=
  | Both : bytes β†’ a β†’ t a
  | Bytes : bytes β†’ t a
  | Value : a β†’ t a.

  Arguments Both {_}.
  Arguments Bytes {_}.
  Arguments Value {_}.
End Lazy.

Definition lazy_t : βˆ€ (a : Set), Set := Lazy.t.

Parameter lazy_encoding : βˆ€ {a : Set}, encoding a β†’ encoding (lazy_t a).

Parameter force_decode : βˆ€ {a : Set}, lazy_t a β†’ option a.

Parameter force_bytes : βˆ€ {a : Set}, lazy_t a β†’ bytes.

Parameter make_lazy : βˆ€ {a : Set}, encoding a β†’ a β†’ lazy_t a.

Definition apply_lazy {a b : Set}
  (fun_value : a β†’ b) (fun_bytes : bytes β†’ b) (fun_combine : b β†’ b β†’ b)
  (le : lazy_t a) : b :=
  match le with
  | Lazy.Both bytes value β‡’ fun_combine (fun_value value) (fun_bytes bytes)
  | Lazy.Bytes bytes β‡’ fun_bytes bytes
  | Lazy.Value value β‡’ fun_value value
  end.

Module Json.
  Parameter schema : βˆ€ {a : Set},
    option string β†’ encoding a β†’ json_schema.

  Parameter construct : βˆ€ {t : Set},
    option Variant.t β†’ encoding t β†’ t β†’ json.

  Parameter destruct : βˆ€ {t : Set},
    option bool β†’ encoding t β†’ json β†’ t.

  Reserved Notation "'path".

  Inductive path_item : Set :=
  | Index : int β†’ path_item
  | Field : string β†’ path_item
  | Next : path_item
  | Star : path_item
  
  where "'path" := (list path_item).

  Definition path := 'path.

  Parameter print_error :
    option (Format.formatter β†’ extensible_type β†’ unit) β†’
    Format.formatter β†’ extensible_type β†’ unit.

  Parameter cannot_destruct : βˆ€ {a b : Set},
    Pervasives.format4 a Format.formatter unit b β†’ a.

  Definition wrap_error {a b : Set} (f : a β†’ b) (x : a) : b :=
    f x.

  Parameter pp : Format.formatter β†’ json β†’ unit.
End Json.

Module Binary.
  Parameter fixed_length : βˆ€ {a : Set}, encoding a β†’ option int.

  Parameter maximum_length : βˆ€ {a : Set}, encoding a β†’ option int.

  Parameter length : βˆ€ {a : Set}, encoding a β†’ a β†’ int.

  Parameter to_bytes_opt : βˆ€ {a : Set},
    option int β†’ encoding a β†’ a β†’ option bytes.

  Definition to_bytes_exn {a : Set} (buffer_size : option int)
    (encoding : encoding a) (value : a) : bytes :=
    match to_bytes_opt buffer_size encoding value with
    | Some bytes β‡’ bytes
    | None β‡’ axiom
    end.

  Parameter of_bytes_opt : βˆ€ {a : Set}, encoding a β†’ bytes β†’ option a.

  Parameter to_string_opt : βˆ€ {a : Set},
    option int β†’ encoding a β†’ a β†’ option string.

  Parameter to_string_exn : βˆ€ {a : Set},
    option int β†’ encoding a β†’ a β†’ string.

  Parameter of_string_opt : βˆ€ {a : Set},
    encoding a β†’ string β†’ option a.
End Binary.

Parameter check_size : βˆ€ {a : Set}, int β†’ encoding a β†’ encoding a.

Module Compact.
  Parameter t : βˆ€ (a : Set), Set.

  Parameter make : βˆ€ {a : Set}, option Variant.t β†’ t a β†’ encoding a.

  Parameter tag_bit_count : βˆ€ {a : Set}, t a β†’ int.

  Definition void := Empty_set.

  Parameter void_value : t void.

  Definition refute {a : Set} (v : void) : a :=
    match v with end.

  Parameter unit_value : t unit.

  Parameter null : t unit.

  Parameter bool_value : t bool.

  Parameter payload : βˆ€ {a : Set}, encoding a β†’ t a.

  Parameter option_value : βˆ€ {a : Set}, t a β†’ t (option a).

  Parameter conv : βˆ€ {a b : Set},
    option (encoding a) β†’ (a β†’ b) β†’ (b β†’ a) β†’ t b β†’ t a.

  Parameter tup1 : βˆ€ {a : Set}, t a β†’ t a.

  Parameter tup2 : βˆ€ {a b : Set}, t a β†’ t b β†’ t (a Γ— b).

  Parameter tup3 : βˆ€ {a b c : Set}, t a β†’ t b β†’ t c β†’ t (a Γ— b Γ— c).

  Parameter tup4 : βˆ€ {a b c d : Set},
    t a β†’ t b β†’ t c β†’ t d β†’ t (a Γ— b Γ— c Γ— d).

  Parameter tup5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
    t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

  Parameter tup6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
    t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

  Parameter tup7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
    t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

  Parameter tup8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’ t f8 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

  Parameter tup9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’ t f8 β†’ t f9 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

  Parameter tup10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’ t f8 β†’ t f9 β†’
    t f10 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

  Parameter field : βˆ€ (a : Set), Set.

  Parameter req : βˆ€ {a : Set}, string β†’ t a β†’ field a.

  Parameter opt : βˆ€ {a : Set}, string β†’ t a β†’ field (option a).

  Parameter obj1 : βˆ€ {a : Set}, field a β†’ t a.

  Parameter obj2 : βˆ€ {a b : Set}, field a β†’ field b β†’ t (a Γ— b).

  Parameter obj3 : βˆ€ {a b c : Set},
    field a β†’ field b β†’ field c β†’ t (a Γ— b Γ— c).

  Parameter obj4 : βˆ€ {a b c d : Set},
    field a β†’ field b β†’ field c β†’ field d β†’ t (a Γ— b Γ— c Γ— d).

  Parameter obj5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

  Parameter obj6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

  Parameter obj7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

  Parameter obj8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

  Parameter obj9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ field f9 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

  Parameter obj10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ field f9 β†’ field f10 β†’
    t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

  Parameter int32_value : t int32.

  Parameter int64_value : t int64.

  Parameter list_value : βˆ€ {a : Set}, int β†’ encoding a β†’ t (list a).

  Parameter case : βˆ€ (a : Set), Set.

  Parameter case_value : βˆ€ {a b : Set},
    string β†’ option string β†’ t b β†’ (a β†’ option b) β†’ (b β†’ a) β†’ case a.

  Parameter union : βˆ€ {a : Set},
    option int β†’ option int β†’ list (case a) β†’ t a.

  Parameter void_case : βˆ€ {a : Set}, string β†’ case a.

  Parameter or_int32 : βˆ€ {a : Set},
    string β†’ string β†’ option string β†’ encoding a β†’ t (Either.t int32 a).

  Module Custom.
    Definition tag : Set := int.

    Parameter join_tags : list (tag Γ— int) β†’ tag.

    Module S.
      Record signature {input layout : Set} : Set := {
        
The type of [input] this module allows to encode.
        input := input;
        
The various ways to efficiently encode [input].
        layout := layout;
        
The list of layouts available to encode [input].
        layouts : list layout;
        
The number of bits necessary to distinguish between the various layouts.
        tag_len : int;
        
[tag layout] computes the tag of {!Data_encoding.union} to be used to encode values classified as [layout].
{b Warning:} It is expected that [tag layout < 2^tag_len - 1].
        tag : layout β†’ tag;
        
[partial_encoding layout] returns the encoding to use for values classified as [layout].
This encoding can be partial in the sense that it may fail (it will raise an [Invalid_argument]) for some values of [x]. However, it is expected that [partial_encoding (classify x) x] will always succeed.
        partial_encoding : layout β†’ encoding input;
        
[classify x] returns the layout to be used to encode [x].
        classify : input β†’ layout;
        
The encoding to use when targeting a JSON output.
        json_encoding : encoding input;
      }.
    End S.
    Definition S := @S.signature.
    Arguments S {_ _}.

    Parameter make : βˆ€ {a : Set},
      {layout : Set @ S (input := a) (layout := layout)} β†’ t a.
  End Custom.
End Compact.

Definition compact (a : Set) : Set := Compact.t a.