shttpd/coq/S/Lucid/Lift.v

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

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

(* Lift Gallina functions to arrows
   (or rather, lift the functions to
   corresponding arrow signatures)
   (actually lifting the arrows is
   in S.Lucid.Primitives). *)
Section definitions.

(* The behaviour of a pure Gallina function. *)
Record PureSig A B := {
  (* precondition *)
  P : A -> Prop;
  (* postcondition *)
  Q : B -> Prop;
  (* function (sig: subset type) *)
  f : sig (A := A) P -> sig (A := B) Q;
}.

Variable World : Type.

(* Lift a PureSig to an ArrowSig *)
Definition PureArrowSig A B (p : PureSig A B) (rely_guarantee : Situation (World := World) A -> Frame World) : ArrowSig World A B
  := {| rely := rely_guarantee;
        guarantee := rely_guarantee;
        pre := compose (P _  _ p) snd;
        (* the output value is, in fact, in function
           of the input value. *)
        post := fun t u => exists pf, snd u = proj1_sig (f _ _ p (exist _ (snd t) pf)) |}.

End definitions.

Arguments P { _ _ }.
Arguments Q { _ _ }.
Arguments f { _ _ }.
Arguments PureArrowSig { _ _ _ }.