Skip to main content

🍃 RPC_answer.v

Environment

Gitlab , OCaml

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

Require Proto_alpha.Environment.Error_monad.

Module stream.
  Record record {next shutdown : Set} : Set := Build {
    next : next;
    shutdown : shutdown }.
  Arguments record : clear implicits.
  Definition with_next {t_next t_shutdown} next
    (r : record t_next t_shutdown) :=
    Build t_next t_shutdown next r.(shutdown).
  Definition with_shutdown {t_next t_shutdown} shutdown
    (r : record t_next t_shutdown) :=
    Build t_next t_shutdown r.(next) shutdown.
End stream.
Definition stream_skeleton := stream.record.

Reserved Notation "'stream".

Inductive t (o : Set) : Set :=
| OkStream : 'stream o t o
| Unauthorized : option (list Error_monad._error) t o
| OkChunk : o t o
| Error : option (list Error_monad._error) t o
| Ok : o t o
| Not_found : option (list Error_monad._error) t o
| Forbidden : option (list Error_monad._error) t o
| Created : option string t o
| Conflict : option (list Error_monad._error) t o
| No_content : t o

where "'stream" := (fun (t_a : Set) ⇒
  stream_skeleton (unit option t_a) (unit unit)).

Definition stream := 'stream.

Arguments OkStream {_}.
Arguments Unauthorized {_}.
Arguments OkChunk {_}.
Arguments Error {_}.
Arguments Ok {_}.
Arguments Not_found {_}.
Arguments Forbidden {_}.
Arguments Created {_}.
Arguments Conflict {_}.
Arguments No_content {_}.

Parameter _return : {o : Set}, o t o.

Parameter return_chunked : {o : Set}, o t o.

Parameter return_stream : {o : Set}, stream o t o.

Parameter not_found : {o : Set}, t o.

Parameter fail : {a : Set}, list Error_monad._error t a.