Skip to content
Snippets Groups Projects
Commit a2df6db0 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Revert "Bounded subtyping."

This reverts commit 582ce16e.
parent d20b3324
No related branches found
No related tags found
No related merge requests found
Pipeline #27519 passed
......@@ -49,13 +49,9 @@ Section subtyping_rules.
Qed.
(** Term subtyping *)
Lemma lty_le_bot A : <: A.
Lemma lty_le_any A : A <: any.
Proof. by iIntros (v) "!> H". Qed.
Lemma lty_copyable_bot : ⊢@{iPropI Σ} lty_copyable .
Proof. iApply lty_le_bot. Qed.
Lemma lty_le_top A : A <: .
Proof. by iIntros (v) "!> H". Qed.
Lemma lty_copyable_top : ⊢@{iPropI Σ} lty_copyable .
Lemma lty_copyable_any : ⊢@{iPropI Σ} lty_copyable any.
Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
Lemma lty_le_copy A B : A <: B -∗ copy A <: copy B.
......@@ -133,41 +129,32 @@ Section subtyping_rules.
try iModIntro; first [iLeft; by auto|iRight; by auto].
Qed.
Lemma lty_le_forall {k} (Mlow1 Mup1 Mlow2 Mup2 : lty Σ k) C1 C2 :
Mlow1 <: Mlow2 -∗ Mup2 <: Mup1 -∗
( M, Mlow2 <: M -∗ M <: Mup2 -∗ C1 M <: C2 M) -∗
lty_forall Mlow1 Mup1 C1 <: lty_forall Mlow2 Mup2 C2.
Lemma lty_le_forall C1 C2 :
( A, C1 A <: C2 A) -∗
( A, C1 A) <: ( A, C2 A).
Proof.
iIntros "#Hlow #Hup #Hle" (v) "!> H". iIntros (M) "#Hlow' #Hup'".
iApply wp_step_fupd; first done.
{ iIntros "!> !> !>". iExact "Hle". }
iApply (wp_wand with "(H [] [])").
{ iApply (lty_le_trans with "Hlow Hlow'"). }
{ iApply (lty_le_trans with "Hup' Hup"). }
iIntros (v') "H Hle' !>". by iApply "Hle'".
iIntros "#Hle" (v) "!> H". iIntros (w).
iApply (wp_step_fupd); first done.
{ iIntros "!>!>!>". iExact "Hle". }
iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
by iApply "Hle'".
Qed.
(* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
Lemma lty_le_exist {k} (Mlow1 Mup1 Mlow2 Mup2 : lty Σ k) C1 C2 :
Mlow2 <: Mlow1 -∗ Mup1 <: Mup2 -∗
( M, Mlow1 <: M -∗ M <: Mup1 -∗ C1 M <: C2 M) -∗
lty_exist Mlow1 Mup1 C1 <: lty_exist Mlow2 Mup2 C2.
Lemma lty_le_exist C1 C2 :
( A, C1 A <: C2 A) -∗
( A, C1 A) <: ( A, C2 A).
Proof.
iIntros "#Hlow #Hup #Hle" (v) "!>". iDestruct 1 as (M) "(#Hlow' & #Hup' & H)".
iExists M. iSplit; [|iSplit].
{ iApply (lty_le_trans with "Hlow Hlow'"). }
{ iApply (lty_le_trans with "Hup' Hup"). }
by iApply "Hle".
iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
Qed.
Lemma lty_le_exist_intro {k} (Mlow Mup : lty Σ k) C M :
Mlow <: M -∗ M <: Mup -∗
C M <: lty_exist Mlow Mup C.
Proof. iIntros "#Hlow #Hup !>" (v) "Hle". iExists M. auto. Qed.
Lemma lty_le_exist_copy {k} (Mlow Mup : lty Σ k) C :
lty_exist Mlow Mup (λ M, copy (C M))%lty <:> copy (lty_exist Mlow Mup C).
Lemma lty_le_exist_elim C B :
C B <: A, C A.
Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
Lemma lty_le_exist_copy F :
( A, copy (F A)) <:> copy ( A, F A).
Proof.
iSplit; iIntros "!>" (v);
iDestruct 1 as (A) "#(Hlow & Hup & Hv)"; iExists A; auto.
iSplit; iIntros "!>" (v); iDestruct 1 as (A) "#Hv";
iExists A; repeat iModIntro; iApply "Hv".
Qed.
(* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
......
......@@ -4,8 +4,7 @@ From iris.heap_lang Require Export spin_lock.
From actris.logrel Require Export subtyping.
From actris.channel Require Export channel.
Instance lty_bot {Σ} : Bottom (ltty Σ) := Ltty (λ w, False%I).
Instance lty_top {Σ} : Top (ltty Σ) := Ltty (λ w, True%I).
Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ltty_car A w)%I.
Definition lty_copy_inv {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
......@@ -25,11 +24,10 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
( w1, w = InjLV w1 ltty_car A1 w1)
( w2, w = InjRV w2 ltty_car A2 w2))%I.
Definition lty_forall `{heapG Σ} {k} (Mlow Mup : lty Σ k)
(C : lty Σ k ltty Σ) : ltty Σ :=
Ltty (λ w, M, Mlow <: M -∗ M <: Mup -∗ WP w #() {{ ltty_car (C M) }})%I.
Definition lty_exist {Σ k} (Mlow Mup : lty Σ k) (C : lty Σ k ltty Σ) : ltty Σ :=
Ltty (λ w, M, Mlow <: M M <: Mup ltty_car (C M) w)%I.
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_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
(l : loc) (v : val), w = #l l v ltty_car A v)%I.
......@@ -64,6 +62,7 @@ Instance: Params (@lty_mutex) 3 := {}.
Instance: Params (@lty_mutexguard) 3 := {}.
Instance: Params (@lty_chan) 3 := {}.
Notation any := lty_any.
Notation "()" := lty_unit : lty_scope.
Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
Notation "'copy-' A" := (lty_copy_inv A) (at level 10) : lty_scope.
......@@ -74,11 +73,10 @@ Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
Infix "*" := lty_prod : lty_scope.
Infix "+" := lty_sum : lty_scope.
(* TODO: Have nice notations for bounded quantifiers *)
Notation "∀ A1 .. An , C" :=
(lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope.
(lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope.
Notation "∃ A1 .. An , C" :=
(lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
(lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
......@@ -123,25 +121,20 @@ Section term_types.
Proof. solve_proper. Qed.
Global Instance lty_forall_contractive `{heapG Σ} k n :
Proper (dist n ==> dist n ==> pointwise_relation _ (dist_later n) ==> dist n)
(@lty_forall Σ _ k).
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
Proof.
intros Ml Ml' Hl Mu Mu' Hu C C' HC w. apply Ltty_ne=> v. f_equiv=> M.
do 2 (f_equiv; [by f_equiv|]).
apply (wp_contractive _ _ _ _ _)=> u. specialize (HC M).
intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
by destruct n as [|n]; simpl.
Qed.
Global Instance lty_forall_ne `{heapG Σ} k n :
Proper (dist n ==> dist n ==> pointwise_relation _ (dist n) ==> dist n)
(@lty_forall Σ _ k).
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
Proof. solve_proper. Qed.
Global Instance lty_exist_contractive k n :
Proper (dist n ==> dist n ==> pointwise_relation _ (dist_later n) ==> dist n)
(@lty_exist Σ k).
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
Proof. solve_contractive. Qed.
Global Instance lty_exist_ne k n :
Proper (dist n ==> dist n ==> pointwise_relation _ (dist n) ==> dist n)
(@lty_exist Σ k).
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
Proof. solve_proper. Qed.
Global Instance lty_ref_mut_contractive `{heapG Σ} : Contractive lty_ref_mut.
......
......@@ -202,39 +202,43 @@ Section properties.
Qed.
(** Universal Properties *)
Lemma ltyped_tlam Γ e k Mlow Mup (C : lty Σ k ltty Σ) :
( M, Mlow <: M -∗ M <: Mup -∗ Γ e : C M ) -∗
Γ (λ: <>, e) : lty_forall Mlow Mup C ∅.
Lemma ltyped_tlam Γ e k (C : lty Σ k ltty Σ) :
( M, Γ e : C M ) -∗ Γ (λ: <>, e) : M, C M ∅.
Proof.
iIntros "#He" (vs) "!> HΓ /=". wp_pures.
iSplitL; last by iApply env_ltyped_empty.
iIntros (M) "/= Hlow Hup". wp_pures.
iApply (wp_wand with "(He Hlow Hup HΓ)"). iIntros (v) "[$ _]".
iIntros (M) "/=". wp_pures.
iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
Qed.
Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k ltty Σ) Mlow Mup M :
Mlow <: M -∗ M <: Mup -∗
(Γ e : lty_forall Mlow Mup C Γ2) -∗
Γ e #() : C M Γ2.
Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k ltty Σ) M :
(Γ e : M, C M Γ2) -∗ Γ e #() : C M Γ2.
Proof.
iIntros "#Hlow #Hup #He" (vs) "!> HΓ /=".
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
iApply (wp_wand with "(HB Hlow Hup) [HΓ]"). by iIntros (v) "$".
iApply (wp_wand with "HB [HΓ]"). by iIntros (v) "$".
Qed.
(** Existential properties *)
Lemma ltyped_pack Γ e k (C : lty Σ k ltty Σ) M :
(Γ e : C M) -∗ Γ e : M, C M.
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
Qed.
Definition unpack : val := λ: "exist" "f", "f" #() "exist".
Lemma ltyped_unpack k (C : lty Σ k ltty Σ) Mlow Mup B :
unpack : lty_exist Mlow Mup C lty_forall Mlow Mup (λ M, C M B)%lty B.
Lemma ltyped_unpack k (C : lty Σ k ltty Σ) B :
unpack : ( M, C M) ( M, C M B) B.
Proof.
iIntros (vs) "!> HΓ /=". iApply wp_value.
iSplitL; last by iApply env_ltyped_empty.
iIntros "!>" (v). iDestruct 1 as (M) "(Hlow & Hup & Hv)".
iIntros "!>" (v). iDestruct 1 as (M) "Hv".
rewrite /unpack. wp_pures.
iIntros (fty) "Hfty". wp_pures.
iSpecialize ("Hfty" $! M).
wp_bind (fty _). wp_apply (wp_wand with "(Hfty Hlow Hup)").
wp_bind (fty _). wp_apply (wp_wand with "Hfty").
iIntros (f) "Hf".
wp_apply (wp_wand with "(Hf [Hv //])").
iIntros (w) "HB". iApply "HB".
......@@ -260,7 +264,7 @@ Section properties.
longer use the memory at the old location. *)
Definition load : val := λ: "r", (!"r", "r").
Lemma ltyped_load A :
load : ref_mut A A * ref_mut .
load : ref_mut A A * ref_mut any.
Proof.
iIntros (vs) "!> HΓ /=". iApply wp_value.
iSplitL; last by iApply env_ltyped_empty.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment