🍃 RPC_directory.v

Environment

Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.RPC_answer.
Require Proto_alpha.Environment.RPC_path.
Require Proto_alpha.Environment.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.