shttpd/coq/S/Lucid/Parallel.v

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

Require Import S.Lucid.Arrow.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Program.Basics.


(* Parallel composition of Arrows

   On <https://www.haskell.org/arrows/index.html>,
   only arr, seqA and firstA is described,
   so from these primitives, parallel composition
   is in fact sequential.

   This defines an actual parallel composition
   primitive, with interleaving, interference, and
   parallelism (as in, multi-threading!). *)
Section definitions.

Variable World : Type.
Definition left_situation A B (X : Situation (A * B)) : Situation (World := World) A
  := match X with (w, (x, y)) => (w, x) end.
Definition right_situation A B (X : Situation (A * B)) : Situation (World := World) B
  := match X with (w, (x, y)) => (w, y) end.

Arguments left_situation { _ _ } _.
Arguments right_situation { _ _ } _.

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

Variable A B C D : Type.

Definition parA_sig (this : ArrowSig World A B) (that : ArrowSig World C D)
  : ArrowSig World (A * C) (B * D)
  := {| rely := fun p w => rely this (left_situation p) w
          /\ rely that (right_situation p) w;
        (* conjunction, not disjunction -- it is only guaranteed
           if both guarantee it*)
        guarantee := fun p w => guarantee this (left_situation p) w
          /\ guarantee that (right_situation p) w;
        (* Combine ordinary Hoare preconditions,
           and require that this/that fulfill each other rely/guarantee *)
        pre := fun p =>
          (pre this (left_situation p) /\ pre that (right_situation p))
          /\ (forall w, guarantee this (left_situation p) w -> rely that (right_situation p) w)
          /\ (forall w, guarantee that (right_situation p) w -> rely this (left_situation p) w);
        (* (The postconditions assume that 'rely' and 'pre' were respected)
           XXX still, this looks very suspicious!
           Better find a paper that says this is good or bad, or find an answer
           myself! *)
        post := fun p q => post this (left_situation p) (left_situation q)
          /\ post that (right_situation p) (right_situation q); |}.

End definitions.

Arguments parA_sig { _ _ _ _ _ } _ _.