shttpd/coq/S/Lucid/PureConstructions.v

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

Require Import Coq.Program.Basics.
Require Import S.Lucid.Lift.

(* Define some pure ‘glue’ arrows, manipulating
   pre- and post-conditions and reordering data.
   They are not that useful on theirselves, but
   are great for composition. *)
Section pure_constructions.

(* The indexed pure identity arrow.
   The precondition P must imply the postcondition Q.
   When sequenced, this can be used to transform
   the pre- and post-conditions. *)
Program Definition hoareA_sig_pure A (P : A -> Prop) (Q : A -> Prop) (sense : forall a : A, P a -> Q a) : PureSig A A
  := {| P := P;
        Q := Q;
        f := id |}.

(* The indexed pure identity arrow,
   with equal pre- and post-conditions *)
Program Definition identityA_sig_pure0 A P : PureSig A A := hoareA_sig_pure A P P _.

(* Reverse an input and output pair and the condition *)
Program Definition revA_sig_pure A B P : PureSig (A * B) (B * A)
  := {| P := P;
        Q := prod_curry (flip (prod_uncurry P));
        f := prod_curry (flip pair) |}.

Definition assoc_pairs A B C : A * (B * C) -> (A * B) * C
  := fun p => match p with (a, (b, c)) => ((a, b), c) end.
Definition assoc_pairs_reverse A B C : (A * B) * C -> A * (B * C)
  := fun p => match p with ((a, b), c) => (a, (b, c)) end.

(* Change the association of nested products.
   This can be neccessary due to use of parA and seqA. *)
Program Definition assocA_sig_pure A B C (P : (A * (B * C)) -> Prop) : PureSig (A * (B * C)) ((A * B) * C)
  := {| P := P;
        Q := compose P (assoc_pairs_reverse A B C);
        f := assoc_pairs A B C; |}.

Program Definition assocA_sig_pure_reverse A B C (P : (A * B) * C -> Prop) : PureSig ((A * B) * C) (A * (B * C))
  := {| P := P;
        Q := compose P (assoc_pairs A B C);
        f := assoc_pairs_reverse A B C; |}.

End pure_constructions.