Skip to main content

🍃 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.