πΒ 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},
option Variant.t β 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
| CDynDescr : string β string β 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},
option Variant.t β 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
| CDynDescr : string β string β 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.