shttpd/coq/S/Lucid/ArrowLift.v

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

Require Import S.Lucid.Arrow.

(* Well-behaved lifting from arrows to other arrows. *)

(* Lift an arrow to another arrow *)
Record arrow_lift_ops (from : arrow_basic) (to : arrow_basic) := {
  (* Different arrows may have different data types *)
  dwarpA : D from -> D to;
  (* Split the warp of a type product.

     Sequencing with this may ensure type-checking,
     but it may also have computational value:
     `D2 t A B` may map to `(t, A, B)`
     and `dwarpA t A` to `(t, A)`. *)
  dwarpAsplit : forall A B, Arr to (dwarpA (D2 _ A B)) (D2 to (dwarpA A) (dwarpA B));
  (* Merge the product of a warp into the warp of the product *)
  dwarpAmerge : forall A B, Arr to (D2 to (dwarpA A) (dwarpA B)) (dwarpA (D2 _ A B));
  (* change the arrow type, warping the data types *)
  arrA : forall A B, Arr from A B -> Arr to (dwarpA A) (dwarpA B);
}.

Arguments dwarpA { _ _ } a _.
Arguments dwarpAsplit { _ _ } a { _ _ }.
Arguments dwarpAmerge { _ _ } a { _ _ }.
Arguments arrA { _ _ } a { _ _ } _.

(* Simplification rules for lifts

   We try to move idA, assocA_r and assocA_l to the
   outer `to` arrow, such that they can fuse with `to`
   arrows.

   Lifts are also moved *into* compositions,
   for they probably cannot directly fuse with
   `to` arrows, but might with `from` arrows
   which are probably more lightweight as well.

   (The rules were taken from Haskell base-4.9.0.0 Control.Arrow). *)
Record arrow_lift_lawful (from : arrow_basic) (to : arrow_basic) (lift : arrow_lift_ops from to) := {
  (* Warp splitting / merging artifacts can be deletedd *)
  dwarpAsplit_merge : forall A B, eqvA to (seqA to (dwarpAsplit (A := A) (B := B) lift) (dwarpAmerge lift)) (idA to);
  dwarpAmerge_split : forall A B, eqvA to (seqA to (dwarpAmerge (A := A) (B := B) lift) (dwarpAsplit lift)) (idA to);

  (* The lift of the identity arrow

     This can be rewritten out by seqA_idA_l and seqA_idA_r. *)
  arrAid : forall A, eqvA to (arrA lift (idA (A := A) from)) (idA to);
  (* Sequential composition of lifts *)
  arrAseq : forall A B C (f : Arr from A B) (g : Arr from B C),
    eqvA to (seqA to (arrA lift f) (arrA lift g))
      (arrA lift (seqA from f g));
  (* Parallel composition of lifts *)
  arrApar : forall A B C D (f : Arr from A B) (g : Arr from C D),
    eqvA to
      (parA to (arrA lift f) (arrA lift g))
      (* The input and output require some pre- and
         post-processing, due to the change in type system *)
      (seqA3 to
        (dwarpAmerge lift (A := A) (B := C))
        (arrA lift (parA from f g))
        (dwarpAsplit lift));
}.

Arguments dwarpAsplit_merge { _ _ _ } a _ _.
Arguments dwarpAmerge_split { _ _ _ } a _ _.
Arguments arrAid { _ _ _ } a _.
Arguments arrAseq { _ _ _ } a { _ _ _ } f g.
Arguments arrApar { _ _ _ } a { _ _ _ _ } f g.

Record arrow_lift := {
  liftA_from : arrow_basic;
  liftA_to : arrow_basic;
  liftA_ops : arrow_lift_ops liftA_from liftA_to;
  liftA_laws : arrow_lift_lawful liftA_from liftA_to liftA_ops;
}.

Coercion liftA_to : arrow_lift >-> arrow_basic.
Coercion liftA_ops : arrow_lift >-> arrow_lift_ops.
Coercion liftA_laws : arrow_lift >-> arrow_lift_lawful.