Skip to main content

💾 Storage_description.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.

Require Import TezosOfOCaml.Environment.V7.

Definition StringMap :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := String.compare
    |}.

Records for the constructor parameters
Module ConstructorRecords_description.
  Module description.
    Module Value.
      Record record {get encoding : Set} : Set := Build {
        get : get;
        encoding : encoding;
      }.
      Arguments record : clear implicits.
      Definition with_get {t_get t_encoding} get
        (r : record t_get t_encoding) :=
        Build t_get t_encoding get r.(encoding).
      Definition with_encoding {t_get t_encoding} encoding
        (r : record t_get t_encoding) :=
        Build t_get t_encoding r.(get) encoding.
    End Value.
    Definition Value_skeleton := Value.record.

    Module IndexedDir.
      Record record {arg arg_encoding list subdir : Set} : Set := Build {
        arg : arg;
        arg_encoding : arg_encoding;
        list : list;
        subdir : subdir;
      }.
      Arguments record : clear implicits.
      Definition with_arg {t_arg t_arg_encoding t_list t_subdir} arg
        (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir arg r.(arg_encoding) r.(list)
          r.(subdir).
      Definition with_arg_encoding {t_arg t_arg_encoding t_list t_subdir}
        arg_encoding (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir r.(arg) arg_encoding r.(list)
          r.(subdir).
      Definition with_list {t_arg t_arg_encoding t_list t_subdir} list
        (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir r.(arg) r.(arg_encoding) list
          r.(subdir).
      Definition with_subdir {t_arg t_arg_encoding t_list t_subdir} subdir
        (r : record t_arg t_arg_encoding t_list t_subdir) :=
        Build t_arg t_arg_encoding t_list t_subdir r.(arg) r.(arg_encoding)
          r.(list) subdir.
    End IndexedDir.
    Definition IndexedDir_skeleton := IndexedDir.record.
  End description.
End ConstructorRecords_description.
Import ConstructorRecords_description.

Module desc_with_path.
  Record record {rev_path dir : Set} : Set := Build {
    rev_path : rev_path;
    dir : dir;
  }.
  Arguments record : clear implicits.
  Definition with_rev_path {t_rev_path t_dir} rev_path
    (r : record t_rev_path t_dir) :=
    Build t_rev_path t_dir rev_path r.(dir).
  Definition with_dir {t_rev_path t_dir} dir (r : record t_rev_path t_dir) :=
    Build t_rev_path t_dir r.(rev_path) dir.
End desc_with_path.
Definition desc_with_path_skeleton := desc_with_path.record.

Reserved Notation "'description.Value".
Reserved Notation "'description.IndexedDir".
Reserved Notation "'t".
Reserved Notation "'desc_with_path".

Inductive description (key : Set) : Set :=
| Empty : description key
| Value : {a : Set}, 'description.Value a key description key
| NamedDir : StringMap.(Map.S.t) ('t key) description key
| IndexedDir : {a : Set},
  'description.IndexedDir a key description key

where "'desc_with_path" :=
  (fun (t_key : Set) ⇒ desc_with_path_skeleton (list string)
    (description t_key))
and "'t" := (fun (t_key : Set) ⇒ 'desc_with_path t_key)
and "'description.Value" :=
  (fun (t_a t_key : Set) ⇒ description.Value_skeleton
    (t_key M? (option t_a)) (Data_encoding.t t_a))
and "'description.IndexedDir" :=
  (fun (t_a t_key : Set) ⇒ description.IndexedDir_skeleton (RPC_arg.t t_a)
    (Data_encoding.t t_a) (t_key M? (list t_a)) ('t (t_key × t_a))).

Module description.
  Include ConstructorRecords_description.description.
  Definition Value := 'description.Value.
  Definition IndexedDir := 'description.IndexedDir.
End description.

Definition t := 't.
Definition desc_with_path := 'desc_with_path.

Arguments Empty {_}.
Arguments Value {_ _}.
Arguments NamedDir {_}.
Arguments IndexedDir {_ _}.

Reserved Notation "'pp_item".

#[bypass_check(guard)]
Fixpoint pp {a : Set} (ppf : Format.formatter) (function_parameter : t a)
  {struct function_parameter} : unit :=
  let pp_item {a} := 'pp_item a in
  let '{| desc_with_path.dir := dir |} := function_parameter in
  match dir with
  | Empty
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Empty"
          CamlinternalFormatBasics.End_of_format) "Empty")
  | Value _e
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Value"
          CamlinternalFormatBasics.End_of_format) "Value")
  | NamedDir map
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v>"
                CamlinternalFormatBasics.End_of_format) "<v>"))
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Formatting_lit
              CamlinternalFormatBasics.Close_box
              CamlinternalFormatBasics.End_of_format))) "@[<v>%a@]")
      (Format.pp_print_list None pp_item) (StringMap.(Map.S.bindings) map)
  |
    IndexedDir {|
      description.IndexedDir.arg := arg;
        description.IndexedDir.subdir := subdir
        |} ⇒
    let name :=
      Format.asprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Char_literal "<" % char
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              (CamlinternalFormatBasics.Char_literal ">" % char
                CamlinternalFormatBasics.End_of_format))) "<%s>")
        (RPC_arg.descr_value arg).(RPC_arg.descr.name) in
    pp_item ppf (name, subdir)
  end

where "'pp_item" :=
  (fun (a : Set) ⇒ fun
    (ppf : Format.formatter) (function_parameter : string × t a) ⇒
    let '(name, desc) := function_parameter in
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<hv 2>"
                CamlinternalFormatBasics.End_of_format) "<hv 2>"))
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Formatting_lit
                  CamlinternalFormatBasics.Close_box
                  CamlinternalFormatBasics.End_of_format))))) "@[<hv 2>%s@ %a@]")
      name pp desc).

Definition pp_item {a : Set} := 'pp_item a.

Definition pp_rev_path (ppf : Format.formatter) (path : list string) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Char_literal "[" % char
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Char_literal "]" % char
            CamlinternalFormatBasics.End_of_format))) "[%a]")
    (Format.pp_print_list
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf " / ")) Format.pp_print_string)
    (List.rev path).

Fixpoint register_named_subcontext {r : Set} (desc : t r) (names : list string)
  : t r :=
  match (desc.(desc_with_path.dir), names) with
  | (_, [])desc
  | ((Value _, _) | (IndexedDir _, _)) ⇒
    Format.kasprintf Pervasives.invalid_arg
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Could not register a named subcontext at "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal " because of an existing "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal "." % char
                  CamlinternalFormatBasics.End_of_format)))))
        "Could not register a named subcontext at %a because of an existing %a.")
      pp_rev_path desc.(desc_with_path.rev_path) pp desc
  | (Empty, cons name names)
    let subdir :=
      {| desc_with_path.rev_path := cons name desc.(desc_with_path.rev_path);
        desc_with_path.dir := Empty; |} in
    let '_ :=
      (* ❌ Set record field not handled. *)
      set_record_field desc "dir"
        (NamedDir (StringMap.(Map.S.singleton) name subdir)) in
    register_named_subcontext subdir names
  | (NamedDir map, cons name names)
    let subdir :=
      match StringMap.(Map.S.find) name map with
      | Some subdirsubdir
      | None
        let subdir :=
          {|
            desc_with_path.rev_path := cons name desc.(desc_with_path.rev_path);
            desc_with_path.dir := Empty; |} in
        let '_ :=
          (* ❌ Set record field not handled. *)
          set_record_field desc "dir"
            (NamedDir (StringMap.(Map.S.add) name subdir map)) in
        subdir
      end in
    register_named_subcontext subdir names
  end.

Records for the constructor parameters
Module ConstructorRecords_args.
  Module args.
    Module One.
      Record record {rpc_arg encoding compare : Set} : Set := Build {
        rpc_arg : rpc_arg;
        encoding : encoding;
        compare : compare;
      }.
      Arguments record : clear implicits.
      Definition with_rpc_arg {t_rpc_arg t_encoding t_compare} rpc_arg
        (r : record t_rpc_arg t_encoding t_compare) :=
        Build t_rpc_arg t_encoding t_compare rpc_arg r.(encoding) r.(compare).
      Definition with_encoding {t_rpc_arg t_encoding t_compare} encoding
        (r : record t_rpc_arg t_encoding t_compare) :=
        Build t_rpc_arg t_encoding t_compare r.(rpc_arg) encoding r.(compare).
      Definition with_compare {t_rpc_arg t_encoding t_compare} compare
        (r : record t_rpc_arg t_encoding t_compare) :=
        Build t_rpc_arg t_encoding t_compare r.(rpc_arg) r.(encoding) compare.
    End One.
    Definition One_skeleton := One.record.
  End args.
End ConstructorRecords_args.
Import ConstructorRecords_args.

Reserved Notation "'args.One".

Inductive args : Set :=
| One : {a : Set}, 'args.One a args
| Pair : args args args

where "'args.One" :=
  (fun (t_a : Set) ⇒ args.One_skeleton (RPC_arg.t t_a) (Data_encoding.t t_a)
    (t_a t_a int)).

Module args.
  Include ConstructorRecords_args.args.
  Definition One := 'args.One.
End args.

#[bypass_check(guard)]
Fixpoint unpack {c a b : Set} (function_parameter : args)
  {struct function_parameter} : c a × b :=
  match function_parameter with
  | One _cast (c a × b) (fun (x_value : c) ⇒ x_value)
  | Pair l_value r_value
    let 'existT _ [__Pair_'inter_key, __1, __0] [r_value, l_value] :=
      cast_exists (Es := [Set ** Set ** Set])
        (fun '[__Pair_'inter_key, __1, __0][args ** args])
        [r_value, l_value] in
    cast (c a × b)
    (let unpack_l := (unpack : args __Pair_'inter_key a × __0) l_value in
    let unpack_r := (unpack : args c __Pair_'inter_key × __1) r_value in
    fun (x_value : c) ⇒
      let '(c_value, d_value) := unpack_r x_value in
      let '(b_value, a_value) := unpack_l c_value in
      (b_value, (a_value, d_value)))
  end.

#[bypass_check(guard)]
Fixpoint _pack {a b c : Set} (function_parameter : args)
  {struct function_parameter} : a b c :=
  match function_parameter with
  | One _
    cast (a b c)
    (fun (b_value : a) ⇒ fun (a_value : b) ⇒ (b_value, a_value))
  | Pair l_value r_value
    let 'existT _ [__Pair_'inter_key, __1, __0] [r_value, l_value] :=
      cast_exists (Es := [Set ** Set ** Set])
        (fun '[__Pair_'inter_key, __1, __0][args ** args])
        [r_value, l_value] in
    cast (a b c)
    (let pack_l := (_pack : args a __0 __Pair_'inter_key) l_value in
    let pack_r := (_pack : args __Pair_'inter_key __1 c) r_value in
    fun (b_value : a) ⇒
      fun (function_parameter : __0 × __1) ⇒
        let '(a_value, d_value) := function_parameter in
        let c_value := pack_l b_value a_value in
        pack_r c_value d_value)
  end.

#[bypass_check(guard)]
Fixpoint compare {b : Set} (function_parameter : args)
  {struct function_parameter} : b b int :=
  match function_parameter with
  | One {| args.One.compare := local_compare |} ⇒
    let local_compare := cast (b b int) local_compare in
    cast (b b int) local_compare
  | Pair l_value r_value
    let 'existT _ [__1, __0] [r_value, l_value] :=
      cast_exists (Es := [Set ** Set]) (fun '[__1, __0][args ** args])
        [r_value, l_value] in
    cast (b b int)
    (let compare_l := compare l_value in
    let compare_r := compare r_value in
    fun (function_parameter : __0 × __1) ⇒
      let '(a1, b1) := function_parameter in
      fun (function_parameter : __0 × __1) ⇒
        let '(a2, b2) := function_parameter in
        match compare_l a1 a2 with
        | 0 ⇒ compare_r b1 b2
        | x_valuex_value
        end)
  end.

Definition destutter {A B : Set}
  (equal : A A bool) (l_value : list (A × B)) : list A :=
  match l_value with
  | []nil
  | cons (i_value, _) l_value
    let fix loop {C : Set}
      (acc_value : list A) (i_value : A) (function_parameter : list (A × C))
      : list A :=
      match function_parameter with
      | []acc_value
      | cons (j_value, _) l_value
        if equal i_value j_value then
          loop acc_value i_value l_value
        else
          loop (cons j_value acc_value) j_value l_value
      end in
    loop [ i_value ] i_value l_value
  end.

#[bypass_check(guard)]
Fixpoint register_indexed_subcontext {r a b : Set}
  (desc : t r) (list_value : r M? (list a)) (path : args) {struct desc}
  : t b :=
  match (path, desc, list_value) with
  | (Pair _left _right, desc, list_value)
    let 'existT _ [__0, __1, __Pair_'inter_key]
      [list_value, desc, _right, _left] :=
      cast_exists (Es := [Set ** Set ** Set])
        (fun '[__0, __1, __Pair_'inter_key]
          [r M? (list (__0 × __1)) ** t r ** args ** args])
        [list_value, desc, _right, _left] in
    let compare_left := compare _left in
    let equal_left (x_value : __0) (y_value : __0) : bool :=
      (compare_left x_value y_value) =i 0 in
    let list_left (r_value : r) : M? (list __0) :=
      let? l_value := list_value r_value in
      return? (destutter equal_left l_value) in
    let list_right (r_value : __Pair_'inter_key) : M? (list __1) :=
      let '(a_value, k_value) := unpack _left r_value in
      let? l_value := list_value a_value in
      return?
        (List.map Pervasives.snd
          (List.filter
            (fun (function_parameter : __0 × __1) ⇒
              let '(x_value, _) := function_parameter in
              equal_left x_value k_value) l_value)) in
    register_indexed_subcontext
      (register_indexed_subcontext desc list_left _left) list_right _right
  |
    (One {| args.One.rpc_arg := arg; args.One.encoding := arg_encoding |}, desc,
      list_value)
    let '[list_value, desc, arg_encoding, arg] :=
      cast [r M? (list a) ** t r ** Data_encoding.t a ** RPC_arg.t a]
        [list_value, desc, arg_encoding, arg] in
    match desc.(desc_with_path.dir) with
    | (Value _ | NamedDir _) ⇒
      Format.kasprintf Pervasives.invalid_arg
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "Could not register an indexed subcontext at "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal
                " because of an existing "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal "." % char
                    CamlinternalFormatBasics.End_of_format)))))
          "Could not register an indexed subcontext at %a because of an existing %a.")
        pp_rev_path desc.(desc_with_path.rev_path) pp desc
    | Empty
      let subdir :=
        {|
          desc_with_path.rev_path :=
            cons
              (Format.sprintf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal "(Maybe of "
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.Char_literal ")" % char
                        CamlinternalFormatBasics.End_of_format)))
                  "(Maybe of %s)")
                (RPC_arg.descr_value arg).(RPC_arg.descr.name))
              desc.(desc_with_path.rev_path); desc_with_path.dir := Empty; |} in
      let '_ :=
        (* ❌ Set record field not handled. *)
        set_record_field desc "dir"
          (IndexedDir
            {| description.IndexedDir.arg := arg;
              description.IndexedDir.arg_encoding := arg_encoding;
              description.IndexedDir.list := list_value;
              description.IndexedDir.subdir := subdir; |}) in
      cast (t b) subdir
    |
      IndexedDir {|
        description.IndexedDir.arg := inner_arg;
          description.IndexedDir.subdir := subdir
          |} ⇒
      match RPC_arg.eq_value arg inner_arg with
      | None
        Format.kasprintf Pervasives.invalid_arg
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "An indexed subcontext at "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.String_literal
                  " already exists but has a different argument: `"
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.String_literal "` <> `"
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal "`."
                          CamlinternalFormatBasics.End_of_format)))))))
            "An indexed subcontext at %a already exists but has a different argument: `%s` <> `%s`.")
          pp_rev_path desc.(desc_with_path.rev_path)
          (RPC_arg.descr_value arg).(RPC_arg.descr.name)
          (RPC_arg.descr_value inner_arg).(RPC_arg.descr.name)
      | Some RPC_arg.Eqcast (t b) subdir
      end
    end
  end.

Definition register_value {a b : Set}
  (desc : t a) (get : a M? (option b)) (encoding : Data_encoding.t b)
  : unit :=
  match desc.(desc_with_path.dir) with
  | Empty
    (* ❌ Set record field not handled. *)
    set_record_field desc "dir"
      (Value
        {| description.Value.get := get; description.Value.encoding := encoding;
          |})
  | _
    Format.kasprintf Pervasives.invalid_arg
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Could not register a value at "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal " because of an existing "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal "." % char
                  CamlinternalFormatBasics.End_of_format)))))
        "Could not register a value at %a because of an existing %a.")
      pp_rev_path desc.(desc_with_path.rev_path) pp desc
  end.

Definition create {A : Set} (function_parameter : unit) : desc_with_path A :=
  let '_ := function_parameter in
  {| desc_with_path.rev_path := nil; desc_with_path.dir := Empty; |}.

Module INDEX.
  Record signature {t : Set} : Set := {
    t := t;
    to_path : t list string list string;
    of_path : list string M? (option t);
    path_length : M? int;
    rpc_arg : RPC_arg.t t;
    encoding : Data_encoding.t t;
    compare : t t int;
  }.
End INDEX.
Definition INDEX := @INDEX.signature.
Arguments INDEX {_}.

Records for the constructor parameters
Module ConstructorRecords_handler.
  Module handler.
    Module Handler.
      Record record {encoding get : Set} : Set := Build {
        encoding : encoding;
        get : get;
      }.
      Arguments record : clear implicits.
      Definition with_encoding {t_encoding t_get} encoding
        (r : record t_encoding t_get) :=
        Build t_encoding t_get encoding r.(get).
      Definition with_get {t_encoding t_get} get
        (r : record t_encoding t_get) :=
        Build t_encoding t_get r.(encoding) get.
    End Handler.
    Definition Handler_skeleton := Handler.record.
  End handler.
End ConstructorRecords_handler.
Import ConstructorRecords_handler.

Reserved Notation "'handler.Handler".

Inductive handler (key : Set) : Set :=
| Handler : {a : Set}, 'handler.Handler a key handler key

where "'handler.Handler" :=
  (fun (t_a t_key : Set) ⇒ handler.Handler_skeleton (Data_encoding.t t_a)
    (t_key int M? t_a)).

Module handler.
  Include ConstructorRecords_handler.handler.
  Definition Handler := 'handler.Handler.
End handler.

Arguments Handler {_ _}.

Records for the constructor parameters
Module ConstructorRecords_opt_handler.
  Module opt_handler.
    Module Opt_handler.
      Record record {encoding get : Set} : Set := Build {
        encoding : encoding;
        get : get;
      }.
      Arguments record : clear implicits.
      Definition with_encoding {t_encoding t_get} encoding
        (r : record t_encoding t_get) :=
        Build t_encoding t_get encoding r.(get).
      Definition with_get {t_encoding t_get} get
        (r : record t_encoding t_get) :=
        Build t_encoding t_get r.(encoding) get.
    End Opt_handler.
    Definition Opt_handler_skeleton := Opt_handler.record.
  End opt_handler.
End ConstructorRecords_opt_handler.
Import ConstructorRecords_opt_handler.

Reserved Notation "'opt_handler.Opt_handler".

Inductive opt_handler (key : Set) : Set :=
| Opt_handler : {a : Set},
  'opt_handler.Opt_handler a key opt_handler key

where "'opt_handler.Opt_handler" :=
  (fun (t_a t_key : Set) ⇒ opt_handler.Opt_handler_skeleton
    (Data_encoding.t t_a) (t_key int M? (option t_a))).

Module opt_handler.
  Include ConstructorRecords_opt_handler.opt_handler.
  Definition Opt_handler := 'opt_handler.Opt_handler.
End opt_handler.

Arguments Opt_handler {_ _}.

Fixpoint combine_object {A : Set}
  (function_parameter : list (string × opt_handler A)) : handler A :=
  match function_parameter with
  | []
    Handler
      {| handler.Handler.encoding := Data_encoding.unit_value;
        handler.Handler.get :=
          fun (function_parameter : A) ⇒
            let '_ := function_parameter in
            fun (function_parameter : int) ⇒
              let '_ := function_parameter in
              Error_monad.return_unit; |}
  | cons (name, Opt_handler handler_value) fields
    let 'Handler handlers := combine_object fields in
    Handler
      {|
        handler.Handler.encoding :=
          Data_encoding.merge_objs
            (Data_encoding.obj1
              (Data_encoding.opt None None name
                (Data_encoding.dynamic_size None
                  handler_value.(opt_handler.Opt_handler.encoding))))
            handlers.(handler.Handler.encoding);
        handler.Handler.get :=
          fun (k_value : A) ⇒
            fun (i_value : int) ⇒
              let? v1 :=
                handler_value.(opt_handler.Opt_handler.get) k_value i_value in
              let? v2 := handlers.(handler.Handler.get) k_value i_value in
              return? (v1, v2); |}
  end.

Module query.
  Record record : Set := Build {
    depth : int;
  }.
  Definition with_depth depth (r : record) :=
    Build depth.
End query.
Definition query := query.record.

Definition depth_query : RPC_query.t query :=
  RPC_query.seal
    (RPC_query.op_pipeplus
      (RPC_query.query_value (fun (depth : int) ⇒ {| query.depth := depth; |}))
      (RPC_query.field_value None "depth" RPC_arg.uint 0
        (fun (t_value : query) ⇒ t_value.(query.depth)))).

#[bypass_check(guard)]
Definition build_directory {key : Set} (dir : t key) : RPC_directory.t key :=
  let rpc_dir := Pervasives.ref_value RPC_directory.empty in
  let register {ikey : Set}
    (chunked : bool) (path : RPC_path.t key ikey)
    (function_parameter : opt_handler ikey) : unit :=
    let
      'Opt_handler {|
        opt_handler.Opt_handler.encoding := encoding;
          opt_handler.Opt_handler.get := get
          |} := function_parameter in
    let service := RPC_service.get_service None depth_query encoding path in
    Pervasives.op_coloneq rpc_dir
      (RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_dir)
        service
        (fun (k_value : ikey) ⇒
          fun (q_value : query) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              get k_value (q_value.(query.depth) +i 1))) in
  let fix build_handler {ikey : Set}
    (desc : t ikey) (path : RPC_path.t key ikey) {struct desc}
    : opt_handler ikey :=
    match desc.(desc_with_path.dir) with
    | Empty
      Opt_handler
        {| opt_handler.Opt_handler.encoding := Data_encoding.unit_value;
          opt_handler.Opt_handler.get :=
            fun (function_parameter : ikey) ⇒
              let '_ := function_parameter in
              fun (function_parameter : int) ⇒
                let '_ := function_parameter in
                Error_monad.return_none; |}
    |
      Value {|
        description.Value.get := get;
          description.Value.encoding := encoding
          |} ⇒
      let 'existT _ __Value_'a [encoding, get] :=
        cast_exists (Es := Set)
          (fun __Value_'a
            [Data_encoding.t __Value_'a ** ikey M? (option __Value_'a)])
          [encoding, get] in
      let handler_value :=
        Opt_handler
          {| opt_handler.Opt_handler.encoding := encoding;
            opt_handler.Opt_handler.get :=
              fun (k_value : ikey) ⇒
                fun (i_value : int) ⇒
                  if i_value <i 0 then
                    Error_monad.return_none
                  else
                    get k_value; |} in
      let '_ := register true path handler_value in
      handler_value
    | NamedDir map
      let map := cast (StringMap.(Map.S.t) (t ikey)) map in
      let fields := StringMap.(Map.S.bindings) map in
      let fields :=
        List.map
          (fun (function_parameter : String.t × t ikey) ⇒
            let '(name, dir) := function_parameter in
            (name, (build_handler dir (RPC_path.op_div path name)))) fields in
      let 'Handler handler_value := combine_object fields in
      let handler_value :=
        Opt_handler
          {|
            opt_handler.Opt_handler.encoding :=
              handler_value.(handler.Handler.encoding);
            opt_handler.Opt_handler.get :=
              fun (k_value : ikey) ⇒
                fun (i_value : int) ⇒
                  if i_value <i 0 then
                    Error_monad.return_none
                  else
                    let? v_value :=
                      handler_value.(handler.Handler.get) k_value (i_value -i 1)
                      in
                    Error_monad.return_some v_value; |} in
      let '_ := register true path handler_value in
      handler_value
    |
      IndexedDir {|
        description.IndexedDir.arg := arg;
          description.IndexedDir.arg_encoding := arg_encoding;
          description.IndexedDir.list := list_value;
          description.IndexedDir.subdir := subdir
          |} ⇒
      let 'existT _ __IndexedDir_'a [subdir, list_value, arg_encoding, arg] :=
        cast_exists (Es := Set)
          (fun __IndexedDir_'a
            [t (ikey × __IndexedDir_'a) ** ikey M? (list __IndexedDir_'a) **
              Data_encoding.t __IndexedDir_'a ** RPC_arg.t __IndexedDir_'a])
          [subdir, list_value, arg_encoding, arg] in
      let 'Opt_handler handler_value :=
        build_handler subdir (RPC_path.op_divcolon path arg) in
      let 'existT _ __Opt_handler_'a1 handler_value :=
        cast_exists (Es := Set)
          (fun __Opt_handler_'a1
            opt_handler.Opt_handler __Opt_handler_'a1 (ikey × __IndexedDir_'a))
          handler_value in
      let encoding :=
        Data_encoding.union None
          [
            Data_encoding.case_value "Leaf" None (Data_encoding.Tag 0)
              (Data_encoding.dynamic_size None arg_encoding)
              (fun (function_parameter :
                __IndexedDir_'a × option __Opt_handler_'a1) ⇒
                match function_parameter with
                | (key_value, None)Some key_value
                | _None
                end)
              (fun (key_value : __IndexedDir_'a) ⇒ (key_value, None));
            Data_encoding.case_value "Dir" None (Data_encoding.Tag 1)
              (Data_encoding.tup2
                (Data_encoding.dynamic_size None arg_encoding)
                (Data_encoding.dynamic_size None
                  handler_value.(opt_handler.Opt_handler.encoding)))
              (fun (function_parameter :
                __IndexedDir_'a × option __Opt_handler_'a1) ⇒
                match function_parameter with
                | (key_value, Some value_value)
                  Some (key_value, value_value)
                | _None
                end)
              (fun (function_parameter :
                __IndexedDir_'a × __Opt_handler_'a1) ⇒
                let '(key_value, value_value) :=
                  function_parameter in
                (key_value, (Some value_value)))
          ] in
      let get (k_value : ikey) (i_value : int)
        : M? (option (list (__IndexedDir_'a × option __Opt_handler_'a1))) :=
        if i_value <i 0 then
          Error_monad.return_none
        else
          if i_value =i 0 then
            Error_monad.return_some nil
          else
            let? keys := list_value k_value in
            let? values :=
              List.map_es
                (fun (key_value : __IndexedDir_'a) ⇒
                  if i_value =i 1 then
                    return? (key_value, None)
                  else
                    let? value_value :=
                      handler_value.(opt_handler.Opt_handler.get)
                        (k_value, key_value) (i_value -i 1) in
                    return? (key_value, value_value)) keys in
            Error_monad.return_some values in
      let handler_value :=
        Opt_handler
          {|
            opt_handler.Opt_handler.encoding :=
              Data_encoding.list_value None
                (Data_encoding.dynamic_size None encoding);
            opt_handler.Opt_handler.get := get; |} in
      let '_ := register true path handler_value in
      handler_value
    end in
  let '_ := Pervasives.ignore (build_handler dir RPC_path.open_root) in
  Pervasives.op_exclamation rpc_dir.