Skip to main content

🍃 Data_encoding.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import Proto_alpha.Environment.Variant.

Require Proto_alpha.Environment.Either.
Require Proto_alpha.Environment.Format.
Require Proto_alpha.Environment.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.

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 bool_value : encoding bool.

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 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).

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.

Parameter string_enum : {a : Set}, list (string × a) encoding a.

Module Fixed.
  Parameter string_value : int encoding string.

  Parameter bytes_value : int encoding bytes.

  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 bytes_value : encoding bytes.

  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_value : int encoding string.

  Parameter bytes_value : int encoding bytes.
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 valuefun_combine (fun_value value) (fun_bytes bytes)
  | Lazy.Bytes bytesfun_bytes bytes
  | Lazy.Value valuefun_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 bytesbytes
    | Noneaxiom
    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 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.