Commit dd104e06 authored by Daniël Louwrink's avatar Daniël Louwrink
Browse files

update more typing rules

parent 9d43893c
...@@ -171,7 +171,7 @@ Section subtyping_rules. ...@@ -171,7 +171,7 @@ Section subtyping_rules.
Qed. Qed.
Lemma lty_le_exist C1 C2 : Lemma lty_le_exist C1 C2 :
( A, C1 A <: C2 A) - ( A, C1 A <: C2 A) -
( A, C1 A) <: ( A, C2 A). ( A, C1 A) <: ( A, C2 A).
Proof. Proof.
iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle". iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
...@@ -187,7 +187,7 @@ Section subtyping_rules. ...@@ -187,7 +187,7 @@ Section subtyping_rules.
Qed. Qed.
Lemma lty_copyable_exist (C : ltty Σ ltty Σ) : Lemma lty_copyable_exist (C : ltty Σ ltty Σ) :
( M, lty_copyable (C M)) - lty_copyable (lty_exist C). ( M, lty_copyable (C M)) - lty_copyable (lty_exist C).
Proof. Proof.
iIntros "#Hle". rewrite /lty_copyable /tc_opaque. iIntros "#Hle". rewrite /lty_copyable /tc_opaque.
iApply lty_le_r; last by iApply lty_le_exist_copy. iApply lty_le_r; last by iApply lty_le_exist_copy.
......
...@@ -27,7 +27,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w, ...@@ -27,7 +27,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
Definition lty_forall `{heapG Σ} {k} (C : lty Σ k ltty Σ) : ltty Σ := Definition lty_forall `{heapG Σ} {k} (C : lty Σ k ltty Σ) : ltty Σ :=
Ltty (λ w, A, WP w #() {{ ltty_car (C A) }})%I. Ltty (λ w, A, WP w #() {{ ltty_car (C A) }})%I.
Definition lty_exist {Σ k} (C : lty Σ k ltty Σ) : ltty Σ := Definition lty_exist {Σ k} (C : lty Σ k ltty Σ) : ltty Σ :=
Ltty (λ w, A, ltty_car (C A) w)%I. Ltty (λ w, A, ltty_car (C A) w)%I.
Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
(l : loc) (v : val), w = #l l v ltty_car A v)%I. (l : loc) (v : val), w = #l l v ltty_car A v)%I.
...@@ -130,9 +130,6 @@ Section term_types. ...@@ -130,9 +130,6 @@ Section term_types.
Global Instance lty_forall_ne `{heapG Σ} k n : Global Instance lty_forall_ne `{heapG Σ} k n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k). Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance lty_exist_contractive k n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
Proof. solve_contractive. Qed.
Global Instance lty_exist_ne k n : Global Instance lty_exist_ne k n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k). Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
......
...@@ -15,14 +15,18 @@ Section properties. ...@@ -15,14 +15,18 @@ Section properties.
Implicit Types Γ : gmap string (ltty Σ). Implicit Types Γ : gmap string (ltty Σ).
(** Variable properties *) (** Variable properties *)
(* TODO(TYRULES) *)
Lemma ltyped_var Γ (x : string) A : Lemma ltyped_var Γ (x : string) A :
Γ !! x = Some A Γ x : A <[x := (copy- A)%lty]> Γ. Γ !! x = Some A Γ x : A <[x := (copy- A)%lty]> Γ.
Proof. Proof.
iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=". iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=".
(* iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "[HA HΓ]"; first done. *) iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
(* iApply wp_value. eauto with iFrame. *) iApply wp_value.
Admitted. iAssert (ltty_car (copy- A) v)%lty as "#HAm". { iApply coreP_intro. iApply "HA". }
iFrame "HA".
iDestruct (env_ltyped_insert _ _ x with "HAm HΓ") as "HΓ".
rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
iApply "HΓ".
Qed.
(** Subtyping *) (** Subtyping *)
Theorem ltyped_subsumption Γ Γ2 e τ1 τ2 : Theorem ltyped_subsumption Γ Γ2 e τ1 τ2 :
...@@ -194,26 +198,28 @@ Section properties. ...@@ -194,26 +198,28 @@ Section properties.
iRight. iExists v. auto. iRight. iExists v. auto.
Qed. Qed.
(* TODO(TYRULES) *) (* TODO: This probably requires there to be a rule that allows dropping arbitrary
resources from the postcondition. Check if there is such a rule. *)
Lemma ltyped_case Γ1 Γ2 Γ3 e1 e2 e3 A1 A2 B : Lemma ltyped_case Γ1 Γ2 Γ3 e1 e2 e3 A1 A2 B :
(Γ1 e1 : A1 + A2 Γ2) - (Γ1 e1 : A1 + A2 Γ2) -
(Γ2 e2 : A1 B Γ3) - (Γ2 e2 : A1 B Γ3) -
(Γ2 e3 : A2 B Γ3) - (Γ2 e3 : A2 B Γ3) -
(Γ1 Case e1 e2 e3 : B Γ3). (Γ1 Case e1 e2 e3 : B Γ3).
Proof. Proof.
(* iIntros (vs) "!> HΓ /=". iApply wp_value. *) iIntros "#H1 #H2 #H3" (vs) "!> HΓ1 /=".
(* iSplitL; last by iApply env_ltyped_empty. *) wp_bind (subst_map vs e1).
(* rewrite /paircase. iIntros "!>" (p) "Hp". wp_pures. *) iSpecialize ("H1" with "HΓ1").
(* iIntros (f_left) "Hleft". wp_pures. *) iApply (wp_wand with "H1"). iIntros (s) "[Hs HΓ2]".
(* iIntros (f_right) "Hright". wp_pures. *) iDestruct "Hs" as "[Hs|Hs]"; iDestruct "Hs" as (w ->) "HA"; wp_case.
(* iDestruct "Hp" as "[Hp|Hp]". *) - wp_bind (subst_map vs e2).
(* - iDestruct "Hp" as (w1 ->) "Hp". wp_pures. *) iApply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv HΓ3]".
(* wp_apply (wp_wand with "(Hleft [Hp //])"). *) iApply (wp_wand with "(Hv HA)"). iIntros (v') "HB".
(* iIntros (v) "HB". iApply "HB". *) iFrame "HΓ3 HB".
(* - iDestruct "Hp" as (w2 ->) "Hp". wp_pures. *) - wp_bind (subst_map vs e3).
(* wp_apply (wp_wand with "(Hright [Hp //])"). *) iApply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv HΓ3]".
(* iIntros (v) "HB". iApply "HB". *) iApply (wp_wand with "(Hv HA)"). iIntros (v') "HB".
Admitted. iFrame "HΓ3 HB".
Qed.
(** Universal Properties *) (** Universal Properties *)
Lemma ltyped_tlam Γ e k (C : lty Σ k ltty Σ) : Lemma ltyped_tlam Γ e k (C : lty Σ k ltty Σ) :
...@@ -242,74 +248,69 @@ Section properties. ...@@ -242,74 +248,69 @@ Section properties.
Qed. Qed.
(* TODO(TYRULES) *) (* TODO(TYRULES) *)
(* NOTE: This only works when `x` is a string, not when it is a (more general)
binder. This means that it doesn't work for anonymous binders, but there
really isn't any reason to unpack those anyway. *)
Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 (x : string) e (C : lty Σ k ltty Σ) A : Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 (x : string) e (C : lty Σ k ltty Σ) A :
Γ1 !! x = Some (lty_exist C) Γ1 !! x = Some (lty_exist C)
( X, binder_insert x (C X) Γ1 e : A Γ2) - ( X, binder_insert x (C X) Γ1 e : A Γ2) -
(Γ1 e : A Γ2). (Γ1 e : A Γ2).
Proof. Proof.
(* iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=. *) iIntros (Hx) "#He". iIntros (vs) "!> HΓ".
(* wp_apply (wp_wand with "(He1 HΓ1)"). *) iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HB HΓ]"; first done.
(* iIntros (v) "[HC HΓ2]". *) iDestruct ("HB") as (B) "HB".
(* iDestruct "HC" as (X) "HX". *) iDestruct (env_ltyped_insert _ _ x with "HB HΓ") as "HΓ".
(* wp_pures. *) rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
(* iDestruct (env_ltyped_insert _ _ x with "HX HΓ2") as "HΓ2". *) iApply (wp_wand with "(He HΓ)"). eauto.
(* iDestruct ("He2" with "HΓ2") as "He2'". *) Qed.
(* destruct x as [|x]; rewrite /= -?subst_map_insert //. *)
(* wp_apply (wp_wand with "He2'"). *)
(* iIntros (w) "[HA2 HΓ3]". *)
(* iFrame. *)
(* iApply env_ltyped_delete=> //. *)
Admitted.
(** Mutable Reference properties *) (** Mutable Reference properties *)
(* TODO(TYRULES) *)
Lemma ltyped_alloc Γ1 Γ2 e A : Lemma ltyped_alloc Γ1 Γ2 e A :
(Γ1 e : A Γ2) - (Γ1 e : A Γ2) -
(Γ1 ref e : ref_mut A Γ2). (Γ1 ref e : ref_mut A Γ2).
Proof. Proof.
(* iIntros (vs) "!> HΓ /=". iApply wp_value. *) iIntros "#He" (vs) "!> HΓ1 /=".
(* iSplitL; last by iApply env_ltyped_empty. *) wp_bind (subst_map vs e).
(* iIntros "!>" (v) "Hv". rewrite /alloc. wp_pures. *) iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv HΓ2]".
(* wp_alloc l as "Hl". *) wp_alloc l as "Hl".
(* iExists l, v. iSplit=> //. *) iFrame "HΓ2".
(* iFrame "Hv Hl". *) iExists l, v; iSplit=>//. iFrame "Hv Hl".
Admitted. Qed.
(* The intuition for the any is that the value is still there, but
it no longer holds any Iris resources. Just as in Rust, where a move
might turn into a memcpy, which leaves the original memory
unmodified, but moves the resources, in the sense that you can no
longer use the memory at the old location. *)
Definition load : val := λ: "r", (!"r", "r").
Lemma ltyped_load Γ (x : string) A : Lemma ltyped_load Γ (x : string) A :
Γ !! x = Some (ref_mut A)%lty Γ !! x = Some (ref_mut A)%lty
Γ ! x : A <[x := (ref_mut (copy- A))%lty]> Γ. Γ ! x : A <[x := (ref_mut (copy- A))%lty]> Γ.
Proof. Proof.
(* iIntros (vs) "!> HΓ /=". iApply wp_value. *) iIntros (Hx vs) "!> HΓ".
(* iSplitL; last by iApply env_ltyped_empty. *) iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done.
(* iIntros "!>" (v) "Hv". rewrite /load. wp_pures. *) simpl. rewrite Hv.
(* iDestruct "Hv" as (l w ->) "[Hl Hw]". *) iDestruct "HA" as (l w ->) "[Hl Hw]".
(* wp_load. wp_pures. *) wp_load.
(* iExists w, #l. iSplit=> //. iFrame "Hw". *) iAssert (ltty_car (copy- A) w)%lty as "#HAm".
(* iExists l, w. iSplit=> //. iFrame "Hl". *) { iApply coreP_intro. iApply "Hw". }
(* by iModIntro. *) iFrame "Hw".
Admitted. iAssert (ltty_car (ref_mut (copy- A))%lty #l) with "[Hl]" as "HA".
{ iExists l, w. iSplit=>//. iFrame "Hl HAm". }
Lemma ltyped_store Γ Γ' x e1 e2 A B : iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
iFrame "HΓ".
Qed.
Lemma ltyped_store Γ Γ' (x : string) e A B :
Γ' !! x = Some (ref_mut A)%lty Γ' !! x = Some (ref_mut A)%lty
(Γ e2 : B Γ') - (Γ e : B Γ') -
Γ e1 <- e2 : () <[x := (ref_mut B)%lty]> Γ'. Γ x <- e : () <[x := (ref_mut B)%lty]> Γ'.
Proof. Proof.
(* iIntros (vs) "!> HΓ /=". iApply wp_value. *) iIntros (Hx) "#He". iIntros (vs) "!> HΓ /=".
(* iSplitL; last by iApply env_ltyped_empty. *) wp_bind (subst_map vs e).
(* iIntros "!>" (v) "Hv". rewrite /store. wp_pures. *) iApply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
(* iDestruct "Hv" as (l old ->) "[Hl Hold]". *) iDestruct (env_ltyped_lookup with "HΓ'") as (w Hw) "[HA HΓ']"; first done.
(* iIntros (new) "Hnew". wp_store. *) rewrite Hw.
(* iExists l, new. eauto with iFrame. *) iDestruct "HA" as (l v' ->) "[Hl HA]".
Admitted. wp_store. iSplitR; first done.
iAssert (ltty_car (ref_mut B)%lty #l) with "[Hl HB]" as "HB".
{ iExists l, v. iSplit=>//. iFrame "Hl HB". }
iDestruct (env_ltyped_insert _ _ x with "HB HΓ'") as "HΓ'".
rewrite /binder_insert insert_delete (insert_id _ _ _ Hw).
iFrame "HΓ'".
Qed.
(** Weak Reference properties *) (** Weak Reference properties *)
Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc". Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc".
......
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