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}, 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.