Skip to main content

πŸƒΒ RPC_directory.v

Environment

Gitlab

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.