WIP: Polymorphic rule for receive

_CoqProject

@@ -18,6 +18,7 @@ theories/examples/sort_fg.v
 theories/examples/map.v
 theories/examples/map_reduce.v
 theories/logrel/model.v
+theories/logrel/kind_tele.v
 theories/logrel/subtyping.v
 theories/logrel/environments.v
 theories/logrel/term_types.v

theories/logrel/kind_tele.v

+From stdpp Require Import base tactics.
+From actris.logrel Require Import model.
+Set Default Proof Using "Type".
+
+(** NB: This is overkill for the current setting, as there are no
+dependencies between binders, hence we might have just used a list of [kind]
+but might be needed for future extensions, such as for bounded polymorphism *)
+(** Type Telescopes *)
+Inductive ktele {Σ} : Type :=
+  | KTeleO : ktele
+  | KTeleS {k} (binder : lty Σ k → ktele) : ktele.
+
+Arguments ktele : clear implicits.
+
+(** The telescope version of kind types *)
+Fixpoint ktele_fun {Σ} (kt : ktele Σ) (T : Type) : Type :=
+  match kt with
+  | KTeleO => T
+  | KTeleS b => ∀ K, ktele_fun (b K) T
+  end.
+
+Notation "kt -k> A" :=
+  (ktele_fun kt A) (at level 99, A at level 200, right associativity).
+
+(** An eliminator for elements of [ktele_fun].
+    We use a [fix] because, for some reason, that makes stuff print nicer
+    in the proofs in iris:bi/lib/telescopes.v *)
+Definition ktele_fold {Σ X Y} {kt : ktele Σ}
+    (step : ∀ {k}, (lty Σ k → Y) → Y) (base : X → Y) : (kt -k> X) → Y :=
+  (fix rec {kt} : (kt -k> X) → Y :=
+     match kt as kt return (kt -k> X) → Y with
+     | KTeleO => λ x : X, base x
+     | KTeleS b => λ f, step (λ x, rec (f x))
+     end) kt.
+Arguments ktele_fold {_ _ _ !_} _ _ _ /.
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it *)
+(*   takes to get a [T] from a [kt -t> T]. *)
+Inductive ltys {Σ} : ktele Σ → Type :=
+  | LTysO : ltys KTeleO
+  (* the [X] is the only relevant data here *)
+  | LTysS {k} {binder} (K : lty Σ k) :
+      ltys (binder K) →
+      ltys (KTeleS binder).
+
+Definition ktele_app {Σ} {kt : ktele Σ} {T} (f : kt -k> T) : ltys kt → T :=
+  λ Ks, (fix rec {kt} (Ks : ltys kt) : (kt -k> T) → T :=
+     match Ks in ltys kt return (kt -k> T) → T with
+     | LTysO => λ t : T, t
+     | LTysS K Ks => λ f, rec Ks (f K)
+     end) kt Ks f.
+Arguments ktele_app {_} {!_ _} _ !_ /.
+
+(* Coercion ltys : ktele >-> Sortclass. *)
+(* This is a local coercion because otherwise, the "λ.." notation stops working. *)
+(* Local Coercion ktele_app : ktele_fun >-> Funclass. *)
+
+(** Inversion lemma for [tele_arg] *)
+Lemma ltys_inv {Σ} {kt : ktele Σ} (Ks : ltys kt) :
+  match kt as kt return ltys kt → Prop with
+  | KTeleO => λ Ks, Ks = LTysO
+  | KTeleS f => λ Ks, ∃ K Ks', Ks = LTysS K Ks'
+  end Ks.
+Proof. induction Ks; eauto. Qed.
+Lemma ltys_O_inv {Σ} (Ks : ltys (@KTeleO Σ)) : Ks = LTysO.
+Proof. exact (ltys_inv Ks). Qed.
+Lemma ltys_S_inv {Σ} {X} {f : lty Σ X → ktele Σ} (Ks : ltys (KTeleS f)) :
+  ∃ K Ks', Ks = LTysS K Ks'.
+Proof. exact (ltys_inv Ks). Qed.
+(*
+(** Map below a tele_fun *)
+Fixpoint ktele_map {Σ} {T U} {kt : ktele Σ} : (T → U) → (kt -k> T) → kt -k> U :=
+  match kt as kt return (T → U) → (kt -k> T) → kt -k> U with
+  | KTeleO => λ F : T → U, F
+  | @KTeleS _ X b => λ (F : T → U) (f : KTeleS b -k> T) (x : lty Σ X),
+                  ktele_map F (f x)
+  end.
+Arguments ktele_map {_} {_ _ !_} _ _ /.
+Lemma ktele_map_app {Σ} {T U} {kt : ktele Σ} (F : T → U) (t : kt -k> T) (x : kt) :
+  (ktele_map F t) x = F (t x).
+Proof.
+  induction kt as [|X f IH]; simpl in *.
+  - rewrite (ltys_O_inv x). done.
+  - destruct (ltys_S_inv x) as [x' [a' ->]]. simpl.
+    rewrite <-IH. done.
+Qed.
+
+Global Instance ktele_fmap {Σ} {kt : ktele Σ} : FMap (ktele_fun kt) :=
+  λ T U, ktele_map.
+
+Lemma ktele_fmap_app {Σ} {T U} {kt : ktele Σ} (F : T → U) (t : kt -k> T) (x : kt) :
+  (F <$> t) x = F (t x).
+Proof. apply ktele_map_app. Qed.
+*)
+(** Operate below [tele_fun]s with argument telescope [kt]. *)
+Fixpoint ktele_bind {Σ} {U} {kt : ktele Σ} : (ltys kt → U) → kt -k> U :=
+  match kt as kt return (ltys kt → U) → kt -k> U with
+  | KTeleO => λ F, F LTysO
+  | @KTeleS _ k b => λ (F : ltys (KTeleS b) → U) (K : lty Σ k), (* b x -t> U *)
+                  ktele_bind (λ Ks, F (LTysS K Ks))
+  end.
+Arguments ktele_bind {_} {_ !_} _ /.
+
+(* Show that tele_app ∘ tele_bind is the identity. *)
+Lemma ktele_app_bind {Σ} {U} {kt : ktele Σ} (f : ltys kt → U) K :
+  ktele_app (ktele_bind f) K = f K.
+Proof.
+  induction kt as [|k b IH]; simpl in *.
+  - rewrite (ltys_O_inv K). done.
+  - destruct (ltys_S_inv K) as [K' [Ks' ->]]. simpl.
+    rewrite IH. done.
+Qed.
+
+(*
+(** We can define the identity function and composition of the [-t>] function *)
+(* space. *)
+Definition ktele_fun_id {Σ} {kt : ktele Σ} : kt -k> kt := ktele_bind id.
+
+Lemma ktele_fun_id_eq {Σ} {kt : ktele Σ} (x : kt) :
+  ktele_fun_id x = x.
+Proof. unfold ktele_fun_id. rewrite ktele_app_bind. done. Qed.
+
+Definition ktele_fun_compose {Σ} {kt1 kt2 kt3 : ktele Σ} :
+  (kt2 -k> kt3) → (kt1 -k> kt2) → (kt1 -k> kt3) :=
+  λ t1 t2, ktele_bind (compose (ktele_app t1) (ktele_app t2)).
+
+Lemma ktele_fun_compose_eq {Σ} {kt1 kt2 kt3 : ktele Σ} (f : kt2 -k> kt3) (g : kt1 -k> kt2) x :
+  ktele_fun_compose f g $ x = (f ∘ g) x.
+Proof. unfold ktele_fun_compose. rewrite ktele_app_bind. done. Qed.
+*)
+
+(*
+(** Notation-compatible telescope mapping *)
+(* This adds (tele_app ∘ tele_bind), which is an identity function, around every *)
+(*    binder so that, after simplifying, this matches the way we typically write *)
+(*    notations involving telescopes. *)
+Notation "'λ..' x .. y , e" :=
+  (ktele_app (ktele_bind (λ x, .. (ktele_app (ktele_bind (λ y, e))) .. )))
+  (at level 200, x binder, y binder, right associativity,
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e") : stdpp_scope.
+
+
+(** Telescopic quantifiers *)
+Definition ktforall {Σ} {kt : ktele Σ} (Ψ : kt → Prop) : Prop :=
+  ktele_fold (λ (T : kind), λ (b : (lty Σ T) → Prop), (∀ x : (lty Σ T), b x)) (λ x, x) (ktele_bind Ψ).
+Arguments ktforall {_ !_} _ /.
+
+Notation "'∀..' x .. y , P" := (ktforall (λ x, .. (ktforall (λ y, P)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+  format "∀..  x  ..  y ,  P") : stdpp_scope.
+
+Lemma ktforall_forall {Σ} {kt : ktele Σ} (Ψ : kt → Prop) :
+  ktforall Ψ ↔ (∀ x, Ψ x).
+Proof.
+  symmetry. unfold ktforall. induction kt as [|X ft IH].
+  - simpl. split.
+    + done.
+    + intros ? p. rewrite (ltys_O_inv p). done.
+  - simpl. split; intros Hx a.
+    + rewrite <-IH. done.
+    + destruct (ltys_S_inv a) as [x [pf ->]].
+      revert pf. setoid_rewrite IH. done.
+Qed.
+
+(* Teach typeclass resolution how to make progress on these binders *)
+Typeclasses Opaque ktforall.
+Hint Extern 1 (ktforall _) =>
+  progress cbn [ttforall ktele_fold ktele_bind ktele_app] : typeclass_instances.
+*)

theories/logrel/session_types.v

 From iris.algebra Require Export gmap.
-From actris.logrel Require Export model.
+From actris.logrel Require Export model kind_tele.
 From actris.channel Require Export channel.
 
 Definition lmsg Σ := iMsg Σ.
@@ -7,7 +7,10 @@ Delimit Scope lmsg_scope with lmsg.
 Bind Scope lmsg_scope with lmsg.
 
 Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
-  (∃ v, M v)%msg.
+  (∃ X, M X)%msg.
+
+Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys kt → lmsg Σ) : lmsg Σ :=
+  ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M).
 
 Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
   (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
@@ -33,8 +36,12 @@ Instance: Params (@lty_app) 1 := {}.
 Notation "'TY' A ; S" := (lty_msg_base A S)
   (at level 200, right associativity,
    format "'TY'  A  ;  S") : lmsg_scope.
-Notation "∃ x .. y , m" :=
-  (lty_msg_exist (λ x, .. (lty_msg_exist (λ y, m)) ..)%lmsg) : lmsg_scope.
+Notation "∃ X .. Y , M" :=
+  (lty_msg_exist (λ X, .. (lty_msg_exist (λ Y, M)) ..)%lmsg) : lmsg_scope.
+Notation "'∃..' X .. Y , M" :=
+  (lty_msg_texist (λ X, .. (lty_msg_texist (λ Y, M)) .. )%lmsg)
+  (at level 200, X binder, Y binder, right associativity,
+   format "∃..  X  ..  Y ,  M") : lmsg_scope.
 
 Notation "'END'" := lty_end : lty_scope.
 Notation "<!!> M" :=

theories/logrel/term_types.v

 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Export spin_lock.
-From actris.logrel Require Export subtyping.
+From actris.logrel Require Export subtyping kind_tele.
 From actris.channel Require Export channel.
 
 Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
@@ -28,6 +28,8 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I.
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
+Definition lty_texist {Σ} {TT : ktele Σ} (C : kt → ltty Σ) : ltty Σ :=
+  ktele_fold (@lty_exist Σ) (λ x, x) (ktele_bind C).
 
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.

theories/logrel/term_typing_rules.v

@@ -515,7 +515,13 @@ Section properties.
       iExists v, c. eauto with iFrame.
     Qed.
 
-    Lemma ltyped_recv Γ (x : string) A S :
+    Lemma ltyped_recv {kt : ktele Σ} Γ1 Γ2 (c : string) (x : binder) (e : expr)
+          (A : ltys kt → ltty Σ) (S : ltys kt → lsty Σ) (B : ltty Σ) :
+      ⊢ (∀ Ys, binder_insert x (A Ys) (<[c := (chan (S Ys))%lty ]> Γ1) ⊨ e : B ⫤ Γ2) -∗
+        <[c := (chan (<??> ∃.. Xs, TY A Xs; S Xs))%lty]> Γ1 ⊨
+          (let x := recv c in e) : B ⫤ Γ2.
+
+   Lemma ltyped_recv Γ (x : string) A S :
       ⊢ <[x := (chan (<??> TY A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
     Proof.
       iIntros "!>" (vs) "HΓ"=> /=.