Require Import FunctionalExtensionality.
Require Import Classical.
Require Import coqrel.LogicalRelations.
Require Import coqrel.OptionRel.
Require Import structures.Poset.
Require Import structures.Lattice.
Require Import structures.Effects.
Require Import structures.Monad.
Require Import lattices.Downset.
Require Import lattices.Upset.
Require Import lattices.FCD.
Require Import lattices.LatticeProduct.

Instance bigop_eq {I A B} (f : (I → A) → B) :
  Proper (pointwise_relation I eq ==> eq) f.

(*
(** The discrete poset on a set, currently unused. *)

Module Discrete.

  Record t A := emb { elt : A }.
  Arguments emb {A} _.
  Arguments elt {A} _.

  Instance poset A : Poset (t A) :=
    {
      ref := eq;
    }.
  Proof.
    abstract firstorder.
  Defined.

  Definition ext {A B} (f : A -> B) : t A -> B :=
    fun x => f (elt x).

  Instance mor {A B} `{!Poset B} (f : t A -> B) :
    PosetMorphism f.
  Proof.
    constructor. cbn. rauto.
  Qed.

End Discrete.
*)

(*
(** * Lattice interpretations of effect signature *)

Program Instance option_poset A : Poset (option A) :=
  {
    ref := option_le eq;
  }.
Next Obligation.
  split; typeclasses eauto.
Qed.
Next Obligation.
  intros x y Hxy Hyx.
  destruct Hxy; inversion Hyx; congruence.
Qed.

Class Interp (E : esig) (D : Type) :=
  {
    interp_cdl :> CDLattice D;
    eval : forall {ar}, E ar -> option (ar -> D) -> D;

    eval_sup {ar I} (m : E ar) (k : I -> option (ar -> D)) :
      eval m (fun n => ⋁ i:I; k i n) = ⋁ i:I; eval m (k i);
    eval_inf {ar I} (m : E ar) (k : I -> option ar -> D) :
      eval m (fun n => ⋀ i:I; k i n) = ⋀ i:I; eval m (k i);
  }.

Class InterpMorphism {E : esig} {A B} `{Interp E A} `{Interp E B} (f : A -> B) :=
  {
    int_mor :> CDL.Morphism f;
    eval_mor {ar} (m : E ar) (k : option ar -> A) `{!PosetMorphism k} :
      f (eval m k) = eval m (fun n => f (k n));
  }.
*)

Module ISpec.

  Ltac depsubst :=
    subst;
    lazymatch goal with
      | H : existT _ ?x _ = existT _ ?x _ |- _ ⇒
        apply inj_pair2 in H; depsubst
      | _ ⇒
        idtac
    end.

  Inductive play {E : esig} {V} :=
    | pret (v : V)
    | pmove {X} (m : E X)
    | pcons {X} (m : E X) (n : X) (s : play).

  Arguments play : clear implicits.

  Inductive pref {E : esig} {V} : relation (play E V) :=
    | pret_ref (v : V) :
        pref (pret v) (pret v)
    | pmove_ref {N} (m : E N) :
        pref (pmove m) (pmove m)
    | pmove_cons_ref {N} (m : E N) (n : N) (s : play E V) :
        pref (pmove m) (pcons m n s)
    | pcons_ref {N} (m : E N) (n : N) (s t : play E V) :
        pref s t → pref (pcons m n s) (pcons m n t).

  Instance pref_preo (E : esig) V :
    PreOrder (@pref E V).

  Instance pref_antisym (E : esig) V :
    Antisymmetric (play E V) eq pref.

  Canonical Structure play_poset E V : poset :=
    {|
      ref := @pref E V;
    |}.

  (*
  (** ** Free interpretation *)

  Program Instance ti E V : Interp E (t E V) :=
    {
      eval ar m k :=
        FCD.emb (pmove m) ⊔
        ⋁ n; FCD.ext (fun s => FCD.emb (pmove m n s)) (k n);
    }.

  Next Obligation.
    apply join_ub_l.
  Qed.

  Next Obligation.
    apply antisymmetry.
    - apply join_lub.
  Admitted.

  Next Obligation.
    rewrite <- @Inf.mor. f_equal.
  Admitted.
   *)

  Definition t E V :=
    FCD.F (play_poset E V).

  Definition ret {E A} (a : A) : t E A :=
    FCD.emb (pret a).

  Fixpoint pbind {E A B} (f : A → t E B) (p : play E A) : t E B :=
    match p with
      | pret a ⇒ f a
      | pmove m ⇒
        FCD.emb (pmove m)
      | pcons m n q ⇒
        FCD.emb (pmove m) ||
        FCD.ext (fun s ⇒ FCD.emb (pcons m n s)) (pbind f q)
    end.

  Global Instance pbind_mor E A B (f : A → t E B):
    PosetMorphism (pbind f).

  Definition bind {E A B} (f : A → t E B) : t E A → t E B :=
    FCD.ext (pbind f).

  Instance bind_mor {E A B} (f : A → t E B) :
    CDL.Morphism (bind f).

  Instance bind_mor_params :
    Params (@bind) 1 := { }.

  Lemma bind_ret_r {E A B} (a : A) (f : A → t E B) :
    bind f (ret a) = f a.

  Lemma pbind_ret_l {E A} :
    pbind (@ret E A) = FCD.emb.

  Lemma bind_ret_l {E A} (x : t E A) :
    bind ret x = x.

  Lemma bind_bind {E A B C} (g : B → t E C) (f : A → t E B) (x : t E A) :
    bind g (bind f x) = bind (fun a ⇒ bind g (f a)) x.

  Definition int {E ar} (m : E ar) : t E ar :=
    sup k : option ar,
      match k with
        | Some n ⇒ FCD.emb (pcons m n (pret n))
        | None ⇒ FCD.emb (pmove m)
      end.

  Definition subst (E F : esig) : cdlattice :=
    pi ar, t E ar ^ F ar.

  Fixpoint papply {E F A} (f : subst E F) (s : play F A) : t E A :=
    match s with
      | pret a ⇒ FCD.emb (pret a)
      | pmove m ⇒ bind (fun _ ⇒ bot) (f _ m)
      | pcons m n t ⇒ bind (fun n' ⇒ sup H : n' = n, papply f t) (f _ m)
    end.

  Instance papply_mor {E F A} (f : subst E F) :
    PosetMorphism (@papply E F A f).

  Definition apply {E F A} (f : subst E F) : t F A → t E A :=
    FCD.ext (papply f).

  Instance apply_mor {E F A} (f : subst E F) :
    CDL.Morphism (@apply E F A f).

  Instance apply_mor_params :
    Params (@apply) 1 := { }.

  Definition compose {E F G} (g : subst F G) (f : subst E F) : subst E G :=
    fun ar m ⇒ apply f (g ar m).

  Lemma apply_ret {E F A} (f : subst E F) (a : A) :
    apply f (ret a) = ret a.

  Lemma apply_bind {E F A B} (f : subst E F) (g : A → t F B) (x : t F A) :
    apply f (bind g x) = bind (fun a ⇒ apply f (g a)) (apply f x).

  Lemma apply_int_r {E F ar} (m : F ar) (f : subst E F) :
    apply f (int m) = f ar m.

  Lemma apply_int_l {E A} (x : t E A) :
    apply (@int E) x = x.
  Lemma apply_assoc {E F G A} (f : subst E F) (g : subst F G) (x : t G A) :
    apply f (apply g x) = apply (compose g f) x.

  Lemma compose_int_l {E F} (f : subst E F) :
    compose (@int F) f = f.

  Lemma compose_int_r {E F} (f : subst E F) :
    compose f (@int E) = f.

  Lemma compose_assoc {E F G H} (f : subst E F) (g : subst F G) (h : subst G H) :
    compose (compose h g) f = compose h (compose g f).

End ISpec.

Notation ispec := ISpec.t.