shttpd/coq/S/Lucid/Primitives.v

(* SPDX-License-Identifier: GPL-2.0 or GPL-3.0
   Copyright © 2019 Ariadne Devos *)

Require Import S.Lucid.Arrow.
Require Import S.Lucid.Parallel.
Require Import S.Lucid.Sequential.
Require Import S.Lucid.Lift.
Require Import S.Lucid.Equivalence.
Require Import Coq.Program.Basics.

(* Pure arrows and sequential and parallel composition,
   the most common operators. *)
Section definitions.

Variable World : Type.
Variable Arrow : forall A B, ArrowSig World A B -> Type.

Arguments Arrow { _ _ } _.

Record arrow_primitives := {
  (* sequential composition *)
  seqA : forall A B C (stop : ArrowSig World A B) (start : ArrowSig World B C)
    (f : Arrow stop) (g : Arrow start), Arrow (seq_sig stop start);
  (* parallel composition *)
  parA : forall A B C D (up : ArrowSig World A B) (down : ArrowSig World C D)
    (f : Arrow up) (g : Arrow down), Arrow (parA_sig up down);
  (* TODO: or allow custom arrows-within-arrows?
     Proving with reification, arrow transformers etc. *)
  (* TODO: variant with bijections *)
  pureA : forall A B (p : PureSig A B) (relyg : Situation A -> Frame World), Arrow (PureArrowSig p relyg);
}.

End definitions.

Arguments seqA { _ _ } _ { _ _ _ } _ _ _ _.
Arguments parA { _ _ } _ { _ _ _ _ } _ _ _ _.
Arguments pureA { _ _ } _ { _ _ } _ _.