Commit e0d15199 authored by Jonas Kastberg's avatar Jonas Kastberg

Refactoring - Moved spar to own file and renamed as par_start

parent fd7dc61d
...@@ -36,6 +36,7 @@ theories/logrel/term_typing_judgment.v ...@@ -36,6 +36,7 @@ theories/logrel/term_typing_judgment.v
theories/logrel/subtyping_rules.v theories/logrel/subtyping_rules.v
theories/logrel/term_typing_rules.v theories/logrel/term_typing_rules.v
theories/logrel/lib/mutex.v theories/logrel/lib/mutex.v
theories/logrel/lib/par_start.v
theories/logrel/examples/double.v theories/logrel/examples/double.v
theories/logrel/examples/pair.v theories/logrel/examples/pair.v
theories/logrel/examples/rec_subtyping.v theories/logrel/examples/rec_subtyping.v
......
From actris.logrel Require Export term_typing_rules environments.
From actris.channel Require Import proofmode.
Section properties.
Context `{heapG Σ}.
Context `{chanG Σ}.
Context `{spawnG Σ}.
Definition par_start : expr :=
(λ: "e1" "e2",
let: "c" := new_chan #() in
let: "c1" := Fst "c" in
let: "c2" := Snd "c" in
("e1" "c1") ||| ("e2" "c2"))%E.
Lemma ltyped_par_start Γ S A B :
Γ par_start : ((chan S) A) (chan (lty_dual S) B) A * B.
Proof.
iApply ltyped_lam; [ iApply env_split_id_l | ].
iApply ltyped_lam; [ iApply env_split_id_r | ].
iApply ltyped_let.
{ iApply ltyped_app; [ iApply ltyped_unit | iApply ltyped_new_chan ]. }
iApply ltyped_let; [ by iApply ltyped_fst | ].
rewrite insert_insert.
iApply ltyped_let; [ by iApply ltyped_snd | ].
rewrite /binder_insert (insert_commute _ "c1" "c") // insert_insert.
iApply (ltyped_par).
- iApply env_split_right; last first.
{ rewrite (insert_commute _ "c1" "e2"); [ | eauto ].
rewrite (insert_commute _ "c" "e2"); [ | eauto ].
iApply env_split_right; last by iApply env_split_id_r.
eauto. eauto. }
eauto. eauto.
- iApply ltyped_app; by iApply ltyped_var.
- iApply ltyped_app; by iApply ltyped_var.
- rewrite insert_insert.
rewrite (insert_commute _ "c2" "e2") // insert_insert.
rewrite (insert_commute _ "c1" "c") // insert_insert.
rewrite (insert_commute _ "c1" "e1") //
(insert_commute _ "c" "e1") // insert_insert.
iApply env_split_left=> //; last first.
iApply env_split_left=> //; last first.
iApply env_split_left=> //; last first.
iApply env_split_id_l.
eauto. eauto. eauto.
Qed.
End properties.
...@@ -6,7 +6,8 @@ From iris.bi.lib Require Import core. ...@@ -6,7 +6,8 @@ From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import metatheory. From iris.heap_lang Require Import metatheory.
From iris.heap_lang.lib Require Export spawn par assert. From iris.heap_lang.lib Require Export spawn par assert.
From actris.logrel Require Export subtyping term_typing_judgment operators session_types. From actris.logrel Require Export subtyping term_typing_judgment operators
session_types.
From actris.logrel Require Import environments. From actris.logrel Require Import environments.
From actris.utils Require Import switch. From actris.utils Require Import switch.
From actris.channel Require Import proofmode. From actris.channel Require Import proofmode.
...@@ -468,51 +469,6 @@ Section properties. ...@@ -468,51 +469,6 @@ Section properties.
iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2". iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
Qed. Qed.
Section with_spawn.
Context `{spawnG Σ}.
Definition spar : expr :=
(λ: "e1" "e2",
let: "c" := new_chan #() in
let: "c1" := Fst "c" in
let: "c2" := Snd "c" in
("e1" "c1") ||| ("e2" "c2"))%E.
Lemma ltyped_spar Γ S A B :
Γ spar : ((chan S) A) (chan (lty_dual S) B) A * B.
Proof.
rewrite /spar.
iApply ltyped_lam; [ iApply env_split_id_l | ].
iApply ltyped_lam; [ iApply env_split_id_r | ].
iApply ltyped_let.
{ iApply ltyped_app; [ iApply ltyped_unit | iApply ltyped_new_chan ]. }
iApply ltyped_let; [ by iApply ltyped_fst | ].
rewrite insert_insert.
iApply ltyped_let; [ by iApply ltyped_snd | ].
rewrite /binder_insert (insert_commute _ "c1" "c") // insert_insert.
iApply (ltyped_par).
- iApply env_split_right; last first.
{ rewrite (insert_commute _ "c1" "e2"); [ | eauto ].
rewrite (insert_commute _ "c" "e2"); [ | eauto ].
iApply env_split_right; last by iApply env_split_id_r.
eauto. eauto. }
eauto. eauto.
- iApply ltyped_app; by iApply ltyped_var.
- iApply ltyped_app; by iApply ltyped_var.
- rewrite insert_insert.
rewrite (insert_commute _ "c2" "e2") // insert_insert.
rewrite (insert_commute _ "c1" "c") // insert_insert.
rewrite (insert_commute _ "c1" "e1") //
(insert_commute _ "c" "e1") // insert_insert.
iApply env_split_left=> //; last first.
iApply env_split_left=> //; last first.
iApply env_split_left=> //; last first.
iApply env_split_id_l.
eauto. eauto. eauto.
Qed.
End with_spawn.
Lemma ltyped_send Γ Γ' (x : string) e A S : Lemma ltyped_send Γ Γ' (x : string) e A S :
Γ' !! x = Some (chan (<!!> TY A; S))%lty Γ' !! x = Some (chan (<!!> TY A; S))%lty
(Γ e : A Γ') - (Γ e : A Γ') -
......
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