🍃 Data_encoding.v
Environment
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 := {
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.
The various ways to efficiently encode [input].
The list of layouts available to encode [input].
The number of bits necessary to distinguish between the various
layouts.
[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].
[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.
[classify x] returns the layout to be used to encode [x].
The encoding to use when targeting a JSON output.