Commit 9a99553c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Explicit syntax for pack.

parent f85abf28
...@@ -115,10 +115,11 @@ Section compatibility. ...@@ -115,10 +115,11 @@ Section compatibility.
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A). wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A).
Qed. Qed.
Lemma Pack_sem_typed Γ e C A : Γ e : C A - Γ e : A, C A. Lemma Pack_sem_typed Γ e C A : Γ e : C A - Γ (pack: e) : A, C A.
Proof. Proof.
iIntros "#H" (vs) "!# #HΓ /=". iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iExists A. wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB".
wp_lam. by iExists A.
Qed. Qed.
Lemma Unpack_sem_typed Γ x e1 e2 C B : Lemma Unpack_sem_typed Γ x e1 e2 C B :
(Γ e1 : A, C A) - ( A, binder_insert x (C A) Γ e2 : B) - (Γ e1 : A, C A) - ( A, binder_insert x (C A) Γ e2 : B) -
......
...@@ -155,14 +155,18 @@ Proof. ...@@ -155,14 +155,18 @@ Proof.
auto. auto.
Qed. Qed.
(** We wrap unpack into an explicitly function so that we can have a nice (** We wrap [pack] and [unpack] into an explicitly function so that we can have
notation for it. *) a nice notation for it. *)
Definition exist_pack : val := λ: "x", "x".
Definition exist_unpack : val := λ: "x" "y", "x" "y". Definition exist_unpack : val := λ: "x" "y", "x" "y".
Notation "'pack:' e" := (exist_pack e%E)
(at level 200, e at level 200,
format "'[' 'pack:' e ']'") : expr_scope.
Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (Lam x%binder e2%E) e1%E) Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (Lam x%binder e2%E) e1%E)
(at level 200, x at level 1, e1, e2 at level 200, only parsing, (at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'unpack:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. format "'[' 'unpack:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (LamV x%binder e2%E) e1%E) Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (LamV x%binder e2%E) e1%E)
(at level 200, x at level 1, e1, e2 at level 200, only parsing, (at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'unpack:' x := '[' e1 ']' 'in' '/' e2 ']'") : val_scope. format "'[' 'unpack:' x := '[' e1 ']' 'in' '/' e2 ']'") : val_scope.
...@@ -75,7 +75,7 @@ Inductive typed : gmap string ty → expr → ty → Prop := ...@@ -75,7 +75,7 @@ Inductive typed : gmap string ty → expr → ty → Prop :=
Γ e <_> : ty_subst 0 τ' τ Γ e <_> : ty_subst 0 τ' τ
| Pack_typed Γ e τ τ' : | Pack_typed Γ e τ τ' :
Γ e : ty_subst 0 τ' τ Γ e : ty_subst 0 τ' τ
Γ e : TExist τ Γ (pack: e) : TExist τ
| Unpack_typed Γ e1 x e2 τ τ2 : | Unpack_typed Γ e1 x e2 τ τ2 :
Γ e1 : TExist τ Γ e1 : TExist τ
binder_insert x τ (ty_lift 0 <$> Γ) e2 : ty_lift 0 τ2 binder_insert x τ (ty_lift 0 <$> Γ) e2 : ty_lift 0 τ2
......
...@@ -128,7 +128,7 @@ Section unsafe. ...@@ -128,7 +128,7 @@ Section unsafe.
Definition symbol_adt_inc : val := λ: "x" <>, FAA "x" #1. Definition symbol_adt_inc : val := λ: "x" <>, FAA "x" #1.
Definition symbol_adt_check : val := λ: "x" "y", assert: "y" < !"x". Definition symbol_adt_check : val := λ: "x" "y", assert: "y" < !"x".
Definition symbol_adt : val := λ: <>, Definition symbol_adt : val := λ: <>,
let: "x" := Alloc #0 in (symbol_adt_inc "x", symbol_adt_check "x"). let: "x" := Alloc #0 in pack: (symbol_adt_inc "x", symbol_adt_check "x").
Definition symbol_adt_ty `{heapG Σ} : sem_ty Σ := Definition symbol_adt_ty `{heapG Σ} : sem_ty Σ :=
(() A, (() A) * (A ())). (() A, (() A) * (A ())).
...@@ -151,7 +151,7 @@ Section unsafe. ...@@ -151,7 +151,7 @@ Section unsafe.
iMod (counter_alloc 0) as (γ) "Hc". iMod (counter_alloc 0) as (γ) "Hc".
iMod (inv_alloc symbol_adtN _ (symbol_inv γ l) with "[Hl Hc]") as "#?". iMod (inv_alloc symbol_adtN _ (symbol_inv γ l) with "[Hl Hc]") as "#?".
{ iExists 0%nat. by iFrame. } { iExists 0%nat. by iFrame. }
do 2 (wp_lam; wp_pures). do 2 (wp_lam; wp_pures). wp_lam.
iExists (sem_ty_symbol γ), _, _; repeat iSplit=> //. iExists (sem_ty_symbol γ), _, _; repeat iSplit=> //.
- repeat rewrite /sem_ty_car /=. iIntros "!#" (? ->). wp_pures. - repeat rewrite /sem_ty_car /=. iIntros "!#" (? ->). wp_pures.
iInv symbol_adtN as (n) ">[Hl Hc]". wp_faa. iInv symbol_adtN as (n) ">[Hl Hc]". wp_faa.
......
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