Commit 860d808b authored by Jonas Kastberg's avatar Jonas Kastberg

Merge branch 'jonas/more_polymorphism' into 'master'

Jonas/more polymorphism

See merge request !13
parents 623b6232 5b787817
Pipeline #27525 passed with stage
in 5 minutes and 45 seconds
......@@ -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
......
From stdpp Require Import base tactics telescopes.
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}
(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).
Arguments ltys : clear implicits.
Definition ktele_app {Σ kt 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} (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} : (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} (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.
Fixpoint ktele_to_tele {Σ} (kt : ktele Σ) : tele :=
match kt with
| KTeleO => TeleO
| KTeleS b => TeleS (λ x, ktele_to_tele (b x))
end.
Fixpoint ltys_to_tele_args {Σ} {kt} (Ks : ltys Σ kt) :
tele_arg (ktele_to_tele kt) :=
match Ks with
| LTysO => TargO
| LTysS K Ks => TargS K (ltys_to_tele_args Ks)
end.
(*
(** 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.
*)
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" :=
......@@ -43,6 +50,9 @@ Notation "<!! X .. Y > M" :=
(<!!> X, .. ( Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200,
format "<!! X .. Y > M") : lty_scope.
Notation "<!!.. X .. Y > M" := (<!!> .. X, .. (.. Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200,
format "<!!.. X .. Y > M") : lty_scope.
Notation "<??> M" :=
(lty_message Recv M) (at level 200, M at level 200) : lty_scope.
......@@ -50,6 +60,9 @@ Notation "<?? X .. Y > M" :=
(<??> X, .. ( Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200,
format "<?? X .. Y > M") : lty_scope.
Notation "<??.. X .. Y > M" := (<??> .. X, .. (.. Y, M) ..)%lty
(at level 200, X closed binder, Y closed binder, M at level 200,
format "<??.. X .. Y > M") : lty_scope.
Notation lty_select := (lty_choice Send).
Notation lty_branch := (lty_choice Recv).
Infix "<++>" := lty_app (at level 60) : lty_scope.
......
......@@ -267,6 +267,39 @@ Section subtyping_rules.
(<??> M A) <: (<?? X> M X).
Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
(* Elimination rules need inhabited variant of telescopes in the model *)
Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt lmsg Σ) S :
( Xs, (<??> M Xs) <: S) -
(<??.. Xs> M Xs) <: S.
Proof.
iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
iApply lty_le_exist_elim_l; iIntros (X).
iApply "IH". iIntros (Xs). iApply "H".
Qed.
Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys Σ kt lmsg Σ) S :
( Xs, S <: (<!!> M Xs)) -
S <: (<!!.. Xs> M Xs).
Proof.
iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
iApply lty_le_exist_elim_r; iIntros (X).
iApply "IH". iIntros (Xs). iApply "H".
Qed.
Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys Σ kt lmsg Σ) Ks :
(<!!.. Xs> M Xs) <: (<!!> M Ks).
Proof.
induction Ks as [|k kT X Xs IH]; simpl; [iApply lty_le_refl|].
iApply lty_le_trans; [by iApply lty_le_exist_intro_l|]. iApply IH.
Qed.
Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys Σ kt lmsg Σ) Ks :
(<??> M Ks) <: (<??.. Xs> M Xs).
Proof.
induction Ks as [|k kt X Xs IH]; simpl; [iApply lty_le_refl|].
iApply lty_le_trans; [|by iApply lty_le_exist_intro_r]. iApply IH.
Qed.
Lemma lty_le_swap_recv_send A1 A2 S :
(<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
Proof.
......
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).
......
......@@ -240,9 +240,9 @@ Section properties.
Qed.
Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k ltty Σ) B :
(Γ1 e1 : lty_exist C Γ2) -
( Y, binder_insert x (C Y) Γ2 e2 : B Γ3) -
Γ1 (let: x := e1 in e2) : B binder_delete x Γ3.
(Γ1 e1 : lty_exist C Γ2) -
( Y, binder_insert x (C Y) Γ2 e2 : B Γ3) -
Γ1 (let: x := e1 in e2) : B binder_delete x Γ3.
Proof.
iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
wp_apply (wp_wand with "(He1 HΓ1)").
......@@ -515,6 +515,40 @@ Section properties.
iExists v, c. eauto with iFrame.
Qed.
Lemma iProto_le_lmsg_texist {kt : ktele Σ} (m : ltys Σ kt iMsg Σ) :
(<?> (.. Xs : ltys Σ kt, m Xs)%lmsg) (<? (Xs : ltys Σ kt)> m Xs).
Proof.
iInduction kt as [|k kt] "IH".
{ rewrite /lty_msg_texist /=. by iExists LTysO. }
rewrite /lty_msg_texist /=. iIntros (X).
iApply (iProto_le_trans with "IH"). iIntros (Xs). by iExists (LTysS _ _).
Qed.
Lemma ltyped_recv_texist {kt} Γ1 Γ2 (xc : string) (x : binder) (e : expr)
(A : ltys Σ kt ltty Σ) (S : ltys Σ kt lsty Σ) (B : ltty Σ) :
( Ys,
binder_insert x (A Ys) (<[xc:=(chan (S Ys))%lty]> Γ1) e : B Γ2) -
<[xc:=(chan (<??.. Xs> TY A Xs; S Xs))%lty]> Γ1
(let: x := recv xc in e) : B binder_delete x Γ2.
Proof.
iIntros "#He !>". iIntros (vs) "HΓ /=".
iDestruct (env_ltyped_lookup with "HΓ") as (c Hxc) "[Hc HΓ]".
{ by apply lookup_insert. }
rewrite Hxc.
iAssert (c <? (Xs : ltys Σ kt) (v : val)>
MSG v {{ ltty_car (A Xs) v }}; lsty_car (S Xs)) with "[Hc]" as "Hc".
{ iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
iApply iProto_le_lmsg_texist. }
wp_recv (Xs v) as "HA". wp_pures.
rewrite -subst_map_binder_insert.
wp_apply (wp_wand with "(He [-]) []").
{ iApply (env_ltyped_insert _ _ x with "HA").
rewrite delete_insert_delete.
iEval (rewrite -(insert_id vs xc c) // -(insert_delete Γ1)).
by iApply (env_ltyped_insert _ _ xc with "[Hc] HΓ"). }
iIntros (w) "[$ HΓ]". by destruct x; [|by iApply env_ltyped_delete].
Qed.
Lemma ltyped_recv Γ (x : string) A S :
<[x := (chan (<??> TY A; S))%lty]> Γ recv x : A <[x:=(chan S)%lty]> Γ.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment