💾 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.V8.
Definition StringMap :=
Map.Make
{|
Compare.COMPARABLE.compare := String.compare
|}.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.
Require Import TezosOfOCaml.Environment.V8.
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 subdir ⇒ subdir
| 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.
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 subdir ⇒ subdir
| 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_value ⇒ x_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.Eq ⇒ cast (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 {_}.
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_value ⇒ x_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.Eq ⇒ cast (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 {_ _}.
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.
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.