💾 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.Proto_alpha.Environment.
Definition StringMap :=
Map.Make
{|
Compare.COMPARABLE.compare := String.compare
|}.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.
Require Import TezosOfOCaml.Proto_alpha.Environment.
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.
Axiom compare : ∀ {b : Set}, args → b → b → int.
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.
Axiom register_indexed_subcontext : ∀ {r a b : Set},
t r → (r → M? (list a)) → args → t b.
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 → option t;
path_length : 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.
Axiom compare : ∀ {b : Set}, args → b → b → int.
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.
Axiom register_indexed_subcontext : ∀ {r a b : Set},
t r → (r → M? (list a)) → args → t b.
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 → option t;
path_length : 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 : Set :=
| Handler : ∀ {a key : Set}, 'handler.Handler a key → handler
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.
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 : Set :=
| Handler : ∀ {a key : Set}, 'handler.Handler a key → handler
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.
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 : Set :=
| Opt_handler : ∀ {a key : Set},
'opt_handler.Opt_handler a key → opt_handler
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.
Axiom combine_object : list (string × opt_handler) → handler.
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)))).
Axiom build_directory : ∀ {key : Set}, t key → RPC_directory.t key.
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 : Set :=
| Opt_handler : ∀ {a key : Set},
'opt_handler.Opt_handler a key → opt_handler
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.
Axiom combine_object : list (string × opt_handler) → handler.
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)))).
Axiom build_directory : ∀ {key : Set}, t key → RPC_directory.t key.