๐ย RPC_directory.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.RPC_answer.
Require TezosOfOCaml.Environment.Structs.V0.RPC_path.
Require TezosOfOCaml.Environment.Structs.V0.RPC_service.
Parameter t : โ (prefix : Set), Set.
Definition directory (prefix : Set) : Set := t prefix.
Parameter empty : โ {prefix : Set}, directory prefix.
Parameter map : โ {a b : Set},
(a โ b) โ directory b โ directory a.
Parameter prefix : โ {p pr : Set},
RPC_path.path pr p โ directory p โ directory pr.
Parameter merge : โ {a : Set}, directory a โ directory a โ directory a.
Inductive step : Set :=
| Static : string โ step
| Dynamic : RPC_arg.descr โ step
| DynamicTail : RPC_arg.descr โ step.
Inductive conflict : Set :=
| CService : RPC_service.meth โ conflict
| CDir : conflict
| CBuilder : conflict
| CTail : conflict
| CTypes : RPC_arg.descr โ RPC_arg.descr โ conflict
| CType : RPC_arg.descr โ list string โ conflict.
Parameter register : โ {input output params prefix query : Set},
bool โ directory prefix โ
RPC_service.t prefix params query input output โ
(params โ query โ input โ Error_monad.tzresult output) โ
directory prefix.
Parameter opt_register : โ {input output params prefix query : Set},
bool โ directory prefix โ
RPC_service.t prefix params query input output โ
(params โ query โ input โ Error_monad.tzresult (option output))
โ directory prefix.
Parameter gen_register : โ {input output params prefix query : Set},
directory prefix โ RPC_service.t prefix params query input output โ
(params โ query โ input โ Variant.t) โ directory prefix.
Parameter lwt_register : โ {input output params prefix query : Set},
bool โ directory prefix โ
RPC_service.t prefix params query input output โ
(params โ query โ input โ output) โ directory prefix.
Parameter register0 : โ {i o q : Set},
bool โ directory unit โ RPC_service.t unit unit q i o โ
(q โ i โ Error_monad.tzresult o) โ directory unit.
Parameter register1 : โ {a i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ Error_monad.tzresult o) โ directory prefix.
Parameter register2 : โ {a b i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ Error_monad.tzresult o) โ directory prefix.
Parameter register3 : โ {a b c i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ Error_monad.tzresult o) โ
directory prefix.
Parameter register4 : โ {a b c d i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ Error_monad.tzresult o) โ
directory prefix.
Parameter register5 : โ {a b c d e i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ Error_monad.tzresult o) โ
directory prefix.
Parameter opt_register0 : โ {i o q : Set},
bool โ directory unit โ RPC_service.t unit unit q i o โ
(q โ i โ Error_monad.tzresult (option o)) โ directory unit.
Parameter opt_register1 : โ {a i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ Error_monad.tzresult (option o)) โ directory prefix.
Parameter opt_register2 : โ {a b i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ Error_monad.tzresult (option o)) โ
directory prefix.
Parameter opt_register3 : โ {a b c i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ Error_monad.tzresult (option o)) โ
directory prefix.
Parameter opt_register4 : โ {a b c d i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ Error_monad.tzresult (option o)) โ
directory prefix.
Parameter opt_register5 : โ {a b c d e i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ Error_monad.tzresult (option o))
โ directory prefix.
Parameter gen_register0 : โ {i o q : Set},
directory unit โ RPC_service.t unit unit q i o โ (q โ i โ Variant.t) โ
directory unit.
Parameter gen_register1 : โ {a i o prefix q : Set},
directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register2 : โ {a b i o prefix q : Set},
directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register3 : โ {a b c i o prefix q : Set},
directory prefix โ RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register4 : โ {a b c d i o prefix q : Set},
directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register5 : โ {a b c d e i o prefix q : Set},
directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ Variant.t) โ directory prefix.
Parameter lwt_register0 : โ {i o q : Set},
bool โ directory unit โ RPC_service.t unit unit q i o โ
(q โ i โ o) โ directory unit.
Parameter lwt_register1 : โ {a i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ o) โ directory prefix.
Parameter lwt_register2 : โ {a b i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ o) โ directory prefix.
Parameter lwt_register3 : โ {a b c i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ o) โ directory prefix.
Parameter lwt_register4 : โ {a b c d i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ o) โ directory prefix.
Parameter lwt_register5 : โ {a b c d e i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ o) โ directory prefix.
Parameter register_dynamic_directory : โ {a prefix : Set},
option string โ directory prefix โ RPC_path.t prefix a โ
(a โ directory a) โ directory prefix.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.RPC_answer.
Require TezosOfOCaml.Environment.Structs.V0.RPC_path.
Require TezosOfOCaml.Environment.Structs.V0.RPC_service.
Parameter t : โ (prefix : Set), Set.
Definition directory (prefix : Set) : Set := t prefix.
Parameter empty : โ {prefix : Set}, directory prefix.
Parameter map : โ {a b : Set},
(a โ b) โ directory b โ directory a.
Parameter prefix : โ {p pr : Set},
RPC_path.path pr p โ directory p โ directory pr.
Parameter merge : โ {a : Set}, directory a โ directory a โ directory a.
Inductive step : Set :=
| Static : string โ step
| Dynamic : RPC_arg.descr โ step
| DynamicTail : RPC_arg.descr โ step.
Inductive conflict : Set :=
| CService : RPC_service.meth โ conflict
| CDir : conflict
| CBuilder : conflict
| CTail : conflict
| CTypes : RPC_arg.descr โ RPC_arg.descr โ conflict
| CType : RPC_arg.descr โ list string โ conflict.
Parameter register : โ {input output params prefix query : Set},
bool โ directory prefix โ
RPC_service.t prefix params query input output โ
(params โ query โ input โ Error_monad.tzresult output) โ
directory prefix.
Parameter opt_register : โ {input output params prefix query : Set},
bool โ directory prefix โ
RPC_service.t prefix params query input output โ
(params โ query โ input โ Error_monad.tzresult (option output))
โ directory prefix.
Parameter gen_register : โ {input output params prefix query : Set},
directory prefix โ RPC_service.t prefix params query input output โ
(params โ query โ input โ Variant.t) โ directory prefix.
Parameter lwt_register : โ {input output params prefix query : Set},
bool โ directory prefix โ
RPC_service.t prefix params query input output โ
(params โ query โ input โ output) โ directory prefix.
Parameter register0 : โ {i o q : Set},
bool โ directory unit โ RPC_service.t unit unit q i o โ
(q โ i โ Error_monad.tzresult o) โ directory unit.
Parameter register1 : โ {a i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ Error_monad.tzresult o) โ directory prefix.
Parameter register2 : โ {a b i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ Error_monad.tzresult o) โ directory prefix.
Parameter register3 : โ {a b c i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ Error_monad.tzresult o) โ
directory prefix.
Parameter register4 : โ {a b c d i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ Error_monad.tzresult o) โ
directory prefix.
Parameter register5 : โ {a b c d e i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ Error_monad.tzresult o) โ
directory prefix.
Parameter opt_register0 : โ {i o q : Set},
bool โ directory unit โ RPC_service.t unit unit q i o โ
(q โ i โ Error_monad.tzresult (option o)) โ directory unit.
Parameter opt_register1 : โ {a i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ Error_monad.tzresult (option o)) โ directory prefix.
Parameter opt_register2 : โ {a b i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ Error_monad.tzresult (option o)) โ
directory prefix.
Parameter opt_register3 : โ {a b c i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ Error_monad.tzresult (option o)) โ
directory prefix.
Parameter opt_register4 : โ {a b c d i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ Error_monad.tzresult (option o)) โ
directory prefix.
Parameter opt_register5 : โ {a b c d e i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ Error_monad.tzresult (option o))
โ directory prefix.
Parameter gen_register0 : โ {i o q : Set},
directory unit โ RPC_service.t unit unit q i o โ (q โ i โ Variant.t) โ
directory unit.
Parameter gen_register1 : โ {a i o prefix q : Set},
directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register2 : โ {a b i o prefix q : Set},
directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register3 : โ {a b c i o prefix q : Set},
directory prefix โ RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register4 : โ {a b c d i o prefix q : Set},
directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ Variant.t) โ directory prefix.
Parameter gen_register5 : โ {a b c d e i o prefix q : Set},
directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ Variant.t) โ directory prefix.
Parameter lwt_register0 : โ {i o q : Set},
bool โ directory unit โ RPC_service.t unit unit q i o โ
(q โ i โ o) โ directory unit.
Parameter lwt_register1 : โ {a i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix (unit ร a) q i o โ
(a โ q โ i โ o) โ directory prefix.
Parameter lwt_register2 : โ {a b i o prefix q : Set},
bool โ directory prefix โ RPC_service.t prefix ((unit ร a) ร b) q i o โ
(a โ b โ q โ i โ o) โ directory prefix.
Parameter lwt_register3 : โ {a b c i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((unit ร a) ร b) ร c) q i o โ
(a โ b โ c โ q โ i โ o) โ directory prefix.
Parameter lwt_register4 : โ {a b c d i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix ((((unit ร a) ร b) ร c) ร d) q i o โ
(a โ b โ c โ d โ q โ i โ o) โ directory prefix.
Parameter lwt_register5 : โ {a b c d e i o prefix q : Set},
bool โ directory prefix โ
RPC_service.t prefix (((((unit ร a) ร b) ร c) ร d) ร e) q i o โ
(a โ b โ c โ d โ e โ q โ i โ o) โ directory prefix.
Parameter register_dynamic_directory : โ {a prefix : Set},
option string โ directory prefix โ RPC_path.t prefix a โ
(a โ directory a) โ directory prefix.